Rewrite-equiv
Force ACL2 to perform substitution using a stylized equivalence hypothesis
Rewrite-equiv is actually the identity function:
(rewrite-equiv x) = x for all x. However, a term of the form
(hide (rewrite-equiv (equiv x y))) appearing in the hypothesis induces
ACL2 to aggressively substitute y for x when equiv is an equivalence relation (including equal) and x appears in a context
in which equiv is being maintained.
Equivalence relations appearing in the hypothesis are not generally used by
ACL2 to perform substitutions except under special circumstances, such as when
one argument is a symbol or a constant or during the fertilization stage of
the waterfall process. A stylized rewrite-equiv expression of the
form (hide (rewrite-equiv (equiv x y))) can be used to override this
default behavior. Care should be taken in using rewrite-equiv, however,
because it can easily result in rewrite loops.
For an example of a clause-processor that leverages
Rewrite-equiv to induce substitution using equivalence relations
appearing in the hypothesis, see rewrite-equiv-hint.
