Getting rid of unnecessary specificity
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 fourth hypothesis implies the negation of the fifth. 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
It would be nice if we could think of a ``strong'' version, one in which
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 between the various propositional parts (as here, with the fourth
and fifth hypotheses). It is a good heuristic to look for relations between
parts with the same top-level function symbol (as here, with
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.