PRACTICE-FORMULATING-STRONG-RULES-3.html -- ACL2 Version 6.1

PRACTICE-FORMULATING-STRONG-RULES-3

rules suggested by (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)))

(implies (member e y) (member e (append x y)))

because they each cause the system to backchain upon seeing (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 every occurrence.

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.