		Search-engine friendly clone of the ACL2 documentation.

Introduction-to-the-theorem-prover

Example-induction-scheme-nat-recursion

Induction on natural numbers

See logic-knowledge-taken-for-granted-inductive-proof for an explanation of what we mean by the induction suggested by a recursive function or a term.

Classical Induction on Natural Numbers: Induction is familiar in the arithmetic setting. 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.

A function that suggests this induction is

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

Similarly, the term (fact n) suggests this induction if fact is defined:

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

even though the formal parameter of this definition of fact is k, not n.