From 809e0d1d24f67e62b1958e4b3a6b6b57b3f8b556 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 24 Apr 2019 10:34:32 +0200
Subject: [PATCH] Generalize `gset_to_propset` to `set_to_propset` for any
 SemiSet.

This closes issue #25.
---
 theories/gmap.v    | 5 -----
 theories/propset.v | 6 ++++++
 2 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/theories/gmap.v b/theories/gmap.v
index feff8ab1..4de58576 100644
--- a/theories/gmap.v
+++ b/theories/gmap.v
@@ -237,11 +237,6 @@ Section gset.
   Global Instance gset_dom {A} : Dom (gmap K A) (gset K) := mapset_dom.
   Global Instance gset_dom_spec : FinMapDom K (gmap K) (gset K) := mapset_dom_spec.
 
-  Definition gset_to_propset (X : gset K) : propset K :=
-    {[ x | x ∈ X ]}.
-  Lemma elem_of_gset_to_propset (X : gset K) x : x ∈ gset_to_propset X ↔ x ∈ X.
-  Proof. done. Qed.
-
   Definition gset_to_gmap {A} (x : A) (X : gset K) : gmap K A :=
     (λ _, x) <$> mapset_car X.
 
diff --git a/theories/propset.v b/theories/propset.v
index 9d7165ad..529dd471 100644
--- a/theories/propset.v
+++ b/theories/propset.v
@@ -34,6 +34,12 @@ Lemma top_subseteq {A} (X : propset A) : X ⊆ ⊤.
 Proof. done. Qed.
 Hint Resolve top_subseteq : core.
 
+Definition set_to_propset `{ElemOf A C} (X : C) : propset A :=
+  {[ x | x ∈ X ]}.
+Lemma elem_of_set_to_propset `{SemiSet A C} x (X : C) :
+  x ∈ set_to_propset X ↔ x ∈ X.
+Proof. done. Qed.
+
 Instance propset_ret : MRet propset := λ A (x : A), {[ x ]}.
 Instance propset_bind : MBind propset := λ A B (f : A → propset B) (X : propset A),
   PropSet (λ b, ∃ a, b ∈ f a ∧ a ∈ X).
-- 
GitLab