[Haskell-cafe] Clarification on proof section of HS: The Craft
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
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).
More information about the Haskell-Cafe