proofmode.v 30.5 KB
Newer Older
1
From iris.proofmode Require Import tactics intro_patterns.
2
Set Ltac Backtrace.
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 10 11 12
Lemma test_eauto_emp_isplit_biwand P : emp  P - P.
Proof. eauto 6. Qed.

Lemma test_eauto_isplit_biwand P : (P - P)%I.
Paolo G. Giarrusso's avatar
Paolo G. Giarrusso committed
13
Proof. eauto. Qed.
14

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
43
Lemma demo_3 P1 P2 P3 :
Robbert Krebbers's avatar
Robbert Krebbers committed
44 45
  P1  P2  P3 - P1   (P2   x, (P3  x = 0)  P3).
Proof. iIntros "($ & $ & $)". iNext. by iExists 0. Qed.
46

Robbert Krebbers's avatar
Robbert Krebbers committed
47 48
Definition foo (P : PROP) := (P - P)%I.
Definition bar : PROP := ( P, foo P)%I.
49

Robbert Krebbers's avatar
Robbert Krebbers committed
50 51
Lemma test_unfold_constants : bar.
Proof. iIntros (P) "HP //". Qed.
52

Ralf Jung's avatar
Ralf Jung committed
53
Check "test_iStopProof".
Robbert Krebbers's avatar
Robbert Krebbers committed
54
Lemma test_iStopProof Q : emp - Q - Q.
Ralf Jung's avatar
Ralf Jung committed
55
Proof. iIntros "#H1 H2". Show. iStopProof. Show. by rewrite bi.sep_elim_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
56

Robbert Krebbers's avatar
Robbert Krebbers committed
57
Lemma test_iRewrite {A : ofeT} (x y : A) P :
58
   ( z, P - <affine> (z  y)) - (P - P  (x,x)  (y,x)).
59
Proof.
60
  iIntros "#H1 H2".
Robbert Krebbers's avatar
Robbert Krebbers committed
61
  iRewrite (bi.internal_eq_sym x x with "[# //]").
62
  iRewrite -("H1" $! _ with "[- //]").
Robbert Krebbers's avatar
Robbert Krebbers committed
63
  auto.
64 65
Qed.

Ralf Jung's avatar
Ralf Jung committed
66
Check "test_iDestruct_and_emp".
67
Lemma test_iDestruct_and_emp P Q `{!Persistent P, !Persistent Q} :
68
  P  emp - emp  Q - <affine> (P  Q).
Ralf Jung's avatar
Ralf Jung committed
69
Proof. iIntros "[#? _] [_ #?]". Show. auto. Qed.
70 71

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

Robbert Krebbers's avatar
Robbert Krebbers committed
74 75 76 77 78 79 80 81
Lemma test_iDestruct_intuitionistic_1 P Q `{!Persistent P}:
  Q   (Q - P) - P  Q.
Proof. iIntros "[HQ #HQP]". iDestruct ("HQP" with "HQ") as "#HP". by iFrame. Qed.

Lemma test_iDestruct_intuitionistic_2 P Q `{!Persistent P, !Affine P}:
  Q  (Q - P) - P.
Proof. iIntros "[HQ HQP]". iDestruct ("HQP" with "HQ") as "#HP". done. Qed.

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

86 87 88
Lemma test_iIntros_pure (ψ φ : Prop) P : ψ  ( φ   P   φ  ψ   P)%I.
Proof. iIntros (??) "H". auto. Qed.

89 90 91
Lemma test_iIntros_pure_not : ( ¬False  : PROP)%I.
Proof. by iIntros (?). Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
92
Lemma test_fast_iIntros P Q :
93 94
  ( x y z : nat,
    x = plus 0 x  y = 0  z = 0  P   Q  foo (x  x))%I.
95
Proof.
96
  iIntros (a) "*".
97
  iIntros "#Hfoo **".
Robbert Krebbers's avatar
Robbert Krebbers committed
98
  iIntros "_ //".
99
Qed.
100

101
Lemma test_very_fast_iIntros P :
Robbert Krebbers's avatar
Robbert Krebbers committed
102
   x y : nat, ( x = y   P - P)%I.
103 104
Proof. by iIntros. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
105 106 107 108 109
(** 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.

110 111 112
Lemma test_iAssumption_affine P Q R `{!Affine P, !Affine R} : P - Q - R - Q.
Proof. iIntros "H1 H2 H3". iAssumption. Qed.

113 114 115
Lemma test_done_goal_evar Q :  P, Q  P.
Proof. eexists. iIntros "H". Fail done. iAssumption. Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
119
Lemma test_iAssert_persistent P Q : P - Q - True.
Robbert Krebbers's avatar
Robbert Krebbers committed
120 121 122 123 124 125 126 127
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.
128

129 130 131 132 133
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
134
Lemma test_iSpecialize_auto_frame P Q R :
135
  (P - True - True - Q - R) - P - Q - R.
136
Proof. iIntros "H ? HQ". by iApply ("H" with "[$]"). Qed.
137

Ralf Jung's avatar
Ralf Jung committed
138 139 140 141
Lemma test_iSpecialize_pure (φ : Prop) Q R:
  φ  (⌜φ⌝ - Q)  Q.
Proof. iIntros (HP HPQ). iDestruct (HPQ $! HP) as "?". done. Qed.

142 143 144 145
Lemma test_iSpecialize_Coq_entailment P Q R :
  P  (P - Q)  Q.
Proof. iIntros (HP HPQ). iDestruct (HPQ $! HP) as "?". done. Qed.

146 147 148 149
Lemma test_iPure_intro_emp R `{!Affine R} :
  R - emp.
Proof. iIntros "HR". by iPureIntro. Qed.

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

154 155 156 157 158 159 160
Lemma test_iPure_intro (φ : nat  Prop) P Q R `{!Affine P, !Persistent Q, !Affine R} :
  φ 0  P - Q  R -  x : nat, <affine>  φ x    φ x .
Proof. iIntros (?) "HP #HQ HR". iPureIntro; eauto. Qed.
Lemma test_iPure_intro_2 (φ : nat  Prop) P Q R `{!Persistent Q} :
  φ 0  P - Q  R -  x : nat, <affine>  φ x    φ x .
Proof. iIntros (?) "HP #HQ HR". iPureIntro; eauto. Qed.

Ralf Jung's avatar
Ralf Jung committed
161
Lemma test_fresh P Q:
162 163 164 165 166
  (P  Q) - (P  Q).
Proof.
  iIntros "H".
  let H1 := iFresh in
  let H2 := iFresh in
Paolo G. Giarrusso's avatar
Paolo G. Giarrusso committed
167
  let pat :=constr:(IList [cons (IIdent H1) (cons (IIdent H2) nil)]) in
168 169 170 171
  iDestruct "H" as pat.
  iFrame.
Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
176
Lemma test_iExist_tc `{Set_ A C} P : ( x1 x2 : gset positive, P - P)%I.
177 178 179
Proof. iExists {[ 1%positive ]}, . auto. Qed.

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

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

190 191 192 193 194 195 196 197 198 199 200 201 202 203
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.

204
Lemma test_iFrame_later `{!BiAffine PROP} P Q : P - Q -  P  Q.
205 206
Proof. iIntros "H1 H2". by iFrame "H1". Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
207 208 209
Lemma test_iAssert_modality P :  False -  P.
Proof.
  iIntros "HF".
210
  iAssert (<affine> False)%I with "[> -]" as %[].
Robbert Krebbers's avatar
Robbert Krebbers committed
211 212
  by iMod "HF".
Qed.
213

214
Lemma test_iMod_affinely_timeless P `{!Timeless P} :
215
  <affine>  P -  <affine> P.
216 217
Proof. iIntros "H". iMod "H". done. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
218
Lemma test_iAssumption_False P : False - P.
219
Proof. iIntros "H". done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
220 221

(* Check instantiation and dependent types *)
Robbert Krebbers's avatar
Robbert Krebbers committed
222
Lemma test_iSpecialize_dependent_type (P :  n, vec nat n  PROP) :
Robbert Krebbers's avatar
Robbert Krebbers committed
223 224 225 226 227
  ( 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
228

229 230 231 232 233
(* 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".
234
  iDestruct (big_sepL_elem_of _ _ _ Hp with "HT") as "Hp".
235 236 237
  done.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
238 239
Lemma test_eauto_iFrame P Q R `{!Persistent R} :
  P - Q - R  R  Q  P  R  False.
240
Proof. eauto 10 with iFrame. Qed.
241

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

246 247 248 249
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
250
Lemma test_iNext_evar P : P - True.
Ralf Jung's avatar
Ralf Jung committed
251 252 253 254
Proof.
  iIntros "HP". iAssert ( _ -  P)%I as "?"; last done.
  iIntros "?". iNext. iAssumption.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
255

256 257
Lemma test_iNext_sep1 P Q (R1 := (P  Q)%I) :
  ( P   Q)  R1 -  ((P  Q)  R1).
Robbert Krebbers's avatar
Robbert Krebbers committed
258 259 260 261
Proof.
  iIntros "H". iNext.
  rewrite {1 2}(lock R1). (* check whether R1 has not been unfolded *) done.
Qed.
262

Robbert Krebbers's avatar
Robbert Krebbers committed
263
Lemma test_iNext_sep2 P Q :  P   Q -  (P  Q).
264 265 266
Proof.
  iIntros "H". iNext. iExact "H". (* Check that the laters are all gone. *)
Qed.
267

Robbert Krebbers's avatar
Robbert Krebbers committed
268
Lemma test_iNext_quantifier {A} (Φ : A  A  PROP) :
Robbert Krebbers's avatar
Robbert Krebbers committed
269 270 271
  ( y,  x,  Φ x y) -  ( y,  x, Φ x y).
Proof. iIntros "H". iNext. done. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
272
Lemma test_iFrame_persistent (P Q : PROP) :
273
   P - Q - <pers> (P  P)  (P  Q  Q).
274
Proof. iIntros "#HP". iFrame "HP". iIntros "$". Qed.
275

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

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

282
Lemma test_iDestruct_persistent P (Φ : nat  PROP) `{! x, Persistent (Φ x)}:
283
   (P -  x, Φ x) -
284 285 286 287 288
  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
289 290 291 292 293
Lemma test_iLöb P : ( n, ^n P)%I.
Proof.
  iLöb as "IH". iDestruct "IH" as (n) "IH".
  by iExists (S n).
Qed.
294

295
Lemma test_iInduction_wf (x : nat) P Q :
296
   P - Q -  (x + 0 = x)%nat .
297 298 299 300 301 302
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.

303 304 305 306 307 308 309 310 311
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.

312
Lemma test_iIntros_start_proof :
Robbert Krebbers's avatar
Robbert Krebbers committed
313
  (True : PROP)%I.
314 315 316 317 318
Proof.
  (* Make sure iIntros actually makes progress and enters the proofmode. *)
  progress iIntros. done.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
319
Lemma test_True_intros : (True : PROP) - True.
320 321 322
Proof.
  iIntros "?". done.
Qed.
323 324 325 326 327 328 329 330 331 332

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

Robbert Krebbers's avatar
Robbert Krebbers committed
336
Lemma test_iNext_iRewrite P Q : <affine>  (Q  P) - <affine>  Q - <affine>  P.
337
Proof.
338
  iIntros "#HPQ HQ !#". iNext. by iRewrite "HPQ" in "HQ".
339 340
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
341
Lemma test_iIntros_modalities `(!Absorbing P) :
342
  (<pers> (   x : nat,  x = 0    x = 0  - False - P - P))%I.
343 344 345 346 347
Proof.
  iIntros (x ??).
  iIntros "* **". (* Test that fast intros do not work under modalities *)
  iIntros ([]).
Qed.
348

349 350 351
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
352

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

356
Lemma test_iAlways P Q R :
357
   P - <pers> Q  R - <pers> <affine> <affine> P   Q.
358
Proof. iIntros "#HP #HQ HR". iSplitL. iAlways. done. iAlways. done. Qed.
359

Robbert Krebbers's avatar
Robbert Krebbers committed
360 361 362
(* A bunch of test cases from #127 to establish that tactics behave the same on
`⌜ φ ⌝ → P` and `∀ _ : φ, P` *)
Lemma test_forall_nondep_1 (φ : Prop) :
363
  φ  ( _ : φ, False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
364 365
Proof. iIntros (Hφ) "Hφ". by iApply "Hφ". Qed.
Lemma test_forall_nondep_2 (φ : Prop) :
366
  φ  ( _ : φ, False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
367 368
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" with "[% //]"). done. Qed.
Lemma test_forall_nondep_3 (φ : Prop) :
369
  φ  ( _ : φ, False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
370 371
Proof. iIntros (Hφ) "Hφ". unshelve iSpecialize ("Hφ" $! _). done. done. Qed.
Lemma test_forall_nondep_4 (φ : Prop) :
372
  φ  ( _ : φ, False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
373 374 375
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" $! Hφ); done. Qed.

Lemma test_pure_impl_1 (φ : Prop) :
376
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
377 378
Proof. iIntros (Hφ) "Hφ". by iApply "Hφ". Qed.
Lemma test_pure_impl_2 (φ : Prop) :
379
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
380 381
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" with "[% //]"). done. Qed.
Lemma test_pure_impl_3 (φ : Prop) :
382
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
383 384
Proof. iIntros (Hφ) "Hφ". unshelve iSpecialize ("Hφ" $! _). done. done. Qed.
Lemma test_pure_impl_4 (φ : Prop) :
385
  φ  (⌜φ⌝  False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
386 387 388
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" $! Hφ). done. Qed.

Lemma test_forall_nondep_impl2 (φ : Prop) P :
389
  φ  P - ( _ : φ, P - False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
390 391 392 393 394 395 396
Proof.
  iIntros (Hφ) "HP Hφ".
  Fail iSpecialize ("Hφ" with "HP").
  iSpecialize ("Hφ" with "[% //] HP"). done.
Qed.

Lemma test_pure_impl2 (φ : Prop) P :
397
  φ  P - (⌜φ⌝  P - False : PROP) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
398 399 400 401 402 403
Proof.
  iIntros (Hφ) "HP Hφ".
  Fail iSpecialize ("Hφ" with "HP").
  iSpecialize ("Hφ" with "[% //] HP"). done.
Qed.

404 405 406 407 408
Lemma demo_laterN_forall {A} (Φ Ψ: A  PROP) n: ( x, ^n Φ x) - ^n ( x, Φ x).
Proof.
  iIntros "H" (w). iApply ("H" $! w).
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
409
Lemma test_iNext_laterN_later P n :  ^n P - ^n  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
410
Proof. iIntros "H". iNext. by iNext. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
411
Lemma test_iNext_later_laterN P n : ^n  P -  ^n P.
Robbert Krebbers's avatar
Robbert Krebbers committed
412
Proof. iIntros "H". iNext. by iNext. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
413
Lemma test_iNext_plus_1 P n1 n2 :  ^n1 ^n2 P - ^n1 ^n2  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
414
Proof. iIntros "H". iNext. iNext. by iNext. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
415 416
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
417
Check "test_iNext_plus_3".
Robbert Krebbers's avatar
Robbert Krebbers committed
418 419
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).
420
Proof. iIntros "H1 H2". iNext. iNext. iNext. iFrame. Show. iModIntro. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
421

422 423 424 425 426 427 428 429
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.

430 431 432
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.
433 434

Lemma test_specialize_affine_pure (φ : Prop) P :
435
  φ  (<affine> ⌜φ⌝ - P)  P.
436 437 438 439 440
Proof.
  iIntros (Hφ) "H". by iSpecialize ("H" with "[% //]").
Qed.

Lemma test_assert_affine_pure (φ : Prop) P :
441 442
  φ  P  P  <affine> ⌜φ⌝.
Proof. iIntros (Hφ). iAssert (<affine> ⌜φ⌝)%I with "[%]" as "$"; auto. Qed.
443 444
Lemma test_assert_pure (φ : Prop) P :
  φ  P  P  ⌜φ⌝.
445
Proof. iIntros (Hφ). iAssert ⌜φ⌝%I with "[%]" as "$"; auto with iFrame. Qed.
446

447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485
Lemma test_specialize_very_nested (φ : Prop) P P2 Q R1 R2 :
  φ 
  P - P2 -
  (<affine>  φ  - P2 - Q) -
  (P - Q - R1) -
  (R1 - True - R2) -
  R2.
Proof.
  iIntros (?) "HP HP2 HQ H1 H2".
  by iApply ("H2" with "(H1 HP (HQ [% //] [-])) [//]").
Qed.

Lemma test_specialize_very_very_nested P1 P2 P3 P4 P5 :
   P1 -
   (P1 - P2) -
  (P2 - P2 - P3) -
  (P3 - P4) -
  (P4 - P5) -
  P5.
Proof.
  iIntros "#H #H1 H2 H3 H4".
  by iSpecialize ("H4" with "(H3 (H2 (H1 H) (H1 H)))").
Qed.

Check "test_specialize_nested_intuitionistic".
Lemma test_specialize_nested_intuitionistic (φ : Prop) P P2 Q R1 R2 :
  φ 
   P -  (P - Q) - (Q - Q - R2) - R2.
Proof.
  iIntros (?) "#HP #HQ HR".
  iSpecialize ("HR" with "(HQ HP) (HQ HP)").
  Show.
  done.
Qed.

Lemma test_specialize_intuitionistic P Q :
   P -  (P - Q) -  Q.
Proof. iIntros "#HP #HQ". iSpecialize ("HQ" with "HP"). done. Qed.

486
Lemma test_iEval x y :  (y + x)%nat = 1  -  S (x + y) = 2%nat  : PROP.
487 488 489 490 491 492
Proof.
  iIntros (H).
  iEval (rewrite (Nat.add_comm x y) // H).
  done.
Qed.

493 494 495 496 497 498 499
Lemma test_iEval_precedence : True  True : PROP.
Proof.
  iIntros.
  (* Ensure that in [iEval (a); b], b is not parsed as part of the argument of [iEval]. *)
  iEval (rewrite /=); iPureIntro; exact I.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
500 501 502 503
Check "test_iSimpl_in".
Lemma test_iSimpl_in x y :  (3 + x)%nat = y  -  S (S (S x)) = y  : PROP.
Proof. iIntros "H". iSimpl in "H". Show. done. Qed.

504 505 506 507 508
Lemma test_iSimpl_in_2 x y z :
   (3 + x)%nat = y  -  (1 + y)%nat = z  -
   S (S (S x)) = y  : PROP.
Proof. iIntros "H1 H2". iSimpl in "H1 H2". Show. done. Qed.

509 510 511 512 513
Lemma test_iSimpl_in3 x y z :
   (3 + x)%nat = y  -  (1 + y)%nat = z  -
   S (S (S x)) = y  : PROP.
Proof. iIntros "#H1 H2". iSimpl in "#". Show. done. Qed.

Dan Frumin's avatar
Dan Frumin committed
514 515 516 517
Check "test_iSimpl_in4".
Lemma test_iSimpl_in4 x y :  (3 + x)%nat = y  -  S (S (S x)) = y  : PROP.
Proof. iIntros "H". Fail iSimpl in "%". by iSimpl in "H". Qed.

518
Lemma test_iIntros_pure_neg : ( ¬False  : PROP)%I.
519
Proof. by iIntros (?). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
520

521 522 523 524
Lemma test_iPureIntro_absorbing (φ : Prop) :
  φ  sbi_emp_valid (PROP:=PROP) (<absorb> ⌜φ⌝)%I.
Proof. intros ?. iPureIntro. done. Qed.

Ralf Jung's avatar
Ralf Jung committed
525
Check "test_iFrame_later_1".
526
Lemma test_iFrame_later_1 P Q : P   Q -  (P   Q).
527
Proof. iIntros "H". iFrame "H". Show. auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
528

Ralf Jung's avatar
Ralf Jung committed
529
Check "test_iFrame_later_2".
530
Lemma test_iFrame_later_2 P Q :  P   Q -  ( P   Q).
531
Proof. iIntros "H". iFrame "H". Show. auto. Qed.
532 533 534 535 536

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

Lemma iFrame_with_evar_r P Q :
541
   R, (P - Q - P  R)  R = Q.
542
Proof.
543
  eexists. split. iIntros "HP HQ". iFrame. iApply "HQ". done.
544 545
Qed.
Lemma iFrame_with_evar_l P Q :
546
   R, (P - Q - R  P)  R = Q.
547
Proof.
548
  eexists. split. iIntros "HP HQ". Fail iFrame "HQ".
549
  iSplitR "HP"; iAssumption. done.
550
Qed.
551 552 553 554 555 556
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
557 558 559 560 561 562
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
563
Lemma test_iAssumption_evar P :  R, (R  P)  R = P.
564 565 566 567 568 569 570
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
571 572 573
Lemma test_iAssumption_False_no_loop :  R, R   P, P.
Proof. eexists. iIntros "?" (P). done. Qed.

574 575 576 577
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
578 579 580 581
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.

582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597
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.
598

Ralf Jung's avatar
Ralf Jung committed
599
Check "test_and_sep_affine_bi".
600
Lemma test_and_sep_affine_bi `{!BiAffine PROP} P Q :  P  Q   P  Q.
601
Proof.
602
  iIntros "[??]". iSplit; last done. Show. done.
603
Qed.
604

Ralf Jung's avatar
Ralf Jung committed
605
Check "test_big_sepL_simpl".
606
Lemma test_big_sepL_simpl x (l : list nat) P :
Robbert Krebbers's avatar
Robbert Krebbers committed
607
   P -
608 609 610
  ([ list] ky  l, <affine>  y = y ) -
  ([ list] y  x :: l, <affine>  y = y ) -
  P.
611
Proof. iIntros "HP ??". Show. simpl. Show. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
612

Ralf Jung's avatar
Ralf Jung committed
613
Check "test_big_sepL2_simpl".
Robbert Krebbers's avatar
Robbert Krebbers committed
614 615 616 617 618
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).
619
Proof. iIntros "HP ??". Show. simpl. Show. by iLeft. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
620

Ralf Jung's avatar
Ralf Jung committed
621
Check "test_big_sepL2_iDestruct".
Robbert Krebbers's avatar
Robbert Krebbers committed
622 623 624 625 626 627 628 629 630
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.
631 632 633 634

Lemma test_lemma_1 (b : bool) :
  emp @{PROP} ?b True.
Proof. destruct b; simpl; eauto. Qed.
Ralf Jung's avatar
Ralf Jung committed
635
Check "test_reducing_after_iDestruct".
636 637 638 639 640 641 642 643
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
644
Check "test_reducing_after_iApply".
645 646 647 648 649 650 651 652
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
653
Check "test_reducing_after_iApply_late_evar".
654 655 656 657 658 659
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
660
  Import proofmode.base.
Ralf Jung's avatar
Ralf Jung committed
661
  Check "test_wandM".
Ralf Jung's avatar
Ralf Jung committed
662 663 664 665 666 667 668
  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.
669 670
End wandM.

671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690
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.
691

692 693 694 695 696
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
697
End tests.
698 699 700 701 702

(** Test specifically if certain things print correctly. *)
Section printing_tests.
Context {PROP : sbi} `{!BiFUpd PROP}.
Implicit Types P Q R : PROP.
703 704 705 706 707

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.
708 709 710

(* Test line breaking of long assumptions. *)
Section linebreaks.
Ralf Jung's avatar
Ralf Jung committed
711 712
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) :
713 714 715 716
  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.
717
  iIntros "HP". Show. Undo. iIntros "?". Show.
718 719
Abort.

720
(* This is specifically crafted such that not having the printing box in
721 722 723
   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
724 725
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) :
726 727 728
  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.
729
  iIntros "HP". Show. Undo. iIntros "?". Show.
730
Abort.
731

Ralf Jung's avatar
Ralf Jung committed
732
Check "long_impl".
733 734 735 736 737
Lemma long_impl (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
  (PPPPPPPPPPPPPPPPP  (QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ  QQQQQQQQQQQQQQQQQQ))%I.
Proof.
  iStartProof. Show.
Abort.
Ralf Jung's avatar
Ralf Jung committed
738
Check "long_impl_nested".
739 740 741 742 743
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
744
Check "long_wand".
745 746 747 748 749
Lemma long_wand (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ