proofmode.v 11.6 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
From iris.proofmode Require Import tactics.
2
From iris.base_logic.lib Require Import invariants.
3
From stdpp Require Import gmap.
4
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
5

Ralf Jung's avatar
Ralf Jung committed
6
7
Section tests.
Context {M : ucmraT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
8
9
10
Implicit Types P Q R : uPred M.

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

Ralf Jung's avatar
Ralf Jung committed
19
Lemma demo_1 (P1 P2 P3 : nat  uPred M) :
20
  ( (x y : nat) a b,
Robbert Krebbers's avatar
Robbert Krebbers committed
21
    x  y 
22
23
24
     (uPred_ownM (a  b) -
    ( y1 y2 c, P1 ((x + y1) + y2)  True   uPred_ownM c) -
      ( z, P2 z  True  P2 z) -
Ralf Jung's avatar
Ralf Jung committed
25
     ( n m : nat, P1 n   ((True  P2 n)   (n = n  P3 n))) -
26
     x = 0   x z,  P3 (x + z)  uPred_ownM b  uPred_ownM (core b)))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
27
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
28
  iIntros (i [|j] a b ?) "!# [Ha Hb] H1 #H2 H3"; setoid_subst.
Robbert Krebbers's avatar
Robbert Krebbers committed
29
30
  { iLeft. by iNext. }
  iRight.
31
  iDestruct "H1" as (z1 z2 c) "(H1&_&#Hc)".
32
  iPoseProof "Hc" as "foo".
33
  iRevert (a b) "Ha Hb". iIntros (b a) "? {foo} Ha".
34
  iAssert (uPred_ownM (a  core a)) with "[Ha]" as "[Ha #Hac]".
Robbert Krebbers's avatar
Robbert Krebbers committed
35
  { by rewrite cmra_core_r. }
36
  iIntros "{$Hac $Ha}".
Robbert Krebbers's avatar
Robbert Krebbers committed
37
38
  iExists (S j + z1), z2.
  iNext.
39
  iApply ("H3" $! _ 0 with "[$]").
40
  - iSplit. done. iApply "H2". iLeft. iApply "H2". by iRight.
Robbert Krebbers's avatar
Robbert Krebbers committed
41
42
43
  - done.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
44
Lemma demo_2 P1 P2 P3 P4 Q (P5 : nat  uPredC M):
45
46
47
  P2  (P3  Q)  True  P1  P2  (P4  ( x:nat, P5 x  P3))  True -
    P1 - (True  True) -
  (((P2  False  P2  0 = 0)  P3)  Q  P1  True) 
48
     (P2  False)  (False  P5 0).
Robbert Krebbers's avatar
Robbert Krebbers committed
49
50
51
52
53
54
55
56
57
58
59
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".
  * iFrame "H3". by iRight.
  * iSplitL "HQ". iAssumption. by iSplitL "H1".
Robbert Krebbers's avatar
Robbert Krebbers committed
60
61
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
62
Lemma demo_3 P1 P2 P3 :
63
  P1  P2  P3 -  P1   (P2   x, (P3  x = 0)  P3).
64
65
Proof. iIntros "($ & $ & H)". iFrame "H". iNext. by iExists 0. Qed.

Ralf Jung's avatar
Ralf Jung committed
66
67
Definition foo (P : uPred M) := (P  P)%I.
Definition bar : uPred M := ( P, foo P)%I.
68

Robbert Krebbers's avatar
Robbert Krebbers committed
69
Lemma test_unfold_constants : True - bar.
70
Proof. iIntros. iIntros (P) "HP //". Qed.
71

Robbert Krebbers's avatar
Robbert Krebbers committed
72
Lemma test_iRewrite (x y : M) P :
73
  ( z, P  z  y) - (P - (x,x)  (y,x)).
74
75
Proof.
  iIntros "H1 H2".
76
77
  iRewrite (uPred.internal_eq_sym x x with "[# //]").
  iRewrite -("H1" $! _ with "[- //]").
78
  done.
79
80
Qed.

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
87
Lemma test_fast_iIntros P Q :
88
89
  ( x y z : nat,
    x = plus 0 x  y = 0  z = 0  P   Q  foo (x  x))%I.
90
Proof.
91
  iIntros (a) "*".
92
  iIntros "#Hfoo **".
93
  iIntros "# _ //".
94
Qed.
95

96
97
98
99
Lemma test_very_fast_iIntros P :
   x y : nat,  x = y  - P - P.
Proof. by iIntros. Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
103
Lemma test_iFrame_pure (x y z : M) :
104
   x  y  z - ( x   x  y  z : uPred M).
105
Proof. iIntros (Hv) "Hxy". iFrame (Hv) "Hxy". Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
106

107
108
109
110
111
112
Lemma test_iFrame_disjunction_1 P1 P2 Q1 Q2 :
   P1 - Q2 - P2 - (P1  P2  False  P2)  (Q1  Q2).
Proof. 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.

113
114
115
116
117
118
119
Lemma test_iFrame_conjunction_1 P Q :
  P - Q - (P  Q)  (P  Q).
Proof. iIntros "HP HQ". iFrame "HP HQ". Qed.
Lemma test_iFrame_conjunction_2 P Q :
  P - Q - (P  P)  (Q  Q).
Proof. iIntros "HP HQ". iFrame "HP HQ". Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
130
Lemma test_iSpecialize_auto_frame P Q R :
131
  (P - True - True - Q - R) - P - Q - R.
132
Proof. iIntros "H ? HQ". by iApply ("H" with "[$]"). Qed.
133
134

(* Check coercions *)
Robbert Krebbers's avatar
Robbert Krebbers committed
135
Lemma test_iExist_coercion (P : Z  uPred M) : ( x, P x) -  x, P x.
136
Proof. iIntros "HP". iExists (0:nat). iApply ("HP" $! (0:nat)). Qed.
137

138
139
140
141
142
143
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.
Proof. iIntros "H". iSpecialize ("H" $!  {[ 1%positive ]} ). done. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
144
Lemma test_iAssert_modality P : (|==> False) - |==> P.
145
Proof. iIntros. iAssert False%I with "[> - //]" as %[]. Qed.
146

Robbert Krebbers's avatar
Robbert Krebbers committed
147
Lemma test_iAssumption_False P : False - P.
148
Proof. iIntros "H". done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
149
150

(* Check instantiation and dependent types *)
Robbert Krebbers's avatar
Robbert Krebbers committed
151
Lemma test_iSpecialize_dependent_type (P :  n, vec nat n  uPred M) :
Robbert Krebbers's avatar
Robbert Krebbers committed
152
153
154
155
156
  ( 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
157

Robbert Krebbers's avatar
Robbert Krebbers committed
158
Lemma test_eauto_iFrame P Q R `{!Persistent R} :
Robbert Krebbers's avatar
Robbert Krebbers committed
159
  P - Q - R - R  Q  P  R  False.
160
Proof. eauto 10 with iFrame. Qed.
161

162
Lemma test_iCombine_persistent P Q R `{!Persistent R} :
163
164
  P - Q - R - R  Q  P  R  False.
Proof. iIntros "HP HQ #HR". iCombine "HR HQ HP HR" as "H". auto. Qed.
Ralf Jung's avatar
Ralf Jung committed
165

Robbert Krebbers's avatar
Robbert Krebbers committed
166
Lemma test_iNext_evar P : P - True.
Ralf Jung's avatar
Ralf Jung committed
167
168
169
170
Proof.
  iIntros "HP". iAssert ( _ -  P)%I as "?"; last done.
  iIntros "?". iNext. iAssumption.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
171

Robbert Krebbers's avatar
Robbert Krebbers committed
172
Lemma test_iNext_sep1 P Q
Robbert Krebbers's avatar
Robbert Krebbers committed
173
174
175
176
177
178
    (R1 := (P  Q)%I) (R2 := ( P   Q)%I) :
  ( P   Q)  R1  R2 -  (P  Q)   R1  R2.
Proof.
  iIntros "H". iNext.
  rewrite {1 2}(lock R1). (* check whether R1 has not been unfolded *) done.
Qed.
179

Robbert Krebbers's avatar
Robbert Krebbers committed
180
Lemma test_iNext_sep2 P Q :  P   Q -  (P  Q).
181
182
183
Proof.
  iIntros "H". iNext. iExact "H". (* Check that the laters are all gone. *)
Qed.
184

Robbert Krebbers's avatar
Robbert Krebbers committed
185
186
187
188
Lemma test_iNext_quantifier (Φ : M  M  uPred M) :
  ( y,  x,  Φ x y) -  ( y,  x, Φ x y).
Proof. iIntros "H". iNext. done. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
189
Lemma test_iFrame_persistent (P Q : uPred M) :
190
191
   P - Q -  (P  P)  (P  Q  Q).
Proof. iIntros "#HP". iFrame "HP". iIntros "$". Qed.
192

193
Lemma test_iSplit_persistently P Q :  P -  (P  P).
194
Proof. iIntros "#?". by iSplit. Qed.
Ralf Jung's avatar
Ralf Jung committed
195

Robbert Krebbers's avatar
Robbert Krebbers committed
196
Lemma test_iSpecialize_persistent P Q :
197
198
   P - ( P - Q) - Q.
Proof. iIntros "#HP HPQ". by iSpecialize ("HPQ" with "HP"). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
199
200
201
202
203
204

Lemma test_iLöb P : ( n, ^n P)%I.
Proof.
  iLöb as "IH". iDestruct "IH" as (n) "IH".
  by iExists (S n).
Qed.
205

206
207
208
209
210
211
212
213
Lemma test_iInduction_wf (x : nat) P Q :
   P - Q -  (x + 0 = x)%nat .
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.

214
215
216
217
218
219
220
221
222
223
224
Lemma test_iIntros_start_proof :
  (True : uPred M)%I.
Proof.
  (* Make sure iIntros actually makes progress and enters the proofmode. *)
  progress iIntros. done.
Qed.

Lemma test_True_intros : (True : uPred M) - True.
Proof.
  iIntros "?". done.
Qed.
225
226
227
228
229
230
231
232
233
234
235
236

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 :
   Q, let R := True%I in P - R - Q - P  Q.
Proof. iIntros (Q R) "$ HR $". Qed.
237
238
239
240
241
242
243
244

Lemma test_iIntros_modalities P :
  (   x : nat,  x = 0  -  x = 0   False - P - P)%I.
Proof.
  iIntros (x ??).
  iIntros "* **". (* Test that fast intros do not work under modalities *)
  iIntros ([]).
Qed.
245
246
247
248

Lemma test_iIntros_rewrite P (x1 x2 x3 x4 : nat) :
  x1 = x2  ( x2 = x3    x3  x4   P) -  x1 = x4   P.
Proof. iIntros (?) "(-> & -> & $)"; auto. Qed.
249

Robbert Krebbers's avatar
Robbert Krebbers committed
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
(* A bunch of test cases from #127 to establish that tactics behave the same on
`⌜ φ ⌝ → P` and `∀ _ : φ, P` *)
Lemma test_forall_nondep_1 (φ : Prop) :
  φ  ( _ : φ, False : uPred M) - False.
Proof. iIntros (Hφ) "Hφ". by iApply "Hφ". Qed.
Lemma test_forall_nondep_2 (φ : Prop) :
  φ  ( _ : φ, False : uPred M) - False.
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" with "[% //]"). done. Qed.
Lemma test_forall_nondep_3 (φ : Prop) :
  φ  ( _ : φ, False : uPred M) - False.
Proof. iIntros (Hφ) "Hφ". unshelve iSpecialize ("Hφ" $! _). done. done. Qed.
Lemma test_forall_nondep_4 (φ : Prop) :
  φ  ( _ : φ, False : uPred M) - False.
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" $! Hφ); done. Qed.

Lemma test_pure_impl_1 (φ : Prop) :
  φ  (⌜φ⌝  False : uPred M) - False.
Proof. iIntros (Hφ) "Hφ". by iApply "Hφ". Qed.
Lemma test_pure_impl_2 (φ : Prop) :
  φ  (⌜φ⌝  False : uPred M) - False.
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" with "[% //]"). done. Qed.
Lemma test_pure_impl_3 (φ : Prop) :
  φ  (⌜φ⌝  False : uPred M) - False.
Proof. iIntros (Hφ) "Hφ". unshelve iSpecialize ("Hφ" $! _). done. done. Qed.
Lemma test_pure_impl_4 (φ : Prop) :
  φ  (⌜φ⌝  False : uPred M) - False.
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" $! Hφ). done. Qed.

Lemma test_forall_nondep_impl2 (φ : Prop) P :
  φ  P - ( _ : φ, P - False : uPred M) - False.
Proof.
  iIntros (Hφ) "HP Hφ".
  Fail iSpecialize ("Hφ" with "HP").
  iSpecialize ("Hφ" with "[% //] HP"). done.
Qed.

Lemma test_pure_impl2 (φ : Prop) P :
  φ  P - (⌜φ⌝  P - False : uPred M) - False.
Proof.
  iIntros (Hφ) "HP Hφ".
  Fail iSpecialize ("Hφ" with "HP").
  iSpecialize ("Hφ" with "[% //] HP"). done.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
294
Lemma test_iNext_laterN_later P n :  ^n P - ^n  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
295
Proof. iIntros "H". iNext. by iNext. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
296
Lemma test_iNext_later_laterN P n : ^n  P -  ^n P.
Robbert Krebbers's avatar
Robbert Krebbers committed
297
Proof. iIntros "H". iNext. by iNext. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
298
Lemma test_iNext_plus_1 P n1 n2 :  ^n1 ^n2 P - ^n1 ^n2  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
299
Proof. iIntros "H". iNext. iNext. by iNext. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
300
301
302
303
304
Lemma test_iNext_plus_2 P n m : ^n ^m P - ^(n+m) P.
Proof. iIntros "H". iNext. done. Qed.
Lemma test_iNext_plus_3 P Q n m k :
  ^m ^(2 + S n + k) P - ^m  ^(2 + S n) Q - ^k  ^(S (S n + S m)) (P  Q).
Proof. iIntros "H1 H2". iNext. iNext. iNext. iFrame. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
305

306
307
308
309
310
311
312
313
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.

314
315
316
317
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.

318
319
320
321
322
323
324
Lemma test_iEval x y :  (y + x)%nat = 1  -  S (x + y) = 2%nat  : uPred M.
Proof.
  iIntros (H).
  iEval (rewrite (Nat.add_comm x y) // H).
  done.
Qed.

325
326
327
328
329
330
(* TODO: This test is broken in Coq 8.6. Should be restored once we drop Coq
8.6 support. See also issue #108. *)
(*
Lemma test_iIntros_pure : (⌜ ¬False ⌝ : uPred M)%I.
Proof. by iIntros (?). Qed.
*)
Ralf Jung's avatar
Ralf Jung committed
331
End tests.
Robbert Krebbers's avatar
Robbert Krebbers committed
332
333
334
335
336
337
338
339
340
341
342
343
344
345

Section more_tests.
  Context `{invG Σ}.
  Implicit Types P Q R : iProp Σ.

  Lemma test_masks  N E P Q R :
    N  E 
    (True - P - inv N Q - True - R) - P -  Q ={E}= R.
  Proof.
    iIntros (?) "H HP HQ".
    iApply ("H" with "[% //] [$] [> HQ] [> //]").
    by iApply inv_alloc.
  Qed.
End more_tests.