Formulating good rewrite rules
Suppose you notice the following term in a Key Checkpoint:
You might think of two theorems for handling this term, which we'll call
the ``weak'' and ``strong'' version of
(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:
Technical Note: Actually, both rules concern propositional
occurrences of the ``target'' expression,
So the strong version is better because it will always eliminate
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
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
and it will not be obvious that the problem would go away if you
could establish that
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.