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
bof 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 1and
(< i (len a)). ; hyp 2If 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
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
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
(IF X Y Y), and
(OR p q). The last is illegal because
ORis just an abbreviation for a certain
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
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
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
(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
eis a free variable but
xwas bound to
Ain the pattern matching, then it will guess that
(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
ein 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
(+ 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.