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

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

Theorem: emptyp-subset-2

(defthm emptyp-subset-2
  (implies (emptyp y)
           (equal (subset x y) (emptyp 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)))))