proofmode.v 42.8 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

71
Lemma test_iRewrite `{!BiInternalEq PROP} {A : ofeT} (x y : A) P :
72
   ( z, P - <affine> (z  y)) - (P - P  (x,x)  (y,x)).
73
Proof.
74
  iIntros "#H1 H2".
75
  iRewrite (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.

115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
Lemma test_iDestruct_exists (Φ: nat  PROP) :
  ( y, Φ y) -  n, Φ n.
Proof. iIntros "H". iDestruct "H" as (y) "H". by iExists y. Qed.

Lemma test_iDestruct_exists_automatic (Φ: nat  PROP) :
  ( y, Φ y) -  n, Φ n.
Proof.
  iIntros "H".
  iDestruct "H" as (?) "H".
  (* the automatic name should by [y] *)
  by iExists y.
Qed.

Lemma test_iDestruct_exists_automatic_multiple (Φ: nat  PROP) :
  ( y n baz, Φ (y+n+baz)) -  n, Φ n.
Proof. iDestruct 1 as (???) "H". by iExists (y+n+baz). Qed.

Lemma test_iDestruct_exists_freshen (y:nat) (Φ: nat  PROP) :
  ( y, Φ y) -  n, Φ n.
Proof.
  iIntros "H".
  iDestruct "H" as (?) "H".
  (* the automatic name is the freshened form of [y] *)
  by iExists y0.
Qed.

Check "test_iDestruct_exists_not_exists".
Lemma test_iDestruct_exists_not_exists P :
  P - P.
Proof. Fail iDestruct 1 as (?) "H". Abort.

Lemma test_iDestruct_exists_explicit_name (Φ: nat  PROP) :
  ( y, Φ y) -  n, Φ n.
Proof.
  (* give an explicit name that isn't the binder name *)
  iDestruct 1 as (foo) "?".
  by iExists foo.
Qed.

Lemma test_iDestruct_exists_pure (Φ: nat  Prop) :
   y, Φ y @{PROP}  n, ⌜Φ n.
Proof.
  iDestruct 1 as (?) "H".
  by iExists y.
Qed.

Lemma test_iDestruct_exists_and_pure (H: True) P :
  False  P - False.
Proof.
  (* this automatic name uses [fresh H] as a sensible default (it's a hypothesis
  in [Prop] and the user cannot supply a name in their code) *)
  iDestruct 1 as (?) "H".
  contradict H0.
Qed.

Check "test_iDestruct_exists_intuitionistic".
Lemma test_iDestruct_exists_intuitionistic P (Φ: nat  PROP) :
   ( y, Φ y  P) - P.
Proof.
  iDestruct 1 as (?) "#H". Show.
  iDestruct "H" as "[_ $]".
Qed.

Lemma test_iDestruct_exists_freshen_local_name (Φ: nat  PROP) :
  let y := 0 in
   ( y, Φ y) -  n, Φ (y+n).
Proof.
  iIntros (y) "#H".
  iDestruct "H" as (?) "H".
  iExists y0; auto.
Qed.

187
188
189
190
191
192
193
194
195
196
197
198
(* regression test for #337 *)
Check "test_iDestruct_exists_anonymous".
Lemma test_iDestruct_exists_anonymous P Φ :
  ( _:nat, P)  ( x:nat, Φ x) - P   x, Φ x.
Proof.
  iIntros "[HP HΦ]".
  (* this should not use [x] as the default name for the unnamed binder *)
  iDestruct "HP" as (?) "$". Show.
  iDestruct "HΦ" as (x) "HΦ".
  by iExists x.
Qed.

199
200
201
202
203
204
205
Definition an_exists P : PROP := ( (an_exists_name:nat), ^an_exists_name P)%I.

(* should use the name from within [an_exists] *)
Lemma test_iDestruct_exists_automatic_def P :
  an_exists P -  k, ^k P.
Proof. iDestruct 1 as (?) "H". by iExists an_exists_name. Qed.

Gregory Malecha's avatar
Gregory Malecha committed
206
Lemma test_iIntros_pure (ψ φ : Prop) P : ψ    φ   P   φ  ψ   P.
207
208
Proof. iIntros (??) "H". auto. Qed.

209
210
211
212
213
214
215
216
217
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.

218
Lemma test_iIntros_pure_not `{!BiPureForall PROP} : @{PROP}  ¬False .
219
220
Proof. by iIntros (?). Qed.

221
Lemma test_fast_iIntros `{!BiInternalEq PROP} P Q :
Gregory Malecha's avatar
Gregory Malecha committed
222
223
    x y z : nat,
    x = plus 0 x  y = 0  z = 0  P   Q  foo (x  x).
224
Proof.
225
  iIntros (a) "*".
226
  iIntros "#Hfoo **".
Robbert Krebbers's avatar
Robbert Krebbers committed
227
  iIntros "_ //".
228
Qed.
229

230
Lemma test_very_fast_iIntros P :
Gregory Malecha's avatar
Gregory Malecha committed
231
   x y : nat,   x = y   P - P.
232
233
Proof. by iIntros. Qed.

234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
Lemma test_iIntros_automatic_name (Φ: nat  PROP) :
   y, Φ y -  x, Φ x.
Proof. iIntros (?) "H". by iExists y. Qed.

Lemma test_iIntros_automatic_name_proofmode_intro (Φ: nat  PROP) :
   y, Φ y -  x, Φ x.
Proof. iIntros "% H". by iExists y. Qed.

(* even an object-level forall should get the right name *)
Lemma test_iIntros_object_forall P :
  P -  (y:unit), P.
Proof. iIntros "H". iIntros (?). destruct y. iAssumption. Qed.

Lemma test_iIntros_object_proofmode_intro (Φ: nat  PROP) :
    y, Φ y -  x, Φ x.
Proof. iIntros "% H". by iExists y. Qed.

Check "test_iIntros_pure_names".
Lemma test_iIntros_pure_names (H:True) P :
   x y : nat,   x = y   P - P.
Proof.
  iIntros (???).
  (* the pure hypothesis should get a sensible [H0] as its name *)
  Show. auto.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
260
Definition tc_opaque_test : PROP := tc_opaque ( x : nat,  x = x )%I.
Gregory Malecha's avatar
Gregory Malecha committed
261
Lemma test_iIntros_tc_opaque :  tc_opaque_test.
Robbert Krebbers's avatar
Robbert Krebbers committed
262
Proof. by iIntros (x). Qed.
263

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

269
270
271
Lemma test_iApply_evar P Q R : ( Q, Q - P) - R - P.
Proof. iIntros "H1 H2". iApply "H1". iExact "H2". Qed.

272
273
274
Lemma test_iAssumption_affine P Q R `{!Affine P, !Affine R} : P - Q - R - Q.
Proof. iIntros "H1 H2 H3". iAssumption. Qed.

275
276
277
Lemma test_done_goal_evar Q :  P, Q  P.
Proof. eexists. iIntros "H". Fail done. iAssumption. Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
281
Lemma test_iAssert_persistent P Q : P - Q - True.
Robbert Krebbers's avatar
Robbert Krebbers committed
282
283
284
285
286
287
288
289
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.
290

291
292
293
294
295
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
296
Lemma test_iSpecialize_auto_frame P Q R :
297
  (P - True - True - Q - R) - P - Q - R.
298
Proof. iIntros "H ? HQ". by iApply ("H" with "[$]"). Qed.
299

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

304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
Lemma test_iSpecialize_pure_done (φ: Prop) Q :
  φ  (⌜φ⌝ - Q)  Q.
Proof. iIntros (HP) "HQ". iApply ("HQ" with "[% //]"). Qed.

Check "test_iSpecialize_pure_error".
Lemma test_iSpecialize_not_pure_error P Q :
  (P - Q)  Q.
Proof. iIntros "HQ". Fail iSpecialize ("HQ" with "[%]"). Abort.

Check "test_iSpecialize_pure_error".
Lemma test_iSpecialize_pure_done_error (φ: Prop) Q :
  (⌜φ⌝ - Q)  Q.
Proof. iIntros "HQ". Fail iSpecialize ("HQ" with "[% //]"). Abort.

Check "test_iSpecialize_done_error".
Lemma test_iSpecialize_done_error P Q :
  (P - Q)  Q.
Proof. iIntros "HQ". Fail iSpecialize ("HQ" with "[//]"). Abort.

323
Lemma test_iSpecialize_Coq_entailment P Q R :
Gregory Malecha's avatar
Gregory Malecha committed
324
  ( P)  (P - Q)  ( Q).
325
326
Proof. iIntros (HP HPQ). iDestruct (HPQ $! HP) as "?". done. Qed.

327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
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.

383
384
385
Lemma test_iSpecialize_evar P : ( R, R - R) - P - P.
Proof. iIntros "H HP". iApply ("H" with "[HP]"). done. Qed.

386
387
388
389
Lemma test_iPure_intro_emp R `{!Affine R} :
  R - emp.
Proof. iIntros "HR". by iPureIntro. Qed.

390
391
392
393
Lemma test_iEmp_intro P Q R `{!Affine P, !Persistent Q, !Affine R} :
  P - Q  R - emp.
Proof. iIntros "HP #HQ HR". iEmpIntro. Qed.

394
395
396
397
398
399
400
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
401
Lemma test_fresh P Q:
402
403
404
405
406
  (P  Q) - (P  Q).
Proof.
  iIntros "H".
  let H1 := iFresh in
  let H2 := iFresh in
Paolo G. Giarrusso's avatar
Paolo G. Giarrusso committed
407
  let pat :=constr:(IList [cons (IIdent H1) (cons (IIdent H2) nil)]) in
408
409
410
411
  iDestruct "H" as pat.
  iFrame.
Qed.

412
(* Test for issue #288 *)
413
Lemma test_iExists_unused :   P : PROP,  x : nat, P.
Robbert Krebbers's avatar
Robbert Krebbers committed
414
415
416
417
418
419
420
Proof.
  iExists _.
  iExists 10.
  iAssert emp%I as "H"; first done.
  iExact "H".
Qed.

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

Gregory Malecha's avatar
Gregory Malecha committed
425
Lemma test_iExist_tc `{Set_ A C} P :   x1 x2 : gset positive, P - P.
426
427
428
Proof. iExists {[ 1%positive ]}, . auto. Qed.

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

435
Lemma test_iFrame_pure `{!BiInternalEq PROP} {A : ofeT} (φ : Prop) (y z : A) :
436
  φ  <affine> y  z - ( φ    φ   y  z : PROP).
Robbert Krebbers's avatar
Robbert Krebbers committed
437
438
Proof. iIntros (Hv) "#Hxy". iFrame (Hv) "Hxy". Qed.

439
440
441
442
443
444
445
446
447
448
449
450
451
452
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.

453
Lemma test_iFrame_later `{!BiAffine PROP} P Q : P - Q -  P  Q.
454
455
Proof. iIntros "H1 H2". by iFrame "H1". Qed.

456
457
Lemma test_iFrame_affinely_1 P Q `{!Affine P} :
  P - <affine> Q - <affine> (P  Q).
458
Proof. iIntros "HP HQ". iFrame "HQ". by iModIntro. Qed.
459
460
Lemma test_iFrame_affinely_2 P Q `{!Affine P, !Affine Q} :
  P - Q - <affine> (P  Q).
461
Proof. iIntros "HP HQ". iFrame "HQ". by iModIntro. Qed.
462

Robbert Krebbers's avatar
Robbert Krebbers committed
463
464
465
Lemma test_iAssert_modality P :  False -  P.
Proof.
  iIntros "HF".
466
  iAssert (<affine> False)%I with "[> -]" as %[].
Robbert Krebbers's avatar
Robbert Krebbers committed
467
468
  by iMod "HF".
Qed.
469

470
Lemma test_iMod_affinely_timeless P `{!Timeless P} :
471
  <affine>  P -  <affine> P.
472
473
Proof. iIntros "H". iMod "H". done. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
474
Lemma test_iAssumption_False P : False - P.
475
Proof. iIntros "H". done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
476

477
478
479
480
481
482
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
483
(* Check instantiation and dependent types *)
Robbert Krebbers's avatar
Robbert Krebbers committed
484
Lemma test_iSpecialize_dependent_type (P :  n, vec nat n  PROP) :
Robbert Krebbers's avatar
Robbert Krebbers committed
485
486
487
488
489
  ( 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
490

491
492
493
494
495
(* 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".
496
  iDestruct (big_sepL_elem_of _ _ _ Hp with "HT") as "Hp".
497
498
499
  done.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
500
501
Lemma test_eauto_iFrame P Q R `{!Persistent R} :
  P - Q - R  R  Q  P  R  False.
502
Proof. eauto 10 with iFrame. Qed.
503

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

508
509
510
511
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
512
Lemma test_iNext_evar P : P - True.
Ralf Jung's avatar
Ralf Jung committed
513
514
515
516
Proof.
  iIntros "HP". iAssert ( _ -  P)%I as "?"; last done.
  iIntros "?". iNext. iAssumption.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
517

518
519
Lemma test_iNext_sep1 P Q (R1 := (P  Q)%I) :
  ( P   Q)  R1 -  ((P  Q)  R1).
Robbert Krebbers's avatar
Robbert Krebbers committed
520
521
522
523
Proof.
  iIntros "H". iNext.
  rewrite {1 2}(lock R1). (* check whether R1 has not been unfolded *) done.
Qed.
524

Robbert Krebbers's avatar
Robbert Krebbers committed
525
Lemma test_iNext_sep2 P Q :  P   Q -  (P  Q).
526
527
528
Proof.
  iIntros "H". iNext. iExact "H". (* Check that the laters are all gone. *)
Qed.
529

Robbert Krebbers's avatar
Robbert Krebbers committed
530
Lemma test_iNext_quantifier {A} (Φ : A  A  PROP) :
Robbert Krebbers's avatar
Robbert Krebbers committed
531
532
533
  ( y,  x,  Φ x y) -  ( y,  x, Φ x y).
Proof. iIntros "H". iNext. done. Qed.

534
Lemma text_iNext_Next `{!BiInternalEq PROP} {A B : ofeT} (f : A -n> A) x y :
535
536
537
  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
538
Lemma test_iFrame_persistent (P Q : PROP) :
539
   P - Q - <pers> (P  P)  (P  Q  Q).
540
Proof. iIntros "#HP". iFrame "HP". iIntros "$". Qed.
541

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

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

548
Lemma test_iDestruct_persistent P (Φ : nat  PROP) `{! x, Persistent (Φ x)}:
549
   (P -  x, Φ x) -
550
551
552
553
554
  P -  x, Φ x  P.
Proof.
  iIntros "#H HP". iDestruct ("H" with "HP") as (x) "#H2". eauto with iFrame.
Qed.

555
Lemma test_iLöb `{!BiLöb PROP} P :   n, ^n P.
Robbert Krebbers's avatar
Robbert Krebbers committed
556
557
558
559
Proof.
  iLöb as "IH". iDestruct "IH" as (n) "IH".
  by iExists (S n).
Qed.
560

561
Lemma test_iInduction_wf (x : nat) P Q :
562
   P - Q -  (x + 0 = x)%nat .
563
564
565
Proof.
  iIntros "#HP HQ".
  iInduction (lt_wf x) as [[|x] _] "IH"; simpl; first done.
566
  rewrite (inj_iff S). by iApply ("IH" with "[%]"); first lia.
567
568
Qed.

569
570
571
572
573
574
575
576
577
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.

578
Lemma test_iIntros_start_proof :
Gregory Malecha's avatar
Gregory Malecha committed
579
  @{PROP} True.
580
581
582
583
584
Proof.
  (* Make sure iIntros actually makes progress and enters the proofmode. *)
  progress iIntros. done.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
585
Lemma test_True_intros : (True : PROP) - True.
586
587
588
Proof.
  iIntros "?". done.
Qed.
589
590
591
592
593
594
595
596
597
598

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

602
603
Lemma test_iNext_iRewrite `{!BiInternalEq PROP} P Q :
  <affine>  (Q  P) - <affine>  Q - <affine>  P.
604
Proof.
605
  iIntros "#HPQ HQ !>". iNext. by iRewrite "HPQ" in "HQ".
606
607
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
608
Lemma test_iIntros_modalities `(!Absorbing P) :
Gregory Malecha's avatar
Gregory Malecha committed
609
   <pers> (   x : nat,  x = 0    x = 0  - False - P - P).
610
611
612
613
614
Proof.
  iIntros (x ??).
  iIntros "* **". (* Test that fast intros do not work under modalities *)
  iIntros ([]).
Qed.
615

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

620
621
Lemma test_iNext_affine `{!BiInternalEq PROP} P Q :
  <affine>  (Q  P) - <affine>  Q - <affine>  P.
622
Proof. iIntros "#HPQ HQ !>". iNext. by iRewrite "HPQ" in "HQ". Qed.
623

624
Lemma test_iAlways P Q R :
625
   P - <pers> Q  R - <pers> <affine> <affine> P   Q.
Ralf Jung's avatar
Ralf Jung committed
626
Proof. iIntros "#HP #HQ HR". iSplitL. iModIntro. done. iModIntro. done. Qed.
627

Robbert Krebbers's avatar
Robbert Krebbers committed
628
629
630
(* A bunch of test cases from #127 to establish that tactics behave the same on
`⌜ φ ⌝ → P` and `∀ _ : φ, P` *)
Lemma test_forall_nondep_1 (φ : Prop) :
631
  φ  ( _ : φ, False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
632
633
Proof. iIntros (Hφ) "Hφ". by iApply "Hφ". Qed.
Lemma test_forall_nondep_2 (φ : Prop) :
634
  φ  ( _ : φ, False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
635
636
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" with "[% //]"). done. Qed.
Lemma test_forall_nondep_3 (φ : Prop) :
637
  φ  ( _ : φ, False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
638
639
Proof. iIntros (Hφ) "Hφ". unshelve iSpecialize ("Hφ" $! _). done. done. Qed.
Lemma test_forall_nondep_4 (φ : Prop) :
640
  φ  ( _ : φ, False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
641
642
643
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" $! Hφ); done. Qed.

Lemma test_pure_impl_1 (φ : Prop) :
644
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
645
646
Proof. iIntros (Hφ) "Hφ". by iApply "Hφ". Qed.
Lemma test_pure_impl_2 (φ : Prop) :
647
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
648
649
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" with "[% //]"). done. Qed.
Lemma test_pure_impl_3 (φ : Prop) :
650
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
651
652
Proof. iIntros (Hφ) "Hφ". unshelve iSpecialize ("Hφ" $! _). done. done. Qed.
Lemma test_pure_impl_4 (φ : Prop) :
653
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
654
655
656
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" $! Hφ). done. Qed.

Lemma test_forall_nondep_impl2 (φ : Prop) P :
657
  φ  P - ( _ : φ, P - False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
658
659
660
661
662
663
664
Proof.
  iIntros (Hφ) "HP Hφ".
  Fail iSpecialize ("Hφ" with "HP").
  iSpecialize ("Hφ" with "[% //] HP"). done.
Qed.

Lemma test_pure_impl2 (φ : Prop) P :
665
  φ  P - (⌜φ⌝  P - False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
666
667
668
669
670
671
Proof.
  iIntros (Hφ) "HP Hφ".
  Fail iSpecialize ("Hφ" with "HP").
  iSpecialize ("Hφ" with "[% //] HP"). done.
Qed.

672
673
674
675
676
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
677
Lemma test_iNext_laterN_later P n :  ^n P - ^n  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
678
Proof. iIntros "H". iNext. by iNext. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
679
Lemma test_iNext_later_laterN P n : ^n  P -  ^n P.
Robbert Krebbers's avatar
Robbert Krebbers committed
680
Proof. iIntros "H". iNext. by iNext. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
681
Lemma test_iNext_plus_1 P n1 n2 :  ^n1 ^n2 P - ^n1 ^n2  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
682
Proof. iIntros "H". iNext. iNext. by iNext. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
683
684
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
685
Check "test_iNext_plus_3".
Robbert Krebbers's avatar
Robbert Krebbers committed
686
687
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).
688
Proof. iIntros "H1 H2". iNext. iNext. iNext. iFrame. Show. iModIntro. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
689

690
691
692
693
694
695
696
697
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.

698
699
700
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.
701
702

Lemma test_specialize_affine_pure (φ : Prop) P :
703
  φ  (<affine> ⌜φ⌝ - P)  P.
704
705
706
707
708
Proof.
  iIntros (Hφ) "H". by iSpecialize ("H" with "[% //]").
Qed.

Lemma test_assert_affine_pure (φ : Prop) P :
709
710
  φ  P  P  <affine> ⌜φ⌝.
Proof. iIntros (Hφ). iAssert (<affine> ⌜φ⌝)%I with "[%]" as "$"; auto. Qed.
711
712
Lemma test_assert_pure (φ : Prop) P :
  φ  P  P  ⌜φ⌝.
713
Proof. iIntros (Hφ). iAssert ⌜φ⌝%I with "[%]" as "$"; auto with iFrame. Qed.
714

715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
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.

754
Lemma test_iEval x y :  (y + x)%nat = 1  -  S (x + y) = 2%nat  : PROP.
755
756
757
758
759
760
Proof.
  iIntros (H).
  iEval (rewrite (Nat.add_comm x y) // H).
  done.
Qed.

761
762
763
764
765
766
767
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
768
769
770
771
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.

772
773
774
775
776
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.

777
778
779
780
781
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
782
783
784
785
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.

786
Lemma test_iPureIntro_absorbing (φ : Prop) :
Gregory Malecha's avatar
Gregory Malecha committed
787
  φ  @{PROP} <absorb> ⌜φ⌝.
788
789
Proof. intros ?. iPureIntro. done. Qed.

Ralf Jung's avatar
Ralf Jung committed
790
Check "test_iFrame_later_1".
791
Lemma test_iFrame_later_1 P Q : P   Q -  (P   Q).
792
Proof. iIntros "H". iFrame "H". Show. auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
793

Ralf Jung's avatar
Ralf Jung committed
794
Check "test_iFrame_later_2".
795
Lemma test_iFrame_later_2 P Q :  P   Q -  ( P   Q).
796
Proof. iIntros "H". iFrame "H". Show. auto. Qed.
797
798
799
800
801

Lemma test_with_ident P Q R : P - Q - (P - Q - R) - R.
Proof.
  iIntros "? HQ H".
  iMatchHyp (fun H _ =>
802
    iApply ("H" with [spec_patterns.SIdent H []; spec_patterns.SIdent "HQ" []])).
803
Qed.
804
805

Lemma iFrame_with_evar_r P Q :
806
   R, (P - Q - P  R)  R = Q.
807
Proof.
808
  eexists. split. iIntros "HP HQ". iFrame. iApply "HQ". done.
809
810
Qed.
Lemma iFrame_with_evar_l P Q :
811
   R, (P - Q - R  P)  R = Q.
812
Proof.
813
  eexists. split. iIntros "HP HQ". Fail iFrame "HQ".
814
  iSplitR "HP"; iAssumption. done.
815
Qed.
816
817
818
819
820
821
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
822
823
824
825
826
827
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
828
Lemma test_iAssumption_evar P :  R, (R  P)  R = P.
829
830
831
832
833
834
835
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
836
837
838
Lemma test_iAssumption_False_no_loop :  R, R   P, P.
Proof. eexists. iIntros "?" (P). done. Qed.

839
840
841
842
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
843
844
845
846
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.

847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
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.
863

Ralf Jung's avatar
Ralf Jung committed
864
Check "test_and_sep_affine_bi".
865
Lemma test_and_sep_affine_bi `{!BiAffine PROP} P Q :  P  Q   P  Q.
866
Proof.
867
  iIntros "[??]". iSplit; last done. Show. done.
868
Qed.
869

Ralf Jung's avatar
Ralf Jung committed
870
Check "test_big_sepL_simpl".
871
Lemma test_big_sepL_simpl x (l : list nat) P :
Robbert Krebbers's avatar
Robbert Krebbers committed
872
   P -
873
874
875
  ([ list] ky  l, <affine>  y = y ) -
  ([ list] y  x :: l, <affine>  y = y ) -
  P.
876
Proof. iIntros "HP ??". Show. simpl. Show. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
877

Ralf Jung's avatar
Ralf Jung committed
878
Check "test_big_sepL2_simpl".
Robbert Krebbers's avatar
Robbert Krebbers committed
879
880
881
882
883
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).
884
Proof. iIntros "HP ??". Show. simpl. Show. by iLeft. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
885

Ralf Jung's avatar
Ralf Jung committed
886
Check "test_big_sepL2_iDestruct".
Robbert Krebbers's avatar
Robbert Krebbers committed
887
888
889
890
891
892
893
894
895
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.
896
897
898
899

Lemma test_lemma_1 (b : bool) :
  emp @{PROP} ?b True.
Proof. destruct b; simpl; eauto. Qed.
Ralf Jung's avatar
Ralf Jung committed
900
Check "test_reducing_after_iDestruct".
901
902
903
904
905
906
907
908
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
909
Check "test_reducing_after_iApply".
910
911
912
913
914
915
916
917
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
918
Check "test_reducing_after_iApply_late_evar".
919
920
921
922
923
924
Lemma test_reducing_after_iApply_late_evar : emp @{PROP} true = true.
Proof.
  iIntros "#H". iApply (test_lemma_3). Show. auto.
Qed.

Section