Commit 398bae9d authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Curry saved_prop_agree. This fixes #90.

parent af18cb32
......@@ -34,8 +34,9 @@ Section saved_prop.
Proof. by apply own_alloc. Qed.
Lemma saved_prop_agree γ x y :
saved_prop_own γ x saved_prop_own γ y (x y).
saved_prop_own γ x - saved_prop_own γ y - (x y).
apply wand_intro_r.
rewrite -own_op own_valid agree_validI agree_equivI later_equivI.
set (G1 := cFunctor_map F (iProp_fold, iProp_unfold)).
set (G2 := cFunctor_map F (@iProp_unfold Σ, @iProp_fold Σ)).
......@@ -78,7 +78,7 @@ Proof.
iIntros (????) "#HQ #H1 #H2 HQR"; iDestruct 1 as (Ψ) "[HPΨ HΨ]".
iDestruct (big_opS_delete _ _ i with "HΨ") as "[#HΨi HΨ]"; first done.
iExists (<[i1:=R1]> (<[i2:=R2]> Ψ)). iSplitL "HQR HPΨ".
- iPoseProof (saved_prop_agree i Q (Ψ i) with "[#]") as "Heq"; first by iSplit.
- iPoseProof (saved_prop_agree with "HQ HΨi") as "#Heq".
iNext. iRewrite "Heq" in "HQR". iIntros "HP". iSpecialize ("HPΨ" with "HP").
iDestruct (big_opS_delete _ _ i with "HPΨ") as "[HΨ HPΨ]"; first done.
iDestruct ("HQR" with "HΨ") as "[HR1 HR2]".
......@@ -153,7 +153,7 @@ Proof.
iMod ("Hclose" $! (State High (I {[ i ]})) ( : set token) with "[HΨ' Hl Hsp]").
{ iSplit; [iPureIntro; by eauto using wait_step|].
rewrite /barrier_inv /=. iNext. iFrame "Hl". iExists Ψ; iFrame. auto. }
iPoseProof (saved_prop_agree i Q (Ψ i) with "[#]") as "Heq"; first by auto.
iPoseProof (saved_prop_agree with "HQ HΨi") as "#Heq".
iModIntro. wp_if.
iApply "HΦ". iApply "HQR". by iRewrite "Heq".
Supports Markdown
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