Equivalent-formulas-different-rewrite-rules
Logically equivalent formulas can generate radically different rules
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.
