From c02ea520606e678b8ac9c09093073dbd47c47f3c 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

---
 barrier/heap_lang.v |  5 +++--
 barrier/lifting.v   |  6 ++++--
 prelude/gmap.v      | 17 +++++++++++++++++
 3 files changed, 24 insertions(+), 4 deletions(-)

diff --git a/barrier/heap_lang.v b/barrier/heap_lang.v
index 9ac5c9094..a23dbaca9 100644
--- a/barrier/heap_lang.v
+++ b/barrier/heap_lang.v
@@ -1,7 +1,8 @@
 Require Import Autosubst.Autosubst.
 Require Import prelude.option prelude.gmap iris.language.
 
-(** Some tactics useful when dealing with equality of sigma-like types: existT T0 t0 = existT T1 t1.
+(** Some tactics useful when dealing with equality of sigma-like types:
+    existT T0 t0 = existT T1 t1.
     They all assume such an equality is the first thing on the "stack" (goal). *)
 Ltac case_depeq1 := let Heq := fresh "Heq" in
   case=>_ /EqdepFacts.eq_sigT_sig_eq=>Heq;
@@ -20,7 +21,7 @@ Ltac case_depeq3 := let Heq := fresh "Heq" in
   destruct Heq as (->,<-).
 
 (** Expressions and values. *)
-Definition loc := nat. (* Any countable type. *)
+Definition loc := positive. (* Really, any countable type. *)
 
 Inductive expr :=
 (* Base lambda calculus *)
diff --git a/barrier/lifting.v b/barrier/lifting.v
index 7aa8401cb..56dbe7131 100644
--- a/barrier/lifting.v
+++ b/barrier/lifting.v
@@ -56,7 +56,9 @@ Proof.
   - intros e2 σ2 ef Hstep. inversion_clear Hstep. split; first done.
     rewrite v2v in Hv. inversion_clear Hv.
     eexists; split_ands; done.
-  - (* RJ FIXME: Need to find a fresh location. *) admit.
+  - set (l := fresh $ dom (gset loc) σ).
+    exists (Loc l), ((<[l:=v]>)σ), None. eapply AllocS; first by rewrite v2v.
+    apply (not_elem_of_dom (D := gset loc)). apply is_fresh.
   - reflexivity.
   - reflexivity.
   - (* RJ FIXME I am sure there is a better way to invoke right_id, but I could not find it. *)
@@ -69,7 +71,7 @@ Proof.
     erewrite <-exist_intro with (a := l). apply and_intro.
     + by apply const_intro.
     + done.
-Abort.
+Qed.
 
 Lemma wp_load E σ l v:
   σ !! l = Some v →
diff --git a/prelude/gmap.v b/prelude/gmap.v
index 68530c024..917bfb29e 100644
--- a/prelude/gmap.v
+++ b/prelude/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