Commit 97f90263 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Make use of better `iMod` for updates.

parent f086d04b
......@@ -114,14 +114,11 @@ Section proofs.
P cinv_own γ p ( E' : coPset, P cinv_own γ 1 ={E',N E'}= True)).
Proof.
iIntros (?) "Hinv Hown".
iPoseProof (inv_acc ( N) N with "Hinv") as "H"; first done.
rewrite difference_diag_L.
iPoseProof (fupd_mask_frame_r _ _ (E N) with "H") as "H"; first set_solver.
rewrite left_id_L -union_difference_L //. iMod "H" as "[[$ | >Hown'] H]".
- iIntros "{$Hown} !>" (E') "HP".
iPoseProof (fupd_mask_frame_r _ _ E' with "(H [HP])") as "H"; first set_solver.
{ iDestruct "HP" as "[?|?]"; eauto. }
by rewrite left_id_L.
iMod (inv_acc ( N) N with "Hinv") as "[[$ | >Hown'] H]"; first done.
- iApply fupd_intro_mask_eq; [set_solver|].
iIntros "{$Hown}" (E') "HP".
iMod ("H" with "[HP]") as "_"; [by iModIntro|set_solver|..].
by iApply fupd_intro_mask_eq; [set_solver|].
- iDestruct (cinv_own_1_l with "Hown' Hown") as %[].
Qed.
......@@ -131,9 +128,8 @@ Section proofs.
Proof.
iIntros (?) "#Hinv Hγ".
iMod (cinv_acc_strong with "Hinv Hγ") as "($ & $ & H)"; first done.
iIntros "!> HP".
rewrite {2}(union_difference_L (N) E)=> //.
iApply "H". by iLeft.
iIntros "!> HP". iMod ("H" with "[$HP]") as "_".
by rewrite -union_difference_L.
Qed.
(*** Other *)
......@@ -141,8 +137,8 @@ Section proofs.
Proof.
iIntros (?) "#Hinv Hγ".
iMod (cinv_acc_strong with "Hinv Hγ") as "($ & Hγ & H)"; first done.
rewrite {2}(union_difference_L (N) E)=> //.
iApply "H". by iRight.
iMod ("H" with "[$Hγ]") as "_".
by rewrite -union_difference_L.
Qed.
Global Instance into_inv_cinv N γ P : IntoInv (cinv N γ P) N := {}.
......
......@@ -65,7 +65,7 @@ Lemma fupd_plain_soundness `{!invPreG Σ} E1 E2 (P: iProp Σ) `{!Plain P} :
Proof.
iIntros (Hfupd). apply later_soundness. iMod wsat_alloc as (Hinv) "[Hw HE]".
iAssert (|={,E2}=> P)%I as "H".
{ iMod fupd_intro_mask'; last iApply Hfupd. done. }
{ iMod Hfupd as "$". iApply fupd_intro_mask_subseteq; [set_solver|]; auto. }
rewrite uPred_fupd_eq /uPred_fupd_def.
iMod ("H" with "[$]") as "[Hw [HE >H']]"; iFrame.
Qed.
......
......@@ -140,8 +140,8 @@ Section inv.
rewrite inv_eq. iIntros (??) "#HinvP #HinvQ !>"; iIntros (E ?).
iMod ("HinvP" with "[%]") as "[$ HcloseP]"; first set_solver.
iMod ("HinvQ" with "[%]") as "[$ HcloseQ]"; first set_solver.
iMod (fupd_intro_mask' _ (E N)) as "Hclose"; first set_solver.
iIntros "!> [HP HQ]".
iApply fupd_mask_subseteq; first set_solver.
iIntros "Hclose !> [HP HQ]".
iMod "Hclose" as %_. iMod ("HcloseQ" with "HQ") as %_. by iApply "HcloseP".
Qed.
......@@ -174,13 +174,10 @@ Section inv.
N E inv N P ={E,E∖↑N}= P E', P ={E',N E'}= True.
Proof.
iIntros (?) "Hinv".
iPoseProof (inv_acc ( N) N with "Hinv") as "H"; first done.
rewrite difference_diag_L.
iPoseProof (fupd_mask_frame_r _ _ (E N) with "H") as "H"; first set_solver.
rewrite left_id_L -union_difference_L //. iMod "H" as "[$ H]"; iModIntro.
iIntros (E') "HP".
iPoseProof (fupd_mask_frame_r _ _ E' with "(H HP)") as "H"; first set_solver.
by rewrite left_id_L.
iMod (inv_acc ( N) N with "Hinv") as "[$ H]"; first done.
iApply fupd_intro_mask_eq; [set_solver|].
iIntros (E') "HP". iMod ("H" with "HP") as "_"; [set_solver|].
by iApply fupd_intro_mask_eq; first set_solver.
Qed.
Lemma inv_acc_timeless E N P `{!Timeless P} :
......
......@@ -311,7 +311,7 @@ Section lemmas.
atomic_acc Eo Ei α P β Φ).
Proof.
iIntros (? x) "Hα Hclose".
iMod fupd_intro_mask' as "Hclose'"; last iModIntro; first set_solver.
iApply fupd_intro_mask_subseteq; [done|]; iIntros "Hclose'".
iExists x. iFrame. iSplitWith "Hclose".
- iIntros "Hα". iMod "Hclose'" as "_". iApply "Hclose". done.
- iIntros (y) "Hβ". iMod "Hclose'" as "_". iApply "Hclose". done.
......@@ -331,7 +331,7 @@ Section lemmas.
to happen only if one argument is a constructor. *)
iIntros "Hinner >Hacc". iDestruct "Hacc" as (x') "[Hα' Hclose]".
iMod ("Hinner" with "Hα'") as (x) "[Hα Hclose']".
iMod (fupd_intro_mask') as "Hclose''"; last iModIntro; first done.
iApply fupd_intro_mask_subseteq; [done|]; iIntros "Hclose''".
iExists x. iFrame. iSplitWith "Hclose'".
- iIntros "Hα". iMod "Hclose''" as "_".
iMod ("Hclose'" with "Hα") as "[Hβ' HPas]".
......
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