		Search-engine friendly clone of the ACL2 documentation.

Introduction-to-the-theorem-prover

Introduction-to-rewrite-rules-part-2

How to arrange rewrite rules

You should design your rewrite rules to canonicalize the terms in your problem, that is, your rules should drive terms into some normal form so that different but equivalent terms are rewritten into the preferred shape, making equivalent terms identical. You are very familiar with this idea from algebra, where you learned to normalize polynomials. Thus, when you see (2x + 6)(3x - 9) you automatically normalize it, by ``multiplying out and collecting like terms,'' to get (6x^2 - 54). This normalization strategy allows you to recognize equivalent terms presented differently, such as 6(x^2 - 9).

The ACL2 user is responsible for making up the rules. (Standard ``books'' — files of ACL2 definitions and theorems — can often provide rules for some sets of functions, e.g., arithmetic.) This is a heavy burden on you but it means you are in charge of your own normal forms. For example, if you use the function nthcdr, which returns the nth cdr of a list, you might see both (cdr (nthcdr i x)) and (nthcdr i (cdr x)). These two expressions are equivalent but not identical. You will want to decide which you want to see and prove the rewrite rule that converts the other to that preferred form.

Most good users develop an implicit ordering on terms and rewrite ``heavy'' terms to ``lighter'' ones. This ensures that there are no loops in their rewrite rules. But this ordering changes according to the user and the problem.

Generally, the lightest terms are primitives such as IF, EQUAL, arithmetic, etc. Functions defined without explicit recursion tend to be ignored because they are just expanded away (but see below). Recursively defined functions tend to be heavier than any other recursive function used in their definitions, so, for example, if rev is defined in terms of append, rev is heavier than append. But the size and subtlety of recursively defined functions also affects their place in the ordering.

But rewrite rules are surprisingly subtle. Recall that a rewrite rule can be made from a formula of this form:

(IMPLIES (AND hyp1 ... hypk) 
         (eqv lhs rhs))

where eqv is either EQUAL or IFF, and lhs is a call of a function other than IF. In such a rule, lhs is the pattern responsible for triggering the rule, the hypi are conditions which must be satisfied by the context of the target being rewritten, and rhs is the replacement. The replacement only happens if the rule is enabled, the pattern matches, the conditions are satisfied, and (in the case of an IFF rule) the target occurs propositionally. There are other heuristic restrictions that we won't discuss here.

So how should you phrase a theorem in order to make it an effective rule?

General Principles:

* Strengthen the Formula: The fewer hypotheses a formula has the better the rewrite rule formed from it. The more general the left-hand side the better the rule. The fewer free variables in the hypothesis, the better. The idea is to form a rule that fires predictably. Later in this tutorial you'll get some practice formulating strong rules.

* Choosing the Conclusion: If a lemma is an implication, you have to choose what the conclusion will be. (You'll also have to ``orient'' that conclusion by choosing a left-hand side and a right-hand side, but we discuss that below). You can swap the conclusion and any hypothesis by negating both, producing a different conclusion. There are generally two (possibly conflicting) heuristics for deciding which part of the formula should be the conclusion:

Choosing the Conclusion Heuristic 1: Can you make the conclusion be an EQUAL or IFF expression that has a ``heavy term'' on one side? That will make a rule that replaces the heavy term with a lighter one. We discuss this situation more below.

Choosing the Conclusion Heuristic 2: Can you make the conclusion be a non-propositional term that contains all the variables mentioned in the hypotheses? By ``non-propositional'' we mean a term that is not just the propositional combination (e.g., with AND or OR) of other terms but instead some call of some ``heavy'' function? If your conclusion contains all the variables mentioned in the hypotheses, matching it will instantiate all the variables in the hypotheses. That way ACL2 will not have to guess instantiations of unbound variables when it tries to relieve the hypotheses. It is not very good at guessing.

* Orienting the Conclusion: If the conclusion is an EQUAL or an IFF, you have to decide which is the left-hand side and which is the right. If the conclusion is (NOT lhs), then the left-hand side is lhs and the right-hand side is NIL. If the conclusion is not an EQUAL, an IFF, or a NOT then the conclusion itself will be the left-hand side and the right-hand side will be T. If your lemma was created by looking at Key Checkpoints while using The Method, the left-hand side should match some term in that checkpoint.

Remember, the left-hand side is the ``trigger'' that will make the rule fire. It is the pattern that ACL2 will be looking for.

* Pay attention to the free variables: Look at the variables that occur in the pattern (the left-hand side) and compare them to the variables that occur in the hypotheses. Does some hypothesis contain a variable, say v, that is not in the pattern? We call v a free variable because it will not be assigned a value (``bound'') by the process of pattern matching. ACL2 will have to guess a value for v. If some hypothesis contains v as a free variable, ask whether more than one hypothesis contains v? ACL2 uses the first hypothesis containing a free v to guide its guess for v. To ``guess'' a value for v, ACL2 uses that hypothesis as a pattern and tries to match it against the assumptions in the checkpoint formula being proved. This means that key hypothesis must be in normal form, to match the rewritten assumptions of the goal. It also means that you should reorder the hypotheses to put the most unusual hypothesis containing a free v first in the list of conjuncts. For example, if v is free in two hypotheses, (natp v) and (member (nthcdr v a) b), then we recommend putting the member term first. There are likely to be many terms in the goal satisfying the natp hypothesis — or none if natp has expanded to an integer inequality — while there are likely to be few terms satisfying the member hypothesis, especially if a and b are bound by the left-hand side of the rule.

Here are some (possibly conflicting) heuristics for choosing the left-hand side:

Choose a Left-Hand Side that Occurs in a Key Checkpoint: If you use the Method you will tend to do this anyway, because you'll see terms in the Key Checkpoints that you want to get rid of. But many moderately experienced users ``look ahead'' to how the proof will go and formulate a few anticipatory rules with the idea of guiding ACL2 down the preferred path to the proof. When you do that, you risk choosing left-hand sides that won't actually arise in the problem. So when you formulate anticipatory rules, pay special attention to the functions and terms you put in the left-hand sides. The next few paragraphs deal with specific cases.

Avoid Non-Recursive Functions in the Left-Hand Side: If the left-hand side contains a call of a defined function whose definition is not recursive, then it will almost never match any target in the formula being rewritten unless the function is disabled. Suppose for example you have defined SQ so that (SQ x) is (* x x). Suppose you considered choosing a left-hand side like (+ (SQ x) (SQ y)). Suppose you hoped it would hit the target (+ (SQ A) (SQ B)) in some formula. But when ACL2 simplifies the formula, it will first rewrite that target to

(+ (* A A) (* B B))

by expanding the definition of SQ, since it could do so without introducing any recursive calls. But now the target won't match your rule. By choosing a left-hand side that occurs in a Key Checkpoint (and is not one of a handful of abbreviations ACL2 uses in its output like AND, NOT), you'll avoid this problem since SQ will have already been expanded before the Key Checkpoint is printed.

Disable Non-Recursive Functions: If you insist on a left-hand side that contains calls of non-recursive functions, remember to disable those non-recursive functions after you've proved all the rules you want about them. By disabling SQ you can prevent ACL2 from expanding the definition as it did above. Sometimes you will define a function non-recursively to formalize some concept that is common in your application and you will want to create a sort of algebra of rules about the function. By all means do so, so you can conduct your formal reasoning in terms of the concepts you're informally manipulating. But after proving the required laws, disable the non-recursive concept so that ACL2 just uses your laws and not the messy definition.

Choose a Left-Hand Side Already in Simplest Form: This is a generalization of the advice above. If any rule will rewrite your left-hand side, it will prevent your rule from matching any target. For example, if you write a left-hand side like (foo (car (cons x y))) then it would never match any target! The reason is that even if (FOO (CAR (CONS A B))) did occur in some goal formula, before ACL2 would try your rule about foo it will use the obvious rule about CAR and CONS to transform your imagined target to (FOO A). Thus, your rule would not match. So you have to keep in mind all your other rules when you choose a left-hand side (and when you choose the hypotheses to guide free variable selection). If you always choose a pattern that matches a term in a Key Checkpoint, you avoid this problem. Also see community-books example books/demos/knuth-bendix-problem-1.lisp.

Make Sure the Left-Hand Side is ``Heavier'' than the Right: Sometimes this is obvious, as when you choose (REV (REV x)) for the left-hand side and x for the right. But what do you about (REV (APPEND x y)) versus (APPEND (REV y) (REV x))? Most of the time we choose to drive the heaviest function (in this case REV) down toward the variables, lifting the lighter function (APPEND) up so that we can reason about the lighter function's interaction with the surrounding ``matrix'' of the formula. So we'd rewrite (REV (APPEND x y)) to (APPEND (REV y) (REV x)), not vice versa.

Alternative Ways to Talk About the Same Thing: If your problem and specification use two different ways to talk about the same thing, choose one form and rewrite the other into that form. For example, the ACL2 built-in nth returns the nth element of a list, and the built-in function nthcdr returns the nth cdr of a list. They are defined independently. But (nth n x) is the same thing as (car (nthcdr n x)). Since nth can be expressed in terms of nthcdr but not vice versa, it is clear we should prove (equal (nth n x) (car (nthcdr n x))) as a rewrite rule if both nth and nthcdr are involved in the problem.

Don't Let Computational Efficiency Dictate the Terms: If you have two functions that are equivalent (perhaps one was defined to be computationally more efficient), prove their equivalence as a rewrite rule that eliminates the more complicated function. An extreme example would be a model that uses a sophisticated data structure (like a balanced binary tree, red-black tree, ordered array, or hash table) to implement something simple like an association of keys to values. By proving the equivalence as stated you can eliminate the messy function early and do the bulk of your reasoning in terms of its simple specification.

The best ACL2 users become very good at keeping all these things in mind when designing their rewrite rules. Practice makes perfect. Don't be afraid during your learning of ACL2 to undo the rules you first invented and try to make better ones.

Finally, be patient! There will be times when you think to yourself ``Why should I spend my time thinking of rules that guide ACL2? I know the proof!'' There are two reasons. First, you may ``know'' the proof but you may well be wrong and part-way through this whole exercise you may realize that you're missing a major hypothesis or special case that breaks your whole conception of the problem. The proof is in the details. Second, most of the time the library of rules you develop in this process will be used over and over again on variants of the main problem in the months and years ahead. This is sometimes called the proof maintenance problem. Theorems don't suffer bit rot! But the artifacts you're modeling change and you will need to prove new versions of old theorems. A good general purpose library makes this much easier.

We now recommend that you practice inventing strong rules; see strong-rewrite-rules.

For advice on handling specific kinds of formulas and definitions, see specific-kinds-of-formulas-as-rewrite-rules.

For more information about the rewriter works and how rules are created, see further-information-on-rewriting.

If you are working your way through the tutorial introduction to the theorem prover, use your browser's Back Button to return to introduction-to-the-theorem-prover.