proofmode.v 17.2 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.
11
  iIntros "H #H2". Show. iDestruct "H" as "###H".
12
  (* should remove the disjunction "H" *)
13
  iDestruct "H" as "[#?|#?]"; last by iLeft. Show.
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

40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72
(* Test line breaking of long assumptions. *)
Section linebreaks.
Lemma print_long_line P :
  (P  P  P  P  P  P  P  P  P  P)  P  P  P  P  P  P  P  P  P
  - P.
Proof.
  iIntros "HP". Show.
Abort.
Lemma print_long_line_anon P :
  (P  P  P  P  P  P  P  P  P  P)  P  P  P  P  P  P  P  P  P
  - P.
Proof.
  iIntros "?". Show.
Abort.

(* This is specifically crafted such that not having the `hv` in
   the proofmode notation breaks the output. *)
Local Notation "'TESTNOTATION' '{{' P '|' Q '}' '}'" := (P  Q)%I
  (format "'TESTNOTATION'  '{{'  P  '|'  Q  '}' '}'") : bi_scope.
Lemma print_long_line P :
  TESTNOTATION {{ P  P  P  P  P  P  P  P  P  P  P  P  P | P  P  P  P  P  P  P }}
  - P.
Proof.
  iIntros "HP". Show.
Abort.
Lemma print_long_line_anon P :
  TESTNOTATION {{ P  P  P  P  P  P  P  P  P  P  P  P  P | P  P  P  P  P  P  P }}
  - P.
Proof.
  iIntros "?". Show.
Abort.
End linebreaks.

Robbert Krebbers's avatar
Robbert Krebbers committed
73 74
Definition foo (P : PROP) := (P - P)%I.
Definition bar : PROP := ( P, foo P)%I.
75

Robbert Krebbers's avatar
Robbert Krebbers committed
76 77
Lemma test_unfold_constants : bar.
Proof. iIntros (P) "HP //". Qed.
78

Robbert Krebbers's avatar
Robbert Krebbers committed
79
Lemma test_iRewrite {A : ofeT} (x y : A) P :
80
   ( z, P - <affine> (z  y)) - (P - P  (x,x)  (y,x)).
81
Proof.
82
  iIntros "#H1 H2".
Robbert Krebbers's avatar
Robbert Krebbers committed
83
  iRewrite (bi.internal_eq_sym x x with "[# //]").
84
  iRewrite -("H1" $! _ with "[- //]").
Robbert Krebbers's avatar
Robbert Krebbers committed
85
  auto.
86 87
Qed.

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

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

95 96 97
Lemma test_iIntros_pure (ψ φ : Prop) P : ψ  ( φ   P   φ  ψ   P)%I.
Proof. iIntros (??) "H". auto. Qed.

98 99 100
Lemma test_iIntros_pure_not : ( ¬False  : PROP)%I.
Proof. by iIntros (?). Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
101
Lemma test_fast_iIntros P Q :
102 103
  ( x y z : nat,
    x = plus 0 x  y = 0  z = 0  P   Q  foo (x  x))%I.
104
Proof.
105
  iIntros (a) "*".
106
  iIntros "#Hfoo **".
Robbert Krebbers's avatar
Robbert Krebbers committed
107
  iIntros "_ //".
108
Qed.
109

110
Lemma test_very_fast_iIntros P :
Robbert Krebbers's avatar
Robbert Krebbers committed
111
   x y : nat, ( x = y   P - P)%I.
112 113
Proof. by iIntros. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
114 115 116 117 118
(** 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.

119 120 121
Lemma test_iAssumption_affine P Q R `{!Affine P, !Affine R} : P - Q - R - Q.
Proof. iIntros "H1 H2 H3". iAssumption. Qed.

122 123 124
Lemma test_done_goal_evar Q :  P, Q  P.
Proof. eexists. iIntros "H". Fail done. iAssumption. Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
128
Lemma test_iAssert_persistent P Q : P - Q - True.
Robbert Krebbers's avatar
Robbert Krebbers committed
129 130 131 132 133 134 135 136
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.
137

138 139 140 141 142
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
143
Lemma test_iSpecialize_auto_frame P Q R :
144
  (P - True - True - Q - R) - P - Q - R.
145
Proof. iIntros "H ? HQ". by iApply ("H" with "[$]"). Qed.
146

147 148 149 150
Lemma test_iEmp_intro P Q R `{!Affine P, !Persistent Q, !Affine R} :
  P - Q  R - emp.
Proof. iIntros "HP #HQ HR". iEmpIntro. Qed.

Ralf Jung's avatar
Ralf Jung committed
151
Lemma test_fresh P Q:
152 153 154 155 156 157 158 159 160 161
  (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.

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

166 167 168 169
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.
170 171
Proof.
  iIntros "H".
Ralf Jung's avatar
Ralf Jung committed
172
  (* FIXME: this [unshelve] and [apply _] should not be needed. *)
173 174
  unshelve iSpecialize ("H" $!  {[ 1%positive ]} ); try apply _. done.
Qed.
175

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

180 181 182 183 184 185 186 187 188 189 190 191 192 193
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.

194 195 196
Lemma test_iFrame_later `{BiAffine PROP} P Q : P - Q -  P  Q.
Proof. iIntros "H1 H2". by iFrame "H1". Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
197 198 199
Lemma test_iAssert_modality P :  False -  P.
Proof.
  iIntros "HF".
200
  iAssert (<affine> False)%I with "[> -]" as %[].
Robbert Krebbers's avatar
Robbert Krebbers committed
201 202
  by iMod "HF".
Qed.
203

204
Lemma test_iMod_affinely_timeless P `{!Timeless P} :
205
  <affine>  P -  <affine> P.
206 207
Proof. iIntros "H". iMod "H". done. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
208
Lemma test_iAssumption_False P : False - P.
209
Proof. iIntros "H". done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
210 211

(* Check instantiation and dependent types *)
Robbert Krebbers's avatar
Robbert Krebbers committed
212
Lemma test_iSpecialize_dependent_type (P :  n, vec nat n  PROP) :
Robbert Krebbers's avatar
Robbert Krebbers committed
213 214 215 216 217
  ( 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
218

219 220 221 222 223
(* 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".
224
  iDestruct (big_sepL_elem_of _ _ _ Hp with "HT") as "Hp".
225 226 227
  done.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
228 229
Lemma test_eauto_iFrame P Q R `{!Persistent R} :
  P - Q - R  R  Q  P  R  False.
230
Proof. eauto 10 with iFrame. Qed.
231

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

236 237 238 239
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
240
Lemma test_iNext_evar P : P - True.
Ralf Jung's avatar
Ralf Jung committed
241 242 243 244
Proof.
  iIntros "HP". iAssert ( _ -  P)%I as "?"; last done.
  iIntros "?". iNext. iAssumption.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
245

246 247
Lemma test_iNext_sep1 P Q (R1 := (P  Q)%I) :
  ( P   Q)  R1 -  ((P  Q)  R1).
Robbert Krebbers's avatar
Robbert Krebbers committed
248 249 250 251
Proof.
  iIntros "H". iNext.
  rewrite {1 2}(lock R1). (* check whether R1 has not been unfolded *) done.
Qed.
252

Robbert Krebbers's avatar
Robbert Krebbers committed
253
Lemma test_iNext_sep2 P Q :  P   Q -  (P  Q).
254 255 256
Proof.
  iIntros "H". iNext. iExact "H". (* Check that the laters are all gone. *)
Qed.
257

Robbert Krebbers's avatar
Robbert Krebbers committed
258
Lemma test_iNext_quantifier {A} (Φ : A  A  PROP) :
Robbert Krebbers's avatar
Robbert Krebbers committed
259 260 261
  ( y,  x,  Φ x y) -  ( y,  x, Φ x y).
Proof. iIntros "H". iNext. done. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
262
Lemma test_iFrame_persistent (P Q : PROP) :
263
   P - Q - <pers> (P  P)  (P  Q  Q).
264
Proof. iIntros "#HP". iFrame "HP". iIntros "$". Qed.
265

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

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

272
Lemma test_iDestruct_persistent P (Φ : nat  PROP) `{! x, Persistent (Φ x)}:
273
   (P -  x, Φ x) -
274 275 276 277 278
  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
279 280 281 282 283
Lemma test_iLöb P : ( n, ^n P)%I.
Proof.
  iLöb as "IH". iDestruct "IH" as (n) "IH".
  by iExists (S n).
Qed.
284

285
Lemma test_iInduction_wf (x : nat) P Q :
286
   P - Q -  (x + 0 = x)%nat .
287 288 289 290 291 292
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.

293
Lemma test_iIntros_start_proof :
Robbert Krebbers's avatar
Robbert Krebbers committed
294
  (True : PROP)%I.
295 296 297 298 299
Proof.
  (* Make sure iIntros actually makes progress and enters the proofmode. *)
  progress iIntros. done.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
300
Lemma test_True_intros : (True : PROP) - True.
301 302 303
Proof.
  iIntros "?". done.
Qed.
304 305 306 307 308 309 310 311 312 313

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

317
Lemma test_foo P Q : <affine>  (Q  P) - <affine>  Q - <affine>  P.
318
Proof.
319
  iIntros "#HPQ HQ !#". iNext. by iRewrite "HPQ" in "HQ".
320 321
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
322
Lemma test_iIntros_modalities `(!Absorbing P) :
323
  (<pers> (   x : nat,  x = 0    x = 0  - False - P - P))%I.
324 325 326 327 328
Proof.
  iIntros (x ??).
  iIntros "* **". (* Test that fast intros do not work under modalities *)
  iIntros ([]).
Qed.
329

330 331 332
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
333

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

337
Lemma test_iAlways P Q R :
338
   P - <pers> Q  R - <pers> <affine> <affine> P   Q.
339
Proof. iIntros "#HP #HQ HR". iSplitL. iAlways. done. iAlways. done. Qed.
340

Robbert Krebbers's avatar
Robbert Krebbers committed
341 342 343
(* A bunch of test cases from #127 to establish that tactics behave the same on
`⌜ φ ⌝ → P` and `∀ _ : φ, P` *)
Lemma test_forall_nondep_1 (φ : Prop) :
344
  φ  ( _ : φ, False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
345 346
Proof. iIntros (Hφ) "Hφ". by iApply "Hφ". Qed.
Lemma test_forall_nondep_2 (φ : Prop) :
347
  φ  ( _ : φ, False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
348 349
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" with "[% //]"). done. Qed.
Lemma test_forall_nondep_3 (φ : Prop) :
350
  φ  ( _ : φ, False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
351 352
Proof. iIntros (Hφ) "Hφ". unshelve iSpecialize ("Hφ" $! _). done. done. Qed.
Lemma test_forall_nondep_4 (φ : Prop) :
353
  φ  ( _ : φ, False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
354 355 356
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" $! Hφ); done. Qed.

Lemma test_pure_impl_1 (φ : Prop) :
357
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
358 359
Proof. iIntros (Hφ) "Hφ". by iApply "Hφ". Qed.
Lemma test_pure_impl_2 (φ : Prop) :
360
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
361 362
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" with "[% //]"). done. Qed.
Lemma test_pure_impl_3 (φ : Prop) :
363
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
364 365
Proof. iIntros (Hφ) "Hφ". unshelve iSpecialize ("Hφ" $! _). done. done. Qed.
Lemma test_pure_impl_4 (φ : Prop) :
366
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
367 368 369
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" $! Hφ). done. Qed.

Lemma test_forall_nondep_impl2 (φ : Prop) P :
370
  φ  P - ( _ : φ, P - False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
371 372 373 374 375 376 377
Proof.
  iIntros (Hφ) "HP Hφ".
  Fail iSpecialize ("Hφ" with "HP").
  iSpecialize ("Hφ" with "[% //] HP"). done.
Qed.

Lemma test_pure_impl2 (φ : Prop) P :
378
  φ  P - (⌜φ⌝  P - False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
379 380 381 382 383 384
Proof.
  iIntros (Hφ) "HP Hφ".
  Fail iSpecialize ("Hφ" with "HP").
  iSpecialize ("Hφ" with "[% //] HP"). done.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
385
Lemma test_iNext_laterN_later P n :  ^n P - ^n  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
386
Proof. iIntros "H". iNext. by iNext. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
387
Lemma test_iNext_later_laterN P n : ^n  P -  ^n P.
Robbert Krebbers's avatar
Robbert Krebbers committed
388
Proof. iIntros "H". iNext. by iNext. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
389
Lemma test_iNext_plus_1 P n1 n2 :  ^n1 ^n2 P - ^n1 ^n2  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
390
Proof. iIntros "H". iNext. iNext. by iNext. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
391 392 393 394 395
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
396

397 398 399 400 401 402 403 404
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.

405 406 407
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.
408 409

Lemma test_specialize_affine_pure (φ : Prop) P :
410
  φ  (<affine> ⌜φ⌝ - P)  P.
411 412 413 414 415
Proof.
  iIntros (Hφ) "H". by iSpecialize ("H" with "[% //]").
Qed.

Lemma test_assert_affine_pure (φ : Prop) P :
416 417
  φ  P  P  <affine> ⌜φ⌝.
Proof. iIntros (Hφ). iAssert (<affine> ⌜φ⌝)%I with "[%]" as "$"; auto. Qed.
418 419
Lemma test_assert_pure (φ : Prop) P :
  φ  P  P  ⌜φ⌝.
420
Proof. iIntros (Hφ). iAssert ⌜φ⌝%I with "[%]" as "$"; auto with iFrame. Qed.
421

422
Lemma test_iEval x y :  (y + x)%nat = 1  -  S (x + y) = 2%nat  : PROP.
423 424 425 426 427 428
Proof.
  iIntros (H).
  iEval (rewrite (Nat.add_comm x y) // H).
  done.
Qed.

429
Lemma test_iIntros_pure_neg : ( ¬False  : PROP)%I.
430
Proof. by iIntros (?). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
431

432 433 434 435
Lemma test_iPureIntro_absorbing (φ : Prop) :
  φ  sbi_emp_valid (PROP:=PROP) (<absorb> ⌜φ⌝)%I.
Proof. intros ?. iPureIntro. done. Qed.

436 437
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
438

439 440
Lemma test_iFrame_later_2 P Q :  P   Q -  ( P   Q).
Proof. iIntros "H". iFrame "H". auto. Qed.
441 442 443 444 445 446 447

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.
448 449

Lemma iFrame_with_evar_r P Q :
450
   R, (P - Q - P  R)  R = Q.
451
Proof.
452
  eexists. split. iIntros "HP HQ". iFrame. iApply "HQ". done.
453 454
Qed.
Lemma iFrame_with_evar_l P Q :
455
   R, (P - Q - R  P)  R = Q.
456
Proof.
457
  eexists. split. iIntros "HP HQ". Fail iFrame "HQ".
458
  iSplitR "HP"; iAssumption. done.
459
Qed.
460 461 462 463 464 465
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
466 467 468 469 470 471
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
472
Lemma test_iAssumption_evar P :  R, (R  P)  R = P.
473 474 475 476 477 478 479
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
480 481 482
Lemma test_iAssumption_False_no_loop :  R, R   P, P.
Proof. eexists. iIntros "?" (P). done. Qed.

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

491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506
Lemma test_and_sep (P Q R : PROP) : P  (Q   R)  (P  Q)   R.
Proof.
  iIntros "H". repeat iSplit.
  - iDestruct "H" as "[$ _]".
  - iDestruct "H" as "[_ [$ _]]".
  - iDestruct "H" as "[_ [_ #$]]".
Qed.

Lemma test_and_sep_2 (P Q R : PROP) `{!Persistent R, !Affine R} :
  P  (Q  R)  (P  Q)  R.
Proof.
  iIntros "H". repeat iSplit.
  - iDestruct "H" as "[$ _]".
  - iDestruct "H" as "[_ [$ _]]".
  - iDestruct "H" as "[_ [_ #$]]".
Qed.
507 508 509 510 511 512

Lemma test_and_sep_affine_bi `{BiAffine PROP} P Q :  P  Q   P  Q.
Proof.
  iIntros "[??]". iSplit; last done.
  lazymatch goal with |- coq_tactics.envs_entails _ ( P) => done end.
Qed.
Ralf Jung's avatar
Ralf Jung committed
513
End tests.