2 
data Nat = Zero | Succ Nat
type Predicate = (Nat -> Bool)

-- forAllNat p = (p n) for every finite defined n :: Nat

implies :: Bool -> Bool -> Bool
implies p q = (not p) || q 

basecase :: Predicate -> Bool
basecase p = p Zero 

jump :: Predicate -> Predicate
jump p n = implies (p n) (p (Succ n)) 

indstep :: Predicate -> Bool
indstep p = forallnat (jump p)

问题：

证明 ifbasecase p和indstep p, 那么forAllNat p

我不明白的是，如果basecase p和indstep p，那么当然forAllNat p应该是True。

我认为basecase p说那P(0)是真的， indstep p说那P(Succ n)是P(n+1)真的而且我们需要证明那P(n)是真的。我对吗？关于如何做到这一点的任何建议？

4

2 回答 2

8

正如 Benjamin Hodgson 所指出的，你无法在 Haskell 中完全证明这一点。但是，您可以用稍强的前提条件来证明一个陈述。我还将忽略Bool.

{-# LANGUAGE GADTs, KindSignatures, DataKinds, RankNTypes, ScopedTypeVariables #-}

data Nat = Z | S Nat

data Natty :: Nat -> * where
  Zy :: Natty 'Z
  Sy :: Natty n -> Natty ('S n)

type Base (p :: Nat -> *) = p 'Z
type Step (p :: Nat -> *) = forall (n :: Nat) . p n -> p ('S n)

induction :: forall (p :: Nat -> *) (n :: Nat) .
             Base p -> Step p -> Natty n -> p n
induction b _ Zy = b
induction b s (Sy n) = s (induction b s n)
于 2016-04-07T17:28:19.383 回答
7

你无法在 Haskell 中证明这一点。（事实证明你可以。）语言没有足够的依赖类型。它是一种编程语言，而不是证明助手。我认为作业可能希望你用铅笔和纸证明它。

不过，您可以在 Agda 中进行操作。

data Nat : Set where
  zero : Nat
  suc : Nat -> Nat

Pred : Set -> Set1
Pred A = A -> Set

Universal : {A : Set} -> Pred A -> Set
Universal {A} P = (x : A) -> P x

Base : Pred Nat -> Set
Base P = P zero
Step : Pred Nat -> Set
Step P = (n : Nat) -> P n -> P (suc n)

induction-principle : (P : Pred Nat) -> Base P -> Step P -> Universal P
induction-principle P b s zero = b
induction-principle P b s (suc n) = s n (induction-principle P b s n)

（你可能会认出induction-principle是Nat的foldr。）

当你登陆 GHC 8 时，你可能会得到一些类似的东西TypeInType。但它不会很漂亮。

于 2016-04-07T17:03:54.920 回答