proofmode_iris.v 8.63 KB
Newer Older
1
From iris.algebra Require Import frac.
Ralf Jung's avatar
Ralf Jung committed
2
From iris.proofmode Require Import tactics monpred.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
3
4
From iris.base_logic Require Import base_logic.
From iris.base_logic.lib Require Import invariants cancelable_invariants na_invariants.
Robbert Krebbers's avatar
Robbert Krebbers committed
5

6
7
Unset Mangle Names.

Robbert Krebbers's avatar
Robbert Krebbers committed
8
Section base_logic_tests.
9
  Context {M : ucmra}.
Robbert Krebbers's avatar
Robbert Krebbers committed
10
11
  Implicit Types P Q R : uPred M.

12
13
14
  (* Test scopes for bupd *)
  Definition use_bupd_uPred (n : nat) : uPred M :=
     |==>  m : nat ,  n = 2 .
15
16
  Definition use_plainly_uPred (n : nat) : uPred M :=
     |==>  m : nat ,  n = 2 .
17

Robbert Krebbers's avatar
Robbert Krebbers committed
18
  Lemma test_random_stuff (P1 P2 P3 : nat  uPred M) :
Gregory Malecha's avatar
Gregory Malecha committed
19
      (x y : nat) a b,
Robbert Krebbers's avatar
Robbert Krebbers committed
20
21
22
23
24
      x  y 
       (uPred_ownM (a  b) -
      ( y1 y2 c, P1 ((x + y1) + y2)  True   uPred_ownM c) -
        ( z, P2 z  True  P2 z) -
       ( n m : nat, P1 n   ((True  P2 n)   (n = n  P3 n))) -
Gregory Malecha's avatar
Gregory Malecha committed
25
       x = 0   x z,  P3 (x + z)  uPred_ownM b  uPred_ownM (core b)).
Robbert Krebbers's avatar
Robbert Krebbers committed
26
  Proof.
27
    iIntros (i [|j] a b ?) "!> [Ha Hb] H1 #H2 H3"; setoid_subst.
Robbert Krebbers's avatar
Robbert Krebbers committed
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
    { 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) :
     x  y  z - ( x   x  y  z : uPred M).
  Proof. iIntros (Hv) "Hxy". by iFrame (Hv) "Hxy". Qed.

  Lemma test_iAssert_modality P : (|==> False) - |==> P.
  Proof. iIntros. iAssert False%I with "[> - //]" as %[]. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
49
50
51
52
53
54

  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.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
56
  Lemma test_iStartProof_4 P : P - P.
57
  Proof. iStartProof (uPredI _). iStartProof (uPred _). iIntros "$". Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
58
59
60
End base_logic_tests.

Section iris_tests.
61
  Context `{!invG Σ, !cinvG Σ, !na_invG Σ}.
Ralf Jung's avatar
Ralf Jung committed
62
  Implicit Types P Q R : iProp Σ.
Robbert Krebbers's avatar
Robbert Krebbers committed
63

64
65
66
67
68
69
  (* Test scopes for bupd and fupd *)
  Definition use_bupd_iProp (n : nat) : iProp Σ :=
     |==>  m : nat ,  n = 2 .
  Definition use_fupd_iProp (n : nat) : iProp Σ :=
     |={}=>  m : nat ,  n = 2 .

Robbert Krebbers's avatar
Robbert Krebbers committed
70
71
72
73
74
75
76
77
  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.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
78

79
  Lemma test_iInv_0 N P: inv N (<pers> P) ={}=  P.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
80
81
  Proof.
    iIntros "#H".
82
    iInv N as "#H2". Show.
Ralf Jung's avatar
Ralf Jung committed
83
    iModIntro. iSplit; auto.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
84
85
  Qed.

86
87
88
  Lemma test_iInv_0_with_close N P: inv N (<pers> P) ={}=  P.
  Proof.
    iIntros "#H".
89
    iInv N as "#H2" "Hclose". Show.
90
91
92
93
    iMod ("Hclose" with "H2").
    iModIntro. by iNext.
  Qed.

Joseph Tassarotti's avatar
Joseph Tassarotti committed
94
95
  Lemma test_iInv_1 N E P:
    N  E 
96
    inv N (<pers> P) ={E}=  P.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
97
98
  Proof.
    iIntros (?) "#H".
Ralf Jung's avatar
Ralf Jung committed
99
100
    iInv N as "#H2".
    iModIntro. iSplit; auto.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
101
102
  Qed.

Joseph Tassarotti's avatar
Joseph Tassarotti committed
103
  Lemma test_iInv_2 γ p N P:
104
    cinv N γ (<pers> P)  cinv_own γ p ={}= cinv_own γ p   P.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
105
  Proof.
106
    Show.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
107
    iIntros "(#?&?)".
108
    iInv N as "(#HP&Hown)". Show.
Ralf Jung's avatar
Ralf Jung committed
109
    iModIntro. iSplit; auto with iFrame.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
110
111
  Qed.

112
113
114
115
  Lemma test_iInv_2_with_close γ p N P:
    cinv N γ (<pers> P)  cinv_own γ p ={}= cinv_own γ p   P.
  Proof.
    iIntros "(#?&?)".
116
    iInv N as "(#HP&Hown)" "Hclose". Show.
117
118
119
120
    iMod ("Hclose" with "HP").
    iModIntro. iFrame. by iNext.
  Qed.

Joseph Tassarotti's avatar
Joseph Tassarotti committed
121
  Lemma test_iInv_3 γ p1 p2 N P:
122
    cinv N γ (<pers> P)  cinv_own γ p1  cinv_own γ p2
Joseph Tassarotti's avatar
Joseph Tassarotti committed
123
124
125
      ={}= cinv_own γ p1  cinv_own γ p2    P.
  Proof.
    iIntros "(#?&Hown1&Hown2)".
Ralf Jung's avatar
Ralf Jung committed
126
127
    iInv N with "[Hown2 //]" as "(#HP&Hown2)".
    iModIntro. iSplit; auto with iFrame.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
128
129
130
131
  Qed.

  Lemma test_iInv_4 t N E1 E2 P:
    N  E2 
132
    na_inv t N (<pers> P)  na_own t E1  na_own t E2
Joseph Tassarotti's avatar
Joseph Tassarotti committed
133
134
135
          |={}=> na_own t E1  na_own t E2    P.
  Proof.
    iIntros (?) "(#?&Hown1&Hown2)".
136
    iInv N as "(#HP&Hown2)". Show.
Ralf Jung's avatar
Ralf Jung committed
137
    iModIntro. iSplitL "Hown2"; auto with iFrame.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
138
139
  Qed.

140
141
142
143
144
  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
          |={}=> na_own t E1  na_own t E2    P.
  Proof.
145
    Show.
146
    iIntros (?) "(#?&Hown1&Hown2)".
147
    iInv N as "(#HP&Hown2)" "Hclose". Show.
148
149
150
151
152
    iMod ("Hclose" with "[HP Hown2]").
    { iFrame. done. }
    iModIntro. iFrame. by iNext.
  Qed.

Joseph Tassarotti's avatar
Joseph Tassarotti committed
153
154
155
  (* test named selection of which na_own to use *)
  Lemma test_iInv_5 t N E1 E2 P:
    N  E2 
156
    na_inv t N (<pers> P)  na_own t E1  na_own t E2
Joseph Tassarotti's avatar
Joseph Tassarotti committed
157
158
159
      ={}= na_own t E1  na_own t E2    P.
  Proof.
    iIntros (?) "(#?&Hown1&Hown2)".
Ralf Jung's avatar
Ralf Jung committed
160
161
    iInv N with "Hown2" as "(#HP&Hown2)".
    iModIntro. iSplitL "Hown2"; auto with iFrame.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
162
163
164
165
  Qed.

  Lemma test_iInv_6 t N E1 E2 P:
    N  E1 
166
    na_inv t N (<pers> P)  na_own t E1  na_own t E2
Joseph Tassarotti's avatar
Joseph Tassarotti committed
167
168
169
      ={}= na_own t E1  na_own t E2    P.
  Proof.
    iIntros (?) "(#?&Hown1&Hown2)".
Ralf Jung's avatar
Ralf Jung committed
170
171
    iInv N with "Hown1" as "(#HP&Hown1)".
    iModIntro. iSplitL "Hown1"; auto with iFrame.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
172
173
174
175
176
  Qed.

  (* test robustness in presence of other invariants *)
  Lemma test_iInv_7 t N1 N2 N3 E1 E2 P:
    N3  E1 
177
    inv N1 P  na_inv t N3 (<pers> P)  inv N2 P   na_own t E1  na_own t E2
Joseph Tassarotti's avatar
Joseph Tassarotti committed
178
179
180
      ={}= na_own t E1  na_own t E2    P.
  Proof.
    iIntros (?) "(#?&#?&#?&Hown1&Hown2)".
Ralf Jung's avatar
Ralf Jung committed
181
182
    iInv N3 with "Hown1" as "(#HP&Hown1)".
    iModIntro. iSplitL "Hown1"; auto with iFrame.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
183
184
185
186
187
188
  Qed.

  (* iInv should work even where we have "inv N P" in which P contains an evar *)
  Lemma test_iInv_8 N :  P, inv N P ={}= P  True  inv N P.
  Proof.
    eexists. iIntros "#H".
Ralf Jung's avatar
Ralf Jung committed
189
    iInv N as "HP". iFrame "HP". auto.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
190
  Qed.
191
192
193
194

  (* test selection by hypothesis name instead of namespace *)
  Lemma test_iInv_9 t N1 N2 N3 E1 E2 P:
    N3  E1 
195
    inv N1 P  na_inv t N3 (<pers> P)  inv N2 P   na_own t E1  na_own t E2
196
197
198
      ={}= na_own t E1  na_own t E2    P.
  Proof.
    iIntros (?) "(#?&#HInv&#?&Hown1&Hown2)".
Ralf Jung's avatar
Ralf Jung committed
199
200
    iInv "HInv" with "Hown1" as "(#HP&Hown1)".
    iModIntro. iSplitL "Hown1"; auto with iFrame.
201
202
203
204
205
  Qed.

  (* test selection by hypothesis name instead of namespace *)
  Lemma test_iInv_10 t N1 N2 N3 E1 E2 P:
    N3  E1 
206
    inv N1 P  na_inv t N3 (<pers> P)  inv N2 P   na_own t E1  na_own t E2
207
208
209
      ={}= na_own t E1  na_own t E2    P.
  Proof.
    iIntros (?) "(#?&#HInv&#?&Hown1&Hown2)".
Ralf Jung's avatar
Ralf Jung committed
210
211
    iInv "HInv" as "(#HP&Hown1)".
    iModIntro. iSplitL "Hown1"; auto with iFrame.
212
213
214
  Qed.

  (* test selection by ident name *)
215
  Lemma test_iInv_11 N P: inv N (<pers> P) ={}=  P.
216
217
  Proof.
    let H := iFresh in
Ralf Jung's avatar
Ralf Jung committed
218
    (iIntros H; iInv H as "#H2"). auto.
219
220
221
  Qed.

  (* error messages *)
222
  Check "test_iInv_12".
223
  Lemma test_iInv_12 N P: inv N (<pers> P) ={}= True.
224
225
  Proof.
    iIntros "H".
Ralf Jung's avatar
Ralf Jung committed
226
227
228
    Fail iInv 34 as "#H2".
    Fail iInv nroot as "#H2".
    Fail iInv "H2" as "#H2".
229
230
    done.
  Qed.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
231
232
233
234
235

  (* test destruction of existentials when opening an invariant *)
  Lemma test_iInv_13 N:
    inv N ( (v1 v2 v3 : nat), emp  emp  emp) ={}=  emp.
  Proof.
Ralf Jung's avatar
Ralf Jung committed
236
237
    iIntros "H"; iInv "H" as (v1 v2 v3) "(?&?&_)".
    eauto.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
238
  Qed.
239
240
241
242
243

  Theorem test_iApply_inG `{!inG Σ A} γ (x x' : A) :
    x'  x 
    own γ x - own γ x'.
  Proof. intros. by iApply own_mono. Qed.
244
245
246
247
248
249
250
251
252
253

  Check "test_frac_split_combine".
  Lemma test_frac_split_combine `{!inG Σ fracR} γ :
    own γ 1%Qp - own γ 1%Qp.
  Proof.
    iIntros "[H1 H2]". Show.
    iCombine "H1 H2" as "H". Show.
    iExact "H".
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
254
End iris_tests.
Ralf Jung's avatar
Ralf Jung committed
255
256

Section monpred_tests.
257
  Context `{!invG Σ}.
Ralf Jung's avatar
Ralf Jung committed
258
259
260
261
262
263
  Context {I : biIndex}.
  Local Notation monPred := (monPred I (iPropI Σ)).
  Local Notation monPredI := (monPredI I (iPropI Σ)).
  Implicit Types P Q R : monPred.
  Implicit Types 𝓟 𝓠 𝓡 : iProp Σ.

264
  Check "test_iInv".
Ralf Jung's avatar
Ralf Jung committed
265
266
267
268
269
270
271
272
273
  Lemma test_iInv N E 𝓟 :
    N  E 
    inv N 𝓟⎤ @{monPredI} |={E}=> emp.
  Proof.
    iIntros (?) "Hinv".
    iInv N as "HP". Show.
    iFrame "HP". auto.
  Qed.

274
  Check "test_iInv_with_close".
Ralf Jung's avatar
Ralf Jung committed
275
276
277
278
279
280
281
282
283
284
  Lemma test_iInv_with_close N E 𝓟 :
    N  E 
    inv N 𝓟⎤ @{monPredI} |={E}=> emp.
  Proof.
    iIntros (?) "Hinv".
    iInv N as "HP" "Hclose". Show.
    iMod ("Hclose" with "HP"). auto.
  Qed.

End monpred_tests.