• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
      • Omaps
      • All-by-membership
      • In
      • Defset
      • Primitives
      • Subset
      • Mergesort
      • Intersect
      • Union
      • Pick-a-point-subset-strategy
      • Delete
      • Difference
      • Cardinality
      • Set
      • Double-containment
      • Intersectp
    • 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/osets

Intersect

(intersect x y) constructs the intersection of X and Y.

The logical definition is very simple, and the essential correctness property is given by intersect-in.

The execution uses a better, O(n) algorithm to intersect the sets by exploiting the set order.

See also intersectp, which doesn't construct a new set but just tells you whether the sets have any overlap. It's potentially faster if you don't care about constructing the set, because it doesn't have to do any consing.

Definitions and Theorems

Function: intersect

(defun intersect (x y)
       (declare (xargs :guard (and (setp x) (setp y))))
       (mbe :logic (cond ((empty x) (sfix x))
                         ((in (head x) y)
                          (insert (head x)
                                  (intersect (tail x) y)))
                         (t (intersect (tail x) y)))
            :exec (fast-intersect x y nil)))

Theorem: intersect-set

(defthm intersect-set (setp (intersect x y)))

Theorem: intersect-sfix-cancel-x

(defthm intersect-sfix-cancel-x
        (equal (intersect (sfix x) y)
               (intersect x y)))

Theorem: intersect-sfix-cancel-y

(defthm intersect-sfix-cancel-y
        (equal (intersect x (sfix y))
               (intersect x y)))

Theorem: intersect-empty-x

(defthm intersect-empty-x
        (implies (empty x)
                 (empty (intersect x y))))

Theorem: intersect-empty-y

(defthm intersect-empty-y
        (implies (empty y)
                 (empty (intersect x y))))

Theorem: intersect-in

(defthm intersect-in
        (equal (in a (intersect x y))
               (and (in a y) (in a x))))

Theorem: intersect-symmetric

(defthm intersect-symmetric
        (equal (intersect x y) (intersect y x))
        :rule-classes ((:rewrite :loop-stopper ((x y)))))

Theorem: intersect-subset-x

(defthm intersect-subset-x
        (subset (intersect x y) x))

Theorem: intersect-subset-y

(defthm intersect-subset-y
        (subset (intersect x y) y))

Theorem: intersect-insert-x

(defthm intersect-insert-x
        (implies (not (in a y))
                 (equal (intersect (insert a x) y)
                        (intersect x y))))

Theorem: intersect-insert-y

(defthm intersect-insert-y
        (implies (not (in a x))
                 (equal (intersect x (insert a y))
                        (intersect x y))))

Theorem: intersect-with-subset-left

(defthm intersect-with-subset-left
        (implies (subset x y)
                 (equal (intersect x y) (sfix x)))
        :rule-classes ((:rewrite :backchain-limit-lst 1)))

Theorem: intersect-with-subset-right

(defthm intersect-with-subset-right
        (implies (subset x y)
                 (equal (intersect y x) (sfix x)))
        :rule-classes ((:rewrite :backchain-limit-lst 1)))

Theorem: intersect-self

(defthm intersect-self
        (equal (intersect x x) (sfix x)))

Theorem: intersect-associative

(defthm intersect-associative
        (equal (intersect (intersect x y) z)
               (intersect x (intersect y z))))

Theorem: intersect-commutative

(defthm intersect-commutative
        (equal (intersect x (intersect y z))
               (intersect y (intersect x z)))
        :rule-classes ((:rewrite :loop-stopper ((x y)))))

Theorem: intersect-outer-cancel

(defthm intersect-outer-cancel
        (equal (intersect x (intersect x z))
               (intersect x z)))