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

(put i v (append a b))it considers the rule, with the variables

`i`

, `v`

, `a`

, and `b`

of the rule (natpandi) ;hyp 1

(<If both hyptheses rewrite to true, then the rulei(lena)). ;hyp 2

(append (putIn short, rewrite rules direct ACL2 to rearrange the terms in the goal formulas.iva)b).

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

(defthmcommands ACL2 to try to provenameformula...)

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

(defthmis successful, ACL2 will have a new rewrite rule in the database, even though you did notnameformula)

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 (ANDwherehyp1...hypk) (eqvlhsrhs))

`EQUAL`

or `IFF`

, and `IF`

, and not
a call of an abbreviation (``macro'') that expands to any of these. So illegal
`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.