EQUIVALENT-FORMULAS-DIFFERENT-REWRITE-RULES

Major Section:  INTRODUCTION-TO-THE-THEOREM-PROVER

Consider the rewrite rules that would be generated from the three commands below. In all three cases, the fact being stated relates the nth element of the reverse of x to the nth element of x. In fact, the three formulas are simple rearrangements of each other and are all equivalent. The theorem prover treats all three formulas equivalently when proving them. But the rules generated from them are very different.

(defthm nth-rev-1
  (implies (and (natp n)
                (< n (len x)))
           (equal (nth n (rev x))
                  (nth (- (len x) (+ 1 n)) x))))

(defthm nth-rev-2
  (implies (and (natp n)
                (< n (len x)))
           (equal (nth (- (len x) (+ 1 n)) x)
                  (nth n (rev x)))))

(defthm nth-rev-3
  (implies (and (natp n)
                (not (equal (nth n (rev x))
                            (nth (- (len x) (+ 1 n)) x))))
           (not (< n (len x)))))

Here are the three rewrite rules:

nth-rev-1:
Replace instances of (NTH n (REV x))
by (NTH (- (LEN x) (+ 1 n)) x),
if you can establish that n is a natural number less than the length of x.

nth-rev-2:
Replace instances of (NTH (- (LEN x) (+ 1 n)) x)
by (NTH n (REV x)),
if you can establish that n is a natural number less than the length of x.

nth-rev-3:
Replace instances of (< n (LEN x))
by NIL
if you can establish that n is a natural number and that (NTH n (REV x)) is different from (NTH (- (LEN x) (+ 1 n)) x).

As the driver of ACL2, you have to decide which rule you want when you give the command to prove it.

If you tell the theorem prover to use both nth-rev-1 and nth-rev-2, ACL2 will enter an infinite loop when it sees any term matching either NTH expression.

Most users would choose form nth-rev-1 of the rule. It eliminates rev from the problem -- at the expense of introducing some arithmetic. But arithmetic is so fundamental it is rarely possible to avoid it and it is likely to be in the problem already since you're indexing into (rev x). The nth-rev-2 form of the rule is ``bad'' because it introduces rev into a problem where it might not have appeared. The nth-rev-3 version is ``bad'' because it makes the theorem prover shift its attention from a simple arithmetic inequality to a complicated property of nth and rev, which might not be in the problem.

Use your browser's Back Button now to return to introduction-to-rewrite-rules-part-1.