On Wed, May 7, 2008 at 9:27 PM, PR Stanley <[EMAIL PROTECTED]> wrote: > 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
To prove this by induction on m, you would need to show: 1) add Zero Zero = Zero 2) If "add m Zero = m", then "add (Succ m) Zero = Succ m" Number (1) is completely trivial, nothing more needs to be said. (2) is easy, after expanding the definition. Here the P I used was P(x) := add m Zero = m, the thing we were trying to prove. (1) is a base case, P(Zero). (2) is the inductive step, "If P(m) then P(Succ m)". Hoping I don't sound patronizing: if you're still having trouble, then I suspect you haven't heard what it means to prove an "if-then" statement. Here's a silly example. We want to prove: If y = 10, then y - 10 = 0. First we *assume* the condition of the if. We can consider it true. Assume y = 10. Show y - 10 = 0. Well, y = 10, so that's equivalent to 10 - 10 = 0, which is true. Luke _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe