• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
      • Std/lists/abstract
      • Rev
        • Rev-theorems
      • Defsort
      • List-fix
      • Std/lists/nth
      • Hons-remove-duplicates
      • Std/lists/update-nth
      • Set-equiv
      • Duplicity
      • Prefixp
      • Std/lists/take
      • Std/lists/intersection$
      • Nats-equiv
      • Repeat
      • Index-of
      • All-equalp
      • Sublistp
      • Std/lists/nthcdr
      • Std/lists/append
      • Listpos
      • List-equiv
      • Final-cdr
      • Std/lists/remove
      • Subseq-list
      • Rcons
      • Std/lists/revappend
      • Std/lists/remove-duplicates-equal
      • Std/lists/last
      • Std/lists/reverse
      • Std/lists/resize-list
      • Flatten
      • Suffixp
      • Std/lists/set-difference
      • Std/lists/butlast
      • Std/lists/len
      • Std/lists/intersectp
      • Std/lists/true-listp
      • Intersectp-witness
      • Subsetp-witness
      • Std/lists/remove1-equal
      • Rest-n
      • First-n
      • Std/lists/union
      • Append-without-guard
      • Std/lists/subsetp
      • Std/lists/member
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
    • Std/system
    • Std/basic
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
    • Std-extensions
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Std/lists
• Reverse

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-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: rev-of-append

(defthm rev-of-append
        (equal (rev (append x y))
               (append (rev y) (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.