proofmode_ascii.v 10.3 KB
Newer Older
1
2
3
4
5
6
From iris.proofmode Require Import tactics monpred.
From iris.base_logic Require Import base_logic.
From iris.base_logic.lib Require Import invariants cancelable_invariants na_invariants.

From iris.bi Require Import ascii.

7
Set Default Proof Using "Type".
Ralf Jung's avatar
Ralf Jung committed
8
Unset Printing Use Implicit Types. (* FIXME: remove once we drop support for Coq <=8.11. *)
9

10
11
12
13
14
Section base_logic_tests.
  Context {M : ucmraT}.
  Implicit Types P Q R : uPred M.

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

  Lemma test_iFrame_pure (x y z : M) :
Gregory Malecha's avatar
Gregory Malecha committed
40
     x -> y  z |-@{uPredI M}  x /\  x /\ y  z.
41
42
43
44
45
46
47
48
49
50
  Proof. iIntros (Hv) "Hxy". by iFrame (Hv) "Hxy". Qed.

  Lemma test_iAssert_modality P : (|==> False) -* |==> P.
  Proof. iIntros. iAssert False%I with "[> - //]" as %[]. Qed.

  Lemma test_iStartProof_1 P : P -* P.
  Proof. iStartProof. iStartProof. iIntros "$". Qed.
  Lemma test_iStartProof_2 P : P -* P.
  Proof. iStartProof (uPred _). iStartProof (uPredI _). iIntros "$". Qed.
  Lemma test_iStartProof_3 P : P -* P.
51
  Proof. iStartProof (uPredI _). iStartProof (uPredI _). iIntros "$". Qed.
52
  Lemma test_iStartProof_4 P : P -* P.
53
  Proof. iStartProof (uPredI _). iStartProof (uPred _). iIntros "$". Qed.
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
End base_logic_tests.

Section iris_tests.
  Context `{!invG Σ, !cinvG Σ, !na_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.

  Lemma test_iInv_0 N P: inv N (<pers> P) ={}=* |> P.
  Proof.
    iIntros "#H".
    iInv N as "#H2". Show.
    iModIntro. iSplit; auto.
  Qed.

  Lemma test_iInv_0_with_close N P: inv N (<pers> P) ={}=* |> P.
  Proof.
    iIntros "#H".
    iInv N as "#H2" "Hclose". Show.
    iMod ("Hclose" with "H2").
    iModIntro. by iNext.
  Qed.

  Lemma test_iInv_1 N E P:
    N  E ->
    inv N (<pers> P) ={E}=* |> P.
  Proof.
    iIntros (?) "#H".
    iInv N as "#H2".
    iModIntro. iSplit; auto.
  Qed.

  Lemma test_iInv_2 γ p N P:
    cinv N γ (<pers> P) ** cinv_own γ p ={}=* cinv_own γ p ** |> P.
  Proof.
    iIntros "(#?&?)".
    iInv N as "(#HP&Hown)". Show.
    iModIntro. iSplit; auto with iFrame.
  Qed.

  Lemma test_iInv_2_with_close γ p N P:
    cinv N γ (<pers> P) ** cinv_own γ p ={}=* cinv_own γ p ** |> P.
  Proof.
    iIntros "(#?&?)".
    iInv N as "(#HP&Hown)" "Hclose". Show.
    iMod ("Hclose" with "HP").
    iModIntro. iFrame. by iNext.
  Qed.

  Lemma test_iInv_3 γ p1 p2 N P:
    cinv N γ (<pers> P) ** cinv_own γ p1 ** cinv_own γ p2
      ={}=* cinv_own γ p1 ** cinv_own γ p2  ** |> P.
  Proof.
    iIntros "(#?&Hown1&Hown2)".
    iInv N with "[Hown2 //]" as "(#HP&Hown2)".
    iModIntro. iSplit; auto with iFrame.
  Qed.

  Lemma test_iInv_4 t N E1 E2 P:
    N  E2 ->
    na_inv t N (<pers> P) ** na_own t E1 ** na_own t E2
Gregory Malecha's avatar
Gregory Malecha committed
122
         |- |={}=> na_own t E1 ** na_own t E2  ** |> P.
123
124
125
126
127
128
129
130
131
  Proof.
    iIntros (?) "(#?&Hown1&Hown2)".
    iInv N as "(#HP&Hown2)". Show.
    iModIntro. iSplitL "Hown2"; auto with iFrame.
  Qed.

  Lemma test_iInv_4_with_close t N E1 E2 P:
    N  E2 ->
    na_inv t N (<pers> P) ** na_own t E1 ** na_own t E2
Gregory Malecha's avatar
Gregory Malecha committed
132
         |- |={}=> na_own t E1 ** na_own t E2  ** |> P.
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
  Proof.
    iIntros (?) "(#?&Hown1&Hown2)".
    iInv N as "(#HP&Hown2)" "Hclose". Show.
    iMod ("Hclose" with "[HP Hown2]").
    { iFrame. done. }
    iModIntro. iFrame. by iNext.
  Qed.

  (* test named selection of which na_own to use *)
  Lemma test_iInv_5 t N E1 E2 P:
    N  E2 ->
    na_inv t N (<pers> P) ** na_own t E1 ** na_own t E2
      ={}=* na_own t E1 ** na_own t E2  ** |> P.
  Proof.
    iIntros (?) "(#?&Hown1&Hown2)".
    iInv N with "Hown2" as "(#HP&Hown2)".
    iModIntro. iSplitL "Hown2"; auto with iFrame.
  Qed.

  Lemma test_iInv_6 t N E1 E2 P:
    N  E1 ->
    na_inv t N (<pers> P) ** na_own t E1 ** na_own t E2
      ={}=* na_own t E1 ** na_own t E2  ** |> P.
  Proof.
    iIntros (?) "(#?&Hown1&Hown2)".
    iInv N with "Hown1" as "(#HP&Hown1)".
    iModIntro. iSplitL "Hown1"; auto with iFrame.
  Qed.

  (* test robustness in presence of other invariants *)
  Lemma test_iInv_7 t N1 N2 N3 E1 E2 P:
    N3  E1 ->
165
166
    inv N1 P ** na_inv t N3 (<pers> P) ** inv N2 P ** na_own t E1 ** na_own t E2
      ={}=* na_own t E1 ** na_own t E2 ** |> P.
167
168
169
170
171
172
173
  Proof.
    iIntros (?) "(#?&#?&#?&Hown1&Hown2)".
    iInv N3 with "Hown1" as "(#HP&Hown1)".
    iModIntro. iSplitL "Hown1"; auto with iFrame.
  Qed.

  (* iInv should work even where we have "inv N P" in which P contains an evar *)
174
  Lemma test_iInv_8 N :  P, inv N P ={}=* P  True /\ inv N P.
175
176
177
178
179
180
181
182
  Proof.
    eexists. iIntros "#H".
    iInv N as "HP". iFrame "HP". auto.
  Qed.

  (* test selection by hypothesis name instead of namespace *)
  Lemma test_iInv_9 t N1 N2 N3 E1 E2 P:
    N3  E1 ->
183
184
    inv N1 P ** na_inv t N3 (<pers> P) ** inv N2 P ** na_own t E1 ** na_own t E2
      ={}=* na_own t E1 ** na_own t E2 ** |> P.
185
186
187
188
189
190
191
192
193
  Proof.
    iIntros (?) "(#?&#HInv&#?&Hown1&Hown2)".
    iInv "HInv" with "Hown1" as "(#HP&Hown1)".
    iModIntro. iSplitL "Hown1"; auto with iFrame.
  Qed.

  (* test selection by hypothesis name instead of namespace *)
  Lemma test_iInv_10 t N1 N2 N3 E1 E2 P:
    N3  E1 ->
194
195
    inv N1 P ** na_inv t N3 (<pers> P) ** inv N2 P ** na_own t E1 ** na_own t E2
      ={}=* na_own t E1 ** na_own t E2 ** |> P.
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
  Proof.
    iIntros (?) "(#?&#HInv&#?&Hown1&Hown2)".
    iInv "HInv" as "(#HP&Hown1)".
    iModIntro. iSplitL "Hown1"; auto with iFrame.
  Qed.

  (* test selection by ident name *)
  Lemma test_iInv_11 N P: inv N (<pers> P) ={}=* |> P.
  Proof.
    let H := iFresh in
    (iIntros H; iInv H as "#H2"). auto.
  Qed.

  (* error messages *)
  Check "test_iInv_12".
  Lemma test_iInv_12 N P: inv N (<pers> P) ={}=* True.
  Proof.
    iIntros "H".
    Fail iInv 34 as "#H2".
    Fail iInv nroot as "#H2".
    Fail iInv "H2" as "#H2".
    done.
  Qed.

  (* test destruction of existentials when opening an invariant *)
  Lemma test_iInv_13 N:
    inv N ( (v1 v2 v3 : nat), emp ** emp ** emp) ={}=* |> emp.
  Proof.
    iIntros "H"; iInv "H" as (v1 v2 v3) "(?&?&_)".
    eauto.
  Qed.

  Theorem test_iApply_inG `{!inG Σ A} γ (x x' : A) :
    x'  x ->
    own γ x -* own γ x'.
  Proof. intros. by iApply own_mono. Qed.
End iris_tests.

Section monpred_tests.
  Context `{!invG Σ}.
  Context {I : biIndex}.
  Local Notation monPred := (monPred I (iPropI Σ)).
  Local Notation monPredI := (monPredI I (iPropI Σ)).
  Implicit Types P Q R : monPred.
  Implicit Types 𝓟 𝓠 𝓡 : iProp Σ.

  Check "test_iInv".
  Lemma test_iInv N E 𝓟 :
    N  E ->
Gregory Malecha's avatar
Gregory Malecha committed
245
    inv N 𝓟⎤ |-@{monPredI} |={E}=> emp.
246
247
248
249
250
251
252
253
254
  Proof.
    iIntros (?) "Hinv".
    iInv N as "HP". Show.
    iFrame "HP". auto.
  Qed.

  Check "test_iInv_with_close".
  Lemma test_iInv_with_close N E 𝓟 :
    N  E ->
Gregory Malecha's avatar
Gregory Malecha committed
255
    inv N 𝓟⎤ |-@{monPredI} |={E}=> emp.
256
257
258
259
260
261
262
  Proof.
    iIntros (?) "Hinv".
    iInv N as "HP" "Hclose". Show.
    iMod ("Hclose" with "HP"). auto.
  Qed.

End monpred_tests.
263
264
265

(** Test specifically if certain things parse correctly. *)
Section parsing_tests.
266
Context {PROP : bi}.
267
268
Implicit Types P : PROP.

Gregory Malecha's avatar
Gregory Malecha committed
269
Lemma test_bi_emp_valid : |-@{PROP} True.
270
271
Proof. naive_solver. Qed.

Gregory Malecha's avatar
Gregory Malecha committed
272
Lemma test_bi_emp_valid_parens : (|-@{PROP} True) /\ ((|-@{PROP} True)).
273
274
Proof. naive_solver. Qed.

Gregory Malecha's avatar
Gregory Malecha committed
275
Lemma test_bi_emp_valid_parens_space_open : ( |-@{PROP} True).
276
277
Proof. naive_solver. Qed.

Gregory Malecha's avatar
Gregory Malecha committed
278
Lemma test_bi_emp_valid_parens_space_close : (|-@{PROP} True ).
279
280
281
Proof. naive_solver. Qed.

Lemma test_entails_annot_sections P :
Gregory Malecha's avatar
Gregory Malecha committed
282
  (P |-@{PROP} P) /\ (|-@{PROP}) P P /\
283
284
285
286
  (P -|-@{PROP} P) /\ (-|-@{PROP}) P P.
Proof. naive_solver. Qed.

Lemma test_entails_annot_sections_parens P :
Gregory Malecha's avatar
Gregory Malecha committed
287
  ((P |-@{PROP} P)) /\ ((|-@{PROP})) P P /\
288
289
290
291
  ((P -|-@{PROP} P)) /\ ((-|-@{PROP})) P P.
Proof. naive_solver. Qed.

Lemma test_entails_annot_sections_space_open P :
Gregory Malecha's avatar
Gregory Malecha committed
292
  ( P |-@{PROP} P) /\
293
294
295
296
  ( P -|-@{PROP} P).
Proof. naive_solver. Qed.

Lemma test_entails_annot_sections_space_close P :
Gregory Malecha's avatar
Gregory Malecha committed
297
  (P |-@{PROP} P ) /\ (|-@{PROP} ) P P /\
298
299
  (P -|-@{PROP} P ) /\ (-|-@{PROP} ) P P.
Proof. naive_solver. Qed.
300
301
302


Check "p1".
Gregory Malecha's avatar
Gregory Malecha committed
303
Lemma p1 : forall P, True -> P |- P.
304
305
306
307
308
Proof.
  Unset Printing Notations. Show. Set Printing Notations.
Abort.

Check "p2".
Gregory Malecha's avatar
Gregory Malecha committed
309
Lemma p2 : forall P, True /\ (P |- P).
310
311
312
313
314
Proof.
  Unset Printing Notations. Show. Set Printing Notations.
Abort.

Check "p3".
Gregory Malecha's avatar
Gregory Malecha committed
315
Lemma p3 : exists P, P |- P.
316
317
318
319
320
Proof.
  Unset Printing Notations. Show. Set Printing Notations.
Abort.

Check "p4".
Gregory Malecha's avatar
Gregory Malecha committed
321
Lemma p4 : |-@{PROP} exists (x : nat), x = 0.
322
323
324
325
326
Proof.
  Unset Printing Notations. Show. Set Printing Notations.
Abort.

Check "p5".
Gregory Malecha's avatar
Gregory Malecha committed
327
Lemma p5 : |-@{PROP} exists (x : nat), forall y : nat, y = y.
328
329
330
331
332
Proof.
  Unset Printing Notations. Show. Set Printing Notations.
Abort.

Check "p6".
Gregory Malecha's avatar
Gregory Malecha committed
333
Lemma p6 : exists! (z : nat), |-@{PROP} exists (x : nat), forall y : nat, y = y ** z = 0.
334
335
336
337
338
Proof.
  Unset Printing Notations. Show. Set Printing Notations.
Abort.

Check "p7".
Gregory Malecha's avatar
Gregory Malecha committed
339
Lemma p7 : forall (a : nat), a = 0 -> forall y, True |-@{PROP} y >= 0.
340
341
342
343
344
Proof.
  Unset Printing Notations. Show. Set Printing Notations.
Abort.

Check "p8".
Gregory Malecha's avatar
Gregory Malecha committed
345
Lemma p8 : forall (a : nat), a = 0 -> forall y, |-@{PROP} y >= 0.
346
347
348
349
350
Proof.
  Unset Printing Notations. Show. Set Printing Notations.
Abort.

Check "p9".
Gregory Malecha's avatar
Gregory Malecha committed
351
Lemma p9 : forall (a : nat), a = 0 -> forall y : nat, |-@{PROP} forall z : nat, z >= 0.
352
353
354
355
356
357
Proof.
  Unset Printing Notations. Show. Set Printing Notations.
Abort.

Set Printing Notations.

358
End parsing_tests.