Commit 9de17fa7 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'ralf/saved_prop' into 'master'

update for more general saved_prop

See merge request FP/iris-examples!1
parents 322cef94 39ed59b0
...@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"] ...@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"] install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"] remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
depends: [ depends: [
"coq-iris" { (= "dev.2017-10-28.10") | (= "dev") } "coq-iris" { (= "dev.2017-11-18.1") | (= "dev") }
"coq-autosubst" { = "dev.coq86" } "coq-autosubst" { = "dev.coq86" }
] ]
...@@ -10,9 +10,9 @@ Set Default Proof Using "Type". ...@@ -10,9 +10,9 @@ Set Default Proof Using "Type".
(** The CMRAs/functors we need. *) (** The CMRAs/functors we need. *)
Class barrierG Σ := BarrierG { Class barrierG Σ := BarrierG {
barrier_stsG :> stsG Σ sts; barrier_stsG :> stsG Σ sts;
barrier_savedPropG :> savedPropG Σ idCF; barrier_savedPropG :> savedPropG Σ;
}. }.
Definition barrierΣ : gFunctors := #[stsΣ sts; savedPropΣ idCF]. Definition barrierΣ : gFunctors := #[stsΣ sts; savedPropΣ].
Instance subG_barrierΣ {Σ} : subG barrierΣ Σ barrierG Σ. Instance subG_barrierΣ {Σ} : subG barrierΣ Σ barrierG Σ.
Proof. solve_inG. Qed. Proof. solve_inG. Qed.
...@@ -94,7 +94,7 @@ Proof. ...@@ -94,7 +94,7 @@ Proof.
iIntros (Φ) "_ HΦ". iIntros (Φ) "_ HΦ".
rewrite -wp_fupd /newbarrier /=. wp_seq. wp_alloc l as "Hl". rewrite -wp_fupd /newbarrier /=. wp_seq. wp_alloc l as "Hl".
iApply ("HΦ" with "[> -]"). iApply ("HΦ" with "[> -]").
iMod (saved_prop_alloc (F:=idCF) P) as (γ) "#?". iMod (saved_prop_alloc P) as (γ) "#?".
iMod (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]") iMod (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]")
as (γ') "[#? Hγ']"; eauto. as (γ') "[#? Hγ']"; eauto.
{ iNext. rewrite /barrier_inv /=. iFrame. { iNext. rewrite /barrier_inv /=. iFrame.
...@@ -165,8 +165,8 @@ Proof. ...@@ -165,8 +165,8 @@ Proof.
iIntros (?). iDestruct 1 as (γ P Q i) "(#Hsts & Hγ & #HQ & HQR)". iIntros (?). iDestruct 1 as (γ P Q i) "(#Hsts & Hγ & #HQ & HQR)".
iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]") iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto. as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
iMod (saved_prop_alloc_strong (R1: %CF (iProp Σ)) I) as (i1) "[% #Hi1]". iMod (saved_prop_alloc_strong I) as (i1) "[% #Hi1]".
iMod (saved_prop_alloc_strong (R2: %CF (iProp Σ)) (I {[i1]})) iMod (saved_prop_alloc_strong (I {[i1]}))
as (i2) "[Hi2' #Hi2]"; iDestruct "Hi2'" as %Hi2. as (i2) "[Hi2' #Hi2]"; iDestruct "Hi2'" as %Hi2.
rewrite ->not_elem_of_union, elem_of_singleton in Hi2; destruct Hi2. rewrite ->not_elem_of_union, elem_of_singleton in Hi2; destruct Hi2.
iMod ("Hclose" $! (State p ({[i1; i2]} I {[i]})) iMod ("Hclose" $! (State p ({[i1; i2]} I {[i]}))
......
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