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

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

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

The Base Case establishes that `zp`

The Induction Step establishes that if *induction
hypothesis*.

Note that if the Base Case and Induction Step are valid, then we know

There is a duality between recursion and induction that ACL2 exploits. The
fact that the Base and Induction steps above are sufficient to prove

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

When this function is admitted we have to prove that if *measure* of the arguments.
That measure must return an ordinal (see ordinals *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<`

The recursion in **suggests** the induction shown
above: the Base Case is defined by the *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

Note that the term

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

The induction suggested by a term like

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.,

All that matters is (i) how the

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.)

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 *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.