A brief explanation of rewriting from the logical perspective

First we give two examples of rewriting. Then we give a rather detailed description. We recommend you read the description, even if you understand the two examples, just so that you learn our terminology.

**Example 1**: Suppose your goal conjecture is:

Goal Conjecture: (implies (and (endp z) (true-listp z)) (equal (rev (rev z)) z))

Then you can use the following theorem (actually the definitional axiom
introduced by the

Definitional Axiom: endp (equal (endp x) (not (consp x))).

to *rewrite* the *Goal Conjecture* to

Rewritten Goal Conjecture: (implies (and (not (consp z)) (true-listp z)) (equal (rev (rev z)) z))

Note that in this example, rewriting replaced the call of *expanding* the definition of *formal*, *body*, *call*, and *actuals* are
discussed in programming-knowledge-taken-for-granted.)

Expanding a definition is an example of *unconditional* rewriting.
All definitions in ACL2 are just bare equalities relating a call of the
function on its formals to its body. Any time you use an equality theorem,
whether a definitional equality or something more general like

(equal (append (append x y) z) (append x (append y z)))

to replace an instance of one side by the corresponding instance of the
other in a goal conjecture, we call that *unconditional* rewriting with
the equality.

**Example 2**: Suppose your goal conjecture is:

Goal Conjecture: (implies (and (subsetp a b) (true-listp b) (member e a)) (< (len (rm e b)) (len b))).

This conjecture may be read ``if

You can use the following theorem:

Theorem: (implies (member u v) (equal (len (rm u v)) (- (len v) 1)))

to *rewrite* the *Goal Conjecture* to

Rewritten Goal Conjecture: (implies (and (subsetp a b) (true-listp b) (member e a)) (< (- (len b) 1) (len b))).

To do this you must know that the following subgoal is provable:

Subgoal to Relieve Hyp 1: (implies (and (subsetp a b) (true-listp b) (member e a)) (member e b)).

This is an example of *conditional* rewriting. In order to use the
*Theorem* we had to establish that its hypotheses are satisfied. That is
called *relieving the hypotheses* and was done by proving the *Subgoal
to Relieve Hyp 1*. Conditional rewriting is the most commonly used proof
technique in ACL2.

Unconditional rewriting is just a special case, where there are no hypotheses to relieve.

Expanding a definition is just another special case, where there are no hypotheses to relieve and the pattern is easy to match because it is a call of a function on distinct variables.

This page discusses *rewriting* from the logical perspective. It is
important that you are familiar with the notions of a *target* term being
an *pattern* term. We often say the pattern *matches* the target.
These notions involve a corresponding *substitution* of terms for
variables. All these notions are discussed in the link for ``**Back Button** to come back here.

You should also be aware of the terms introduced in our discussion of

*Rewriting* is a fundamental rule of inference in our system. The
rule allows you to use a theorem, i.e., an axiom, lemma, or definition, to
replace one term by another in the goal conjecture you're trying to prove.

Suppose you have a theorem that is of the form (or can be put into the form):

Theorem: (implies (andhyp1...hypk) (equalpatternreplacement))

From the logical perspective we don't care how the theorem was actually
written when it was proved. It might have no hypotheses (in which case the
*hypi* could just be *hyp1**replacement* *pattern*

Suppose some target term, *target* that occurs in your goal conjecture
is an instance of *pattern*. Let the corresponding substitution be
*sigma*. If *sigma* does not contain a binding for every variable
that occurs in *Theorem*, then extend *sigma* to *sigma'* by
adding one binding for each such variable. (This is necessary only if
*pattern* does not contain every variable in *Theorem*.)

Let *replacement'* be the result of instantiating *replacement*
with *sigma'*. Let *hypi'* be the result of instantiating
*hypi* with *sigma'*.

Then the **Rewrite Rule of Inference** tells us it is permitted to
replace that occurrence of *target* in the goal by *replacement'*
— **if you can prove** each *hypi'* in this context. We make
this last condition clear in a moment.

The justification for this is that *Theorem* is true for all values of
the variables. Hence, it is true for the values specified by *sigma'*.
If the *hypi'* are true, then the target is really equal to
*replacement'*. But it is always permitted to replace something by
something it's equal to.

Rewriting thus involves several steps:

(1) Finding a *target* and a *theorem* to use to rewrite it to
some more desirable *replacement*.

(2) Instantiating *pattern* in the (rearranged) theorem to match
*target*.

(3) Extending *sigma* to *sigma'* to bind all the variables in
*Theorem*.

(4) Establishing that the *sigma'* instances of each of the
*hypi* hold. This is called *relieving the hypotheses* of the
theorem and is discussed in greater detail below.

(5) Replacing the occurrence of *target* in the goal conjecture by the
*sigma'* instance of *replacement*, provided all the hypotheses are
relieved.

Step (4) above, *relieving the hypotheses*, requires first identifying
the ``context'' of the target in the goal conjecture. To do this, use
propositional calculus to rearrange the goal conjecture so the occurrence of
*target* is in the conclusion and let *context* be the
hypothesis.

Rearranged Conjecture: (impliescontext(...target...))

To relieve the hypotheses you must then prove each of the following subgoals:

Subgoal to Relieve Hyp i: (impliescontexthypi').

It is important to note that this description of rewriting with
*Theorem* describes the process from a strictly logical perspective. The
syntax of the theorem and the goal don't matter. You're free to use
propositional calculus to rearrange them to put them into the appropriate
forms to fit the descriptions given. Clearly, if you have a candidate Theorem
in the ``wrong'' form and but it can be rearranged with propositional calculus
into the ``right'' form, then that rearranged theorem is also a *Theorem*
and can be used as described. But in the actual implementation of ACL2, the
syntactic form of a proved *Theorem* affects how it is used by rewriting.
If a proved theorem takes the form of an implication concluding with an
equality, ACL2 treats the left-hand side of the equality as *pattern* and
the right-hand side as *replacement*, unless you tell it otherwise.
We'll discuss this later.

Furthermore, being from the logical perspective this discussion of
rewriting does not address (a) how you extend *sigma* to *sigma'*
— any extension will do provided it allows you to relieve the
hypotheses. The ACL2 theorem prover uses certain heuristics which we'll
discuss later, including methods by which you can guide the system in the
selection.

Crucially, it does not discuss whether it is a *good idea* to do a
particular rewrite! For example, the definitional equality:

(equal (len x) (if (endp x) 0 (+ 1 (len (cdr x)))))

may be used repeatedly, endlessly, to replace

(len a) = (if (endp a) 0 (+ 1 (len (cdr a)))) = (if (endp a) 0 (+ 1 (if (endp (cdr a)) 0 (+ 1 (len (cdr (cdr a))))))) = ...

The ACL2 implementation of rewriting uses certain heuristics and the you can guide the system in its choices. We'll discuss this later.

Now use your browser's **Back Button** to return to the example proof in
logic-knowledge-taken-for-granted.