Practice-formulating-strong-rules-3
Rules suggested by (MEMBER (FOO A) (APPEND (BAR B) (MUM C)))
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 truth value 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.
