• 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
      • 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
      • 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
    • Std-extensions
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Std/lists
• Intersection$

Std/lists/intersection$

Lemmas about intersection$ available in the std/lists library.

Definitions and Theorems

We'll take intersectp as the desired normal form for asking whether intersections are empty.

Theorem: intersection$-under-iff

(defthm intersection$-under-iff
  (iff (intersection$ x y)
       (intersectp x y)))

Theorem: consp-of-intersection$

(defthm consp-of-intersection$
  (equal (consp (intersection$ x y))
         (intersectp x y)))

Basic atom/cons rules.

Theorem: intersection$-when-atom-left

(defthm intersection$-when-atom-left
  (implies (atom x)
           (equal (intersection$ x y) nil)))

Theorem: intersection$-of-cons-left

(defthm intersection$-of-cons-left
  (equal (intersection$ (cons a x) y)
         (if (member a y)
             (cons a (intersection$ x y))
           (intersection$ x y))))

Theorem: intersection$-when-atom-right

(defthm intersection$-when-atom-right
  (implies (atom y)
           (equal (intersection$ x y) nil)))

We don't have a very nice rule for cons on the right if we're trying to maintain equal, because we don't know where in x the element occurs. However, if we're only maintaining set-equiv, then we can just put the element on the front and we get a perfectly nice rule:

Theorem: intersection$-of-cons-right-under-set-equiv

(defthm intersection$-of-cons-right-under-set-equiv
  (set-equiv (intersection$ x (cons a y))
             (if (member a x)
                 (cons a (intersection$ x y))
               (intersection$ x y))))

Basic set reasoning

Theorem: member-of-intersection$

(defthm member-of-intersection$
 (iff (member a (intersection$ x y))
      (and (member a x) (member a y)))
 :rule-classes
 (:rewrite
   (:type-prescription
        :corollary (implies (not (member a x))
                            (not (member a (intersection$ x y)))))
   (:type-prescription
        :corollary (implies (not (member a y))
                            (not (member a (intersection$ x y)))))))

Theorem: subsetp-equal-of-intersection$-1

(defthm subsetp-equal-of-intersection$-1
  (subsetp-equal (intersection$ x y) x))

Theorem: subsetp-equal-of-intersection$-2

(defthm subsetp-equal-of-intersection$-2
  (subsetp-equal (intersection$ x y) y))

Theorem: intersection$-commutes-under-set-equiv

(defthm intersection$-commutes-under-set-equiv
  (set-equiv (intersection$ x y)
             (intersection$ y x)))

Length bound

Here is a nice bounding theorem. Note that there is no analogous rule for -right, because, e.g., X could have multiple copies of some member in Y, and if so we end up reproducing them. Consider for instance:

(intersection$ '(a a a) '(a)) ==> '(a a a)

Theorem: len-of-intersection$-upper-bound

(defthm len-of-intersection$-upper-bound
  (<= (len (intersection$ x y)) (len x))
  :rule-classes ((:rewrite) (:linear)))