`(MEMBER (FOO A) (APPEND (BAR B) (MUM C)))`

Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER

What rules come to mind when looking at the following subterm of a Key
Checkpoint? Think of *strong* rules (see strong-rewrite-rules).

(MEMBER (FOO A) (APPEND (BAR B) (MUM C)))

Since `(append x y)`

contains all the members of `x`

and all the members
of `y`

, `e`

is a member of `(append x y)`

precisely when `e`

is a
member of `x`

or of `y`

. So a strong statement of this is:

(defthm member-append-strong-false (equal (member e (append x y)) (or (member e x) (member e y))))

However, this is not a theorem because `member`

is not Boolean.
`(Member e x)`

, for example, returns the first tail of `x`

that starts
with `e`

, or else `nil`

. To see an example of this formula that
evaluates to `nil`

, let

e = 3 x = '(1 2 3) y = '(4 5 6).Then the left-hand side,

`(member e (append x y))`

evaluates to `(3 4 5 6)`

while
the right-hand side evaluates to `(3)`

.
However, the two sides are propositionally equivalent (both either `nil`

or non-`nil`

together). So this is a useful :`rewrite`

rule:

(defthm member-append-strong (iff (member e (append x y)) (or (member e x) (member e y)))).It tells the system that whenever it encounters an instance of

`(MEMBER e (APPEND x y))`

in a propositional occurrence (where only
its truthvalue is relevant), it should be replaced by this
disjunction of `(MEMBER e x)`

and `(MEMBER e y)`

.The following two formulas are true but provide much weaker rules and we would not add them:

(implies (member e x) (member e (append x y)))because they each cause the system to backchain upon seeing(implies (member e y) (member e (append x y)))

`(MEMBER e (APPEND x y))`

expressions and will not apply unless one of the two side-conditions can be established.
There is a rewrite rule that is even stronger than `member-append-strong`

.
It is suggested by the counterexample, above, for the `EQUAL`

version of the rule.

(defthm member-append-really-strong (equal (member e (append x y)) (if (member e x) (append (member e x) y) (member e y))))While

`member-append-strong`

only rewrites `member-append`

expressions
occurring propositionally, the `-really-strong`

version rewrites
However, this rule will be more useful than `member-append-strong`

only
if you have occurrences of `member`

in non-propositional places. For example,
suppose you encountered a term like:

(CONS (MEMBER e (APPEND x y)) z).Then the

`-strong`

rule does not apply but the `-really-strong`

rule does.
Furthermore, the `-really-strong`

rule, by itself, is not quite as good as
the `-strong`

rule in propositional settings! For example, if you have proved
the `-really-strong`

rule, you'll notice that the system still has to use
induction to prove

(IMPLIES (MEMBER E A) (MEMBER E (APPEND B A))).The

`-really-strong`

rule would rewrite it to
(IMPLIES (MEMBER E A) (IF (MEMBER E A) (APPEND (MEMBER E A) B) (MEMBER E B)))which would further simplify to

(IMPLIES (MEMBER E A) (APPEND (MEMBER E A) B))What lemma does this suggest? The answer is the rather odd:

(implies x (append x y))which rewrites propositional occurrences of

`(APPEND x y)`

to `T`

if
`x`

is non-`nil`

. This is an inductive fact about `append`

.
A problem with the `-really-strong`

rule is that it transforms even
propositional occurrences of `member`

into mixed propositional and
non-propositional occurrences.

(defthm member-append-really-strong (equal (member e (append x y)) ; <-- even if this is a propositional occurrence (if (member e x) (append (member e x) y) ; <-- the member in here is not! (member e y))))So if you are using the

`-really-strong`

lemma in a situation in which
all your `member`

expressions are used propositionally, you'll suddenly
find yourself confronted with non-propositional uses of `member`

.
Our advice is not to use the `-really-strong`

version unless your application is
inherently using `member`

in a non-propositional way.

Use your browser's **Back Button** now to return to
practice-formulating-strong-rules.