difference

(in-package "SET")

(include-book "membership")

(set-verify-guards-eagerness 2)

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

(verify-guards fast-difference-old
  :hints (("Goal" :in-theory (enable (:ruleset low-level-rules)))))

(local (encapsulate nil
    (local (defthm l0
        (implies (and (consp (fast-difference-old x y))
            (or (atom x) (<< a (car x)))
            (setp x))
          (<< a
            (car (fast-difference-old x y))))
        :hints (("Goal" :in-theory (enable (:ruleset low-level-rules))))))
    (defthm fast-difference-old-set
      (implies (and (setp x) (setp y))
        (setp (fast-difference-old x y)))
      :hints (("Goal" :in-theory (enable (:ruleset low-level-rules)))))
    (local (defthm l1
        (implies (and (member a x)
            (not (member a y))
            (setp x)
            (setp y))
          (member a (fast-difference-old x y)))
        :hints (("Goal" :in-theory (enable (:ruleset low-level-rules))))))
    (local (defthm l2
        (implies (and (member a (fast-difference-old x y))
            (setp x)
            (setp y))
          (and (member a x) (not (member a y))))
        :hints (("Goal" :in-theory (enable (:ruleset low-level-rules))))))
    (local (defthm member-of-fast-difference-old
        (implies (and (setp x) (setp y))
          (iff (member a (fast-difference-old x y))
            (and (member a x) (not (member a y)))))))
    (defthm fast-difference-old-membership
      (implies (and (setp x) (setp y))
        (equal (in a (fast-difference-old x y))
          (and (in a x) (not (in a y)))))
      :hints (("Goal" :in-theory (enable (:ruleset low-level-rules)))))))

(defun fast-difference
  (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 nil))
    ((endp y) (revappend acc x))
    ((equal (car x) (car y)) (fast-difference (cdr x) (cdr y) acc))
    ((mbe :logic (<< (car x) (car y))
       :exec (fast-lexorder (car x) (car y))) (fast-difference (cdr x)
        y
        (cons (car x) acc)))
    (t (fast-difference x (cdr y) acc))))

(verify-guards fast-difference
  :hints (("Goal" :in-theory (enable (:ruleset low-level-rules)))))

(encapsulate nil
  (local (defthm lemma
      (implies (true-listp acc)
        (equal (fast-difference x y acc)
          (revappend acc
            (fast-difference-old x y))))))
  (local (defthm lemma2
      (equal (fast-difference x y nil)
        (fast-difference-old x y))))
  (defthm fast-difference-set
    (implies (and (force (setp x))
        (force (setp y)))
      (setp (fast-difference x y nil))))
  (defthm fast-difference-membership
    (implies (and (setp x) (setp y))
      (equal (in a (fast-difference x y nil))
        (and (in a x) (not (in a y))))))
  (in-theory (disable fast-difference
      fast-difference-set
      fast-difference-membership)))

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

<p>The execution uses a better, O(n) algorithm to remove the elements by
exploiting the set order.</p>"
  (defun-inline difference
    (x y)
    (declare (xargs :guard (and (setp x) (setp y))
        :verify-guards nil))
    (mbe :logic (cond ((emptyp x) (sfix x))
        ((in (head x) y) (difference (tail x) y))
        (t (insert (head x)
            (difference (tail x) y))))
      :exec (fast-difference x y nil)))
  (defthm difference-set
    (setp (difference x y)))
  (defthm difference-sfix-x
    (equal (difference (sfix x) y)
      (difference x y)))
  (defthm difference-sfix-y
    (equal (difference x (sfix y))
      (difference x y)))
  (defthm difference-emptyp-x
    (implies (emptyp x)
      (equal (difference x y) (sfix x))))
  (defthm difference-emptyp-y
    (implies (emptyp y)
      (equal (difference x y) (sfix x))))
  (encapsulate nil
    (local (defthm difference-in-x
        (implies (in a (difference x y))
          (in a x))))
    (local (defthm difference-in-y
        (implies (in a (difference x y))
          (not (in a y)))))
    (defthm difference-in
      (equal (in a (difference x y))
        (and (in a x) (not (in a y))))))
  (encapsulate nil
    (local (defthm l0
        (implies (and (setp y)
            (setp x)
            (emptyp x))
          (not (fast-difference x y nil)))
        :hints (("Goal" :in-theory (enable fast-difference
             (:ruleset low-level-rules))))))
    (verify-guards difference$inline
      :hints (("Goal" :in-theory (enable fast-difference-set
           fast-difference-membership)))))
  (defthm difference-subset-x
    (subset (difference x y) x))
  (defthm subset-difference
    (equal (emptyp (difference x y))
      (subset x y))
    :hints (("Goal" :in-theory (enable subset))))
  (defthm difference-insert-x
    (equal (difference (insert a x) y)
      (if (in a y)
        (difference x y)
        (insert a (difference x y)))))
  (defthm difference-preserves-subset
    (implies (subset x y)
      (subset (difference x z)
        (difference y z)))))