### EQUIVALENT-FORMULAS-DIFFERENT-REWRITE-RULES

logically equivalent formulas can generate radically different 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
`n`

th element of the reverse of `x`

to the `n`

th 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.