LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-INDUCTIVE-PROOF

Major Section:  INTRODUCTION-TO-THE-THEOREM-PROVER

We start by showing classical induction on the natural numbers in an ACL2 setting before turning to a more general treatment of induction.

Classical Induction on Natural Numbers: Induction is familiar in the arithmetic setting. Let (p n) denote some formula involving the variable n (and perhaps some other variables which we don't exhibit). Then to prove (p n), for all n, by classical induction on the construction of the natural numbers, prove each of the following:

Base Case:
(implies (zp n) (p n))

Induction Step:
(implies (and (not (zp n))
              (p (- n 1)))
         (p n))

The Induction Step establishes that if n is a natural number other than 0, and if p holds for n-1, then p holds for n. The hypothesis (p (- n 1)) above is called the induction hypothesis.

Note that if the Base Case and Induction Step are valid, then we know (p n), for all n. You can convince yourself of this by picking any object and asking ``how do I know p holds for this object?'' For example, (p -7), (p 'abc), and (p 0) are all established by the Base Case. What about (p 1)? That follows from (p 0), given the Induction Step. Why? To prove (p 1) using the Induction Step, you have to establish (not (zp 1)), which is true, and (p (- 1 1)), which is (p 0), which is true by the Base Case. So (p 1) is true. Similar reasoning proves (p 2) from from (p 1), etc. Clearly, for every natural number other than 0 we could reason like this to show that p holds. Since the Base Case handled all the objects that are not natural numbers, and handled 0, we know (p n), for all n.

There is a duality between recursion and induction that ACL2 exploits. The fact that the Base and Induction steps above are sufficient to prove p for all objects is related to the fact that the following recursion defines a total, terminating function:

(defun nat-recursion (n)
  (if (zp n)
      n
      (nat-recursion (- n 1))))

When this function is admitted we have to prove that if (zp n) does not hold, then (- n 1) is smaller, in some sense, than n. This sense of ``smaller'' is determined by some measure of the arguments. That measure must return an ordinal (ordinals ), but the most common measures return natural numbers, which are among the ordinals. Furthermore, that measure should insure that the terms in the recursive calls are smaller than the formals, i.e., the measure of (- n 1) must be smaller than the measure of n, when the recursive branches are taken. This sense of ``smaller'' must be well-founded: it must be impossible to have an infinitely descending chain of smaller things. This is true of the less-than relation on the ordinals (see o< ). Well-foundedness means that eventually any recursion must ``bottom out'' because things can't keep getting smaller forever.

The recursion in nat-recursion suggests the induction shown above: the Base Case is defined by the if branch that does not lead to a recursive call. The Induction Step is defined by the other branch. The induction hypothesis is defined by what we recur on, i.e., (- n 1). The theorems proved when nat-recursion is introduced justify the classical induction scheme noted above.

Every recursively defined ACL2 function suggests a legal induction and vice versa.

Furthermore, every call of a recursively defined function on distinct variable symbols also suggests a legal induction: just take the induction suggested by the function's recursive definition after renaming the formal parameters to be the variables in the call.

For example, it should be clear that (nat-recursion a) suggests a Base Case defined by (zp a), and induction step defined by (not (zp a)) and an induction hypothesis about (- a 1).

Note that the term (fact n) suggests the same classical induction on natural numbers shown above, where fact is defined as follows (even though we've used the formal parameter k below).

(defun fact (k)
  (if (zp k)
      1
      (* k (fact (- k 1)))))

The induction suggested by a function or term is insensitive to the value returned by the function or term.

It doesn't matter what the function returns in its ``base case'' (e.g., 1 in fact) or what the function ``does'' to its recursive call (e.g., multiply by k in the defun of fact).

All that matters is (i) how the if structure breaks down the cases on k, (ii) which branches lead to recursion, and (iii) what arguments are passed to the recursive calls. Those things determine (i) the case analysis of the induction scheme, (ii) which cases are Base Cases and which are Induction Steps, and (iii) what the induction hypotheses are.

For a selection of common inductions schemes in ACL2 (e.g., on the structure of natural numbers, lists, and trees and on several variables at once, multiple base cases, multiple induction hypotheses, multiple induction steps, etc.) check this link.

Every legal ACL2 induction corresponds to an admissible recursive function and vice versa. Similarly, every legal ACL2 induction corresponds to a call of a recursively defined function on distinct variables.

ACL2 chooses which induction to do by looking at the terms that occur in the conjecture. For many elementary theorems, ACL2 chooses the right induction by itself.

You may occasionally need to tell it what induction to do. You do that by showing it a term that suggests the induction you want. We'll explain how you communicate this to ACL2 later. If you understand how recursive functions suggest inductions, then you know what you need to know to use ACL2.

The main point of this discussion of induction is familiarize you with the basic terms: Base Case (of which there may be several), Induction Step (of which there may be several), Induction Hypothesis (of which there may be several in each Induction Step), measure and well-founded relation justifying an induction, and the induction suggested by a term or recursive function definition. Furthermore, every Induction Hypothesis is always an instance of the conjecture being proved: each induction hypothesis is obtained from the conjecture being proved by applying a substitution replacing variables by terms.

If you are reviewing the material taken for granted about logic while working your way through the introduction to the theorem prover, please use your browser's Back Button to return to the example proof in logic-knowledge-taken-for-granted.