Commit c02ea520 authored by Ralf Jung's avatar Ralf Jung

prove that we can pick a fresh location

parent f71e526a
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 *)
......
......@@ -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
......
......@@ -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.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment