[Haskell-cafe] Induction (help!)

[Luke Palmer]

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
>  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