Major Section: TUTORIAL5-MISCELLANEOUS-EXAMPLES

Sometimes one wants to reason about mutually recursive functions. Although this is possible in ACL2, it can be a bit awkward. This example is intended to give some ideas about how one can go about such proofs.

For an introduction to mutual recursion in ACL2, see mutual-recursion.

We begin by defining two mutually recursive functions: one that
collects the variables from a term, the other that collects the
variables from a list of terms. We actually imagine the term
argument to be a `pseudo-termp`

; see pseudo-termp.

(mutual-recursionThe idea of the following function is that it suggests a proof by induction in two cases, according to the top-level(defun free-vars1 (term ans) (cond ((atom term) (add-to-set-eq term ans)) ((fquotep term) ans) (t (free-vars1-lst (fargs term) ans))))

(defun free-vars1-lst (lst ans) (cond ((atom lst) ans) (t (free-vars1-lst (cdr lst) (free-vars1 (car lst) ans)))))

)

`if`

structure of
the body. In one case, `(atom x)`

is true, and the theorem to be
proved should be proved under no additional hypotheses except for
`(atom x)`

. In the other case, `(not (atom x))`

is assumed together
with three instances of the theorem to be proved, one for each
recursive call in this case. So, one instance substitutes `(car x)`

for `x`

; one substitutes `(cdr x)`

for `x`

; and the third substitutes
`(cdr x)`

for `x`

and `(free-vars1 (car x) ans)`

for `ans`

. If you think
about how you would go about a hand proof of the theorem to follow,
you'll come up with a similar scheme.
(defun symbol-listp-free-vars1-induction (x ans) (if (atom x) ; then we just make sure x and ans aren't considered irrelevant (list x ans) (list (symbol-listp-free-vars1-induction (car x) ans) (symbol-listp-free-vars1-induction (cdr x) ans) (symbol-listp-free-vars1-induction (cdr x) (free-vars1 (car x) ans)))))We now prove the two theorems together as a conjunction, because the inductive hypotheses for one are sometimes needed in the proof of the other (even when you do this proof on paper!).

(defthm symbol-listp-free-vars1 (and (implies (and (pseudo-termp x) (symbol-listp ans)) (symbol-listp (free-vars1 x ans))) (implies (and (pseudo-term-listp x) (symbol-listp ans)) (symbol-listp (free-vars1-lst x ans)))) :hints (("Goal" :induct (symbol-listp-free-vars1-induction x ans))))The above works, but let's try for a more efficient proof, which avoids cluttering the proof with irrelevant (false) inductive hypotheses.

(ubt 'symbol-listp-free-vars1-induction)We now state the theorem as a conditional, so that it can be proved nicely using the induction scheme that we have just coded. The prover will not store an(defun symbol-listp-free-vars1-induction (flg x ans)

; Flg is non-nil (or t) if we are ``thinking'' of a single term.

(if (atom x) (list x ans) (if flg (symbol-listp-free-vars1-induction nil (cdr x) ans) (list (symbol-listp-free-vars1-induction t (car x) ans) (symbol-listp-free-vars1-induction nil (cdr x) (free-vars1 (car x) ans))))))

`if`

term as a rewrite rule, but that's OK
(as long as we tell it not to try), because we're going to derive
the corollaries of interest later and make (defthm symbol-listp-free-vars1-flg (if flg (implies (and (pseudo-termp x) (symbol-listp ans)) (symbol-listp (free-vars1 x ans))) (implies (and (pseudo-term-listp x) (symbol-listp ans)) (symbol-listp (free-vars1-lst x ans)))) :hints (("Goal" :induct (symbol-listp-free-vars1-induction flg x ans))) :rule-classes nil)And finally, we may derive the theorems we are interested in as immediate corollaries.

(defthm symbol-listp-free-vars1 (implies (and (pseudo-termp x) (symbol-listp ans)) (symbol-listp (free-vars1 x ans))) :hints (("Goal" :by (:instance symbol-listp-free-vars1-flg (flg t)))))(defthm symbol-listp-free-vars1-lst (implies (and (pseudo-term-listp x) (symbol-listp ans)) (symbol-listp (free-vars1-lst x ans))) :hints (("Goal" :by (:instance symbol-listp-free-vars1-flg (flg nil)))))