Commit 3ebc0000 authored by Robbert's avatar Robbert

Merge branch 'cinv_open_stronger' into 'master'

Added a stronger version of cinv_open_strong

See merge request iris/iris!326
parents 1bb62ee3 27426fec
Pipeline #20891 passed with stage
in 16 minutes and 26 seconds
...@@ -9,6 +9,8 @@ Coq development, but not every API-breaking change is listed. Changes marked ...@@ -9,6 +9,8 @@ Coq development, but not every API-breaking change is listed. Changes marked
* [#] Redefine invariants as "semantic invariants" so that they support * [#] Redefine invariants as "semantic invariants" so that they support
splitting and other forms of weakening. splitting and other forms of weakening.
* Updated the strong variant of the opening lemma for cancellable invariants
to match that of regular invariants, where you can pick the mask at a later time.
**Changes in Coq:** **Changes in Coq:**
......
...@@ -81,17 +81,24 @@ Section proofs. ...@@ -81,17 +81,24 @@ Section proofs.
Lemma cinv_open_strong E N γ p P : Lemma cinv_open_strong E N γ p P :
N E N E
cinv N γ P - cinv_own γ p ={E,E∖↑N}= cinv N γ P - (cinv_own γ p ={E,E∖↑N}=
P cinv_own γ p ( P cinv_own γ 1 ={E∖↑N,E}= True). P cinv_own γ p ( E' : coPset, P cinv_own γ 1 ={E',N E'}= True)).
Proof. Proof.
iIntros (?) "#Hinv Hγ". iDestruct "Hinv" as (P') "[#HP' Hinv]". iIntros (?) "Hinv Hown".
iInv N as "[HP | >Hγ']" "Hclose". unfold cinv. iDestruct "Hinv" as (P') "[#HP' Hinv]".
- iIntros "!> {$Hγ}". iSplitL "HP". iPoseProof (inv_open ( N) N (P cinv_own γ 1) with "[Hinv]") as "H"; first done.
+ iNext. iApply "HP'". done. { iApply inv_iff=> //.
+ iIntros "[HP|Hγ]". iModIntro. iModIntro.
* iApply "Hclose". iLeft. iNext. by iApply "HP'". iSplit; iIntros "[H | $]"; iDestruct ("HP'" with "H") as "$". }
* iApply "Hclose". iRight. by iNext. rewrite difference_diag_L.
- iDestruct (cinv_own_1_l with "Hγ' Hγ") as %[]. iPoseProof (fupd_mask_frame_r _ _ (E N) with "H") as "H"; first set_solver.
rewrite left_id_L -union_difference_L //. iMod "H" as "[[$ | >HP] H]".
- iFrame "Hown". iModIntro.
iIntros (E') "HP".
iPoseProof (fupd_mask_frame_r _ _ E' with "(H [HP])") as "H"; first set_solver.
{ iDestruct "HP" as "[HP | Hown]"; eauto. }
by rewrite left_id_L.
- iDestruct (cinv_own_1_l with "HP Hown") as %[].
Qed. Qed.
Lemma cinv_alloc E N P : P ={E}= γ, cinv N γ P cinv_own γ 1. Lemma cinv_alloc E N P : P ={E}= γ, cinv N γ P cinv_own γ 1.
...@@ -104,6 +111,7 @@ Section proofs. ...@@ -104,6 +111,7 @@ Section proofs.
Proof. Proof.
iIntros (?) "#Hinv Hγ". iIntros (?) "#Hinv Hγ".
iMod (cinv_open_strong with "Hinv Hγ") as "($ & Hγ & H)"; first done. iMod (cinv_open_strong with "Hinv Hγ") as "($ & Hγ & H)"; first done.
rewrite {2}(union_difference_L (N) E)=> //.
iApply "H". by iRight. iApply "H". by iRight.
Qed. Qed.
...@@ -113,7 +121,9 @@ Section proofs. ...@@ -113,7 +121,9 @@ Section proofs.
Proof. Proof.
iIntros (?) "#Hinv Hγ". iIntros (?) "#Hinv Hγ".
iMod (cinv_open_strong with "Hinv Hγ") as "($ & $ & H)"; first done. iMod (cinv_open_strong with "Hinv Hγ") as "($ & $ & H)"; first done.
iIntros "!> HP". iApply "H"; auto. iIntros "!> HP".
rewrite {2}(union_difference_L (N) E)=> //.
iApply "H". by iLeft.
Qed. Qed.
Global Instance into_inv_cinv N γ P : IntoInv (cinv N γ P) N := {}. Global Instance into_inv_cinv N γ P : IntoInv (cinv N γ P) N := {}.
......
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