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 not a theorem, because (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 our knowledge of how ACL2 turns formulas into rules!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.
