Rewrite
Make some :rewrite rules (possibly conditional ones)
See rule-classes for a general discussion of rule classes,
including how they are used to build rules from formulas and a discussion of
the various keywords in a rule class description.
This doc topic discusses the rule-class :rewrite. If you want a
general discussion of how rewriting works in ACL2 and some guidance on how to
construct effective rewrite rules, see introduction-to-rewrite-rules-part-1 and then see introduction-to-rewrite-rules-part-2. If you want a flexible, convenient
interface to the ACL2 rewriter that can be called programmatically, see rewrite$.
Examples:
(defthm plus-commutes ; Replace (+ a b) by (+ b a) provided
(equal (+ x y) (+ y x))) ; certain heuristics approve the
; permutation.
(defthm plus-commutes ; equivalent to the above
(equal (+ x y) (+ y x))
:rule-classes ((:rewrite :corollary (equal (+ x y) (+ y x))
:loop-stopper ((x y binary-+))
:match-free :all)))
(defthm append-nil ; Replace (append a nil) by a, if
(implies (true-listp x) ; (true-listp a) rewrites to t.
(equal (append x nil) x)))
(defthm append-nil ; as above, but with defaults and
(implies (true-listp x) ; a backchain limit
(equal (append x nil) x))
:rule-classes ((:rewrite :corollary (implies (true-listp x)
(equal (append x nil) x))
:backchain-limit-lst (3) ; or equivalently, 3
:match-free :all)))
(defthm member-append ; Replace (member e (append b c)) by
(implies ; (or (member e b) (member e c) in
(and ; contexts in which propositional
(true-listp x) ; equivalence is sufficient, provided
(true-listp y)) ; b and c are true-lists.
(iff (member e (append x y))
(or (member e x) (member e y)))))
General Form:
(and ...
(implies (and ...hi...)
(implies (and ...hk...)
(and ...
(equiv lhs rhs)
...)))
...)
Note: One :rewrite rule class object might create many rewrite rules
from the :corollary formula. To create the rules, we first
translate the formula, expanding all macros (see trans) and also
removing guard-holders. Next, we then flatten the and and
implies structure of the formula; for example, if the hypothesis or
conclusion is of the form (and (and term1 term2) term3), then we replace
that by the ``flat'' term (and term1 term2 term3). (The latter is
actually an abbreviation for the right-associated term (and term1 (and
term2 term3)).) During this flattening process, we eliminate lambdas as necessary in order to continue flattening; one may think of this
step as simply substituting to eliminate let, let*, and mv-let in order to expose more calls of implies and and. The
result is a conjunction of formulas, each of the form
(implies (and h1 ... hn) concl)
where no hypothesis is a conjunction and concl is neither a
conjunction nor an implication. If necessary, the hypothesis of such a
conjunct may be vacuous. We then further coerce each concl into the form
(equiv lhs rhs), where we continue to eliminate lambdas until we
reach this form, and then we eliminate lambdas from the first argument of
equiv but not the second argument. Here equiv is a known equivalence relation. If we do not reach an equivalence relation, even after
eliminating lambdas, then we replace the resulting term, term by
(iff term t), except that we replace (not term) by (iff term
nil). By these steps we reduce the given :corollary to a
sequence of conjuncts, each of which is of the form
(implies (and h1 ... hn)
(equiv lhs rhs))
where equiv is a known equivalence relation and lhs has no
lambdas. See equivalence for a general discussion of the
introduction of new equivalence relations. At this point, we check
whether lhs and rhs are the same term; if so, we cause an error,
since this rule will loop. (But this is just a basic check; the rule could
loop in other cases, for example if rhs is an instance of lhs; see
loop-stopper.)
You can experiment by creating some rewrite rules using defthm and
then using :pr to see how the rule was stored.
We create a :rewrite rule for each such conjunct, if possible, and
otherwise cause an error. It is possible to create a rewrite rule from such a
conjunct provided lhs is not a variable, a quoted constant, a let-expression, or a lambda application. Although it is legal to create
a rewrite rule from an if-expression (if tst tbr fbr), note that
the rewriter uses the truth or falsity of the test, tst, when rewriting
the true and false branches tbr and fbr, respectively; so rewrite
rules are most often unnecessary for if-expressions.
A :rewrite rule is used when any instance of the lhs occurs in a
context in which the equivalence relation is an admissible congruence relation. First, we find a substitution that makes lhs equal
to the target term. Then we attempt to relieve the instantiated hypotheses of
the rule. Hypotheses that are fully instantiated are relieved by recursive
rewriting. Hypotheses that contain ``free variables'' (variables not assigned
by the unifying substitution) are relieved by attempting to guess a suitable
instance so as to make the hypothesis equal to some known assumption in the
context of the target. If the hypotheses are relieved, and certain
restrictions that prevent some forms of infinite regress are met (see loop-stopper), the target is replaced by the instantiated rhs, which is
then recursively rewritten.
ACL2's rewriting process has some optimizations, including the
following.
- The suggestion, above, that the rewriter looks through the goal clause for ``any instance of the lhs'' is not quite true. :Rewrite
rules are never applied to quoted constants or any term inside a call of
hide. If you want to rewrite a quoted constant use a :rewrite-quoted-constant rule.
- The notion of ``a substitution that makes lhs equal to the target
term'' is a bit more generous than the most straightforward such notion.
Suppose for example that lhs is (f (+ 3 x)) and the target term is
(f (+ 3 (g y)). (Aside: ACL2 deals in so-called translated terms, so
since + is a macro, lhs and term would actually be (f (binary-+
'3 x)) and (f (binary-+ '3 (g y))); we will ignore this distinction,
but if you want more information, see term.) Then of course, that
substitution binds x to (g y). But now suppose that instead the
target term is (f 10). You may be surprised to learn that the
substitution binding x to 7 makes (f (+ 3 x)) equal to (f
10); for example, the rewrite rule (equal (f (+ x 3)) (h x))) would
rewrite (f 10) to (h 7). This would also be the case if lhs
were instead (f (+ x 3)). This sort of optimization occurs when the new
constant has ACL2-count no greater than the old constant. There are
similar optimizations for *, /, -, strings, symbols, and
conses (for details see ACL2 source function
one-way-unify1-quotep-subproblems).
- When a term t1 is rewritten to a new term t2, the rewriter is
then immediately applied to t2. On rare occasions you may find that you
do not want this behavior, in which case you may wish to use a trick involving
hide; see meta, near the end of that documentation.
- When the hypotheses and right-hand side are rewritten, ACL2 does not
really first apply the substitution and then rewrite; instead, as it
rewrites those terms it looks up the already rewritten values of the
bound variables. Sometimes you may want those bindings rewritten again, e.g.,
because the variables occur in slots that admit additional equivalence
relations. See double-rewrite.
See introduction-to-rewrite-rules-part-1 and see introduction-to-rewrite-rules-part-2 for an extended discussion of how to
create effective rewrite rules.
Subtopics
- Force
- Identity function used to force a hypothesis
- Hide
- Hide a term from the rewriter
- Syntaxp
- Attach a heuristic filter on a rule
- Free-variables
- Free variables in rules
- Bind-free
- To bind free variables of a rewrite, definition, or linear rule
- Loop-stopper
- Limit application of permutative rewrite rules
- Backchain-limit
- Limiting the effort expended on relieving hypotheses
- Double-rewrite
- Cause a term to be rewritten twice
- Rewrite-lambda-object
- rewriting lambda objects in :FN slots
- Rewriting-versus-cleaning-up-lambda-objects
- why change the default action on rewriting lambda objects
- Random-remarks-on-rewriting
- Some basic facts about the ACL2 rewriter
- Set-rw-cache-state
- Set the default rw-cache-state
- Case-split
- Like force but immediately splits the top-level goal on the hypothesis
- Rewrite-lambda-object-actions
- actions available when rewriting lambda objects
- Syntactically-clean-lambda-objects-theory
- how to specify syntactic cleaning of lambda objects
- Hands-off-lambda-objects-theory
- how to specify no modification of lambda objects
- Rewrite-lambda-objects-theory
- how to specify rewriting of lambda objects
- Simple
- :definition and :rewrite rules used in
preprocessing
- Rewrite-stack-limit
- Limiting the stack depth of the ACL2 rewriter
- Rewrite-equiv
- Force ACL2 to perform substitution using a stylized equivalence hypothesis
- Assume-true-false-aggressive-p
- Control rewriter's use of the type-alist with IF calls
- Remove-trivial-equivalences-enabled-p
- Avoid removal of trivial equivalences during rewriting
- Rewrite-lambda-modep
- switch controlling rewriting of lambda objects
- Rewrite-if-avoid-swap
- Control rewriter's swapping of branches of IF calls
- Set-rw-cache-state!
- Set the default rw-cache-state non-locally
- Rw-cache-state
- The current rw-cache-state
