How to get rid of key combinations of function symbols

Suppose

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 *semantics* of

You might formalize this insight as

(equal (member e (rev x)) (member e x))

But this conjecture is *not* a theorem, because

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

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

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, *alpha*
*beta**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 *bad advice*. We would be telling it ``replace
instances of

(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

Now suppose we've proved

(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

By proving

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.