Re: [Haskell-cafe] Induction (help!)

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