From 04f407300f560be9791b0e61a33c91fdf38a6f96 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 17 Nov 2015 15:49:51 +0100
Subject: [PATCH] Sets over A as A -> bool.

---
 prelude/bsets.v       | 35 +++++++++++++++++++++++++++++++++++
 prelude/collections.v |  2 +-
 2 files changed, 36 insertions(+), 1 deletion(-)
 create mode 100644 prelude/bsets.v

diff --git a/prelude/bsets.v b/prelude/bsets.v
new file mode 100644
index 000000000..87e1c50ea
--- /dev/null
+++ b/prelude/bsets.v
@@ -0,0 +1,35 @@
+(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* This file is distributed under the terms of the BSD license. *)
+(** This file implements bsets as functions into Prop. *)
+Require Export prelude.prelude.
+
+Record bset (A : Type) : Type := mkBSet { bset_car : A → bool }.
+Arguments mkBSet {_} _.
+Arguments bset_car {_} _ _.
+Definition bset_all {A} : bset A := mkBSet (λ _, true).
+Instance bset_empty {A} : Empty (bset A) := mkBSet (λ _, false).
+Instance bset_singleton {A} `{∀ x y : A, Decision (x = y)} :
+  Singleton A (bset A) := λ x, mkBSet (λ y, bool_decide (y = x)).
+Instance bset_elem_of {A} : ElemOf A (bset A) := λ x X, bset_car X x.
+Instance bset_union {A} : Union (bset A) := λ X1 X2,
+  mkBSet (λ x, bset_car X1 x || bset_car X2 x).
+Instance bset_intersection {A} : Intersection (bset A) := λ X1 X2,
+  mkBSet (λ x, bset_car X1 x && bset_car X2 x).
+Instance bset_difference {A} : Difference (bset A) := λ X1 X2,
+  mkBSet (λ x, bset_car X1 x && negb (bset_car X2 x)).
+Instance bset_collection {A} `{∀ x y : A, Decision (x = y)} :
+  Collection A (bset A).
+Proof.
+  split; [split| |].
+  * by intros x ?.
+  * by intros x y; rewrite <-(bool_decide_spec (x = y)).
+  * split. apply orb_prop_elim. apply orb_prop_intro.
+  * split. apply andb_prop_elim. apply andb_prop_intro.
+  * intros X Y x; unfold elem_of, bset_elem_of; simpl. 
+    destruct (bset_car X x), (bset_car Y x); simpl; tauto.
+Qed.
+Instance bset_elem_of_dec {A} x (X : bset A) : Decision (x ∈ X) := _.
+
+Typeclasses Opaque bset_elem_of.
+Global Opaque bset_empty bset_singleton bset_union
+  bset_intersection bset_difference.
diff --git a/prelude/collections.v b/prelude/collections.v
index dd1d2f9e9..a43a22e08 100644
--- a/prelude/collections.v
+++ b/prelude/collections.v
@@ -313,7 +313,7 @@ Section collection.
   End leibniz.
 
   Section dec.
-    Context `{∀ X Y : C, Decision (X ⊆ Y)}.
+    Context `{∀ (x : A) (X : C), Decision (x ∈ X)}.
     Lemma not_elem_of_intersection x X Y : x ∉ X ∩ Y ↔ x ∉ X ∨ x ∉ Y.
     Proof. rewrite elem_of_intersection. destruct (decide (x ∈ X)); tauto. Qed.
     Lemma not_elem_of_difference x X Y : x ∉ X ∖ Y ↔ x ∉ X ∨ x ∈ Y.
-- 
GitLab