[Haskell-cafe] Induction (help!)

[Ryan Ingram]

On 5/8/08, Daniel Fischer <daniel.is.fischer at web.de> wrote:
> No. In the induction step, we prove that
> IF p(j) holds, THEN p(j+1) holds, too.
> p(j) is the assumption, and we prove that *given that assumption*, p(j+1)
> follows.
> Then we have proved
> (*) p(j) implies p(j+1), for all j.

To formalize this, you can work in a system of logic with the following rules:

Variable introduction:
   x is not free in L,
   L |- t is a type
   proves
   L, x :: t |- x :: t     --- this is a proof of "x has type t"

Forall introduction (removing the above assumption)
   L, x :: t |- p
   proves
   L |- forall x :: t. p

Assumption of a proposition:
   L, p |- p    --- no pre-requisites

Impication introduction ("Deduction"; if P then Q)
   L, p |- q
   proves
   L |- p => q

The part to the left of the |- is an "environment"; it represents
assumptions you have made up to this point.   The part to the right is
a statement which is "true" in that environment; the L just represents
"any environment".

For example, in the first rule, we say that if we know that t is a
type, and we haven't assumed anything about x yet, we can assume that
x is a member of that type.  Then in the second rule, if we've proved
some proposition "p" once we've assumed that x is something of type t,
we can say that p holds for -all- x of type t; we didn't assume
anything about that x besides its type.

Induction corresponds to adding the following rule to the logic:

L |- p(0)
L |- forall x :: Nat, p(x) => p(x+1)
proves
L |- forall x :: Nat, p(x)

A "true" statement is one that holds with no environment:
|- p

Now, if you are proving something by induction, you had to prove that
second line; and the only way to do so is by making some assumptions.
A skeleton of a proof:

axiom
|- Nat is a type

variable introduction
x :: Nat |- x :: Nat

proposition introduction
x :: Nat, p(x) |- p(x)

... some proof using p(x) here ...
x :: Nat, p(x) |- p(x+1)

deduction
x :: Nat |- p(x) => p(x+1)

forall introduction
|- forall x :: Nat, p(x) => p(x+1)

... some proof of p(0) here ...
|- p(0)

induction
|- forall x :: Nat, p(x)

Every proof by induction looks basically like this; you just need to
fill in the "... some proof here..." parts.

  -- ryan