From 631a05533c42bc9d96204bdc3ddb14ba55db66b2 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.
---
 prelude/collections.v     |  9 ---------
 prelude/fin_collections.v | 14 +-------------
 2 files changed, 1 insertion(+), 22 deletions(-)

diff --git a/prelude/collections.v b/prelude/collections.v
index 9a08413fc..ef1103b26 100644
--- a/prelude/collections.v
+++ b/prelude/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/prelude/fin_collections.v b/prelude/fin_collections.v
index 0fdf95e92..fd557f5c0 100644
--- a/prelude/fin_collections.v
+++ b/prelude/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