Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER
You might think that in order to use the theorem prover you have to know the mathematical logic supported by ACL2. But you need to know a lot less about it than you might think.
Technically, a theorem is a formula that can be derived from axioms by using rules of inference. Thus, to do a proof you have to know (a) the syntax of formulas, (b) the axioms, and (c) the rules of inference. Traditionally, these things are spelled out in excruciating detail in treatments of mathematical logic -- and for good reason.
The whole point of proving theorems is that it is a way to determine that a formula is ``always true'' (under some model of the axioms). By ``always true'' we actually mean what logicians mean when they say the formula is valid: true in the model, for all possible values of the variables. Here by ``model of the axioms'' we mean an understanding of the meaning of the various function symbols so that the axioms are true for all values of the variables. If the variables in your conjecture can take on an infinite number of values, proof is often the only way to determine that a conjecture is ``always true.'' So if proof is being used to determine that a questionable formula is always true the proof must be carried out flawlessly. Thus, the (a) syntax, (b) axioms, and (c) rules of inference must be described precisely and followed to the letter.
But formal mathematical logic was invented to explain how people reason. To the extent that logic mimics human reasoning, proofs can be seen as just extremely carefully crafted arguments. Given that ACL2 is responsible for following the rules ``to the letter,'' your main job is ``explain'' the big leaps.
To use the theorem prover you must understand (a) the syntax, because you must be able to write formulas flawlessly. But you don't have to know (b) the axioms and (c) the rules of inference at nearly the same level of precision, as long as you understand the basic structure and language of proofs.
Below is part of a proof of a certain theorem. You ought to be able to understand the following. Since what we describe is a proof of one case of the formula, we hope that you're convinced that the formula holds for that case.
Read this and follow the links to confirm that you understand what happens. Be sure to then use your browser's Back Button to return to this page and continue.
An Annotated Proof of
(implies (true-listp z)
(equal (rev (rev z)) z))
``We will prove that reversing the reverse of a true-listp yields the
original list. The formula stating this is above. We will prove it by
induction on the
list structure of z.
The base case of the induction is:
(implies (endp z)
(implies (true-listp z)
(equal (rev (rev z)) z))).
This formula is equivalent, by
propositional calculus,
to
(implies (and (endp z)
(true-listp z))
(equal (rev (rev z)) z))
Rewriting
with the definition of endp produces:
(implies (and (not (consp z))
(true-listp z))
(equal (rev (rev z)) z))
Rewriting repeatedly
starting with the definition of true-listp produces:
(implies (and (not (consp z))
(equal z nil))
(equal (rev (rev z)) z))
Then using the second hypothesis, just
substituting equals for equals,
we get
(implies (and (not (consp z))
(equal z nil))
(equal (rev (rev nil)) nil))
Since the conclusion involves no variables, we can
evaluate it,
getting
(implies (and (not (consp z))
(equal z nil))
T)
But this is an instance of
the tautology
(implies p T). Thus, the base case is proved.''Now it is time for a little quiz. There are just three questions.
Q1: The case above was the Base Case of an inductive proof of
(implies (true-listp z)
(equal (rev (rev z)) z))
in which we did induction on the structure of the linear list z. What
is the Induction Step? That is, what do you have to prove besides the Base
Case to complete this inductive proof?Below are four commonly given answers; choose one. Then look here to find out if you're right.
Induction Step -- Choice (i):
(implies (not (endp z))
(implies (true-listp z)
(equal (rev (rev z)) z)))
Induction Step -- Choice (ii):
(implies (true-listp (cdr z))
(equal (rev (rev (cdr z))) (cdr z)))
Induction Step -- Choice (iii):
(implies (and (not (endp z))
(equal (rev (rev (cdr x))) (cdr x)))
(implies (true-listp z)
(equal (rev (rev z)) z)))
Induction Step -- Choice (iv):
(implies (and (not (endp z))
(implies (true-listp (cdr z))
(equal (rev (rev (cdr z))) (cdr z))))
(implies (true-listp z)
(equal (rev (rev z)) z)))
Q2: To prove the Induction Step we must prove one or more of the goals below.
Which combinations are sufficient to imply the Induction Step? Decide what is required and then look here to find out if you're right. To help you, the Induction Step is of the form:
Induction Step:
(implies (and c
(implies p' q'))
(implies p q))
and beside each candidate subgoal we show its structure in those terms.
Subgoal (i):
(implies (and (not (endp z)) ; (implies (and c
(true-listp z)) ; p)
(true-listp (cdr z))) ; p')
Subgoal (ii):
(implies (and (not (endp z)) ; (implies (and c
(true-listp z) ; p
(equal (rev (rev (cdr z))) (cdr z))) ; q')
(equal (rev (rev z)) z)) ; q)
Subgoal (iii):
(implies (and (not (endp z)) ; (implies (and c
(equal (rev (rev (cdr z))) (cdr z))) ; q')
(equal (rev (rev z)) z)) ; q)
Subgoal (iv):
(implies (and (not (endp z)) ; (implies (and c
(true-listp (cdr z)) ; p'
(equal (rev (rev (cdr z))) (cdr z))) ; q')
(equal (rev (rev z)) z)) ; q)
Q3: Suppose you know the theorem
Theorem:
(implies (p (f x))
(equal (g (h x))
x))
and you wish to rewrite the target (g (h a)) to a in
Goal Conjecture:
(implies (and (q (f a))
(r a))
(s (g (h a))))
What must you prove to relieve the hypothesis of Theorem?After you've thought about it, look here for our answer.
End of the Quiz
If this page made sense, you're ready to read the introduction to the theorem prover.
If you are reading this as part of the tutorial introduction to the theorem prover, use your browser's Back Button now to return to introduction-to-the-theorem-prover.
