Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER
Suppose you notice the following term in a Key Checkpoint:
(MEMBER (CAR A) (REV B)).You might think of two theorems for handling this term, which we'll call the ``weak'' and ``strong'' version of
member-rev.
(defthm member-rev-weak
(implies (member e b)
(member e (rev b)))).
(defthm member-rev-strong
(iff (member e (rev b))
(member e b))).
The ``strong'' version logically implies the ``weak'' version and so deserves the adjective. (Recall that ``p <---> q'' is just ``p ---> q'' and ``q ---> p.'' So the strong version quite literally says everything the weak version does and then some.)
But the ``strong'' version also produces a better rewrite rule. Here are the rules generated from these two formulas, phrased as directives to ACL2's simplifier:
member-rev-weak: If you ever see an instance of (MEMBER e (REV b)),
backchain to (MEMBER e b) (i.e., turn your attention to that term)
and if you can show that it is true, replace (MEMBER e (REV b)) by T.
member-rev-strong: If you ever see an instance of (MEMBER e (REV b)),
replace it by (MEMBER e b).
Technical Note: Actually, both rules concern propositional occurrences
of the ``target'' expression, (MEMBER e (REV b)), i.e., occurrences of
the target in which its truthvalue is the only thing of relevance. (Recall
that (MEMBER x y) returns the tail of y starting with x!
Evaluate some simple MEMBER expressions, like (MEMBER 3 '(1 2 3 4 5))
to see what we mean.) Both theorems tell us about circumstances in which
the target is non-NIL (i.e., ``true'') without telling us its identity.
But ACL2 keeps track of when the target is in a propositional occurrence and
can use such rules to rewrite the target to propositionally equivalent
terms.
So the strong version is better because it will always eliminate
(MEMBER e (REV b)) in favor of (MEMBER e b). That simpler
expression may be further reduced if the context allows it. But in
any case, the strong version eliminates REV from the problem. The weak
version only eliminates REV when a side-condition can be proved.
While either version may permit us to prove the Key Checkpoint that ``suggested'' the rule, the strong version is a better rule to have in the database going forward.
For example, suppose NATS-BELOW returns the list of natural numbers below its
argument. Imagine two alternative scenarios in which a key checkpoint
is about to arise involving this term:
(MEMBER K (REV (NATS-BELOW J)))
Scenario 1 is when you've got the strong version in your database: it will rewrite the key checkpoint term to
(MEMBER K (NATS-BELOW J))and that's what you'll see in the printed checkpoint unless other rules reduce it further.
Scenario 2 is when you have only the weak version in your database: the weak
rule will attempt to reduce the term above to T and will, if there are
sufficient rules and hypotheses about K's membership in (NATS-BELOW J). But if no
such rules or hypotheses are available, you'll be confronted with a key checkpoint
involving
(MEMBER K (REV (NATS-BELOW J)))and it will not be obvious that the problem would go away if you could establish that
K is in (NATS-BELOW J). Clearly, Scenario 1 is better.We recommend that you now practice formulating strong versions of rules suggested by terms you might see. See practice-formulating-strong-rules.
When you are finished with that, use your browser's Back Button to return to introduction-to-key-checkpoints.
