Am Mittwoch, 7. Mai 2008 23:27 schrieb PR Stanley:
> Hi
> One of you chaps mentioned the Nat data type
> data Nat = Zero | Succ Nat
>
> Let's have
> add :: Nat -> Nat -> Nat
> add Zero n = n
> add (Succ m) n = Succ (add m n)
>
> Prove
> add m Zero = m
>
> I'm on the verge of giving up on this. :-(
> Cheers
> Paul
>
Proposition:
forall n. P(n)
, where
P(n): add n Zero = n
Base case: P(Zero)
add Zero Zero = Zero
by definition of add (first clause).
Induction step:
Induction hypothesis is P(n) for some arbitrary, but fixed, n.
Then:
add (Succ n) Zero
= Succ (add n Zero) -- by the second clause of add
= Succ (n) -- by the induction hypothesis
qed
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
