So, when you apply the function to the first element in the set - e.g. Zero or Nil in the case of lists - you're actually testing to see the function works. Then in the inductive step you base everything on the assumption that p holds for some n and of course if that's true then p must hold for Succ n but you have to prove this by taking Succ from n and thus going bakc to its predecessor which is also the hypothesis p(n). So, to reiterate assumption: if hypothesis then conclusion if p(n) then p(Succ n) proof of assumption if p(Succ n) = Succ(p(n)) then we've won. If pn+1) = p(n) + p(1) then we have liftoff! I'm not going to go any further in case I'm once again on the wrong track. Cheers Paul At 22:43 07/05/2008, you wrote:

On Wed, May 7, 2008 at 9:27 PM, PR Stanley 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