[Haskell-cafe] Induction (help!)

[Daniel Fischer]

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