• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • 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
        • Set-equiv-congruences
        • Set-unequal-witness
      • 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

Set-equiv

(set-equiv x y) is an equivalence relation that determines whether x and y have the same members, in the sense of member.

This is a very useful equivalence relation; typically any function that treats lists as sets will have good set-equiv congruence properties.

We prove various congruences and rewrites relating set-equiv to basic list functions like append, reverse, set-difference$, union$, etc. This is often sufficient for lightweight set reasoning. A heavier-weight (but not necessarily recommended) alternative is to use the std/osets library.

Definitions and Theorems

Function: set-equiv

(defun set-equiv (x y)
       (declare (xargs :guard (and (true-listp x) (true-listp y))))
       (and (subsetp-equal x y)
            (subsetp-equal y x)))

Theorem: set-equiv-asym

(defthm set-equiv-asym
        (equal (set-equiv x y) (set-equiv y x)))

Theorem: set-equiv-is-an-equivalence

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

Theorem: list-equiv-refines-set-equiv

(defthm list-equiv-refines-set-equiv
        (implies (list-equiv x y)
                 (set-equiv x y))
        :rule-classes (:refinement))

Theorem: set-equiv-congruence-over-elementlist-projection

(defthm set-equiv-congruence-over-elementlist-projection
        (implies (set-equiv x y)
                 (set-equiv (elementlist-projection x)
                            (elementlist-projection y)))
        :rule-classes :congruence)

Theorem: set-equiv-of-nil

(defthm set-equiv-of-nil
        (equal (set-equiv nil x) (atom x)))

Subtopics

Set-equiv-congruences

Basic congruence rules relating set-equiv to list functions.

Set-unequal-witness

(set-unequal-witness x y) finds a member of x that is not a member of y, or vice versa.