under-set-equiv

(in-package "SET")

(include-book "outer")

(include-book "sort")

(include-book "std/lists/sets" :dir :system)

(defun all-list
  (x)
  (declare (xargs :guard (true-listp x)))
  (if (endp x)
    t
    (and (predicate (car x))
      (all-list (cdr x)))))

(encapsulate (((all-list-hyps) => *) ((all-list-list) => *))
  (local (defun all-list-hyps nil nil))
  (local (defun all-list-list nil nil))
  (defthmd list-membership-constraint
    (implies (all-list-hyps)
      (implies (member arbitrary-element (all-list-list))
        (predicate arbitrary-element)))))

(encapsulate nil
  (local (defun all-list-badguy
      (x)
      (if (consp x)
        (if (predicate (car x))
          (all-list-badguy (cdr x))
          (list (car x)))
        nil)))
  (local (defthmd all-list-badguy-membership-property
      (implies (all-list-badguy x)
        (and (member-equal (car (all-list-badguy x))
            x)
          (not (predicate (car (all-list-badguy x))))))
      :hints (("Goal" :induct (all-list-badguy x)))))
  (local (defthm all-list-badguy-under-iff
      (iff (all-list-badguy x)
        (not (all-list x)))
      :hints (("Goal" :in-theory (enable all-list)))))
  (defthmd all-list-by-membership
    (implies (all-list-hyps)
      (all-list (all-list-list)))
    :hints (("Goal" :in-theory (enable list-membership-constraint)
       :use ((:instance all-list-badguy-membership-property
          (x (all-list-list))))))))

(defund subsetp-equal-trigger
  (x y)
  (declare (xargs :guard (and (true-listp x) (true-listp y))))
  (subsetp-equal x y))

(defthm pick-a-point-subsetp-equal-strategy
  (implies (and (syntaxp (rewriting-goal-lit mfc state))
      (syntaxp (rewriting-conc-lit `(subsetp-equal ,SET::X ,SET::Y)
          mfc
          state)))
    (equal (subsetp-equal x y)
      (subsetp-equal-trigger x y)))
  :hints (("Goal" :in-theory (enable subsetp-equal-trigger))))

(automate-instantiation :new-hint-name pick-a-point-subsetp-equal-hint
  :generic-theorem all-list-by-membership
  :generic-predicate predicate
  :generic-hyps all-list-hyps
  :generic-collection all-list-list
  :generic-collection-predicate all-list
  :actual-collection-predicate subsetp-equal
  :actual-trigger subsetp-equal-trigger
  :predicate-rewrite (((predicate ?x ?y) (member-equal ?x ?y)))
  :tagging-theorem pick-a-point-subsetp-equal-strategy)

(local (defthm promote-member-to-in
    (implies (setp x)
      (iff (member a x) (in a x)))
    :hints (("Goal" :in-theory (enable in-to-member)))))

(local (in-theory (enable set-equiv)))

(defthm insert-under-set-equiv
  (set-equiv (insert a x)
    (cons a (sfix x)))
  :hints (("Goal" :do-not-induct t)))

(defthm delete-under-set-equiv
  (set-equiv (delete a x)
    (remove-equal a (sfix x))))

(encapsulate nil
  (local (defthm l0
      (subsetp (union x y)
        (append (sfix x) (sfix y)))))
  (local (defthm l1
      (subsetp (append (sfix x) (sfix y))
        (union x y))))
  (defthm union-under-set-equiv
    (set-equiv (union x y)
      (append (sfix x) (sfix y)))
    :hints (("Goal" :do-not-induct t))))

(defthm intersect-under-set-equiv
  (set-equiv (intersect x y)
    (intersection-equal (sfix x)
      (sfix y)))
  :hints (("Goal" :do-not-induct t)))

(defthm difference-under-set-equiv
  (set-equiv (difference x y)
    (set-difference-equal (sfix x)
      (sfix y)))
  :hints (("Goal" :do-not-induct t)))

(defthm mergesort-under-set-equiv
  (set-equiv (mergesort x) x)
  :hints (("Goal" :do-not-induct t)))

(encapsulate nil
  (local (defthm l0
      (implies (set-equiv x y)
        (subsetp (mergesort x) (mergesort y)))))
  (local (defthm l1
      (implies (and (subsetp x y) (member a x))
        (member a y))))
  (defcong set-equiv
    equal
    (mergesort x)
    1
    :event-name set-equiv-implies-equal-mergesort-1
    :hints (("Goal" :do-not-induct t
       :do-not '(generalize fertilize)
       :in-theory (enable set-equiv)))))