cancelable_invariants.v 2.46 KB
 Robbert Krebbers committed Aug 25, 2016 1 2 ``````From iris.program_logic Require Export invariants. From iris.algebra Require Export frac. `````` Robbert Krebbers committed Oct 05, 2016 3 ``````From iris.proofmode Require Import tactics. `````` Robbert Krebbers committed Aug 25, 2016 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 ``````Import uPred. Class cinvG Σ := cinv_inG :> inG Σ fracR. Section defs. Context `{irisG Λ Σ, cinvG Σ}. Definition cinv_own (γ : gname) (p : frac) : iProp Σ := own γ p. Definition cinv (N : namespace) (γ : gname) (P : iProp Σ) : iProp Σ := inv N (P ∨ cinv_own γ 1%Qp)%I. End defs. Instance: Params (@cinv) 6. Typeclasses Opaque cinv_own cinv. Section proofs. Context `{irisG Λ Σ, cinvG Σ}. Global Instance cinv_own_timeless γ p : TimelessP (cinv_own γ p). Proof. rewrite /cinv_own; apply _. Qed. Global Instance cinv_ne N γ n : Proper (dist n ==> dist n) (cinv N γ). Proof. solve_proper. Qed. Global Instance cinv_proper N γ : Proper ((≡) ==> (≡)) (cinv N γ). Proof. apply (ne_proper _). Qed. Global Instance cinv_persistent N γ P : PersistentP (cinv N γ P). Proof. rewrite /cinv; apply _. Qed. Lemma cinv_own_op γ q1 q2 : cinv_own γ q1 ★ cinv_own γ q2 ⊣⊢ cinv_own γ (q1 + q2). Proof. by rewrite /cinv_own own_op. Qed. Lemma cinv_own_half γ q : cinv_own γ (q/2) ★ cinv_own γ (q/2) ⊣⊢ cinv_own γ q. Proof. by rewrite cinv_own_op Qp_div_2. Qed. Lemma cinv_own_valid γ q1 q2 : cinv_own γ q1 ★ cinv_own γ q2 ⊢ ✓ (q1 + q2)%Qp. `````` Robbert Krebbers committed Sep 20, 2016 42 `````` Proof. rewrite /cinv_own own_valid_2. by iIntros "% !%". Qed. `````` Robbert Krebbers committed Aug 25, 2016 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 `````` Lemma cinv_own_1_l γ q : cinv_own γ 1 ★ cinv_own γ q ⊢ False. Proof. rewrite cinv_own_valid. by iIntros (?%(exclusive_l 1%Qp)). Qed. Lemma cinv_alloc E N P : ▷ P ={E}=> ∃ γ, cinv N γ P ★ cinv_own γ 1. Proof. rewrite /cinv /cinv_own. iIntros "HP". iVs (own_alloc 1%Qp) as (γ) "H1"; first done. iVs (inv_alloc N _ (P ∨ own γ 1%Qp)%I with "[HP]"); eauto. Qed. Lemma cinv_cancel E N γ P : nclose N ⊆ E → cinv N γ P ⊢ cinv_own γ 1 ={E}=★ ▷ P. Proof. rewrite /cinv. iIntros (?) "#Hinv Hγ". iInv N as "[\$|>Hγ']" "Hclose"; first iApply "Hclose"; eauto. iDestruct (cinv_own_1_l with "[Hγ Hγ']") as %[]. by iFrame. Qed. Lemma cinv_open E N γ p P : nclose N ⊆ E → cinv N γ P ⊢ cinv_own γ p ={E,E∖N}=★ ▷ P ★ cinv_own γ p ★ (▷ P ={E∖N,E}=★ True). Proof. rewrite /cinv. iIntros (?) "#Hinv Hγ". iInv N as "[\$|>Hγ']" "Hclose". - iIntros "!==> {\$Hγ} HP". iApply "Hclose"; eauto. - iDestruct (cinv_own_1_l with "[Hγ Hγ']") as %[]. by iFrame. Qed. End proofs.``````