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

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

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

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

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

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

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

Ralf Jung's avatar
Ralf Jung committed
56
Check "test_iDestruct_and_emp".
57
Lemma test_iDestruct_and_emp P Q `{!Persistent P, !Persistent Q} :
58
  P  emp - emp  Q - <affine> (P  Q).
Ralf Jung's avatar
Ralf Jung committed
59
Proof. iIntros "[#? _] [_ #?]". Show. auto. Qed.
60 61

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

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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
83 84 85 86 87
(** 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.

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

91 92 93
Lemma test_done_goal_evar Q :  P, Q  P.
Proof. eexists. iIntros "H". Fail done. iAssumption. Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
97
Lemma test_iAssert_persistent P Q : P - Q - True.
Robbert Krebbers's avatar
Robbert Krebbers committed
98 99 100 101 102 103 104 105
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.
106

107 108 109 110 111
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
112
Lemma test_iSpecialize_auto_frame P Q R :
113
  (P - True - True - Q - R) - P - Q - R.
114
Proof. iIntros "H ? HQ". by iApply ("H" with "[$]"). Qed.
115

Ralf Jung's avatar
Ralf Jung committed
116 117 118 119
Lemma test_iSpecialize_pure (φ : Prop) Q R:
  φ  (⌜φ⌝ - Q)  Q.
Proof. iIntros (HP HPQ). iDestruct (HPQ $! HP) as "?". done. Qed.

120 121 122 123
Lemma test_iSpecialize_Coq_entailment P Q R :
  P  (P - Q)  Q.
Proof. iIntros (HP HPQ). iDestruct (HPQ $! HP) as "?". done. Qed.

124 125 126 127
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
128
Lemma test_fresh P Q:
129 130 131 132 133 134 135 136 137 138
  (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.

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

143 144 145 146
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.
147 148
Proof.
  iIntros "H".
Ralf Jung's avatar
Ralf Jung committed
149
  (* FIXME: this [unshelve] and [apply _] should not be needed. *)
150 151
  unshelve iSpecialize ("H" $!  {[ 1%positive ]} ); try apply _. done.
Qed.
152

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

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

171 172 173
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
174 175 176
Lemma test_iAssert_modality P :  False -  P.
Proof.
  iIntros "HF".
177
  iAssert (<affine> False)%I with "[> -]" as %[].
Robbert Krebbers's avatar
Robbert Krebbers committed
178 179
  by iMod "HF".
Qed.
180

181
Lemma test_iMod_affinely_timeless P `{!Timeless P} :
182
  <affine>  P -  <affine> P.
183 184
Proof. iIntros "H". iMod "H". done. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
185
Lemma test_iAssumption_False P : False - P.
186
Proof. iIntros "H". done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
187 188

(* Check instantiation and dependent types *)
Robbert Krebbers's avatar
Robbert Krebbers committed
189
Lemma test_iSpecialize_dependent_type (P :  n, vec nat n  PROP) :
Robbert Krebbers's avatar
Robbert Krebbers committed
190 191 192 193 194
  ( 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
195

196 197 198 199 200
(* 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".
201
  iDestruct (big_sepL_elem_of _ _ _ Hp with "HT") as "Hp".
202 203 204
  done.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
205 206
Lemma test_eauto_iFrame P Q R `{!Persistent R} :
  P - Q - R  R  Q  P  R  False.
207
Proof. eauto 10 with iFrame. Qed.
208

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

213 214 215 216
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
217
Lemma test_iNext_evar P : P - True.
Ralf Jung's avatar
Ralf Jung committed
218 219 220 221
Proof.
  iIntros "HP". iAssert ( _ -  P)%I as "?"; last done.
  iIntros "?". iNext. iAssumption.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
222

223 224
Lemma test_iNext_sep1 P Q (R1 := (P  Q)%I) :
  ( P   Q)  R1 -  ((P  Q)  R1).
Robbert Krebbers's avatar
Robbert Krebbers committed
225 226 227 228
Proof.
  iIntros "H". iNext.
  rewrite {1 2}(lock R1). (* check whether R1 has not been unfolded *) done.
Qed.
229

Robbert Krebbers's avatar
Robbert Krebbers committed
230
Lemma test_iNext_sep2 P Q :  P   Q -  (P  Q).
231 232 233
Proof.
  iIntros "H". iNext. iExact "H". (* Check that the laters are all gone. *)
Qed.
234

Robbert Krebbers's avatar
Robbert Krebbers committed
235
Lemma test_iNext_quantifier {A} (Φ : A  A  PROP) :
Robbert Krebbers's avatar
Robbert Krebbers committed
236 237 238
  ( y,  x,  Φ x y) -  ( y,  x, Φ x y).
Proof. iIntros "H". iNext. done. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
239
Lemma test_iFrame_persistent (P Q : PROP) :
240
   P - Q - <pers> (P  P)  (P  Q  Q).
241
Proof. iIntros "#HP". iFrame "HP". iIntros "$". Qed.
242

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

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

249
Lemma test_iDestruct_persistent P (Φ : nat  PROP) `{! x, Persistent (Φ x)}:
250
   (P -  x, Φ x) -
251 252 253 254 255
  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
256 257 258 259 260
Lemma test_iLöb P : ( n, ^n P)%I.
Proof.
  iLöb as "IH". iDestruct "IH" as (n) "IH".
  by iExists (S n).
Qed.
261

262
Lemma test_iInduction_wf (x : nat) P Q :
263
   P - Q -  (x + 0 = x)%nat .
264 265 266 267 268 269
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.

270 271 272 273 274 275 276 277 278
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.

279
Lemma test_iIntros_start_proof :
Robbert Krebbers's avatar
Robbert Krebbers committed
280
  (True : PROP)%I.
281 282 283 284 285
Proof.
  (* Make sure iIntros actually makes progress and enters the proofmode. *)
  progress iIntros. done.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
286
Lemma test_True_intros : (True : PROP) - True.
287 288 289
Proof.
  iIntros "?". done.
Qed.
290 291 292 293 294 295 296 297 298 299

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

303
Lemma test_foo P Q : <affine>  (Q  P) - <affine>  Q - <affine>  P.
304
Proof.
305
  iIntros "#HPQ HQ !#". iNext. by iRewrite "HPQ" in "HQ".
306 307
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
308
Lemma test_iIntros_modalities `(!Absorbing P) :
309
  (<pers> (   x : nat,  x = 0    x = 0  - False - P - P))%I.
310 311 312 313 314
Proof.
  iIntros (x ??).
  iIntros "* **". (* Test that fast intros do not work under modalities *)
  iIntros ([]).
Qed.
315

316 317 318
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
319

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

323
Lemma test_iAlways P Q R :
324
   P - <pers> Q  R - <pers> <affine> <affine> P   Q.
325
Proof. iIntros "#HP #HQ HR". iSplitL. iAlways. done. iAlways. done. Qed.
326

Robbert Krebbers's avatar
Robbert Krebbers committed
327 328 329
(* A bunch of test cases from #127 to establish that tactics behave the same on
`⌜ φ ⌝ → P` and `∀ _ : φ, P` *)
Lemma test_forall_nondep_1 (φ : Prop) :
330
  φ  ( _ : φ, False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
331 332
Proof. iIntros (Hφ) "Hφ". by iApply "Hφ". Qed.
Lemma test_forall_nondep_2 (φ : Prop) :
333
  φ  ( _ : φ, False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
334 335
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" with "[% //]"). done. Qed.
Lemma test_forall_nondep_3 (φ : Prop) :
336
  φ  ( _ : φ, False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
337 338
Proof. iIntros (Hφ) "Hφ". unshelve iSpecialize ("Hφ" $! _). done. done. Qed.
Lemma test_forall_nondep_4 (φ : Prop) :
339
  φ  ( _ : φ, False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
340 341 342
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" $! Hφ); done. Qed.

Lemma test_pure_impl_1 (φ : Prop) :
343
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
344 345
Proof. iIntros (Hφ) "Hφ". by iApply "Hφ". Qed.
Lemma test_pure_impl_2 (φ : Prop) :
346
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
347 348
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" with "[% //]"). done. Qed.
Lemma test_pure_impl_3 (φ : Prop) :
349
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
350 351
Proof. iIntros (Hφ) "Hφ". unshelve iSpecialize ("Hφ" $! _). done. done. Qed.
Lemma test_pure_impl_4 (φ : Prop) :
352
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
353 354 355
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" $! Hφ). done. Qed.

Lemma test_forall_nondep_impl2 (φ : Prop) P :
356
  φ  P - ( _ : φ, P - False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
357 358 359 360 361 362 363
Proof.
  iIntros (Hφ) "HP Hφ".
  Fail iSpecialize ("Hφ" with "HP").
  iSpecialize ("Hφ" with "[% //] HP"). done.
Qed.

Lemma test_pure_impl2 (φ : Prop) P :
364
  φ  P - (⌜φ⌝  P - False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
365 366 367 368 369 370
Proof.
  iIntros (Hφ) "HP Hφ".
  Fail iSpecialize ("Hφ" with "HP").
  iSpecialize ("Hφ" with "[% //] HP"). done.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
371
Lemma test_iNext_laterN_later P n :  ^n P - ^n  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
372
Proof. iIntros "H". iNext. by iNext. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
373
Lemma test_iNext_later_laterN P n : ^n  P -  ^n P.
Robbert Krebbers's avatar
Robbert Krebbers committed
374
Proof. iIntros "H". iNext. by iNext. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
375
Lemma test_iNext_plus_1 P n1 n2 :  ^n1 ^n2 P - ^n1 ^n2  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
376
Proof. iIntros "H". iNext. iNext. by iNext. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
377 378
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
379
Check "test_iNext_plus_3".
Robbert Krebbers's avatar
Robbert Krebbers committed
380 381
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).
382
Proof. iIntros "H1 H2". iNext. iNext. iNext. iFrame. Show. iModIntro. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
383

384 385 386 387 388 389 390 391
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.

392 393 394
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.
395 396

Lemma test_specialize_affine_pure (φ : Prop) P :
397
  φ  (<affine> ⌜φ⌝ - P)  P.
398 399 400 401 402
Proof.
  iIntros (Hφ) "H". by iSpecialize ("H" with "[% //]").
Qed.

Lemma test_assert_affine_pure (φ : Prop) P :
403 404
  φ  P  P  <affine> ⌜φ⌝.
Proof. iIntros (Hφ). iAssert (<affine> ⌜φ⌝)%I with "[%]" as "$"; auto. Qed.
405 406
Lemma test_assert_pure (φ : Prop) P :
  φ  P  P  ⌜φ⌝.
407
Proof. iIntros (Hφ). iAssert ⌜φ⌝%I with "[%]" as "$"; auto with iFrame. Qed.
408

409
Lemma test_iEval x y :  (y + x)%nat = 1  -  S (x + y) = 2%nat  : PROP.
410 411 412 413 414 415
Proof.
  iIntros (H).
  iEval (rewrite (Nat.add_comm x y) // H).
  done.
Qed.

416
Lemma test_iIntros_pure_neg : ( ¬False  : PROP)%I.
417
Proof. by iIntros (?). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
418

419 420 421 422
Lemma test_iPureIntro_absorbing (φ : Prop) :
  φ  sbi_emp_valid (PROP:=PROP) (<absorb> ⌜φ⌝)%I.
Proof. intros ?. iPureIntro. done. Qed.

Ralf Jung's avatar
Ralf Jung committed
423
Check "test_iFrame_later_1".
424
Lemma test_iFrame_later_1 P Q : P   Q -  (P   Q).
425
Proof. iIntros "H". iFrame "H". Show. auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
426

Ralf Jung's avatar
Ralf Jung committed
427
Check "test_iFrame_later_2".
428
Lemma test_iFrame_later_2 P Q :  P   Q -  ( P   Q).
429
Proof. iIntros "H". iFrame "H". Show. auto. Qed.
430 431 432 433 434 435 436

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

Lemma iFrame_with_evar_r P Q :
439
   R, (P - Q - P  R)  R = Q.
440
Proof.
441
  eexists. split. iIntros "HP HQ". iFrame. iApply "HQ". done.
442 443
Qed.
Lemma iFrame_with_evar_l P Q :
444
   R, (P - Q - R  P)  R = Q.
445
Proof.
446
  eexists. split. iIntros "HP HQ". Fail iFrame "HQ".
447
  iSplitR "HP"; iAssumption. done.
448
Qed.
449 450 451 452 453 454
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
455 456 457 458 459 460
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
461
Lemma test_iAssumption_evar P :  R, (R  P)  R = P.
462 463 464 465 466 467 468
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
469 470 471
Lemma test_iAssumption_False_no_loop :  R, R   P, P.
Proof. eexists. iIntros "?" (P). done. Qed.

472 473 474 475
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
476 477 478 479
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.

480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495
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.
496

Ralf Jung's avatar
Ralf Jung committed
497
Check "test_and_sep_affine_bi".
498 499
Lemma test_and_sep_affine_bi `{BiAffine PROP} P Q :  P  Q   P  Q.
Proof.
500
  iIntros "[??]". iSplit; last done. Show. done.
501
Qed.
502

Ralf Jung's avatar
Ralf Jung committed
503
Check "test_big_sepL_simpl".
504
Lemma test_big_sepL_simpl x (l : list nat) P :
Robbert Krebbers's avatar
Robbert Krebbers committed
505
   P -
506 507 508
  ([ list] ky  l, <affine>  y = y ) -
  ([ list] y  x :: l, <affine>  y = y ) -
  P.
509
Proof. iIntros "HP ??". Show. simpl. Show. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
510

Ralf Jung's avatar
Ralf Jung committed
511
Check "test_big_sepL2_simpl".
Robbert Krebbers's avatar
Robbert Krebbers committed
512 513 514 515 516
Lemma test_big_sepL2_simpl x1 x2 (l1 l2 : list nat) P :
  P -
  ([ list] ky1;y2  []; l2, <affine>  y1 = y2 ) -
  ([ list] y1;y2  x1 :: l1; (x2 :: l2) ++ l2, <affine>  y1 = y2 ) -
  P  ([ list] y1;y2  x1 :: l1; x2 :: l2, True).
517
Proof. iIntros "HP ??". Show. simpl. Show. by iLeft. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
518

Ralf Jung's avatar
Ralf Jung committed
519
Check "test_big_sepL2_iDestruct".
Robbert Krebbers's avatar
Robbert Krebbers committed
520 521 522 523 524 525 526 527 528
Lemma test_big_sepL2_iDestruct (Φ : nat  nat  PROP) x1 x2 (l1 l2 : list nat) :
  ([ list] y1;y2  x1 :: l1; x2 :: l2, Φ y1 y2) -
  <absorb> Φ x1 x2.
Proof. iIntros "[??]". Show. iFrame. Qed.

Lemma test_big_sepL2_iFrame (Φ : nat  nat  PROP) (l1 l2 : list nat) P :
  Φ 0 10 - ([ list] y1;y2  l1;l2, Φ y1 y2) -
  ([ list] y1;y2  (0 :: l1);(10 :: l2), Φ y1 y2).
Proof. iIntros "$ ?". iFrame. Qed.
529 530 531 532

Lemma test_lemma_1 (b : bool) :
  emp @{PROP} ?b True.
Proof. destruct b; simpl; eauto. Qed.
Ralf Jung's avatar
Ralf Jung committed
533
Check "test_reducing_after_iDestruct".
534 535 536 537 538 539 540 541
Lemma test_reducing_after_iDestruct : emp @{PROP} True.
Proof.
  iIntros "H". iDestruct (test_lemma_1 true with "H") as "H". Show. done.
Qed.

Lemma test_lemma_2 (b : bool) :
  ?b emp @{PROP} emp.
Proof. destruct b; simpl; eauto. Qed.
Ralf Jung's avatar
Ralf Jung committed
542
Check "test_reducing_after_iApply".
543 544 545 546 547 548 549 550
Lemma test_reducing_after_iApply : emp @{PROP} emp.
Proof.
  iIntros "#H". iApply (test_lemma_2 true). Show. auto.
Qed.

Lemma test_lemma_3 (b : bool) :
  ?b emp @{PROP} b = b.
Proof. destruct b; simpl; eauto. Qed.
Ralf Jung's avatar
Ralf Jung committed
551
Check "test_reducing_after_iApply_late_evar".
552 553 554 555 556 557
Lemma test_reducing_after_iApply_late_evar : emp @{PROP} true = true.
Proof.
  iIntros "#H". iApply (test_lemma_3). Show. auto.
Qed.

Section wandM.
Ralf Jung's avatar
Ralf Jung committed
558
  Import proofmode.base.
Ralf Jung's avatar
Ralf Jung committed
559
  Check "test_wandM".
Ralf Jung's avatar
Ralf Jung committed
560 561 562 563 564 565 566
  Lemma test_wandM mP Q R :
    (mP -? Q) - (Q - R) - (mP -? R).
  Proof.
    iIntros "HPQ HQR HP". Show.
    iApply "HQR". iApply "HPQ". Show.
    done.
  Qed.
567 568
End wandM.

569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588
Definition modal_if_def b (P : PROP) :=
  (?b P)%I.
Lemma modal_if_lemma1 b P :
  False - ?b P.
Proof. iIntros "?". by iExFalso. Qed.
Lemma test_iApply_prettification1 (P : PROP) :
  False - modal_if_def true P.
Proof.
  (* Make sure the goal is not prettified before [iApply] unifies. *)
  iIntros "?". rewrite /modal_if_def. iApply modal_if_lemma1. iAssumption.
Qed.
Lemma modal_if_lemma2 P :
  False - ?false P.
Proof. iIntros "?". by iExFalso. Qed.
Lemma test_iApply_prettification2 (P  : PROP) :
  False -  b, ?b P.
Proof.
  (* Make sure the conclusion of the lemma is not prettified too early. *)
  iIntros "?". iExists _. iApply modal_if_lemma2. done.
Qed.
589

590 591 592 593 594 595
Lemma test_iDestruct_clear P Q R :
  P - (Q  R) - True.
Proof.
  iIntros "HP HQR". iDestruct "HQR" as "{HP} [HQ HR]". done.
Qed.

Ralf Jung's avatar
Ralf Jung committed
596
End tests.
597 598 599 600 601

(** Test specifically if certain things print correctly. *)
Section printing_tests.
Context {PROP : sbi} `{!BiFUpd PROP}.
Implicit Types P Q R : PROP.
602 603 604 605 606

Check "elim_mod_accessor".
Lemma elim_mod_accessor {X : Type} E1 E2 α (β : X  PROP) γ :
  accessor (fupd E1 E2) (fupd E2 E1) α β γ - |={E1}=> True.
Proof. iIntros ">Hacc". Show. Abort.
607 608 609

(* Test line breaking of long assumptions. *)
Section linebreaks.
Ralf Jung's avatar
Ralf Jung committed
610 611
Check "print_long_line_1".
Lemma print_long_line_1 (P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP) :
612 613 614 615
  P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P 
  P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P
  - True.
Proof.
616
  iIntros "HP". Show. Undo. iIntros "?". Show.
617 618
Abort.

619
(* This is specifically crafted such that not having the printing box in
620 621 622
   the proofmode notation breaks the output. *)
Local Notation "'TESTNOTATION' '{{' P '|' Q '}' '}'" := (P  Q)%I
  (format "'TESTNOTATION'  '{{'  P  '|'  '/' Q  '}' '}'") : bi_scope.
Ralf Jung's avatar
Ralf Jung committed
623 624
Check "print_long_line_2".
Lemma print_long_line_2 (P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP) :
625 626 627
  TESTNOTATION {{ P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P | P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P }}
  - True.
Proof.
628
  iIntros "HP". Show. Undo. iIntros "?". Show.
629
Abort.
630

Ralf Jung's avatar
Ralf Jung committed
631
Check "long_impl".
632 633 634 635 636
Lemma long_impl (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
  (PPPPPPPPPPPPPPPPP  (QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ))%I.
Proof.
  iStartProof. Show.
Abort.
Ralf Jung's avatar
Ralf Jung committed
637
Check "long_impl_nested".
638 639 640 641 642
Lemma long_impl_nested (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
  (PPPPPPPPPPPPPPPPP  (QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ)  (QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ))%I.
Proof.
  iStartProof. Show.
Abort.
Ralf Jung's avatar
Ralf Jung committed
643
Check "long_wand".
644 645 646 647 648
Lemma long_wand (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
  (PPPPPPPPPPPPPPPPP - (QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ))%I.
Proof.
  iStartProof. Show.
Abort.
Ralf Jung's avatar
Ralf Jung committed
649
Check "long_wand_nested".
650 651 652 653 654
Lemma long_wand_nested (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
  (PPPPPPPPPPPPPPPPP - (QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ) - (QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ))%I.
Proof.
  iStartProof. Show.
Abort.
Ralf Jung's avatar
Ralf Jung committed
655
Check "long_fupd".
656 657 658 659 660
Lemma long_fupd E (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
  PPPPPPPPPPPPPPPPP ={E}= QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ.
Proof.
  iStartProof. Show.
Abort.
Ralf Jung's avatar
Ralf Jung committed
661
Check "long_fupd_nested".
662 663 664
Lemma long_fupd_nested E1 E2 (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
  PPPPPPPPPPPPPPPPP ={E1,E2}= QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ
  ={E1,E2}= QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ.
665 666 667
Proof.
  iStartProof. Show.
Abort.
668 669 670
End linebreaks.

End printing_tests.
671 672 673 674 675 676

(** Test error messages *)
Section error_tests.
Context {PROP : sbi}.
Implicit Types P Q R : PROP.

677
Check "iAlways_spatial_non_empty".
678 679 680 681
Lemma iAlways_spatial_non_empty P :
  P -  emp.
Proof. iIntros "HP". Fail iAlways. Abort.

682
Check "iDestruct_bad_name".
683 684 685 686
Lemma iDestruct_bad_name P :
  P - P.
Proof. iIntros "HP". Fail iDestruct "HQ" as "HP". Abort.

687
Check "iIntros_dup_name".
688 689 690 691 692 693
Lemma iIntros_dup_name P Q :
  P - Q -  x y : (), P.
Proof.
  iIntros "HP". Fail iIntros "HP".
  iIntros "HQ" (x). Fail iIntros (x).
Abort.
694

695
Check "iSplit_one_of_many".
696 697 698 699 700 701
Lemma iSplit_one_of_many P :
  P - P - P  P.
Proof.
  iIntros "HP1 HP2". Fail iSplitL "HP1 HPx". Fail iSplitL "HPx HP1".
Abort.

702 703 704
Check "iExact_fail".
Lemma iExact_fail P Q :
  <affine> P - Q - <affine> P.
705
Proof.
706
  iIntros "HP". Fail iExact "HQ". iIntros "HQ". Fail iExact "HQ". Fail iExact "HP".
707 708
Abort.

709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736
Check "iClear_fail".
Lemma iClear_fail P : P - P.
Proof. Fail iClear "HP". iIntros "HP". Fail iClear "HP". Abort.

Check "iSpecializeArgs_fail".
Lemma iSpecializeArgs_fail P :
  ( x : nat, P) - P.
Proof. iIntros "HP". Fail iSpecialize ("HP" $! true). Abort.

Check "iStartProof_fail".
Lemma iStartProof_fail : 0 = 0.
Proof. Fail iStartProof. Abort.

Check "iPoseProof_fail".
Lemma iPoseProof_fail P : P - P.
Proof.
  Fail iPoseProof (eq_refl 0) as "H".
  iIntros "H". Fail iPoseProof bi.and_intro as "H".
Abort.

Check "iRevert_fail".
Lemma iRevert_fail P : P - P.
Proof. Fail iRevert "H". Abort.

Check "iDestruct_fail".
Lemma iDestruct_fail P : P - <absorb> P.
Proof. iIntros "HP". Fail iDestruct "HP" as "{HP}". Fail iDestruct "HP" as "[{HP}]". Abort.

737 738 739 740
Check "iApply_fail".
Lemma iApply_fail P Q : P - Q.
Proof. iIntros "HP". Fail iApply "HP". Abort.

741
End error_tests.