#### MUTUAL-RECURSION-PROOF-EXAMPLE

a small proof about mutually recursive functions
```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)
((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 `(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`.