# [Haskell-cafe] Clarification on proof section of HS: The Craft of FP

Ben Rudiak-Gould Benjamin.Rudiak-Gould at cl.cam.ac.uk
Tue May 3 19:32:53 EDT 2005

```Echo Nolan wrote:
> 	My copy of HS: The Craft Of FP just arrived and I was reading
> section 8.5 about induction. On page 141, Simon Thompson gives a
> method of proving properties of functions on lists:
> 	1) Prove that the property holds for the null list
> 	2) Prove that the property holds for (x:xs) under the assumption
> 		that the property holds for xs.
>
> My question is this: what is the proof of
> (P([]) and ( P(xs) => P(x:xs))) => P(xs)?

Forget all the other replies. :-) The *real* reason that induction is a
valid method of proving properties of lists is that *lists are themselves
defined inductively*. (Except they aren't in Haskell--but let's pretend
we're talking about ML for the moment.)

In ML (with Haskell syntax), when you write

data Nat = Zero | Succ Nat

what it means is something like this:

1. Zero is in Nat.
2. If x is in Nat, then Succ x is in Nat.
3. Nat contains only such elements as can be proven to belong to it by
rules 1 and 2.

For example, Succ Zero is in Nat. Proof: Zero is in Nat (1); if Zero is in
Nat, then Succ Zero is in Nat (instantiation of (2)); Succ Zero is in Nat
(modus ponens). Note that this mirrors the way the value is actually
constructed in program code (the Curry-Howard isomorphism).

Now, suppose you've proven

A. P(Zero).
B. P(x) => P(Succ x).

Let n be any element of Nat. By rule 3, there is a proof that n belongs to
Nat. Take that proof, and replace every occurrence of "x is in Nat" with
"P(x)". The result will be a proof of P(n).

In other words, the inductive structure of the type ensures that we can
construct a proof of P(n) for any n in the type by gluing together a finite
number of primitive pieces (one for each data constructor). This is why it's
sufficient to prove just A and B, and why they have this particular form.