PR Stanley prstanley at ntlworld.com
Wed May 7 20:01:26 EDT 2008

```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 <prstanley at ntlworld.com> 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
> >
> >  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

```