Commit 404b952d authored by Robbert Krebbers's avatar Robbert Krebbers

Use multisets for U modality to be closer to the paper.

parent ac9bae94
......@@ -8,5 +8,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris-c-monad"]
depends: [
"coq-iris" { (= "dev.2019-01-25.3.6a8c782b") | (= "dev") }
"coq-iris" { (= "dev.2019-01-26.0.b036013f") | (= "dev") }
]
......@@ -395,15 +395,15 @@ Section proofs.
iDestruct "Henv" as (X σ _) "[Hlocks Hσ]".
wp_apply (mset_clear_spec with "Hlocks"); iIntros "Hlocks".
rewrite U_eq. iDestruct "H" as (us) "[Hus H]".
iInduction us as [|[ul [uq uv]] us] "IH" forall (σ); simpl.
iInduction us as [|[ul [uq uv]] us] "IH" using gmultiset_ind forall (σ); simpl.
- iModIntro. iSplitR "H".
+ iExists , σ. by iFrame.
+ iNext. cwp_lam. by iApply "H".
- iDestruct "Hus" as "[Hu Hus]".
- iDestruct "Hus" as "[Hu Hus]". rewrite !big_sepMS_singleton /=.
iDestruct (full_locking_heap_locked_present with "Hu Hσ") as %[z Hz].
iMod (full_locking_heap_unlock with "Hσ Hu") as "[Hσ Hu]".
iApply ("IH" with "Hus [H Hu] Hσ Hlocks").
iIntros "Hus". iApply "H". by iFrame.
iIntros "Hus". iApply "H". iFrame. by rewrite !big_sepMS_singleton /=.
Qed.
Lemma cwp_seq_bind R Φ x e1 e2 :
......
......@@ -8,9 +8,9 @@ Section U.
(** * Unlocking modality *)
Definition U_def (P : iProp Σ) : iProp Σ :=
( ls : list (cloc * (frac * val)),
([ list] x ls, x.1 C[LLvl]{x.2.1} x.2.2)
(([ list] x ls, x.1 C{x.2.1} x.2.2) - P))%I.
( ls : gmultiset (cloc * (frac * val)),
([ mset] x ls, x.1 C[LLvl]{x.2.1} x.2.2)
(([ mset] x ls, x.1 C{x.2.1} x.2.2) - P))%I.
Definition U_aux : seal (@U_def). by eexists. Qed.
Definition U := unseal U_aux.
Definition U_eq : @U = @U_def := seal_eq U_aux.
......@@ -25,7 +25,7 @@ Section U.
Proof. rewrite U_eq. solve_proper. Qed.
Lemma U_intro P : P U P.
Proof. iIntros "HP". rewrite U_eq. iExists []. eauto. Qed.
Proof. iIntros "HP". rewrite U_eq. iExists . eauto. Qed.
(** [U] behaves like an applicative functor aka "lax functor with a strength" *)
Lemma U_sep_2 P Q : U P U Q U (P Q).
......@@ -33,7 +33,7 @@ Section U.
iIntros "[HP HQ]". rewrite U_eq.
iDestruct "HP" as (ls1) "[HP1 HP2]".
iDestruct "HQ" as (ls2) "[HQ1 HQ2]".
iExists (ls1 ++ ls2). iFrame.
iExists (ls1 ls2). iFrame "HP1 HQ1".
iIntros "[HP1 HQ1]". iSplitL "HP1 HP2".
- by iApply "HP2".
- by iApply "HQ2".
......@@ -44,7 +44,8 @@ Section U.
Lemma U_unlock l q v : l C[LLvl]{q} v U (l C{q} v).
Proof.
iIntros "Hl". rewrite U_eq. iExists [(l,(q,v))]. iIntros "/= {$Hl} [$ _]".
iIntros "Hl". rewrite U_eq. iExists {[ (l,(q,v)) ]}.
rewrite !big_sepMS_singleton /=. auto with iFrame.
Qed.
(* Derived properties *)
......
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