• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • 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

Subset

(subset x y) determines if X is a subset of Y.

We use a logically simple definition, but using MBE we exploit the set order to implement a tail-recursive, linear subset check.

The :exec version of fast-subset just inlines the set primitives and tweaks the way the order check is done. It is about 3x faster than the :logic version of fast-subset on the following loop:

;; 3.83 sec logic, 1.24 seconds exec
(let ((x (loop for i from 1 to 1000 collect i)))
  (gc$)
  (time$ (loop for i fixnum from 1 to 100000 do (set::subset x x))))

In the future we may investigate developing a faster subset check based on galloping.

Definitions and Theorems

Function: fast-subset

(defun fast-subset (x y)
       (declare (xargs :guard (and (setp x) (setp y))))
       (mbe :logic (cond ((empty x) t)
                         ((empty y) nil)
                         ((<< (head x) (head y)) nil)
                         ((equal (head x) (head y))
                          (fast-subset (tail x) (tail y)))
                         (t (fast-subset x (tail y))))
            :exec (cond ((null x) t)
                        ((null y) nil)
                        ((fast-lexorder (car x) (car y))
                         (and (equal (car x) (car y))
                              (fast-subset (cdr x) (cdr y))))
                        (t (fast-subset x (cdr y))))))

Function: subset

(defun subset (x y)
       (declare (xargs :guard (and (setp x) (setp y))))
       (mbe :logic (if (empty x)
                       t
                       (and (in (head x) y)
                            (subset (tail x) y)))
            :exec (fast-subset x y)))

Theorem: subset-type

(defthm subset-type
        (or (equal (subset x y) t)
            (equal (subset x y) nil))
        :rule-classes :type-prescription)

Theorem: subset-sfix-cancel-x

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

Theorem: subset-sfix-cancel-y

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

Theorem: empty-subset

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

Theorem: empty-subset-2

(defthm empty-subset-2
        (implies (empty y)
                 (equal (subset x y) (empty x))))

Theorem: subset-in

(defthm subset-in
        (and (implies (and (subset x y) (in a x))
                      (in a y))
             (implies (and (in a x) (subset x y))
                      (in a y))))

Theorem: subset-in-2

(defthm subset-in-2
        (and (implies (and (subset x y) (not (in a y)))
                      (not (in a x)))
             (implies (and (not (in a y)) (subset x y))
                      (not (in a x)))))

Theorem: subset-insert-x

(defthm subset-insert-x
        (equal (subset (insert a x) y)
               (and (subset x y) (in a y))))

Theorem: subset-reflexive

(defthm subset-reflexive (subset x x))

Theorem: subset-transitive

(defthm subset-transitive
        (and (implies (and (subset x y) (subset y z))
                      (subset x z))
             (implies (and (subset y z) (subset x y))
                      (subset x z))))

Theorem: subset-membership-tail

(defthm subset-membership-tail
        (implies (and (subset x y) (in a (tail x)))
                 (in a (tail y))))

Theorem: subset-membership-tail-2

(defthm subset-membership-tail-2
        (implies (and (subset x y) (not (in a (tail y))))
                 (not (in a (tail x)))))

Theorem: subset-insert

(defthm subset-insert (subset x (insert a x)))

Theorem: subset-tail

(defthm
     subset-tail (subset (tail x) x)
     :rule-classes ((:rewrite)
                    (:forward-chaining :trigger-terms ((tail x)))))