`(MEMBER (FOO A) (NATS-BELOW (BAR B)))`

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) (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 nd 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.