Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER
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 insure 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)).
