Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER
Here are some pages illustrating various induction schemes suggested by recursive functions.
Classical Induction on Natural Numbers: see example-induction-scheme-nat-recursion.
Induction Preserving Even/Odd Parity or
Induction Downwards by 2 or
Induction with Multiple Base Cases:
see example-induction-scheme-down-by-2 for an induction in which the
induction hypothesis decreases the induction variable by an amount other
than 1. This illustrates that the induction hypothesis can be about
whatever term or terms are needed to explain how the formula recurs. The
example also illustrates an induction with more than one Base Case.
Classical Induction on Lists:
see example-induction-scheme-on-lists for an induction over linear lists,
in which we inductively assume the conjecture for (cdr x) and prove it
for x. It doesn't matter whether the list is nil-terminated or not;
the Base Case addresses all the possibilities.
Classical Induction on Binary (Cons) Trees: see example-induction-scheme-binary-trees for an induction over the simplest form of binary tree. Here the Induction Step provides two hypotheses, one about the left subtree and one about the right subtree.
Induction on Several Variables: see example-induction-scheme-on-several-variables for an induction in which several variables participate in the case analysis and induction hypotheses.
Induction Upwards: see example-induction-scheme-upwards for an induction scheme in which the induction hypothesis is about something ``bigger than'' the induction conclusion. This illustrates that the sense in which the hypothesis is about something ``smaller'' than the conclusion is determined by a measure of all the variables, not the magnitude or extent of some single variable.
Induction with Auxiliary Variables or
Induction with Accumulators:
see example-induction-scheme-with-accumulators for an induction scheme in which
one variable ``gets smaller'' but another is completely arbitrary. Such schemes
are common when dealing with tail-recursive functions that accumulate partial
results in auxiliary variables. This example also shows how to provide
several arbitrary terms in a non-inductive variable of a scheme.
Induction with Multiple Induction Steps: see example-induction-scheme-with-multiple-induction-steps for an induction in which we make different inductive hypotheses depending on which case we're in. This example also illustrates the handling of auxiliary variables or accumulators.