`(subset x y)` determines if

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.

**Function: **

(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: **

(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: **

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

**Theorem: **

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

**Theorem: **

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

**Theorem: **

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

**Theorem: **

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

**Theorem: **

(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: **

(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: **

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

**Theorem: **

(defthm subset-reflexive (subset x x))

**Theorem: **

(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: **

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

**Theorem: **

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

**Theorem: **

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

**Theorem: **

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