		Search-engine friendly clone of the ACL2 documentation.

Std/lists/reverse

Lemmas about reverse available in the std/lists library.

The built-in reverse function is overly complex because it can operate on either lists or strings. To reverse a list, it is generally preferable to use rev, which has a very simple definition.

We ordinarily expect reverse to be enabled, in which case it expands (in the list case) to (revappend x nil), which we generally expect to be rewritten to (rev x) due to the revappend-removal theorem.

Because of this, we do not expect these lemmas to be very useful unless, for some reason, you have disabled reverse itself.

Definitions and Theorems

Theorem: stringp-of-reverse

(defthm stringp-of-reverse
  (equal (stringp (reverse x))
         (stringp x)))

Theorem: true-listp-of-reverse

(defthm true-listp-of-reverse
  (equal (true-listp (reverse x))
         (not (stringp x))))

Theorem: equal-of-reverses

(defthm equal-of-reverses
  (equal (equal (reverse x) (reverse y))
         (if (or (stringp x) (stringp y))
             (and (stringp x)
                  (stringp y)
                  (equal x y))
           (equal (list-fix x) (list-fix y)))))