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-recursion (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))))) )Now suppose that we want to prove the following theorem.

(defthm symbol-listp-free-vars1-try-1 (implies (and (pseudo-termp x) (symbol-listp ans)) (symbol-listp (free-vars1 x ans))))Often ACL2 can generate a proof by induction based on the structure of definitions of function symbols occurring in the conjecture. In this case, ACL2 chooses to use an induction scheme suggested by

`(symbol-listp ans)`

,
and sadly, that doesn't work. If one were doing this proof with pencil and
paper, one would be more likely to prove a combination of the conjecture
above and an analogous conjecture about free-vars1-lst. Feel free to try a
pencil and paper proof! Or you can read on, to see how one can get ACL2 to
do such a proof after all.The trick is to define a function that suggests an appropriate induction. The induction suggested is based on the if-then-else structure of the function's definition, where inductive hypotheses are generated for recursive calls -- below we explain how that works for this function.

(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)))))The if-then-else structure of this function generates two cases. 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 other words,
`(atom x)`

gives us the base case of the induction. In the other case,
`(not (atom x))`

is assumed together with three instances of the theorem to
be proved, one for each recursive call. 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 likely come up with a similar scheme.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 we conclude by illustrating a more efficient approach, in which we restrict to appropriate inductive hypotheses for each case.

(ubt 'symbol-listp-free-vars1-induction) (defun symbol-listp-free-vars1-induction (flg x ans) ; Flg is nil if we are ``thinking'' of a single term. (if (atom x) ; whether x is a single term or a list of terms (list x ans) (if flg ; i.e., if x is a list of terms (list (symbol-listp-free-vars1-induction nil (car x) ans) (symbol-listp-free-vars1-induction t (cdr x) (free-vars1 (car x) ans))) (symbol-listp-free-vars1-induction t (cdr x) ans))))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

`IF`

term as a rewrite rule, but that's OK (provided
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-term-listp x) (symbol-listp ans)) (symbol-listp (free-vars1-lst x ans))) (implies (and (pseudo-termp x) (symbol-listp ans)) (symbol-listp (free-vars1 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 nil))))) (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 t)))))

You may find community books (see community-books that help you to automate
this kind of reasoning about mutually recursive functions. See for example
the community book `tools/flag.lisp`

.