		Search-engine friendly clone of the ACL2 documentation.

Introduction-to-the-theorem-prover

Strong-rewrite-rules

Formulating good rewrite rules

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 truth value 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.