Commit 6606345b authored by Ralf Jung's avatar Ralf Jung
Browse files

fix previous commit

parent 650de4e4
Pipeline #15060 passed with stage
in 11 minutes and 38 seconds
...@@ -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.2019-02-22.0.0c5f29db") | (= "dev") } "coq-iris" { (= "dev.2019-02-22.1.9c04e2b4") | (= "dev") }
"coq-autosubst" { = "dev.coq86" } "coq-autosubst" { = "dev.coq86" }
] ]
...@@ -52,7 +52,7 @@ Section proof. ...@@ -52,7 +52,7 @@ Section proof.
Fixpoint bag_of_val (ls : val) : gmultiset val := Fixpoint bag_of_val (ls : val) : gmultiset val :=
match ls with match ls with
| NONEV => | NONEV =>
| SOMEV (v1, t) => {[v1]} bag_of_val t | SOMEV (v1, t) => {[v1]} bag_of_val t
| _ => | _ =>
end. end.
Fixpoint val_of_list (ls : list val) : val := Fixpoint val_of_list (ls : list val) : val :=
...@@ -62,7 +62,7 @@ Section proof. ...@@ -62,7 +62,7 @@ Section proof.
end. end.
Definition bag_inv (γb : gname) (b : loc) : iProp Σ := Definition bag_inv (γb : gname) (b : loc) : iProp Σ :=
( ls : list val, b (val_of_list ls) own γb ((1/2)%Qp, to_agree (list_to_set ls)))%I. ( ls : list val, b (val_of_list ls) own γb ((1/2)%Qp, to_agree (list_to_set_disj ls)))%I.
Definition is_bag (γb : gname) (x : val) := Definition is_bag (γb : gname) (x : val) :=
( (lk : val) (b : loc) (γ : gname), ( (lk : val) (b : loc) (γ : gname),
...@@ -116,7 +116,7 @@ Section proof. ...@@ -116,7 +116,7 @@ Section proof.
Local Opaque acquire release. (* so that wp_pure doesn't stumble *) Local Opaque acquire release. (* so that wp_pure doesn't stumble *)
Lemma pushBag_spec (P Q : iProp Σ) γ (x v : val) : Lemma pushBag_spec (P Q : iProp Σ) γ (x v : val) :
( (X : gmultiset val), bag_contents γ X P ( (X : gmultiset val), bag_contents γ X P
={∖↑N}= (bag_contents γ ({[v]} X) Q)) - ={∖↑N}= (bag_contents γ ({[v]} X) Q)) -
{{{ is_bag γ x P }}} {{{ is_bag γ x P }}}
pushBag x (of_val v) pushBag x (of_val v)
{{{ RET #(); Q }}}. {{{ RET #(); Q }}}.
...@@ -141,7 +141,7 @@ Section proof. ...@@ -141,7 +141,7 @@ Section proof.
Lemma popBag_spec (P : iProp Σ) (Q : val iProp Σ) γ x : Lemma popBag_spec (P : iProp Σ) (Q : val iProp Σ) γ x :
( (X : gmultiset val) (y : val), ( (X : gmultiset val) (y : val),
bag_contents γ ({[y]} X) P bag_contents γ ({[y]} X) P
={∖↑N}= (bag_contents γ X Q (SOMEV y))) - ={∖↑N}= (bag_contents γ X Q (SOMEV y))) -
(bag_contents γ P ={∖↑N}= (bag_contents γ Q NONEV)) - (bag_contents γ P ={∖↑N}= (bag_contents γ Q NONEV)) -
{{{ is_bag γ x P }}} {{{ is_bag γ x P }}}
......
...@@ -87,11 +87,11 @@ Section proof. ...@@ -87,11 +87,11 @@ Section proof.
iDestruct (mapsto_agree l' q q' (PairV x tl) (PairV y tl') iDestruct (mapsto_agree l' q q' (PairV x tl) (PairV y tl')
with "Hro Hro'") as %?. simplify_eq/=. with "Hro Hro'") as %?. simplify_eq/=.
iDestruct ("IH" with "Hls Hls'") as %->. done. iDestruct ("IH" with "Hls Hls'") as %->. done.
Qed. Qed.
Definition bag_inv (γb : gname) (b : loc) : iProp Σ := Definition bag_inv (γb : gname) (b : loc) : iProp Σ :=
( (hd : val) (ls : list val), ( (hd : val) (ls : list val),
b hd is_list hd ls own γb ((1/2)%Qp, to_agree (list_to_set ls)))%I. b hd is_list hd ls own γb ((1/2)%Qp, to_agree (list_to_set_disj ls)))%I.
Definition is_bag (γb : gname) (x : val) := Definition is_bag (γb : gname) (x : val) :=
( (b : loc), x = #b inv N (bag_inv γb b))%I. ( (b : loc), x = #b inv N (bag_inv γb b))%I.
Definition bag_contents (γb : gname) (X : gmultiset val) : iProp Σ := Definition bag_contents (γb : gname) (X : gmultiset val) : iProp Σ :=
...@@ -142,7 +142,7 @@ Section proof. ...@@ -142,7 +142,7 @@ Section proof.
Lemma pushBag_spec (P Q : iProp Σ) γ (x v : val) : Lemma pushBag_spec (P Q : iProp Σ) γ (x v : val) :
( (X : gmultiset val), bag_contents γ X P ( (X : gmultiset val), bag_contents γ X P
={∖↑N}= (bag_contents γ ({[v]} X) Q)) - ={∖↑N}= (bag_contents γ ({[v]} X) Q)) -
{{{ is_bag γ x P }}} {{{ is_bag γ x P }}}
pushBag x (of_val v) pushBag x (of_val v)
{{{ RET #(); Q }}}. {{{ RET #(); Q }}}.
...@@ -179,7 +179,7 @@ Section proof. ...@@ -179,7 +179,7 @@ Section proof.
Lemma popBag_spec (P : iProp Σ) (Q : val iProp Σ) γ x : Lemma popBag_spec (P : iProp Σ) (Q : val iProp Σ) γ x :
( (X : gmultiset val) (y : val), ( (X : gmultiset val) (y : val),
bag_contents γ ({[y]} X) P bag_contents γ ({[y]} X) P
={∖↑N}= (bag_contents γ X Q (SOMEV y))) - ={∖↑N}= (bag_contents γ X Q (SOMEV y))) -
(bag_contents γ P ={∖↑N}= (bag_contents γ Q NONEV)) - (bag_contents γ P ={∖↑N}= (bag_contents γ Q NONEV)) -
{{{ is_bag γ x P }}} {{{ is_bag γ x P }}}
......
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