[Haskell-cafe] Induction (help!)

[Dan Weston]

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