Paul, Sometimes it helps to go exhaustively through every detail to be sure there is no magic going on. Proceed only if you want exhaustive detail... If it seems that people are skipping some steps in their argument, it is because they are! They already understand it so well that they forgot to add them. Here is what I believe is an excruciatingly complete proof, to assure you that no handwaving is going on. The values of Nat are defined inductively on their structure, using its initial algebra. Take the data type definition data Nat = Zero | Succ Nat There is actually an implied undefined as well, so this is really Nat = undefined | Zero | Succ Nat Just as 3 = const 3 x for any x, we can convert from pointed to pointfree notation (i.e. go from a recursive definition to a least-defined fixed point definition): f = const undefined | const Zero | Succ Nat = LFP (m -> infinity) ( f^m undefined ) [ For the notationally picky, I am using | instead of + in the functor for clarity, which causes no ambiguity.] Because we are overachievers, we will prove our theorem not just for the least-defined fixed point of f, but change the limit to a union and prove it for (f^m undefined) for every m, which includes the fixed point. Why the extra work? Because now we have an inductive argument. The base case is undefined, and each step is another application of f. DEFINITION: add Zero n = n -- Line 1 add (Succ m) n = Succ (add m n) -- Line 2 THEOREM: forall x :: Nat, add x Zero = x PROOF: By induction BASE CASE: x = f^0 undefined = undefined add undefined Zero = undefined { Line 1, strict pattern match failure in first arg } STEP CASE: Assume add x Zero = x, Prove add y Zero = y where y in f x What y are in f x? f x = (const undefined | const Zero | Succ) x = const undefined x | const Zero x | Succ x = undefined | Zero | Succ x We have to consider each of these possibilities for y. 1) add undefined Zero = undefined { Base case } 2) add Zero Zero = Zero { Def. line 1 } 3) add (Succ x) Zero = Succ (add x Zero) { Def. line 2 } = Succ x { Step case assumption } This exhausts the three cases for y. Therefore, by induction add x Zero = x for all x :: Nat Note how structural induction maps to induction over integers. You do not have to enumerate some flattened form of the domain and do induction over their enumerated order. Indeed, some domains (like binary trees) are not even countably infinite, so the induction hypothesis would not be valid when used in this way. Instead you rely on the fact that all algebraic data types already have an (at most countably infinite) complete partial order based on constructor application (or eqivalently, initial algebra composition) [and always remembering that there is an implied union in | with undefined], grounded at undefined, and that consequently you can do induction over constructor application. I hope that there are no errors in the above and that I have not left out even the smallest detail. You should be able to see from the above that structural induction works on any algebraic data type. Obviously, after the first time only a masochist would be so verbose. But the induction hypothesis does after all require a first time! :) Dan Weston PR Stanley 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
I'm on the verge of giving up on this. :-( Cheers Paul