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

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

8
9
10
11
Lemma type_sbi_internal_eq_annot P :
  P @{PROP} P  (@{PROP}) P P  (P .) P  (. P) P.
Proof. done. Qed.

12
13
14
Lemma test_eauto_emp_isplit_biwand P : emp  P - P.
Proof. eauto 6. Qed.

Gregory Malecha's avatar
Gregory Malecha committed
15
Lemma test_eauto_isplit_biwand P :  P - P.
Paolo G. Giarrusso's avatar
Paolo G. Giarrusso committed
16
Proof. eauto. Qed.
17

Gregory Malecha's avatar
Gregory Malecha committed
18
Fixpoint test_fixpoint (n : nat) {struct n} : True  emp @{PROP}  (n + 0)%nat = n .
19
20
21
22
23
24
Proof.
  case: n => [|n] /=; first (iIntros (_) "_ !%"; reflexivity).
  iIntros (_) "_".
  by iDestruct (test_fixpoint with "[//]") as %->.
Qed.

Ralf Jung's avatar
Ralf Jung committed
25
Check "demo_0".
26
Lemma demo_0 P Q :  (P  Q) - ( x, x = 0  x = 1)  (Q  P).
27
Proof.
28
  iIntros "H #H2". Show. iDestruct "H" as "###H".
29
  (* should remove the disjunction "H" *)
30
  iDestruct "H" as "[#?|#?]"; last by iLeft. Show.
31
32
33
34
  (* should keep the disjunction "H" because it is instantiated *)
  iDestruct ("H2" $! 10) as "[%|%]". done. done.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
35
36
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 -
37
38
    P1 - (True  True) -
  (((P2  False  P2  0 = 0)  P3)  Q  P1  True) 
39
     (P2  False)  (False  P5 0).
Robbert Krebbers's avatar
Robbert Krebbers committed
40
41
42
43
44
45
46
47
48
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
49
50
  - iFrame "H3". iRight. auto.
  - iSplitL "HQ". iAssumption. by iSplitL "H1".
Robbert Krebbers's avatar
Robbert Krebbers committed
51
52
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
53
Lemma demo_3 P1 P2 P3 :
Robbert Krebbers's avatar
Robbert Krebbers committed
54
55
  P1  P2  P3 - P1   (P2   x, (P3  x = 0)  P3).
Proof. iIntros "($ & $ & $)". iNext. by iExists 0. Qed.
56

Robbert Krebbers's avatar
Robbert Krebbers committed
57
58
Definition foo (P : PROP) := (P - P)%I.
Definition bar : PROP := ( P, foo P)%I.
59

Gregory Malecha's avatar
Gregory Malecha committed
60
Lemma test_unfold_constants :  bar.
Robbert Krebbers's avatar
Robbert Krebbers committed
61
Proof. iIntros (P) "HP //". Qed.
62

Ralf Jung's avatar
Ralf Jung committed
63
Check "test_iStopProof".
Robbert Krebbers's avatar
Robbert Krebbers committed
64
Lemma test_iStopProof Q : emp - Q - Q.
Ralf Jung's avatar
Ralf Jung committed
65
Proof. iIntros "#H1 H2". Show. iStopProof. Show. by rewrite bi.sep_elim_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
66

Robbert Krebbers's avatar
Robbert Krebbers committed
67
Lemma test_iRewrite {A : ofeT} (x y : A) P :
68
   ( z, P - <affine> (z  y)) - (P - P  (x,x)  (y,x)).
69
Proof.
70
  iIntros "#H1 H2".
Robbert Krebbers's avatar
Robbert Krebbers committed
71
  iRewrite (bi.internal_eq_sym x x with "[# //]").
72
  iRewrite -("H1" $! _ with "[- //]").
Robbert Krebbers's avatar
Robbert Krebbers committed
73
  auto.
74
75
Qed.

Ralf Jung's avatar
Ralf Jung committed
76
Check "test_iDestruct_and_emp".
77
Lemma test_iDestruct_and_emp P Q `{!Persistent P, !Persistent Q} :
78
  P  emp - emp  Q - <affine> (P  Q).
Ralf Jung's avatar
Ralf Jung committed
79
Proof. iIntros "[#? _] [_ #?]". Show. auto. Qed.
80

Gregory Malecha's avatar
Gregory Malecha committed
81
Lemma test_iIntros_persistent P Q `{!Persistent Q} :  (P  Q  P  Q).
82
Proof. iIntros "H1 #H2". by iFrame "∗#". Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
83

Robbert Krebbers's avatar
Robbert Krebbers committed
84
85
86
87
88
89
90
91
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.

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

96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
Check "test_iDestruct_spatial".
Lemma test_iDestruct_spatial Q :  Q - Q.
Proof. iIntros "#HQ". iDestruct "HQ" as "-#HQ". Show. done. Qed.

Check "test_iDestruct_spatial_affine".
Lemma test_iDestruct_spatial_affine Q `{!Affine Q} :  Q - Q.
Proof.
  iIntros "#-#HQ".
  (* Since [Q] is affine, it should not add an <affine> modality *)
  Show. done.
Qed.

Lemma test_iDestruct_spatial_noop Q : Q - Q.
Proof. iIntros "-#HQ". done. Qed.

Gregory Malecha's avatar
Gregory Malecha committed
111
Lemma test_iIntros_pure (ψ φ : Prop) P : ψ    φ   P   φ  ψ   P.
112
113
Proof. iIntros (??) "H". auto. Qed.

Gregory Malecha's avatar
Gregory Malecha committed
114
Lemma test_iIntros_pure_not : @{PROP}  ¬False .
115
116
Proof. by iIntros (?). Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
117
Lemma test_fast_iIntros P Q :
Gregory Malecha's avatar
Gregory Malecha committed
118
119
    x y z : nat,
    x = plus 0 x  y = 0  z = 0  P   Q  foo (x  x).
120
Proof.
121
  iIntros (a) "*".
122
  iIntros "#Hfoo **".
Robbert Krebbers's avatar
Robbert Krebbers committed
123
  iIntros "_ //".
124
Qed.
125

126
Lemma test_very_fast_iIntros P :
Gregory Malecha's avatar
Gregory Malecha committed
127
   x y : nat,   x = y   P - P.
128
129
Proof. by iIntros. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
130
Definition tc_opaque_test : PROP := tc_opaque ( x : nat,  x = x )%I.
Gregory Malecha's avatar
Gregory Malecha committed
131
Lemma test_iIntros_tc_opaque :  tc_opaque_test.
Robbert Krebbers's avatar
Robbert Krebbers committed
132
Proof. by iIntros (x). Qed.
133

Robbert Krebbers's avatar
Robbert Krebbers committed
134
135
(** Prior to 0b84351c this used to loop, now [iAssumption] instantiates [R] with
[False] and performs false elimination. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
136
137
138
Lemma test_iAssumption_evar_ex_false :  R, R   P, P.
Proof. eexists. iIntros "?" (P). iAssumption. Qed.

139
140
141
Lemma test_iApply_evar P Q R : ( Q, Q - P) - R - P.
Proof. iIntros "H1 H2". iApply "H1". iExact "H2". Qed.

142
143
144
Lemma test_iAssumption_affine P Q R `{!Affine P, !Affine R} : P - Q - R - Q.
Proof. iIntros "H1 H2 H3". iAssumption. Qed.

145
146
147
Lemma test_done_goal_evar Q :  P, Q  P.
Proof. eexists. iIntros "H". Fail done. iAssumption. Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
151
Lemma test_iAssert_persistent P Q : P - Q - True.
Robbert Krebbers's avatar
Robbert Krebbers committed
152
153
154
155
156
157
158
159
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.
160

161
162
163
164
165
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
166
Lemma test_iSpecialize_auto_frame P Q R :
167
  (P - True - True - Q - R) - P - Q - R.
168
Proof. iIntros "H ? HQ". by iApply ("H" with "[$]"). Qed.
169

Gregory Malecha's avatar
Gregory Malecha committed
170
171
Lemma test_iSpecialize_pure (φ : Prop) Q R :
  φ  (⌜φ⌝ - Q)   Q.
Ralf Jung's avatar
Ralf Jung committed
172
173
Proof. iIntros (HP HPQ). iDestruct (HPQ $! HP) as "?". done. Qed.

174
Lemma test_iSpecialize_Coq_entailment P Q R :
Gregory Malecha's avatar
Gregory Malecha committed
175
  ( P)  (P - Q)  ( Q).
176
177
Proof. iIntros (HP HPQ). iDestruct (HPQ $! HP) as "?". done. Qed.

178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
Lemma test_iSpecialize_intuitionistic P Q R :
   P -  (P - P - P - P -  P - P - Q) - R - R   (P  Q).
Proof.
  iIntros "#HP #H HR".
  (* Test that [H] remains in the intuitionistic context *)
  iSpecialize ("H" with "HP").
  iSpecialize ("H" with "[HP]"); first done.
  iSpecialize ("H" with "[]"); first done.
  iSpecialize ("H" with "[-HR]"); first done.
  iSpecialize ("H" with "[#]"); first done.
  iFrame "HR".
  iSpecialize ("H" with "[-]"); first done.
  by iFrame "#".
Qed.

Lemma test_iSpecialize_intuitionistic_2 P Q R :
   P -  (P - P - P - P -  P - P - Q) - R - R   (P  Q).
Proof.
  iIntros "#HP #H HR".
  (* Test that [H] remains in the intuitionistic context *)
  iSpecialize ("H" with "HP") as #.
  iSpecialize ("H" with "[HP]") as #; first done.
  iSpecialize ("H" with "[]") as #; first done.
  iSpecialize ("H" with "[-HR]") as #; first done.
  iSpecialize ("H" with "[#]") as #; first done.
  iFrame "HR".
  iSpecialize ("H" with "[-]") as #; first done.
  by iFrame "#".
Qed.

Lemma test_iSpecialize_intuitionistic_3 P Q R :
  P -  (P - Q) -  (P - <pers> Q) -  (Q - R) - P   (Q  R).
Proof.
  iIntros "HP #H1 #H2 #H3".
  (* Should fail, [Q] is not persistent *)
  Fail iSpecialize ("H1" with "HP") as #.
  (* Should succeed, [<pers> Q] is persistent *)
  iSpecialize ("H2" with "HP") as #.
  (* Should succeed, despite [R] not being persistent, no spatial premises are
  needed to prove [Q] *)
  iSpecialize ("H3" with "H2") as #.
  by iFrame "#".
Qed.

Check "test_iAssert_intuitionistic".
Lemma test_iAssert_intuitionistic `{!BiBUpd PROP} P :
   P -  |==> P.
Proof.
  iIntros "#HP".
  (* Test that [HPupd1] ends up in the intuitionistic context *)
  iAssert (|==> P)%I with "[]" as "#HPupd1"; first done.
  (* This should not work, [|==> P] is not persistent. *)
  Fail iAssert (|==> P)%I with "[#]" as "#HPupd2"; first done.
  done.
Qed.

234
235
236
Lemma test_iSpecialize_evar P : ( R, R - R) - P - P.
Proof. iIntros "H HP". iApply ("H" with "[HP]"). done. Qed.

237
238
239
240
Lemma test_iPure_intro_emp R `{!Affine R} :
  R - emp.
Proof. iIntros "HR". by iPureIntro. Qed.

241
242
243
244
Lemma test_iEmp_intro P Q R `{!Affine P, !Persistent Q, !Affine R} :
  P - Q  R - emp.
Proof. iIntros "HP #HQ HR". iEmpIntro. Qed.

245
246
247
248
249
250
251
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
252
Lemma test_fresh P Q:
253
254
255
256
257
  (P  Q) - (P  Q).
Proof.
  iIntros "H".
  let H1 := iFresh in
  let H2 := iFresh in
Paolo G. Giarrusso's avatar
Paolo G. Giarrusso committed
258
  let pat :=constr:(IList [cons (IIdent H1) (cons (IIdent H2) nil)]) in
259
260
261
262
  iDestruct "H" as pat.
  iFrame.
Qed.

263
264
(* Test for issue #288 *)
(* FIXME: Restore once we drop support for Coq 8.8 and Coq 8.9.
Robbert Krebbers's avatar
Robbert Krebbers committed
265
266
267
268
269
270
271
Lemma test_iExists_unused : (∃ P : PROP, ∃ x : nat, P)%I.
Proof.
  iExists _.
  iExists 10.
  iAssert emp%I as "H"; first done.
  iExact "H".
Qed.
272
*)
Robbert Krebbers's avatar
Robbert Krebbers committed
273

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

Gregory Malecha's avatar
Gregory Malecha committed
278
Lemma test_iExist_tc `{Set_ A C} P :   x1 x2 : gset positive, P - P.
279
280
281
Proof. iExists {[ 1%positive ]}, . auto. Qed.

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

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

292
293
294
295
296
297
298
299
300
301
302
303
304
305
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.

306
Lemma test_iFrame_later `{!BiAffine PROP} P Q : P - Q -  P  Q.
307
308
Proof. iIntros "H1 H2". by iFrame "H1". Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
309
310
311
Lemma test_iAssert_modality P :  False -  P.
Proof.
  iIntros "HF".
312
  iAssert (<affine> False)%I with "[> -]" as %[].
Robbert Krebbers's avatar
Robbert Krebbers committed
313
314
  by iMod "HF".
Qed.
315

316
Lemma test_iMod_affinely_timeless P `{!Timeless P} :
317
  <affine>  P -  <affine> P.
318
319
Proof. iIntros "H". iMod "H". done. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
320
Lemma test_iAssumption_False P : False - P.
321
Proof. iIntros "H". done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
322

323
324
325
326
327
328
Lemma test_iAssumption_coq_1 P Q : ( Q)  <affine> P - Q.
Proof. iIntros (HQ) "_". iAssumption. Qed.

Lemma test_iAssumption_coq_2 P Q : (  Q)  <affine> P -  Q.
Proof. iIntros (HQ) "_". iAssumption. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
329
(* Check instantiation and dependent types *)
Robbert Krebbers's avatar
Robbert Krebbers committed
330
Lemma test_iSpecialize_dependent_type (P :  n, vec nat n  PROP) :
Robbert Krebbers's avatar
Robbert Krebbers committed
331
332
333
334
335
  ( 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
336

337
338
339
340
341
(* 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".
342
  iDestruct (big_sepL_elem_of _ _ _ Hp with "HT") as "Hp".
343
344
345
  done.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
346
347
Lemma test_eauto_iFrame P Q R `{!Persistent R} :
  P - Q - R  R  Q  P  R  False.
348
Proof. eauto 10 with iFrame. Qed.
349

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

354
355
356
357
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
358
Lemma test_iNext_evar P : P - True.
Ralf Jung's avatar
Ralf Jung committed
359
360
361
362
Proof.
  iIntros "HP". iAssert ( _ -  P)%I as "?"; last done.
  iIntros "?". iNext. iAssumption.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
363

364
365
Lemma test_iNext_sep1 P Q (R1 := (P  Q)%I) :
  ( P   Q)  R1 -  ((P  Q)  R1).
Robbert Krebbers's avatar
Robbert Krebbers committed
366
367
368
369
Proof.
  iIntros "H". iNext.
  rewrite {1 2}(lock R1). (* check whether R1 has not been unfolded *) done.
Qed.
370

Robbert Krebbers's avatar
Robbert Krebbers committed
371
Lemma test_iNext_sep2 P Q :  P   Q -  (P  Q).
372
373
374
Proof.
  iIntros "H". iNext. iExact "H". (* Check that the laters are all gone. *)
Qed.
375

Robbert Krebbers's avatar
Robbert Krebbers committed
376
Lemma test_iNext_quantifier {A} (Φ : A  A  PROP) :
Robbert Krebbers's avatar
Robbert Krebbers committed
377
378
379
  ( y,  x,  Φ x y) -  ( y,  x, Φ x y).
Proof. iIntros "H". iNext. done. Qed.

380
381
382
383
Lemma text_iNext_Next {A B : ofeT} (f : A -n> A) x y :
  Next x  Next y - (Next (f x)  Next (f y) : PROP).
Proof. iIntros "H". iNext. by iRewrite "H". Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
384
Lemma test_iFrame_persistent (P Q : PROP) :
385
   P - Q - <pers> (P  P)  (P  Q  Q).
386
Proof. iIntros "#HP". iFrame "HP". iIntros "$". Qed.
387

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

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

394
Lemma test_iDestruct_persistent P (Φ : nat  PROP) `{! x, Persistent (Φ x)}:
395
   (P -  x, Φ x) -
396
397
398
399
400
  P -  x, Φ x  P.
Proof.
  iIntros "#H HP". iDestruct ("H" with "HP") as (x) "#H2". eauto with iFrame.
Qed.

Gregory Malecha's avatar
Gregory Malecha committed
401
Lemma test_iLöb P :   n, ^n P.
Robbert Krebbers's avatar
Robbert Krebbers committed
402
403
404
405
Proof.
  iLöb as "IH". iDestruct "IH" as (n) "IH".
  by iExists (S n).
Qed.
406

407
Lemma test_iInduction_wf (x : nat) P Q :
408
   P - Q -  (x + 0 = x)%nat .
409
410
411
412
413
414
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.

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

424
Lemma test_iIntros_start_proof :
Gregory Malecha's avatar
Gregory Malecha committed
425
  @{PROP} True.
426
427
428
429
430
Proof.
  (* Make sure iIntros actually makes progress and enters the proofmode. *)
  progress iIntros. done.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
431
Lemma test_True_intros : (True : PROP) - True.
432
433
434
Proof.
  iIntros "?". done.
Qed.
435
436
437
438
439
440
441
442
443
444

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

Robbert Krebbers's avatar
Robbert Krebbers committed
448
Lemma test_iNext_iRewrite P Q : <affine>  (Q  P) - <affine>  Q - <affine>  P.
449
Proof.
450
  iIntros "#HPQ HQ !>". iNext. by iRewrite "HPQ" in "HQ".
451
452
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
453
Lemma test_iIntros_modalities `(!Absorbing P) :
Gregory Malecha's avatar
Gregory Malecha committed
454
   <pers> (   x : nat,  x = 0    x = 0  - False - P - P).
455
456
457
458
459
Proof.
  iIntros (x ??).
  iIntros "* **". (* Test that fast intros do not work under modalities *)
  iIntros ([]).
Qed.
460

461
462
463
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
464

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

468
Lemma test_iAlways P Q R :
469
   P - <pers> Q  R - <pers> <affine> <affine> P   Q.
470
Proof. iIntros "#HP #HQ HR". iSplitL. iAlways. done. iAlways. done. Qed.
471

Robbert Krebbers's avatar
Robbert Krebbers committed
472
473
474
(* A bunch of test cases from #127 to establish that tactics behave the same on
`⌜ φ ⌝ → P` and `∀ _ : φ, P` *)
Lemma test_forall_nondep_1 (φ : Prop) :
475
  φ  ( _ : φ, False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
476
477
Proof. iIntros (Hφ) "Hφ". by iApply "Hφ". Qed.
Lemma test_forall_nondep_2 (φ : Prop) :
478
  φ  ( _ : φ, False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
479
480
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" with "[% //]"). done. Qed.
Lemma test_forall_nondep_3 (φ : Prop) :
481
  φ  ( _ : φ, False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
482
483
Proof. iIntros (Hφ) "Hφ". unshelve iSpecialize ("Hφ" $! _). done. done. Qed.
Lemma test_forall_nondep_4 (φ : Prop) :
484
  φ  ( _ : φ, False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
485
486
487
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" $! Hφ); done. Qed.

Lemma test_pure_impl_1 (φ : Prop) :
488
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
489
490
Proof. iIntros (Hφ) "Hφ". by iApply "Hφ". Qed.
Lemma test_pure_impl_2 (φ : Prop) :
491
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
492
493
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" with "[% //]"). done. Qed.
Lemma test_pure_impl_3 (φ : Prop) :
494
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
495
496
Proof. iIntros (Hφ) "Hφ". unshelve iSpecialize ("Hφ" $! _). done. done. Qed.
Lemma test_pure_impl_4 (φ : Prop) :
497
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
498
499
500
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" $! Hφ). done. Qed.

Lemma test_forall_nondep_impl2 (φ : Prop) P :
501
  φ  P - ( _ : φ, P - False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
502
503
504
505
506
507
508
Proof.
  iIntros (Hφ) "HP Hφ".
  Fail iSpecialize ("Hφ" with "HP").
  iSpecialize ("Hφ" with "[% //] HP"). done.
Qed.

Lemma test_pure_impl2 (φ : Prop) P :
509
  φ  P - (⌜φ⌝  P - False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
510
511
512
513
514
515
Proof.
  iIntros (Hφ) "HP Hφ".
  Fail iSpecialize ("Hφ" with "HP").
  iSpecialize ("Hφ" with "[% //] HP"). done.
Qed.

516
517
518
519
520
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
521
Lemma test_iNext_laterN_later P n :  ^n P - ^n  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
522
Proof. iIntros "H". iNext. by iNext. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
523
Lemma test_iNext_later_laterN P n : ^n  P -  ^n P.
Robbert Krebbers's avatar
Robbert Krebbers committed
524
Proof. iIntros "H". iNext. by iNext. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
525
Lemma test_iNext_plus_1 P n1 n2 :  ^n1 ^n2 P - ^n1 ^n2  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
526
Proof. iIntros "H". iNext. iNext. by iNext. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
527
528
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
529
Check "test_iNext_plus_3".
Robbert Krebbers's avatar
Robbert Krebbers committed
530
531
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).
532
Proof. iIntros "H1 H2". iNext. iNext. iNext. iFrame. Show. iModIntro. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
533

534
535
536
537
538
539
540
541
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.

542
543
544
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.
545
546

Lemma test_specialize_affine_pure (φ : Prop) P :
547
  φ  (<affine> ⌜φ⌝ - P)  P.
548
549
550
551
552
Proof.
  iIntros (Hφ) "H". by iSpecialize ("H" with "[% //]").
Qed.

Lemma test_assert_affine_pure (φ : Prop) P :
553
554
  φ  P  P  <affine> ⌜φ⌝.
Proof. iIntros (Hφ). iAssert (<affine> ⌜φ⌝)%I with "[%]" as "$"; auto. Qed.
555
556
Lemma test_assert_pure (φ : Prop) P :
  φ  P  P  ⌜φ⌝.
557
Proof. iIntros (Hφ). iAssert ⌜φ⌝%I with "[%]" as "$"; auto with iFrame. Qed.
558

559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
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.

598
Lemma test_iEval x y :  (y + x)%nat = 1  -  S (x + y) = 2%nat  : PROP.
599
600
601
602
603
604
Proof.
  iIntros (H).
  iEval (rewrite (Nat.add_comm x y) // H).
  done.
Qed.

605
606
607
608
609
610
611
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
612
613
614
615
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.

616
617
618
619
620
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.

621
622
623
624
625
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
626
627
628
629
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.

Gregory Malecha's avatar
Gregory Malecha committed
630
Lemma test_iIntros_pure_neg : @{PROP}  ¬False .
631
Proof. by iIntros (?). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
632

633
Lemma test_iPureIntro_absorbing (φ : Prop) :
Gregory Malecha's avatar
Gregory Malecha committed
634
  φ  @{PROP} <absorb> ⌜φ⌝.
635
636
Proof. intros ?. iPureIntro. done. Qed.

Ralf Jung's avatar
Ralf Jung committed
637
Check "test_iFrame_later_1".
638
Lemma test_iFrame_later_1 P Q : P   Q -  (P   Q).
639
Proof. iIntros "H". iFrame "H". Show. auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
640

Ralf Jung's avatar
Ralf Jung committed
641
Check "test_iFrame_later_2".
642
Lemma test_iFrame_later_2 P Q :  P   Q -  ( P   Q).
643
Proof. iIntros "H". iFrame "H". Show. auto. Qed.
644
645
646
647
648

Lemma test_with_ident P Q R : P - Q - (P - Q - R) - R.
Proof.
  iIntros "? HQ H".
  iMatchHyp (fun H _ =>
649
    iApply ("H" with [spec_patterns.SIdent H []; spec_patterns.SIdent "HQ" []])).
650
Qed.
651
652

Lemma iFrame_with_evar_r P Q :
653
   R, (P - Q - P  R)  R = Q.
654
Proof.
655
  eexists. split. iIntros "HP HQ". iFrame. iApply "HQ". done.
656
657
Qed.
Lemma iFrame_with_evar_l P Q :
658
   R, (P - Q - R  P)  R = Q.
659
Proof.
660
  eexists. split. iIntros "HP HQ". Fail iFrame "HQ".
661
  iSplitR "HP"; iAssumption. done.
662
Qed.
663
664
665
666
667
668
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
669
670
671
672
673
674
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
675
Lemma test_iAssumption_evar P :  R, (R  P)  R = P.
676
677
678
679
680
681
682
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
683
684
685
Lemma test_iAssumption_False_no_loop :  R, R   P, P.
Proof. eexists. iIntros "?" (P). done. Qed.

686
687
688
689
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
690
691
692
693
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.

694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
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.
710

Ralf Jung's avatar
Ralf Jung committed
711
Check "test_and_sep_affine_bi".
712
Lemma test_and_sep_affine_bi `{!BiAffine PROP} P Q :  P  Q   P  Q.
713
Proof.
714
  iIntros "[??]". iSplit; last done. Show. done.
715
Qed.
716

Ralf Jung's avatar
Ralf Jung committed
717
Check "test_big_sepL_simpl".
718
Lemma test_big_sepL_simpl x (l : list nat) P :
Robbert Krebbers's avatar
Robbert Krebbers committed
719
   P -
720
721
722
  ([ list] ky  l, <affine>  y = y ) -
  ([ list] y  x :: l, <affine>  y = y ) -
  P.
723
Proof. iIntros "HP ??". Show. simpl. Show. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
724

Ralf Jung's avatar
Ralf Jung committed
725
Check "test_big_sepL2_simpl".
Robbert Krebbers's avatar
Robbert Krebbers committed
726
727
728
729
730
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).
731
Proof. iIntros "HP ??". Show. simpl. Show. by iLeft. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
732

Ralf Jung's avatar
Ralf Jung committed
733
Check "test_big_sepL2_iDestruct".
Robbert Krebbers's avatar
Robbert Krebbers committed
734
735
736
737
738
739
740
741
742
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.
743
744
745
746

Lemma test_lemma_1 (b : bool) :
  emp @{PROP} ?b True.
Proof. destruct b; simpl; eauto. Qed.
Ralf Jung's avatar
Ralf Jung committed
747
Check "test_reducing_after_iDestruct".
748
749
750
751
752
753
754
755
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
756
Check "test_reducing_after_iApply".
757
758
759
760
761
762
763
764
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
765
Check "test_reducing_after_iApply_late_evar".
766
767
768
769
770
771
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
772
  Import proofmode.base.
Ralf Jung's avatar
Ralf Jung committed
773
  Check "test_wandM".
Ralf Jung's avatar
Ralf Jung committed
774
775
776
777
778
779
780
  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.
781
782
End wandM.

783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
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.
803

804
805
806
807
808
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
809
End tests.
810
811
812
813
814

(** Test specifically if certain things print correctly. *)
Section printing_tests.
Context {PROP : sbi} `{!BiFUpd PROP}.
Implicit Types P Q R : PROP.
815
816
817
818
819

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.
820
821
822

(* Test line breaking of long assumptions. *)
Section linebreaks.
Ralf Jung's avatar
Ralf Jung committed
823
824
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) :
825
826
827
828
  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.
829
  iIntros "HP". Show. Undo. iIntros "?". Show.
830
831
Abort.

832
(* This is specifically crafted such that not having the printing box in
833
834
835
   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
836
837
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) :
838
839
840
  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.
841
  iIntros "HP". Show. Undo. iIntros "?". Show.
842
Abort.
843

Ralf Jung's avatar
Ralf Jung committed
844
Check "long_impl".