proofmode.v 30.3 KB
Newer Older
1
From iris.proofmode Require Import tactics intro_patterns.
2
Set Ltac Backtrace.
3
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
4

Ralf Jung's avatar
Ralf Jung committed
5
Section tests.
Robbert Krebbers's avatar
Robbert Krebbers committed
6 7
Context {PROP : sbi}.
Implicit Types P Q R : PROP.
8

Ralf Jung's avatar
Ralf Jung committed
9
Check "demo_0".
10
Lemma demo_0 P Q :  (P  Q) - ( x, x = 0  x = 1)  (Q  P).
11
Proof.
12
  iIntros "H #H2". Show. iDestruct "H" as "###H".
13
  (* should remove the disjunction "H" *)
14
  iDestruct "H" as "[#?|#?]"; last by iLeft. Show.
15 16 17 18
  (* should keep the disjunction "H" because it is instantiated *)
  iDestruct ("H2" $! 10) as "[%|%]". done. done.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
19 20
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 -
21 22
    P1 - (True  True) -
  (((P2  False  P2  0 = 0)  P3)  Q  P1  True) 
23
     (P2  False)  (False  P5 0).
Robbert Krebbers's avatar
Robbert Krebbers committed
24 25 26 27 28 29 30 31 32
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's avatar
Robbert Krebbers committed
33 34
  - iFrame "H3". iRight. auto.
  - iSplitL "HQ". iAssumption. by iSplitL "H1".
Robbert Krebbers's avatar
Robbert Krebbers committed
35 36
Qed.

37
Lemma demo_3 P1 P2 P3 :
Robbert Krebbers's avatar
Robbert Krebbers committed
38 39
  P1  P2  P3 - P1   (P2   x, (P3  x = 0)  P3).
Proof. iIntros "($ & $ & $)". iNext. by iExists 0. Qed.
40

Robbert Krebbers's avatar
Robbert Krebbers committed
41 42
Definition foo (P : PROP) := (P - P)%I.
Definition bar : PROP := ( P, foo P)%I.
43

Robbert Krebbers's avatar
Robbert Krebbers committed
44 45
Lemma test_unfold_constants : bar.
Proof. iIntros (P) "HP //". Qed.
46

47 48 49
Lemma test_iStopProof Q : emp - Q - Q.
Proof. iIntros "#H1 H2". iStopProof. by rewrite bi.sep_elim_r. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
50
Lemma test_iRewrite {A : ofeT} (x y : A) P :
51
   ( z, P - <affine> (z  y)) - (P - P  (x,x)  (y,x)).
52
Proof.
53
  iIntros "#H1 H2".
Robbert Krebbers's avatar
Robbert Krebbers committed
54
  iRewrite (bi.internal_eq_sym x x with "[# //]").
55
  iRewrite -("H1" $! _ with "[- //]").
Robbert Krebbers's avatar
Robbert Krebbers committed
56
  auto.
57 58
Qed.

Ralf Jung's avatar
Ralf Jung committed
59
Check "test_iDestruct_and_emp".
60
Lemma test_iDestruct_and_emp P Q `{!Persistent P, !Persistent Q} :
61
  P  emp - emp  Q - <affine> (P  Q).
Ralf Jung's avatar
Ralf Jung committed
62
Proof. iIntros "[#? _] [_ #?]". Show. auto. Qed.
63 64

Lemma test_iIntros_persistent P Q `{!Persistent Q} : (P  Q  P  Q)%I.
65
Proof. iIntros "H1 #H2". by iFrame "∗#". Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
66

Robbert Krebbers's avatar
Robbert Krebbers committed
67 68 69 70 71 72 73 74
Lemma test_iDestruct_intuitionistic_1 P Q `{!Persistent P}:
  Q   (Q - P) - P  Q.
Proof. iIntros "[HQ #HQP]". iDestruct ("HQP" with "HQ") as "#HP". by iFrame. Qed.

Lemma test_iDestruct_intuitionistic_2 P Q `{!Persistent P, !Affine P}:
  Q  (Q - P) - P.
Proof. iIntros "[HQ HQP]". iDestruct ("HQP" with "HQ") as "#HP". done. Qed.

75
Lemma test_iDestruct_intuitionistic_affine_bi `{!BiAffine PROP} P Q `{!Persistent P}:
Robbert Krebbers's avatar
Robbert Krebbers committed
76 77 78
  Q  (Q - P) - P  Q.
Proof. iIntros "[HQ HQP]". iDestruct ("HQP" with "HQ") as "#HP". by iFrame. Qed.

79 80 81
Lemma test_iIntros_pure (ψ φ : Prop) P : ψ  ( φ   P   φ  ψ   P)%I.
Proof. iIntros (??) "H". auto. Qed.

82 83 84
Lemma test_iIntros_pure_not : ( ¬False  : PROP)%I.
Proof. by iIntros (?). Qed.

85
Lemma test_fast_iIntros P Q :
86 87
  ( x y z : nat,
    x = plus 0 x  y = 0  z = 0  P   Q  foo (x  x))%I.
88
Proof.
89
  iIntros (a) "*".
90
  iIntros "#Hfoo **".
Robbert Krebbers's avatar
Robbert Krebbers committed
91
  iIntros "_ //".
92
Qed.
93

94
Lemma test_very_fast_iIntros P :
Robbert Krebbers's avatar
Robbert Krebbers committed
95
   x y : nat, ( x = y   P - P)%I.
96 97
Proof. by iIntros. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
98 99 100 101 102
(** 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.

103 104 105
Lemma test_iAssumption_affine P Q R `{!Affine P, !Affine R} : P - Q - R - Q.
Proof. iIntros "H1 H2 H3". iAssumption. Qed.

106 107 108
Lemma test_done_goal_evar Q :  P, Q  P.
Proof. eexists. iIntros "H". Fail done. iAssumption. Qed.

109
Lemma test_iDestruct_spatial_and P Q1 Q2 : P  (Q1  Q2) - P  Q1.
110
Proof. iIntros "[H [? _]]". by iFrame. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
111

112
Lemma test_iAssert_persistent P Q : P - Q - True.
Robbert Krebbers's avatar
Robbert Krebbers committed
113 114 115 116 117 118 119 120
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.
121

122 123 124 125 126
Lemma test_iAssert_persistently P :  P - True.
Proof.
  iIntros "HP". iAssert ( P)%I with "[# //]" as "#H". done.
Qed.

127
Lemma test_iSpecialize_auto_frame P Q R :
128
  (P - True - True - Q - R) - P - Q - R.
129
Proof. iIntros "H ? HQ". by iApply ("H" with "[$]"). Qed.
130

131 132 133 134
Lemma test_iSpecialize_pure (φ : Prop) Q R:
  φ  (⌜φ⌝ - Q)  Q.
Proof. iIntros (HP HPQ). iDestruct (HPQ $! HP) as "?". done. Qed.

135 136 137 138
Lemma test_iSpecialize_Coq_entailment P Q R :
  P  (P - Q)  Q.
Proof. iIntros (HP HPQ). iDestruct (HPQ $! HP) as "?". done. Qed.

139 140 141 142
Lemma test_iPure_intro_emp R `{!Affine R} :
  R - emp.
Proof. iIntros "HR". by iPureIntro. Qed.

143 144 145 146
Lemma test_iEmp_intro P Q R `{!Affine P, !Persistent Q, !Affine R} :
  P - Q  R - emp.
Proof. iIntros "HP #HQ HR". iEmpIntro. Qed.

147 148 149 150 151 152 153
Lemma test_iPure_intro (φ : nat  Prop) P Q R `{!Affine P, !Persistent Q, !Affine R} :
  φ 0  P - Q  R -  x : nat, <affine>  φ x    φ x .
Proof. iIntros (?) "HP #HQ HR". iPureIntro; eauto. Qed.
Lemma test_iPure_intro_2 (φ : nat  Prop) P Q R `{!Persistent Q} :
  φ 0  P - Q  R -  x : nat, <affine>  φ x    φ x .
Proof. iIntros (?) "HP #HQ HR". iPureIntro; eauto. Qed.

Ralf Jung's avatar
Ralf Jung committed
154
Lemma test_fresh P Q:
155 156 157 158 159 160 161 162 163 164
  (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.

165
(* Check coercions *)
Robbert Krebbers's avatar
Robbert Krebbers committed
166
Lemma test_iExist_coercion (P : Z  PROP) : ( x, P x) -  x, P x.
167
Proof. iIntros "HP". iExists (0:nat). iApply ("HP" $! (0:nat)). Qed.
168

Robbert Krebbers's avatar
Robbert Krebbers committed
169
Lemma test_iExist_tc `{Set_ A C} P : ( x1 x2 : gset positive, P - P)%I.
170 171 172
Proof. iExists {[ 1%positive ]}, . auto. Qed.

Lemma test_iSpecialize_tc P : ( x y z : gset positive, P) - P.
173 174
Proof.
  iIntros "H".
Ralf Jung's avatar
Ralf Jung committed
175
  (* FIXME: this [unshelve] and [apply _] should not be needed. *)
176 177
  unshelve iSpecialize ("H" $!  {[ 1%positive ]} ); try apply _. done.
Qed.
178

Robbert Krebbers's avatar
Robbert Krebbers committed
179
Lemma test_iFrame_pure {A : ofeT} (φ : Prop) (y z : A) :
180
  φ  <affine> y  z - ( φ    φ   y  z : PROP).
Robbert Krebbers's avatar
Robbert Krebbers committed
181 182
Proof. iIntros (Hv) "#Hxy". iFrame (Hv) "Hxy". Qed.

183 184 185 186 187 188 189 190 191 192 193 194 195 196
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.

197
Lemma test_iFrame_later `{!BiAffine PROP} P Q : P - Q -  P  Q.
198 199
Proof. iIntros "H1 H2". by iFrame "H1". Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
200 201 202
Lemma test_iAssert_modality P :  False -  P.
Proof.
  iIntros "HF".
203
  iAssert (<affine> False)%I with "[> -]" as %[].
Robbert Krebbers's avatar
Robbert Krebbers committed
204 205
  by iMod "HF".
Qed.
206

207
Lemma test_iMod_affinely_timeless P `{!Timeless P} :
208
  <affine>  P -  <affine> P.
209 210
Proof. iIntros "H". iMod "H". done. Qed.

211
Lemma test_iAssumption_False P : False - P.
212
Proof. iIntros "H". done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
213 214

(* Check instantiation and dependent types *)
Robbert Krebbers's avatar
Robbert Krebbers committed
215
Lemma test_iSpecialize_dependent_type (P :  n, vec nat n  PROP) :
Robbert Krebbers's avatar
Robbert Krebbers committed
216 217 218 219 220
  ( n v, P n v) -  n v, P n v.
Proof.
  iIntros "H". iExists _, [#10].
  iSpecialize ("H" $! _ [#10]). done.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
221

222 223 224 225 226
(* 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".
227
  iDestruct (big_sepL_elem_of _ _ _ Hp with "HT") as "Hp".
228 229 230
  done.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
231 232
Lemma test_eauto_iFrame P Q R `{!Persistent R} :
  P - Q - R  R  Q  P  R  False.
233
Proof. eauto 10 with iFrame. Qed.
234

235
Lemma test_iCombine_persistent P Q R `{!Persistent R} :
Robbert Krebbers's avatar
Robbert Krebbers committed
236
  P - Q - R  R  Q  P  R  False.
237
Proof. iIntros "HP HQ #HR". iCombine "HR HQ HP HR" as "H". auto. Qed.
Ralf Jung's avatar
Ralf Jung committed
238

239 240 241 242
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.

243
Lemma test_iNext_evar P : P - True.
Ralf Jung's avatar
Ralf Jung committed
244 245 246 247
Proof.
  iIntros "HP". iAssert ( _ -  P)%I as "?"; last done.
  iIntros "?". iNext. iAssumption.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
248

249 250
Lemma test_iNext_sep1 P Q (R1 := (P  Q)%I) :
  ( P   Q)  R1 -  ((P  Q)  R1).
Robbert Krebbers's avatar
Robbert Krebbers committed
251 252 253 254
Proof.
  iIntros "H". iNext.
  rewrite {1 2}(lock R1). (* check whether R1 has not been unfolded *) done.
Qed.
255

256
Lemma test_iNext_sep2 P Q :  P   Q -  (P  Q).
257 258 259
Proof.
  iIntros "H". iNext. iExact "H". (* Check that the laters are all gone. *)
Qed.
260

Robbert Krebbers's avatar
Robbert Krebbers committed
261
Lemma test_iNext_quantifier {A} (Φ : A  A  PROP) :
Robbert Krebbers's avatar
Robbert Krebbers committed
262 263 264
  ( y,  x,  Φ x y) -  ( y,  x, Φ x y).
Proof. iIntros "H". iNext. done. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
265
Lemma test_iFrame_persistent (P Q : PROP) :
266
   P - Q - <pers> (P  P)  (P  Q  Q).
267
Proof. iIntros "#HP". iFrame "HP". iIntros "$". Qed.
268

269
Lemma test_iSplit_persistently P Q :  P - <pers> (P  P).
270
Proof. iIntros "#?". by iSplit. Qed.
Ralf Jung's avatar
Ralf Jung committed
271

272
Lemma test_iSpecialize_persistent P Q :  P - (<pers> P  Q) - Q.
273
Proof. iIntros "#HP HPQ". by iSpecialize ("HPQ" with "HP"). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
274

275
Lemma test_iDestruct_persistent P (Φ : nat  PROP) `{! x, Persistent (Φ x)}:
276
   (P -  x, Φ x) -
277 278 279 280 281
  P -  x, Φ x  P.
Proof.
  iIntros "#H HP". iDestruct ("H" with "HP") as (x) "#H2". eauto with iFrame.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
282 283 284 285 286
Lemma test_iLöb P : ( n, ^n P)%I.
Proof.
  iLöb as "IH". iDestruct "IH" as (n) "IH".
  by iExists (S n).
Qed.
287

288
Lemma test_iInduction_wf (x : nat) P Q :
289
   P - Q -  (x + 0 = x)%nat .
290 291 292 293 294 295
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.

296 297 298 299 300 301 302 303 304
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.

305
Lemma test_iIntros_start_proof :
Robbert Krebbers's avatar
Robbert Krebbers committed
306
  (True : PROP)%I.
307 308 309 310 311
Proof.
  (* Make sure iIntros actually makes progress and enters the proofmode. *)
  progress iIntros. done.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
312
Lemma test_True_intros : (True : PROP) - True.
313 314 315
Proof.
  iIntros "?". done.
Qed.
316 317 318 319 320 321 322 323 324 325

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's avatar
Robbert Krebbers committed
326 327
   Q, let R := emp%I in P - R - Q - P  Q.
Proof. iIntros (Q R) "$ _ $". Qed.
328

329
Lemma test_iNext_iRewrite P Q : <affine>  (Q  P) - <affine>  Q - <affine>  P.
330
Proof.
331
  iIntros "#HPQ HQ !#". iNext. by iRewrite "HPQ" in "HQ".
332 333
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
334
Lemma test_iIntros_modalities `(!Absorbing P) :
335
  (<pers> (   x : nat,  x = 0    x = 0  - False - P - P))%I.
336 337 338 339 340
Proof.
  iIntros (x ??).
  iIntros "* **". (* Test that fast intros do not work under modalities *)
  iIntros ([]).
Qed.
341

342 343 344
Lemma test_iIntros_rewrite P (x1 x2 x3 x4 : nat) :
  x1 = x2  ( x2 = x3    x3  x4   P) -  x1 = x4   P.
Proof. iIntros (?) "(-> & -> & $)"; auto. Qed.
345

346
Lemma test_iNext_affine P Q : <affine>  (Q  P) - <affine>  Q - <affine>  P.
347 348
Proof. iIntros "#HPQ HQ !#". iNext. by iRewrite "HPQ" in "HQ". Qed.

349
Lemma test_iAlways P Q R :
350
   P - <pers> Q  R - <pers> <affine> <affine> P   Q.
351
Proof. iIntros "#HP #HQ HR". iSplitL. iAlways. done. iAlways. done. Qed.
352

Robbert Krebbers's avatar
Robbert Krebbers committed
353 354 355
(* A bunch of test cases from #127 to establish that tactics behave the same on
`⌜ φ ⌝ → P` and `∀ _ : φ, P` *)
Lemma test_forall_nondep_1 (φ : Prop) :
356
  φ  ( _ : φ, False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
357 358
Proof. iIntros (Hφ) "Hφ". by iApply "Hφ". Qed.
Lemma test_forall_nondep_2 (φ : Prop) :
359
  φ  ( _ : φ, False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
360 361
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" with "[% //]"). done. Qed.
Lemma test_forall_nondep_3 (φ : Prop) :
362
  φ  ( _ : φ, False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
363 364
Proof. iIntros (Hφ) "Hφ". unshelve iSpecialize ("Hφ" $! _). done. done. Qed.
Lemma test_forall_nondep_4 (φ : Prop) :
365
  φ  ( _ : φ, False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
366 367 368
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" $! Hφ); done. Qed.

Lemma test_pure_impl_1 (φ : Prop) :
369
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
370 371
Proof. iIntros (Hφ) "Hφ". by iApply "Hφ". Qed.
Lemma test_pure_impl_2 (φ : Prop) :
372
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
373 374
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" with "[% //]"). done. Qed.
Lemma test_pure_impl_3 (φ : Prop) :
375
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
376 377
Proof. iIntros (Hφ) "Hφ". unshelve iSpecialize ("Hφ" $! _). done. done. Qed.
Lemma test_pure_impl_4 (φ : Prop) :
378
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
379 380 381
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" $! Hφ). done. Qed.

Lemma test_forall_nondep_impl2 (φ : Prop) P :
382
  φ  P - ( _ : φ, P - False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
383 384 385 386 387 388 389
Proof.
  iIntros (Hφ) "HP Hφ".
  Fail iSpecialize ("Hφ" with "HP").
  iSpecialize ("Hφ" with "[% //] HP"). done.
Qed.

Lemma test_pure_impl2 (φ : Prop) P :
390
  φ  P - (⌜φ⌝  P - False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
391 392 393 394 395 396
Proof.
  iIntros (Hφ) "HP Hφ".
  Fail iSpecialize ("Hφ" with "HP").
  iSpecialize ("Hφ" with "[% //] HP"). done.
Qed.

397 398 399 400 401
Lemma demo_laterN_forall {A} (Φ Ψ: A  PROP) n: ( x, ^n Φ x) - ^n ( x, Φ x).
Proof.
  iIntros "H" (w). iApply ("H" $! w).
Qed.

402
Lemma test_iNext_laterN_later P n :  ^n P - ^n  P.
403
Proof. iIntros "H". iNext. by iNext. Qed.
404
Lemma test_iNext_later_laterN P n : ^n  P -  ^n P.
405
Proof. iIntros "H". iNext. by iNext. Qed.
406
Lemma test_iNext_plus_1 P n1 n2 :  ^n1 ^n2 P - ^n1 ^n2  P.
407
Proof. iIntros "H". iNext. iNext. by iNext. Qed.
408 409
Lemma test_iNext_plus_2 P n m : ^n ^m P - ^(n+m) P.
Proof. iIntros "H". iNext. done. Qed.
Ralf Jung's avatar
Ralf Jung committed
410
Check "test_iNext_plus_3".
411 412
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).
413
Proof. iIntros "H1 H2". iNext. iNext. iNext. iFrame. Show. iModIntro. done. Qed.
414

415 416 417 418 419 420 421 422
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.

423 424 425
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.
426 427

Lemma test_specialize_affine_pure (φ : Prop) P :
428
  φ  (<affine> ⌜φ⌝ - P)  P.
429 430 431 432 433
Proof.
  iIntros (Hφ) "H". by iSpecialize ("H" with "[% //]").
Qed.

Lemma test_assert_affine_pure (φ : Prop) P :
434 435
  φ  P  P  <affine> ⌜φ⌝.
Proof. iIntros (Hφ). iAssert (<affine> ⌜φ⌝)%I with "[%]" as "$"; auto. Qed.
436 437
Lemma test_assert_pure (φ : Prop) P :
  φ  P  P  ⌜φ⌝.
438
Proof. iIntros (Hφ). iAssert ⌜φ⌝%I with "[%]" as "$"; auto with iFrame. Qed.
439

440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478
Lemma test_specialize_very_nested (φ : Prop) P P2 Q R1 R2 :
  φ 
  P - P2 -
  (<affine>  φ  - P2 - Q) -
  (P - Q - R1) -
  (R1 - True - R2) -
  R2.
Proof.
  iIntros (?) "HP HP2 HQ H1 H2".
  by iApply ("H2" with "(H1 HP (HQ [% //] [-])) [//]").
Qed.

Lemma test_specialize_very_very_nested P1 P2 P3 P4 P5 :
   P1 -
   (P1 - P2) -
  (P2 - P2 - P3) -
  (P3 - P4) -
  (P4 - P5) -
  P5.
Proof.
  iIntros "#H #H1 H2 H3 H4".
  by iSpecialize ("H4" with "(H3 (H2 (H1 H) (H1 H)))").
Qed.

Check "test_specialize_nested_intuitionistic".
Lemma test_specialize_nested_intuitionistic (φ : Prop) P P2 Q R1 R2 :
  φ 
   P -  (P - Q) - (Q - Q - R2) - R2.
Proof.
  iIntros (?) "#HP #HQ HR".
  iSpecialize ("HR" with "(HQ HP) (HQ HP)").
  Show.
  done.
Qed.

Lemma test_specialize_intuitionistic P Q :
   P -  (P - Q) -  Q.
Proof. iIntros "#HP #HQ". iSpecialize ("HQ" with "HP"). done. Qed.

479
Lemma test_iEval x y :  (y + x)%nat = 1  -  S (x + y) = 2%nat  : PROP.
480 481 482 483 484 485
Proof.
  iIntros (H).
  iEval (rewrite (Nat.add_comm x y) // H).
  done.
Qed.

486 487 488 489 490 491 492
Lemma test_iEval_precedence : True  True : PROP.
Proof.
  iIntros.
  (* Ensure that in [iEval (a); b], b is not parsed as part of the argument of [iEval]. *)
  iEval (rewrite /=); iPureIntro; exact I.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
493 494 495 496
Check "test_iSimpl_in".
Lemma test_iSimpl_in x y :  (3 + x)%nat = y  -  S (S (S x)) = y  : PROP.
Proof. iIntros "H". iSimpl in "H". Show. done. Qed.

497 498 499 500 501
Lemma test_iSimpl_in_2 x y z :
   (3 + x)%nat = y  -  (1 + y)%nat = z  -
   S (S (S x)) = y  : PROP.
Proof. iIntros "H1 H2". iSimpl in "H1 H2". Show. done. Qed.

502 503 504 505 506
Lemma test_iSimpl_in3 x y z :
   (3 + x)%nat = y  -  (1 + y)%nat = z  -
   S (S (S x)) = y  : PROP.
Proof. iIntros "#H1 H2". iSimpl in "#". Show. done. Qed.

Dan Frumin's avatar
Dan Frumin committed
507 508 509 510
Check "test_iSimpl_in4".
Lemma test_iSimpl_in4 x y :  (3 + x)%nat = y  -  S (S (S x)) = y  : PROP.
Proof. iIntros "H". Fail iSimpl in "%". by iSimpl in "H". Qed.

511
Lemma test_iIntros_pure_neg : ( ¬False  : PROP)%I.
512
Proof. by iIntros (?). Qed.
513

514 515 516 517
Lemma test_iPureIntro_absorbing (φ : Prop) :
  φ  sbi_emp_valid (PROP:=PROP) (<absorb> ⌜φ⌝)%I.
Proof. intros ?. iPureIntro. done. Qed.

Ralf Jung's avatar
Ralf Jung committed
518
Check "test_iFrame_later_1".
519
Lemma test_iFrame_later_1 P Q : P   Q -  (P   Q).
520
Proof. iIntros "H". iFrame "H". Show. auto. Qed.
521

Ralf Jung's avatar
Ralf Jung committed
522
Check "test_iFrame_later_2".
523
Lemma test_iFrame_later_2 P Q :  P   Q -  ( P   Q).
524
Proof. iIntros "H". iFrame "H". Show. auto. Qed.
525 526 527 528 529

Lemma test_with_ident P Q R : P - Q - (P - Q - R) - R.
Proof.
  iIntros "? HQ H".
  iMatchHyp (fun H _ =>
530
    iApply ("H" with [spec_patterns.SIdent H []; spec_patterns.SIdent "HQ" []])).
531
Qed.
532 533

Lemma iFrame_with_evar_r P Q :
534
   R, (P - Q - P  R)  R = Q.
535
Proof.
536
  eexists. split. iIntros "HP HQ". iFrame. iApply "HQ". done.
537 538
Qed.
Lemma iFrame_with_evar_l P Q :
539
   R, (P - Q - R  P)  R = Q.
540
Proof.
541
  eexists. split. iIntros "HP HQ". Fail iFrame "HQ".
542
  iSplitR "HP"; iAssumption. done.
543
Qed.
544 545 546 547 548 549
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's avatar
Jacques-Henri Jourdan committed
550 551 552 553 554 555
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's avatar
Ralf Jung committed
556
Lemma test_iAssumption_evar P :  R, (R  P)  R = P.
557 558 559 560 561 562 563
Proof.
  eexists. split.
  - iIntros "H". iAssumption.
  (* Now verify that the evar was chosen as desired (i.e., it should not pick False). *)
  - reflexivity.
Qed.

564 565 566
Lemma test_iAssumption_False_no_loop :  R, R   P, P.
Proof. eexists. iIntros "?" (P). done. Qed.

567 568 569 570
Lemma test_apply_affine_impl `{!BiPlainly PROP} (P : PROP) :
  P - ( Q : PROP,  (Q - <pers> Q)   (P - Q)  Q).
Proof. iIntros "HP" (Q) "_ #HPQ". by iApply "HPQ". Qed.

Ralf Jung's avatar
Ralf Jung committed
571 572 573 574
Lemma test_apply_affine_wand `{!BiPlainly PROP} (P : PROP) :
  P - ( Q : PROP, <affine>  (Q - <pers> Q) - <affine>  (P - Q) - Q).
Proof. iIntros "HP" (Q) "_ #HPQ". by iApply "HPQ". Qed.

575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590
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.
591

Ralf Jung's avatar
Ralf Jung committed
592
Check "test_and_sep_affine_bi".
593
Lemma test_and_sep_affine_bi `{!BiAffine PROP} P Q :  P  Q   P  Q.
594
Proof.
595
  iIntros "[??]". iSplit; last done. Show. done.
596
Qed.
597

Ralf Jung's avatar
Ralf Jung committed
598
Check "test_big_sepL_simpl".
599
Lemma test_big_sepL_simpl x (l : list nat) P :
Robbert Krebbers's avatar
Robbert Krebbers committed
600
   P -
601 602 603
  ([ list] ky  l, <affine>  y = y ) -
  ([ list] y  x :: l, <affine>  y = y ) -
  P.
604
Proof. iIntros "HP ??". Show. simpl. Show. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
605

Ralf Jung's avatar
Ralf Jung committed
606
Check "test_big_sepL2_simpl".
Robbert Krebbers's avatar
Robbert Krebbers committed
607 608 609 610 611
Lemma test_big_sepL2_simpl x1 x2 (l1 l2 : list nat) P :
  P -
  ([ list] ky1;y2  []; l2, <affine>  y1 = y2 ) -
  ([ list] y1;y2  x1 :: l1; (x2 :: l2) ++ l2, <affine>  y1 = y2 ) -
  P  ([ list] y1;y2  x1 :: l1; x2 :: l2, True).
612
Proof. iIntros "HP ??". Show. simpl. Show. by iLeft. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
613

Ralf Jung's avatar
Ralf Jung committed
614
Check "test_big_sepL2_iDestruct".
Robbert Krebbers's avatar
Robbert Krebbers committed
615 616 617 618 619 620 621 622 623
Lemma test_big_sepL2_iDestruct (Φ : nat  nat  PROP) x1 x2 (l1 l2 : list nat) :
  ([ list] y1;y2  x1 :: l1; x2 :: l2, Φ y1 y2) -
  <absorb> Φ 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.
624 625 626 627

Lemma test_lemma_1 (b : bool) :
  emp @{PROP} ?b True.
Proof. destruct b; simpl; eauto. Qed.
Ralf Jung's avatar
Ralf Jung committed
628
Check "test_reducing_after_iDestruct".
629 630 631 632 633 634 635 636
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's avatar
Ralf Jung committed
637
Check "test_reducing_after_iApply".
638 639 640 641 642 643 644 645
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's avatar
Ralf Jung committed
646
Check "test_reducing_after_iApply_late_evar".
647 648 649 650 651 652
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's avatar
Ralf Jung committed
653
  Import proofmode.base.
Ralf Jung's avatar
Ralf Jung committed
654
  Check "test_wandM".
Ralf Jung's avatar
Ralf Jung committed
655 656 657 658 659 660 661
  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.
662 663
End wandM.

664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683
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.
684

685 686 687 688 689
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's avatar
Ralf Jung committed
690
End tests.
691 692 693 694 695

(** Test specifically if certain things print correctly. *)
Section printing_tests.
Context {PROP : sbi} `{!BiFUpd PROP}.
Implicit Types P Q R : PROP.
696 697 698 699 700

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.
701 702 703

(* Test line breaking of long assumptions. *)
Section linebreaks.
Ralf Jung's avatar
Ralf Jung committed
704 705
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) :
706 707 708 709
  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.
710
  iIntros "HP". Show. Undo. iIntros "?". Show.
711 712
Abort.

713
(* This is specifically crafted such that not having the printing box in
714 715 716
   the proofmode notation breaks the output. *)
Local Notation "'TESTNOTATION' '{{' P '|' Q '}' '}'" := (P  Q)%I
  (format "'TESTNOTATION'  '{{'  P  '|'  '/' Q  '}' '}'") : bi_scope.
Ralf Jung's avatar
Ralf Jung committed
717 718
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) :
719 720 721
  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.
722
  iIntros "HP". Show. Undo. iIntros "?". Show.
723
Abort.
724

Ralf Jung's avatar
Ralf Jung committed
725
Check "long_impl".
726 727 728 729 730
Lemma long_impl (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
  (PPPPPPPPPPPPPPPPP  (QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ))%I.
Proof.
  iStartProof. Show.
Abort.
Ralf Jung's avatar
Ralf Jung committed
731
Check "long_impl_nested".
732 733 734 735 736
Lemma long_impl_nested (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
  (PPPPPPPPPPPPPPPPP  (QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ)  (QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ))%I.
Proof.
  iStartProof. Show.
Abort.
Ralf Jung's avatar
Ralf Jung committed
737
Check "long_wand".
738 739 740 741 742
Lemma long_wand (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
  (PPPPPPPPPPPPPPPPP - (QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ))%I.
Proof.
  iStartProof. Show.
Abort.
Ralf Jung's avatar
Ralf Jung committed
743
Check "long_wand_nested".
744 745 746 747 748
Lemma long_wand_nested (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
  (PPPPPPPPPPPPPPPPP - (QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ) - (QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ))%I.
Proof.
  iStartProof. Show.
Abort.
Ralf Jung's avatar
Ralf Jung committed
749
Check "long_fupd".
750 751 752 753 754
Lemma long_fupd E (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
  PPPPPPPPPPPPPPPPP ={E}= QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ.
Proof.
  iStartProof. Show.
Abort.
Ralf Jung's avatar
Ralf Jung committed
755
Check "long_fupd_nested".
756 757 758
Lemma long_fupd_nested E1 E2 (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
  PPPPPPPPPPPPPPPPP ={E1,E2}= QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ
  ={E1,E2}= QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ.
759 760 761
Proof.
  iStartProof. Show.
Abort.
762 763 764
End linebreaks.

End printing_tests.
765 766 767 768 769 770

(** Test error messages *)
Section error_tests.
Context {PROP : sbi}.
Implicit Types P Q R : PROP.

771 772 773 774
Check "iStopProof_not_proofmode".
Lemma iStopProof_not_proofmode : 10 = 10.
Proof. Fail iStopProof. Abort.

775
Check "iAlways_spatial_non_empty".
776 777 778 779
Lemma iAlways_spatial_non_empty P :
  P -  emp.
Proof. iIntros "HP". Fail iAlways. Abort.

780
Check "iDestruct_bad_name".
781 782 783 784
Lemma iDestruct_bad_name P :
  P - P.
Proof. iIntros "HP". Fail iDestruct "HQ" as "HP". Abort.

785
Check "iIntros_dup_name".
786 787 788 789 790 791
Lemma iIntros_dup_name P Q :
  P - Q -  x y : (), P.
Proof.
  iIntros "HP". Fail iIntros "HP".
  iIntros "HQ" (x). Fail iIntros (x).
Abort.
792

793 794
Check "iSplitL_one_of_many".
Lemma iSplitL_one_of_many P :
795 796 797 798 799
  P - P - P  P.
Proof.
  iIntros "HP1 HP2". Fail iSplitL "HP1 HPx". Fail iSplitL "HPx HP1".
Abort.

800 801 802 803 804 805 806
Check "iSplitR_one_of_many".
Lemma iSplitR_one_of_many P :
  P - P - P  P.
Proof.
  iIntros "HP1 HP2". Fail iSplitR "HP1 HPx". Fail iSplitR "HPx HP1".
Abort.

807 808 809 810 811 812 813 814 815 816 817 818 819 820
Check "iSplitL_non_splittable".
Lemma iSplitL_non_splittable P :
  P.
Proof.
  Fail iSplitL "".
Abort.

Check "iSplitR_non_splittable".
Lemma iSplitR_non_splittable P :
  P.
Proof.
  Fail iSplitR "".
Abort.

821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841
Check "iCombine_fail".
Lemma iCombine_fail P:
  P - P - P  P.
Proof.
  iIntros "HP1 HP2". Fail iCombine "HP1 HP3" as "HP".
Abort.

Check "iSpecialize_bad_name1_fail".
Lemma iSpecialize_bad_name1_fail P Q:
  (P - Q) - P - Q.
Proof.
  iIntros "HW HP". Fail iSpecialize ("H" with "HP").
Abort.

Check "iSpecialize_bad_name2_fail".
Lemma iSpecialize_bad_name2_fail P Q:
  (P - Q) - P - Q.
Proof.
  iIntros "HW HP". Fail iSpecialize ("HW" with "H").
Abort.

842 843 844
Check "iExact_fail".
Lemma iExact_fail P Q :
  <affine> P - Q - <affine> P.
845
Proof.
846
  iIntros "HP". Fail iExact "HQ". iIntros "HQ". Fail iExact "HQ". Fail iExact "HP".
847 848
Abort.

849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868
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.

869 870 871 872 873 874
Check "iPoseProof_not_found_fail".
Lemma iPoseProof_not_found_fail P : P - P.
Proof.
  iIntros "H". Fail iPoseProof "Hx" as "H1".
Abort.

875 876 877 878 879 880
Check "iPoseProof_not_found_fail2".
Lemma iPoseProof_not_found_fail2 P Q (H: P - Q) : P - Q.
Proof.
  iIntros "HP". Fail iPoseProof (H with "[HQ]") as "H".
Abort.

881 882 883 884 885 886 887 888 889 890 891 892
Check "iPoseProofCoreHyp_not_found_fail".
Lemma iPoseProofCoreHyp_not_found_fail P : P - P - P.
Proof.
  iIntros "H". Fail iPoseProofCoreHyp "Hx" as "H1".
Abort.

Check "iPoseProofCoreHyp_not_fresh_fail".
Lemma iPoseProofCoreHyp_not_fresh_fail P : P - P - P.
Proof.
  iIntros "H0 H1". Fail iPoseProofCoreHyp "H0" as "H1".
Abort.

893 894 895 896 897 898 899 900
Check "iRevert_fail".
Lemma iRevert_fail P : P - P.
Proof. Fail iRevert "H". Abort.

Check "iDestruct_fail".
Lemma iDestruct_fail P : P - <absorb> P.
Proof. iIntros "HP". Fail iDestruct "HP" as "{HP}". Fail iDestruct "HP" as "[{HP}]". Abort.

901 902 903 904 905 906
Check "iOrDestruct_fail".
Lemma iOrDestruct_fail P : (P  P) - P - P.
Proof.
  iIntros "H H'". Fail iOrDestruct "H" as "H'" "H2". Fail iOrDestruct "H" as "H1" "H'".
Abort.

907 908 909 910
Check "iApply_fail".
Lemma iApply_fail P Q : P - Q.
Proof. iIntros "HP". Fail iApply "HP". Abort.

911 912 913 914 915 916 917
Check "iApply_fail_not_affine_1".
Lemma iApply_fail_not_affine_1 P Q : P - Q - Q.
Proof. iIntros "HP HQ". Fail iApply "HQ". Abort.

Check "iApply_fail_not_affine_2".
Lemma iApply_fail_not_affine_1 P Q R : P - R - (R - Q) - Q.
Proof. iIntros "HP HR HQ". Fail iApply ("HQ" with "HR"). Abort.
918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936

Check "iRevert_wrong_var".
Lemma iRevert_wrong_var (k : nat) (Φ : nat  PROP) : Φ (S k).
Proof.
  Fail iRevert (k1).
  Fail iLöb as "IH" forall (k1).
Abort.

Check "iRevert_dup_var".
Lemma iRevert_dup_var (k : nat) (Φ : nat  PROP) : Φ (S k).
Proof. Fail iRevert (k k). Abort.

Check "iRevert_dep_var_coq".
Lemma iRevert_dep_var_coq (k : nat) (Φ : nat  PROP) : k = 0  Φ (S k).
Proof. intros Hk. Fail iRevert (k). Abort.

Check "iRevert_dep_var".
Lemma iRevert_dep_var (k : nat) (Φ : nat  PROP) : Φ k - Φ (S k).
Proof. iIntros "Hk". Fail iRevert (k). Abort.
937
End error_tests.
Robbert Krebbers's avatar
Robbert Krebbers committed
938 939 940 941 942 943 944 945 946

Section error_tests_bi.
Context {PROP : bi}.
Implicit Types P Q R : PROP.

Check "iLöb_no_sbi".
Lemma iLöb_no_sbi P : P.
Proof. Fail iLöb as "IH". Abort.
End error_tests_bi.