proofmode.v 52.3 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
86
87
88
89
Lemma test_iRewrite_dom `{!BiInternalEq PROP} {A : ofe} (m1 m2 : gmap nat A) :
  m1  m2 @{PROP}
   dom (gset nat) m1 = dom (gset nat) m2 .
Proof. iIntros "H". by iRewrite "H". Qed.

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

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

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

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
151
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.

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

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

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
242
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.

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

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

262
(* use an Iris intro pattern [% H] rather than (?) to indicate iExistDestruct *)
263
264
265
266
267
268
269
270
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
271
Lemma test_iIntros_pure (ψ φ : Prop) P : ψ    φ   P   φ  ψ   P.
272
273
Proof. iIntros (??) "H". auto. Qed.

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

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

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

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

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
324
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
325
Definition tc_opaque_test : PROP := tc_opaque ( x : nat,  x = x )%I.
Gregory Malecha's avatar
Gregory Malecha committed
326
Lemma test_iIntros_tc_opaque :  tc_opaque_test.
Robbert Krebbers's avatar
Robbert Krebbers committed
327
Proof. by iIntros (x). Qed.
328

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

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

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

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

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

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

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

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

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

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
430
431
432
433
434
435
436
437
438
439
440
441
442
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.

443
444
445
Lemma test_iSpecialize_evar P : ( R, R - R) - P - P.
Proof. iIntros "H HP". iApply ("H" with "[HP]"). done. Qed.

446
447
448
449
Lemma test_iPure_intro_emp R `{!Affine R} :
  R - emp.
Proof. iIntros "HR". by iPureIntro. Qed.

450
451
452
453
Lemma test_iEmp_intro P Q R `{!Affine P, !Persistent Q, !Affine R} :
  P - Q  R - emp.
Proof. iIntros "HP #HQ HR". iEmpIntro. Qed.

454
455
456
457
458
459
460
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.

461
462
(* Ensure that [% ...] works as a pattern when the left-hand side of and/sep is
pure. *)
Ralf Jung's avatar
Ralf Jung committed
463
Lemma test_pure_and_sep_destruct_affine `{!BiAffine PROP} (φ : Prop) P :
464
465
466
467
  ⌜φ⌝  (⌜φ⌝  P) - P.
Proof.
  iIntros "[% [% $]]".
Qed.
Ralf Jung's avatar
Ralf Jung committed
468
Lemma test_pure_and_sep_destruct_1 (φ : Prop) P :
Ralf Jung's avatar
Ralf Jung committed
469
470
471
472
  ⌜φ⌝  (<affine> ⌜φ⌝  P) - P.
Proof.
  iIntros "[% [% $]]".
Qed.
Ralf Jung's avatar
Ralf Jung committed
473
Lemma test_pure_and_sep_destruct_2 (φ : Prop) P :
Ralf Jung's avatar
Ralf Jung committed
474
475
476
477
  ⌜φ⌝  (⌜φ⌝  <absorb> P) - <absorb> P.
Proof.
  iIntros "[% [% $]]".
Qed.
478
479
480
481
482
483
484
485
(* 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. *)
486
Lemma test_exist_pure_destruct_1 :
487
488
489
490
  ( x,  x = 0 ) @{PROP} True.
Proof.
  iIntros "[% %]". done.
Qed.
491
492
493
494
495
496
497
(* 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.
498

Ralf Jung's avatar
Ralf Jung committed
499
Lemma test_fresh P Q:
500
501
502
503
504
  (P  Q) - (P  Q).
Proof.
  iIntros "H".
  let H1 := iFresh in
  let H2 := iFresh in
Paolo G. Giarrusso's avatar
Paolo G. Giarrusso committed
505
  let pat :=constr:(IList [cons (IIdent H1) (cons (IIdent H2) nil)]) in
506
507
508
509
  iDestruct "H" as pat.
  iFrame.
Qed.

510
(* Test for issue #288 *)
511
Lemma test_iExists_unused :   P : PROP,  x : nat, P.
Robbert Krebbers's avatar
Robbert Krebbers committed
512
513
514
515
516
517
518
Proof.
  iExists _.
  iExists 10.
  iAssert emp%I as "H"; first done.
  iExact "H".
Qed.

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

Gregory Malecha's avatar
Gregory Malecha committed
523
Lemma test_iExist_tc `{Set_ A C} P :   x1 x2 : gset positive, P - P.
524
525
526
Proof. iExists {[ 1%positive ]}, . auto. Qed.

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

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

537
538
539
540
541
542
543
544
545
546
547
548
549
550
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.

551
Lemma test_iFrame_later `{!BiAffine PROP} P Q : P - Q -  P  Q.
552
553
Proof. iIntros "H1 H2". by iFrame "H1". Qed.

554
555
Lemma test_iFrame_affinely_1 P Q `{!Affine P} :
  P - <affine> Q - <affine> (P  Q).
556
Proof. iIntros "HP HQ". iFrame "HQ". by iModIntro. Qed.
557
558
Lemma test_iFrame_affinely_2 P Q `{!Affine P, !Affine Q} :
  P - Q - <affine> (P  Q).
559
Proof. iIntros "HP HQ". iFrame "HQ". by iModIntro. Qed.
560

Robbert Krebbers's avatar
Robbert Krebbers committed
561
562
563
Lemma test_iAssert_modality P :  False -  P.
Proof.
  iIntros "HF".
564
  iAssert (<affine> False)%I with "[> -]" as %[].
Robbert Krebbers's avatar
Robbert Krebbers committed
565
566
  by iMod "HF".
Qed.
567

568
Lemma test_iMod_affinely_timeless P `{!Timeless P} :
569
  <affine>  P -  <affine> P.
570
571
Proof. iIntros "H". iMod "H". done. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
572
Lemma test_iAssumption_False P : False - P.
573
Proof. iIntros "H". done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
574

575
576
577
578
579
580
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
581
(* Check instantiation and dependent types *)
Robbert Krebbers's avatar
Robbert Krebbers committed
582
Lemma test_iSpecialize_dependent_type (P :  n, vec nat n  PROP) :
Robbert Krebbers's avatar
Robbert Krebbers committed
583
584
585
586
587
  ( 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
588

589
590
591
592
593
(* 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".
594
  iDestruct (big_sepL_elem_of _ Hp with "HT") as "Hp".
595
596
597
  done.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
598
599
Lemma test_eauto_iFrame P Q R `{!Persistent R} :
  P - Q - R  R  Q  P  R  False.
600
Proof. eauto 10 with iFrame. Qed.
601

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

606
607
608
609
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
610
Lemma test_iNext_evar P : P - True.
Ralf Jung's avatar
Ralf Jung committed
611
612
613
614
Proof.
  iIntros "HP". iAssert ( _ -  P)%I as "?"; last done.
  iIntros "?". iNext. iAssumption.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
615

616
617
Lemma test_iNext_sep1 P Q (R1 := (P  Q)%I) :
  ( P   Q)  R1 -  ((P  Q)  R1).
Robbert Krebbers's avatar
Robbert Krebbers committed
618
619
620
621
Proof.
  iIntros "H". iNext.
  rewrite {1 2}(lock R1). (* check whether R1 has not been unfolded *) done.
Qed.
622

Robbert Krebbers's avatar
Robbert Krebbers committed
623
Lemma test_iNext_sep2 P Q :  P   Q -  (P  Q).
624
625
626
Proof.
  iIntros "H". iNext. iExact "H". (* Check that the laters are all gone. *)
Qed.
627

Robbert Krebbers's avatar
Robbert Krebbers committed
628
Lemma test_iNext_quantifier {A} (Φ : A  A  PROP) :
Robbert Krebbers's avatar
Robbert Krebbers committed
629
630
631
  ( y,  x,  Φ x y) -  ( y,  x, Φ x y).
Proof. iIntros "H". iNext. done. Qed.

632
Lemma text_iNext_Next `{!BiInternalEq PROP} {A B : ofe} (f : A -n> A) x y :
633
634
635
  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
636
Lemma test_iFrame_persistent (P Q : PROP) :
637
   P - Q - <pers> (P  P)  (P  Q  Q).
638
Proof. iIntros "#HP". iFrame "HP". iIntros "$". Qed.
639

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

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

646
Lemma test_iDestruct_persistent P (Φ : nat  PROP) `{! x, Persistent (Φ x)}:
647
   (P -  x, Φ x) -
648
649
650
651
652
  P -  x, Φ x  P.
Proof.
  iIntros "#H HP". iDestruct ("H" with "HP") as (x) "#H2". eauto with iFrame.
Qed.

653
Lemma test_iLöb `{!BiLöb PROP} P :   n, ^n P.
Robbert Krebbers's avatar
Robbert Krebbers committed
654
655
656
657
Proof.
  iLöb as "IH". iDestruct "IH" as (n) "IH".
  by iExists (S n).
Qed.
658

659
Lemma test_iInduction_wf (x : nat) P Q :
660
   P - Q -  (x + 0 = x)%nat .
661
662
663
Proof.
  iIntros "#HP HQ".
  iInduction (lt_wf x) as [[|x] _] "IH"; simpl; first done.
664
  rewrite (inj_iff S). by iApply ("IH" with "[%]"); first lia.
665
666
Qed.

667
668
669
670
671
672
673
674
675
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.

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

688
Lemma test_iIntros_start_proof :
Gregory Malecha's avatar
Gregory Malecha committed
689
  @{PROP} True.
690
691
692
693
694
Proof.
  (* Make sure iIntros actually makes progress and enters the proofmode. *)
  progress iIntros. done.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
695
Lemma test_True_intros : (True : PROP) - True.
696
697
698
Proof.
  iIntros "?". done.
Qed.
699
700
701
702
703
704
705
706
707
708

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

712
713
Lemma test_iNext_iRewrite `{!BiInternalEq PROP} P Q :
  <affine>  (Q  P) - <affine>  Q - <affine>  P.
714
Proof.
715
  iIntros "#HPQ HQ !>". iNext. by iRewrite "HPQ" in "HQ".
716
717
Qed.

718
Lemma test_iIntros_modalities `{!BiPersistentlyForall PROP} `(!Absorbing P) :
Gregory Malecha's avatar
Gregory Malecha committed
719
   <pers> (   x : nat,  x = 0    x = 0  - False - P - P).
720
721
722
723
724
Proof.
  iIntros (x ??).
  iIntros "* **". (* Test that fast intros do not work under modalities *)
  iIntros ([]).
Qed.
725

726
727
728
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
729

730
731
Lemma test_iNext_affine `{!BiInternalEq PROP} P Q :
  <affine>  (Q  P) - <affine>  Q - <affine>  P.
732
Proof. iIntros "#HPQ HQ !>". iNext. by iRewrite "HPQ" in "HQ". Qed.
733

734
Lemma test_iAlways P Q R :
735
   P - <pers> Q  R - <pers> <affine> <affine> P   Q.
Ralf Jung's avatar
Ralf Jung committed
736
737
738
739
740
Proof.
  iIntros "#HP #HQ HR". iSplitL.
  - iModIntro. done.
  - iModIntro. done.
Qed.
741

Robbert Krebbers's avatar
Robbert Krebbers committed
742
743
744
(* A bunch of test cases from #127 to establish that tactics behave the same on
`⌜ φ ⌝ → P` and `∀ _ : φ, P` *)
Lemma test_forall_nondep_1 (φ : Prop) :
745
  φ  ( _ : φ, False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
746
747
Proof. iIntros (Hφ) "Hφ". by iApply "Hφ". Qed.
Lemma test_forall_nondep_2 (φ : Prop) :
748
  φ  ( _ : φ, False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
749
750
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" with "[% //]"). done. Qed.
Lemma test_forall_nondep_3 (φ : Prop) :
751
  φ  ( _ : φ, False : PROP) - False.
Ralf Jung's avatar
Ralf Jung committed
752
Proof. iIntros (Hφ) "Hφ". unshelve iSpecialize ("Hφ" $! _); done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
753
Lemma test_forall_nondep_4 (φ : Prop) :
754
  φ  ( _ : φ, False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
755
756
757
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" $! Hφ); done. Qed.

Lemma test_pure_impl_1 (φ : Prop) :
758
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
759
760
Proof. iIntros (Hφ) "Hφ". by iApply "Hφ". Qed.
Lemma test_pure_impl_2 (φ : Prop) :
761
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
762
763
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" with "[% //]"). done. Qed.
Lemma test_pure_impl_3 (φ : Prop) :
764
  φ  (⌜φ⌝  False : PROP) - False.
Ralf Jung's avatar
Ralf Jung committed
765
Proof. iIntros (Hφ) "Hφ". unshelve iSpecialize ("Hφ" $! _); done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
766
Lemma test_pure_impl_4 (φ : Prop) :
767
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
768
769
770
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" $! Hφ). done. Qed.

Lemma test_forall_nondep_impl2 (φ : Prop) P :
771
  φ  P - ( _ : φ, P - False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
772
773
774
775
776
777
778
Proof.
  iIntros (Hφ) "HP Hφ".
  Fail iSpecialize ("Hφ" with "HP").
  iSpecialize ("Hφ" with "[% //] HP"). done.
Qed.

Lemma test_pure_impl2 (φ : Prop) P :
779
  φ  P - (⌜φ⌝  P - False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
780
781
782
783
784
785
Proof.
  iIntros (Hφ) "HP Hφ".
  Fail iSpecialize ("Hφ" with "HP").
  iSpecialize ("Hφ" with "[% //] HP"). done.
Qed.

786
787
788
789
790
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
791
Lemma test_iNext_laterN_later P n :  ^n P - ^n  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
792
Proof. iIntros "H". iNext. by iNext. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
793
Lemma test_iNext_later_laterN P n : ^n  P -  ^n P.
Robbert Krebbers's avatar
Robbert Krebbers committed
794
Proof. iIntros "H". iNext. by iNext. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
795
Lemma test_iNext_plus_1 P n1 n2 :  ^n1 ^n2 P - ^n1 ^n2  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
796
Proof. iIntros "H". iNext. iNext. by iNext. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
797
798
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
799
Check "test_iNext_plus_3".
Robbert Krebbers's avatar
Robbert Krebbers committed
800
801
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).
802
Proof. iIntros "H1 H2". iNext. iNext. iNext. iFrame. Show. iModIntro. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
803

804
805
806
807
808
809
810
811
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.

812
813
814
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.
815
816

Lemma test_specialize_affine_pure (φ : Prop) P :
817
  φ  (<affine> ⌜φ⌝ - P)  P.
818
819
820
821
822
Proof.
  iIntros (Hφ) "H". by iSpecialize ("H" with "[% //]").
Qed.

Lemma test_assert_affine_pure (φ : Prop) P :
823
824
  φ  P  P  <affine> ⌜φ⌝.
Proof. iIntros (Hφ). iAssert (<affine> ⌜φ⌝)%I with "[%]" as "$"; auto. Qed.
825
826
Lemma test_assert_pure (φ : Prop) P :
  φ  P  P  ⌜φ⌝.
827
Proof. iIntros (Hφ). iAssert ⌜φ⌝%I with "[%]" as "$"; auto with iFrame. Qed.
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
863
864
865
866
867
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.

868
Lemma test_iEval x y :  (y + x)%nat = 1  -  S (x + y) = 2%nat  : PROP.
869
870
871
872
873
874
Proof.
  iIntros (H).
  iEval (rewrite (Nat.add_comm x y) // H).
  done.
Qed.

875
876
877
878
879
880
881
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
882
883
884
885
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.

886
887
888
889
890
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.

891
892
893
894
895
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
896
897
898
899
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.

900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
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.

922
Lemma test_iPureIntro_absorbing (φ : Prop) :
Gregory Malecha's avatar
Gregory Malecha committed
923
  φ  @{PROP} <absorb> ⌜φ⌝.
924
925
Proof. intros ?. iPureIntro. done. Qed.

Ralf Jung's avatar
Ralf Jung committed
926
Check "test_iFrame_later_1".
927
Lemma test_iFrame_later_1 P Q : P   Q -  (P   Q).
928
Proof. iIntros "H". iFrame "H". Show. auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
929

Ralf Jung's avatar
Ralf Jung committed
930
Check "test_iFrame_later_2".
931
Lemma test_iFrame_later_2 P Q :  P   Q -  ( P   Q).
932
Proof. iIntros "H". iFrame "H". Show. auto. Qed.
933
934
935
936
937

Lemma test_with_ident P Q R : P - Q - (P - Q - R) - R.
Proof.
  iIntros "? HQ H".
  iMatchHyp (fun H _ =>
938
    iApply ("H" with [spec_patterns.SIdent H []; spec_patterns.SIdent "HQ" []])).
939
Qed.
940
941

Lemma iFrame_with_evar_r P Q :
942
   R, (P - Q - P  R)  R = Q.
943
Proof.
Ralf Jung's avatar
Ralf Jung committed
944
945
946
  eexists. split.
  - iIntros "HP HQ". iFrame. iApply "HQ".
  - done.
947
948
Qed.
Lemma iFrame_with_evar_l P Q :
949
   R, (P - Q - R  P)