• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
      • Std/lists/abstract
      • Rev
      • 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
      • Listpos
      • List-equiv
        • Basic-list-equiv-congruences
        • List-equiv-reductions
      • Final-cdr
      • Std/lists/append
      • Std/lists/remove
      • Subseq-list
      • Rcons
      • Std/lists/revappend
      • Std/lists/remove-duplicates-equal
      • Std/lists/reverse
      • Std/lists/last
      • Std/lists/resize-list
      • Flatten
      • Suffixp
      • Std/lists/butlast
      • Std/lists/set-difference
      • 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
      • Std/lists/add-to-set
      • Append-without-guard
      • Std/lists/subsetp
      • Std/lists/member
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Std/lists

List-equiv

(list-equiv x y) is an equivalence relation that determines whether x and y are identical except perhaps in their final-cdrs.

This is a very common equivalence relation for functions that process lists. See also list-fix for more discussion.

Definitions and Theorems

Function: fast-list-equiv

(defun fast-list-equiv (x y)
  (declare (xargs :guard t))
  (if (consp x)
      (and (consp y)
           (equal (car x) (car y))
           (fast-list-equiv (cdr x) (cdr y)))
    (atom y)))

Function: list-equiv

(defun list-equiv (x y)
  (mbe :logic (equal (list-fix x) (list-fix y))
       :exec (fast-list-equiv x y)))

Theorem: list-equiv-is-an-equivalence

(defthm list-equiv-is-an-equivalence
  (and (booleanp (list-equiv x y))
       (list-equiv x x)
       (implies (list-equiv x y)
                (list-equiv y x))
       (implies (and (list-equiv x y) (list-equiv y z))
                (list-equiv x z)))
  :rule-classes (:equivalence))

Theorem: list-equiv-when-atom-left

(defthm list-equiv-when-atom-left
  (implies (atom x)
           (equal (list-equiv x y) (atom y))))

Theorem: list-equiv-when-atom-right

(defthm list-equiv-when-atom-right
  (implies (atom y)
           (equal (list-equiv x y) (atom x))))

Theorem: list-equiv-of-nil-left

(defthm list-equiv-of-nil-left
  (equal (list-equiv nil y)
         (not (consp y))))

Theorem: list-equiv-of-nil-right

(defthm list-equiv-of-nil-right
  (equal (list-equiv x nil)
         (not (consp x))))

Theorem: list-fix-under-list-equiv

(defthm list-fix-under-list-equiv
  (list-equiv (list-fix x) x))

Theorem: list-fix-equal-forward-to-list-equiv

(defthm list-fix-equal-forward-to-list-equiv
  (implies (equal (list-fix x) (list-fix y))
           (list-equiv x y))
  :rule-classes :forward-chaining)

Theorem: append-atom-under-list-equiv

(defthm append-atom-under-list-equiv
  (implies (atom y)
           (list-equiv (append x y) x)))

Subtopics

Basic-list-equiv-congruences

Basic list-equiv congruence theorems for built-in functions.

List-equiv-reductions

Lemmas for reducing list-equiv terms involving basic functions.