### A stronger version of `cinv_open`.

`This version allows one to either close or cancel the invariant after opening it.`
parent b043f3a3
 ... @@ -70,6 +70,21 @@ Section proofs. ... @@ -70,6 +70,21 @@ Section proofs. iIntros "!>". iExists P. iSplit; last done. iIntros "!# !>"; iSplit; auto. iIntros "!>". iExists P. iSplit; last done. iIntros "!# !>"; iSplit; auto. Qed. Qed. Lemma cinv_open_strong E N γ p P : ↑N ⊆ E → cinv N γ P -∗ cinv_own γ p ={E,E∖↑N}=∗ ▷ P ∗ cinv_own γ p ∗ (▷ P ∨ cinv_own γ 1 ={E∖↑N,E}=∗ True). Proof. iIntros (?) "#Hinv Hγ". iDestruct "Hinv" as (P') "[#HP' Hinv]". iInv N as "[HP | >Hγ']" "Hclose". - iIntros "!> {\$Hγ}". iSplitL "HP". + iNext. iApply "HP'". done. + iIntros "[HP|Hγ]". * iApply "Hclose". iLeft. iNext. by iApply "HP'". * iApply "Hclose". iRight. by iNext. - iDestruct (cinv_own_1_l with "Hγ' Hγ") as %[]. 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. Proof. Proof. iIntros "HP". iMod (cinv_alloc_strong ∅ E N) as (γ _) "[Hγ Halloc]". iIntros "HP". iMod (cinv_alloc_strong ∅ E N) as (γ _) "[Hγ Halloc]". ... @@ -78,23 +93,18 @@ Section proofs. ... @@ -78,23 +93,18 @@ Section proofs. Lemma cinv_cancel E N γ P : ↑N ⊆ E → cinv N γ P -∗ cinv_own γ 1 ={E}=∗ ▷ P. Lemma cinv_cancel E N γ P : ↑N ⊆ E → cinv N γ P -∗ cinv_own γ 1 ={E}=∗ ▷ P. Proof. Proof. iIntros (?) "#Hinv Hγ". iDestruct "Hinv" as (P') "[#HP' Hinv]". iIntros (?) "#Hinv Hγ". iInv N as "[HP|>Hγ']" "Hclose". iMod (cinv_open_strong with "Hinv Hγ") as "(\$ & Hγ & H)"; first done. - iMod ("Hclose" with "[Hγ]") as "_"; first by eauto. iModIntro. iNext. iApply "H". by iRight. iApply "HP'". done. - iDestruct (cinv_own_1_l with "Hγ Hγ'") as %[]. Qed. Qed. Lemma cinv_open E N γ p P : Lemma cinv_open E N γ p P : ↑N ⊆ E → ↑N ⊆ E → cinv N γ P -∗ cinv_own γ p ={E,E∖↑N}=∗ ▷ P ∗ cinv_own γ p ∗ (▷ P ={E∖↑N,E}=∗ True). cinv N γ P -∗ cinv_own γ p ={E,E∖↑N}=∗ ▷ P ∗ cinv_own γ p ∗ (▷ P ={E∖↑N,E}=∗ True). Proof. Proof. iIntros (?) "#Hinv Hγ". iDestruct "Hinv" as (P') "[#HP' Hinv]". iIntros (?) "#Hinv Hγ". iInv N as "[HP | >Hγ']" "Hclose". iMod (cinv_open_strong with "Hinv Hγ") as "(\$ & \$ & H)"; first done. - iIntros "!> {\$Hγ}". iSplitL "HP". iIntros "!> HP". iApply "H"; auto. + iNext. iApply "HP'". done. + iIntros "HP". iApply "Hclose". iLeft. iNext. by iApply "HP'". - iDestruct (cinv_own_1_l with "Hγ' Hγ") as %[]. Qed. Qed. End proofs. End proofs. ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!