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)We might expect the proof of this final; 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)))

`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- rewrite for more information on this issue.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)))