Double-rewrite
Cause a term to be rewritten twice
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-
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 this can 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. Optionally, also see the paper
``Double Rewriting for Equivalential Reasoning in ACL2'' by Matt Kaufmann and
J Strother Moore, in the proceedings of the 2006 ACL2 Workshop (paper is
published in the ACM
Digital Library); you might also find it for free here.
Suggesting congruence rules.
Sometimes the best way to respond to a ``Double-rewrite'' warning may
be to prove a congruence rule. Consider for example this rule.
(defthm insert-sort-is-id
(perm (insert-sort x) x))
Assuming that perm has been identified as an equivalence
relation (see defequiv), we will get the following warning.
ACL2 Warning [Double-rewrite] in ( DEFTHM INSERT-SORT-IS-ID ...):
In a :REWRITE rule generated from INSERT-SORT-IS-ID, equivalence relation
PERM is maintained at one problematic occurrence of variable X in the
right-hand side, but not at any binding occurrence of X. Consider
replacing that occurrence of X in the right-hand side with
(DOUBLE-REWRITE X). See :doc double-rewrite for more information on
this issue.
The problem is that the second occurrence of x (the right-hand side of
the rule insert-sort-is-id) is in a context where perm is to be
maintained, yet in this example, the argument x of insert-sort on
the left-hand side of that rule is in a context where perm will not be
maintained. This can lead one to consider the possibility that perm
could be maintained in that left-hand side occurrence of x, and if so, to
prove the following congruence rule.
(defcong perm perm (insert-sort x) 1)
This will eliminate the above warning for insert-sort-is-id. More
important, this defcong event would probably be useful, since it would
allow rewrite rules with equivalence relation perm to operate on the
first argument of any call of insert-sort whose context calls for
maintaining perm.
Details on double-rewrite.
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. Such warnings may appear for
hypotheses or right-hand side of a :rewrite rule, and for
hypotheses or full conclusion (as opposed to just the trigger term) of a
:linear 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
about 1900 such warnings (but note that 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 across 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)))
