proofmode_iris.v 7.74 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
From iris.proofmode Require Import tactics monpred.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
2 3
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
4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39

Section base_logic_tests.
  Context {M : ucmraT}.
  Implicit Types P Q R : uPred M.

  Lemma test_random_stuff (P1 P2 P3 : nat  uPred M) :
    ( (x y : nat) a b,
      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))) -
       x = 0   x z,  P3 (x + z)  uPred_ownM b  uPred_ownM (core b)))%I.
  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) :
     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
40 41 42 43 44 45 46 47 48

  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.
  Proof. iStartProof (uPredI _). iStartProof (uPredSI _). iIntros "$". Qed.
  Lemma test_iStartProof_4 P : P - P.
  Proof. iStartProof (uPredSI _). iStartProof (uPred _). iIntros "$". Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
49 50 51
End base_logic_tests.

Section iris_tests.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
52
  Context `{invG Σ, cinvG Σ, na_invG Σ}.
Ralf Jung's avatar
Ralf Jung committed
53
  Implicit Types P Q R : iProp Σ.
Robbert Krebbers's avatar
Robbert Krebbers committed
54 55 56 57 58 59 60 61 62

  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
63

64
  Lemma test_iInv_0 N P: inv N (<pers> P) ={}=  P.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
65 66
  Proof.
    iIntros "#H".
67
    iInv N as "#H2". Show.
Ralf Jung's avatar
Ralf Jung committed
68
    iModIntro. iSplit; auto.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
69 70
  Qed.

71 72 73
  Lemma test_iInv_0_with_close N P: inv N (<pers> P) ={}=  P.
  Proof.
    iIntros "#H".
74
    iInv N as "#H2" "Hclose". Show.
75 76 77 78
    iMod ("Hclose" with "H2").
    iModIntro. by iNext.
  Qed.

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

Joseph Tassarotti's avatar
Joseph Tassarotti committed
88
  Lemma test_iInv_2 γ p N P:
89
    cinv N γ (<pers> P)  cinv_own γ p ={}= cinv_own γ p   P.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
90 91
  Proof.
    iIntros "(#?&?)".
92
    iInv N as "(#HP&Hown)". Show.
Ralf Jung's avatar
Ralf Jung committed
93
    iModIntro. iSplit; auto with iFrame.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
94 95
  Qed.

96 97 98 99
  Lemma test_iInv_2_with_close γ p N P:
    cinv N γ (<pers> P)  cinv_own γ p ={}= cinv_own γ p   P.
  Proof.
    iIntros "(#?&?)".
100
    iInv N as "(#HP&Hown)" "Hclose". Show.
101 102 103 104
    iMod ("Hclose" with "HP").
    iModIntro. iFrame. by iNext.
  Qed.

Joseph Tassarotti's avatar
Joseph Tassarotti committed
105
  Lemma test_iInv_3 γ p1 p2 N P:
106
    cinv N γ (<pers> P)  cinv_own γ p1  cinv_own γ p2
Joseph Tassarotti's avatar
Joseph Tassarotti committed
107 108 109
      ={}= cinv_own γ p1  cinv_own γ p2    P.
  Proof.
    iIntros "(#?&Hown1&Hown2)".
Ralf Jung's avatar
Ralf Jung committed
110 111
    iInv N with "[Hown2 //]" as "(#HP&Hown2)".
    iModIntro. iSplit; auto with iFrame.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
112 113 114 115
  Qed.

  Lemma test_iInv_4 t N E1 E2 P:
    N  E2 
116
    na_inv t N (<pers> P)  na_own t E1  na_own t E2
Joseph Tassarotti's avatar
Joseph Tassarotti committed
117 118 119
          |={}=> na_own t E1  na_own t E2    P.
  Proof.
    iIntros (?) "(#?&Hown1&Hown2)".
120
    iInv N as "(#HP&Hown2)". Show.
Ralf Jung's avatar
Ralf Jung committed
121
    iModIntro. iSplitL "Hown2"; auto with iFrame.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
122 123
  Qed.

124 125 126 127 128 129
  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.
    iIntros (?) "(#?&Hown1&Hown2)".
130
    iInv N as "(#HP&Hown2)" "Hclose". Show.
131 132 133 134 135
    iMod ("Hclose" with "[HP Hown2]").
    { iFrame. done. }
    iModIntro. iFrame. by iNext.
  Qed.

Joseph Tassarotti's avatar
Joseph Tassarotti committed
136 137 138
  (* test named selection of which na_own to use *)
  Lemma test_iInv_5 t N E1 E2 P:
    N  E2 
139
    na_inv t N (<pers> P)  na_own t E1  na_own t E2
Joseph Tassarotti's avatar
Joseph Tassarotti committed
140 141 142
      ={}= na_own t E1  na_own t E2    P.
  Proof.
    iIntros (?) "(#?&Hown1&Hown2)".
Ralf Jung's avatar
Ralf Jung committed
143 144
    iInv N with "Hown2" as "(#HP&Hown2)".
    iModIntro. iSplitL "Hown2"; auto with iFrame.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
145 146 147 148
  Qed.

  Lemma test_iInv_6 t N E1 E2 P:
    N  E1 
149
    na_inv t N (<pers> P)  na_own t E1  na_own t E2
Joseph Tassarotti's avatar
Joseph Tassarotti committed
150 151 152
      ={}= na_own t E1  na_own t E2    P.
  Proof.
    iIntros (?) "(#?&Hown1&Hown2)".
Ralf Jung's avatar
Ralf Jung committed
153 154
    iInv N with "Hown1" as "(#HP&Hown1)".
    iModIntro. iSplitL "Hown1"; auto with iFrame.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
155 156 157 158 159
  Qed.

  (* test robustness in presence of other invariants *)
  Lemma test_iInv_7 t N1 N2 N3 E1 E2 P:
    N3  E1 
160
    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
161 162 163
      ={}= na_own t E1  na_own t E2    P.
  Proof.
    iIntros (?) "(#?&#?&#?&Hown1&Hown2)".
Ralf Jung's avatar
Ralf Jung committed
164 165
    iInv N3 with "Hown1" as "(#HP&Hown1)".
    iModIntro. iSplitL "Hown1"; auto with iFrame.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
166 167 168 169 170 171
  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
172
    iInv N as "HP". iFrame "HP". auto.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
173
  Qed.
174 175 176 177

  (* test selection by hypothesis name instead of namespace *)
  Lemma test_iInv_9 t N1 N2 N3 E1 E2 P:
    N3  E1 
178
    inv N1 P  na_inv t N3 (<pers> P)  inv N2 P   na_own t E1  na_own t E2
179 180 181
      ={}= na_own t E1  na_own t E2    P.
  Proof.
    iIntros (?) "(#?&#HInv&#?&Hown1&Hown2)".
Ralf Jung's avatar
Ralf Jung committed
182 183
    iInv "HInv" with "Hown1" as "(#HP&Hown1)".
    iModIntro. iSplitL "Hown1"; auto with iFrame.
184 185 186 187 188
  Qed.

  (* test selection by hypothesis name instead of namespace *)
  Lemma test_iInv_10 t N1 N2 N3 E1 E2 P:
    N3  E1 
189
    inv N1 P  na_inv t N3 (<pers> P)  inv N2 P   na_own t E1  na_own t E2
190 191 192
      ={}= na_own t E1  na_own t E2    P.
  Proof.
    iIntros (?) "(#?&#HInv&#?&Hown1&Hown2)".
Ralf Jung's avatar
Ralf Jung committed
193 194
    iInv "HInv" as "(#HP&Hown1)".
    iModIntro. iSplitL "Hown1"; auto with iFrame.
195 196 197
  Qed.

  (* test selection by ident name *)
198
  Lemma test_iInv_11 N P: inv N (<pers> P) ={}=  P.
199 200
  Proof.
    let H := iFresh in
Ralf Jung's avatar
Ralf Jung committed
201
    (iIntros H; iInv H as "#H2"). auto.
202 203 204
  Qed.

  (* error messages *)
205
  Lemma test_iInv_12 N P: inv N (<pers> P) ={}= True.
206 207
  Proof.
    iIntros "H".
Ralf Jung's avatar
Ralf Jung committed
208 209 210
    Fail iInv 34 as "#H2".
    Fail iInv nroot as "#H2".
    Fail iInv "H2" as "#H2".
211 212
    done.
  Qed.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
213 214 215 216 217

  (* 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
218 219
    iIntros "H"; iInv "H" as (v1 v2 v3) "(?&?&_)".
    eauto.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
220
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
221
End iris_tests.
Ralf Jung's avatar
Ralf Jung committed
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 249 250

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

  Lemma test_iInv N E 𝓟 :
    N  E 
    inv N 𝓟⎤ @{monPredI} |={E}=> emp.
  Proof.
    iIntros (?) "Hinv".
    iInv N as "HP". Show.
    iFrame "HP". auto.
  Qed.

  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.