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

[Ben Rudiak-Gould]

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.

This doesn't work in Haskell because Haskell types aren't constructed in 
this way. It's harder to prove properties of types in Haskell (and fewer 
properties actually hold).

-- Ben