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

Suppose `REV`

reverses a list, `MEMBER`

checks that its first argument
is an element of its second, and `SQUARES-PLUS-3P`

is some complicated
predicate. Suppose you're proving some Main Theorem that involves those
concepts and the theorem prover presents you with the following hideous
formula as a key checkpoint. What action should you take?

Hint: Don't read the formula ``for sense,'' i.e., don't try to understand
what this formula is saying! Just look at every subterm involving a nest of
two function symbols and ask if you know something about those two symbols
that allows you to *simplify* that one subterm.

(IMPLIES (AND (CONSP X) (MEMBER (+ 3 (* I I)) (REV X)) (LIST-OF-INTEGERS X) (INTEGERP I) (<= 0 I) (INTEGERP K) (<= 0 K) (< I K) (SQUARES-PLUS-3P K X) (NOT (EQUAL (CAR X) (+ 3 (* I I)))) (NOT (MEMBER (+ 3 (* I I)) X))) (SQUARES-PLUS-3P K (REV X)))?

The experienced ACL2 user will stop reading at the second hypothesis!

(MEMBER (+ 3 (* I I)) (REV X))

The combination of `MEMBER`

and `REV`

can be simplified. The question
``is `e`

a member of `(REV x)`

'' can be answered by asking ``is `e`

a
member of `x`

''. The two questions are equivalent. This insight comes from
your intuition about the *semantics* of `REV`

-- it just reorders the
elements but doesn't add or delete any. The second question is simpler
since it doesn't mention `REV`

, so this is a good transformation to make.
And the theorem that they are equivalent is simpler than the key checkpoint
above because it involves fewer functions and smaller expressions.

You might formalize this insight as

(equal (member e (rev x)) (member e x))But this conjecture is

`(member e x)`

returns the
`cdr`

of `x`

that begins with `e`

, not just a Boolean (`t`

or
`nil`

) indicating whether `e`

is an element of `x`

. The location
of the first `e`

in `(rev x)`

is generally different than the
location in `x`

. So when we say the two questions are ``equivalent''
we don't mean they are equal. We mean that they're propositionally equivalent:
both `nil`

or both non-`nil`

. This sense of equivalence is called
``if and only if'' and is checked by the function `iff`

.So our intuitive insight can be phrased as this theorem:

(iff (member e (rev x)) (member e x))

Suggesting that this formulation of the insight is ``obvious'' begs many questions.
Mathematically, we could have avoided `iff`

and just written two implications:

(and (implies (member e x) (member e (rev x))) (implies (member e (rev x)) (member e x))).or

(and (implies (member e x) (member e (rev x))) (implies (not (member e x)) (not (member e (rev x))))).Or we could have used

`iff`

but ``oriented'' it the other way:
(iff (member e x) (member e (rev x)))We choose to write

(iff (member e (rev x)) (member e x))because of

We deal with this at greater length later. But just to drive the point home, if we issue the command:

(defthm member-rev (iff (member e (rev x)) (member e x)))ACL2 will build in a rule that causes every propositional occurrence of

`(MEMBER e (REV x))`

to be replaced by `(MEMBER e x)`

. (By
``propositional occurrence'' we mean an occurrence in which the value is
tested, as by `IF`

or the propositional connectives. Remember, one
might use `member`

to determine the location of an element too.)
Note carefully: *if you do not tell ACL2 how to make a rule* from a
theorem, it makes a rewrite rule. Rewrite rules always replace instances of
the left-hand side by the corresponding instances of the right-hand side.
That is, when interpreted as a rewrite rule, `(iff `

*alpha*
*beta*`)`

makes ACL2 replace *alpha* by *beta*.

Probably the biggest mistake new users make is forgetting that every theorem
they prove creates a very specific rule. You must remember that you are
*programming* ACL2 with these rules. Being careless in your statement of
theorems is tantamount to being careless in your programming. What you get
is a mess.

Had we proved the same equivalence, but with the `iff`

commuted, we would
be giving ACL2 *bad advice*. We would be telling it ``replace instances
of `(MEMBER e x)`

by the corresponding instances of `(MEMBER e (REV x))`

''!
If ACL2 had that rule and ever tried to simplify any `member`

expression, e.g., `(MEMBER A B)`

, it would get into an infinite loop,
e.g., producing the following sequence of transformations:

(MEMBER A B) (MEMBER A (REV B)) (MEMBER A (REV (REV B))) ...until it eventually exhausted some resource.

Recall that we entertained the idea of phrasing our insight about `member`

and `rev`

with implications rather than `iff`

. Generally speaking,
implications produce weaker rules -- rules that apply less often. We
discuss that later.

Now suppose we've proved `member-rev`

, oriented so as to rewrite
`(member e (rev x))`

to `(member e x)`

, and built it in as a rewrite
rule. Then suppose we repeated the attempt to prove our Main Theorem.
This time, when the prover is processing the hideous Key Checkpoint printed above,
our new lemma, `member-rev`

, will hit it. It will transform the formula to:

(IMPLIES (AND (CONSP X) (MEMBER (+ 3 (* I I)) X) ; <-- the hyp has simplified (LIST-OF-INTEGERS X) (INTEGERP I) (<= 0 I) (INTEGERP K) (<= 0 K) (< I K) (SQUARES-PLUS-3P K X) (NOT (EQUAL (CAR X) (+ 3 (* I I)))) (NOT (MEMBER (+ 3 (* I I)) X))) (SQUARES-PLUS-3P K (REV X)))?

and then that will collapse to `T`

, since the `IMPLIES`

has
contradictory hypotheses (note the last hypothesis above).

By proving `member-rev`

we proved the hideous checkpoint. We never had to look
at the rest of the formula or think about why it is a theorem. Furthermore,
attacking the main theorem again, from scratch, with `member-rev`

in
the database, may eliminate other checkpoints that came up the last time we
tried to prove our main goal. So we recommend addressing one checkpoint at
a time.

This example illustrates that purely *local* thinking -- looking for
simplifiable combinations of function symbols -- can sometimes lead to
proofs and should always be your first reaction to a key checkpoint: what
local fact do you know that would clean up the formula? Don't think about
deep questions like ``why is this true?'' until you can't see any way to
make it simpler.

It is important to train yourself to see combinations of function symbols and to create strong rules for eliminating them. We will give you opportunities to practice this later in the tutorial.

If you have been reading the tutorial introduction to the theorem prover,
use your browser's **Back Button** now to return to
INTRODUCTION-TO-KEY-CHECKPOINTS.