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:
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 defun of endp):
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 endp by its
body after instantiating its body with the actuals from the call. This is
sometimes just called expanding the definition of endp.
(The notions 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 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:
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 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 (and hyp1
...
hypk)
(equal pattern
replacement))
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:
(implies context
(... target ...))
To relieve the hypotheses you must then prove each of the following subgoals:
Subgoal to Relieve Hyp i: (implies context hypi').
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.
