proofmode_ascii.v 10.9 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".
8
Unset Mangle Names.
9

Ralf Jung's avatar
Ralf Jung committed
10
11
12
13
(* Remove this and the [Set Printing Raw Literals.] below once we require Coq
8.14. *)
Set Warnings "-unknown-option".

14
Section base_logic_tests.
15
  Context {M : ucmra}.
16
17
18
  Implicit Types P Q R : uPred M.

  Lemma test_random_stuff (P1 P2 P3 : nat -> uPred M) :
Gregory Malecha's avatar
Gregory Malecha committed
19
    |- forall (x y : nat) a b,
20
      x  y ->
Gregory Malecha's avatar
Gregory Malecha committed
21
      <#> (uPred_ownM (a  b) -*
22
      (exists y1 y2 c, P1 ((x + y1) + y2) /\ True /\ <#> uPred_ownM c) -*
Gregory Malecha's avatar
Gregory Malecha committed
23
      <#> |> (forall z, P2 z  True -> P2 z) -*
24
      |> (forall n m : nat, P1 n -> <#> (True /\ P2 n -> <#> (n = n <-> P3 n))) -*
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
      |> 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
44
     x -> y  z |-@{uPredI M}  x /\  x /\ y  z.
45
46
47
48
49
50
51
52
53
54
  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.
55
  Proof. iStartProof (uPredI _). iStartProof (uPredI _). iIntros "$". Qed.
56
  Lemma test_iStartProof_4 P : P -* P.
57
  Proof. iStartProof (uPredI _). iStartProof (uPred _). iIntros "$". Qed.
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
122
123
124
125
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
126
         |- |={}=> na_own t E1 ** na_own t E2  ** |> P.
127
128
129
130
131
132
133
134
135
  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
136
         |- |={}=> na_own t E1 ** na_own t E2  ** |> P.
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
165
166
167
168
  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 ->
169
170
    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.
171
172
173
174
175
176
177
  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 *)
178
  Lemma test_iInv_8 N :  P, inv N P ={}=* P  True /\ inv N P.
179
180
181
182
183
184
185
186
  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 ->
187
188
    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.
189
190
191
192
193
194
195
196
197
  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 ->
198
199
    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.
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
245
246
247
248
  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
249
    inv N 𝓟⎤ |-@{monPredI} |={E}=> emp.
250
251
252
253
254
255
256
257
258
  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
259
    inv N 𝓟⎤ |-@{monPredI} |={E}=> emp.
260
261
262
263
264
265
266
  Proof.
    iIntros (?) "Hinv".
    iInv N as "HP" "Hclose". Show.
    iMod ("Hclose" with "HP"). auto.
  Qed.

End monpred_tests.
267
268
269

(** Test specifically if certain things parse correctly. *)
Section parsing_tests.
270
Context {PROP : bi}.
271
272
Implicit Types P : PROP.

Gregory Malecha's avatar
Gregory Malecha committed
273
Lemma test_bi_emp_valid : |-@{PROP} True.
274
275
Proof. naive_solver. Qed.

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

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

Gregory Malecha's avatar
Gregory Malecha committed
282
Lemma test_bi_emp_valid_parens_space_close : (|-@{PROP} True ).
283
284
285
Proof. naive_solver. Qed.

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

Lemma test_entails_annot_sections_parens P :
Gregory Malecha's avatar
Gregory Malecha committed
291
  ((P |-@{PROP} P)) /\ ((|-@{PROP})) P P /\
292
293
294
295
  ((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
296
  ( P |-@{PROP} P) /\
297
298
299
300
  ( P -|-@{PROP} P).
Proof. naive_solver. Qed.

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

305
306
307
(* Make sure these all parse as they should.
To make the [Check] print correctly, we need to set and reset the printing
settings each time. *)
308
Check "p1".
Gregory Malecha's avatar
Gregory Malecha committed
309
Lemma p1 : forall P, True -> P |- P.
310
Proof.
Enrico Tassi's avatar
Enrico Tassi committed
311
  Unset Printing Notations. Set Printing Raw Literals. Show. Set Printing Notations. Unset Printing Raw Literals.
312
313
314
Abort.

Check "p2".
Gregory Malecha's avatar
Gregory Malecha committed
315
Lemma p2 : forall P, True /\ (P |- P).
316
Proof.
Enrico Tassi's avatar
Enrico Tassi committed
317
  Unset Printing Notations. Set Printing Raw Literals. Show. Set Printing Notations. Unset Printing Raw Literals.
318
319
320
Abort.

Check "p3".
Gregory Malecha's avatar
Gregory Malecha committed
321
Lemma p3 : exists P, P |- P.
322
Proof.
Enrico Tassi's avatar
Enrico Tassi committed
323
  Unset Printing Notations. Set Printing Raw Literals. Show. Set Printing Notations. Unset Printing Raw Literals.
324
325
326
Abort.

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

Check "p5".
Gregory Malecha's avatar
Gregory Malecha committed
333
Lemma p5 : |-@{PROP} exists (x : nat), forall y : nat, y = y.
334
Proof.
Enrico Tassi's avatar
Enrico Tassi committed
335
  Unset Printing Notations. Set Printing Raw Literals. Show. Set Printing Notations. Unset Printing Raw Literals.
336
337
338
Abort.

Check "p6".
Gregory Malecha's avatar
Gregory Malecha committed
339
Lemma p6 : exists! (z : nat), |-@{PROP} exists (x : nat), forall y : nat, y = y ** z = 0.
340
Proof.
Enrico Tassi's avatar
Enrico Tassi committed
341
  Unset Printing Notations. Set Printing Raw Literals. Show. Set Printing Notations. Unset Printing Raw Literals.
342
343
344
Abort.

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

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

Check "p9".
Gregory Malecha's avatar
Gregory Malecha committed
357
Lemma p9 : forall (a : nat), a = 0 -> forall y : nat, |-@{PROP} forall z : nat, z >= 0.
358
Proof.
Enrico Tassi's avatar
Enrico Tassi committed
359
  Unset Printing Notations. Set Printing Raw Literals. Show. Set Printing Notations. Unset Printing Raw Literals.
360
361
Abort.

362
End parsing_tests.