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

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
Lemma test_iIntros_start_proof :
Robbert Krebbers's avatar
Robbert Krebbers committed
271
  (True : PROP)%I.
272 273 274 275 276
Proof.
  (* Make sure iIntros actually makes progress and enters the proofmode. *)
  progress iIntros. done.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
277
Lemma test_True_intros : (True : PROP) - True.
278 279 280
Proof.
  iIntros "?". done.
Qed.
281 282 283 284 285 286 287 288 289 290

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

294
Lemma test_foo P Q : <affine>  (Q  P) - <affine>  Q - <affine>  P.
295
Proof.
296
  iIntros "#HPQ HQ !#". iNext. by iRewrite "HPQ" in "HQ".
297 298
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
299
Lemma test_iIntros_modalities `(!Absorbing P) :
300
  (<pers> (   x : nat,  x = 0    x = 0  - False - P - P))%I.
301 302 303 304 305
Proof.
  iIntros (x ??).
  iIntros "* **". (* Test that fast intros do not work under modalities *)
  iIntros ([]).
Qed.
306

307 308 309
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
310

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

314
Lemma test_iAlways P Q R :
315
   P - <pers> Q  R - <pers> <affine> <affine> P   Q.
316
Proof. iIntros "#HP #HQ HR". iSplitL. iAlways. done. iAlways. done. Qed.
317

Robbert Krebbers's avatar
Robbert Krebbers committed
318 319 320
(* A bunch of test cases from #127 to establish that tactics behave the same on
`⌜ φ ⌝ → P` and `∀ _ : φ, P` *)
Lemma test_forall_nondep_1 (φ : Prop) :
321
  φ  ( _ : φ, False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
322 323
Proof. iIntros (Hφ) "Hφ". by iApply "Hφ". Qed.
Lemma test_forall_nondep_2 (φ : Prop) :
324
  φ  ( _ : φ, False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
325 326
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" with "[% //]"). done. Qed.
Lemma test_forall_nondep_3 (φ : Prop) :
327
  φ  ( _ : φ, False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
328 329
Proof. iIntros (Hφ) "Hφ". unshelve iSpecialize ("Hφ" $! _). done. done. Qed.
Lemma test_forall_nondep_4 (φ : Prop) :
330
  φ  ( _ : φ, False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
331 332 333
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" $! Hφ); done. Qed.

Lemma test_pure_impl_1 (φ : Prop) :
334
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
335 336
Proof. iIntros (Hφ) "Hφ". by iApply "Hφ". Qed.
Lemma test_pure_impl_2 (φ : Prop) :
337
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
338 339
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" with "[% //]"). done. Qed.
Lemma test_pure_impl_3 (φ : Prop) :
340
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
341 342
Proof. iIntros (Hφ) "Hφ". unshelve iSpecialize ("Hφ" $! _). done. done. Qed.
Lemma test_pure_impl_4 (φ : Prop) :
343
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
344 345 346
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" $! Hφ). done. Qed.

Lemma test_forall_nondep_impl2 (φ : Prop) P :
347
  φ  P - ( _ : φ, P - False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
348 349 350 351 352 353 354
Proof.
  iIntros (Hφ) "HP Hφ".
  Fail iSpecialize ("Hφ" with "HP").
  iSpecialize ("Hφ" with "[% //] HP"). done.
Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
362
Lemma test_iNext_laterN_later P n :  ^n P - ^n  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
363
Proof. iIntros "H". iNext. by iNext. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
364
Lemma test_iNext_later_laterN P n : ^n  P -  ^n P.
Robbert Krebbers's avatar
Robbert Krebbers committed
365
Proof. iIntros "H". iNext. by iNext. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
366
Lemma test_iNext_plus_1 P n1 n2 :  ^n1 ^n2 P - ^n1 ^n2  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
367
Proof. iIntros "H". iNext. iNext. by iNext. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
368 369
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
370
Check "test_iNext_plus_3".
Robbert Krebbers's avatar
Robbert Krebbers committed
371 372
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).
373
Proof. iIntros "H1 H2". iNext. iNext. iNext. iFrame. Show. iModIntro. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
374

375 376 377 378 379 380 381 382
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.

383 384 385
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.
386 387

Lemma test_specialize_affine_pure (φ : Prop) P :
388
  φ  (<affine> ⌜φ⌝ - P)  P.
389 390 391 392 393
Proof.
  iIntros (Hφ) "H". by iSpecialize ("H" with "[% //]").
Qed.

Lemma test_assert_affine_pure (φ : Prop) P :
394 395
  φ  P  P  <affine> ⌜φ⌝.
Proof. iIntros (Hφ). iAssert (<affine> ⌜φ⌝)%I with "[%]" as "$"; auto. Qed.
396 397
Lemma test_assert_pure (φ : Prop) P :
  φ  P  P  ⌜φ⌝.
398
Proof. iIntros (Hφ). iAssert ⌜φ⌝%I with "[%]" as "$"; auto with iFrame. Qed.
399

400
Lemma test_iEval x y :  (y + x)%nat = 1  -  S (x + y) = 2%nat  : PROP.
401 402 403 404 405 406
Proof.
  iIntros (H).
  iEval (rewrite (Nat.add_comm x y) // H).
  done.
Qed.

407
Lemma test_iIntros_pure_neg : ( ¬False  : PROP)%I.
408
Proof. by iIntros (?). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
409

410 411 412 413
Lemma test_iPureIntro_absorbing (φ : Prop) :
  φ  sbi_emp_valid (PROP:=PROP) (<absorb> ⌜φ⌝)%I.
Proof. intros ?. iPureIntro. done. Qed.

Ralf Jung's avatar
Ralf Jung committed
414
Check "test_iFrame_later_1".
415
Lemma test_iFrame_later_1 P Q : P   Q -  (P   Q).
416
Proof. iIntros "H". iFrame "H". Show. auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
417

Ralf Jung's avatar
Ralf Jung committed
418
Check "test_iFrame_later_2".
419
Lemma test_iFrame_later_2 P Q :  P   Q -  ( P   Q).
420
Proof. iIntros "H". iFrame "H". Show. auto. Qed.
421 422 423 424 425 426 427

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.
428 429

Lemma iFrame_with_evar_r P Q :
430
   R, (P - Q - P  R)  R = Q.
431
Proof.
432
  eexists. split. iIntros "HP HQ". iFrame. iApply "HQ". done.
433 434
Qed.
Lemma iFrame_with_evar_l P Q :
435
   R, (P - Q - R  P)  R = Q.
436
Proof.
437
  eexists. split. iIntros "HP HQ". Fail iFrame "HQ".
438
  iSplitR "HP"; iAssumption. done.
439
Qed.
440 441 442 443 444 445
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
446 447 448 449 450 451
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
452
Lemma test_iAssumption_evar P :  R, (R  P)  R = P.
453 454 455 456 457 458 459
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
460 461 462
Lemma test_iAssumption_False_no_loop :  R, R   P, P.
Proof. eexists. iIntros "?" (P). done. Qed.

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

471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486
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.
487

Ralf Jung's avatar
Ralf Jung committed
488
Check "test_and_sep_affine_bi".
489 490
Lemma test_and_sep_affine_bi `{BiAffine PROP} P Q :  P  Q   P  Q.
Proof.
491
  iIntros "[??]". iSplit; last done. Show. done.
492
Qed.
493

Ralf Jung's avatar
Ralf Jung committed
494
Check "test_big_sepL_simpl".
495
Lemma test_big_sepL_simpl x (l : list nat) P :
Robbert Krebbers's avatar
Robbert Krebbers committed
496
   P -
497 498 499
  ([ list] ky  l, <affine>  y = y ) -
  ([ list] y  x :: l, <affine>  y = y ) -
  P.
500
Proof. iIntros "HP ??". Show. simpl. Show. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
501

Ralf Jung's avatar
Ralf Jung committed
502
Check "test_big_sepL2_simpl".
Robbert Krebbers's avatar
Robbert Krebbers committed
503 504 505 506 507
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).
508
Proof. iIntros "HP ??". Show. simpl. Show. by iLeft. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
509

Ralf Jung's avatar
Ralf Jung committed
510
Check "test_big_sepL2_iDestruct".
Robbert Krebbers's avatar
Robbert Krebbers committed
511 512 513 514 515 516 517 518 519
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.
520 521 522 523

Lemma test_lemma_1 (b : bool) :
  emp @{PROP} ?b True.
Proof. destruct b; simpl; eauto. Qed.
Ralf Jung's avatar
Ralf Jung committed
524
Check "test_reducing_after_iDestruct".
525 526 527 528 529 530 531 532
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
533
Check "test_reducing_after_iApply".
534 535 536 537 538 539 540 541
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
542
Check "test_reducing_after_iApply_late_evar".
543 544 545 546 547 548
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
549
  Import proofmode.base.
Ralf Jung's avatar
Ralf Jung committed
550
  Check "test_wandM".
Ralf Jung's avatar
Ralf Jung committed
551 552 553 554 555 556 557
  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.
558 559
End wandM.

560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579
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.
580

Ralf Jung's avatar
Ralf Jung committed
581
End tests.
582 583 584 585 586

(** Test specifically if certain things print correctly. *)
Section printing_tests.
Context {PROP : sbi} `{!BiFUpd PROP}.
Implicit Types P Q R : PROP.
587 588 589 590 591

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.
592 593 594

(* Test line breaking of long assumptions. *)
Section linebreaks.
Ralf Jung's avatar
Ralf Jung committed
595 596
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) :
597 598 599 600
  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.
601
  iIntros "HP". Show. Undo. iIntros "?". Show.
602 603
Abort.

604
(* This is specifically crafted such that not having the printing box in
605 606 607
   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
608 609
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) :
610 611 612
  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.
613
  iIntros "HP". Show. Undo. iIntros "?". Show.
614
Abort.
615

Ralf Jung's avatar
Ralf Jung committed
616
Check "long_impl".
617 618 619 620 621
Lemma long_impl (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
  (PPPPPPPPPPPPPPPPP  (QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ))%I.
Proof.
  iStartProof. Show.
Abort.
Ralf Jung's avatar
Ralf Jung committed
622
Check "long_impl_nested".
623 624 625 626 627
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
628
Check "long_wand".
629 630 631 632 633
Lemma long_wand (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
  (PPPPPPPPPPPPPPPPP - (QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ))%I.
Proof.
  iStartProof. Show.
Abort.
Ralf Jung's avatar
Ralf Jung committed
634
Check "long_wand_nested".
635 636 637 638 639
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
640
Check "long_fupd".
641 642 643 644 645
Lemma long_fupd E (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
  PPPPPPPPPPPPPPPPP ={E}= QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ.
Proof.
  iStartProof. Show.
Abort.
Ralf Jung's avatar
Ralf Jung committed
646
Check "long_fupd_nested".
647 648 649
Lemma long_fupd_nested E1 E2 (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
  PPPPPPPPPPPPPPPPP ={E1,E2}= QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ
  ={E1,E2}= QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ.
650 651 652
Proof.
  iStartProof. Show.
Abort.
653 654 655
End linebreaks.

End printing_tests.
656 657 658 659 660 661

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

662
Check "iAlways_spatial_non_empty".
663 664 665 666
Lemma iAlways_spatial_non_empty P :
  P -  emp.
Proof. iIntros "HP". Fail iAlways. Abort.

667
Check "iDestruct_bad_name".
668 669 670 671
Lemma iDestruct_bad_name P :
  P - P.
Proof. iIntros "HP". Fail iDestruct "HQ" as "HP". Abort.

672
Check "iIntros_dup_name".
673 674 675 676 677 678
Lemma iIntros_dup_name P Q :
  P - Q -  x y : (), P.
Proof.
  iIntros "HP". Fail iIntros "HP".
  iIntros "HQ" (x). Fail iIntros (x).
Abort.
679

680
Check "iSplit_one_of_many".
681 682 683 684 685 686
Lemma iSplit_one_of_many P :
  P - P - P  P.
Proof.
  iIntros "HP1 HP2". Fail iSplitL "HP1 HPx". Fail iSplitL "HPx HP1".
Abort.

687 688 689
Check "iExact_fail".
Lemma iExact_fail P Q :
  <affine> P - Q - <affine> P.
690
Proof.
691
  iIntros "HP". Fail iExact "HQ". iIntros "HQ". Fail iExact "HQ". Fail iExact "HP".
692 693
Abort.

694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721
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.

722 723 724 725
Check "iApply_fail".
Lemma iApply_fail P Q : P - Q.
Proof. iIntros "HP". Fail iApply "HP". Abort.

726
End error_tests.