proofmode_monpred.v 6.67 KB
Newer Older
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
1
From iris.proofmode Require Import tactics monpred.
2
From iris.base_logic.lib Require Import invariants.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
3

4
5
Unset Mangle Names.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
6
Section tests.
7
  Context {I : biIndex} {PROP : bi}.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
8
9
10
  Local Notation monPred := (monPred I PROP).
  Local Notation monPredI := (monPredI I PROP).
  Implicit Types P Q R : monPred.
11
  Implicit Types 𝓟 𝓠 𝓡 : PROP.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
12
13
14
15
16
17
18
19
20
21
  Implicit Types i j : I.

  Lemma test0 P : P - P.
  Proof. iIntros "$". Qed.

  Lemma test_iStartProof_1 P : P - P.
  Proof. iStartProof. iStartProof. iIntros "$". Qed.
  Lemma test_iStartProof_2 P : P - P.
  Proof. iStartProof monPred. iStartProof monPredI. iIntros "$". Qed.
  Lemma test_iStartProof_3 P : P - P.
22
  Proof. iStartProof monPredI. iStartProof monPredI. iIntros "$". Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
23
  Lemma test_iStartProof_4 P : P - P.
24
  Proof. iStartProof monPredI. iStartProof monPred. iIntros "$". Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
25
26
27
28
  Lemma test_iStartProof_5 P : P - P.
  Proof. iStartProof PROP. iIntros (i) "$". Qed.
  Lemma test_iStartProof_6 P : P  P.
  Proof. iStartProof PROP. iIntros (i). iSplit; iIntros "$". Qed.
29
  Lemma test_iStartProof_7 `{!BiInternalEq PROP} P : @{monPredI} P  P.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
30
31
  Proof. iStartProof PROP. done. Qed.

32
33
  Lemma test_intowand_1 P Q : (P - Q) - P - Q.
  Proof.
Ralf Jung's avatar
Ralf Jung committed
34
35
    iStartProof PROP. iIntros (i) "HW". Show.
    iIntros (j ->) "HP". Show. by iApply "HW".
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
  Qed.
  Lemma test_intowand_2 P Q : (P - Q) - P - Q.
  Proof.
    iStartProof PROP. iIntros (i) "HW". iIntros (j ->) "HP".
    iSpecialize ("HW" with "[HP //]"). done.
  Qed.
  Lemma test_intowand_3 P Q : (P - Q) - P - Q.
  Proof.
    iStartProof PROP. iIntros (i) "HW". iIntros (j ->) "HP".
    iSpecialize ("HW" with "HP"). done.
  Qed.
  Lemma test_intowand_4 P Q : (P - Q) -  P -  Q.
  Proof.
    iStartProof PROP. iIntros (i) "HW". iIntros (j ->) "HP". by iApply "HW".
  Qed.
  Lemma test_intowand_5 P Q : (P - Q) -  P -  Q.
  Proof.
    iStartProof PROP. iIntros (i) "HW". iIntros (j ->) "HP".
    iSpecialize ("HW" with "HP"). done.
  Qed.
56

57
58
  Lemma test_apply_in_elim (P : monPredI) (i : I) : monPred_in i -  P i   P.
  Proof. iIntros. by iApply monPred_in_elim. Qed.
59
60
61
62
63
64
65
66
67

  Lemma test_iStartProof_forall_1 (Φ : nat  monPredI) :  n, Φ n - Φ n.
  Proof.
    iStartProof PROP. iIntros (n i) "$".
  Qed.
  Lemma test_iStartProof_forall_2 (Φ : nat  monPredI) :  n, Φ n - Φ n.
  Proof.
    iStartProof. iIntros (n) "$".
  Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
68
69
70
71
72

  Lemma test_embed_wand (P Q : PROP) : (P - Q) - P - Q : monPred.
  Proof.
    iIntros "H HP". by iApply "H".
  Qed.
73

Robbert Krebbers's avatar
Robbert Krebbers committed
74
  Lemma test_objectively P Q : <obj> emp - <obj> P - <obj> Q - <obj> (P  Q).
Ralf Jung's avatar
Ralf Jung committed
75
  Proof. iIntros "#? HP HQ". iModIntro. by iSplitL "HP". Qed.
76

77
  Lemma test_objectively_absorbing P Q R `{!Absorbing P} :
Robbert Krebbers's avatar
Robbert Krebbers committed
78
    <obj> emp - <obj> P - <obj> Q - R - <obj> (P  Q).
Ralf Jung's avatar
Ralf Jung committed
79
  Proof. iIntros "#? HP HQ HR". iModIntro. by iSplitL "HP". Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
80

81
  Lemma test_objectively_affine P Q R `{!Affine R} :
Robbert Krebbers's avatar
Robbert Krebbers committed
82
    <obj> emp - <obj> P - <obj> Q - R - <obj> (P  Q).
Ralf Jung's avatar
Ralf Jung committed
83
  Proof. iIntros "#? HP HQ HR". iModIntro. by iSplitL "HP". Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
84

85
86
  Lemma test_iModIntro_embed P `{!Affine Q} 𝓟 𝓠 :
     P - Q - ⎡𝓟⎤ - ⎡𝓠⎤ -  𝓟  𝓠 .
Ralf Jung's avatar
Ralf Jung committed
87
  Proof. iIntros "#H1 _ H2 H3". iModIntro. iFrame. Qed.
88

89
  Lemma test_iModIntro_embed_objective P `{!Objective Q} 𝓟 𝓠 :
90
     P - Q - ⎡𝓟⎤ - ⎡𝓠⎤ -   i, 𝓟  𝓠  Q i .
Ralf Jung's avatar
Ralf Jung committed
91
  Proof. iIntros "#H1 H2 H3 H4". iModIntro. Show. iFrame. Qed.
92

93
94
95
96
  Lemma test_iModIntro_embed_nested P 𝓟 𝓠 :
     P - ⎡◇ 𝓟⎤ - ⎡◇ 𝓠⎤ -   (𝓟  𝓠) .
  Proof. iIntros "#H1 H2 H3". iModIntro  _ %I. by iSplitL "H2". Qed.

97
98
  Lemma test_into_wand_embed 𝓟 𝓠 :
    (𝓟 -  𝓠) 
Ralf Jung's avatar
Ralf Jung committed
99
    ⎡𝓟⎤ @{monPredI}  ⎡𝓠⎤.
100
101
102
103
104
105
  Proof.
    iIntros (HPQ) "HP".
    iMod (HPQ with "[-]") as "$"; last by auto.
    iAssumption.
  Qed.

Ralf Jung's avatar
Ralf Jung committed
106
  Context (FU : BiFUpd PROP).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
107

108
  Lemma test_apply_fupd_intro_mask_subseteq E1 E2 P :
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
109
    E2  E1  P - |={E1,E2}=> |={E2,E1}=> P.
110
  Proof. iIntros. by iApply @fupd_mask_intro_subseteq. Qed.
Ralf Jung's avatar
Ralf Jung committed
111
  Lemma test_apply_fupd_mask_subseteq E1 E2 P :
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
112
    E2  E1  P - |={E1,E2}=> |={E2,E1}=> P.
Ralf Jung's avatar
Ralf Jung committed
113
  Proof. iIntros. iFrame. by iApply @fupd_mask_subseteq. Qed.
114
115
116
117
118
119
120

  Lemma test_iFrame_embed_persistent (P : PROP) (Q: monPred) :
    Q   P  Q  P  P.
  Proof.
    iIntros "[$ #HP]". iFrame "HP".
  Qed.

121
  Lemma test_iNext_Bi P :
122
     P @{monPredI}  P.
123
124
125
  Proof. iIntros "H". by iNext. Qed.

  (** Test monPred_at framing *)
126
127
128
129
  Lemma test_iFrame_monPred_at_wand (P Q : monPred) i :
    P i - (Q - P) i.
  Proof. iIntros "$". Show. Abort.

130
131
132
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
165
  Program Definition monPred_id (R : monPred) : monPred :=
    MonPred (λ V, R V) _.
  Next Obligation. intros ? ???. eauto. Qed.

  Lemma test_iFrame_monPred_id (Q R : monPred) i :
    Q i  R i - (Q  monPred_id R) i.
  Proof.
    iIntros "(HQ & HR)". iFrame "HR". iAssumption.
  Qed.

  Lemma test_iFrame_rel P i j ij :
    IsBiIndexRel i ij  IsBiIndexRel j ij 
    P i - P j - P ij  P ij.
  Proof. iIntros (??) "HPi HPj". iFrame. Qed.

  Lemma test_iFrame_later_rel `{!BiAffine PROP} P i j :
    IsBiIndexRel i j 
     (P i) - ( P) j.
  Proof. iIntros (?) "?". iFrame. Qed.

  Lemma test_iFrame_laterN n P i :
    ^n (P i) - (^n P) i.
  Proof. iIntros "?". iFrame. Qed.

  Lemma test_iFrame_quantifiers P i :
    P i - ( _:(),  _:(), P) i.
  Proof. iIntros "?". iFrame. Show. iIntros ([]). iExists (). iEmpIntro. Qed.

  Lemma test_iFrame_embed (P : PROP) i :
    P - (embed (B:=monPredI) P) i.
  Proof. iIntros "$". Qed.

  (* Make sure search doesn't diverge on an evar *)
  Lemma test_iFrame_monPred_at_evar (P : monPred) i j :
    P i -  Q, (Q j).
  Proof. iIntros "HP". iExists _. Fail iFrame "HP". Abort.
166

167
End tests.
168
169
170
171
172

Section tests_iprop.
  Context {I : biIndex} `{!invG Σ}.

  Local Notation monPred := (monPred I (iPropI Σ)).
173
174
  Implicit Types P Q R : monPred.
  Implicit Types 𝓟 𝓠 𝓡 : iProp Σ.
175

176
177
  Lemma test_iInv_0 N 𝓟 :
    embed (B:=monPred) (inv N (<pers> 𝓟)) ={}= ⎡▷ 𝓟⎤.
178
179
180
181
182
183
  Proof.
    iIntros "#H".
    iInv N as "#H2". Show.
    iModIntro. iSplit=>//. iModIntro. iModIntro; auto.
  Qed.

184
185
  Lemma test_iInv_0_with_close N 𝓟 :
    embed (B:=monPred) (inv N (<pers> 𝓟)) ={}= ⎡▷ 𝓟⎤.
186
187
188
189
190
191
  Proof.
    iIntros "#H".
    iInv N as "#H2" "Hclose". Show.
    iMod ("Hclose" with "H2").
    iModIntro. iModIntro. by iNext.
  Qed.
192
193
194
195
196
197
198
199

  Lemma test_iPoseProof `{inG Σ A} P γ (x y : A) :
    x ~~> y  P  own γ x == own γ y.
  Proof.
    iIntros (?) "[_ Hγ]".
    iPoseProof (own_update with "Hγ") as "H"; first done.
    by iMod "H".
  Qed.
200
End tests_iprop.