Introduction to ACL2's notion of rewrite rules
This topic is an introduction to rewrite rules in ACL2 and is intended for the newcomer to ACL2. The slightly more experienced user might benefit from reading random-remarks-on-rewriting instead.
Rewrite rules make ACL2 replace one term by another. This is done by the rewriter, which is part of ACL2's simplifier. The rewriter sweeps through the goal formula trying all the rewrite, definition, and meta rules it knows, in order from the most recently submitted rule to the oldest, until it finds one to apply.
Here's an example. Just pretend that you have made a rewrite rule from the formula below.
(implies (and (natp i) (< i (len a))) (equal (put i v (append a b)) (append (put i v a) b)))
Then every time the rewriter sees a target term that matches
(put i v (append a b))
it considers the rule, with the variables
(natp i) ; hyp 1
(< i (len a)). ; hyp 2
If both hypotheses rewrite to true, then the rule fires and replaces the target by:
(append (put i v a) b).
In short, rewrite rules direct ACL2 to rearrange the terms in the goal formulas.
We are more precise later, but for now we turn to the question of how do
you make a rewrite rule from a formula? The answer is, you prove the formula
(defthm name formula ...)
commands ACL2 to try to prove formula and, if successful, build it into the database as a rule according to your specification in the rule-classes argument of the ... part of the command.
To make it easy for you to generate rewrite rules,
(defthm name formula)
is successful, ACL2 will have a new rewrite rule in the database, even though you did not explicitly tell it to add a rule.
A common mistake for new users is to forget that the above command adds a rewrite rule. This often results in a tangle of rules that lead nowhere or to infinite rewriting that you will have to interrupt. It is also good to remember that the command only adds a rule. It does not magically make ACL2 aware of all the mathematical consequences of the formula: it just makes a rewrite rule.
When you prove a theorem with
ACL2 can generate rewrite rules from formulas that look like this:
(IMPLIES (AND hyp1 ... hypk) (eqv lhs rhs))
where eqv is either
Technical Note: This tutorial introduction to the theorem prover takes
liberties with the truth! We are trying to give you a useful predictive model
of the system without burdening you with all the details, which are discussed
in the ACL2 User's Manual. For example, using directives in the rule-classes
you can rearrange the proved formula into the form you want your rule to take,
and you can make ACL2 take advantage of equivalence relations eqv other
We call the hyp terms the hypotheses of the rule. We call
lhs the left-hand side of the rule, and we call rhs the
right-hand side of the rule. If the conclusion of the rule is an
ACL2 allows several special cases of the shapes above. See special-cases-for-rewrite-rules, but come back here and continue.
A rewrite rule makes ACL2 seek out occurrences of terms that match the left-hand side of the rule and replace those occurrences using the right-hand side, provided all the hypotheses rewrite to true in the context of the application of the rule.
That is, the left-hand side is treated as a pattern that triggers the rule. The hypotheses are conditions that have to be proved in order for the rule to fire. The right-hand side is the replacement and is put into the formula where the pattern occurred.
Now for some clarifications. ACL2 only considers enabled rules. And ACL2
will use a propositional rule to replace a target only if the target occurs in
a propositional place in the formula. Generally that means it occurs in the
argument of a propositional connective, like
If a hypothesis has variables that do not occur in the left-hand side of the rule, then the pattern matching process won't find values for those variables. We call those free variables. They must be instantiated before ACL2 can relieve that hypothesis. To instantiate them, ACL2 has to guess values that would make the hypothesis true in this context, i.e., true given the assumptions of the goal theorem. So if you're trying to prove
(IMPLIES (AND (TRUE-LISTP A) (MEMBER (CAR P) A) (MEMBER (CDR P) A)) ...)
and the target you're rewriting is in the ``...'' part of the formula, the
rewriter knows that
The most predictable rewrite rules have no free variables. You can add pragmatic advice to help ACL2 with free variables, telling it to try all the possibilities it finds, to try just the first, or even to compute a ``creative'' guess.
It is possible to make the rewriting process loop forever, e.g., by
rewriting alpha to beta with one set of rules and rewriting
beta to alpha with another. Even a single rule can make the
process loop; we'll show you an example of that later in the tutorial. ACL2
can handle commutativity rules without looping. It uses
Logically equivalent formulas can generate radically different rewrite rules! Rearranging the propositional structure of the formula or swapping the left and right sides of an equality — while having no effect on the mathematical meaning of a formula — can have a drastic impact on the pragmatic meaning as a rule. To see an illustration of this, see equivalent-formulas-different-rewrite-rules.
Developing an effective set of rewrite rules is key to success at using ACL2. We'll look more at this later in the tutorial.
If you are working your way through the tutorial for the theorem prover, use your browser's Back Button now to return to introduction-to-the-theorem-prover. If you are reading just about how to make effective rewrite rules, go on to introduction-to-rewrite-rules-part-2.