DOUBLE-REWRITE

Major Section:  MISCELLANEOUS

Logically, double-rewrite is the identity function: (double-rewrite x) is equal to x. However, the ACL2 rewriter treats calls of double-rewrite in the following special manner. When it encounters a term (double-rewrite u), it first rewrites u in the current context, and then the rewriter rewrites the result.

Such double-rewriting is rarely necessary, but it can be useful when rewriting under non-trivial equivalence relations (see equivalence). The following example will illustrate the issue.

; Define an equivalence relation.
(defun my-equiv (x y)
  (equal x y))
(defequiv my-equiv)


; Define a unary function whose argument is preserved by my-equiv.
(defun foo (x)
  (declare (ignore x))
  t)
(defcong my-equiv equal (foo x) 1)


; Define some other unary functions.
(defun g (x) x)
(defun h1 (x) x)
(defun h2 (x) x)


; Prove some lemmas and then disable the functions above.
(defthm lemma-1
  (my-equiv (h1 x) (h2 x)))
(defthm lemma-2
  (foo (h2 x)))
(defthm lemma-3
  (implies (foo x)
           (equal (g x) x)))
(in-theory (union-theories (theory 'minimal-theory)
                           '(lemma-1 lemma-2 lemma-3
                             my-equiv-implies-equal-foo-1)))


; Attempt to prove a simple theorem that follows ``obviously'' from the
; events above.
(thm (equal (g (h1 a)) (h1 a)))

Unfortunately, the proof fails. But fortunately, ACL2 gives the following useful warning when lemma-3 is submitted:

ACL2 Warning [Double-rewrite] in ( DEFTHM LEMMA-3 ...):  In the :REWRITE
rule generated from LEMMA-3, equivalence relation MY-EQUIV is maintained
at one problematic occurrence of variable X in hypothesis (FOO X),
but not at any binding occurrence of X.  Consider replacing that occurrence
of X in this hypothesis with (DOUBLE-REWRITE X).  See :doc double-
rewrite for more information on this issue.

(defthm lemma-3
  (implies (foo (double-rewrite x))
           (equal (g x) x)))

In practice, it should suffice for users to follow the advice given in the ``Double-rewrite'' warnings, by adding calls of double-rewrite around certain variable occurrences. But we do not know if this is could cause inefficiency in large proof efforts. For that reason, and for completeness, it seems prudent to explain more carefully what is going on; and that is what we do for the remainder of this documentation topic.

Details.

The reader who wants these details may first wish to see equivalence for relevant review.

The ACL2 rewriter takes a number of contextual arguments, including the generated equivalence relation being maintained (see congruence) and an association list that maps variables to terms. We call the latter alist the unify-subst because it is produced by unifying (actually matching) a pattern against a current term; let us explain this point by returning to the example above. Consider what happens when the rewriter is given the top-level goal of the thm above.

(equal (g (h1 a)) (h1 a))

(g (h1 a))

Consider what happens now if the hypothesis of lemma-3 is (foo x). To rewrite this hypothesis under a unify-subst of ((x . (h1 a))), it will first rewrite x under this unify-subst. The key observation here is that this rewrite takes place simply by returning the value of x in the unify-subst, namely (h1 a). No further rewriting is done! The efficiency of the ACL2 rewriter depends on such caching of previous rewriting results.

But suppose that, instead, the hypothesis of lemma-3 is (foo (double-rewrite x)). As before, the rewriter dives to the first argument of this call of foo. But this time the rewriter sees the call (double-rewrite x), which it handles as follows. First, x is rewritten as before, yielding (h1 a). But now, because of the call of double-rewrite, the rewriter takes (h1 a) and rewrites it under the empty unify-subst. What's more, because of the defcong event above, this rewrite takes place in a context where it suffices to maintain the equivalence relation my-equiv. This allows for the application of lemma-1, hence (h1 a) is rewritten (under unify-subst = nil) to (h2 a). Popping back up, the rewriter will now rewrite the call of foo to t using lemma-2.

The example above explains how the rewriter treats calls of double-rewrite, but it may leave the unfortunate impression that the user needs to consider each :rewrite or :linear rule carefully, just in case a call of double-rewrite may be appropriate. Fortunately, ACL2 provides a ``[Double-rewrite]'' warning to inform the user of just this sort of situation. If you don't see this warning when you submit a (:rewrite or :linear) rule, then the issue described here shouldn't come up for that rule.

If you do see a ``[Double-rewrite]'' warning, then should you add the indicated call(s) of double-rewrite? At the time of writing this documentation, the answer is not clear. Early experiments with double rewriting suggested that it may be too expensive to call double-rewrite in every instance where a warning indicates that there could be an advantage to doing so. And at the time of this writing, the ACL2 regression suite has over 1300 such warnings (with all books were developed before double-rewrite or the ``[Double-rewrite]'' warning were implemented), which suggests that one can often do fine just ignoring such warnings. However, it seems advisable to go ahead and add the calls of double-rewrite indicated by the warnings unless you run acrossan efficiency problems caused by doing so. Of course, if you decide to ignore all such warnings you can execute the event:
(set-inhibit-warnings "Double-rewrite").

Finally, we note that it is generally not necessary to call double-rewrite in order to get its effect in the following case, where the discussion above might have led one to consider a call of double-rewrite: a hypothesis is a variable, or more generally, we are considering a variable occurrence that is a branch of the top-level IF structure of a hypothesis. The automatic handling of this case, by a form of double rewriting, was instituted in ACL2 Version_2.9 and remains in place with the introduction of double-rewrite. Here is a simple illustrative example. Notice that foo-holds applies to prove the final thm below, even without a call of double-rewrite in the hypothesis of foo-holds, and that there is no ``[Double-rewrite]'' warning when submitting foo-holds.

(encapsulate
 (((foo *) => *)
  ((bar *) => *))


 (local (defun foo (x) (declare (ignore x)) t))
 (local (defun bar (x) (declare (ignore x)) t))


 (defthm foo-holds
   (implies x
            (equal (foo x) t)))
 (defthm bar-holds-propositionally
   (iff (bar x) t)))

(thm (foo (bar y)))