Cause a term to be rewritten twice

Logically, `identity` function:

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

Unfortunately, the proof fails. But fortunately, ACL2 gives the following
useful warning when

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

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

With this change, the proof succeeds for the final

In practice, it should suffice for users to follow the advice given in the
``

**Suggesting congruence rules.**

Sometimes the best way to respond to a ``

(defthm insert-sort-is-id (perm (insert-sort x) x))

Assuming that

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

(defcong perm perm (insert-sort x) 1)

This will eliminate the above warning for `defcong` event would probably be useful, since it would
allow rewrite rules with equivalence relation

**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

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

This rewrite is performed with the empty alist (

(g (h1 a))

Note that the only equivalence relation being maintained at this point is

Consider what happens now if the hypothesis of

But suppose that, instead, the hypothesis of

The example above explains how the rewriter treats calls of
`rewrite` or `linear` rule
carefully, just in case a call of `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

`set-inhibit-warnings`

Finally, we note that it is generally not necessary to call
`thm`
below, even without a call of

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