cancelable_invariants.v 4.76 KB
 Robbert Krebbers committed Oct 30, 2017 1 ``````From iris.base_logic.lib Require Export invariants. `````` Ralf Jung committed Feb 15, 2018 2 ``````From iris.bi.lib Require Import fractional. `````` Robbert Krebbers committed Aug 25, 2016 3 ``````From iris.algebra Require Export frac. `````` Robbert Krebbers committed Oct 05, 2016 4 ``````From iris.proofmode Require Import tactics. `````` Ralf Jung committed Jan 05, 2017 5 ``````Set Default Proof Using "Type". `````` Robbert Krebbers committed Aug 25, 2016 6 7 8 ``````Import uPred. Class cinvG Σ := cinv_inG :> inG Σ fracR. `````` Ralf Jung committed Apr 07, 2017 9 10 11 12 ``````Definition cinvΣ : gFunctors := #[GFunctor fracR]. Instance subG_cinvΣ {Σ} : subG cinvΣ Σ → cinvG Σ. Proof. solve_inG. Qed. `````` Robbert Krebbers committed Aug 25, 2016 13 14 `````` Section defs. `````` Ralf Jung committed Mar 05, 2019 15 `````` Context `{!invG Σ, !cinvG Σ}. `````` Robbert Krebbers committed Aug 25, 2016 16 17 18 19 `````` Definition cinv_own (γ : gname) (p : frac) : iProp Σ := own γ p. Definition cinv (N : namespace) (γ : gname) (P : iProp Σ) : iProp Σ := `````` Ralf Jung committed Apr 11, 2017 20 `````` (∃ P', □ ▷ (P ↔ P') ∗ inv N (P' ∨ cinv_own γ 1%Qp))%I. `````` Robbert Krebbers committed Aug 25, 2016 21 22 ``````End defs. `````` Maxime Dénès committed Jan 24, 2019 23 ``````Instance: Params (@cinv) 5 := {}. `````` Robbert Krebbers committed Aug 25, 2016 24 25 `````` Section proofs. `````` Ralf Jung committed Mar 05, 2019 26 `````` Context `{!invG Σ, !cinvG Σ}. `````` Robbert Krebbers committed Aug 25, 2016 27 `````` `````` Robbert Krebbers committed Oct 25, 2017 28 `````` Global Instance cinv_own_timeless γ p : Timeless (cinv_own γ p). `````` Robbert Krebbers committed Aug 25, 2016 29 30 `````` Proof. rewrite /cinv_own; apply _. Qed. `````` Ralf Jung committed Apr 11, 2017 31 32 `````` Global Instance cinv_contractive N γ : Contractive (cinv N γ). Proof. solve_contractive. Qed. `````` Ralf Jung committed Jan 27, 2017 33 `````` Global Instance cinv_ne N γ : NonExpansive (cinv N γ). `````` Ralf Jung committed Apr 11, 2017 34 `````` Proof. exact: contractive_ne. Qed. `````` Robbert Krebbers committed Aug 25, 2016 35 `````` Global Instance cinv_proper N γ : Proper ((≡) ==> (≡)) (cinv N γ). `````` Ralf Jung committed Apr 11, 2017 36 `````` Proof. exact: ne_proper. Qed. `````` Robbert Krebbers committed Aug 25, 2016 37 `````` `````` Robbert Krebbers committed Oct 25, 2017 38 `````` Global Instance cinv_persistent N γ P : Persistent (cinv N γ P). `````` Robbert Krebbers committed Aug 25, 2016 39 40 `````` Proof. rewrite /cinv; apply _. Qed. `````` Robbert Krebbers committed Mar 28, 2018 41 `````` Global Instance cinv_own_fractional γ : Fractional (cinv_own γ). `````` Robbert Krebbers committed Oct 30, 2017 42 `````` Proof. intros ??. by rewrite /cinv_own -own_op. Qed. `````` Robbert Krebbers committed Mar 28, 2018 43 `````` Global Instance cinv_own_as_fractional γ q : `````` Jacques-Henri Jourdan committed Nov 23, 2016 44 `````` AsFractional (cinv_own γ q) (cinv_own γ) q. `````` Jacques-Henri Jourdan committed Dec 13, 2016 45 `````` Proof. split. done. apply _. Qed. `````` Robbert Krebbers committed Aug 25, 2016 46 `````` `````` Robbert Krebbers committed Dec 09, 2016 47 48 `````` Lemma cinv_own_valid γ q1 q2 : cinv_own γ q1 -∗ cinv_own γ q2 -∗ ✓ (q1 + q2)%Qp. Proof. apply (own_valid_2 γ q1 q2). Qed. `````` Robbert Krebbers committed Aug 25, 2016 49 `````` `````` Robbert Krebbers committed Dec 09, 2016 50 51 52 53 54 `````` Lemma cinv_own_1_l γ q : cinv_own γ 1 -∗ cinv_own γ q -∗ False. Proof. iIntros "H1 H2". iDestruct (cinv_own_valid with "H1 H2") as %[]%(exclusive_l 1%Qp). Qed. `````` Robbert Krebbers committed Aug 25, 2016 55 `````` `````` Ralf Jung committed Apr 11, 2017 56 57 58 59 `````` Lemma cinv_iff N γ P P' : ▷ □ (P ↔ P') -∗ cinv N γ P -∗ cinv N γ P'. Proof. iIntros "#HP' Hinv". iDestruct "Hinv" as (P'') "[#HP'' Hinv]". `````` Robbert Krebbers committed Mar 03, 2018 60 `````` iExists _. iFrame "Hinv". iAlways. iNext. iSplit. `````` Ralf Jung committed Apr 11, 2017 61 62 63 64 `````` - iIntros "?". iApply "HP''". iApply "HP'". done. - iIntros "?". iApply "HP'". iApply "HP''". done. Qed. `````` Dan Frumin committed Mar 06, 2019 65 66 67 `````` Lemma cinv_alloc_strong (I : gname → Prop) E N : pred_infinite I → (|={E}=> ∃ γ, ⌜ I γ ⌝ ∧ cinv_own γ 1 ∗ ∀ P, ▷ P ={E}=∗ cinv N γ P)%I. `````` Robbert Krebbers committed Aug 25, 2016 68 `````` Proof. `````` Dan Frumin committed Mar 06, 2019 69 `````` iIntros (?). iMod (own_alloc_strong 1%Qp I) as (γ) "[Hfresh Hγ]"; [done|done|]. `````` Robbert Krebbers committed May 23, 2018 70 `````` iExists γ; iIntros "!> {\$Hγ \$Hfresh}" (P) "HP". `````` Ralf Jung committed Apr 11, 2017 71 `````` iMod (inv_alloc N _ (P ∨ own γ 1%Qp)%I with "[HP]"); first by eauto. `````` Robbert Krebbers committed May 23, 2018 72 73 74 `````` iIntros "!>". iExists P. iSplit; last done. iIntros "!# !>"; iSplit; auto. Qed. `````` Dan Frumin committed Mar 06, 2019 75 76 77 78 79 80 81 `````` Lemma cinv_alloc_cofinite (G : gset gname) E N : (|={E}=> ∃ γ, ⌜ γ ∉ G ⌝ ∧ cinv_own γ 1 ∗ ∀ P, ▷ P ={E}=∗ cinv N γ P)%I. Proof. apply cinv_alloc_strong. apply (pred_infinite_set (C:=gset gname))=> E'. exists (fresh (G ∪ E')). apply not_elem_of_union, is_fresh. Qed. `````` Robbert Krebbers committed May 23, 2018 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 `````` 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. `````` Robbert Krebbers committed May 23, 2018 97 98 `````` Lemma cinv_alloc E N P : ▷ P ={E}=∗ ∃ γ, cinv N γ P ∗ cinv_own γ 1. Proof. `````` Dan Frumin committed Mar 06, 2019 99 `````` iIntros "HP". iMod (cinv_alloc_cofinite ∅ E N) as (γ _) "[Hγ Halloc]". `````` Robbert Krebbers committed May 23, 2018 100 `````` iExists γ. iFrame "Hγ". by iApply "Halloc". `````` Robbert Krebbers committed Aug 25, 2016 101 102 `````` Qed. `````` 103 `````` Lemma cinv_cancel E N γ P : ↑N ⊆ E → cinv N γ P -∗ cinv_own γ 1 ={E}=∗ ▷ P. `````` Robbert Krebbers committed Aug 25, 2016 104 `````` Proof. `````` Robbert Krebbers committed May 23, 2018 105 106 107 `````` iIntros (?) "#Hinv Hγ". iMod (cinv_open_strong with "Hinv Hγ") as "(\$ & Hγ & H)"; first done. iApply "H". by iRight. `````` Robbert Krebbers committed Aug 25, 2016 108 109 110 `````` Qed. Lemma cinv_open E N γ p P : `````` Robbert Krebbers committed Nov 22, 2016 111 `````` ↑N ⊆ E → `````` 112 `````` cinv N γ P -∗ cinv_own γ p ={E,E∖↑N}=∗ ▷ P ∗ cinv_own γ p ∗ (▷ P ={E∖↑N,E}=∗ True). `````` Robbert Krebbers committed Aug 25, 2016 113 `````` Proof. `````` Robbert Krebbers committed May 23, 2018 114 115 116 `````` iIntros (?) "#Hinv Hγ". iMod (cinv_open_strong with "Hinv Hγ") as "(\$ & \$ & H)"; first done. iIntros "!> HP". iApply "H"; auto. `````` Robbert Krebbers committed Aug 25, 2016 117 `````` Qed. `````` Joseph Tassarotti committed Feb 23, 2018 118 `````` `````` Maxime Dénès committed Jan 24, 2019 119 `````` Global Instance into_inv_cinv N γ P : IntoInv (cinv N γ P) N := {}. `````` Ralf Jung committed Apr 25, 2018 120 `````` `````` Ralf Jung committed May 02, 2018 121 `````` Global Instance into_acc_cinv E N γ P p : `````` Ralf Jung committed Apr 26, 2018 122 `````` IntoAcc (X:=unit) (cinv N γ P) `````` 123 `````` (↑N ⊆ E) (cinv_own γ p) (fupd E (E∖↑N)) (fupd (E∖↑N) E) `````` Ralf Jung committed Apr 26, 2018 124 `````` (λ _, ▷ P ∗ cinv_own γ p)%I (λ _, ▷ P)%I (λ _, None)%I. `````` Joseph Tassarotti committed Feb 23, 2018 125 `````` Proof. `````` Ralf Jung committed Apr 26, 2018 126 127 `````` rewrite /IntoAcc /accessor. iIntros (?) "#Hinv Hown". rewrite exist_unit -assoc. `````` Ralf Jung committed Apr 25, 2018 128 `````` iApply (cinv_open with "Hinv"); done. `````` Joseph Tassarotti committed Feb 23, 2018 129 `````` Qed. `````` Robbert Krebbers committed Aug 25, 2016 130 ``````End proofs. `````` Ralf Jung committed Apr 11, 2017 131 132 `````` Typeclasses Opaque cinv_own cinv.``````