[Haskell-cafe] Induction (help!)

[Ryan Ingram]

Another way to look at it is that induction is just a way to abbreviate proofs.

Lets say you have a proposition over the natural numbers that may or
may not be true; P(x).

If you can prove P(0), and given P(x) you can prove P(x+1), then for
any given natural number n, you can prove P(n):

<insert proof of P(0) here>
<insert proof of P(0) => P(1) here>
P(1). -- from P(0) and P(0) => P(1)
<proof of P(1) => P(2)>
P(2). -- from P(1) and P(1) => P(2)
...
P(n-1). -- from P(n-2) and P(n-2) => P(n-1).
<proof of P(n-1) => P(n)>
P(n). -- from P(n-1) and P(n-1) => P(n)

The magic thing about induction is that it gives you a unifying
principle that allows you to skip these steps and prove an -infinite-
number of hypotheses; even though the natural numbers is an infinite
set, each number is still finite and therefore is subject to the same
logic above.

One point to remember is that structural induction fails to hold on
infinite data structures:

data Nat = Zero | Succ Nat deriving (Eq, Show)

Take P(x) to be (x /= Succ x).

P(0):
Zero /= Succ Zero. (trivial)

P(x) => P(Succ x)

So, given P(x) which is: (x /= Succ x),
we have to prove P(Succ x): (Succ x /= Succ (Succ x))

In the derived Eq typeclass:
   Succ a /= Succ b = a /= b
Taking "x" for a and "Succ x" for b:
   Succ x /= Succ (Succ x) = x /= Succ x
which is P(x).

Now, consider the following definition:
infinity :: Nat
infinity = Succ infinity

infinity /= Succ infinity == _|_; and if you go by definitional
equality, infinity = Succ infinity, so even though P(x) holds on all
natural numbers due to structural induction, it doesn't hold on this
infinite number.

  -- ryan