proofmode.v 56.2 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
From iris.algebra Require Import gmap.
2
From iris.bi Require Import laterable.
3
From iris.proofmode Require Import tactics intro_patterns.
Ralf Jung's avatar
Ralf Jung committed
4
From iris.prelude Require Import options.
Robbert Krebbers's avatar
Robbert Krebbers committed
5

6
7
Unset Mangle Names.

Ralf Jung's avatar
Ralf Jung committed
8
Section tests.
9
Context {PROP : bi}.
Robbert Krebbers's avatar
Robbert Krebbers committed
10
Implicit Types P Q R : PROP.
Robbert Krebbers's avatar
Robbert Krebbers committed
11

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

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

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

58
59
60
61
62
63
64
65
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
66
67
Definition foo (P : PROP) := (P - P)%I.
Definition bar : PROP := ( P, foo P)%I.
68

Gregory Malecha's avatar
Gregory Malecha committed
69
Lemma test_unfold_constants :  bar.
Robbert Krebbers's avatar
Robbert Krebbers committed
70
Proof. iIntros (P) "HP //". Qed.
71

Ralf Jung's avatar
Ralf Jung committed
72
Check "test_iStopProof".
Robbert Krebbers's avatar
Robbert Krebbers committed
73
Lemma test_iStopProof Q : emp - Q - Q.
Ralf Jung's avatar
Ralf Jung committed
74
Proof. iIntros "#H1 H2". Show. iStopProof. Show. by rewrite bi.sep_elim_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
75

76
Lemma test_iRewrite `{!BiInternalEq PROP} {A : ofe} (x y : A) P :
77
   ( z, P - <affine> (z  y)) - (P - P  (x,x)  (y,x)).
78
Proof.
79
  iIntros "#H1 H2".
80
  iRewrite (internal_eq_sym x x with "[# //]").
81
  iRewrite -("H1" $! _ with "[- //]").
Robbert Krebbers's avatar
Robbert Krebbers committed
82
  auto.
83
84
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
85
Lemma test_iRewrite_dom `{!BiInternalEq PROP} {A : ofe} (m1 m2 : gmap nat A) :
86
  m1  m2 @{PROP}  dom m1 = dom m2 .
Robbert Krebbers's avatar
Robbert Krebbers committed
87
88
Proof. iIntros "H". by iRewrite "H". Qed.

Ralf Jung's avatar
Ralf Jung committed
89
Check "test_iDestruct_and_emp".
90
Lemma test_iDestruct_and_emp P Q `{!Persistent P, !Persistent Q} :
91
  P  emp - emp  Q - <affine> (P  Q).
Ralf Jung's avatar
Ralf Jung committed
92
Proof. iIntros "[#? _] [_ #?]". Show. auto. Qed.
93

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

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

105
106
107
108
109
110
111
112
113
114
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
Lemma test_iDestruct_specialize_wand P Q :
  Q - Q -  (Q - P) - P  P.
Proof.
  iIntros "HQ1 HQ2 #HQP".
  (* [iDestruct] does not consume "HQP" because a wand is instantiated *)
  iDestruct ("HQP" with "HQ1") as "HP1".
  iDestruct ("HQP" with "HQ2") as "HP2".
  iFrame.
Qed.
Lemma test_iPoseProof_specialize_wand P Q :
  Q - Q -  (Q - P) - P  P.
Proof.
  iIntros "HQ1 HQ2 #HQP".
  (* [iPoseProof] does not consume "HQP" because a wand is instantiated *)
  iPoseProof ("HQP" with "HQ1") as "HP1".
  iPoseProof ("HQP" with "HQ2") as "HP2".
  iFrame.
Qed.

Lemma test_iDestruct_pose_forall (Φ : nat  PROP) :
   ( x, Φ x) - Φ 0  Φ 1.
Proof.
  iIntros "#H".
  (* [iDestruct] does not consume "H" because quantifiers are instantiated *)
  iDestruct ("H" $! 0) as "$".
  iDestruct ("H" $! 1) as "$".
Qed.

Lemma test_iDestruct_or P Q :  (P  Q) - Q  P.
Proof.
  iIntros "#H".
  (* [iDestruct] consumes "H" because no quantifiers/wands are instantiated *)
  iDestruct "H" as "[H|H]".
  - by iRight.
  - by iLeft.
Qed.
Lemma test_iPoseProof_or P Q :  (P  Q) - (Q  P)  (P  Q).
Proof.
  iIntros "#H".
  (* [iPoseProof] does not consume "H" despite that no quantifiers/wands are
  instantiated. This makes it different from [iDestruct]. *)
  iPoseProof "H" as "[HP|HQ]".
  - iFrame "H". by iRight.
  - iFrame "H". by iLeft.
Qed.

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

155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
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.

170
171
172
173
174
175
176
177
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
234
235
236
237
238
239
240
241
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.

242
243
244
245
246
247
248
249
250
251
252
253
(* 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.

254
255
256
257
258
259
260
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.

261
(* use an Iris intro pattern [% H] rather than (?) to indicate iExistDestruct *)
262
263
264
265
266
267
268
269
Lemma test_exists_intro_pattern_anonymous P (Φ: nat  PROP) :
  P  ( y:nat, Φ y) -  x, P  Φ x.
Proof.
  iIntros "[HP1 [% HP2]]".
  iExists y.
  iFrame "HP1 HP2".
Qed.

Gregory Malecha's avatar
Gregory Malecha committed
270
Lemma test_iIntros_pure (ψ φ : Prop) P : ψ    φ   P   φ  ψ   P.
271
272
Proof. iIntros (??) "H". auto. Qed.

273
274
275
276
277
278
279
280
281
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.

282
Lemma test_iIntros_pure_not `{!BiPureForall PROP} : @{PROP}  ¬False .
283
284
Proof. by iIntros (?). Qed.

285
Lemma test_fast_iIntros `{!BiInternalEq PROP} P Q :
Gregory Malecha's avatar
Gregory Malecha committed
286
287
    x y z : nat,
    x = plus 0 x  y = 0  z = 0  P   Q  foo (x  x).
288
Proof.
289
  iIntros (a) "*".
290
  iIntros "#Hfoo **".
Robbert Krebbers's avatar
Robbert Krebbers committed
291
  iIntros "_ //".
292
Qed.
293

294
Lemma test_very_fast_iIntros P :
Gregory Malecha's avatar
Gregory Malecha committed
295
   x y : nat,   x = y   P - P.
296
297
Proof. by iIntros. Qed.

298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
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
324
Definition tc_opaque_test : PROP := tc_opaque ( x : nat,  x = x )%I.
Gregory Malecha's avatar
Gregory Malecha committed
325
Lemma test_iIntros_tc_opaque :  tc_opaque_test.
Robbert Krebbers's avatar
Robbert Krebbers committed
326
Proof. by iIntros (x). Qed.
327

328
329
330
Lemma test_iApply_evar P Q R : ( Q, Q - P) - R - P.
Proof. iIntros "H1 H2". iApply "H1". iExact "H2". Qed.

331
332
333
Lemma test_iAssumption_affine P Q R `{!Affine P, !Affine R} : P - Q - R - Q.
Proof. iIntros "H1 H2 H3". iAssumption. Qed.

334
335
336
Lemma test_done_goal_evar Q :  P, Q  P.
Proof. eexists. iIntros "H". Fail done. iAssumption. Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
340
Lemma test_iAssert_persistent P Q : P - Q - True.
Robbert Krebbers's avatar
Robbert Krebbers committed
341
342
343
344
345
346
347
348
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.
349

350
351
352
353
354
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
355
Lemma test_iSpecialize_auto_frame P Q R :
356
  (P - True - True - Q - R) - P - Q - R.
357
Proof. iIntros "H ? HQ". by iApply ("H" with "[$]"). Qed.
358

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

363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
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.

382
Lemma test_iSpecialize_Coq_entailment P Q R :
Gregory Malecha's avatar
Gregory Malecha committed
383
  ( P)  (P - Q)  ( Q).
384
385
Proof. iIntros (HP HPQ). iDestruct (HPQ $! HP) as "?". done. Qed.

386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
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.

430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
Check "test_iSpecialize_impl_pure".
Lemma test_iSpecialize_impl_pure (φ : Prop) P Q :
  φ  (⌜φ⌝  P) - (⌜φ⌝  Q) - P  Q.
Proof.
  iIntros (?) "#H1 H2".
  (* Adds an affine modality *)
  iSpecialize ("H1" with "[]"). { Show. done. }
Restart.
  iIntros (?) "#H1 H2".
  (* Solving it directly as a pure goal also works. *)
  iSpecialize ("H1" with "[% //]").
  iSpecialize ("H2" with "[% //]").
  by iFrame.
Abort.

Check "test_iSpecialize_impl_pure_affine".
Lemma test_iSpecialize_impl_pure_affine `{!BiAffine PROP} (φ : Prop) P Q :
  φ  (⌜φ⌝  P) - (⌜φ⌝  Q) - P  Q.
Proof.
  iIntros (?) "#H1 H2".
  (* Does not add an affine modality *)
  iSpecialize ("H1" with "[]"). { Show. done. }
Restart.
  iIntros (?) "#H1 H2".
  (* Solving it directly as a pure goal also works. *)
  iSpecialize ("H1" with "[% //]").
  iSpecialize ("H2" with "[% //]").
  by iFrame.
Abort.

460
461
462
463
464
465
466
467
468
469
470
471
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.

472
473
474
Lemma test_iSpecialize_evar P : ( R, R - R) - P - P.
Proof. iIntros "H HP". iApply ("H" with "[HP]"). done. Qed.

475
476
477
478
Lemma test_iPure_intro_emp R `{!Affine R} :
  R - emp.
Proof. iIntros "HR". by iPureIntro. Qed.

479
480
481
482
Lemma test_iEmp_intro P Q R `{!Affine P, !Persistent Q, !Affine R} :
  P - Q  R - emp.
Proof. iIntros "HP #HQ HR". iEmpIntro. Qed.

483
484
485
486
487
488
489
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.

490
491
(* Ensure that [% ...] works as a pattern when the left-hand side of and/sep is
pure. *)
Ralf Jung's avatar
Ralf Jung committed
492
Lemma test_pure_and_sep_destruct_affine `{!BiAffine PROP} (φ : Prop) P :
493
494
495
496
  ⌜φ⌝  (⌜φ⌝  P) - P.
Proof.
  iIntros "[% [% $]]".
Qed.
Ralf Jung's avatar
Ralf Jung committed
497
Lemma test_pure_and_sep_destruct_1 (φ : Prop) P :
Ralf Jung's avatar
Ralf Jung committed
498
499
500
501
  ⌜φ⌝  (<affine> ⌜φ⌝  P) - P.
Proof.
  iIntros "[% [% $]]".
Qed.
Ralf Jung's avatar
Ralf Jung committed
502
Lemma test_pure_and_sep_destruct_2 (φ : Prop) P :
Ralf Jung's avatar
Ralf Jung committed
503
504
505
506
  ⌜φ⌝  (⌜φ⌝  <absorb> P) - <absorb> P.
Proof.
  iIntros "[% [% $]]".
Qed.
507
508
509
510
511
512
513
514
(* Ensure that [% %] also works when the conjunction is *inside* ⌜...⌝ *)
Lemma test_pure_inner_and_destruct :
  False  True @{PROP} False.
Proof.
  iIntros "[% %]". done.
Qed.

(* Ensure that [% %] works as a pattern for an existential with a pure body. *)
515
Lemma test_exist_pure_destruct_1 :
516
517
518
519
  ( x,  x = 0 ) @{PROP} True.
Proof.
  iIntros "[% %]". done.
Qed.
520
521
522
523
524
525
526
(* Also test nested existentials where the type of the 2nd depends on the first
(which could cause trouble if we do things in the wrong order) *)
Lemma test_exist_pure_destruct_2 :
  ( x (_:x=0), True) @{PROP} True.
Proof.
  iIntros "(% & % & $)".
Qed.
527

Ralf Jung's avatar
Ralf Jung committed
528
Lemma test_fresh P Q:
529
530
531
532
533
  (P  Q) - (P  Q).
Proof.
  iIntros "H".
  let H1 := iFresh in
  let H2 := iFresh in
Paolo G. Giarrusso's avatar
Paolo G. Giarrusso committed
534
  let pat :=constr:(IList [cons (IIdent H1) (cons (IIdent H2) nil)]) in
535
536
537
538
  iDestruct "H" as pat.
  iFrame.
Qed.

539
(* Test for issue #288 *)
540
Lemma test_iExists_unused :   P : PROP,  x : nat, P.
Robbert Krebbers's avatar
Robbert Krebbers committed
541
542
543
544
545
546
547
Proof.
  iExists _.
  iExists 10.
  iAssert emp%I as "H"; first done.
  iExact "H".
Qed.

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

Gregory Malecha's avatar
Gregory Malecha committed
552
Lemma test_iExist_tc `{Set_ A C} P :   x1 x2 : gset positive, P - P.
553
554
555
Proof. iExists {[ 1%positive ]}, . auto. Qed.

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

562
Lemma test_iFrame_pure `{!BiInternalEq PROP} {A : ofe} (φ : Prop) (y z : A) :
563
  φ  <affine> y  z - ( φ    φ   y  z : PROP).
Robbert Krebbers's avatar
Robbert Krebbers committed
564
565
Proof. iIntros (Hv) "#Hxy". iFrame (Hv) "Hxy". Qed.

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

580
Lemma test_iFrame_later `{!BiAffine PROP} P Q : P - Q -  P  Q.
581
582
Proof. iIntros "H1 H2". by iFrame "H1". Qed.

583
584
Lemma test_iFrame_affinely_1 P Q `{!Affine P} :
  P - <affine> Q - <affine> (P  Q).
585
Proof. iIntros "HP HQ". iFrame "HQ". by iModIntro. Qed.
586
587
Lemma test_iFrame_affinely_2 P Q `{!Affine P, !Affine Q} :
  P - Q - <affine> (P  Q).
588
Proof. iIntros "HP HQ". iFrame "HQ". by iModIntro. Qed.
589

Robbert Krebbers's avatar
Robbert Krebbers committed
590
591
592
Lemma test_iAssert_modality P :  False -  P.
Proof.
  iIntros "HF".
593
  iAssert (<affine> False)%I with "[> -]" as %[].
Robbert Krebbers's avatar
Robbert Krebbers committed
594
595
  by iMod "HF".
Qed.
596

597
Lemma test_iMod_affinely_timeless P `{!Timeless P} :
598
  <affine>  P -  <affine> P.
599
600
Proof. iIntros "H". iMod "H". done. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
601
Lemma test_iAssumption_False P : False - P.
602
Proof. iIntros "H". done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
603

604
605
606
607
608
609
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
610
(* Check instantiation and dependent types *)
Robbert Krebbers's avatar
Robbert Krebbers committed
611
Lemma test_iSpecialize_dependent_type (P :  n, vec nat n  PROP) :
Robbert Krebbers's avatar
Robbert Krebbers committed
612
613
614
615
616
  ( 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
617

618
619
620
621
622
(* 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".
623
  iDestruct (big_sepL_elem_of _ _ _ Hp with "HT") as "Hp".
624
625
626
  done.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
627
628
Lemma test_eauto_iFrame P Q R `{!Persistent R} :
  P - Q - R  R  Q  P  R  False.
629
Proof. eauto 10 with iFrame. Qed.
630

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

635
636
637
638
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
639
Lemma test_iNext_evar P : P - True.
Ralf Jung's avatar
Ralf Jung committed
640
641
642
643
Proof.
  iIntros "HP". iAssert ( _ -  P)%I as "?"; last done.
  iIntros "?". iNext. iAssumption.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
644

645
646
Lemma test_iNext_sep1 P Q (R1 := (P  Q)%I) :
  ( P   Q)  R1 -  ((P  Q)  R1).
Robbert Krebbers's avatar
Robbert Krebbers committed
647
648
649
650
Proof.
  iIntros "H". iNext.
  rewrite {1 2}(lock R1). (* check whether R1 has not been unfolded *) done.
Qed.
651

Robbert Krebbers's avatar
Robbert Krebbers committed
652
Lemma test_iNext_sep2 P Q :  P   Q -  (P  Q).
653
654
655
Proof.
  iIntros "H". iNext. iExact "H". (* Check that the laters are all gone. *)
Qed.
656

Robbert Krebbers's avatar
Robbert Krebbers committed
657
Lemma test_iNext_quantifier {A} (Φ : A  A  PROP) :
Robbert Krebbers's avatar
Robbert Krebbers committed
658
659
660
  ( y,  x,  Φ x y) -  ( y,  x, Φ x y).
Proof. iIntros "H". iNext. done. Qed.

661
Lemma text_iNext_Next `{!BiInternalEq PROP} {A B : ofe} (f : A -n> A) x y :
662
663
664
  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
665
Lemma test_iFrame_persistent (P Q : PROP) :
666
   P - Q - <pers> (P  P)  (P  Q  Q).
667
Proof. iIntros "#HP". iFrame "HP". iIntros "$". Qed.
668

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

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

675
Lemma test_iDestruct_persistent P (Φ : nat  PROP) `{! x, Persistent (Φ x)}:
676
   (P -  x, Φ x) -
677
678
679
680
681
  P -  x, Φ x  P.
Proof.
  iIntros "#H HP". iDestruct ("H" with "HP") as (x) "#H2". eauto with iFrame.
Qed.

682
Lemma test_iLöb `{!BiLöb PROP} P :   n, ^n P.
Robbert Krebbers's avatar
Robbert Krebbers committed
683
684
685
686
Proof.
  iLöb as "IH". iDestruct "IH" as (n) "IH".
  by iExists (S n).
Qed.
687

688
Lemma test_iInduction_wf (x : nat) P Q :
689
   P - Q -  (x + 0 = x)%nat .
690
691
692
Proof.
  iIntros "#HP HQ".
  iInduction (lt_wf x) as [[|x] _] "IH"; simpl; first done.
693
  rewrite (inj_iff S). by iApply ("IH" with "[%]"); first lia.
694
695
Qed.

696
697
698
699
700
701
702
703
704
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.

705
706
707
708
709
710
711
712
713
714
715
716
Inductive tree := leaf | node (l r: tree).

Check "test_iInduction_multiple_IHs".
Lemma test_iInduction_multiple_IHs (t: tree) (Φ : tree  PROP) :
   Φ leaf -  ( l r, Φ l - Φ r - Φ (node l r)) - Φ t.
Proof.
  iIntros "#Hleaf #Hnode". iInduction t as [|l r] "IH".
  - iExact "Hleaf".
  - Show. (* should have "IH" and "IH1", since [node] has two trees *)
    iApply ("Hnode" with "IH IH1").
Qed.

717
Lemma test_iIntros_start_proof :
Gregory Malecha's avatar
Gregory Malecha committed
718
  @{PROP} True.
719
720
721
722
723
Proof.
  (* Make sure iIntros actually makes progress and enters the proofmode. *)
  progress iIntros. done.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
724
Lemma test_True_intros : (True : PROP) - True.
725
726
727
Proof.
  iIntros "?". done.
Qed.
728
729
730
731
732
733
734
735
736
737

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

741
742
Lemma test_iNext_iRewrite `{!BiInternalEq PROP} P Q :
  <affine>  (Q  P) - <affine>  Q - <affine>  P.
743
Proof.
744
  iIntros "#HPQ HQ !>". iNext. by iRewrite "HPQ" in "HQ".
745
746
Qed.

747
Lemma test_iIntros_modalities `{!BiPersistentlyForall PROP} `(!Absorbing P) :
Gregory Malecha's avatar
Gregory Malecha committed
748
   <pers> (   x : nat,  x = 0    x = 0  - False - P - P).
749
750
751
752
753
Proof.
  iIntros (x ??).
  iIntros "* **". (* Test that fast intros do not work under modalities *)
  iIntros ([]).
Qed.
754

755
756
757
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
758

759
760
Lemma test_iNext_affine `{!BiInternalEq PROP} P Q :
  <affine>  (Q  P) - <affine>  Q - <affine>  P.
761
Proof. iIntros "#HPQ HQ !>". iNext. by iRewrite "HPQ" in "HQ". Qed.
762

763
Lemma test_iAlways P Q R :
764
   P - <pers> Q  R - <pers> <affine> <affine> P   Q.
Ralf Jung's avatar
Ralf Jung committed
765
766
767
768
769
Proof.
  iIntros "#HP #HQ HR". iSplitL.
  - iModIntro. done.
  - iModIntro. done.
Qed.
770

Robbert Krebbers's avatar
Robbert Krebbers committed
771
772
773
(* A bunch of test cases from #127 to establish that tactics behave the same on
`⌜ φ ⌝ → P` and `∀ _ : φ, P` *)
Lemma test_forall_nondep_1 (φ : Prop) :
774
  φ  ( _ : φ, False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
775
776
Proof. iIntros (Hφ) "Hφ". by iApply "Hφ". Qed.
Lemma test_forall_nondep_2 (φ : Prop) :
777
  φ  ( _ : φ, False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
778
779
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" with "[% //]"). done. Qed.
Lemma test_forall_nondep_3 (φ : Prop) :
780
  φ  ( _ : φ, False : PROP) - False.
Ralf Jung's avatar
Ralf Jung committed
781
Proof. iIntros (Hφ) "Hφ". unshelve iSpecialize ("Hφ" $! _); done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
782
Lemma test_forall_nondep_4 (φ : Prop) :
783
  φ  ( _ : φ, False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
784
785
786
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" $! Hφ); done. Qed.

Lemma test_pure_impl_1 (φ : Prop) :
787
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
788
789
Proof. iIntros (Hφ) "Hφ". by iApply "Hφ". Qed.
Lemma test_pure_impl_2 (φ : Prop) :
790
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
791
792
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" with "[% //]"). done. Qed.
Lemma test_pure_impl_3 (φ : Prop) :
793
  φ  (⌜φ⌝  False : PROP) - False.
Ralf Jung's avatar
Ralf Jung committed
794
Proof. iIntros (Hφ) "Hφ". unshelve iSpecialize ("Hφ" $! _); done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
795
Lemma test_pure_impl_4 (φ : Prop) :
796
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
797
798
799
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" $! Hφ). done. Qed.

Lemma test_forall_nondep_impl2 (φ : Prop) P :
800
  φ  P - ( _ : φ, P - False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
801
802
803
804
805
806
807
Proof.
  iIntros (Hφ) "HP Hφ".
  Fail iSpecialize ("Hφ" with "HP").
  iSpecialize ("Hφ" with "[% //] HP"). done.
Qed.

Lemma test_pure_impl2 (φ : Prop) P :
808
  φ  P - (⌜φ⌝  P - False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
809
810
811
812
813
814
Proof.
  iIntros (Hφ) "HP Hφ".
  Fail iSpecialize ("Hφ" with "HP").
  iSpecialize ("Hφ" with "[% //] HP"). done.
Qed.

815
816
817
818
819
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
820
Lemma test_iNext_laterN_later P n :  ^n P - ^n  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
821
Proof. iIntros "H". iNext. by iNext. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
822
Lemma test_iNext_later_laterN P n : ^n  P -  ^n P.
Robbert Krebbers's avatar
Robbert Krebbers committed
823
Proof. iIntros "H". iNext. by iNext. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
824
Lemma test_iNext_plus_1 P n1 n2 :  ^n1 ^n2 P - ^n1 ^n2  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
825
Proof. iIntros "H". iNext. iNext. by iNext. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
826
827
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
828
Check "test_iNext_plus_3".
Robbert Krebbers's avatar
Robbert Krebbers committed
829
830
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).
831
Proof. iIntros "H1 H2". iNext. iNext. iNext. iFrame. Show. iModIntro. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
832

833
834
835
836
837
838
839
840
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.

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

Lemma test_specialize_affine_pure (φ : Prop) P :
846
  φ  (<affine> ⌜φ⌝ - P)  P.
847
848
849
850
851
Proof.
  iIntros (Hφ) "H". by iSpecialize ("H" with "[% //]").
Qed.

Lemma test_assert_affine_pure (φ : Prop) P :
852
853
  φ  P  P  <affine> ⌜φ⌝.
Proof. iIntros (Hφ). iAssert (<affine> ⌜φ⌝)%I with "[%]" as "$"; auto. Qed.
854
855
Lemma test_assert_pure (φ : Prop) P :
  φ  P  P  ⌜φ⌝.
856
Proof. iIntros (Hφ). iAssert ⌜φ⌝%I with "[%]" as "$"; auto with iFrame. Qed.
857

858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
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.

897
Lemma test_iEval x y :  (y + x)%nat = 1  @{PROP}  S (x + y) = 2%nat .
898
899
900
901
902
903
Proof.
  iIntros (H).
  iEval (rewrite (Nat.add_comm x y) // H).
  done.
Qed.

904
905
906
907
908
909
910
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
911
Check "test_iSimpl_in".
912
Lemma test_iSimpl_in x y :  (3 + x)%nat = y  @{PROP}  S (S (S x)) = y .
Robbert Krebbers's avatar
Robbert Krebbers committed
913
914
Proof. iIntros "H". iSimpl in "H". Show. done. Qed.

915
Lemma test_iSimpl_in_2 x y z :
916
917
   (3 + x)%nat = y  @{PROP}  (1 + y)%nat = z  -
   S (S (S x)) = y .
918
919
Proof. iIntros "H1 H2". iSimpl in "H1 H2". Show. done. Qed.

920
Lemma test_iSimpl_in3 x y z :
921
922
   (3 + x)%nat = y  @{PROP}  (1 + y)%nat = z  -
   S (S (S x)) = y .
923
924
Proof. iIntros "#H1 H2". iSimpl in "#". Show. done. Qed.

Dan Frumin's avatar
Dan Frumin committed
925
Check "test_iSimpl_in4".
926
Lemma test_iSimpl_in4 x y :  (3 + x)%nat = y  @{PROP}  S (S (S x)) = y .
Dan Frumin's avatar
Dan Frumin committed
927
928
Proof. iIntros "H". Fail iSimpl in "%". by iSimpl in "H". Qed.

929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
Check "test_iRename".
Lemma test_iRename P : P - P.
Proof. iIntros "#H". iRename "H" into "X". Show. iExact "X". Qed.

(** [iTypeOf] is an internal tactic for the proofmode *)
Lemma test_iTypeOf Q R φ :  Q  R  ⌜φ⌝ - True.
Proof.
  iIntros "(#HQ & H)".
  lazymatch iTypeOf "HQ" with
  | Some (true, Q) => idtac
  | ?x => fail "incorrect iTypeOf HQ" x
  end.
  lazymatch iTypeOf "H" with
  | Some (false, (R  ⌜φ⌝)%I) => idtac
  | ?x => fail "incorrect iTypeOf H" x
  end.
  lazymatch iTypeOf "missing" with
  | None => idtac
  | ?x => fail "incorrect iTypeOf missing" x
  end.
Abort.

951
Lemma test_iPureIntro_absorbing (φ : Prop) :
Gregory Malecha's avatar
Gregory Malecha committed
952
  φ  @{PROP} <absorb> ⌜φ⌝.
953
954
Proof. intros ?. iPureIntro. done. Qed.

Ralf Jung's avatar
Ralf Jung committed
955
Check "test_iFrame_later_1".
956
Lemma test_iFrame_later_1 P Q : P   Q -  (P   Q).
957
Proof. iIntros "H". iFrame "H". Show. auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
958

Ralf Jung's avatar
Ralf Jung committed
959
Check "test_iFrame_later_2".