union

(in-package "SET")

(include-book "membership")

(set-verify-guards-eagerness 2)

(local (encapsulate nil
    (defun fast-union-old
      (x y)
      (declare (xargs :measure (fast-measure x y)
          :guard (and (setp x) (setp y))
          :verify-guards nil))
      (cond ((endp x) y)
        ((endp y) x)
        ((equal (car x) (car y)) (cons (car x)
            (fast-union-old (cdr x) (cdr y))))
        ((fast-<< (car x) (car y)) (cons (car x)
            (fast-union-old (cdr x) y)))
        (t (cons (car y)
            (fast-union-old x (cdr y))))))
    (defthm fast-union-old-set
      (implies (and (setp x) (setp y))
        (setp (fast-union-old x y)))
      :hints (("Goal" :in-theory (enable (:ruleset low-level-rules)))))
    (defthm member-of-fast-union-old
      (iff (member a (fast-union-old x y))
        (or (member a x) (member a y))))
    (defthm fast-union-old-membership
      (implies (and (setp x) (setp y))
        (equal (in a (fast-union-old x y))
          (or (in a x) (in a y))))
      :hints (("Goal" :do-not '(generalize fertilize)
         :in-theory (enable (:ruleset low-level-rules)))))
    (verify-guards fast-union-old
      :hints (("Goal" :in-theory (enable (:ruleset low-level-rules)))))))

(defun fast-union
  (x y acc)
  (declare (xargs :measure (fast-measure x y)
      :guard (and (setp x)
        (setp y)
        (true-listp acc))
      :verify-guards nil))
  (cond ((endp x) (revappend acc y))
    ((endp y) (revappend acc x))
    ((equal (car x) (car y)) (fast-union (cdr x)
        (cdr y)
        (cons (car x) acc)))
    ((mbe :logic (<< (car x) (car y))
       :exec (fast-lexorder (car x) (car y))) (fast-union (cdr x)
        y
        (cons (car x) acc)))
    (t (fast-union x
        (cdr y)
        (cons (car y) acc)))))

(verify-guards fast-union
  :hints (("Goal" :do-not '(generalize fertilize)
     :in-theory (enable (:ruleset low-level-rules)))))

(encapsulate nil
  (local (defthm lemma
      (equal (fast-union x y acc)
        (revappend acc (fast-union-old x y)))
      :hints (("Goal" :in-theory (enable (:ruleset low-level-rules))))))
  (local (defthm lemma2
      (equal (fast-union x y nil)
        (fast-union-old x y))))
  (defthm fast-union-set
    (implies (and (force (setp x))
        (force (setp y)))
      (setp (fast-union x y nil))))
  (defthm fast-union-membership
    (implies (and (setp x) (setp y))
      (equal (in a (fast-union x y nil))
        (or (in a x) (in a y)))))
  (in-theory (disable fast-union
      fast-union-set
      fast-union-membership)))

(defsection union
  :parents (std/osets)
  :short "@(call union) constructs the union of @('X') and @('Y')."
  :long "<p>The logical definition is very simple, and the essential
correctness property is given by @('union-in').</p>

<p>The execution uses a better, O(n) algorithm to merge the sets by exploiting
the set order.</p>"
  (defun-inline union
    (x y)
    (declare (xargs :guard (and (setp x) (setp y))
        :verify-guards nil))
    (mbe :logic (if (emptyp x)
        (sfix y)
        (insert (head x)
          (union (tail x) y)))
      :exec (fast-union x y nil)))
  (defthm union-set
    (setp (union x y)))
  (defthm union-sfix-cancel-x
    (equal (union (sfix x) y)
      (union x y)))
  (defthm union-sfix-cancel-y
    (equal (union x (sfix y))
      (union x y)))
  (defthm union-emptyp-x
    (implies (emptyp x)
      (equal (union x y) (sfix y))))
  (defthm union-emptyp-y
    (implies (emptyp y)
      (equal (union x y) (sfix x))))
  (defthm union-emptyp
    (equal (emptyp (union x y))
      (and (emptyp x) (emptyp y))))
  (defthm union-in
    (equal (in a (union x y))
      (or (in a x) (in a y))))
  (verify-guards union$inline
    :hints (("Goal" :in-theory (enable fast-union-set fast-union-membership))))
  (defthm union-symmetric
    (equal (union x y) (union y x))
    :rule-classes ((:rewrite :loop-stopper ((x y)))))
  (defthm union-subset-x
    (subset x (union x y)))
  (defthm union-subset-y
    (subset y (union x y)))
  (defthm union-insert-x
    (equal (union (insert a x) y)
      (insert a (union x y))))
  (defthm union-insert-y
    (equal (union x (insert a y))
      (insert a (union x y))))
  (defthm union-with-subset-left
    (implies (subset x y)
      (equal (union x y) (sfix y)))
    :rule-classes ((:rewrite :backchain-limit-lst 1)))
  (defthm union-with-subset-right
    (implies (subset x y)
      (equal (union y x) (sfix y)))
    :rule-classes ((:rewrite :backchain-limit-lst 1)))
  (defthm union-self
    (equal (union x x) (sfix x)))
  (defthm union-associative
    (equal (union (union x y) z)
      (union x (union y z))))
  (defthm union-commutative
    (equal (union x (union y z))
      (union y (union x z)))
    :rule-classes ((:rewrite :loop-stopper ((x y)))))
  (defthm union-outer-cancel
    (equal (union x (union x z))
      (union x z))))