From 9424b7b7678415dbf984932fdb20693cedc83bb0 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Wed, 27 Jan 2016 10:39:54 +0100
Subject: [PATCH] prove that we can pick a fresh location

---
 theories/gmap.v | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/theories/gmap.v b/theories/gmap.v
index 68530c02..917bfb29 100644
--- a/theories/gmap.v
+++ b/theories/gmap.v
@@ -117,3 +117,20 @@ Notation gset K := (mapset (gmap K)).
 Instance gset_dom `{Countable K} {A} : Dom (gmap K A) (gset K) := mapset_dom.
 Instance gset_dom_spec `{Countable K} :
   FinMapDom K (gmap K) (gset K) := mapset_dom_spec.
+
+(** * Fresh positive *)
+Definition Gfresh {A} (m : gmap positive A) : positive :=
+  Pfresh $ gmap_car m.
+Lemma Gfresh_fresh {A} (m : gmap positive A) : m !! Gfresh m = None.
+Proof. destruct m as [[]]. apply Pfresh_fresh; done. Qed. 
+
+Instance Gset_fresh : Fresh positive (gset positive) := λ X,
+  let (m) := X in Gfresh m.
+Instance Gset_fresh_spec : FreshSpec positive (gset positive).
+Proof.
+  split.
+  * apply _.
+  * intros X Y; rewrite <-elem_of_equiv_L. by intros ->.
+  * unfold elem_of, mapset_elem_of, fresh; intros [m]; simpl.
+    by rewrite Gfresh_fresh.
+Qed.
-- 
GitLab