A small proof about mutually recursive functions

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

(mutual-recursion (defun free-vars1 (term ans) (cond ((atom term) (add-to-set-eq term ans)) ((fquotep term) ans) (t (free-vars1-lst (cdr 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

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,

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 that help you to automate this kind of reasoning about mutually recursive functions. See for example make-flag.