		Search-engine friendly clone of the ACL2 documentation.

Introduction-to-the-theorem-prover

Example-induction-scheme-upwards

Induction upwards

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.

Induction Upwards: To (p i max) for all i and all max, prove each of the following:

Base Case: 
(implies (not (and (natp i) 
                   (natp max) 
                   (< i max))) 
         (p i max))

Induction Step: 
(implies (and  (natp i) 
               (natp max) 
               (< i max) 
               (p (+ i 1) max)) 
         (p i max))

Note that the induction hypothesis is about an i that is bigger than the i in in the conclusion. In induction, as in recursion, the sense of one thing being ``smaller'' than another is determined by an arbitrary measure of all the variables, not the magnitude or extent of some particular variable.

A function that suggests this induction is shown below. ACL2 has to be told the measure, namely the difference between max and i (coerced to a natural number to ensure that the measure is an ordinal).

(defun count-up (i max)
  (declare (xargs :measure (nfix (- max i))))
  (if (and (natp i)
           (natp max)
           (< i max))
      (cons i (count-up (+ 1 i) max))
      nil)).