		Search-engine friendly clone of the ACL2 documentation.

Introduction-to-the-theorem-prover

Dealing-with-key-combinations-of-function-symbols

How to get rid of key combinations of function symbols

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

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