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
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
ithat is bigger than the
iin 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
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)).