proofmode.v 29.2 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.

Robbert Krebbers's avatar
Robbert Krebbers committed
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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
64
65
66
67
68
69
70
71
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.

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

76
77
78
Lemma test_iIntros_pure (ψ φ : Prop) P : ψ  ( φ   P   φ  ψ   P)%I.
Proof. iIntros (??) "H". auto. Qed.

79
80
81
Lemma test_iIntros_pure_not : ( ¬False  : PROP)%I.
Proof. by iIntros (?). Qed.

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
95
96
97
98
99
(** 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.

100
101
102
Lemma test_iAssumption_affine P Q R `{!Affine P, !Affine R} : P - Q - R - Q.
Proof. iIntros "H1 H2 H3". iAssumption. Qed.

103
104
105
Lemma test_done_goal_evar Q :  P, Q  P.
Proof. eexists. iIntros "H". Fail done. iAssumption. Qed.

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
124
Lemma test_iSpecialize_auto_frame P Q R :
125
  (P - True - True - Q - R) - P - Q - R.
126
Proof. iIntros "H ? HQ". by iApply ("H" with "[$]"). Qed.
127

Ralf Jung's avatar
Ralf Jung committed
128
129
130
131
Lemma test_iSpecialize_pure (φ : Prop) Q R:
  φ  (⌜φ⌝ - Q)  Q.
Proof. iIntros (HP HPQ). iDestruct (HPQ $! HP) as "?". done. Qed.

132
133
134
135
Lemma test_iSpecialize_Coq_entailment P Q R :
  P  (P - Q)  Q.
Proof. iIntros (HP HPQ). iDestruct (HPQ $! HP) as "?". done. Qed.

136
137
138
139
Lemma test_iPure_intro_emp R `{!Affine R} :
  R - emp.
Proof. iIntros "HR". by iPureIntro. Qed.

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

144
145
146
147
148
149
150
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
151
Lemma test_fresh P Q:
152
153
154
155
156
157
158
159
160
161
  (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.

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

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

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

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

180
181
182
183
184
185
186
187
188
189
190
191
192
193
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.

194
Lemma test_iFrame_later `{!BiAffine PROP} P Q : P - Q -  P  Q.
195
196
Proof. iIntros "H1 H2". by iFrame "H1". Qed.

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

204
Lemma test_iMod_affinely_timeless P `{!Timeless P} :
205
  <affine>  P -  <affine> P.
206
207
Proof. iIntros "H". iMod "H". done. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
208
Lemma test_iAssumption_False P : False - P.
209
Proof. iIntros "H". done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
210
211

(* Check instantiation and dependent types *)
Robbert Krebbers's avatar
Robbert Krebbers committed
212
Lemma test_iSpecialize_dependent_type (P :  n, vec nat n  PROP) :
Robbert Krebbers's avatar
Robbert Krebbers committed
213
214
215
216
217
  ( 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
218

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

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

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

236
237
238
239
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's avatar
Robbert Krebbers committed
240
Lemma test_iNext_evar P : P - True.
Ralf Jung's avatar
Ralf Jung committed
241
242
243
244
Proof.
  iIntros "HP". iAssert ( _ -  P)%I as "?"; last done.
  iIntros "?". iNext. iAssumption.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
245

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

Robbert Krebbers's avatar
Robbert Krebbers committed
253
Lemma test_iNext_sep2 P Q :  P   Q -  (P  Q).
254
255
256
Proof.
  iIntros "H". iNext. iExact "H". (* Check that the laters are all gone. *)
Qed.
257

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

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

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

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

272
Lemma test_iDestruct_persistent P (Φ : nat  PROP) `{! x, Persistent (Φ x)}:
273
   (P -  x, Φ x) -
274
275
276
277
278
  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
279
280
281
282
283
Lemma test_iLöb P : ( n, ^n P)%I.
Proof.
  iLöb as "IH". iDestruct "IH" as (n) "IH".
  by iExists (S n).
Qed.
284

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

293
294
295
296
297
298
299
300
301
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.

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

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

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
323
324
   Q, let R := emp%I in P - R - Q - P  Q.
Proof. iIntros (Q R) "$ _ $". Qed.
325

Robbert Krebbers's avatar
Robbert Krebbers committed
326
Lemma test_iNext_iRewrite P Q : <affine>  (Q  P) - <affine>  Q - <affine>  P.
327
Proof.
328
  iIntros "#HPQ HQ !#". iNext. by iRewrite "HPQ" in "HQ".
329
330
Qed.

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

339
340
341
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's avatar
Robbert Krebbers committed
342

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

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

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

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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
399
Lemma test_iNext_laterN_later P n :  ^n P - ^n  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
400
Proof. iIntros "H". iNext. by iNext. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
401
Lemma test_iNext_later_laterN P n : ^n  P -  ^n P.
Robbert Krebbers's avatar
Robbert Krebbers committed
402
Proof. iIntros "H". iNext. by iNext. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
403
Lemma test_iNext_plus_1 P n1 n2 :  ^n1 ^n2 P - ^n1 ^n2  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
404
Proof. iIntros "H". iNext. iNext. by iNext. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
405
406
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
407
Check "test_iNext_plus_3".
Robbert Krebbers's avatar
Robbert Krebbers committed
408
409
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).
410
Proof. iIntros "H1 H2". iNext. iNext. iNext. iFrame. Show. iModIntro. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
411

412
413
414
415
416
417
418
419
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.

420
421
422
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.
423
424

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

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

437
438
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
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.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
483
484
485
486
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.

487
488
489
490
491
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.

492
493
494
495
496
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
497
498
499
500
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.

501
Lemma test_iIntros_pure_neg : ( ¬False  : PROP)%I.
502
Proof. by iIntros (?). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
503

504
505
506
507
Lemma test_iPureIntro_absorbing (φ : Prop) :
  φ  sbi_emp_valid (PROP:=PROP) (<absorb> ⌜φ⌝)%I.
Proof. intros ?. iPureIntro. done. Qed.

Ralf Jung's avatar
Ralf Jung committed
508
Check "test_iFrame_later_1".
509
Lemma test_iFrame_later_1 P Q : P   Q -  (P   Q).
510
Proof. iIntros "H". iFrame "H". Show. auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
511

Ralf Jung's avatar
Ralf Jung committed
512
Check "test_iFrame_later_2".
513
Lemma test_iFrame_later_2 P Q :  P   Q -  ( P   Q).
514
Proof. iIntros "H". iFrame "H". Show. auto. Qed.
515
516
517
518
519

Lemma test_with_ident P Q R : P - Q - (P - Q - R) - R.
Proof.
  iIntros "? HQ H".
  iMatchHyp (fun H _ =>
520
    iApply ("H" with [spec_patterns.SIdent H []; spec_patterns.SIdent "HQ" []])).
521
Qed.
522
523

Lemma iFrame_with_evar_r P Q :
524
   R, (P - Q - P  R)  R = Q.
525
Proof.
526
  eexists. split. iIntros "HP HQ". iFrame. iApply "HQ". done.
527
528
Qed.
Lemma iFrame_with_evar_l P Q :
529
   R, (P - Q - R  P)  R = Q.
530
Proof.
531
  eexists. split. iIntros "HP HQ". Fail iFrame "HQ".
532
  iSplitR "HP"; iAssumption. done.
533
Qed.
534
535
536
537
538
539
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
540
541
542
543
544
545
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
546
Lemma test_iAssumption_evar P :  R, (R  P)  R = P.
547
548
549
550
551
552
553
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's avatar
Ralf Jung committed
554
555
556
Lemma test_iAssumption_False_no_loop :  R, R   P, P.
Proof. eexists. iIntros "?" (P). done. Qed.

557
558
559
560
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
561
562
563
564
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.

565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
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.
581

Ralf Jung's avatar
Ralf Jung committed
582
Check "test_and_sep_affine_bi".
583
Lemma test_and_sep_affine_bi `{!BiAffine PROP} P Q :  P  Q   P  Q.
584
Proof.
585
  iIntros "[??]". iSplit; last done. Show. done.
586
Qed.
587

Ralf Jung's avatar
Ralf Jung committed
588
Check "test_big_sepL_simpl".
589
Lemma test_big_sepL_simpl x (l : list nat) P :
Robbert Krebbers's avatar
Robbert Krebbers committed
590
   P -
591
592
593
  ([ list] ky  l, <affine>  y = y ) -
  ([ list] y  x :: l, <affine>  y = y ) -
  P.
594
Proof. iIntros "HP ??". Show. simpl. Show. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
595

Ralf Jung's avatar
Ralf Jung committed
596
Check "test_big_sepL2_simpl".
Robbert Krebbers's avatar
Robbert Krebbers committed
597
598
599
600
601
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).
602
Proof. iIntros "HP ??". Show. simpl. Show. by iLeft. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
603

Ralf Jung's avatar
Ralf Jung committed
604
Check "test_big_sepL2_iDestruct".
Robbert Krebbers's avatar
Robbert Krebbers committed
605
606
607
608
609
610
611
612
613
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.
614
615
616
617

Lemma test_lemma_1 (b : bool) :
  emp @{PROP} ?b True.
Proof. destruct b; simpl; eauto. Qed.
Ralf Jung's avatar
Ralf Jung committed
618
Check "test_reducing_after_iDestruct".
619
620
621
622
623
624
625
626
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
627
Check "test_reducing_after_iApply".
628
629
630
631
632
633
634
635
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
636
Check "test_reducing_after_iApply_late_evar".
637
638
639
640
641
642
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
643
  Import proofmode.base.
Ralf Jung's avatar
Ralf Jung committed
644
  Check "test_wandM".
Ralf Jung's avatar
Ralf Jung committed
645
646
647
648
649
650
651
  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.
652
653
End wandM.

654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
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.
674

675
676
677
678
679
680
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
681
End tests.
682
683
684
685
686

(** Test specifically if certain things print correctly. *)
Section printing_tests.
Context {PROP : sbi} `{!BiFUpd PROP}.
Implicit Types P Q R : PROP.
687
688
689
690
691

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.
692
693
694

(* Test line breaking of long assumptions. *)
Section linebreaks.
Ralf Jung's avatar
Ralf Jung committed
695
696
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) :
697
698
699
700
  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.
701
  iIntros "HP". Show. Undo. iIntros "?". Show.
702
703
Abort.

704
(* This is specifically crafted such that not having the printing box in
705
706
707
   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
708
709
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) :
710
711
712
  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.
713
  iIntros "HP". Show. Undo. iIntros "?". Show.
714
Abort.
715

Ralf Jung's avatar
Ralf Jung committed
716
Check "long_impl".
717
718
719
720
721
Lemma long_impl (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
  (PPPPPPPPPPPPPPPPP  (QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ))%I.
Proof.
  iStartProof. Show.
Abort.
Ralf Jung's avatar
Ralf Jung committed
722
Check "long_impl_nested".
723
724
725
726
727
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
728
Check "long_wand".
729
730
731
732
733
Lemma long_wand (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
  (PPPPPPPPPPPPPPPPP - (QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ))%I.
Proof.
  iStartProof. Show.
Abort.
Ralf Jung's avatar
Ralf Jung committed
734
Check "long_wand_nested".
735
736
737
738
739
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
740
Check "long_fupd".
741
742
743
744
745
Lemma long_fupd E (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
  PPPPPPPPPPPPPPPPP ={E}= QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ.
Proof.
  iStartProof. Show.
Abort.
Ralf Jung's avatar
Ralf Jung committed
746
Check "long_fupd_nested".
747
748
749
Lemma long_fupd_nested E1 E2 (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
  PPPPPPPPPPPPPPPPP ={E1,E2}= QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ
  ={E1,E2}= QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ.
750
751
752
Proof.
  iStartProof. Show.
Abort.
753
754
755
End linebreaks.

End printing_tests.
756
757
758
759
760
761

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

762
Check "iAlways_spatial_non_empty".
763
764
765
766
Lemma iAlways_spatial_non_empty P :
  P -  emp.
Proof. iIntros "HP". Fail iAlways. Abort.

767
Check "iDestruct_bad_name".
768
769
770
771
Lemma iDestruct_bad_name P :
  P - P.
Proof. iIntros "HP". Fail iDestruct "HQ" as "HP". Abort.

772
Check "iIntros_dup_name".
773
774
775
776
777
778
Lemma iIntros_dup_name P Q :
  P - Q -  x y : (), P.
Proof.
  iIntros "HP". Fail iIntros "HP".
  iIntros "HQ" (x). Fail iIntros (x).
Abort.
779

780
781
Check "iSplitL_one_of_many".
Lemma iSplitL_one_of_many P :
782
783
784
785
786
  P - P - P  P.
Proof.
  iIntros "HP1 HP2". Fail iSplitL "HP1 HPx". Fail iSplitL "HPx HP1".
Abort.

787
788
789
790
791
792
793
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.

794
795
796
797
798
799
800
801
802
803
804
805
806
807
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.

808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
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.

829
830
831
Check "iExact_fail".
Lemma iExact_fail P Q :
  <affine> P - Q - <affine> P.
832
Proof.
833
  iIntros "HP". Fail iExact "HQ". iIntros "HQ". Fail iExact "HQ". Fail iExact "HP".
834
835
Abort.

836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
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.

856
857
858
859
860
861
Check "iPoseProof_not_found_fail".
Lemma iPoseProof_not_found_fail P : P - P.
Proof.
  iIntros "H". Fail iPoseProof "Hx" as "H1".
Abort.

862
863
864
865
866
867
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.

868
869
870
871
872
873
874
875
876
877
878
879
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.

880
881
882
883
884
885
886
887
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.

888
889
890
891
892
893
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.

894
895
896
897
Check "iApply_fail".
Lemma iApply_fail P Q : P - Q.
Proof. iIntros "HP". Fail iApply "HP". Abort.

898
899
900
901
902
903
904
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.
905
End error_tests.