Commit 650de4e4 authored by Ralf Jung's avatar Ralf Jung

bump Iris, fix for disjoint union rename

parent b32936fa
Pipeline #14938 canceled with stage
in 10 minutes and 37 seconds
......@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
depends: [
"coq-iris" { (= "dev.2019-02-20.0.8a8c1405") | (= "dev") }
"coq-iris" { (= "dev.2019-02-22.0.0c5f29db") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
......@@ -31,13 +31,13 @@ Structure bag Σ `{!heapG Σ} := Bag {
{{{ True }}} newBag #() {{{ x γ, RET x; is_bag N γ x bag_contents γ }}};
pushBag_spec N P Q γ b v :
( (X : gmultiset val), bag_contents γ X P
={⊤∖↑N}= (bag_contents γ ({[v]} X) Q)) -
={⊤∖↑N}= (bag_contents γ ({[v]} X) Q)) -
{{{ is_bag N γ b P }}}
pushBag b (of_val v)
{{{ RET #(); Q }}};
popBag_spec N P Q γ b :
( (X : gmultiset val) (y : val),
bag_contents γ ({[y]} X) P
bag_contents γ ({[y]} X) P
={⊤∖↑N}= (bag_contents γ X Q (SOMEV y))) -
(bag_contents γ P ={⊤∖↑N}= (bag_contents γ Q NONEV)) -
{{{ is_bag N γ b P }}}
......
......@@ -23,19 +23,19 @@ Section proof.
(own γ (!{q} X))%I.
Lemma bagPart_compose (γ: gname) (q1 q2: Qp) (X Y : gmultiset val) :
bagPart γ q1 X - bagPart γ q2 Y - bagPart γ (q1+q2) (X Y).
bagPart γ q1 X - bagPart γ q2 Y - bagPart γ (q1+q2) (X Y).
Proof.
iIntros "Hp1 Hp2".
rewrite /bagPart -gmultiset_op_union -frac_op'.
rewrite /bagPart -gmultiset_op_disj_union -frac_op'.
rewrite frac_auth_frag_op own_op. iFrame.
Qed.
Lemma bagPart_decompose (γ: gname) (q: Qp) (X Y : gmultiset val) :
bagPart γ q (X Y) - bagPart γ (q/2) X bagPart γ (q/2) Y.
bagPart γ q (X Y) - bagPart γ (q/2) X bagPart γ (q/2) Y.
Proof.
iIntros "Hp".
assert (q = (q/2)+(q/2))%Qp as Hq by (by rewrite Qp_div_2).
rewrite /bagPart {1}Hq.
rewrite -gmultiset_op_union -frac_op'.
rewrite -gmultiset_op_disj_union -frac_op'.
rewrite frac_auth_frag_op own_op. iFrame.
Qed.
......@@ -59,17 +59,17 @@ Section proof.
Lemma pushBag_spec γb γ x v q Y :
{{{ bagM γb γ x bagPart γ q Y }}}
pushBag b x (of_val v)
{{{ RET #(); bagPart γ q ({[v]} Y) }}}.
{{{ RET #(); bagPart γ q ({[v]} Y) }}}.
Proof.
iIntros (Φ) "[#[Hbag Hinv] HP] HΦ". rewrite /bagM_inv.
iApply (pushBag_spec b NB (bagPart γ q Y)%I (bagPart γ q ({[v]} Y))%I with "[] [Hbag HP]"); eauto.
iApply (pushBag_spec b NB (bagPart γ q Y)%I (bagPart γ q ({[v]} Y))%I with "[] [Hbag HP]"); eauto.
iAlways. iIntros (X) "[Hb1 HP]".
iInv NI as (X') "[>Hb2 >Hown]" "Hcl".
iDestruct (bag_contents_agree with "Hb1 Hb2") as %<-.
iMod (bag_contents_update b ({[v]} X) with "[$Hb1 $Hb2]") as "[Hb1 Hb2]".
iMod (bag_contents_update b ({[v]} X) with "[$Hb1 $Hb2]") as "[Hb1 Hb2]".
rewrite /bagPart.
iMod (own_update_2 with "Hown HP") as "[Hown HP]".
{ apply (frac_auth_update _ _ _ ({[v]} X) ({[v]} Y)).
{ apply (frac_auth_update _ _ _ ({[v]} X) ({[v]} Y)).
do 2 rewrite (comm _ {[v]}).
apply gmultiset_local_update_alloc. }
iFrame. iApply "Hcl".
......@@ -78,7 +78,7 @@ Section proof.
Local Ltac multiset_solver :=
intro;
repeat (rewrite multiplicity_difference || rewrite multiplicity_union);
repeat (rewrite multiplicity_difference || rewrite multiplicity_disj_union);
(lia || naive_solver).
Lemma popBag_spec γb γ x X :
......@@ -97,20 +97,20 @@ Section proof.
iDestruct (bag_contents_agree with "Hb1 Hb2") as %<-.
iMod (bag_contents_update b Y with "[$Hb1 $Hb2]") as "[Hb1 Hb2]".
rewrite /bagPart.
iAssert (X = ({[y]} Y))%I with "[Hpart HPs]" as %->.
iAssert (X = ({[y]} Y))%I with "[Hpart HPs]" as %->.
{ iDestruct (own_valid_2 with "HPs Hpart") as %Hfoo.
apply frac_auth_agree in Hfoo. by unfold_leibniz. }
iMod (own_update_2 with "HPs Hpart") as "Hown".
{ apply (frac_auth_update _ _ _ (({[y]} Y) {[y]}) (({[y]} Y) {[y]})).
{ apply (frac_auth_update _ _ _ (({[y]} Y) {[y]}) (({[y]} Y) {[y]})).
apply gmultiset_local_update_dealloc; multiset_solver. }
iDestruct "Hown" as "[HPs Hpart]".
iMod ("Hcl" with "[-Hpart Hb1]") as "_".
{ iNext. iExists _; iFrame.
assert (Y = (({[y]} Y) {[y]})) as <-
assert (Y = (({[y]} Y) {[y]})) as <-
by (unfold_leibniz; multiset_solver).
iFrame. }
iModIntro. iNext. iFrame. iRight. iExists y; repeat iSplit; eauto.
iPureIntro. by apply elem_of_union_l, elem_of_singleton. }
iPureIntro. apply gmultiset_elem_of_disj_union. left. by apply elem_of_singleton. }
{ iAlways. iIntros "[Hb1 Hpart]".
iInv NI as (X') "[>Hb2 >HPs]" "Hcl".
iDestruct (bag_contents_agree with "Hb1 Hb2") as %<-.
......
......@@ -33,14 +33,14 @@ Section proof.
Lemma pushBag_spec γ x X v :
{{{ bagE γ x X }}}
pushBag b x (of_val v)
{{{ RET #(); bagE γ x ({[v]} X) }}}.
{{{ RET #(); bagE γ x ({[v]} X) }}}.
Proof.
iIntros (Φ) "Hbag HΦ".
iApply (pushBag_spec b N (bagE γ x X)%I (bagE γ x ({[v]} X))%I with "[] [Hbag]"); eauto.
iApply (pushBag_spec b N (bagE γ x X)%I (bagE γ x ({[v]} X))%I with "[] [Hbag]"); eauto.
{ iAlways. iIntros (Y) "[Hb1 Hb2]".
iDestruct "Hb2" as "[#Hbag Hb2]".
iDestruct (bag_contents_agree with "Hb1 Hb2") as %<-.
iMod (bag_contents_update b ({[v]} Y) with "[$Hb1 $Hb2]") as "[Hb1 Hb2]".
iMod (bag_contents_update b ({[v]} Y) with "[$Hb1 $Hb2]") as "[Hb1 Hb2]".
by iFrame. }
{ iDestruct "Hbag" as "[#Hbag Hb]". iFrame "Hbag". eauto. }
Qed.
......@@ -49,11 +49,11 @@ Section proof.
{{{ bagE γ x X }}}
popBag b x
{{{ v, RET v; (X = ∅⌝ v = NONEV bagE γ x )
( Y y, X = {[y]} Y v = SOMEV y bagE γ x Y)}}}.
( Y y, X = {[y]} Y v = SOMEV y bagE γ x Y)}}}.
Proof.
iIntros (Φ) "Hbag HΦ".
iApply (popBag_spec b N (bagE γ x X)%I (fun v => (X = ∅⌝ v = NONEV bagE γ x )
( Y y, X = {[y]} Y v = SOMEV y bagE γ x Y))%I γ with "[] [] [Hbag]"); eauto.
( Y y, X = {[y]} Y v = SOMEV y bagE γ x Y))%I γ with "[] [] [Hbag]"); eauto.
{ iAlways. iIntros (Y y) "[Hb1 Hb2]".
iDestruct "Hb2" as "[#Hbag Hb2]".
iDestruct (bag_contents_agree with "Hb1 Hb2") as %<-.
......
......@@ -52,7 +52,7 @@ Section proof.
{ iAlways. iIntros (Y) "[Hb1 HP]".
iInv NI as (X) "[>Hb2 HPs]" "Hcl".
iDestruct (bag_contents_agree with "Hb1 Hb2") as %<-.
iMod (bag_contents_update b ({[v]} Y) with "[$Hb1 $Hb2]") as "[Hb1 Hb2]".
iMod (bag_contents_update b ({[v]} Y) with "[$Hb1 $Hb2]") as "[Hb1 Hb2]".
iFrame. iApply "Hcl".
iNext. iExists _; iFrame.
rewrite big_sepMS_singleton. iFrame. }
......@@ -70,7 +70,7 @@ Section proof.
iInv NI as (X) "[>Hb2 HPs]" "Hcl".
iDestruct (bag_contents_agree with "Hb1 Hb2") as %<-.
iMod (bag_contents_update b Y with "[$Hb1 $Hb2]") as "[Hb1 Hb2]".
rewrite big_sepMS_union bi.later_sep big_sepMS_singleton.
rewrite big_sepMS_disj_union bi.later_sep big_sepMS_singleton.
iDestruct "HPs" as "[HP HPs]".
iMod ("Hcl" with "[-HP Hb1]") as "_".
{ iNext. iExists _; iFrame. }
......
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