proofmode.v 24.3 KB
Newer Older
 Joseph Tassarotti committed Mar 12, 2018 1 ``````From iris.proofmode Require Import tactics intro_patterns. `````` Ralf Jung committed Jan 05, 2017 2 ``````Set Default Proof Using "Type". `````` Robbert Krebbers committed Apr 11, 2016 3 `````` `````` Ralf Jung committed Apr 11, 2017 4 ``````Section tests. `````` Robbert Krebbers committed Oct 30, 2017 5 6 ``````Context {PROP : sbi}. Implicit Types P Q R : PROP. `````` Robbert Krebbers committed Apr 13, 2017 7 `````` `````` Ralf Jung committed Jul 04, 2018 8 ``````Check "demo_0". `````` Jacques-Henri Jourdan committed Nov 02, 2017 9 ``````Lemma demo_0 P Q : □ (P ∨ Q) -∗ (∀ x, ⌜x = 0⌝ ∨ ⌜x = 1⌝) → (Q ∨ P). `````` Robbert Krebbers committed May 02, 2016 10 ``````Proof. `````` Ralf Jung committed May 17, 2018 11 `````` iIntros "H #H2". Show. iDestruct "H" as "###H". `````` Robbert Krebbers committed May 02, 2016 12 `````` (* should remove the disjunction "H" *) `````` Ralf Jung committed May 17, 2018 13 `````` iDestruct "H" as "[#?|#?]"; last by iLeft. Show. `````` Robbert Krebbers committed May 02, 2016 14 15 16 17 `````` (* should keep the disjunction "H" because it is instantiated *) iDestruct ("H2" \$! 10) as "[%|%]". done. done. Qed. `````` Robbert Krebbers committed Oct 30, 2017 18 19 ``````Lemma demo_2 P1 P2 P3 P4 Q (P5 : nat → PROP) `{!Affine P4, !Absorbing P2} : P2 ∗ (P3 ∗ Q) ∗ True ∗ P1 ∗ P2 ∗ (P4 ∗ (∃ x:nat, P5 x ∨ P3)) ∗ emp -∗ `````` Robbert Krebbers committed Dec 09, 2016 20 21 `````` P1 -∗ (True ∗ True) -∗ (((P2 ∧ False ∨ P2 ∧ ⌜0 = 0⌝) ∗ P3) ∗ Q ∗ P1 ∗ True) ∧ `````` Robbert Krebbers committed May 31, 2016 22 `````` (P2 ∨ False) ∧ (False → P5 0). `````` Robbert Krebbers committed Apr 11, 2016 23 24 25 26 27 28 29 30 31 ``````Proof. (* Intro-patterns do something :) *) iIntros "[H2 ([H3 HQ]&?&H1&H2'&foo&_)] ? [??]". (* To test destruct: can also be part of the intro-pattern *) iDestruct "foo" as "[_ meh]". repeat iSplit; [|by iLeft|iIntros "#[]"]. iFrame "H2". (* split takes a list of hypotheses just for the LHS *) iSplitL "H3". `````` Robbert Krebbers committed Oct 30, 2017 32 33 `````` - iFrame "H3". iRight. auto. - iSplitL "HQ". iAssumption. by iSplitL "H1". `````` Robbert Krebbers committed Apr 20, 2016 34 35 ``````Qed. `````` Robbert Krebbers committed Apr 13, 2017 36 ``````Lemma demo_3 P1 P2 P3 : `````` Robbert Krebbers committed Oct 30, 2017 37 38 `````` P1 ∗ P2 ∗ P3 -∗ P1 ∗ ▷ (P2 ∗ ∃ x, (P3 ∧ ⌜x = 0⌝) ∨ P3). Proof. iIntros "(\$ & \$ & \$)". iNext. by iExists 0. Qed. `````` Robbert Krebbers committed Apr 27, 2016 39 `````` `````` Robbert Krebbers committed Oct 30, 2017 40 41 ``````Definition foo (P : PROP) := (P -∗ P)%I. Definition bar : PROP := (∀ P, foo P)%I. `````` Robbert Krebbers committed Apr 27, 2016 42 `````` `````` Robbert Krebbers committed Oct 30, 2017 43 44 ``````Lemma test_unfold_constants : bar. Proof. iIntros (P) "HP //". Qed. `````` Robbert Krebbers committed May 02, 2016 45 `````` `````` Robbert Krebbers committed Oct 30, 2017 46 ``````Lemma test_iRewrite {A : ofeT} (x y : A) P : `````` Robbert Krebbers committed Mar 04, 2018 47 `````` □ (∀ z, P -∗ (z ≡ y)) -∗ (P -∗ P ∧ (x,x) ≡ (y,x)). `````` Robbert Krebbers committed May 02, 2016 48 ``````Proof. `````` Robbert Krebbers committed Oct 30, 2017 49 `````` iIntros "#H1 H2". `````` Robbert Krebbers committed Oct 30, 2017 50 `````` iRewrite (bi.internal_eq_sym x x with "[# //]"). `````` Robbert Krebbers committed Mar 14, 2017 51 `````` iRewrite -("H1" \$! _ with "[- //]"). `````` Robbert Krebbers committed Oct 30, 2017 52 `````` auto. `````` Robbert Krebbers committed May 02, 2016 53 54 ``````Qed. `````` Ralf Jung committed Jul 04, 2018 55 ``````Check "test_iDestruct_and_emp". `````` Robbert Krebbers committed Oct 30, 2017 56 ``````Lemma test_iDestruct_and_emp P Q `{!Persistent P, !Persistent Q} : `````` Robbert Krebbers committed Mar 04, 2018 57 `````` P ∧ emp -∗ emp ∧ Q -∗ (P ∗ Q). `````` Ralf Jung committed Jun 05, 2018 58 ``````Proof. iIntros "[#? _] [_ #?]". Show. auto. Qed. `````` Robbert Krebbers committed Oct 30, 2017 59 60 `````` Lemma test_iIntros_persistent P Q `{!Persistent Q} : (P → Q → P ∧ Q)%I. `````` Ralf Jung committed Mar 21, 2018 61 ``````Proof. iIntros "H1 #H2". by iFrame "∗#". Qed. `````` Robbert Krebbers committed Aug 24, 2017 62 `````` `````` Robbert Krebbers committed Aug 28, 2017 63 64 65 ``````Lemma test_iIntros_pure (ψ φ : Prop) P : ψ → (⌜ φ ⌝ → P → ⌜ φ ∧ ψ ⌝ ∧ P)%I. Proof. iIntros (??) "H". auto. Qed. `````` Jacques-Henri Jourdan committed Nov 06, 2017 66 67 68 ``````Lemma test_iIntros_pure_not : (⌜ ¬False ⌝ : PROP)%I. Proof. by iIntros (?). Qed. `````` Robbert Krebbers committed Apr 13, 2017 69 ``````Lemma test_fast_iIntros P Q : `````` Robbert Krebbers committed Dec 09, 2016 70 71 `````` (∀ x y z : nat, ⌜x = plus 0 x⌝ → ⌜y = 0⌝ → ⌜z = 0⌝ → P → □ Q → foo (x ≡ x))%I. `````` Robbert Krebbers committed May 02, 2016 72 ``````Proof. `````` Robbert Krebbers committed Jul 13, 2016 73 `````` iIntros (a) "*". `````` Robbert Krebbers committed May 02, 2016 74 `````` iIntros "#Hfoo **". `````` Robbert Krebbers committed Oct 30, 2017 75 `````` iIntros "_ //". `````` Robbert Krebbers committed May 02, 2016 76 ``````Qed. `````` Ralf Jung committed May 21, 2016 77 `````` `````` Robbert Krebbers committed Sep 27, 2017 78 ``````Lemma test_very_fast_iIntros P : `````` Robbert Krebbers committed Oct 30, 2017 79 `````` ∀ x y : nat, (⌜ x = y ⌝ → P -∗ P)%I. `````` Robbert Krebbers committed Sep 27, 2017 80 81 ``````Proof. by iIntros. Qed. `````` Robbert Krebbers committed Mar 04, 2018 82 83 84 85 86 ``````(** Prior to 0b84351c this used to loop, now `iAssumption` instantiates `R` with `False` and performs false elimination. *) Lemma test_iAssumption_evar_ex_false : ∃ R, R ⊢ ∀ P, P. Proof. eexists. iIntros "?" (P). iAssumption. Qed. `````` Robbert Krebbers committed Oct 30, 2017 87 88 89 ``````Lemma test_iAssumption_affine P Q R `{!Affine P, !Affine R} : P -∗ Q -∗ R -∗ Q. Proof. iIntros "H1 H2 H3". iAssumption. Qed. `````` Robbert Krebbers committed Apr 20, 2018 90 91 92 ``````Lemma test_done_goal_evar Q : ∃ P, Q ⊢ P. Proof. eexists. iIntros "H". Fail done. iAssumption. Qed. `````` Robbert Krebbers committed Apr 13, 2017 93 ``````Lemma test_iDestruct_spatial_and P Q1 Q2 : P ∗ (Q1 ∧ Q2) -∗ P ∗ Q1. `````` Robbert Krebbers committed Nov 13, 2017 94 ``````Proof. iIntros "[H [? _]]". by iFrame. Qed. `````` Robbert Krebbers committed Dec 28, 2016 95 `````` `````` Robbert Krebbers committed Apr 13, 2017 96 ``````Lemma test_iAssert_persistent P Q : P -∗ Q -∗ True. `````` Robbert Krebbers committed Dec 28, 2016 97 98 99 100 101 102 103 104 ``````Proof. iIntros "HP HQ". iAssert True%I as "#_". { by iClear "HP HQ". } iAssert True%I with "[HP]" as "#_". { Fail iClear "HQ". by iClear "HP". } iAssert True%I as %_. { by iClear "HP HQ". } iAssert True%I with "[HP]" as %_. { Fail iClear "HQ". by iClear "HP". } done. Qed. `````` Robbert Krebbers committed Jan 22, 2017 105 `````` `````` Robbert Krebbers committed Feb 20, 2018 106 107 108 109 110 ``````Lemma test_iAssert_persistently P : □ P -∗ True. Proof. iIntros "HP". iAssert (□ P)%I with "[# //]" as "#H". done. Qed. `````` Robbert Krebbers committed Apr 13, 2017 111 ``````Lemma test_iSpecialize_auto_frame P Q R : `````` Robbert Krebbers committed Jan 23, 2017 112 `````` (P -∗ True -∗ True -∗ Q -∗ R) -∗ P -∗ Q -∗ R. `````` Robbert Krebbers committed Nov 13, 2017 113 ``````Proof. iIntros "H ? HQ". by iApply ("H" with "[\$]"). Qed. `````` Robbert Krebbers committed Feb 12, 2017 114 `````` `````` Ralf Jung committed Jun 10, 2018 115 116 117 118 ``````Lemma test_iSpecialize_pure (φ : Prop) Q R: φ → (⌜φ⌝ -∗ Q) → Q. Proof. iIntros (HP HPQ). iDestruct (HPQ \$! HP) as "?". done. Qed. `````` Ralf Jung committed Jun 09, 2018 119 120 121 122 ``````Lemma test_iSpecialize_Coq_entailment P Q R : P → (P -∗ Q) → Q. Proof. iIntros (HP HPQ). iDestruct (HPQ \$! HP) as "?". done. Qed. `````` Robbert Krebbers committed Oct 30, 2017 123 124 125 126 ``````Lemma test_iEmp_intro P Q R `{!Affine P, !Persistent Q, !Affine R} : P -∗ Q → R -∗ emp. Proof. iIntros "HP #HQ HR". iEmpIntro. Qed. `````` Ralf Jung committed Apr 24, 2018 127 ``````Lemma test_fresh P Q: `````` Joseph Tassarotti committed Mar 12, 2018 128 129 130 131 132 133 134 135 136 137 `````` (P ∗ Q) -∗ (P ∗ Q). Proof. iIntros "H". let H1 := iFresh in let H2 := iFresh in let pat :=constr:(IList [cons (IIdent H1) (cons (IIdent H2) nil)]) in iDestruct "H" as pat. iFrame. Qed. `````` Robbert Krebbers committed Feb 12, 2017 138 ``````(* Check coercions *) `````` Robbert Krebbers committed Oct 30, 2017 139 ``````Lemma test_iExist_coercion (P : Z → PROP) : (∀ x, P x) -∗ ∃ x, P x. `````` Robbert Krebbers committed Feb 12, 2017 140 ``````Proof. iIntros "HP". iExists (0:nat). iApply ("HP" \$! (0:nat)). Qed. `````` Jacques-Henri Jourdan committed Feb 13, 2017 141 `````` `````` 142 143 144 145 ``````Lemma test_iExist_tc `{Collection A C} P : (∃ x1 x2 : gset positive, P -∗ P)%I. Proof. iExists {[ 1%positive ]}, ∅. auto. Qed. Lemma test_iSpecialize_tc P : (∀ x y z : gset positive, P) -∗ P. `````` Robbert Krebbers committed Mar 05, 2018 146 147 ``````Proof. iIntros "H". `````` Ralf Jung committed Mar 06, 2018 148 `````` (* FIXME: this [unshelve] and [apply _] should not be needed. *) `````` Robbert Krebbers committed Mar 05, 2018 149 150 `````` unshelve iSpecialize ("H" \$! ∅ {[ 1%positive ]} ∅); try apply _. done. Qed. `````` 151 `````` `````` Robbert Krebbers committed Oct 30, 2017 152 ``````Lemma test_iFrame_pure {A : ofeT} (φ : Prop) (y z : A) : `````` Robbert Krebbers committed Mar 04, 2018 153 `````` φ → ⌜y ≡ z⌝ -∗ (⌜ φ ⌝ ∧ ⌜ φ ⌝ ∧ y ≡ z : PROP). `````` Robbert Krebbers committed Oct 30, 2017 154 155 ``````Proof. iIntros (Hv) "#Hxy". iFrame (Hv) "Hxy". Qed. `````` Jacques-Henri Jourdan committed Feb 20, 2018 156 157 158 159 160 161 162 163 164 165 166 167 168 169 ``````Lemma test_iFrame_disjunction_1 P1 P2 Q1 Q2 : BiAffine PROP → □ P1 -∗ Q2 -∗ P2 -∗ (P1 ∗ P2 ∗ False ∨ P2) ∗ (Q1 ∨ Q2). Proof. intros ?. iIntros "#HP1 HQ2 HP2". iFrame "HP1 HQ2 HP2". Qed. Lemma test_iFrame_disjunction_2 P : P -∗ (True ∨ True) ∗ P. Proof. iIntros "HP". iFrame "HP". auto. Qed. Lemma test_iFrame_conjunction_1 P Q : P -∗ Q -∗ (P ∗ Q) ∧ (P ∗ Q). Proof. iIntros "HP HQ". iFrame "HP HQ". Qed. Lemma test_iFrame_conjunction_2 P Q : P -∗ Q -∗ (P ∧ P) ∗ (Q ∧ Q). Proof. iIntros "HP HQ". iFrame "HP HQ". Qed. `````` Robbert Krebbers committed May 31, 2018 170 171 172 ``````Lemma test_iFrame_later `{BiAffine PROP} P Q : P -∗ Q -∗ ▷ P ∗ Q. Proof. iIntros "H1 H2". by iFrame "H1". Qed. `````` Robbert Krebbers committed Oct 30, 2017 173 174 175 ``````Lemma test_iAssert_modality P : ◇ False -∗ ▷ P. Proof. iIntros "HF". `````` Robbert Krebbers committed Mar 04, 2018 176 `````` iAssert ( False)%I with "[> -]" as %[]. `````` Robbert Krebbers committed Oct 30, 2017 177 178 `````` by iMod "HF". Qed. `````` Robbert Krebbers committed Feb 13, 2017 179 `````` `````` Jacques-Henri Jourdan committed Nov 02, 2017 180 ``````Lemma test_iMod_affinely_timeless P `{!Timeless P} : `````` Robbert Krebbers committed Mar 04, 2018 181 `````` ▷ P -∗ ◇ P. `````` Robbert Krebbers committed Oct 30, 2017 182 183 ``````Proof. iIntros "H". iMod "H". done. Qed. `````` Robbert Krebbers committed Apr 13, 2017 184 ``````Lemma test_iAssumption_False P : False -∗ P. `````` Robbert Krebbers committed Feb 13, 2017 185 ``````Proof. iIntros "H". done. Qed. `````` Robbert Krebbers committed Feb 13, 2017 186 187 `````` (* Check instantiation and dependent types *) `````` Robbert Krebbers committed Oct 30, 2017 188 ``````Lemma test_iSpecialize_dependent_type (P : ∀ n, vec nat n → PROP) : `````` Robbert Krebbers committed Feb 13, 2017 189 190 191 192 193 `````` (∀ n v, P n v) -∗ ∃ n v, P n v. Proof. iIntros "H". iExists _, [#10]. iSpecialize ("H" \$! _ [#10]). done. Qed. `````` Robbert Krebbers committed Feb 15, 2017 194 `````` `````` Ralf Jung committed Mar 06, 2018 195 196 197 198 199 ``````(* Check that typeclasses are not resolved too early *) Lemma test_TC_resolution `{!BiAffine PROP} (Φ : nat → PROP) l x : x ∈ l → ([∗ list] y ∈ l, Φ y) -∗ Φ x. Proof. iIntros (Hp) "HT". `````` Ralf Jung committed May 29, 2018 200 `````` iDestruct (big_sepL_elem_of _ _ _ Hp with "HT") as "Hp". `````` Ralf Jung committed Mar 06, 2018 201 202 203 `````` done. Qed. `````` Robbert Krebbers committed Oct 30, 2017 204 205 ``````Lemma test_eauto_iFrame P Q R `{!Persistent R} : P -∗ Q -∗ R → R ∗ Q ∗ P ∗ R ∨ False. `````` Robbert Krebbers committed Nov 02, 2017 206 ``````Proof. eauto 10 with iFrame. Qed. `````` Robbert Krebbers committed Feb 21, 2017 207 `````` `````` Robbert Krebbers committed Oct 25, 2017 208 ``````Lemma test_iCombine_persistent P Q R `{!Persistent R} : `````` Robbert Krebbers committed Oct 30, 2017 209 `````` P -∗ Q -∗ R → R ∗ Q ∗ P ∗ R ∨ False. `````` Robbert Krebbers committed Feb 21, 2017 210 ``````Proof. iIntros "HP HQ #HR". iCombine "HR HQ HP HR" as "H". auto. Qed. `````` Ralf Jung committed Mar 10, 2017 211 `````` `````` Robbert Krebbers committed May 18, 2018 212 213 214 215 ``````Lemma test_iCombine_frame P Q R `{!Persistent R} : P -∗ Q -∗ R → R ∗ Q ∗ P ∗ R. Proof. iIntros "HP HQ #HR". iCombine "HQ HP HR" as "\$". by iFrame. Qed. `````` Robbert Krebbers committed Apr 13, 2017 216 ``````Lemma test_iNext_evar P : P -∗ True. `````` Ralf Jung committed Mar 10, 2017 217 218 219 220 ``````Proof. iIntros "HP". iAssert (▷ _ -∗ ▷ P)%I as "?"; last done. iIntros "?". iNext. iAssumption. Qed. `````` Robbert Krebbers committed Mar 11, 2017 221 `````` `````` Robbert Krebbers committed Mar 03, 2018 222 223 ``````Lemma test_iNext_sep1 P Q (R1 := (P ∗ Q)%I) : (▷ P ∗ ▷ Q) ∗ R1 -∗ ▷ ((P ∗ Q) ∗ R1). `````` Robbert Krebbers committed Mar 11, 2017 224 225 226 227 ``````Proof. iIntros "H". iNext. rewrite {1 2}(lock R1). (* check whether R1 has not been unfolded *) done. Qed. `````` Ralf Jung committed Mar 12, 2017 228 `````` `````` Robbert Krebbers committed Apr 13, 2017 229 ``````Lemma test_iNext_sep2 P Q : ▷ P ∗ ▷ Q -∗ ▷ (P ∗ Q). `````` Ralf Jung committed Mar 12, 2017 230 231 232 ``````Proof. iIntros "H". iNext. iExact "H". (* Check that the laters are all gone. *) Qed. `````` Robbert Krebbers committed Mar 15, 2017 233 `````` `````` Robbert Krebbers committed Oct 30, 2017 234 ``````Lemma test_iNext_quantifier {A} (Φ : A → A → PROP) : `````` Robbert Krebbers committed Sep 27, 2017 235 236 237 `````` (∀ y, ∃ x, ▷ Φ x y) -∗ ▷ (∀ y, ∃ x, Φ x y). Proof. iIntros "H". iNext. done. Qed. `````` Robbert Krebbers committed Oct 30, 2017 238 ``````Lemma test_iFrame_persistent (P Q : PROP) : `````` Robbert Krebbers committed Mar 04, 2018 239 `````` □ P -∗ Q -∗ (P ∗ P) ∗ (P ∗ Q ∨ Q). `````` Robbert Krebbers committed Mar 15, 2017 240 ``````Proof. iIntros "#HP". iFrame "HP". iIntros "\$". Qed. `````` Robbert Krebbers committed Mar 22, 2017 241 `````` `````` Robbert Krebbers committed Mar 04, 2018 242 ``````Lemma test_iSplit_persistently P Q : □ P -∗ (P ∗ P). `````` Robbert Krebbers committed Mar 22, 2017 243 ``````Proof. iIntros "#?". by iSplit. Qed. `````` Ralf Jung committed Apr 11, 2017 244 `````` `````` Robbert Krebbers committed Mar 04, 2018 245 ``````Lemma test_iSpecialize_persistent P Q : □ P -∗ ( P → Q) -∗ Q. `````` Robbert Krebbers committed Apr 13, 2017 246 ``````Proof. iIntros "#HP HPQ". by iSpecialize ("HPQ" with "HP"). Qed. `````` Robbert Krebbers committed May 17, 2017 247 `````` `````` Robbert Krebbers committed Oct 30, 2017 248 ``````Lemma test_iDestruct_persistent P (Φ : nat → PROP) `{!∀ x, Persistent (Φ x)}: `````` Jacques-Henri Jourdan committed Nov 02, 2017 249 `````` □ (P -∗ ∃ x, Φ x) -∗ `````` Robbert Krebbers committed Oct 30, 2017 250 251 252 253 254 `````` P -∗ ∃ x, Φ x ∗ P. Proof. iIntros "#H HP". iDestruct ("H" with "HP") as (x) "#H2". eauto with iFrame. Qed. `````` Robbert Krebbers committed May 17, 2017 255 256 257 258 259 ``````Lemma test_iLöb P : (∃ n, ▷^n P)%I. Proof. iLöb as "IH". iDestruct "IH" as (n) "IH". by iExists (S n). Qed. `````` Ralf Jung committed Sep 27, 2017 260 `````` `````` Robbert Krebbers committed Oct 05, 2017 261 ``````Lemma test_iInduction_wf (x : nat) P Q : `````` Jacques-Henri Jourdan committed Nov 02, 2017 262 `````` □ P -∗ Q -∗ ⌜ (x + 0 = x)%nat ⌝. `````` Robbert Krebbers committed Oct 05, 2017 263 264 265 266 267 268 ``````Proof. iIntros "#HP HQ". iInduction (lt_wf x) as [[|x] _] "IH"; simpl; first done. rewrite (inj_iff S). by iApply ("IH" with "[%]"); first omega. Qed. `````` Robbert Krebbers committed Jul 31, 2018 269 270 271 272 273 274 275 276 277 ``````Lemma test_iInduction_using (m : gmap nat nat) (Φ : nat → nat → PROP) y : ([∗ map] x ↦ i ∈ m, Φ y x) -∗ ([∗ map] x ↦ i ∈ m, emp ∗ Φ y x). Proof. iIntros "Hm". iInduction m as [|i x m] "IH" using map_ind forall(y). - by rewrite !big_sepM_empty. - rewrite !big_sepM_insert //. iDestruct "Hm" as "[\$ ?]". by iApply "IH". Qed. `````` Ralf Jung committed Sep 27, 2017 278 ``````Lemma test_iIntros_start_proof : `````` Robbert Krebbers committed Oct 30, 2017 279 `````` (True : PROP)%I. `````` Ralf Jung committed Sep 27, 2017 280 281 282 283 284 ``````Proof. (* Make sure iIntros actually makes progress and enters the proofmode. *) progress iIntros. done. Qed. `````` Robbert Krebbers committed Oct 30, 2017 285 ``````Lemma test_True_intros : (True : PROP) -∗ True. `````` Ralf Jung committed Sep 27, 2017 286 287 288 ``````Proof. iIntros "?". done. Qed. `````` Robbert Krebbers committed Sep 29, 2017 289 290 291 292 293 294 295 296 297 298 `````` Lemma test_iPoseProof_let P Q : (let R := True%I in R ∗ P ⊢ Q) → P ⊢ Q. Proof. iIntros (help) "HP". iPoseProof (help with "[\$HP]") as "?". done. Qed. Lemma test_iIntros_let P : `````` Robbert Krebbers committed Oct 30, 2017 299 300 `````` ∀ Q, let R := emp%I in P -∗ R -∗ Q -∗ P ∗ Q. Proof. iIntros (Q R) "\$ _ \$". Qed. `````` Robbert Krebbers committed Oct 25, 2017 301 `````` `````` Robbert Krebbers committed Mar 04, 2018 302 ``````Lemma test_foo P Q : ▷ (Q ≡ P) -∗ ▷ Q -∗ ▷ P. `````` Robbert Krebbers committed Oct 30, 2017 303 ``````Proof. `````` Robbert Krebbers committed Oct 30, 2017 304 `````` iIntros "#HPQ HQ !#". iNext. by iRewrite "HPQ" in "HQ". `````` Robbert Krebbers committed Oct 30, 2017 305 306 ``````Qed. `````` Robbert Krebbers committed Oct 30, 2017 307 ``````Lemma test_iIntros_modalities `(!Absorbing P) : `````` Robbert Krebbers committed Mar 04, 2018 308 `````` ( (▷ ∀ x : nat, ⌜ x = 0 ⌝ → ⌜ x = 0 ⌝ -∗ False -∗ P -∗ P))%I. `````` Robbert Krebbers committed Oct 25, 2017 309 310 311 312 313 ``````Proof. iIntros (x ??). iIntros "* **". (* Test that fast intros do not work under modalities *) iIntros ([]). Qed. `````` Robbert Krebbers committed Oct 30, 2017 314 `````` `````` Robbert Krebbers committed Oct 27, 2017 315 316 317 ``````Lemma test_iIntros_rewrite P (x1 x2 x3 x4 : nat) : x1 = x2 → (⌜ x2 = x3 ⌝ ∗ ⌜ x3 ≡ x4 ⌝ ∗ P) -∗ ⌜ x1 = x4 ⌝ ∗ P. Proof. iIntros (?) "(-> & -> & \$)"; auto. Qed. `````` Robbert Krebbers committed Apr 13, 2017 318 `````` `````` Robbert Krebbers committed Mar 04, 2018 319 ``````Lemma test_iNext_affine P Q : ▷ (Q ≡ P) -∗ ▷ Q -∗ ▷ P. `````` Robbert Krebbers committed Oct 30, 2017 320 321 ``````Proof. iIntros "#HPQ HQ !#". iNext. by iRewrite "HPQ" in "HQ". Qed. `````` Jacques-Henri Jourdan committed Nov 02, 2017 322 ``````Lemma test_iAlways P Q R : `````` Robbert Krebbers committed Mar 04, 2018 323 `````` □ P -∗ Q → R -∗ P ∗ □ Q. `````` Robbert Krebbers committed Oct 30, 2017 324 ``````Proof. iIntros "#HP #HQ HR". iSplitL. iAlways. done. iAlways. done. Qed. `````` Jacques-Henri Jourdan committed Nov 03, 2017 325 `````` `````` Robbert Krebbers committed Dec 20, 2017 326 327 328 ``````(* A bunch of test cases from #127 to establish that tactics behave the same on `⌜ φ ⌝ → P` and `∀ _ : φ, P` *) Lemma test_forall_nondep_1 (φ : Prop) : `````` Jacques-Henri Jourdan committed Dec 21, 2017 329 `````` φ → (∀ _ : φ, False : PROP) -∗ False. `````` Robbert Krebbers committed Dec 20, 2017 330 331 ``````Proof. iIntros (Hφ) "Hφ". by iApply "Hφ". Qed. Lemma test_forall_nondep_2 (φ : Prop) : `````` Jacques-Henri Jourdan committed Dec 21, 2017 332 `````` φ → (∀ _ : φ, False : PROP) -∗ False. `````` Robbert Krebbers committed Dec 20, 2017 333 334 ``````Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" with "[% //]"). done. Qed. Lemma test_forall_nondep_3 (φ : Prop) : `````` Jacques-Henri Jourdan committed Dec 21, 2017 335 `````` φ → (∀ _ : φ, False : PROP) -∗ False. `````` Robbert Krebbers committed Dec 20, 2017 336 337 ``````Proof. iIntros (Hφ) "Hφ". unshelve iSpecialize ("Hφ" \$! _). done. done. Qed. Lemma test_forall_nondep_4 (φ : Prop) : `````` Jacques-Henri Jourdan committed Dec 21, 2017 338 `````` φ → (∀ _ : φ, False : PROP) -∗ False. `````` Robbert Krebbers committed Dec 20, 2017 339 340 341 ``````Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" \$! Hφ); done. Qed. Lemma test_pure_impl_1 (φ : Prop) : `````` Jacques-Henri Jourdan committed Dec 21, 2017 342 `````` φ → (⌜φ⌝ → False : PROP) -∗ False. `````` Robbert Krebbers committed Dec 20, 2017 343 344 ``````Proof. iIntros (Hφ) "Hφ". by iApply "Hφ". Qed. Lemma test_pure_impl_2 (φ : Prop) : `````` Jacques-Henri Jourdan committed Dec 21, 2017 345 `````` φ → (⌜φ⌝ → False : PROP) -∗ False. `````` Robbert Krebbers committed Dec 20, 2017 346 347 ``````Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" with "[% //]"). done. Qed. Lemma test_pure_impl_3 (φ : Prop) : `````` Jacques-Henri Jourdan committed Dec 21, 2017 348 `````` φ → (⌜φ⌝ → False : PROP) -∗ False. `````` Robbert Krebbers committed Dec 20, 2017 349 350 ``````Proof. iIntros (Hφ) "Hφ". unshelve iSpecialize ("Hφ" \$! _). done. done. Qed. Lemma test_pure_impl_4 (φ : Prop) : `````` Jacques-Henri Jourdan committed Dec 21, 2017 351 `````` φ → (⌜φ⌝ → False : PROP) -∗ False. `````` Robbert Krebbers committed Dec 20, 2017 352 353 354 ``````Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" \$! Hφ). done. Qed. Lemma test_forall_nondep_impl2 (φ : Prop) P : `````` Jacques-Henri Jourdan committed Dec 21, 2017 355 `````` φ → P -∗ (∀ _ : φ, P -∗ False : PROP) -∗ False. `````` Robbert Krebbers committed Dec 20, 2017 356 357 358 359 360 361 362 ``````Proof. iIntros (Hφ) "HP Hφ". Fail iSpecialize ("Hφ" with "HP"). iSpecialize ("Hφ" with "[% //] HP"). done. Qed. Lemma test_pure_impl2 (φ : Prop) P : `````` Jacques-Henri Jourdan committed Dec 21, 2017 363 `````` φ → P -∗ (⌜φ⌝ → P -∗ False : PROP) -∗ False. `````` Robbert Krebbers committed Dec 20, 2017 364 365 366 367 368 369 ``````Proof. iIntros (Hφ) "HP Hφ". Fail iSpecialize ("Hφ" with "HP"). iSpecialize ("Hφ" with "[% //] HP"). done. Qed. `````` Robbert Krebbers committed Feb 20, 2018 370 ``````Lemma test_iNext_laterN_later P n : ▷ ▷^n P -∗ ▷^n ▷ P. `````` Robbert Krebbers committed Jan 20, 2018 371 ``````Proof. iIntros "H". iNext. by iNext. Qed. `````` Robbert Krebbers committed Feb 20, 2018 372 ``````Lemma test_iNext_later_laterN P n : ▷^n ▷ P -∗ ▷ ▷^n P. `````` Robbert Krebbers committed Jan 20, 2018 373 ``````Proof. iIntros "H". iNext. by iNext. Qed. `````` Robbert Krebbers committed Feb 20, 2018 374 ``````Lemma test_iNext_plus_1 P n1 n2 : ▷ ▷^n1 ▷^n2 P -∗ ▷^n1 ▷^n2 ▷ P. `````` Robbert Krebbers committed Jan 20, 2018 375 ``````Proof. iIntros "H". iNext. iNext. by iNext. Qed. `````` Robbert Krebbers committed Feb 20, 2018 376 377 ``````Lemma test_iNext_plus_2 P n m : ▷^n ▷^m P -∗ ▷^(n+m) P. Proof. iIntros "H". iNext. done. Qed. `````` Ralf Jung committed Jul 04, 2018 378 ``````Check "test_iNext_plus_3". `````` Robbert Krebbers committed Feb 20, 2018 379 380 ``````Lemma test_iNext_plus_3 P Q n m k : ▷^m ▷^(2 + S n + k) P -∗ ▷^m ▷ ▷^(2 + S n) Q -∗ ▷^k ▷ ▷^(S (S n + S m)) (P ∗ Q). `````` Ralf Jung committed Jul 04, 2018 381 ``````Proof. iIntros "H1 H2". iNext. iNext. iNext. iFrame. Show. iModIntro. done. Qed. `````` Robbert Krebbers committed Jan 20, 2018 382 `````` `````` Robbert Krebbers committed Feb 20, 2018 383 384 385 386 387 388 389 390 ``````Lemma test_iNext_unfold P Q n m (R := (▷^n P)%I) : R ⊢ ▷^m True. Proof. iIntros "HR". iNext. match goal with |- context [ R ] => idtac | |- _ => fail end. done. Qed. `````` Robbert Krebbers committed Feb 20, 2018 391 392 393 ``````Lemma test_iNext_fail P Q a b c d e f g h i j: ▷^(a + b) ▷^(c + d + e) P -∗ ▷^(f + g + h + i + j) True. Proof. iIntros "H". iNext. done. Qed. `````` Jacques-Henri Jourdan committed Feb 12, 2018 394 395 `````` Lemma test_specialize_affine_pure (φ : Prop) P : `````` Robbert Krebbers committed Mar 04, 2018 396 `````` φ → ( ⌜φ⌝ -∗ P) ⊢ P. `````` Jacques-Henri Jourdan committed Feb 12, 2018 397 398 399 400 401 ``````Proof. iIntros (Hφ) "H". by iSpecialize ("H" with "[% //]"). Qed. Lemma test_assert_affine_pure (φ : Prop) P : `````` Robbert Krebbers committed Mar 04, 2018 402 403 `````` φ → P ⊢ P ∗ ⌜φ⌝. Proof. iIntros (Hφ). iAssert ( ⌜φ⌝)%I with "[%]" as "\$"; auto. Qed. `````` Jacques-Henri Jourdan committed Feb 12, 2018 404 405 ``````Lemma test_assert_pure (φ : Prop) P : φ → P ⊢ P ∗ ⌜φ⌝. `````` Ralf Jung committed Mar 21, 2018 406 ``````Proof. iIntros (Hφ). iAssert ⌜φ⌝%I with "[%]" as "\$"; auto with iFrame. Qed. `````` Jacques-Henri Jourdan committed Feb 12, 2018 407 `````` `````` Robbert Krebbers committed Feb 20, 2018 408 ``````Lemma test_iEval x y : ⌜ (y + x)%nat = 1 ⌝ -∗ ⌜ S (x + y) = 2%nat ⌝ : PROP. `````` Robbert Krebbers committed Jan 23, 2018 409 410 411 412 413 414 ``````Proof. iIntros (H). iEval (rewrite (Nat.add_comm x y) // H). done. Qed. `````` Ralf Jung committed Apr 25, 2018 415 ``````Lemma test_iIntros_pure_neg : (⌜ ¬False ⌝ : PROP)%I. `````` 416 ``````Proof. by iIntros (?). Qed. `````` Robbert Krebbers committed Apr 13, 2017 417 `````` `````` Ralf Jung committed May 09, 2018 418 419 420 421 ``````Lemma test_iPureIntro_absorbing (φ : Prop) : φ → sbi_emp_valid (PROP:=PROP) ( ⌜φ⌝)%I. Proof. intros ?. iPureIntro. done. Qed. `````` Ralf Jung committed Jul 04, 2018 422 ``````Check "test_iFrame_later_1". `````` Jacques-Henri Jourdan committed Feb 23, 2018 423 ``````Lemma test_iFrame_later_1 P Q : P ∗ ▷ Q -∗ ▷ (P ∗ ▷ Q). `````` Ralf Jung committed Jul 04, 2018 424 ``````Proof. iIntros "H". iFrame "H". Show. auto. Qed. `````` Robbert Krebbers committed Apr 13, 2017 425 `````` `````` Ralf Jung committed Jul 04, 2018 426 ``````Check "test_iFrame_later_2". `````` Jacques-Henri Jourdan committed Feb 23, 2018 427 ``````Lemma test_iFrame_later_2 P Q : ▷ P ∗ ▷ Q -∗ ▷ (▷ P ∗ ▷ Q). `````` Ralf Jung committed Jul 04, 2018 428 ``````Proof. iIntros "H". iFrame "H". Show. auto. Qed. `````` Robbert Krebbers committed Feb 27, 2018 429 430 431 432 433 434 435 `````` Lemma test_with_ident P Q R : P -∗ Q -∗ (P -∗ Q -∗ R) -∗ R. Proof. iIntros "? HQ H". iMatchHyp (fun H _ => iApply ("H" with [spec_patterns.SIdent H; spec_patterns.SIdent "HQ"])). Qed. `````` Jacques-Henri Jourdan committed Feb 27, 2018 436 437 `````` Lemma iFrame_with_evar_r P Q : `````` Jacques-Henri Jourdan committed Mar 03, 2018 438 `````` ∃ R, (P -∗ Q -∗ P ∗ R) ∧ R = Q. `````` Jacques-Henri Jourdan committed Feb 27, 2018 439 ``````Proof. `````` Jacques-Henri Jourdan committed Mar 03, 2018 440 `````` eexists. split. iIntros "HP HQ". iFrame. iApply "HQ". done. `````` Jacques-Henri Jourdan committed Feb 27, 2018 441 442 ``````Qed. Lemma iFrame_with_evar_l P Q : `````` Jacques-Henri Jourdan committed Mar 03, 2018 443 `````` ∃ R, (P -∗ Q -∗ R ∗ P) ∧ R = Q. `````` Jacques-Henri Jourdan committed Feb 27, 2018 444 ``````Proof. `````` Jacques-Henri Jourdan committed Mar 03, 2018 445 `````` eexists. split. iIntros "HP HQ". Fail iFrame "HQ". `````` Robbert Krebbers committed Apr 20, 2018 446 `````` iSplitR "HP"; iAssumption. done. `````` Jacques-Henri Jourdan committed Feb 27, 2018 447 ``````Qed. `````` Jacques-Henri Jourdan committed Mar 01, 2018 448 449 450 451 452 453 ``````Lemma iFrame_with_evar_persistent P Q : ∃ R, (P -∗ □ Q -∗ P ∗ R ∗ Q) ∧ R = emp%I. Proof. eexists. split. iIntros "HP #HQ". iFrame "HQ HP". iEmpIntro. done. Qed. `````` Jacques-Henri Jourdan committed Mar 03, 2018 454 455 456 457 458 459 ``````Lemma test_iAccu P Q R S : ∃ PP, (□P -∗ Q -∗ R -∗ S -∗ PP) ∧ PP = (Q ∗ R ∗ S)%I. Proof. eexists. split. iIntros "#? ? ? ?". iAccu. done. Qed. `````` Ralf Jung committed Mar 07, 2018 460 ``````Lemma test_iAssumption_evar P : ∃ R, (R ⊢ P) ∧ R = P. `````` Ralf Jung committed Mar 07, 2018 461 462 463 464 465 466 467 ``````Proof. eexists. split. - iIntros "H". iAssumption. (* Now verify that the evar was chosen as desired (i.e., it should not pick False). *) - reflexivity. Qed. `````` Ralf Jung committed Mar 07, 2018 468 469 470 ``````Lemma test_iAssumption_False_no_loop : ∃ R, R ⊢ ∀ P, P. Proof. eexists. iIntros "?" (P). done. Qed. `````` Ralf Jung committed Mar 08, 2018 471 472 473 474 ``````Lemma test_apply_affine_impl `{!BiPlainly PROP} (P : PROP) : P -∗ (∀ Q : PROP, ■ (Q -∗ Q) → ■ (P -∗ Q) → Q). Proof. iIntros "HP" (Q) "_ #HPQ". by iApply "HPQ". Qed. `````` Ralf Jung committed Mar 08, 2018 475 476 477 478 ``````Lemma test_apply_affine_wand `{!BiPlainly PROP} (P : PROP) : P -∗ (∀ Q : PROP, ■ (Q -∗ Q) -∗ ■ (P -∗ Q) -∗ Q). Proof. iIntros "HP" (Q) "_ #HPQ". by iApply "HPQ". Qed. `````` 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 ``````Lemma test_and_sep (P Q R : PROP) : P ∧ (Q ∗ □ R) ⊢ (P ∧ Q) ∗ □ R. Proof. iIntros "H". repeat iSplit. - iDestruct "H" as "[\$ _]". - iDestruct "H" as "[_ [\$ _]]". - iDestruct "H" as "[_ [_ #\$]]". Qed. Lemma test_and_sep_2 (P Q R : PROP) `{!Persistent R, !Affine R} : P ∧ (Q ∗ R) ⊢ (P ∧ Q) ∗ R. Proof. iIntros "H". repeat iSplit. - iDestruct "H" as "[\$ _]". - iDestruct "H" as "[_ [\$ _]]". - iDestruct "H" as "[_ [_ #\$]]". Qed. `````` Robbert Krebbers committed May 03, 2018 495 `````` `````` Ralf Jung committed Jul 04, 2018 496 ``````Check "test_and_sep_affine_bi". `````` Robbert Krebbers committed May 03, 2018 497 498 ``````Lemma test_and_sep_affine_bi `{BiAffine PROP} P Q : □ P ∧ Q ⊢ □ P ∗ Q. Proof. `````` Ralf Jung committed Jun 10, 2018 499 `````` iIntros "[??]". iSplit; last done. Show. done. `````` Robbert Krebbers committed May 03, 2018 500 ``````Qed. `````` Ralf Jung committed Jun 10, 2018 501 `````` `````` Ralf Jung committed Jul 04, 2018 502 ``````Check "test_big_sepL_simpl". `````` Robbert Krebbers committed Jun 15, 2018 503 ``````Lemma test_big_sepL_simpl x (l : list nat) P : `````` Robbert Krebbers committed Jun 16, 2018 504 `````` P -∗ `````` Robbert Krebbers committed Jun 15, 2018 505 506 507 `````` ([∗ list] k↦y ∈ l, ⌜ y = y ⌝) -∗ ([∗ list] y ∈ x :: l, ⌜ y = y ⌝) -∗ P. `````` Ralf Jung committed Jul 04, 2018 508 ``````Proof. iIntros "HP ??". Show. simpl. Show. done. Qed. `````` Robbert Krebbers committed Jun 16, 2018 509 `````` `````` Ralf Jung committed Jul 04, 2018 510 ``````Check "test_big_sepL2_simpl". `````` Robbert Krebbers committed Jun 16, 2018 511 512 513 514 515 ``````Lemma test_big_sepL2_simpl x1 x2 (l1 l2 : list nat) P : P -∗ ([∗ list] k↦y1;y2 ∈ []; l2, ⌜ y1 = y2 ⌝) -∗ ([∗ list] y1;y2 ∈ x1 :: l1; (x2 :: l2) ++ l2, ⌜ y1 = y2 ⌝) -∗ P ∨ ([∗ list] y1;y2 ∈ x1 :: l1; x2 :: l2, True). `````` Ralf Jung committed Jul 04, 2018 516 ``````Proof. iIntros "HP ??". Show. simpl. Show. by iLeft. Qed. `````` Robbert Krebbers committed Jun 16, 2018 517 `````` `````` Ralf Jung committed Jul 04, 2018 518 ``````Check "test_big_sepL2_iDestruct". `````` Robbert Krebbers committed Jun 16, 2018 519 520 521 522 523 524 525 526 527 ``````Lemma test_big_sepL2_iDestruct (Φ : nat → nat → PROP) x1 x2 (l1 l2 : list nat) : ([∗ list] y1;y2 ∈ x1 :: l1; x2 :: l2, Φ y1 y2) -∗ Φ x1 x2. Proof. iIntros "[??]". Show. iFrame. Qed. Lemma test_big_sepL2_iFrame (Φ : nat → nat → PROP) (l1 l2 : list nat) P : Φ 0 10 -∗ ([∗ list] y1;y2 ∈ l1;l2, Φ y1 y2) -∗ ([∗ list] y1;y2 ∈ (0 :: l1);(10 :: l2), Φ y1 y2). Proof. iIntros "\$ ?". iFrame. Qed. `````` Ralf Jung committed Jul 02, 2018 528 529 530 531 `````` Lemma test_lemma_1 (b : bool) : emp ⊢@{PROP} □?b True. Proof. destruct b; simpl; eauto. Qed. `````` Ralf Jung committed Jul 04, 2018 532 ``````Check "test_reducing_after_iDestruct". `````` Ralf Jung committed Jul 02, 2018 533 534 535 536 537 538 539 540 ``````Lemma test_reducing_after_iDestruct : emp ⊢@{PROP} True. Proof. iIntros "H". iDestruct (test_lemma_1 true with "H") as "H". Show. done. Qed. Lemma test_lemma_2 (b : bool) : □?b emp ⊢@{PROP} emp. Proof. destruct b; simpl; eauto. Qed. `````` Ralf Jung committed Jul 04, 2018 541 ``````Check "test_reducing_after_iApply". `````` Ralf Jung committed Jul 02, 2018 542 543 544 545 546 547 548 549 ``````Lemma test_reducing_after_iApply : emp ⊢@{PROP} emp. Proof. iIntros "#H". iApply (test_lemma_2 true). Show. auto. Qed. Lemma test_lemma_3 (b : bool) : □?b emp ⊢@{PROP} ⌜b = b⌝. Proof. destruct b; simpl; eauto. Qed. `````` Ralf Jung committed Jul 04, 2018 550 ``````Check "test_reducing_after_iApply_late_evar". `````` Ralf Jung committed Jul 02, 2018 551 552 553 554 555 556 ``````Lemma test_reducing_after_iApply_late_evar : emp ⊢@{PROP} ⌜true = true⌝. Proof. iIntros "#H". iApply (test_lemma_3). Show. auto. Qed. Section wandM. `````` Ralf Jung committed Jul 02, 2018 557 `````` Import proofmode.base. `````` Ralf Jung committed Jul 04, 2018 558 `````` Check "test_wandM". `````` Ralf Jung committed Jul 02, 2018 559 560 561 562 563 564 565 `````` Lemma test_wandM mP Q R : (mP -∗? Q) -∗ (Q -∗ R) -∗ (mP -∗? R). Proof. iIntros "HPQ HQR HP". Show. iApply "HQR". iApply "HPQ". Show. done. Qed. `````` Ralf Jung committed Jul 02, 2018 566 567 ``````End wandM. `````` 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 ``````Definition modal_if_def b (P : PROP) := (□?b P)%I. Lemma modal_if_lemma1 b P : False -∗ □?b P. Proof. iIntros "?". by iExFalso. Qed. Lemma test_iApply_prettification1 (P : PROP) : False -∗ modal_if_def true P. Proof. (* Make sure the goal is not prettified before [iApply] unifies. *) iIntros "?". rewrite /modal_if_def. iApply modal_if_lemma1. iAssumption. Qed. Lemma modal_if_lemma2 P : False -∗ □?false P. Proof. iIntros "?". by iExFalso. Qed. Lemma test_iApply_prettification2 (P : PROP) : False -∗ ∃ b, □?b P. Proof. (* Make sure the conclusion of the lemma is not prettified too early. *) iIntros "?". iExists _. iApply modal_if_lemma2. done. Qed. `````` Ralf Jung committed Jul 04, 2018 588 `````` `````` Ralf Jung committed Oct 04, 2018 589 590 591 592 593 594 ``````Lemma test_iDestruct_clear P Q R : P -∗ (Q ∗ R) -∗ True. Proof. iIntros "HP HQR". iDestruct "HQR" as "{HP} [HQ HR]". done. Qed. `````` Ralf Jung committed Apr 11, 2017 595 ``````End tests. `````` Ralf Jung committed Jun 06, 2018 596 597 598 599 600 `````` (** Test specifically if certain things print correctly. *) Section printing_tests. Context {PROP : sbi} `{!BiFUpd PROP}. Implicit Types P Q R : PROP. `````` Ralf Jung committed Jul 04, 2018 601 602 603 604 605 `````` Check "elim_mod_accessor". Lemma elim_mod_accessor {X : Type} E1 E2 α (β : X → PROP) γ : accessor (fupd E1 E2) (fupd E2 E1) α β γ -∗ |={E1}=> True. Proof. iIntros ">Hacc". Show. Abort. `````` Ralf Jung committed Jun 06, 2018 606 607 608 `````` (* Test line breaking of long assumptions. *) Section linebreaks. `````` Ralf Jung committed Jul 04, 2018 609 610 ``````Check "print_long_line_1". Lemma print_long_line_1 (P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP) : `````` Ralf Jung committed Jun 06, 2018 611 612 613 614 `````` P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P ∗ P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P -∗ True. Proof. `````` Ralf Jung committed Jun 14, 2018 615 `````` iIntros "HP". Show. Undo. iIntros "?". Show. `````` Ralf Jung committed Jun 06, 2018 616 617 ``````Abort. `````` Ralf Jung committed Jun 06, 2018 618 ``````(* This is specifically crafted such that not having the printing box in `````` Ralf Jung committed Jun 06, 2018 619 620 621 `````` the proofmode notation breaks the output. *) Local Notation "'TESTNOTATION' '{{' P '|' Q '}' '}'" := (P ∧ Q)%I (format "'TESTNOTATION' '{{' P '|' '/' Q '}' '}'") : bi_scope. `````` Ralf Jung committed Jul 04, 2018 622 623 ``````Check "print_long_line_2". Lemma print_long_line_2 (P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP) : `````` Ralf Jung committed Jun 06, 2018 624 625 626 `````` TESTNOTATION {{ P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P | P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P }} -∗ True. Proof. `````` Ralf Jung committed Jun 14, 2018 627 `````` iIntros "HP". Show. Undo. iIntros "?". Show. `````` Ralf Jung committed Jun 06, 2018 628 ``````Abort. `````` Ralf Jung committed Jun 06, 2018 629 `````` `````` Ralf Jung committed Jul 04, 2018 630 ``````Check "long_impl". `````` Ralf Jung committed Jun 06, 2018 631 632 633 634 635 ``````Lemma long_impl (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) : (PPPPPPPPPPPPPPPPP → (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ))%I. Proof. iStartProof. Show. Abort. `````` Ralf Jung committed Jul 04, 2018 636 ``````Check "long_impl_nested". `````` Ralf Jung committed Jun 06, 2018 637 638 639 640 641 ``````Lemma long_impl_nested (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) : (PPPPPPPPPPPPPPPPP → (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ) → (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ))%I. Proof. iStartProof. Show. Abort. `````` Ralf Jung committed Jul 04, 2018 642 ``````Check "long_wand". `````` Ralf Jung committed Jun 06, 2018 643 644 645 646 647 ``````Lemma long_wand (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) : (PPPPPPPPPPPPPPPPP -∗ (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ))%I. Proof. iStartProof. Show. Abort. `````` Ralf Jung committed Jul 04, 2018 648 ``````Check "long_wand_nested". `````` Ralf Jung committed Jun 06, 2018 649 650 651 652 653 ``````Lemma long_wand_nested (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) : (PPPPPPPPPPPPPPPPP -∗ (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ) -∗ (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ))%I. Proof. iStartProof. Show. Abort. `````` Ralf Jung committed Jul 04, 2018 654 ``````Check "long_fupd". `````` Ralf Jung committed Jun 06, 2018 655 656 657 658 659 ``````Lemma long_fupd E (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) : PPPPPPPPPPPPPPPPP ={E}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ. Proof. iStartProof. Show. Abort. `````` Ralf Jung committed Jul 04, 2018 660 ``````Check "long_fupd_nested". `````` Ralf Jung committed Jun 06, 2018 661 662 663 ``````Lemma long_fupd_nested E1 E2 (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) : PPPPPPPPPPPPPPPPP ={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ. `````` Ralf Jung committed Jun 06, 2018 664 665 666 ``````Proof. iStartProof. Show. Abort. `````` Ralf Jung committed Jun 06, 2018 667 668 669 ``````End linebreaks. End printing_tests. `````` Ralf Jung committed Jun 14, 2018 670 671 672 673 674 675 `````` (** Test error messages *) Section error_tests. Context {PROP : sbi}. Implicit Types P Q R : PROP. `````` Ralf Jung committed Jun 15, 2018 676 ``````Check "iAlways_spatial_non_empty". `````` Ralf Jung committed Jun 14, 2018 677 678 679 680 ``````Lemma iAlways_spatial_non_empty P : P -∗ □ emp. Proof. iIntros "HP". Fail iAlways. Abort. `````` Ralf Jung committed Jun 15, 2018 681 ``````Check "iDestruct_bad_name". `````` Ralf Jung committed Jun 14, 2018 682 683 684 685 ``````Lemma iDestruct_bad_name P : P -∗ P. Proof. iIntros "HP". Fail iDestruct "HQ" as "HP". Abort. `````` Ralf Jung committed Jun 15, 2018 686 ``````Check "iIntros_dup_name". `````` Ralf Jung committed Jun 15, 2018 687 688 689 690 691 692 ``````Lemma iIntros_dup_name P Q : P -∗ Q -∗ ∀ x y : (), P. Proof. iIntros "HP". Fail iIntros "HP". iIntros "HQ" (x). Fail iIntros (x). Abort. `````` Ralf Jung committed Jun 14, 2018 693 `````` `````` Ralf Jung committed Jun 15, 2018 694 ``````Check "iSplit_one_of_many". `````` Ralf Jung committed Jun 14, 2018 695 696 697 698 699 700 ``````Lemma iSplit_one_of_many P : P -∗ P -∗ P ∗ P. Proof. iIntros "HP1 HP2". Fail iSplitL "HP1 HPx". Fail iSplitL "HPx HP1". Abort. `````` Ralf Jung committed Jun 15, 2018 701 702 703 ``````Check "iExact_fail". Lemma iExact_fail P Q : P -∗ Q -∗ P. `````` Ralf Jung committed Jun 15, 2018 704 ``````Proof. `````` Ralf Jung committed Jun 15, 2018 705 `````` iIntros "HP". Fail iExact "HQ". iIntros "HQ". Fail iExact "HQ". Fail iExact "HP". `````` Ralf Jung committed Jun 15, 2018 706 707 ``````Abort. `````` Ralf Jung committed Jun 15, 2018 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 ``````Check "iClear_fail". Lemma iClear_fail P : P -∗ P. Proof. Fail iClear "HP". iIntros "HP". Fail iClear "HP". Abort. Check "iSpecializeArgs_fail". Lemma iSpecializeArgs_fail P : (∀ x : nat, P) -∗ P. Proof. iIntros "HP". Fail iSpecialize ("HP" \$! true). Abort. Check "iStartProof_fail". Lemma iStartProof_fail : 0 = 0. Proof. Fail iStartProof. Abort. Check "iPoseProof_fail". Lemma iPoseProof_fail P : P -∗ P. Proof. Fail iPoseProof (eq_refl 0) as "H". iIntros "H". Fail iPoseProof bi.and_intro as "H". Abort. Check "iRevert_fail". Lemma iRevert_fail P : P -∗ P. Proof. Fail iRevert "H". Abort. Check "iDestruct_fail". Lemma iDestruct_fail P : P -∗ P. Proof. iIntros "HP". Fail iDestruct "HP" as "{HP}". Fail iDestruct "HP" as "[{HP}]". Abort. `````` Ralf Jung committed Jun 16, 2018 736 737 738 739 ``````Check "iApply_fail". Lemma iApply_fail P Q : P -∗ Q. Proof. iIntros "HP". Fail iApply "HP". Abort. `````` Ralf Jung committed Jun 14, 2018 740 ``End error_tests.``