PRACTICE-FORMULATING-STRONG-RULES-6.html -- ACL2 Version 6.2

PRACTICE-FORMULATING-STRONG-RULES-6

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