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)
         (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)))))


)
The idea of the following function is that it suggests a proof by induction in two cases, according to the top-level 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)


(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))))))
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 (as long as 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-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)))))