From 68bc02331ccb3bcc129874cf35b901fa31a760b1 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 22 Jul 2016 15:09:27 +0200
Subject: [PATCH] Remove some generic decision procedures for sets.

These just make things more complicated, it would be more useful to
declare (efficient) decision procedures for each instance, so that
we can properly predict which instance we will get.
---
 theories/collections.v     |  9 ---------
 theories/fin_collections.v | 14 +-------------
 2 files changed, 1 insertion(+), 22 deletions(-)

diff --git a/theories/collections.v b/theories/collections.v
index 888be9b6..12ead013 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -115,15 +115,6 @@ Section simple_collection.
     Lemma non_empty_singleton_L x : {[ x ]} ≠ ∅.
     Proof. unfold_leibniz. apply non_empty_singleton. Qed.
   End leibniz.
-
-  Section dec.
-    Context `{∀ X Y : C, Decision (X ⊆ Y)}.
-    Global Instance elem_of_dec_slow (x : A) (X : C) : Decision (x ∈ X) | 100.
-    Proof.
-      refine (cast_if (decide_rel (⊆) {[ x ]} X));
-        by rewrite elem_of_subseteq_singleton.
-    Defined.
-  End dec.
 End simple_collection.
 
 (** * Tactics *)
diff --git a/theories/fin_collections.v b/theories/fin_collections.v
index 21d8476a..c4eb7c51 100644
--- a/theories/fin_collections.v
+++ b/theories/fin_collections.v
@@ -101,24 +101,12 @@ Proof.
     intros x; rewrite !elem_of_elements; set_solver.
   - intros. by rewrite elem_of_app, !elem_of_elements, elem_of_union.
 Qed.
+
 Instance elem_of_dec_slow (x : A) (X : C) : Decision (x ∈ X) | 100.
 Proof.
   refine (cast_if (decide_rel (∈) x (elements X)));
     by rewrite <-(elem_of_elements _).
 Defined.
-Global Program Instance collection_subseteq_dec_slow (X Y : C) :
-    Decision (X ⊆ Y) | 100 :=
-  match decide_rel (=) (size (X ∖ Y)) 0 return _ with
-  | left _ => left _ | right _ => right _
-  end.
-Next Obligation.
-  intros X Y E1 x ?; apply dec_stable; intro. destruct (proj1(elem_of_empty x)).
-  apply (size_empty_inv _ E1). by rewrite elem_of_difference.
-Qed.
-Next Obligation.
-  intros X Y E1 E2; destruct E1. apply size_empty_iff, equiv_empty. intros x.
-  rewrite elem_of_difference. intros [E3 ?]. by apply E2 in E3.
-Qed.
 Lemma size_union_alt X Y : size (X ∪ Y) = size X + size (Y ∖ X).
 Proof.
   rewrite <-size_union by set_solver.
-- 
GitLab