DOUBLE-REWRITE

cause a term to be rewritten twice
```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)))
```
We might expect the proof of this final `thm` to succeed by the following reasoning. it is immediate from `lemma-3` provided we can establish `(foo (h1 a))`. By the `defcong` event above, we know that `(foo (h1 a))` equals `(foo (h2 a))` provided `(my-equiv (h1 a) (h2 a))`; but this is immediate from `lemma-1`. And finally, `(foo (h2 a))` is true by `lemma-2`.

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-
```
We can follow the warning's advice by changing `lemma-3` to the following.
```(defthm lemma-3
(implies (foo (double-rewrite x))
(equal (g x) x)))
```
With this change, the proof succeeds for the final `thm` above.

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))
```
This rewrite is performed with the empty alist (`unify-subst`), and is begun by rewriting the first argument (in that same empty `unify-subst`):
```(g (h1 a))
```
Note that the only equivalence relation being maintained at this point is `equal`. Now, the rewriter notices that the left-hand side of `lemma-3`, which is `(g x)`, matches `(g (h1 a))`. The rewriter thus creates a `unify-subst` binding `x` to `(h1 a)`: `((x . (h1 a)))`. It now attempts to rewrite the hypothesis of `lemma-3` to `t` under this `unify-subst`.

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