cancelable_invariants.v 2.45 KB
 1 ``````From iris.base_logic.lib Require Export invariants. `````` Robbert Krebbers committed Aug 25, 2016 2 ``````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 ``````Import uPred. Class cinvG Σ := cinv_inG :> inG Σ fracR. Section defs. `````` Robbert Krebbers committed Oct 28, 2016 9 `````` Context `{invG Σ, cinvG Σ}. `````` Robbert Krebbers committed Aug 25, 2016 10 11 12 13 14 15 16 `````` 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. `````` Robbert Krebbers committed Oct 28, 2016 17 ``````Instance: Params (@cinv) 5. `````` Robbert Krebbers committed Aug 25, 2016 18 19 20 ``````Typeclasses Opaque cinv_own cinv. Section proofs. `````` Robbert Krebbers committed Oct 28, 2016 21 `````` Context `{invG Σ, cinvG Σ}. `````` Robbert Krebbers committed Aug 25, 2016 22 23 24 25 26 27 28 29 30 31 32 33 34 `````` 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 : `````` Robbert Krebbers committed Nov 03, 2016 35 `````` cinv_own γ q1 ∗ cinv_own γ q2 ⊣⊢ cinv_own γ (q1 + q2). `````` Robbert Krebbers committed Aug 25, 2016 36 37 `````` Proof. by rewrite /cinv_own own_op. Qed. `````` Robbert Krebbers committed Nov 03, 2016 38 `````` Lemma cinv_own_half γ q : cinv_own γ (q/2) ∗ cinv_own γ (q/2) ⊣⊢ cinv_own γ q. `````` Robbert Krebbers committed Aug 25, 2016 39 40 `````` Proof. by rewrite cinv_own_op Qp_div_2. Qed. `````` Robbert Krebbers committed Nov 03, 2016 41 `````` Lemma cinv_own_valid γ q1 q2 : cinv_own γ q1 ∗ cinv_own γ q2 ⊢ ✓ (q1 + q2)%Qp. `````` Robbert Krebbers committed Nov 18, 2016 42 `````` Proof. rewrite /cinv_own -own_op own_valid. by iIntros "% !%". Qed. `````` Robbert Krebbers committed Aug 25, 2016 43 `````` `````` Robbert Krebbers committed Nov 03, 2016 44 `````` Lemma cinv_own_1_l γ q : cinv_own γ 1 ∗ cinv_own γ q ⊢ False. `````` Robbert Krebbers committed Aug 25, 2016 45 46 `````` Proof. rewrite cinv_own_valid. by iIntros (?%(exclusive_l 1%Qp)). Qed. `````` Robbert Krebbers committed Nov 03, 2016 47 `````` Lemma cinv_alloc E N P : ▷ P ={E}=∗ ∃ γ, cinv N γ P ∗ cinv_own γ 1. `````` Robbert Krebbers committed Aug 25, 2016 48 49 `````` Proof. rewrite /cinv /cinv_own. iIntros "HP". `````` Robbert Krebbers committed Oct 25, 2016 50 51 `````` iMod (own_alloc 1%Qp) as (γ) "H1"; first done. iMod (inv_alloc N _ (P ∨ own γ 1%Qp)%I with "[HP]"); eauto. `````` Robbert Krebbers committed Aug 25, 2016 52 53 `````` Qed. `````` Robbert Krebbers committed Nov 22, 2016 54 `````` Lemma cinv_cancel E N γ P : ↑N ⊆ E → cinv N γ P ⊢ cinv_own γ 1 ={E}=∗ ▷ P. `````` Robbert Krebbers committed Aug 25, 2016 55 56 57 58 59 60 61 `````` 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 : `````` Robbert Krebbers committed Nov 22, 2016 62 63 `````` ↑N ⊆ E → cinv N γ P ⊢ cinv_own γ p ={E,E∖↑N}=∗ ▷ P ∗ cinv_own γ p ∗ (▷ P ={E∖↑N,E}=∗ True). `````` Robbert Krebbers committed Aug 25, 2016 64 65 66 `````` Proof. rewrite /cinv. iIntros (?) "#Hinv Hγ". iInv N as "[\$|>Hγ']" "Hclose". `````` Robbert Krebbers committed Oct 25, 2016 67 `````` - iIntros "!> {\$Hγ} HP". iApply "Hclose"; eauto. `````` Robbert Krebbers committed Aug 25, 2016 68 69 70 `````` - iDestruct (cinv_own_1_l with "[Hγ Hγ']") as %[]. by iFrame. Qed. End proofs.``````