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 *bound* to whatever terms matched them in the target,
say the terms *i*, *v*, *a*, and *b*. To consider the
rule, the rewriter first tries to establish (``relieve'') the hypotheses. In
particular, it rewrites:

(natpi) ;hyp 1

and

(<i(lena)). ;hyp 2

If both hypotheses rewrite to true, then the rule *fires* and replaces
the target by:

(append (putiva)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
with the

(defthmnameformula...)

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, *formula*, it generates a rewrite rule! Thus, if this command

(defthmnameformula)

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 *programming* ACL2.
Being careless in your statement of lemmas is tantamount to being careless in
your programming.

ACL2 can generate rewrite rules from formulas that look like this:

(IMPLIES (ANDhyp1...hypk) (eqvlhsrhs))

where *eqv* is either *lhs* is not a
variable symbol, not a constant, and not a call of the function *lhs* include

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
than just

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
*equality* rule. Otherwise, it is a
*propositional equivalence* rule. If there are no hypotheses,
*k*=0, we say the rule is an *unconditional* rewrite rule; otherwise
it is *conditional*.

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 *match* the target we mean that we
can instantiate the variables in the rule to make the left-hand side identical
to the target. To *relieve* or establish the hypotheses of the rule,
ACL2 just applies other rewrite rules to try to prove the instantiated
hypotheses from the assumptions governing the occurrence of the target. When
ACL2 replaces the target, it replaces it with the instantiated right-hand side
of the rule and then applies rewrite rules to that.

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 *permutative*
rules.)

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.