Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER

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:

Then you can use the following theorem (actually the definitional axiom introduced by theGoal Conjecture: (implies (and (endp z) (true-listp z)) (equal (rev (rev z)) z))

`defun`

of `endp`

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

Note that in this example, rewriting replaced the call ofRewritten Goal Conjecture: (implies (and (not (consp z)) (true-listp z)) (equal (rev (rev z)) z))

`endp`

by its
body after instantiating its body with the actuals from the call. This is
sometimes just called `endp`

.
(The notions of 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

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

This conjecture may be read ``ifGoal Conjecture: (implies (and (subsetp a b) (true-listp b) (member e a)) (< (len (rm e b)) (len b))).

`a`

is a subset of the `true-listp`

`b`

and `e`

is
a member of `a`

, then the result of removing `e`

from `b`

has a shorter length
than `b`

.''You can use the following theorem:

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

To do this you must know that the following subgoal is provable:Rewritten Goal Conjecture: (implies (and (subsetp a b) (true-listp b) (member e a)) (< (- (len b) 1) (len b))).

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 *pattern* term being
an instance of a *target*
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
``instance'' above and we
recommend you read it before continuing. Then use your browser's **Back Button**
to come back here.

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

*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 `t`

), or it could have been written in
a different but equivalent propositional style, `(or (not`

*hyp1*`) ...)`

,
or the equality could have been written the other way around,
`(equal `

*replacement* *pattern*`)`

. Such syntactic details don't matter.
Just take a theorem and use propositional calculus to rearrange it equivalently
into this form for the purposes of this one rewrite step.

Suppose *pattern* is an instance of some target term, *target* that
occurs in your goal conjecture. 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 *simga* 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)`

by an
ever growing sequence of terms:
(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 implmentation 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.