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 Base Case establishes that p holds for 0. In fact, because of
the definition of zp , it establishes that (p n) holds when
n is 0 and it holds when n is not a natural number.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 term like (fact n) is insensitive to the
name of the formal parameter used in the defun.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.
