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.
The one weakness of the rule above is that it only rewrites (member
x (nats-below y)) when an instance of that target term occurs in a
propositional setting, e.g., when the governing equivalence relation is
iff. But, thanks to Andrei Koltsov, an even stronger version is
available as an unconditional equality rewrite:
(defthm member-nats-below-stronger
(equal (member x (nats-below y))
(if (natp x)
(if (natp y)
(if (<= x y)
(nats-below x)
nil)
(if (= x 0) '(0) nil))
nil)))
The key observation is that when x and y are both naturals and
(<= x y), the result that member computes can be expressed with
nats-below. You may wonder whether this stronger rule allows the
immediate proof of the earlier member-nats-below-strong and the answer is
yes, because from the definition of nats-below ACL2 has observed that
(nats-below x) is a cons whenever x is a natural.
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.
