proofmode_iris.v 7.83 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. `````` Pierre-Marie Pédrot committed Feb 05, 2019 4 ``````Set Ltac Backtrace. `````` Robbert Krebbers committed Oct 30, 2017 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 `````` 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 41 42 43 44 45 46 47 48 49 `````` 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 50 51 52 ``````End base_logic_tests. Section iris_tests. `````` Joseph Tassarotti committed Feb 23, 2018 53 `````` Context `{invG Σ, cinvG Σ, na_invG Σ}. `````` Ralf Jung committed May 29, 2018 54 `````` Implicit Types P Q R : iProp Σ. `````` Robbert Krebbers committed Oct 30, 2017 55 56 57 58 59 60 61 62 63 `````` 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 64 `````` `````` Robbert Krebbers committed Mar 04, 2018 65 `````` Lemma test_iInv_0 N P: inv N ( P) ={⊤}=∗ ▷ P. `````` Joseph Tassarotti committed Feb 23, 2018 66 67 `````` Proof. iIntros "#H". `````` Ralf Jung committed May 17, 2018 68 `````` iInv N as "#H2". Show. `````` Ralf Jung committed Apr 25, 2018 69 `````` iModIntro. iSplit; auto. `````` Joseph Tassarotti committed Feb 23, 2018 70 71 `````` Qed. `````` Ralf Jung committed Apr 26, 2018 72 73 74 `````` Lemma test_iInv_0_with_close N P: inv N ( P) ={⊤}=∗ ▷ P. Proof. iIntros "#H". `````` Ralf Jung committed May 17, 2018 75 `````` iInv N as "#H2" "Hclose". Show. `````` Ralf Jung committed Apr 26, 2018 76 77 78 79 `````` iMod ("Hclose" with "H2"). iModIntro. by iNext. Qed. `````` Joseph Tassarotti committed Feb 23, 2018 80 81 `````` Lemma test_iInv_1 N E P: ↑N ⊆ E → `````` Robbert Krebbers committed Mar 04, 2018 82 `````` inv N ( P) ={E}=∗ ▷ P. `````` Joseph Tassarotti committed Feb 23, 2018 83 84 `````` Proof. iIntros (?) "#H". `````` Ralf Jung committed Apr 25, 2018 85 86 `````` iInv N as "#H2". iModIntro. iSplit; auto. `````` Joseph Tassarotti committed Feb 23, 2018 87 88 `````` Qed. `````` Joseph Tassarotti committed Feb 23, 2018 89 `````` Lemma test_iInv_2 γ p N P: `````` Robbert Krebbers committed Mar 04, 2018 90 `````` cinv N γ ( P) ∗ cinv_own γ p ={⊤}=∗ cinv_own γ p ∗ ▷ P. `````` Joseph Tassarotti committed Feb 23, 2018 91 92 `````` Proof. iIntros "(#?&?)". `````` Ralf Jung committed May 17, 2018 93 `````` iInv N as "(#HP&Hown)". Show. `````` Ralf Jung committed Apr 25, 2018 94 `````` iModIntro. iSplit; auto with iFrame. `````` Joseph Tassarotti committed Feb 23, 2018 95 96 `````` Qed. `````` Ralf Jung committed Apr 26, 2018 97 98 99 100 `````` 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 101 `````` iInv N as "(#HP&Hown)" "Hclose". Show. `````` Ralf Jung committed Apr 26, 2018 102 103 104 105 `````` iMod ("Hclose" with "HP"). iModIntro. iFrame. by iNext. Qed. `````` Joseph Tassarotti committed Feb 23, 2018 106 `````` Lemma test_iInv_3 γ p1 p2 N P: `````` Robbert Krebbers committed Mar 04, 2018 107 `````` cinv N γ ( P) ∗ cinv_own γ p1 ∗ cinv_own γ p2 `````` Joseph Tassarotti committed Feb 23, 2018 108 109 110 `````` ={⊤}=∗ cinv_own γ p1 ∗ cinv_own γ p2 ∗ ▷ P. Proof. iIntros "(#?&Hown1&Hown2)". `````` Ralf Jung committed Apr 25, 2018 111 112 `````` iInv N with "[Hown2 //]" as "(#HP&Hown2)". iModIntro. iSplit; auto with iFrame. `````` Joseph Tassarotti committed Feb 23, 2018 113 114 115 116 `````` Qed. Lemma test_iInv_4 t N E1 E2 P: ↑N ⊆ E2 → `````` Robbert Krebbers committed Mar 04, 2018 117 `````` na_inv t N ( P) ∗ na_own t E1 ∗ na_own t E2 `````` Joseph Tassarotti committed Feb 23, 2018 118 119 120 `````` ⊢ |={⊤}=> na_own t E1 ∗ na_own t E2 ∗ ▷ P. Proof. iIntros (?) "(#?&Hown1&Hown2)". `````` Ralf Jung committed May 17, 2018 121 `````` iInv N as "(#HP&Hown2)". Show. `````` Ralf Jung committed Apr 25, 2018 122 `````` iModIntro. iSplitL "Hown2"; auto with iFrame. `````` Joseph Tassarotti committed Feb 23, 2018 123 124 `````` Qed. `````` Ralf Jung committed Apr 26, 2018 125 126 127 128 129 130 `````` 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 131 `````` iInv N as "(#HP&Hown2)" "Hclose". Show. `````` Ralf Jung committed Apr 26, 2018 132 133 134 135 136 `````` iMod ("Hclose" with "[HP Hown2]"). { iFrame. done. } iModIntro. iFrame. by iNext. Qed. `````` Joseph Tassarotti committed Feb 23, 2018 137 138 139 `````` (* 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 140 `````` na_inv t N ( P) ∗ na_own t E1 ∗ na_own t E2 `````` Joseph Tassarotti committed Feb 23, 2018 141 142 143 `````` ={⊤}=∗ na_own t E1 ∗ na_own t E2 ∗ ▷ P. Proof. iIntros (?) "(#?&Hown1&Hown2)". `````` Ralf Jung committed Apr 25, 2018 144 145 `````` iInv N with "Hown2" as "(#HP&Hown2)". iModIntro. iSplitL "Hown2"; auto with iFrame. `````` Joseph Tassarotti committed Feb 23, 2018 146 147 148 149 `````` Qed. Lemma test_iInv_6 t N E1 E2 P: ↑N ⊆ E1 → `````` Robbert Krebbers committed Mar 04, 2018 150 `````` na_inv t N ( P) ∗ na_own t E1 ∗ na_own t E2 `````` Joseph Tassarotti committed Feb 23, 2018 151 152 153 `````` ={⊤}=∗ na_own t E1 ∗ na_own t E2 ∗ ▷ P. Proof. iIntros (?) "(#?&Hown1&Hown2)". `````` Ralf Jung committed Apr 25, 2018 154 155 `````` iInv N with "Hown1" as "(#HP&Hown1)". iModIntro. iSplitL "Hown1"; auto with iFrame. `````` Joseph Tassarotti committed Feb 23, 2018 156 157 158 159 160 `````` 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 161 `````` 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 162 163 164 `````` ={⊤}=∗ na_own t E1 ∗ na_own t E2 ∗ ▷ P. Proof. iIntros (?) "(#?&#?&#?&Hown1&Hown2)". `````` Ralf Jung committed Apr 25, 2018 165 166 `````` iInv N3 with "Hown1" as "(#HP&Hown1)". iModIntro. iSplitL "Hown1"; auto with iFrame. `````` Joseph Tassarotti committed Feb 23, 2018 167 168 169 170 171 172 `````` 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 173 `````` iInv N as "HP". iFrame "HP". auto. `````` Joseph Tassarotti committed Feb 23, 2018 174 `````` Qed. `````` Joseph Tassarotti committed Feb 23, 2018 175 176 177 178 `````` (* 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 179 `````` 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 180 181 182 `````` ={⊤}=∗ na_own t E1 ∗ na_own t E2 ∗ ▷ P. Proof. iIntros (?) "(#?&#HInv&#?&Hown1&Hown2)". `````` Ralf Jung committed Apr 25, 2018 183 184 `````` iInv "HInv" with "Hown1" as "(#HP&Hown1)". iModIntro. iSplitL "Hown1"; auto with iFrame. `````` Joseph Tassarotti committed Feb 23, 2018 185 186 187 188 189 `````` 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 190 `````` 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 191 192 193 `````` ={⊤}=∗ na_own t E1 ∗ na_own t E2 ∗ ▷ P. Proof. iIntros (?) "(#?&#HInv&#?&Hown1&Hown2)". `````` Ralf Jung committed Apr 25, 2018 194 195 `````` iInv "HInv" as "(#HP&Hown1)". iModIntro. iSplitL "Hown1"; auto with iFrame. `````` Joseph Tassarotti committed Feb 23, 2018 196 197 198 `````` Qed. (* test selection by ident name *) `````` Robbert Krebbers committed Mar 04, 2018 199 `````` Lemma test_iInv_11 N P: inv N ( P) ={⊤}=∗ ▷ P. `````` Joseph Tassarotti committed Feb 23, 2018 200 201 `````` Proof. let H := iFresh in `````` Ralf Jung committed Apr 25, 2018 202 `````` (iIntros H; iInv H as "#H2"). auto. `````` Joseph Tassarotti committed Feb 23, 2018 203 204 205 `````` Qed. (* error messages *) `````` Ralf Jung committed Oct 04, 2018 206 `````` Check "test_iInv_12". `````` Robbert Krebbers committed Mar 04, 2018 207 `````` Lemma test_iInv_12 N P: inv N ( P) ={⊤}=∗ True. `````` Joseph Tassarotti committed Feb 23, 2018 208 209 `````` Proof. iIntros "H". `````` Ralf Jung committed Apr 25, 2018 210 211 212 `````` Fail iInv 34 as "#H2". Fail iInv nroot as "#H2". Fail iInv "H2" as "#H2". `````` Joseph Tassarotti committed Feb 23, 2018 213 214 `````` done. Qed. `````` Joseph Tassarotti committed Feb 23, 2018 215 216 217 218 219 `````` (* 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 220 221 `````` iIntros "H"; iInv "H" as (v1 v2 v3) "(?&?&_)". eauto. `````` Joseph Tassarotti committed Feb 23, 2018 222 `````` Qed. `````` Robbert Krebbers committed Oct 30, 2017 223 ``````End iris_tests. `````` Ralf Jung committed May 29, 2018 224 225 226 227 228 229 230 231 232 233 `````` 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 Σ. `````` Ralf Jung committed Oct 04, 2018 234 `````` Check "test_iInv". `````` Ralf Jung committed May 29, 2018 235 236 237 238 239 240 241 242 243 `````` Lemma test_iInv N E 𝓟 : ↑N ⊆ E → ⎡inv N 𝓟⎤ ⊢@{monPredI} |={E}=> emp. Proof. iIntros (?) "Hinv". iInv N as "HP". Show. iFrame "HP". auto. Qed. `````` Ralf Jung committed Oct 04, 2018 244 `````` Check "test_iInv_with_close". `````` Ralf Jung committed May 29, 2018 245 246 247 248 249 250 251 252 253 254 `````` 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.``````