monpred.v 23.4 KB
Newer Older
1
From iris.bi Require Export monpred.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
From iris.proofmode Require Import tactics class_instances.
3

4
Class MakeMonPredAt {I : biIndex} {PROP : bi} (i : I)
5
      (P : monPred I PROP) (𝓟 : PROP) :=
6 7 8
  make_monPred_at : P i  𝓟.
Arguments MakeMonPredAt {_ _} _ _%I _%I.
Hint Mode MakeMonPredAt + + - ! - : typeclass_instances.
9

10
Class IsBiIndexRel {I : biIndex} (i j : I) := is_bi_index_rel : i  j.
11
Hint Mode IsBiIndexRel + - - : typeclass_instances.
12
Instance is_bi_index_rel_refl {I : biIndex} (i : I) : IsBiIndexRel i i | 0.
13 14 15 16
Proof. by rewrite /IsBiIndexRel. Qed.
Hint Extern 1 (IsBiIndexRel _ _) => unfold IsBiIndexRel; assumption
            : typeclass_instances.

17
Section modalities.
18
  Context {I : biIndex} {PROP : bi}.
19

20 21 22
  Lemma modality_absolutely_mixin :
    modality_mixin (@monPred_absolutely I PROP)
      (MIEnvFilter Absolute) (MIEnvFilter Absolute).
23
  Proof.
24 25
    split; simpl; split_and?; intros;
      try match goal with H : TCDiag _ _ _ |- _ => destruct H end;
26 27 28
      eauto using bi.equiv_entails_sym, absolute_absolutely,
        monPred_absolutely_mono, monPred_absolutely_and,
        monPred_absolutely_sep_2 with typeclass_instances.
29
  Qed.
30 31 32
  Definition modality_absolutely :=
    Modality _ modality_absolutely_mixin.
End modalities.
33

34
Section bi.
35
Context {I : biIndex} {PROP : bi}.
36
Local Notation monPred := (monPred I PROP).
37
Local Notation MakeMonPredAt := (@MakeMonPredAt I PROP).
38
Implicit Types P Q R : monPred.
39
Implicit Types 𝓟 𝓠 𝓡 : PROP.
40 41 42
Implicit Types φ : Prop.
Implicit Types i j : I.

43
Global Instance from_modal_absolutely P :
44
  FromModal modality_absolutely ( P) ( P) P | 1.
45
Proof. by rewrite /FromModal. Qed.
46
Global Instance from_modal_relatively P :
47
  FromModal modality_id ( P) ( P) P | 1.
48
Proof. by rewrite /FromModal /= -monPred_relatively_intro. Qed.
49

50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73
Global Instance from_modal_affinely_monPred_at `(sel : A) P Q 𝓠 i :
  FromModal modality_affinely sel P Q  MakeMonPredAt i Q 𝓠 
  FromModal modality_affinely sel (P i) 𝓠 | 0.
Proof.
  rewrite /FromModal /MakeMonPredAt /==> <- <-. by rewrite monPred_at_affinely.
Qed.
Global Instance from_modal_persistently_monPred_at `(sel : A) P Q 𝓠 i :
  FromModal modality_persistently sel P Q  MakeMonPredAt i Q 𝓠 
  FromModal modality_persistently sel (P i) 𝓠 | 0.
Proof.
  rewrite /FromModal /MakeMonPredAt /==> <- <-. by rewrite monPred_at_persistently.
Qed.
Global Instance from_modal_affinely_persistently_monPred_at `(sel : A) P Q 𝓠 i :
  FromModal modality_affinely_persistently sel P Q  MakeMonPredAt i Q 𝓠 
  FromModal modality_affinely_persistently sel (P i) 𝓠 | 0.
Proof.
  rewrite /FromModal /MakeMonPredAt /==> <- <-.
  by rewrite monPred_at_affinely monPred_at_persistently.
Qed.
Global Instance from_modal_id_monPred_at `(sel : A) P Q 𝓠 i :
  FromModal modality_id sel P Q  MakeMonPredAt i Q 𝓠 
  FromModal modality_id sel (P i) 𝓠.
Proof. by rewrite /FromModal /MakeMonPredAt=> <- <-. Qed.

74
Global Instance make_monPred_at_pure φ i : MakeMonPredAt i ⌜φ⌝ ⌜φ⌝.
75
Proof. by rewrite /MakeMonPredAt monPred_at_pure. Qed.
76
Global Instance make_monPred_at_emp i : MakeMonPredAt i emp emp.
77
Proof. by rewrite /MakeMonPredAt monPred_at_emp. Qed.
78 79 80
Global Instance make_monPred_at_sep i P 𝓟 Q 𝓠 :
  MakeMonPredAt i P 𝓟  MakeMonPredAt i Q 𝓠 
  MakeMonPredAt i (P  Q) (𝓟  𝓠).
81
Proof. by rewrite /MakeMonPredAt monPred_at_sep=><-<-. Qed.
82 83 84
Global Instance make_monPred_at_and i P 𝓟 Q 𝓠 :
  MakeMonPredAt i P 𝓟  MakeMonPredAt i Q 𝓠 
  MakeMonPredAt i (P  Q) (𝓟  𝓠).
85
Proof. by rewrite /MakeMonPredAt monPred_at_and=><-<-. Qed.
86 87 88
Global Instance make_monPred_at_or i P 𝓟 Q 𝓠 :
  MakeMonPredAt i P 𝓟  MakeMonPredAt i Q 𝓠 
  MakeMonPredAt i (P  Q) (𝓟  𝓠).
89
Proof. by rewrite /MakeMonPredAt monPred_at_or=><-<-. Qed.
90 91
Global Instance make_monPred_at_forall {A} i (Φ : A  monPred) (Ψ : A  PROP) :
  ( a, MakeMonPredAt i (Φ a) (Ψ a))  MakeMonPredAt i ( a, Φ a) ( a, Ψ a).
92
Proof. rewrite /MakeMonPredAt monPred_at_forall=>H. by setoid_rewrite <- H. Qed.
93 94
Global Instance make_monPred_at_exists {A} i (Φ : A  monPred) (Ψ : A  PROP) :
  ( a, MakeMonPredAt i (Φ a) (Ψ a))  MakeMonPredAt i ( a, Φ a) ( a, Ψ a).
95
Proof. rewrite /MakeMonPredAt monPred_at_exist=>H. by setoid_rewrite <- H. Qed.
96 97
Global Instance make_monPred_at_persistently i P 𝓟 :
  MakeMonPredAt i P 𝓟  MakeMonPredAt i (bi_persistently P) (bi_persistently 𝓟).
98
Proof. by rewrite /MakeMonPredAt monPred_at_persistently=><-. Qed.
99 100
Global Instance make_monPred_at_affinely i P 𝓟 :
  MakeMonPredAt i P 𝓟  MakeMonPredAt i (bi_affinely P) (bi_affinely 𝓟).
101
Proof. by rewrite /MakeMonPredAt monPred_at_affinely=><-. Qed.
102 103
Global Instance make_monPred_at_absorbingly i P 𝓟 :
  MakeMonPredAt i P 𝓟  MakeMonPredAt i (bi_absorbingly P) (bi_absorbingly 𝓟).
104
Proof. by rewrite /MakeMonPredAt monPred_at_absorbingly=><-. Qed.
105 106 107
Global Instance make_monPred_at_persistently_if i P 𝓟 p :
  MakeMonPredAt i P 𝓟 
  MakeMonPredAt i (bi_persistently_if p P) (bi_persistently_if p 𝓟).
108
Proof. destruct p; simpl; apply _. Qed.
109 110 111
Global Instance make_monPred_at_affinely_if i P 𝓟 p :
  MakeMonPredAt i P 𝓟 
  MakeMonPredAt i (bi_affinely_if p P) (bi_affinely_if p 𝓟).
112
Proof. destruct p; simpl; apply _. Qed.
113 114
Global Instance make_monPred_at_embed i 𝓟 : MakeMonPredAt i ⎡𝓟⎤ 𝓟.
Proof. by rewrite /MakeMonPredAt monPred_at_embed. Qed.
115
Global Instance make_monPred_at_in i j : MakeMonPredAt j (monPred_in i) i  j.
116
Proof. by rewrite /MakeMonPredAt monPred_at_in. Qed.
117 118
Global Instance make_monPred_at_default i P : MakeMonPredAt i P (P i) | 100.
Proof. by rewrite /MakeMonPredAt. Qed.
119

120 121
Global Instance from_assumption_make_monPred_at_l p i j P 𝓟 :
  MakeMonPredAt i P 𝓟  IsBiIndexRel j i  FromAssumption p (P j) 𝓟.
122
Proof.
123
  rewrite /MakeMonPredAt /FromAssumption /IsBiIndexRel=><- ->.
124 125
  apply  bi.affinely_persistently_if_elim.
Qed.
126 127
Global Instance from_assumption_make_monPred_at_r p i j P 𝓟 :
  MakeMonPredAt i P 𝓟  IsBiIndexRel i j  FromAssumption p 𝓟 (P j).
128
Proof.
129
  rewrite /MakeMonPredAt /FromAssumption /IsBiIndexRel=><- ->.
130 131 132
  apply  bi.affinely_persistently_if_elim.
Qed.

133 134 135 136 137 138
Global Instance from_assumption_make_monPred_absolutely P Q :
  FromAssumption p P Q  FromAssumption p ( P) Q.
Proof. intros ?. by rewrite /FromAssumption monPred_absolutely_elim. Qed.
Global Instance from_assumption_make_monPred_relatively P Q :
  FromAssumption p P Q  FromAssumption p P ( Q).
Proof. intros ?. by rewrite /FromAssumption -monPred_relatively_intro. Qed.
139

140
Global Instance as_valid_monPred_at φ P (Φ : I  PROP) :
141
  AsValid0 φ P  ( i, MakeMonPredAt i P (Φ i))  AsValid φ ( i, Φ i) | 100.
142
Proof.
143
  rewrite /MakeMonPredAt /AsValid0 /AsValid /bi_valid=> -> EQ.
144 145 146
  setoid_rewrite <-EQ. split.
  - move=>[H]. apply bi.forall_intro=>i. rewrite -H. by rewrite monPred_at_emp.
  - move=>HP. split=>i. rewrite monPred_at_emp HP bi.forall_elim //.
147
Qed.
148
Global Instance as_valid_monPred_at_wand φ P Q (Φ Ψ : I  PROP) :
149
  AsValid0 φ (P - Q) 
150
  ( i, MakeMonPredAt i P (Φ i))  ( i, MakeMonPredAt i Q (Ψ i)) 
151
  AsValid φ ( i, Φ i - Ψ i).
152
Proof.
153
  rewrite /AsValid0 /AsValid /MakeMonPredAt. intros -> EQ1 EQ2.
154
  setoid_rewrite <-EQ1. setoid_rewrite <-EQ2. split.
155 156
  - move=>/bi.wand_entails HP. setoid_rewrite HP. by iIntros (i) "$".
  - move=>HP. apply bi.entails_wand. split=>i. iIntros "H". by iApply HP.
157
Qed.
158
Global Instance as_valid_monPred_at_equiv φ P Q (Φ Ψ : I  PROP) :
159
  AsValid0 φ (P - Q) 
160
  ( i, MakeMonPredAt i P (Φ i))  ( i, MakeMonPredAt i Q (Ψ i)) 
161
  AsValid φ ( i, Φ i - Ψ i).
162
Proof.
163
  rewrite /AsValid0 /AsValid /MakeMonPredAt. intros -> EQ1 EQ2.
164
  setoid_rewrite <-EQ1. setoid_rewrite <-EQ2. split.
165 166
  - move=>/bi.wand_iff_equiv HP. setoid_rewrite HP. iIntros. iSplit; iIntros "$".
  - move=>HP. apply bi.equiv_wand_iff. split=>i. by iSplit; iIntros; iApply HP.
167
Qed.
168

169 170
Global Instance into_pure_monPred_at P φ i : IntoPure P φ  IntoPure (P i) φ.
Proof. rewrite /IntoPure=>->. by rewrite monPred_at_pure. Qed.
171 172
Global Instance from_pure_monPred_at a P φ i : FromPure a P φ  FromPure a (P i) φ.
Proof. rewrite /FromPure=><-. by rewrite monPred_at_affinely_if monPred_at_pure. Qed.
173 174
Global Instance into_pure_monPred_in i j : @IntoPure PROP (monPred_in i j) (i  j).
Proof. by rewrite /IntoPure monPred_at_in. Qed.
175 176
Global Instance from_pure_monPred_in i j af : @FromPure PROP af (monPred_in i j) (i  j).
Proof. by rewrite /FromPure monPred_at_in bi.affinely_if_elim. Qed.
177

178 179
Global Instance into_persistent_monPred_at p P Q 𝓠 i :
  IntoPersistent p P Q  MakeMonPredAt i Q 𝓠  IntoPersistent p (P i) 𝓠 | 0.
180
Proof.
181 182
  rewrite /IntoPersistent /MakeMonPredAt  =>-[/(_ i) ?] <-.
  by rewrite -monPred_at_persistently -monPred_at_persistently_if.
183
Qed.
184

185 186
Lemma into_wand_monPred_at_unknown_unknown p q R P 𝓟 Q 𝓠 i :
  IntoWand p q R P Q   MakeMonPredAt i P 𝓟  MakeMonPredAt i Q 𝓠 
187
  IntoWand p q (R i) 𝓟 𝓠.
188
Proof.
189
  rewrite /IntoWand /MakeMonPredAt /bi_affinely_if /bi_persistently_if.
190
  destruct p, q=> /bi.wand_elim_l' [/(_ i) H] <- <-; apply bi.wand_intro_r;
191
  revert H; by rewrite monPred_at_sep ?monPred_at_affinely ?monPred_at_persistently.
192
Qed.
193
Lemma into_wand_monPred_at_unknown_known p q R P 𝓟 Q i j :
194
  IsBiIndexRel i j  IntoWand p q R P Q 
195
  MakeMonPredAt j P 𝓟  IntoWand p q (R i) 𝓟 (Q j).
196
Proof.
197 198
  rewrite /IntoWand /IsBiIndexRel /MakeMonPredAt=>-> ? ?.
  eapply into_wand_monPred_at_unknown_unknown=>//. apply _.
199
Qed.
200
Lemma into_wand_monPred_at_known_unknown_le p q R P Q 𝓠 i j :
201
  IsBiIndexRel i j  IntoWand p q R P Q 
202
  MakeMonPredAt j Q 𝓠  IntoWand p q (R i) (P j) 𝓠.
203
Proof.
204 205
  rewrite /IntoWand /IsBiIndexRel /MakeMonPredAt=>-> ? ?.
  eapply into_wand_monPred_at_unknown_unknown=>//. apply _.
206
Qed.
207
Lemma into_wand_monPred_at_known_unknown_ge p q R P Q 𝓠 i j :
208
  IsBiIndexRel i j  IntoWand p q R P Q 
209
  MakeMonPredAt j Q 𝓠  IntoWand p q (R j) (P i) 𝓠.
210
Proof.
211 212
  rewrite /IntoWand /IsBiIndexRel /MakeMonPredAt=>-> ? ?.
  eapply into_wand_monPred_at_unknown_unknown=>//. apply _.
213
Qed.
214

215 216 217 218 219 220 221
Global Instance into_wand_wand'_monPred p q P Q 𝓟 𝓠 i :
  IntoWand' p q ((P - Q) i) 𝓟 𝓠  IntoWand p q ((P - Q) i) 𝓟 𝓠 | 100.
Proof. done. Qed.
Global Instance into_wand_impl'_monPred p q P Q 𝓟 𝓠 i :
  IntoWand' p q ((P  Q) i) 𝓟 𝓠  IntoWand p q ((P  Q) i) 𝓟 𝓠 | 100.
Proof. done. Qed.

222 223
Global Instance from_forall_monPred_at_wand P Q (Φ Ψ : I  PROP) i :
  ( j, MakeMonPredAt j P (Φ j))  ( j, MakeMonPredAt j Q (Ψ j)) 
224 225
  FromForall ((P - Q) i)%I (λ j, i  j  Φ j - Ψ j)%I.
Proof.
226
  rewrite /FromForall /MakeMonPredAt monPred_at_wand=> H1 H2. do 2 f_equiv.
227
  by rewrite H1 H2.
228
Qed.
229 230
Global Instance from_forall_monPred_at_impl P Q (Φ Ψ : I  PROP) i :
  ( j, MakeMonPredAt j P (Φ j))  ( j, MakeMonPredAt j Q (Ψ j)) 
231 232
  FromForall ((P  Q) i)%I (λ j, i  j  Φ j  Ψ j)%I.
Proof.
233
  rewrite /FromForall /MakeMonPredAt monPred_at_impl=> H1 H2. do 2 f_equiv.
234
  by rewrite H1 H2 bi.pure_impl_forall.
235 236
Qed.

237
Global Instance into_forall_monPred_at_index P i :
238 239 240 241 242
  IntoForall (P i) (λ j, i  j  P j)%I | 100.
Proof.
  rewrite /IntoForall. setoid_rewrite bi.pure_impl_forall.
  do 2 apply bi.forall_intro=>?. by f_equiv.
Qed.
243

244 245
Global Instance from_and_monPred_at P Q1 𝓠1 Q2 𝓠2 i :
  FromAnd P Q1 Q2  MakeMonPredAt i Q1 𝓠1  MakeMonPredAt i Q2 𝓠2 
246
  FromAnd (P i) 𝓠1 𝓠2.
247 248 249 250
Proof.
  rewrite /FromAnd /MakeMonPredAt /MakeMonPredAt=> <- <- <-.
  by rewrite monPred_at_and.
Qed.
251 252
Global Instance into_and_monPred_at p P Q1 𝓠1 Q2 𝓠2 i :
  IntoAnd p P Q1 Q2  MakeMonPredAt i Q1 𝓠1  MakeMonPredAt i Q2 𝓠2 
253
  IntoAnd p (P i) 𝓠1 𝓠2.
254
Proof.
255
  rewrite /IntoAnd /MakeMonPredAt /bi_affinely_if /bi_persistently_if.
256 257
  destruct p=>-[/(_ i) H] <- <-; revert H;
  by rewrite ?monPred_at_affinely ?monPred_at_persistently monPred_at_and.
258 259
Qed.

260 261
Global Instance from_sep_monPred_at P Q1 𝓠1 Q2 𝓠2 i :
  FromSep P Q1 Q2  MakeMonPredAt i Q1 𝓠1  MakeMonPredAt i Q2 𝓠2 
262
  FromSep (P i) 𝓠1 𝓠2.
263
Proof. rewrite /FromSep /MakeMonPredAt=> <- <- <-. by rewrite monPred_at_sep. Qed.
264 265
Global Instance into_sep_monPred_at P Q1 𝓠1 Q2 𝓠2 i :
  IntoSep P Q1 Q2  MakeMonPredAt i Q1 𝓠1  MakeMonPredAt i Q2 𝓠2 
266
  IntoSep (P i) 𝓠1 𝓠2.
267
Proof. rewrite /IntoSep /MakeMonPredAt=> -> <- <-. by rewrite monPred_at_sep. Qed.
268 269
Global Instance from_or_monPred_at P Q1 𝓠1 Q2 𝓠2 i :
  FromOr P Q1 Q2  MakeMonPredAt i Q1 𝓠1  MakeMonPredAt i Q2 𝓠2 
270
  FromOr (P i) 𝓠1 𝓠2.
271
Proof. rewrite /FromOr /MakeMonPredAt=> <- <- <-. by rewrite monPred_at_or. Qed.
272 273
Global Instance into_or_monPred_at P Q1 𝓠1 Q2 𝓠2 i :
  IntoOr P Q1 Q2  MakeMonPredAt i Q1 𝓠1  MakeMonPredAt i Q2 𝓠2 
274
  IntoOr (P i) 𝓠1 𝓠2.
275
Proof. rewrite /IntoOr /MakeMonPredAt=> -> <- <-. by rewrite monPred_at_or. Qed.
276

277 278
Global Instance from_exist_monPred_at {A} P (Φ : A  monPred) (Ψ : A  PROP) i :
  FromExist P Φ  ( a, MakeMonPredAt i (Φ a) (Ψ a))  FromExist (P i) Ψ.
279
Proof.
280 281
  rewrite /FromExist /MakeMonPredAt=><- H. setoid_rewrite <- H.
  by rewrite monPred_at_exist.
282
Qed.
283 284
Global Instance into_exist_monPred_at {A} P (Φ : A  monPred) (Ψ : A  PROP) i :
  IntoExist P Φ  ( a, MakeMonPredAt i (Φ a) (Ψ a))  IntoExist (P i) Ψ.
285
Proof.
286 287
  rewrite /IntoExist /MakeMonPredAt=>-> H. setoid_rewrite <- H.
  by rewrite monPred_at_exist.
288 289
Qed.

290 291
Global Instance foram_forall_monPred_at_plainly i P Φ :
  ( i, MakeMonPredAt i P (Φ i)) 
292
  FromForall (bi_plainly P i) (λ j, bi_plainly (Φ j)).
293 294 295 296
Proof.
  rewrite /FromForall /MakeMonPredAt=>H. rewrite monPred_at_plainly.
  by setoid_rewrite H.
Qed.
297 298
Global Instance into_forall_monPred_at_plainly i P Φ :
  ( i, MakeMonPredAt i P (Φ i)) 
299
  IntoForall (bi_plainly P i) (λ j, bi_plainly (Φ j)).
300 301 302 303
Proof.
  rewrite /IntoForall /MakeMonPredAt=>H. rewrite monPred_at_plainly.
  by setoid_rewrite H.
Qed.
304

305 306
Global Instance from_forall_monPred_at_absolutely P (Φ : I  PROP) i :
  ( i, MakeMonPredAt i P (Φ i))  FromForall (( P) i)%I Φ.
307
Proof.
308
  rewrite /FromForall /MakeMonPredAt monPred_at_absolutely=>H. by setoid_rewrite <- H.
309
Qed.
310 311
Global Instance into_forall_monPred_at_absolutely P (Φ : I  PROP) i :
  ( i, MakeMonPredAt i P (Φ i))  IntoForall (( P) i) Φ.
312
Proof.
313
  rewrite /IntoForall /MakeMonPredAt monPred_at_absolutely=>H. by setoid_rewrite <- H.
314
Qed.
315

316
Global Instance from_exist_monPred_at_ex P (Φ : I  PROP) i :
317
  ( i, MakeMonPredAt i P (Φ i))  FromExist (( P) i) Φ.
318
Proof.
319
  rewrite /FromExist /MakeMonPredAt monPred_at_ex=>H. by setoid_rewrite <- H.
320 321
Qed.
Global Instance into_exist_monPred_at_ex P (Φ : I  PROP) i :
322
  ( i, MakeMonPredAt i P (Φ i))  IntoExist (( P) i) Φ.
323
Proof.
324
  rewrite /IntoExist /MakeMonPredAt monPred_at_ex=>H. by setoid_rewrite <- H.
325 326
Qed.

327 328
Global Instance from_forall_monPred_at {A} P (Φ : A  monPred) (Ψ : A  PROP) i :
  FromForall P Φ  ( a, MakeMonPredAt i (Φ a) (Ψ a))  FromForall (P i) Ψ.
329
Proof.
330 331
  rewrite /FromForall /MakeMonPredAt=><- H. setoid_rewrite <- H.
  by rewrite monPred_at_forall.
332
Qed.
333 334
Global Instance into_forall_monPred_at {A} P (Φ : A  monPred) (Ψ : A  PROP) i :
  IntoForall P Φ  ( a, MakeMonPredAt i (Φ a) (Ψ a))  IntoForall (P i) Ψ.
335
Proof.
336 337
  rewrite /IntoForall /MakeMonPredAt=>-> H. setoid_rewrite <- H.
  by rewrite monPred_at_forall.
338 339
Qed.

340
(* FIXME : there are two good ways to frame under a call to
341
   monPred_at. This may cause some backtracking in the typeclass
342
   search, and hence performance issues. *)
343 344
Global Instance frame_monPred_at p P Q 𝓠 R i j :
  IsBiIndexRel i j  Frame p R P Q  MakeMonPredAt j Q 𝓠 
345
  KnownFrame p (R i) (P j) 𝓠.
346
Proof.
347
  rewrite /KnownFrame /Frame /MakeMonPredAt /bi_affinely_if /bi_persistently_if
348
          /IsBiIndexRel=> Hij <- <-.
349
  destruct p; by rewrite Hij monPred_at_sep ?monPred_at_affinely ?monPred_at_persistently.
350
Qed.
351
Global Instance frame_monPred_at_embed i p P Q 𝓠 𝓡 :
352
  Frame p ⎡𝓡⎤ P Q  MakeMonPredAt i Q 𝓠  KnownFrame p 𝓡 (P i) 𝓠.
353
Proof.
354
  rewrite /KnownFrame /Frame /MakeMonPredAt /bi_affinely_if /bi_persistently_if=> <- <-.
355 356
  destruct p; by rewrite monPred_at_sep ?monPred_at_affinely
                         ?monPred_at_persistently monPred_at_embed.
357 358
Qed.

359 360 361
Global Instance into_embed_absolute P :
  Absolute P  IntoEmbed P ( i, P i).
Proof. rewrite /IntoEmbed=> ?. by rewrite {1}(absolute_absolutely P). Qed.
362 363
End bi.

364
(* When P and/or Q are evars when doing typeclass search on [IntoWand
365
   (R i) P Q], we use [MakeMonPredAt] in order to normalize the
366 367
   result of unification. However, when they are not evars, we want to
   propagate the known information through typeclass search. Hence, we
368
   do not want to use [MakeMonPredAt].
369 370

   As a result, depending on P and Q being evars, we use a different
371 372
   version of [into_wand_monPred_at_xx_xx]. *)
Hint Extern 3 (IntoWand _ _ (monPred_at _ _) ?P ?Q) =>
373
     is_evar P; is_evar Q;
374
     eapply @into_wand_monPred_at_unknown_unknown
375
     : typeclass_instances.
376 377
Hint Extern 2 (IntoWand _ _ (monPred_at _ _) ?P (monPred_at ?Q _)) =>
     eapply @into_wand_monPred_at_unknown_known
378
     : typeclass_instances.
379 380
Hint Extern 2 (IntoWand _ _ (monPred_at _ _) (monPred_at ?P _) ?Q) =>
     eapply @into_wand_monPred_at_known_unknown_le
381
     : typeclass_instances.
382 383
Hint Extern 2 (IntoWand _ _ (monPred_at _ _) (monPred_at ?P _) ?Q) =>
     eapply @into_wand_monPred_at_known_unknown_ge
384
     : typeclass_instances.
385

386
Section sbi.
387
Context {I : biIndex} {PROP : sbi}.
388 389
Local Notation monPred := (monPred I PROP).
Implicit Types P Q R : monPred.
390
Implicit Types 𝓟 𝓠 𝓡 : PROP.
391 392 393
Implicit Types φ : Prop.
Implicit Types i j : I.

394
Global Instance is_except_0_monPred_at i P :
395
  IsExcept0 P  IsExcept0 (P i).
396
Proof. rewrite /IsExcept0=>- [/(_ i)]. by rewrite monPred_at_except_0. Qed.
397

398 399 400
Global Instance make_monPred_at_internal_eq {A : ofeT} (x y : A) i :
  @MakeMonPredAt I PROP i (x  y) (x  y).
Proof. by rewrite /MakeMonPredAt monPred_at_internal_eq. Qed.
401 402
Global Instance make_monPred_at_except_0 i P 𝓠 :
  MakeMonPredAt i P 𝓠  MakeMonPredAt i ( P)%I ( 𝓠)%I.
403
Proof. by rewrite /MakeMonPredAt monPred_at_except_0=><-. Qed.
404 405
Global Instance make_monPred_at_later i P 𝓠 :
  MakeMonPredAt i P 𝓠  MakeMonPredAt i ( P)%I ( 𝓠)%I.
406
Proof. by rewrite /MakeMonPredAt monPred_at_later=><-. Qed.
407 408
Global Instance make_monPred_at_laterN i n P 𝓠 :
  MakeMonPredAt i P 𝓠  MakeMonPredAt i (^n P)%I (^n 𝓠)%I.
409
Proof. rewrite /MakeMonPredAt=> <-. elim n=>//= ? <-. by rewrite monPred_at_later. Qed.
Ralf Jung's avatar
Ralf Jung committed
410 411 412
Global Instance make_monPred_at_bupd `{BUpdFacts PROP} i P 𝓟 :
  MakeMonPredAt i P 𝓟  MakeMonPredAt i (|==> P)%I (|==> 𝓟)%I.
Proof. by rewrite /MakeMonPredAt monPred_at_bupd=> <-. Qed.
413 414
Global Instance make_monPred_at_fupd `{FUpdFacts PROP} i E1 E2 P 𝓟 :
  MakeMonPredAt i P 𝓟  MakeMonPredAt i (|={E1,E2}=> P)%I (|={E1,E2}=> 𝓟)%I.
415
Proof. by rewrite /MakeMonPredAt monPred_at_fupd=> <-. Qed.
416

417 418 419 420
Global Instance into_internal_eq_monPred_at {A : ofeT} (x y : A) P i :
  IntoInternalEq P x y  IntoInternalEq (P i) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite monPred_at_internal_eq. Qed.

421 422
Global Instance into_except_0_monPred_at_fwd i P Q 𝓠 :
  IntoExcept0 P Q  MakeMonPredAt i Q 𝓠  IntoExcept0 (P i) 𝓠.
423
Proof. rewrite /IntoExcept0 /MakeMonPredAt=> -> <-. by rewrite monPred_at_except_0. Qed.
424 425
Global Instance into_except_0_monPred_at_bwd i P 𝓟 Q :
  IntoExcept0 P Q  MakeMonPredAt i P 𝓟  IntoExcept0 𝓟 (Q i).
426
Proof. rewrite /IntoExcept0 /MakeMonPredAt=> H <-. by rewrite H monPred_at_except_0. Qed.
427

428
Global Instance maybe_into_later_monPred_at i n P Q 𝓠 :
429 430
  IntoLaterN false n P Q  MakeMonPredAt i Q 𝓠 
  IntoLaterN false n (P i) 𝓠.
431
Proof.
432
  rewrite /IntoLaterN /MaybeIntoLaterN /MakeMonPredAt=> -> <-. elim n=>//= ? <-.
433
   by rewrite monPred_at_later.
434
Qed.
435 436
Global Instance from_later_monPred_at i n P Q 𝓠 :
  FromLaterN n P Q  MakeMonPredAt i Q 𝓠  FromLaterN n (P i) 𝓠.
437 438 439 440
Proof.
  rewrite /FromLaterN /MakeMonPredAt=> <- <-. elim n=>//= ? ->.
  by rewrite monPred_at_later.
Qed.
441

Ralf Jung's avatar
Ralf Jung committed
442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467
Global Instance elim_modal_embed_bupd_goal `{BUpdFacts PROP} φ P P' 𝓠 𝓠' :
  ElimModal φ P P' (|==> ⎡𝓠⎤)%I (|==> ⎡𝓠')%I 
  ElimModal φ P P' |==> 𝓠⎤ |==> 𝓠'.
Proof. by rewrite /ElimModal !monPred_bupd_embed. Qed.
Global Instance elim_modal_embed_bupd_hyp `{BUpdFacts PROP} φ 𝓟 P' Q Q' :
  ElimModal φ (|==> ⎡𝓟⎤)%I P' Q Q' 
  ElimModal φ |==> 𝓟⎤ P' Q Q'.
Proof. by rewrite /ElimModal monPred_bupd_embed. Qed.

Global Instance add_modal_embed_bupd_goal `{BUpdFacts PROP} P P' 𝓠 :
  AddModal P P' (|==> ⎡𝓠⎤)%I  AddModal P P' |==> 𝓠⎤.
Proof. by rewrite /AddModal !monPred_bupd_embed. Qed.

Global Instance elim_modal_at_bupd_goal `{BUpdFacts PROP} φ 𝓟 𝓟' Q Q' i :
  ElimModal φ 𝓟 𝓟' (|==> Q i) (|==> Q' i) 
  ElimModal φ 𝓟 𝓟' ((|==> Q) i) ((|==> Q') i).
Proof. by rewrite /ElimModal !monPred_at_bupd. Qed.
Global Instance elim_modal_at_bupd_hyp `{BUpdFacts PROP} φ P 𝓟' 𝓠 𝓠' i:
  ElimModal φ (|==> P i) 𝓟' 𝓠 𝓠' 
  ElimModal φ ((|==> P) i) 𝓟' 𝓠 𝓠'.
Proof. by rewrite /ElimModal monPred_at_bupd. Qed.

Global Instance add_modal_at_bupd_goal `{BUpdFacts PROP} φ 𝓟 𝓟' Q i :
  AddModal 𝓟 𝓟' (|==> Q i)%I  AddModal 𝓟 𝓟' ((|==> Q) i).
Proof. by rewrite /AddModal !monPred_at_bupd. Qed.

468 469 470
Global Instance elim_modal_embed_fupd_goal `{FUpdFacts PROP} φ E1 E2 E3 P P' 𝓠 𝓠' :
  ElimModal φ P P' (|={E1,E3}=> ⎡𝓠⎤)%I (|={E2,E3}=> ⎡𝓠')%I 
  ElimModal φ P P' |={E1,E3}=> 𝓠⎤ |={E2,E3}=> 𝓠'.
471
Proof. by rewrite /ElimModal !monPred_fupd_embed. Qed.
472 473 474
Global Instance elim_modal_embed_fupd_hyp `{FUpdFacts PROP} φ E1 E2 𝓟 P' Q Q' :
  ElimModal φ (|={E1,E2}=> ⎡𝓟⎤)%I P' Q Q' 
  ElimModal φ |={E1,E2}=> 𝓟⎤ P' Q Q'.
475 476 477 478 479 480
Proof. by rewrite /ElimModal monPred_fupd_embed. Qed.

Global Instance add_modal_embed_fupd_goal `{FUpdFacts PROP} E1 E2 P P' 𝓠 :
  AddModal P P' (|={E1,E2}=> ⎡𝓠⎤)%I  AddModal P P' |={E1,E2}=> 𝓠⎤.
Proof. by rewrite /AddModal !monPred_fupd_embed. Qed.

481 482 483
Global Instance elim_modal_at_fupd_goal `{FUpdFacts PROP} φ E1 E2 E3 𝓟 𝓟' Q Q' i :
  ElimModal φ 𝓟 𝓟' (|={E1,E3}=> Q i) (|={E2,E3}=> Q' i) 
  ElimModal φ 𝓟 𝓟' ((|={E1,E3}=> Q) i) ((|={E2,E3}=> Q') i).
484
Proof. by rewrite /ElimModal !monPred_at_fupd. Qed.
485 486 487
Global Instance elim_modal_at_fupd_hyp `{FUpdFacts PROP} φ E1 E2 P 𝓟' 𝓠 𝓠' i :
  ElimModal φ (|={E1,E2}=> P i) 𝓟' 𝓠 𝓠' 
  ElimModal φ ((|={E1,E2}=> P) i) 𝓟' 𝓠 𝓠'.
488
Proof. by rewrite /ElimModal monPred_at_fupd. Qed.
489 490 491

Global Instance add_modal_at_fupd_goal `{FUpdFacts PROP} E1 E2 𝓟 𝓟' Q i :
  AddModal 𝓟 𝓟' (|={E1,E2}=> Q i)  AddModal 𝓟 𝓟' ((|={E1,E2}=> Q) i).
492
Proof. by rewrite /AddModal !monPred_at_fupd. Qed.
493 494 495 496 497 498 499 500 501

Global Instance elim_inv_embed φ 𝓟inv 𝓟in 𝓟out 𝓟close Pin Pout Pclose Q Q' :
  ( i, ElimInv φ 𝓟inv 𝓟in 𝓟out 𝓟close (Q i) (Q' i)) 
  MakeEmbed 𝓟in Pin  MakeEmbed 𝓟out Pout  MakeEmbed 𝓟close Pclose 
  ElimInv φ ⎡𝓟inv Pin Pout Pclose Q Q'.
Proof.
  rewrite /MakeEmbed /ElimInv=>H <- <- <- ?. iStartProof PROP.
  iIntros (?) "(?&?&HQ')". iApply H; [done|]. iFrame. iIntros "?". by iApply "HQ'".
Qed.
502
End sbi.