Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER
Suppose MEMBER determines whether its first argument is a member of its
second, and SUBSETP determines whether every element of its first
argument is a member of its second. Suppose that you're trying to prove
some Main Theorem and are told the formula below is a key checkpoint. What
should you do?
Key Checkpoint: (IMPLIES (AND (CONSP A) (INTEGERP (CAR A)) (MEMBER (CAR A) B) (SUBSETP (CDR A) B) (NOT (SUBSETP (CDR A) (APPEND B C)))) (MEMBER (CAR A) C))
The key observation is that the third hypothesis implies the negation of the fourth. Writing it in the contrapositive:
(IMPLIES (AND ...
(SUBSETP (CDR A) B)
...)
(SUBSETP (CDR A) (APPEND B C)))
In fact, that is more complicated than it needs to be.
A ``correct'' response to the key checkpoint above is to prove
(defthm subsetp-append
(implies (subsetp a b)
(subsetp a (append b c)))).
A still better response is to prove this:
(defthm subsetp-append-2
(implies (or (subsetp a b)
(subsetp a c))
(subsetp a (append b c)))).
This version is better because it handles both of the possibilities regarding whether
a is a subset of the arguments of the append.
It would be nice if we could think of a ``strong'' version, one in which
(SUBSETP a (APPEND b c)) is rewritten to some clearly simpler term, but
nothing comes to mind.
In any case, if you cannot see any obvious simplification of the individual
terms in the Key Checkpoint, you should ask yourself whether there are
connections beween the various propositional parts (as here, with the third
and fourth hypotheses). It is a good heuristic to look for relations
between parts with the same top-level function symbol (as here, with
SUBSETP). It is also a good heuristic to throw out parts of the formula
that seem disconnected (as here, with the terms involving (CAR A)).
This discussion suggests several ``modes'' of looking at key checkpoints and the idea of trying the modes in sequence:
(1) look for simplifiable combinations of function symbols within propositional components,
(2) look for relations between propositional components, and
(3) throw out irrelevant or weakly connected components.
In all cases you are bringing to bear your intuitions about the semantics of the terms. That is, you're not just slinging symbols. You should be looking out for obvious truths about individual parts of the checkpoints... truths that are obvious to you but not to ACL2!
Ultimately the three ``modes'' are the same and we do not really recommend adhering to the given sequence. You're just looking for simpler theorems that, in combination, imply the checkpoint. Keeping the ``modes'' in mind may help focus your attention so you consider all the plausible possibilities. After a little experience you'll find yourself looking for all these things simultaneously as part ``cleaning up'' the checkpoints.
When your main goal theorems are harder than these, your main concern will be looking at a Key Checkpoint and asking yourself ``why is this true?'' But you don't want to do that until you've cleaned it up ``locally'' as much as possible and sometimes -- more often than you might think -- local considerations can prove many of your checkpoints.
If you have been working your way through the tutorial introduction to the theorem prover, use your browser's Back Button now to return to introduction-to-key-checkpoints.