### STRONG-REWRITE-RULES

formulating good rewrite rules
```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.