INTRODUCTION-TO-REWRITE-RULES-PART-1.html -- ACL2 Version 6.2

INTRODUCTION-TO-REWRITE-RULES-PART-1

introduction to ACL2's notion of rewrite rules

Major Section:  INTRODUCTION-TO-THE-THEOREM-PROVER

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 rules it knows. 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 i, v, a, and b of the rule 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:

(natp i)           ; hyp 1

and

(< i (len a)). ; hyp 2

If both hyptheses 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 with the defthm command. Recall that

(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 has a simple heuristic: if you don't tell it what kind of rule to generate from formula, it generates a rewrite rule! Thus, if this command

(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 the 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 defthm you are 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 (AND hyp1 ... hypk)
         (eqv lhs rhs))

where eqv is either EQUAL or IFF, and lhs is not a variable symbol, not a constant, and not a call of the function IF, and not a call of an abbreviation (``macro'') that expands to any of these. So illegal lhs include X, 0, (IF X Y Y), and (OR p q). The last is illegal because OR is just an abbreviation for a certain IF-expression.

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 reference 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 EQUAL and IFF. But we'll ignore these fine points for now.

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 EQUAL term we call it 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 AND, OR, NOT, IMPLIES, and IFF, or in the test of an IF. When we say that the left-hand side of the rule must 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 (TRUE-LISTP A) (MEMBER (CAR P) A) and (MEMBER (CDR P) A) are true. So if a rewrite rule is considered and the rule has (member e x) as a hypothesis, where e is a free variable but x was bound to A in the pattern matching, then it will guess that e must be (CAR P) or (CDR P), even though there are many other possibilities that would make (MEMBER e A) true. Of course, whatever guess it makes must also satisfy all the other hypotheses that mention e in the rule. It simply isn't very imaginative at guessing!

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 (equal (+ x y) (+ y x)) to replace (+ B A) by (+ A B), but not vice versa. (It is sensitive to alphabetic ordering when dealing with 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.