		Search-engine friendly clone of the ACL2 documentation.

Rev

Logically simple alternative to reverse for lists.

This function is nicer to reason about than ACL2's built-in reverse function because it is more limited:

reverse can operate on strings or lists, whereas rev can only operate on lists.
reverse has a tail-recursive definition, which makes it generally more difficult to induct over than the non tail-recursive rev.

Despite its simple append-based logical definition, rev should perform quite well thanks to mbe.

Definitions and Theorems

Function: rev

(defun rev (x)
  (declare (xargs :guard t))
  (mbe :logic
       (if (consp x)
           (append (rev (cdr x)) (list (car x)))
         nil)
       :exec (revappend-without-guard x nil)))

Theorem: rev-when-not-consp

(defthm rev-when-not-consp
  (implies (not (consp x))
           (equal (rev x) nil)))

Theorem: rev-of-cons

(defthm rev-of-cons
  (equal (rev (cons a x))
         (append (rev x) (list a))))

Theorem: rev-of-append

(defthm rev-of-append
  (equal (rev (append x y))
         (append (rev y) (rev x))))

Theorem: rev-of-list-fix

(defthm rev-of-list-fix
  (equal (rev (list-fix x)) (rev x)))

Theorem: len-of-rev

(defthm len-of-rev
  (equal (len (rev x)) (len x)))

Theorem: rev-of-rev

(defthm rev-of-rev
  (equal (rev (rev x)) (list-fix x)))

Theorem: consp-of-rev

(defthm consp-of-rev
  (equal (consp (rev x)) (consp x)))

Theorem: rev-under-iff

(defthm rev-under-iff
  (iff (rev x) (consp x)))

Theorem: revappend-removal

(defthm revappend-removal
  (equal (revappend x y)
         (append (rev x) y)))

Theorem: reverse-removal

(defthm reverse-removal
  (implies (true-listp x)
           (equal (reverse x) (rev x))))

Theorem: equal-of-rev-and-rev

(defthm equal-of-rev-and-rev
  (equal (equal (rev x) (rev y))
         (equal (list-fix x) (list-fix y))))

Theorem: make-character-list-of-rev

(defthm make-character-list-of-rev
  (equal (make-character-list (rev x))
         (rev (make-character-list x))))

Theorem: list-equiv-of-rev-and-rev

(defthm list-equiv-of-rev-and-rev
  (equal (list-equiv (rev x) (rev y))
         (list-equiv x y)))

Theorem: element-list-p-of-rev

(defthm element-list-p-of-rev
  (equal (element-list-p (rev x))
         (element-list-p (list-fix x)))
  :rule-classes :rewrite)

Theorem: element-list-fix-of-rev

(defthm element-list-fix-of-rev
  (equal (element-list-fix (rev x))
         (rev (element-list-fix x)))
  :rule-classes :rewrite)

Theorem: elementlist-projection-of-rev

(defthm elementlist-projection-of-rev
  (equal (elementlist-projection (rev x))
         (rev (elementlist-projection x)))
  :rule-classes :rewrite)

Subtopics

Rev-theorems: Some theorems about the library function rev.