EXAMPLE-INDUCTION-SCHEME-WITH-ACCUMULATORS.html -- ACL2 Version 6.2

EXAMPLE-INDUCTION-SCHEME-WITH-ACCUMULATORS

induction scheme with accumulators

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.

To prove (p x a) for all x and all a, prove each of the following:

Base Case:
(implies (endp x)
         (p x a))

Induction Step:
(implies (and (not (endp x))
              (p (cdr x) (cons (car x) a)))
         (p x a))

Note that in the induction hypothesis we assume p for a smaller x but a larger a. In fact, we could include as many induction hypotheses as we want and use any terms we want in the a position as long as the x position is occupied by a smaller term.

A function that suggests this particular induction is shown below.

(defun rev1 (x a)
  (if (endp x)
      a
      (rev1 (cdr x) (cons (car x) a)))).

A function that suggests a similar induction in which three induction hypotheses are provided, one in which the a position is occupied by (cons (car x) a), another in which the a position is occupied by some arbitrary term b, and a third in which the a position is occupied by a, is suggested by the term (rev1-modified x a b) where

(defun rev1-modified (x a b)
  (if (endp x)
      (list x a b)
      (list (rev1-modified (cdr x) (cons (car x) a) b)
            (rev1-modified (cdr x) b b)
            (rev1-modified (cdr x) a b))))

Remember that the value of this term or function is irrelevant to the induction suggested. Because ACL2's definitional principle insists that all the formal parameters play a role in the computation (at least syntactically), it is common practice when defining functions for their induction schemes to return the list of all the formals (to insure all variables are involved) and to combine recursive calls on a given branch with list (to avoid introducing additional case analysis as would happen if and or or or other propositional functions are used).

If you tried to prove (p x a) and suggested the induct hint (rev1-modified x a (fact k)), as by

(thm (p x a)
     :hints (("Goal" :induct (rev1-modified x a (fact k)))))

the inductive argument would be:

Base Case:
(implies (endp x)
         (p x a))

 Inductive Step:
 (implies (and (not (endp x))
               (p (cdr x) (cons (car x) a))
               (p (cdr x) (fact k))
               (p (cdr x) a))
          (p x a))