proofmode.v 37.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.
5
Context {PROP : bi}.
Robbert Krebbers's avatar
Robbert Krebbers committed
6
Implicit Types P Q R : PROP.
Robbert Krebbers's avatar
Robbert Krebbers committed
7

8
9
10
Lemma test_eauto_emp_isplit_biwand P : emp  P - P.
Proof. eauto 6. Qed.

Gregory Malecha's avatar
Gregory Malecha committed
11
Lemma test_eauto_isplit_biwand P :  P - P.
Paolo G. Giarrusso's avatar
Paolo G. Giarrusso committed
12
Proof. eauto. Qed.
13

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
49
Lemma demo_3 P1 P2 P3 :
Robbert Krebbers's avatar
Robbert Krebbers committed
50
51
  P1  P2  P3 - P1   (P2   x, (P3  x = 0)  P3).
Proof. iIntros "($ & $ & $)". iNext. by iExists 0. Qed.
52

53
54
55
56
57
58
59
60
Lemma test_pure_space_separated P1 :
  <affine> True  P1 - P1.
Proof.
  (* [% H] should be parsed as two separate patterns and not the pure name
  [H] *)
  iIntros "[% H] //".
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
61
62
Definition foo (P : PROP) := (P - P)%I.
Definition bar : PROP := ( P, foo P)%I.
63

Gregory Malecha's avatar
Gregory Malecha committed
64
Lemma test_unfold_constants :  bar.
Robbert Krebbers's avatar
Robbert Krebbers committed
65
Proof. iIntros (P) "HP //". Qed.
66

Ralf Jung's avatar
Ralf Jung committed
67
Check "test_iStopProof".
Robbert Krebbers's avatar
Robbert Krebbers committed
68
Lemma test_iStopProof Q : emp - Q - Q.
Ralf Jung's avatar
Ralf Jung committed
69
Proof. iIntros "#H1 H2". Show. iStopProof. Show. by rewrite bi.sep_elim_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
70

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
88
89
90
91
92
93
94
95
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.

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

100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
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
115
Lemma test_iIntros_pure (ψ φ : Prop) P : ψ    φ   P   φ  ψ   P.
116
117
Proof. iIntros (??) "H". auto. Qed.

118
119
120
121
122
123
124
125
126
Check "test_iIntros_forall_pure".
Lemma test_iIntros_forall_pure (Ψ: nat  PROP) :
    x : nat, Ψ x  Ψ x.
Proof.
  iIntros "%".
  (* should be a trivial implication now *)
  Show. auto.
Qed.

Gregory Malecha's avatar
Gregory Malecha committed
127
Lemma test_iIntros_pure_not : @{PROP}  ¬False .
128
129
Proof. by iIntros (?). Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
130
Lemma test_fast_iIntros P Q :
Gregory Malecha's avatar
Gregory Malecha committed
131
132
    x y z : nat,
    x = plus 0 x  y = 0  z = 0  P   Q  foo (x  x).
133
Proof.
134
  iIntros (a) "*".
135
  iIntros "#Hfoo **".
Robbert Krebbers's avatar
Robbert Krebbers committed
136
  iIntros "_ //".
137
Qed.
138

139
Lemma test_very_fast_iIntros P :
Gregory Malecha's avatar
Gregory Malecha committed
140
   x y : nat,   x = y   P - P.
141
142
Proof. by iIntros. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
143
Definition tc_opaque_test : PROP := tc_opaque ( x : nat,  x = x )%I.
Gregory Malecha's avatar
Gregory Malecha committed
144
Lemma test_iIntros_tc_opaque :  tc_opaque_test.
Robbert Krebbers's avatar
Robbert Krebbers committed
145
Proof. by iIntros (x). Qed.
146

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

152
153
154
Lemma test_iApply_evar P Q R : ( Q, Q - P) - R - P.
Proof. iIntros "H1 H2". iApply "H1". iExact "H2". Qed.

155
156
157
Lemma test_iAssumption_affine P Q R `{!Affine P, !Affine R} : P - Q - R - Q.
Proof. iIntros "H1 H2 H3". iAssumption. Qed.

158
159
160
Lemma test_done_goal_evar Q :  P, Q  P.
Proof. eexists. iIntros "H". Fail done. iAssumption. Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
164
Lemma test_iAssert_persistent P Q : P - Q - True.
Robbert Krebbers's avatar
Robbert Krebbers committed
165
166
167
168
169
170
171
172
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.
173

174
175
176
177
178
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
179
Lemma test_iSpecialize_auto_frame P Q R :
180
  (P - True - True - Q - R) - P - Q - R.
181
Proof. iIntros "H ? HQ". by iApply ("H" with "[$]"). Qed.
182

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

187
Lemma test_iSpecialize_Coq_entailment P Q R :
Gregory Malecha's avatar
Gregory Malecha committed
188
  ( P)  (P - Q)  ( Q).
189
190
Proof. iIntros (HP HPQ). iDestruct (HPQ $! HP) as "?". done. Qed.

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
234
235
236
237
238
239
240
241
242
243
244
245
246
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.

247
248
249
Lemma test_iSpecialize_evar P : ( R, R - R) - P - P.
Proof. iIntros "H HP". iApply ("H" with "[HP]"). done. Qed.

250
251
252
253
Lemma test_iPure_intro_emp R `{!Affine R} :
  R - emp.
Proof. iIntros "HR". by iPureIntro. Qed.

254
255
256
257
Lemma test_iEmp_intro P Q R `{!Affine P, !Persistent Q, !Affine R} :
  P - Q  R - emp.
Proof. iIntros "HP #HQ HR". iEmpIntro. Qed.

258
259
260
261
262
263
264
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
265
Lemma test_fresh P Q:
266
267
268
269
270
  (P  Q) - (P  Q).
Proof.
  iIntros "H".
  let H1 := iFresh in
  let H2 := iFresh in
Paolo G. Giarrusso's avatar
Paolo G. Giarrusso committed
271
  let pat :=constr:(IList [cons (IIdent H1) (cons (IIdent H2) nil)]) in
272
273
274
275
  iDestruct "H" as pat.
  iFrame.
Qed.

276
277
(* 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
278
279
280
281
282
283
284
Lemma test_iExists_unused : (∃ P : PROP, ∃ x : nat, P)%I.
Proof.
  iExists _.
  iExists 10.
  iAssert emp%I as "H"; first done.
  iExact "H".
Qed.
285
*)
Robbert Krebbers's avatar
Robbert Krebbers committed
286

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

Gregory Malecha's avatar
Gregory Malecha committed
291
Lemma test_iExist_tc `{Set_ A C} P :   x1 x2 : gset positive, P - P.
292
293
294
Proof. iExists {[ 1%positive ]}, . auto. Qed.

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

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

305
306
307
308
309
310
311
312
313
314
315
316
317
318
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.

319
Lemma test_iFrame_later `{!BiAffine PROP} P Q : P - Q -  P  Q.
320
321
Proof. iIntros "H1 H2". by iFrame "H1". Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
322
323
324
Lemma test_iAssert_modality P :  False -  P.
Proof.
  iIntros "HF".
325
  iAssert (<affine> False)%I with "[> -]" as %[].
Robbert Krebbers's avatar
Robbert Krebbers committed
326
327
  by iMod "HF".
Qed.
328

329
Lemma test_iMod_affinely_timeless P `{!Timeless P} :
330
  <affine>  P -  <affine> P.
331
332
Proof. iIntros "H". iMod "H". done. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
333
Lemma test_iAssumption_False P : False - P.
334
Proof. iIntros "H". done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
335

336
337
338
339
340
341
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
342
(* Check instantiation and dependent types *)
Robbert Krebbers's avatar
Robbert Krebbers committed
343
Lemma test_iSpecialize_dependent_type (P :  n, vec nat n  PROP) :
Robbert Krebbers's avatar
Robbert Krebbers committed
344
345
346
347
348
  ( 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
349

350
351
352
353
354
(* 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".
355
  iDestruct (big_sepL_elem_of _ _ _ Hp with "HT") as "Hp".
356
357
358
  done.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
359
360
Lemma test_eauto_iFrame P Q R `{!Persistent R} :
  P - Q - R  R  Q  P  R  False.
361
Proof. eauto 10 with iFrame. Qed.
362

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

367
368
369
370
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
371
Lemma test_iNext_evar P : P - True.
Ralf Jung's avatar
Ralf Jung committed
372
373
374
375
Proof.
  iIntros "HP". iAssert ( _ -  P)%I as "?"; last done.
  iIntros "?". iNext. iAssumption.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
376

377
378
Lemma test_iNext_sep1 P Q (R1 := (P  Q)%I) :
  ( P   Q)  R1 -  ((P  Q)  R1).
Robbert Krebbers's avatar
Robbert Krebbers committed
379
380
381
382
Proof.
  iIntros "H". iNext.
  rewrite {1 2}(lock R1). (* check whether R1 has not been unfolded *) done.
Qed.
383

Robbert Krebbers's avatar
Robbert Krebbers committed
384
Lemma test_iNext_sep2 P Q :  P   Q -  (P  Q).
385
386
387
Proof.
  iIntros "H". iNext. iExact "H". (* Check that the laters are all gone. *)
Qed.
388

Robbert Krebbers's avatar
Robbert Krebbers committed
389
Lemma test_iNext_quantifier {A} (Φ : A  A  PROP) :
Robbert Krebbers's avatar
Robbert Krebbers committed
390
391
392
  ( y,  x,  Φ x y) -  ( y,  x, Φ x y).
Proof. iIntros "H". iNext. done. Qed.

393
394
395
396
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
397
Lemma test_iFrame_persistent (P Q : PROP) :
398
   P - Q - <pers> (P  P)  (P  Q  Q).
399
Proof. iIntros "#HP". iFrame "HP". iIntros "$". Qed.
400

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

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

407
Lemma test_iDestruct_persistent P (Φ : nat  PROP) `{! x, Persistent (Φ x)}:
408
   (P -  x, Φ x) -
409
410
411
412
413
  P -  x, Φ x  P.
Proof.
  iIntros "#H HP". iDestruct ("H" with "HP") as (x) "#H2". eauto with iFrame.
Qed.

414
Lemma test_iLöb `{!BiLöb PROP} P :   n, ^n P.
Robbert Krebbers's avatar
Robbert Krebbers committed
415
416
417
418
Proof.
  iLöb as "IH". iDestruct "IH" as (n) "IH".
  by iExists (S n).
Qed.
419

420
Lemma test_iInduction_wf (x : nat) P Q :
421
   P - Q -  (x + 0 = x)%nat .
422
423
424
Proof.
  iIntros "#HP HQ".
  iInduction (lt_wf x) as [[|x] _] "IH"; simpl; first done.
425
  rewrite (inj_iff S). by iApply ("IH" with "[%]"); first lia.
426
427
Qed.

428
429
430
431
432
433
434
435
436
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.

437
Lemma test_iIntros_start_proof :
Gregory Malecha's avatar
Gregory Malecha committed
438
  @{PROP} True.
439
440
441
442
443
Proof.
  (* Make sure iIntros actually makes progress and enters the proofmode. *)
  progress iIntros. done.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
444
Lemma test_True_intros : (True : PROP) - True.
445
446
447
Proof.
  iIntros "?". done.
Qed.
448
449
450
451
452
453
454
455
456
457

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

Robbert Krebbers's avatar
Robbert Krebbers committed
461
Lemma test_iNext_iRewrite P Q : <affine>  (Q  P) - <affine>  Q - <affine>  P.
462
Proof.
463
  iIntros "#HPQ HQ !>". iNext. by iRewrite "HPQ" in "HQ".
464
465
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
466
Lemma test_iIntros_modalities `(!Absorbing P) :
Gregory Malecha's avatar
Gregory Malecha committed
467
   <pers> (   x : nat,  x = 0    x = 0  - False - P - P).
468
469
470
471
472
Proof.
  iIntros (x ??).
  iIntros "* **". (* Test that fast intros do not work under modalities *)
  iIntros ([]).
Qed.
473

474
475
476
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
477

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

481
Lemma test_iAlways P Q R :
482
   P - <pers> Q  R - <pers> <affine> <affine> P   Q.
483
Proof. iIntros "#HP #HQ HR". iSplitL. iAlways. done. iAlways. done. Qed.
484

Robbert Krebbers's avatar
Robbert Krebbers committed
485
486
487
(* A bunch of test cases from #127 to establish that tactics behave the same on
`⌜ φ ⌝ → P` and `∀ _ : φ, P` *)
Lemma test_forall_nondep_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_forall_nondep_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_forall_nondep_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_forall_nondep_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_pure_impl_1 (φ : Prop) :
501
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
502
503
Proof. iIntros (Hφ) "Hφ". by iApply "Hφ". Qed.
Lemma test_pure_impl_2 (φ : Prop) :
504
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
505
506
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" with "[% //]"). done. Qed.
Lemma test_pure_impl_3 (φ : Prop) :
507
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
508
509
Proof. iIntros (Hφ) "Hφ". unshelve iSpecialize ("Hφ" $! _). done. done. Qed.
Lemma test_pure_impl_4 (φ : Prop) :
510
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
511
512
513
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" $! Hφ). done. Qed.

Lemma test_forall_nondep_impl2 (φ : Prop) P :
514
  φ  P - ( _ : φ, P - False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
515
516
517
518
519
520
521
Proof.
  iIntros (Hφ) "HP Hφ".
  Fail iSpecialize ("Hφ" with "HP").
  iSpecialize ("Hφ" with "[% //] HP"). done.
Qed.

Lemma test_pure_impl2 (φ : Prop) P :
522
  φ  P - (⌜φ⌝  P - False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
523
524
525
526
527
528
Proof.
  iIntros (Hφ) "HP Hφ".
  Fail iSpecialize ("Hφ" with "HP").
  iSpecialize ("Hφ" with "[% //] HP"). done.
Qed.

529
530
531
532
533
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
534
Lemma test_iNext_laterN_later P n :  ^n P - ^n  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
535
Proof. iIntros "H". iNext. by iNext. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
536
Lemma test_iNext_later_laterN P n : ^n  P -  ^n P.
Robbert Krebbers's avatar
Robbert Krebbers committed
537
Proof. iIntros "H". iNext. by iNext. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
538
Lemma test_iNext_plus_1 P n1 n2 :  ^n1 ^n2 P - ^n1 ^n2  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
539
Proof. iIntros "H". iNext. iNext. by iNext. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
540
541
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
542
Check "test_iNext_plus_3".
Robbert Krebbers's avatar
Robbert Krebbers committed
543
544
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).
545
Proof. iIntros "H1 H2". iNext. iNext. iNext. iFrame. Show. iModIntro. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
546

547
548
549
550
551
552
553
554
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.

555
556
557
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.
558
559

Lemma test_specialize_affine_pure (φ : Prop) P :
560
  φ  (<affine> ⌜φ⌝ - P)  P.
561
562
563
564
565
Proof.
  iIntros (Hφ) "H". by iSpecialize ("H" with "[% //]").
Qed.

Lemma test_assert_affine_pure (φ : Prop) P :
566
567
  φ  P  P  <affine> ⌜φ⌝.
Proof. iIntros (Hφ). iAssert (<affine> ⌜φ⌝)%I with "[%]" as "$"; auto. Qed.
568
569
Lemma test_assert_pure (φ : Prop) P :
  φ  P  P  ⌜φ⌝.
570
Proof. iIntros (Hφ). iAssert ⌜φ⌝%I with "[%]" as "$"; auto with iFrame. Qed.
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
598
599
600
601
602
603
604
605
606
607
608
609
610
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.

611
Lemma test_iEval x y :  (y + x)%nat = 1  -  S (x + y) = 2%nat  : PROP.
612
613
614
615
616
617
Proof.
  iIntros (H).
  iEval (rewrite (Nat.add_comm x y) // H).
  done.
Qed.

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

629
630
631
632
633
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.

634
635
636
637
638
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
639
640
641
642
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
643
Lemma test_iIntros_pure_neg : @{PROP}  ¬False .
644
Proof. by iIntros (?). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
645

646
Lemma test_iPureIntro_absorbing (φ : Prop) :
Gregory Malecha's avatar
Gregory Malecha committed
647
  φ  @{PROP} <absorb> ⌜φ⌝.
648
649
Proof. intros ?. iPureIntro. done. Qed.

Ralf Jung's avatar
Ralf Jung committed
650
Check "test_iFrame_later_1".
651
Lemma test_iFrame_later_1 P Q : P   Q -  (P   Q).
652
Proof. iIntros "H". iFrame "H". Show. auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
653

Ralf Jung's avatar
Ralf Jung committed
654
Check "test_iFrame_later_2".
655
Lemma test_iFrame_later_2 P Q :  P   Q -  ( P   Q).
656
Proof. iIntros "H". iFrame "H". Show. auto. Qed.
657
658
659
660
661

Lemma test_with_ident P Q R : P - Q - (P - Q - R) - R.
Proof.
  iIntros "? HQ H".
  iMatchHyp (fun H _ =>
662
    iApply ("H" with [spec_patterns.SIdent H []; spec_patterns.SIdent "HQ" []])).
663
Qed.
664
665

Lemma iFrame_with_evar_r P Q :
666
   R, (P - Q - P  R)  R = Q.
667
Proof.
668
  eexists. split. iIntros "HP HQ". iFrame. iApply "HQ". done.
669
670
Qed.
Lemma iFrame_with_evar_l P Q :
671
   R, (P - Q - R  P)  R = Q.
672
Proof.
673
  eexists. split. iIntros "HP HQ". Fail iFrame "HQ".
674
  iSplitR "HP"; iAssumption. done.
675
Qed.
676
677
678
679
680
681
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
682
683
684
685
686
687
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
688
Lemma test_iAssumption_evar P :  R, (R  P)  R = P.
689
690
691
692
693
694
695
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
696
697
698
Lemma test_iAssumption_False_no_loop :  R, R   P, P.
Proof. eexists. iIntros "?" (P). done. Qed.

699
700
701
702
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
703
704
705
706
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.

707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
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.
723

Ralf Jung's avatar
Ralf Jung committed
724
Check "test_and_sep_affine_bi".
725
Lemma test_and_sep_affine_bi `{!BiAffine PROP} P Q :  P  Q   P  Q.
726
Proof.
727
  iIntros "[??]". iSplit; last done. Show. done.
728
Qed.
729

Ralf Jung's avatar
Ralf Jung committed
730
Check "test_big_sepL_simpl".
731
Lemma test_big_sepL_simpl x (l : list nat) P :
Robbert Krebbers's avatar
Robbert Krebbers committed
732
   P -
733
734
735
  ([ list] ky  l, <affine>  y = y ) -
  ([ list] y  x :: l, <affine>  y = y ) -
  P.
736
Proof. iIntros "HP ??". Show. simpl. Show. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
737

Ralf Jung's avatar
Ralf Jung committed
738
Check "test_big_sepL2_simpl".
Robbert Krebbers's avatar
Robbert Krebbers committed
739
740
741
742
743
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).
744
Proof. iIntros "HP ??". Show. simpl. Show. by iLeft. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
745

Ralf Jung's avatar
Ralf Jung committed
746
Check "test_big_sepL2_iDestruct".
Robbert Krebbers's avatar
Robbert Krebbers committed
747
748
749
750
751
752
753
754
755
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.
756
757
758
759

Lemma test_lemma_1 (b : bool) :
  emp @{PROP} ?b True.
Proof. destruct b; simpl; eauto. Qed.
Ralf Jung's avatar
Ralf Jung committed
760
Check "test_reducing_after_iDestruct".
761
762
763
764
765
766
767
768
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
769
Check "test_reducing_after_iApply".
770
771
772
773
774
775
776
777
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
778
Check "test_reducing_after_iApply_late_evar".
779
780
781
782
783
784
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
785
  Import proofmode.base.
Ralf Jung's avatar
Ralf Jung committed
786
  Check "test_wandM".
Ralf Jung's avatar
Ralf Jung committed
787
788
789
790
791
792
793
  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.
794
795
End wandM.

796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
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.
816

817
818
819
820
821
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
822
End tests.
823

824
Section parsing_tests.
825
Context {PROP : bi}.
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
Implicit Types P : PROP.

(** Test notations for (bi)entailment and internal equality. These tests are
especially extensive because of past problems such as
https://gitlab.mpi-sws.org/iris/iris/-/issues/302. *)
Lemma test_bi_emp_valid : @{PROP} True.
Proof. naive_solver. Qed.

Lemma test_bi_emp_valid_parens : (@{PROP} True)  ((@{PROP} True)).
Proof. naive_solver. Qed.

Lemma test_bi_emp_valid_parens_space_open : ( @{PROP} True).
Proof. naive_solver. Qed.

Lemma test_bi_emp_valid_parens_space_close : (@{PROP} True ).
Proof. naive_solver. Qed.

Lemma test_entails_annot_sections P :
  (P @{PROP} P)  (@{PROP}) P P  (P .) P  (. P) P 
  (P @{PROP} P)  (@{PROP}) P P  (P .) P  (. P) P.
Proof. naive_solver. Qed.

Lemma test_entails_annot_sections_parens P :
  ((P @{PROP} P))  ((@{PROP})) P P  ((P .)) P  ((. P)) P 
  ((P @{PROP} P))  ((@{PROP})) P P  ((P .)) P  ((. P)) P.
Proof. naive_solver. Qed.

Lemma test_entails_annot_sections_space_open P :
  ( P @{PROP} P)  ( P .) P 
  ( P @{PROP} P)  ( P .) P.
Proof. naive_solver. Qed.

Lemma test_entails_annot_sections_space_close P :
  (P @{PROP} P )  (@{PROP} ) P P