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
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
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
So how should you phrase a theorem in order to make it an effective rule?
* 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
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
* Orienting the Conclusion: If the conclusion is an
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
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
(+ (* A A) (* B B))
by expanding the definition of
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.
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
Make Sure the Left-Hand Side is ``Heavier'' than the Right:
Sometimes this is obvious, as when you choose
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
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.