[Haskell-cafe] Induction (help!)

[Ryan Ingram]

On 5/9/08, Daniel Fischer <daniel.is.fischer at web.de> wrote:
> Right. I only wanted to say that we might have chosen the wrong base case for
> the proposition. If p(0) doesn't hold, then obviously [for all n. p(n)]
> doesn't hold. But [for all n. p(n) implies p(n+1)] could still be true, and
> in that case, if e.g. p(3) holds, then [for all n >= 3. p(n)] holds.
> So if the base case fails, still a large portion of the proposition might be
> saved, but if the induction step fails, that is not so.

Note that this is reasonably trivial to translate into a regular
inductive proof:

let q(x) = p(x) OR (x < 3).
given forall y :: Nat, (y >= 3) => p(y) => p(y+1)
given p(3)

given x :: Nat, and q(x)
x < 2 or x == 2 or x > 2

case (x < 2):
    x+1 <= 2
    q(x+1) holds trivially; x+1 < 3.
case (x == 2)
    x+1 == 3
    p(3) holds (given)
    therefore q(3) holds
    therefore q(x+1) holds
case (x > 2)
    q(x) holds, so either p(x) holds or (x < 3).
    case (x < 3):
        x > 2 and x < 3 is a contradiction.
    case q(x) holds:
        forall y :: Nat, (y >= 3) => p(y) => p(y+1) (given)
        (x >= 3) => p(x) => p(x+1)  (instantiate with y <- x)
        (x >= 3) (since x > 2)
        p(x+1)  (derive from p(x) and x >= 3 and the instantiation)
        (x < 3) or p(x+1)
        therefore q(x+1)

so, forall x::Nat, q(x) => q(x+1).
p(0) is trivial (x < 3).

so, forall x::Nat, q(x)
which means forall x :: Nat, x >= 3 => p(x).

  -- ryan