proofmode_iris.v 7.74 KB
 Ralf Jung committed May 29, 2018 1 ``````From iris.proofmode Require Import tactics monpred. `````` Joseph Tassarotti committed Feb 23, 2018 2 3 ``````From iris.base_logic Require Import base_logic. From iris.base_logic.lib Require Import invariants cancelable_invariants na_invariants. `````` Robbert Krebbers committed Oct 30, 2017 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 `````` Section base_logic_tests. Context {M : ucmraT}. Implicit Types P Q R : uPred M. Lemma test_random_stuff (P1 P2 P3 : nat → uPred M) : (∀ (x y : nat) a b, x ≡ y → □ (uPred_ownM (a ⋅ b) -∗ (∃ y1 y2 c, P1 ((x + y1) + y2) ∧ True ∧ □ uPred_ownM c) -∗ □ ▷ (∀ z, P2 z ∨ True → P2 z) -∗ ▷ (∀ n m : nat, P1 n → □ ((True ∧ P2 n) → □ (⌜n = n⌝ ↔ P3 n))) -∗ ▷ ⌜x = 0⌝ ∨ ∃ x z, ▷ P3 (x + z) ∗ uPred_ownM b ∗ uPred_ownM (core b)))%I. Proof. iIntros (i [|j] a b ?) "!# [Ha Hb] H1 #H2 H3"; setoid_subst. { iLeft. by iNext. } iRight. iDestruct "H1" as (z1 z2 c) "(H1&_&#Hc)". iPoseProof "Hc" as "foo". iRevert (a b) "Ha Hb". iIntros (b a) "Hb {foo} Ha". iAssert (uPred_ownM (a ⋅ core a)) with "[Ha]" as "[Ha #Hac]". { by rewrite cmra_core_r. } iIntros "{\$Hac \$Ha}". iExists (S j + z1), z2. iNext. iApply ("H3" \$! _ 0 with "[\$]"). - iSplit. done. iApply "H2". iLeft. iApply "H2". by iRight. - done. Qed. Lemma test_iFrame_pure (x y z : M) : ✓ x → ⌜y ≡ z⌝ -∗ (✓ x ∧ ✓ x ∧ y ≡ z : uPred M). Proof. iIntros (Hv) "Hxy". by iFrame (Hv) "Hxy". Qed. Lemma test_iAssert_modality P : (|==> False) -∗ |==> P. Proof. iIntros. iAssert False%I with "[> - //]" as %[]. Qed. `````` Jacques-Henri Jourdan committed Dec 22, 2017 40 41 42 43 44 45 46 47 48 `````` Lemma test_iStartProof_1 P : P -∗ P. Proof. iStartProof. iStartProof. iIntros "\$". Qed. Lemma test_iStartProof_2 P : P -∗ P. Proof. iStartProof (uPred _). iStartProof (uPredI _). iIntros "\$". Qed. Lemma test_iStartProof_3 P : P -∗ P. Proof. iStartProof (uPredI _). iStartProof (uPredSI _). iIntros "\$". Qed. Lemma test_iStartProof_4 P : P -∗ P. Proof. iStartProof (uPredSI _). iStartProof (uPred _). iIntros "\$". Qed. `````` Robbert Krebbers committed Oct 30, 2017 49 50 51 ``````End base_logic_tests. Section iris_tests. `````` Joseph Tassarotti committed Feb 23, 2018 52 `````` Context `{invG Σ, cinvG Σ, na_invG Σ}. `````` Ralf Jung committed May 29, 2018 53 `````` Implicit Types P Q R : iProp Σ. `````` Robbert Krebbers committed Oct 30, 2017 54 55 56 57 58 59 60 61 62 `````` Lemma test_masks N E P Q R : ↑N ⊆ E → (True -∗ P -∗ inv N Q -∗ True -∗ R) -∗ P -∗ ▷ Q ={E}=∗ R. Proof. iIntros (?) "H HP HQ". iApply ("H" with "[% //] [\$] [> HQ] [> //]"). by iApply inv_alloc. Qed. `````` Joseph Tassarotti committed Feb 23, 2018 63 `````` `````` Robbert Krebbers committed Mar 04, 2018 64 `````` Lemma test_iInv_0 N P: inv N ( P) ={⊤}=∗ ▷ P. `````` Joseph Tassarotti committed Feb 23, 2018 65 66 `````` Proof. iIntros "#H". `````` Ralf Jung committed May 17, 2018 67 `````` iInv N as "#H2". Show. `````` Ralf Jung committed Apr 25, 2018 68 `````` iModIntro. iSplit; auto. `````` Joseph Tassarotti committed Feb 23, 2018 69 70 `````` Qed. `````` Ralf Jung committed Apr 26, 2018 71 72 73 `````` Lemma test_iInv_0_with_close N P: inv N ( P) ={⊤}=∗ ▷ P. Proof. iIntros "#H". `````` Ralf Jung committed May 17, 2018 74 `````` iInv N as "#H2" "Hclose". Show. `````` Ralf Jung committed Apr 26, 2018 75 76 77 78 `````` iMod ("Hclose" with "H2"). iModIntro. by iNext. Qed. `````` Joseph Tassarotti committed Feb 23, 2018 79 80 `````` Lemma test_iInv_1 N E P: ↑N ⊆ E → `````` Robbert Krebbers committed Mar 04, 2018 81 `````` inv N ( P) ={E}=∗ ▷ P. `````` Joseph Tassarotti committed Feb 23, 2018 82 83 `````` Proof. iIntros (?) "#H". `````` Ralf Jung committed Apr 25, 2018 84 85 `````` iInv N as "#H2". iModIntro. iSplit; auto. `````` Joseph Tassarotti committed Feb 23, 2018 86 87 `````` Qed. `````` Joseph Tassarotti committed Feb 23, 2018 88 `````` Lemma test_iInv_2 γ p N P: `````` Robbert Krebbers committed Mar 04, 2018 89 `````` cinv N γ ( P) ∗ cinv_own γ p ={⊤}=∗ cinv_own γ p ∗ ▷ P. `````` Joseph Tassarotti committed Feb 23, 2018 90 91 `````` Proof. iIntros "(#?&?)". `````` Ralf Jung committed May 17, 2018 92 `````` iInv N as "(#HP&Hown)". Show. `````` Ralf Jung committed Apr 25, 2018 93 `````` iModIntro. iSplit; auto with iFrame. `````` Joseph Tassarotti committed Feb 23, 2018 94 95 `````` Qed. `````` Ralf Jung committed Apr 26, 2018 96 97 98 99 `````` Lemma test_iInv_2_with_close γ p N P: cinv N γ ( P) ∗ cinv_own γ p ={⊤}=∗ cinv_own γ p ∗ ▷ P. Proof. iIntros "(#?&?)". `````` Ralf Jung committed May 17, 2018 100 `````` iInv N as "(#HP&Hown)" "Hclose". Show. `````` Ralf Jung committed Apr 26, 2018 101 102 103 104 `````` iMod ("Hclose" with "HP"). iModIntro. iFrame. by iNext. Qed. `````` Joseph Tassarotti committed Feb 23, 2018 105 `````` Lemma test_iInv_3 γ p1 p2 N P: `````` Robbert Krebbers committed Mar 04, 2018 106 `````` cinv N γ ( P) ∗ cinv_own γ p1 ∗ cinv_own γ p2 `````` Joseph Tassarotti committed Feb 23, 2018 107 108 109 `````` ={⊤}=∗ cinv_own γ p1 ∗ cinv_own γ p2 ∗ ▷ P. Proof. iIntros "(#?&Hown1&Hown2)". `````` Ralf Jung committed Apr 25, 2018 110 111 `````` iInv N with "[Hown2 //]" as "(#HP&Hown2)". iModIntro. iSplit; auto with iFrame. `````` Joseph Tassarotti committed Feb 23, 2018 112 113 114 115 `````` Qed. Lemma test_iInv_4 t N E1 E2 P: ↑N ⊆ E2 → `````` Robbert Krebbers committed Mar 04, 2018 116 `````` na_inv t N ( P) ∗ na_own t E1 ∗ na_own t E2 `````` Joseph Tassarotti committed Feb 23, 2018 117 118 119 `````` ⊢ |={⊤}=> na_own t E1 ∗ na_own t E2 ∗ ▷ P. Proof. iIntros (?) "(#?&Hown1&Hown2)". `````` Ralf Jung committed May 17, 2018 120 `````` iInv N as "(#HP&Hown2)". Show. `````` Ralf Jung committed Apr 25, 2018 121 `````` iModIntro. iSplitL "Hown2"; auto with iFrame. `````` Joseph Tassarotti committed Feb 23, 2018 122 123 `````` Qed. `````` Ralf Jung committed Apr 26, 2018 124 125 126 127 128 129 `````` Lemma test_iInv_4_with_close t N E1 E2 P: ↑N ⊆ E2 → na_inv t N ( P) ∗ na_own t E1 ∗ na_own t E2 ⊢ |={⊤}=> na_own t E1 ∗ na_own t E2 ∗ ▷ P. Proof. iIntros (?) "(#?&Hown1&Hown2)". `````` Ralf Jung committed May 17, 2018 130 `````` iInv N as "(#HP&Hown2)" "Hclose". Show. `````` Ralf Jung committed Apr 26, 2018 131 132 133 134 135 `````` iMod ("Hclose" with "[HP Hown2]"). { iFrame. done. } iModIntro. iFrame. by iNext. Qed. `````` Joseph Tassarotti committed Feb 23, 2018 136 137 138 `````` (* test named selection of which na_own to use *) Lemma test_iInv_5 t N E1 E2 P: ↑N ⊆ E2 → `````` Robbert Krebbers committed Mar 04, 2018 139 `````` na_inv t N ( P) ∗ na_own t E1 ∗ na_own t E2 `````` Joseph Tassarotti committed Feb 23, 2018 140 141 142 `````` ={⊤}=∗ na_own t E1 ∗ na_own t E2 ∗ ▷ P. Proof. iIntros (?) "(#?&Hown1&Hown2)". `````` Ralf Jung committed Apr 25, 2018 143 144 `````` iInv N with "Hown2" as "(#HP&Hown2)". iModIntro. iSplitL "Hown2"; auto with iFrame. `````` Joseph Tassarotti committed Feb 23, 2018 145 146 147 148 `````` Qed. Lemma test_iInv_6 t N E1 E2 P: ↑N ⊆ E1 → `````` Robbert Krebbers committed Mar 04, 2018 149 `````` na_inv t N ( P) ∗ na_own t E1 ∗ na_own t E2 `````` Joseph Tassarotti committed Feb 23, 2018 150 151 152 `````` ={⊤}=∗ na_own t E1 ∗ na_own t E2 ∗ ▷ P. Proof. iIntros (?) "(#?&Hown1&Hown2)". `````` Ralf Jung committed Apr 25, 2018 153 154 `````` iInv N with "Hown1" as "(#HP&Hown1)". iModIntro. iSplitL "Hown1"; auto with iFrame. `````` Joseph Tassarotti committed Feb 23, 2018 155 156 157 158 159 `````` Qed. (* test robustness in presence of other invariants *) Lemma test_iInv_7 t N1 N2 N3 E1 E2 P: ↑N3 ⊆ E1 → `````` Robbert Krebbers committed Mar 04, 2018 160 `````` inv N1 P ∗ na_inv t N3 ( P) ∗ inv N2 P ∗ na_own t E1 ∗ na_own t E2 `````` Joseph Tassarotti committed Feb 23, 2018 161 162 163 `````` ={⊤}=∗ na_own t E1 ∗ na_own t E2 ∗ ▷ P. Proof. iIntros (?) "(#?&#?&#?&Hown1&Hown2)". `````` Ralf Jung committed Apr 25, 2018 164 165 `````` iInv N3 with "Hown1" as "(#HP&Hown1)". iModIntro. iSplitL "Hown1"; auto with iFrame. `````` Joseph Tassarotti committed Feb 23, 2018 166 167 168 169 170 171 `````` Qed. (* iInv should work even where we have "inv N P" in which P contains an evar *) Lemma test_iInv_8 N : ∃ P, inv N P ={⊤}=∗ P ≡ True ∧ inv N P. Proof. eexists. iIntros "#H". `````` Ralf Jung committed Apr 25, 2018 172 `````` iInv N as "HP". iFrame "HP". auto. `````` Joseph Tassarotti committed Feb 23, 2018 173 `````` Qed. `````` Joseph Tassarotti committed Feb 23, 2018 174 175 176 177 `````` (* test selection by hypothesis name instead of namespace *) Lemma test_iInv_9 t N1 N2 N3 E1 E2 P: ↑N3 ⊆ E1 → `````` Robbert Krebbers committed Mar 04, 2018 178 `````` inv N1 P ∗ na_inv t N3 ( P) ∗ inv N2 P ∗ na_own t E1 ∗ na_own t E2 `````` Joseph Tassarotti committed Feb 23, 2018 179 180 181 `````` ={⊤}=∗ na_own t E1 ∗ na_own t E2 ∗ ▷ P. Proof. iIntros (?) "(#?&#HInv&#?&Hown1&Hown2)". `````` Ralf Jung committed Apr 25, 2018 182 183 `````` iInv "HInv" with "Hown1" as "(#HP&Hown1)". iModIntro. iSplitL "Hown1"; auto with iFrame. `````` Joseph Tassarotti committed Feb 23, 2018 184 185 186 187 188 `````` Qed. (* test selection by hypothesis name instead of namespace *) Lemma test_iInv_10 t N1 N2 N3 E1 E2 P: ↑N3 ⊆ E1 → `````` Robbert Krebbers committed Mar 04, 2018 189 `````` inv N1 P ∗ na_inv t N3 ( P) ∗ inv N2 P ∗ na_own t E1 ∗ na_own t E2 `````` Joseph Tassarotti committed Feb 23, 2018 190 191 192 `````` ={⊤}=∗ na_own t E1 ∗ na_own t E2 ∗ ▷ P. Proof. iIntros (?) "(#?&#HInv&#?&Hown1&Hown2)". `````` Ralf Jung committed Apr 25, 2018 193 194 `````` iInv "HInv" as "(#HP&Hown1)". iModIntro. iSplitL "Hown1"; auto with iFrame. `````` Joseph Tassarotti committed Feb 23, 2018 195 196 197 `````` Qed. (* test selection by ident name *) `````` Robbert Krebbers committed Mar 04, 2018 198 `````` Lemma test_iInv_11 N P: inv N ( P) ={⊤}=∗ ▷ P. `````` Joseph Tassarotti committed Feb 23, 2018 199 200 `````` Proof. let H := iFresh in `````` Ralf Jung committed Apr 25, 2018 201 `````` (iIntros H; iInv H as "#H2"). auto. `````` Joseph Tassarotti committed Feb 23, 2018 202 203 204 `````` Qed. (* error messages *) `````` Robbert Krebbers committed Mar 04, 2018 205 `````` Lemma test_iInv_12 N P: inv N ( P) ={⊤}=∗ True. `````` Joseph Tassarotti committed Feb 23, 2018 206 207 `````` Proof. iIntros "H". `````` Ralf Jung committed Apr 25, 2018 208 209 210 `````` Fail iInv 34 as "#H2". Fail iInv nroot as "#H2". Fail iInv "H2" as "#H2". `````` Joseph Tassarotti committed Feb 23, 2018 211 212 `````` done. Qed. `````` Joseph Tassarotti committed Feb 23, 2018 213 214 215 216 217 `````` (* test destruction of existentials when opening an invariant *) Lemma test_iInv_13 N: inv N (∃ (v1 v2 v3 : nat), emp ∗ emp ∗ emp) ={⊤}=∗ ▷ emp. Proof. `````` Ralf Jung committed Apr 25, 2018 218 219 `````` iIntros "H"; iInv "H" as (v1 v2 v3) "(?&?&_)". eauto. `````` Joseph Tassarotti committed Feb 23, 2018 220 `````` Qed. `````` Robbert Krebbers committed Oct 30, 2017 221 ``````End iris_tests. `````` Ralf Jung committed May 29, 2018 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 `````` Section monpred_tests. Context `{invG Σ}. Context {I : biIndex}. Local Notation monPred := (monPred I (iPropI Σ)). Local Notation monPredI := (monPredI I (iPropI Σ)). Local Notation monPredSI := (monPredSI I (iPropSI Σ)). Implicit Types P Q R : monPred. Implicit Types 𝓟 𝓠 𝓡 : iProp Σ. Lemma test_iInv N E 𝓟 : ↑N ⊆ E → ⎡inv N 𝓟⎤ ⊢@{monPredI} |={E}=> emp. Proof. iIntros (?) "Hinv". iInv N as "HP". Show. iFrame "HP". auto. Qed. Lemma test_iInv_with_close N E 𝓟 : ↑N ⊆ E → ⎡inv N 𝓟⎤ ⊢@{monPredI} |={E}=> emp. Proof. iIntros (?) "Hinv". iInv N as "HP" "Hclose". Show. iMod ("Hclose" with "HP"). auto. Qed. End monpred_tests.``````