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

Robbert Krebbers's avatar
Robbert Krebbers committed
113
Lemma test_iAssert_persistent P Q : P - Q - True.
Robbert Krebbers's avatar
Robbert Krebbers committed
114
115
116
117
118
119
120
121
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.
122

Robbert Krebbers's avatar
Robbert Krebbers committed
123
Lemma test_iSpecialize_auto_frame P Q R :
124
  (P - True - True - Q - R) - P - Q - R.
125
Proof. iIntros "H ? HQ". by iApply ("H" with "[$]"). Qed.
126
127

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

131
132
133
134
135
136
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
137
Lemma test_iAssert_modality P : (|==> False) - |==> P.
138
Proof. iIntros. iAssert False%I with "[> - //]" as %[]. Qed.
139

Robbert Krebbers's avatar
Robbert Krebbers committed
140
Lemma test_iAssumption_False P : False - P.
141
Proof. iIntros "H". done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
142
143

(* Check instantiation and dependent types *)
Robbert Krebbers's avatar
Robbert Krebbers committed
144
Lemma test_iSpecialize_dependent_type (P :  n, vec nat n  uPred M) :
Robbert Krebbers's avatar
Robbert Krebbers committed
145
146
147
148
149
  ( 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
150

Robbert Krebbers's avatar
Robbert Krebbers committed
151
Lemma test_eauto_iFrame P Q R `{!Persistent R} :
Robbert Krebbers's avatar
Robbert Krebbers committed
152
  P - Q - R - R  Q  P  R  False.
153
Proof. eauto 10 with iFrame. Qed.
154

155
Lemma test_iCombine_persistent P Q R `{!Persistent R} :
156
157
  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
158

Robbert Krebbers's avatar
Robbert Krebbers committed
159
Lemma test_iNext_evar P : P - True.
Ralf Jung's avatar
Ralf Jung committed
160
161
162
163
Proof.
  iIntros "HP". iAssert ( _ -  P)%I as "?"; last done.
  iIntros "?". iNext. iAssumption.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
164

Robbert Krebbers's avatar
Robbert Krebbers committed
165
Lemma test_iNext_sep1 P Q
Robbert Krebbers's avatar
Robbert Krebbers committed
166
167
168
169
170
171
    (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.
172

Robbert Krebbers's avatar
Robbert Krebbers committed
173
Lemma test_iNext_sep2 P Q :  P   Q -  (P  Q).
174
175
176
Proof.
  iIntros "H". iNext. iExact "H". (* Check that the laters are all gone. *)
Qed.
177

Robbert Krebbers's avatar
Robbert Krebbers committed
178
179
180
181
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
182
Lemma test_iFrame_persistent (P Q : uPred M) :
183
184
   P - Q -  (P  P)  (P  Q  Q).
Proof. iIntros "#HP". iFrame "HP". iIntros "$". Qed.
185

186
Lemma test_iSplit_persistently P Q :  P -  (P  P).
187
Proof. iIntros "#?". by iSplit. Qed.
Ralf Jung's avatar
Ralf Jung committed
188

Robbert Krebbers's avatar
Robbert Krebbers committed
189
Lemma test_iSpecialize_persistent P Q :
190
191
   P - ( P - Q) - Q.
Proof. iIntros "#HP HPQ". by iSpecialize ("HPQ" with "HP"). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
192
193
194
195
196
197

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

199
200
201
202
203
204
205
206
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.

207
208
209
210
211
212
213
214
215
216
217
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.
218
219
220
221
222
223
224
225
226
227
228
229

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.
230
231
232
233
234
235
236
237

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.
238
239
240
241

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

Robbert Krebbers's avatar
Robbert Krebbers committed
243
244
245
246
247
248
249
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
(* 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
287
288
289
290
291
292
293
Lemma test_iNext_laterN_later P n :  ^n P  ^n  P.
Proof. iIntros "H". iNext. by iNext. Qed.
Lemma test_iNext_later_laterN P n : ^n  P   ^n P.
Proof. iIntros "H". iNext. by iNext. Qed.
Lemma test_iNext_laterN_laterN P n1 n2 :  ^n1 ^n2 P  ^n1 ^n2  P.
Proof. iIntros "H". iNext. iNext. by iNext. Qed.

294
295
296
297
298
299
300
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.

301
302
303
304
305
306
(* 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
307
End tests.
Robbert Krebbers's avatar
Robbert Krebbers committed
308
309
310
311
312
313
314
315
316
317
318
319
320
321

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.