Practice-formulating-strong-rules-6
Rules suggested by (MEMBER (FOO A) (NATS-BELOW (BAR B)))
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) (NATS-BELOW (BAR B)))
The definition of NATS-BELOW is
(defun nats-below (j)
(if (zp j)
'(0)
(cons j (nats-below (- j 1)))))
Thus, (nats-below 7) is (7 6 5 4 3 2 1 0). So when is k a
member of (nats-below j)?
The weakest version is
(defthm member-nats-below-weak
(implies (and (natp k)
(natp j)
(<= k j))
(member k (nats-below j))))
But clearly we could improve this to:
(defthm member-nats-below-weak-better
(implies (and (natp k)
(natp j))
(iff (member k (nats-below j))
(<= k j))))
or even
(defthm member-nats-below-weak-better
(implies (natp j)
(iff (member k (nats-below j))
(and (natp k)
(<= k j)))))
Clearly though, we'd like to get rid of the (natp j) hypothesis and
the neatest plausible version is:
(defthm member-nats-below-weak-neatest
(iff (member k (nats-below j))
(and (natp j)
(natp k)
(<= k j))))
But it is not a theorem! For example, if j is -1 and k is
0, then the left-hand side above returns t, because (nats-below j)
is (0), but the right-hand side is nil.
But this suggests a strategy for dealing with necessary hypotheses, like
(natp j). We can move them into an IF on the right-hand side!
Something like this might be a useful rewrite rule:
(iff (member k (nats-below j))
(if (natp j)
(and (natp k)
(<= k j))
...)).
We know, from member-nats-below-weak-better, that if (natp j) is
true, the member is equivalent to (and (natp k) (<= k j)). So now
consider what we know if (natp j) is false. If we can think of some term
it's equivalent to and that term is simpler than the member expression,
we have a strong rule.
But by inspection of the definition of nats-below, we see that when
(natp j) is false, (nats-below j) is the list (0) because
(zp j) is t. That is, nats-below treats all non-natural arguments
like they were 0. Thus, when (natp j) is false, (member k
(nats-below j)) is (member k '(0)), which is (equal k 0).
So the strong version is
(defthm member-nats-below-strong
(iff (member k (nats-below j))
(if (natp j)
(and (natp k)
(<= k j))
(equal k 0))))
This is a great :rewrite
rule. It gets rid of the member and nats-below and introduces
arithmetic.
This example illustrates the idea of putting an if on the
right-hand-side of the equivalence. Many users tend to limit themselves to
propositional forms inside iff or to simple expressions inside of
equal. But it is quite natural to use if to express what the answer
is: if j is a natural, then k is in (nats-below j) precisely if
k is a natural less than or equal to j; if j is not a natural,
then k is in (nats-below j) precisely if k is 0.
Use if to lay out the cases you must consider, if you can think of a
simpler, equivalent expression for every possible case.
Use your browser's Back Button now to return to practice-formulating-strong-rules.
