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 them into rewrite rules.
(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.
