From 834b2046caff105f16b3c5c2cb6357d9d671a788 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 29 Jul 2016 11:30:24 +0200
Subject: [PATCH] Conversion from coPset to gset positive.

---
 prelude/coPset.v | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

diff --git a/prelude/coPset.v b/prelude/coPset.v
index 9e37b07d0..85aec1c9c 100644
--- a/prelude/coPset.v
+++ b/prelude/coPset.v
@@ -315,9 +315,22 @@ Proof.
   apply coPset_finite_spec; destruct X as [[t ?]]; apply of_Pset_raw_finite.
 Qed.
 
-(** * Conversion from gsets of positives *)
+(** * Conversion to and from gsets of positives *)
+Lemma to_gset_wf (m : Pmap ()) : gmap_wf (K:=positive) m.
+Proof. done. Qed.
+Definition to_gset (X : coPset) : gset positive :=
+  let 'Mapset m := to_Pset X in
+  Mapset (GMap m (bool_decide_pack _ (to_gset_wf m))).
+
 Definition of_gset (X : gset positive) : coPset :=
   let 'Mapset (GMap (PMap t Ht) _) := X in of_Pset_raw t ↾ of_Pset_wf _ Ht.
+
+Lemma elem_of_to_gset X i : set_finite X → i ∈ to_gset X ↔ i ∈ X.
+Proof.
+  intros ?. rewrite <-elem_of_to_Pset by done.
+  unfold to_gset. by destruct (to_Pset X).
+Qed.
+
 Lemma elem_of_of_gset X i : i ∈ of_gset X ↔ i ∈ X.
 Proof. destruct X as [[[t ?]]]; apply elem_of_of_Pset_raw. Qed.
 Lemma of_gset_finite X : set_finite (of_gset X).
-- 
GitLab