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 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

(implies (and (not (consp z)) (equal z nil)) (equal (rev (rev nil)) nil))Since the

(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:

and beside each candidate subgoal we show its structure in those terms.Induction Step: (implies (andc(impliesp'q')) (impliespq))

Subgoal (i): (implies (and (not (endp z)) ; (implies (andc(true-listp z)) ;p) (true-listp (cdr z))) ;p')

Subgoal (ii): (implies (and (not (endp z)) ; (implies (andc(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 (andc(equal (rev (rev (cdr z))) (cdr z))) ;q') (equal (rev (rev z)) z)) ;q)

Subgoal (iv): (implies (and (not (endp z)) ; (implies (andc(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

and you wish to rewrite the targetTheorem: (implies (p (f x)) (equal (g (h x)) x))

`(g (h a))`

to `a`

in
What must you prove to relieve the hypothesis ofGoal Conjecture: (implies (and (q (f a)) (r a)) (s (g (h a))))

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.