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

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

9
Lemma demo_0 P Q :  (P  Q) - ( x, x = 0  x = 1)  (Q  P).
10
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
11
  iIntros "H #H2". iDestruct "H" as "###H".
12
  (* should remove the disjunction "H" *)
13
  iDestruct "H" as "[#?|#?]"; last by iLeft.
14
15
16
17
  (* should keep the disjunction "H" because it is instantiated *)
  iDestruct ("H2" $! 10) as "[%|%]". done. done.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
18
19
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 -
20
21
    P1 - (True  True) -
  (((P2  False  P2  0 = 0)  P3)  Q  P1  True) 
22
     (P2  False)  (False  P5 0).
Robbert Krebbers's avatar
Robbert Krebbers committed
23
24
25
26
27
28
29
30
31
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
32
33
  - iFrame "H3". iRight. auto.
  - iSplitL "HQ". iAssumption. by iSplitL "H1".
Robbert Krebbers's avatar
Robbert Krebbers committed
34
35
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
36
Lemma demo_3 P1 P2 P3 :
Robbert Krebbers's avatar
Robbert Krebbers committed
37
38
  P1  P2  P3 - P1   (P2   x, (P3  x = 0)  P3).
Proof. iIntros "($ & $ & $)". iNext. by iExists 0. Qed.
39

Robbert Krebbers's avatar
Robbert Krebbers committed
40
41
Definition foo (P : PROP) := (P - P)%I.
Definition bar : PROP := ( P, foo P)%I.
42

Robbert Krebbers's avatar
Robbert Krebbers committed
43
44
Lemma test_unfold_constants : bar.
Proof. iIntros (P) "HP //". Qed.
45

Robbert Krebbers's avatar
Robbert Krebbers committed
46
Lemma test_iRewrite {A : ofeT} (x y : A) P :
47
   ( z, P - <affine> (z  y)) - (P - P  (x,x)  (y,x)).
48
Proof.
49
  iIntros "#H1 H2".
Robbert Krebbers's avatar
Robbert Krebbers committed
50
  iRewrite (bi.internal_eq_sym x x with "[# //]").
51
  iRewrite -("H1" $! _ with "[- //]").
Robbert Krebbers's avatar
Robbert Krebbers committed
52
  auto.
53
54
Qed.

55
Lemma test_iDestruct_and_emp P Q `{!Persistent P, !Persistent Q} :
56
  P  emp - emp  Q - <affine> (P  Q).
57
58
59
Proof. iIntros "[#? _] [_ #?]". auto. Qed.

Lemma test_iIntros_persistent P Q `{!Persistent Q} : (P  Q  P  Q)%I.
60
Proof. iIntros "H1 #H2". by iFrame "∗#". Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
61

62
63
64
Lemma test_iIntros_pure (ψ φ : Prop) P : ψ  ( φ   P   φ  ψ   P)%I.
Proof. iIntros (??) "H". auto. Qed.

65
66
67
Lemma test_iIntros_pure_not : ( ¬False  : PROP)%I.
Proof. by iIntros (?). Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
68
Lemma test_fast_iIntros P Q :
69
70
  ( x y z : nat,
    x = plus 0 x  y = 0  z = 0  P   Q  foo (x  x))%I.
71
Proof.
72
  iIntros (a) "*".
73
  iIntros "#Hfoo **".
Robbert Krebbers's avatar
Robbert Krebbers committed
74
  iIntros "_ //".
75
Qed.
76

77
Lemma test_very_fast_iIntros P :
Robbert Krebbers's avatar
Robbert Krebbers committed
78
   x y : nat, ( x = y   P - P)%I.
79
80
Proof. by iIntros. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
81
82
83
84
85
(** Prior to 0b84351c this used to loop, now `iAssumption` instantiates `R` with
`False` and performs false elimination. *)
Lemma test_iAssumption_evar_ex_false :  R, R   P, P.
Proof. eexists. iIntros "?" (P). iAssumption. Qed.

86
87
88
Lemma test_iAssumption_affine P Q R `{!Affine P, !Affine R} : P - Q - R - Q.
Proof. iIntros "H1 H2 H3". iAssumption. Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
92
Lemma test_iAssert_persistent P Q : P - Q - True.
Robbert Krebbers's avatar
Robbert Krebbers committed
93
94
95
96
97
98
99
100
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.
101

102
103
104
105
106
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
107
Lemma test_iSpecialize_auto_frame P Q R :
108
  (P - True - True - Q - R) - P - Q - R.
109
Proof. iIntros "H ? HQ". by iApply ("H" with "[$]"). Qed.
110

111
112
113
114
Lemma test_iEmp_intro P Q R `{!Affine P, !Persistent Q, !Affine R} :
  P - Q  R - emp.
Proof. iIntros "HP #HQ HR". iEmpIntro. Qed.

115
116
117
118
119
120
121
122
123
124
125
Let test_fresh P Q:
  (P  Q) - (P  Q).
Proof.
  iIntros "H".
  let H1 := iFresh in
  let H2 := iFresh in
  let pat :=constr:(IList [cons (IIdent H1) (cons (IIdent H2) nil)]) in 
  iDestruct "H" as pat.
  iFrame.
Qed.

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

130
131
132
133
Lemma test_iExist_tc `{Collection A C} P : ( x1 x2 : gset positive, P - P)%I.
Proof. iExists {[ 1%positive ]}, . auto. Qed.

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

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

144
145
146
147
148
149
150
151
152
153
154
155
156
157
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.

Robbert Krebbers's avatar
Robbert Krebbers committed
158
159
160
Lemma test_iAssert_modality P :  False -  P.
Proof.
  iIntros "HF".
161
  iAssert (<affine> False)%I with "[> -]" as %[].
Robbert Krebbers's avatar
Robbert Krebbers committed
162
163
  by iMod "HF".
Qed.
164

165
Lemma test_iMod_affinely_timeless P `{!Timeless P} :
166
  <affine>  P -  <affine> P.
167
168
Proof. iIntros "H". iMod "H". done. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
169
Lemma test_iAssumption_False P : False - P.
170
Proof. iIntros "H". done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
171
172

(* Check instantiation and dependent types *)
Robbert Krebbers's avatar
Robbert Krebbers committed
173
Lemma test_iSpecialize_dependent_type (P :  n, vec nat n  PROP) :
Robbert Krebbers's avatar
Robbert Krebbers committed
174
175
176
177
178
  ( 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
179

180
181
182
183
184
185
186
187
188
(* 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".
  iDestruct (bi.big_sepL_elem_of _ _ _ Hp with "HT") as "Hp".
  done.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
189
190
Lemma test_eauto_iFrame P Q R `{!Persistent R} :
  P - Q - R  R  Q  P  R  False.
191
Proof. eauto 10 with iFrame. Qed.
192

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

Robbert Krebbers's avatar
Robbert Krebbers committed
197
Lemma test_iNext_evar P : P - True.
Ralf Jung's avatar
Ralf Jung committed
198
199
200
201
Proof.
  iIntros "HP". iAssert ( _ -  P)%I as "?"; last done.
  iIntros "?". iNext. iAssumption.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
202

203
204
Lemma test_iNext_sep1 P Q (R1 := (P  Q)%I) :
  ( P   Q)  R1 -  ((P  Q)  R1).
Robbert Krebbers's avatar
Robbert Krebbers committed
205
206
207
208
Proof.
  iIntros "H". iNext.
  rewrite {1 2}(lock R1). (* check whether R1 has not been unfolded *) done.
Qed.
209

Robbert Krebbers's avatar
Robbert Krebbers committed
210
Lemma test_iNext_sep2 P Q :  P   Q -  (P  Q).
211
212
213
Proof.
  iIntros "H". iNext. iExact "H". (* Check that the laters are all gone. *)
Qed.
214

Robbert Krebbers's avatar
Robbert Krebbers committed
215
Lemma test_iNext_quantifier {A} (Φ : A  A  PROP) :
Robbert Krebbers's avatar
Robbert Krebbers committed
216
217
218
  ( y,  x,  Φ x y) -  ( y,  x, Φ x y).
Proof. iIntros "H". iNext. done. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
219
Lemma test_iFrame_persistent (P Q : PROP) :
220
   P - Q - <pers> (P  P)  (P  Q  Q).
221
Proof. iIntros "#HP". iFrame "HP". iIntros "$". Qed.
222

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

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

229
Lemma test_iDestruct_persistent P (Φ : nat  PROP) `{! x, Persistent (Φ x)}:
230
   (P -  x, Φ x) -
231
232
233
234
235
  P -  x, Φ x  P.
Proof.
  iIntros "#H HP". iDestruct ("H" with "HP") as (x) "#H2". eauto with iFrame.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
236
237
238
239
240
Lemma test_iLöb P : ( n, ^n P)%I.
Proof.
  iLöb as "IH". iDestruct "IH" as (n) "IH".
  by iExists (S n).
Qed.
241

242
Lemma test_iInduction_wf (x : nat) P Q :
243
   P - Q -  (x + 0 = x)%nat .
244
245
246
247
248
249
Proof.
  iIntros "#HP HQ".
  iInduction (lt_wf x) as [[|x] _] "IH"; simpl; first done.
  rewrite (inj_iff S). by iApply ("IH" with "[%]"); first omega.
Qed.

250
Lemma test_iIntros_start_proof :
Robbert Krebbers's avatar
Robbert Krebbers committed
251
  (True : PROP)%I.
252
253
254
255
256
Proof.
  (* Make sure iIntros actually makes progress and enters the proofmode. *)
  progress iIntros. done.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
257
Lemma test_True_intros : (True : PROP) - True.
258
259
260
Proof.
  iIntros "?". done.
Qed.
261
262
263
264
265
266
267
268
269
270

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

274
Lemma test_foo P Q : <affine>  (Q  P) - <affine>  Q - <affine>  P.
275
Proof.
276
  iIntros "#HPQ HQ !#". iNext. by iRewrite "HPQ" in "HQ".
277
278
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
279
Lemma test_iIntros_modalities `(!Absorbing P) :
280
  (<pers> (   x : nat,  x = 0    x = 0  - False - P - P))%I.
281
282
283
284
285
Proof.
  iIntros (x ??).
  iIntros "* **". (* Test that fast intros do not work under modalities *)
  iIntros ([]).
Qed.
286

287
288
289
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
290

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

294
Lemma test_iAlways P Q R :
295
   P - <pers> Q  R - <pers> <affine> <affine> P   Q.
296
Proof. iIntros "#HP #HQ HR". iSplitL. iAlways. done. iAlways. done. Qed.
297

Robbert Krebbers's avatar
Robbert Krebbers committed
298
299
300
(* A bunch of test cases from #127 to establish that tactics behave the same on
`⌜ φ ⌝ → P` and `∀ _ : φ, P` *)
Lemma test_forall_nondep_1 (φ : Prop) :
301
  φ  ( _ : φ, False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
302
303
Proof. iIntros (Hφ) "Hφ". by iApply "Hφ". Qed.
Lemma test_forall_nondep_2 (φ : Prop) :
304
  φ  ( _ : φ, False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
305
306
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" with "[% //]"). done. Qed.
Lemma test_forall_nondep_3 (φ : Prop) :
307
  φ  ( _ : φ, False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
308
309
Proof. iIntros (Hφ) "Hφ". unshelve iSpecialize ("Hφ" $! _). done. done. Qed.
Lemma test_forall_nondep_4 (φ : Prop) :
310
  φ  ( _ : φ, False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
311
312
313
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" $! Hφ); done. Qed.

Lemma test_pure_impl_1 (φ : Prop) :
314
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
315
316
Proof. iIntros (Hφ) "Hφ". by iApply "Hφ". Qed.
Lemma test_pure_impl_2 (φ : Prop) :
317
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
318
319
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" with "[% //]"). done. Qed.
Lemma test_pure_impl_3 (φ : Prop) :
320
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
321
322
Proof. iIntros (Hφ) "Hφ". unshelve iSpecialize ("Hφ" $! _). done. done. Qed.
Lemma test_pure_impl_4 (φ : Prop) :
323
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
324
325
326
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" $! Hφ). done. Qed.

Lemma test_forall_nondep_impl2 (φ : Prop) P :
327
  φ  P - ( _ : φ, P - False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
328
329
330
331
332
333
334
Proof.
  iIntros (Hφ) "HP Hφ".
  Fail iSpecialize ("Hφ" with "HP").
  iSpecialize ("Hφ" with "[% //] HP"). done.
Qed.

Lemma test_pure_impl2 (φ : Prop) P :
335
  φ  P - (⌜φ⌝  P - False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
336
337
338
339
340
341
Proof.
  iIntros (Hφ) "HP Hφ".
  Fail iSpecialize ("Hφ" with "HP").
  iSpecialize ("Hφ" with "[% //] HP"). done.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
342
Lemma test_iNext_laterN_later P n :  ^n P - ^n  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
343
Proof. iIntros "H". iNext. by iNext. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
344
Lemma test_iNext_later_laterN P n : ^n  P -  ^n P.
Robbert Krebbers's avatar
Robbert Krebbers committed
345
Proof. iIntros "H". iNext. by iNext. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
346
Lemma test_iNext_plus_1 P n1 n2 :  ^n1 ^n2 P - ^n1 ^n2  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
347
Proof. iIntros "H". iNext. iNext. by iNext. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
348
349
350
351
352
Lemma test_iNext_plus_2 P n m : ^n ^m P - ^(n+m) P.
Proof. iIntros "H". iNext. done. Qed.
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).
Proof. iIntros "H1 H2". iNext. iNext. iNext. iFrame. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
353

354
355
356
357
358
359
360
361
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.

362
363
364
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.
365
366

Lemma test_specialize_affine_pure (φ : Prop) P :
367
  φ  (<affine> ⌜φ⌝ - P)  P.
368
369
370
371
372
Proof.
  iIntros (Hφ) "H". by iSpecialize ("H" with "[% //]").
Qed.

Lemma test_assert_affine_pure (φ : Prop) P :
373
374
  φ  P  P  <affine> ⌜φ⌝.
Proof. iIntros (Hφ). iAssert (<affine> ⌜φ⌝)%I with "[%]" as "$"; auto. Qed.
375
376
Lemma test_assert_pure (φ : Prop) P :
  φ  P  P  ⌜φ⌝.
377
Proof. iIntros (Hφ). iAssert ⌜φ⌝%I with "[%]" as "$"; auto with iFrame. Qed.
378

379
Lemma test_iEval x y :  (y + x)%nat = 1  -  S (x + y) = 2%nat  : PROP.
380
381
382
383
384
385
Proof.
  iIntros (H).
  iEval (rewrite (Nat.add_comm x y) // H).
  done.
Qed.

386
387
Lemma test_iFrame_later_1 P Q : P   Q -  (P   Q).
Proof. iIntros "H". iFrame "H". auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
388

389
390
Lemma test_iFrame_later_2 P Q :  P   Q -  ( P   Q).
Proof. iIntros "H". iFrame "H". auto. Qed.
391
392
393
394
395
396
397

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

Lemma iFrame_with_evar_r P Q :
400
   R, (P - Q - P  R)  R = Q.
401
Proof.
402
  eexists. split. iIntros "HP HQ". iFrame. iApply "HQ". done.
403
404
Qed.
Lemma iFrame_with_evar_l P Q :
405
   R, (P - Q - R  P)  R = Q.
406
Proof.
407
408
  eexists. split. iIntros "HP HQ". Fail iFrame "HQ".
  by iSplitR "HP". done.
409
Qed.
410
411
412
413
414
415
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
416
417
418
419
420
421
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
422
Lemma test_iAssumption_evar P :  R, (R  P)  R = P.
423
424
425
426
427
428
429
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
430
431
432
Lemma test_iAssumption_False_no_loop :  R, R   P, P.
Proof. eexists. iIntros "?" (P). done. Qed.

433
434
435
436
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
437
438
439
440
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.

Ralf Jung's avatar
Ralf Jung committed
441
End tests.