A brief explanation of induction
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:
(implies (zp n) (p n))
(implies (and (not (zp n))
(p (- n 1)))
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
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)
(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 (see ordinals ),
but the most common measures return natural numbers, which are among the
ordinals. Furthermore, that measure should ensure 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
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)
(* 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
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.