monpred.v 23.1 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 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43
Section always_modalities.
Context {I : biIndex} {PROP : bi}.

  Lemma always_modality_absolutely_mixin :
    always_modality_mixin (@monPred_absolutely I PROP)
      (AIEnvFilter Absolute) (AIEnvForall Absolute).
  Proof.
    split; eauto using bi.equiv_entails_sym, absolute_absolutely,
       monPred_absolutely_mono, monPred_absolutely_and,
       monPred_absolutely_sep_2 with typeclass_instances.
  Qed.
  Definition always_modality_absolutely :=
    AlwaysModality _ always_modality_absolutely_mixin.

  (* We can only filter the spatial context in case the BI is affine *)
  Lemma always_modality_absolutely_filter_spatial_mixin `{BiAffine PROP} :
    always_modality_mixin (@monPred_absolutely I PROP)
      (AIEnvFilter Absolute) (AIEnvFilter Absolute).
  Proof.
    split; eauto using bi.equiv_entails_sym, absolute_absolutely,
       monPred_absolutely_mono, monPred_absolutely_and,
       monPred_absolutely_sep_2 with typeclass_instances.
  Qed.
  Definition always_modality_absolutely_filter_spatial `{BiAffine PROP} :=
    AlwaysModality _ always_modality_absolutely_filter_spatial_mixin.
End always_modalities.

44
Section bi.
45
Context {I : biIndex} {PROP : bi}.
46
Local Notation monPred := (monPred I PROP).
47
Local Notation MakeMonPredAt := (@MakeMonPredAt I PROP).
48
Implicit Types P Q R : monPred.
49
Implicit Types 𝓟 𝓠 𝓡 : PROP.
50 51 52
Implicit Types φ : Prop.
Implicit Types i j : I.

53 54 55 56 57 58 59
Global Instance from_always_absolutely P :
  FromAlways always_modality_absolutely ( P) P | 1.
Proof. by rewrite /FromAlways. Qed.
Global Instance from_always_absolutely_filter_spatial `{BiAffine PROP} P :
  FromAlways always_modality_absolutely_filter_spatial ( P) P | 0.
Proof. by rewrite /FromAlways. Qed.

60
Global Instance make_monPred_at_pure φ i : MakeMonPredAt i ⌜φ⌝ ⌜φ⌝.
61
Proof. by rewrite /MakeMonPredAt monPred_at_pure. Qed.
62
Global Instance make_monPred_at_emp i : MakeMonPredAt i emp emp.
63
Proof. by rewrite /MakeMonPredAt monPred_at_emp. Qed.
64 65 66
Global Instance make_monPred_at_sep i P 𝓟 Q 𝓠 :
  MakeMonPredAt i P 𝓟  MakeMonPredAt i Q 𝓠 
  MakeMonPredAt i (P  Q) (𝓟  𝓠).
67
Proof. by rewrite /MakeMonPredAt monPred_at_sep=><-<-. Qed.
68 69 70
Global Instance make_monPred_at_and i P 𝓟 Q 𝓠 :
  MakeMonPredAt i P 𝓟  MakeMonPredAt i Q 𝓠 
  MakeMonPredAt i (P  Q) (𝓟  𝓠).
71
Proof. by rewrite /MakeMonPredAt monPred_at_and=><-<-. Qed.
72 73 74
Global Instance make_monPred_at_or i P 𝓟 Q 𝓠 :
  MakeMonPredAt i P 𝓟  MakeMonPredAt i Q 𝓠 
  MakeMonPredAt i (P  Q) (𝓟  𝓠).
75
Proof. by rewrite /MakeMonPredAt monPred_at_or=><-<-. Qed.
76 77
Global Instance make_monPred_at_forall {A} i (Φ : A  monPred) (Ψ : A  PROP) :
  ( a, MakeMonPredAt i (Φ a) (Ψ a))  MakeMonPredAt i ( a, Φ a) ( a, Ψ a).
78
Proof. rewrite /MakeMonPredAt monPred_at_forall=>H. by setoid_rewrite <- H. Qed.
79 80
Global Instance make_monPred_at_exists {A} i (Φ : A  monPred) (Ψ : A  PROP) :
  ( a, MakeMonPredAt i (Φ a) (Ψ a))  MakeMonPredAt i ( a, Φ a) ( a, Ψ a).
81
Proof. rewrite /MakeMonPredAt monPred_at_exist=>H. by setoid_rewrite <- H. Qed.
82 83
Global Instance make_monPred_at_persistently i P 𝓟 :
  MakeMonPredAt i P 𝓟  MakeMonPredAt i (bi_persistently P) (bi_persistently 𝓟).
84
Proof. by rewrite /MakeMonPredAt monPred_at_persistently=><-. Qed.
85 86
Global Instance make_monPred_at_affinely i P 𝓟 :
  MakeMonPredAt i P 𝓟  MakeMonPredAt i (bi_affinely P) (bi_affinely 𝓟).
87
Proof. by rewrite /MakeMonPredAt monPred_at_affinely=><-. Qed.
88 89
Global Instance make_monPred_at_absorbingly i P 𝓟 :
  MakeMonPredAt i P 𝓟  MakeMonPredAt i (bi_absorbingly P) (bi_absorbingly 𝓟).
90
Proof. by rewrite /MakeMonPredAt monPred_at_absorbingly=><-. Qed.
91 92 93
Global Instance make_monPred_at_persistently_if i P 𝓟 p :
  MakeMonPredAt i P 𝓟 
  MakeMonPredAt i (bi_persistently_if p P) (bi_persistently_if p 𝓟).
94
Proof. destruct p; simpl; apply _. Qed.
95 96 97
Global Instance make_monPred_at_affinely_if i P 𝓟 p :
  MakeMonPredAt i P 𝓟 
  MakeMonPredAt i (bi_affinely_if p P) (bi_affinely_if p 𝓟).
98
Proof. destruct p; simpl; apply _. Qed.
99 100
Global Instance make_monPred_at_embed i 𝓟 : MakeMonPredAt i ⎡𝓟⎤ 𝓟.
Proof. by rewrite /MakeMonPredAt monPred_at_embed. Qed.
101
Global Instance make_monPred_at_in i j : MakeMonPredAt j (monPred_in i) i  j.
102
Proof. by rewrite /MakeMonPredAt monPred_at_in. Qed.
103 104
Global Instance make_monPred_at_default i P : MakeMonPredAt i P (P i) | 100.
Proof. by rewrite /MakeMonPredAt. Qed.
105 106
Global Instance make_monPred_at_bupd `{BUpdFacts PROP} i P 𝓟 :
  MakeMonPredAt i P 𝓟  MakeMonPredAt i (|==> P)%I (|==> 𝓟)%I.
107
Proof. by rewrite /MakeMonPredAt monPred_at_bupd=> <-. Qed.
108

109 110
Global Instance from_assumption_make_monPred_at_l p i j P 𝓟 :
  MakeMonPredAt i P 𝓟  IsBiIndexRel j i  FromAssumption p (P j) 𝓟.
111
Proof.
112
  rewrite /MakeMonPredAt /FromAssumption /IsBiIndexRel=><- ->.
113 114
  apply  bi.affinely_persistently_if_elim.
Qed.
115 116
Global Instance from_assumption_make_monPred_at_r p i j P 𝓟 :
  MakeMonPredAt i P 𝓟  IsBiIndexRel i j  FromAssumption p 𝓟 (P j).
117
Proof.
118
  rewrite /MakeMonPredAt /FromAssumption /IsBiIndexRel=><- ->.
119 120 121
  apply  bi.affinely_persistently_if_elim.
Qed.

122 123 124 125 126 127
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.
128

129
Global Instance as_valid_monPred_at φ P (Φ : I  PROP) :
130
  AsValid0 φ P  ( i, MakeMonPredAt i P (Φ i))  AsValid φ ( i, Φ i) | 100.
131
Proof.
132
  rewrite /MakeMonPredAt /AsValid0 /AsValid /bi_valid=> -> EQ.
133 134 135
  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 //.
136
Qed.
137
Global Instance as_valid_monPred_at_wand φ P Q (Φ Ψ : I  PROP) :
138
  AsValid0 φ (P - Q) 
139
  ( i, MakeMonPredAt i P (Φ i))  ( i, MakeMonPredAt i Q (Ψ i)) 
140
  AsValid φ ( i, Φ i - Ψ i).
141
Proof.
142
  rewrite /AsValid0 /AsValid /MakeMonPredAt. intros -> EQ1 EQ2.
143
  setoid_rewrite <-EQ1. setoid_rewrite <-EQ2. split.
144 145
  - move=>/bi.wand_entails HP. setoid_rewrite HP. by iIntros (i) "$".
  - move=>HP. apply bi.entails_wand. split=>i. iIntros "H". by iApply HP.
146
Qed.
147
Global Instance as_valid_monPred_at_equiv φ P Q (Φ Ψ : I  PROP) :
148
  AsValid0 φ (P - Q) 
149
  ( i, MakeMonPredAt i P (Φ i))  ( i, MakeMonPredAt i Q (Ψ i)) 
150
  AsValid φ ( i, Φ i - Ψ i).
151
Proof.
152
  rewrite /AsValid0 /AsValid /MakeMonPredAt. intros -> EQ1 EQ2.
153
  setoid_rewrite <-EQ1. setoid_rewrite <-EQ2. split.
154 155
  - 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.
156
Qed.
157

158 159
Global Instance into_pure_monPred_at P φ i : IntoPure P φ  IntoPure (P i) φ.
Proof. rewrite /IntoPure=>->. by rewrite monPred_at_pure. Qed.
160 161
Global Instance from_pure_monPred_at P φ i : FromPure P φ  FromPure (P i) φ.
Proof. rewrite /FromPure=><-. by rewrite monPred_at_pure. Qed.
162 163
Global Instance into_pure_monPred_in i j : @IntoPure PROP (monPred_in i j) (i  j).
Proof. by rewrite /IntoPure monPred_at_in. Qed.
164 165
Global Instance from_pure_monPred_in i j : @FromPure PROP (monPred_in i j) (i  j).
Proof. by rewrite /FromPure monPred_at_in. Qed.
166

167 168
Global Instance into_persistent_monPred_at p P Q 𝓠 i :
  IntoPersistent p P Q  MakeMonPredAt i Q 𝓠  IntoPersistent p (P i) 𝓠 | 0.
169
Proof.
170 171
  rewrite /IntoPersistent /MakeMonPredAt  =>-[/(_ i) ?] <-.
  by rewrite -monPred_at_persistently -monPred_at_persistently_if.
172
Qed.
173

Robbert Krebbers's avatar
Robbert Krebbers committed
174 175 176
Global Instance from_always_affinely_monPred_at P Q 𝓠 i :
  FromAlways always_modality_affinely P Q  MakeMonPredAt i Q 𝓠 
  FromAlways always_modality_affinely (P i) 𝓠 | 0.
177
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
178 179 180 181 182 183 184 185 186 187 188 189 190 191
  rewrite /FromAlways /MakeMonPredAt /==> <- <-. by rewrite monPred_at_affinely.
Qed.
Global Instance from_always_persistently_monPred_at P Q 𝓠 i :
  FromAlways always_modality_persistently P Q  MakeMonPredAt i Q 𝓠 
  FromAlways always_modality_persistently (P i) 𝓠 | 0.
Proof.
  rewrite /FromAlways /MakeMonPredAt /==> <- <-. by rewrite monPred_at_persistently.
Qed.
Global Instance from_always_affinely_persistently_monPred_at P Q 𝓠 i :
  FromAlways always_modality_affinely_persistently P Q  MakeMonPredAt i Q 𝓠 
  FromAlways always_modality_affinely_persistently (P i) 𝓠 | 0.
Proof.
  rewrite /FromAlways /MakeMonPredAt /==> <- <-.
  by rewrite monPred_at_affinely monPred_at_persistently.
192 193
Qed.

194 195
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 𝓠 
196
  IntoWand p q (R i) 𝓟 𝓠.
197
Proof.
198
  rewrite /IntoWand /MakeMonPredAt /bi_affinely_if /bi_persistently_if.
199
  destruct p, q=> /bi.wand_elim_l' [/(_ i) H] <- <-; apply bi.wand_intro_r;
200
  revert H; by rewrite monPred_at_sep ?monPred_at_affinely ?monPred_at_persistently.
201
Qed.
202
Lemma into_wand_monPred_at_unknown_known p q R P 𝓟 Q i j :
203
  IsBiIndexRel i j  IntoWand p q R P Q 
204
  MakeMonPredAt j P 𝓟  IntoWand p q (R i) 𝓟 (Q j).
205
Proof.
206 207
  rewrite /IntoWand /IsBiIndexRel /MakeMonPredAt=>-> ? ?.
  eapply into_wand_monPred_at_unknown_unknown=>//. apply _.
208
Qed.
209
Lemma into_wand_monPred_at_known_unknown_le p q R P Q 𝓠 i j :
210
  IsBiIndexRel i j  IntoWand p q R P Q 
211
  MakeMonPredAt j Q 𝓠  IntoWand p q (R i) (P j) 𝓠.
212
Proof.
213 214
  rewrite /IntoWand /IsBiIndexRel /MakeMonPredAt=>-> ? ?.
  eapply into_wand_monPred_at_unknown_unknown=>//. apply _.
215
Qed.
216
Lemma into_wand_monPred_at_known_unknown_ge p q R P Q 𝓠 i j :
217
  IsBiIndexRel i j  IntoWand p q R P Q 
218
  MakeMonPredAt j Q 𝓠  IntoWand p q (R j) (P i) 𝓠.
219
Proof.
220 221
  rewrite /IntoWand /IsBiIndexRel /MakeMonPredAt=>-> ? ?.
  eapply into_wand_monPred_at_unknown_unknown=>//. apply _.
222
Qed.
223

224 225 226 227 228 229 230
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.

231 232
Global Instance from_forall_monPred_at_wand P Q (Φ Ψ : I  PROP) i :
  ( j, MakeMonPredAt j P (Φ j))  ( j, MakeMonPredAt j Q (Ψ j)) 
233 234
  FromForall ((P - Q) i)%I (λ j, i  j  Φ j - Ψ j)%I.
Proof.
235
  rewrite /FromForall /MakeMonPredAt monPred_at_wand=> H1 H2. do 2 f_equiv.
236
  by rewrite H1 H2.
237
Qed.
238 239
Global Instance from_forall_monPred_at_impl P Q (Φ Ψ : I  PROP) i :
  ( j, MakeMonPredAt j P (Φ j))  ( j, MakeMonPredAt j Q (Ψ j)) 
240 241
  FromForall ((P  Q) i)%I (λ j, i  j  Φ j  Ψ j)%I.
Proof.
242
  rewrite /FromForall /MakeMonPredAt monPred_at_impl=> H1 H2. do 2 f_equiv.
243
  by rewrite H1 H2 bi.pure_impl_forall.
244 245
Qed.

246
Global Instance into_forall_monPred_at_index P i :
247 248 249 250 251
  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.
252

253 254
Global Instance from_and_monPred_at P Q1 𝓠1 Q2 𝓠2 i :
  FromAnd P Q1 Q2  MakeMonPredAt i Q1 𝓠1  MakeMonPredAt i Q2 𝓠2 
255
  FromAnd (P i) 𝓠1 𝓠2.
256 257 258 259
Proof.
  rewrite /FromAnd /MakeMonPredAt /MakeMonPredAt=> <- <- <-.
  by rewrite monPred_at_and.
Qed.
260 261
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 
262
  IntoAnd p (P i) 𝓠1 𝓠2.
263
Proof.
264
  rewrite /IntoAnd /MakeMonPredAt /bi_affinely_if /bi_persistently_if.
265 266
  destruct p=>-[/(_ i) H] <- <-; revert H;
  by rewrite ?monPred_at_affinely ?monPred_at_persistently monPred_at_and.
267 268
Qed.

269 270
Global Instance from_sep_monPred_at P Q1 𝓠1 Q2 𝓠2 i :
  FromSep P Q1 Q2  MakeMonPredAt i Q1 𝓠1  MakeMonPredAt i Q2 𝓠2 
271
  FromSep (P i) 𝓠1 𝓠2.
272
Proof. rewrite /FromSep /MakeMonPredAt=> <- <- <-. by rewrite monPred_at_sep. Qed.
273 274
Global Instance into_sep_monPred_at P Q1 𝓠1 Q2 𝓠2 i :
  IntoSep P Q1 Q2  MakeMonPredAt i Q1 𝓠1  MakeMonPredAt i Q2 𝓠2 
275
  IntoSep (P i) 𝓠1 𝓠2.
276
Proof. rewrite /IntoSep /MakeMonPredAt=> -> <- <-. by rewrite monPred_at_sep. Qed.
277 278
Global Instance from_or_monPred_at P Q1 𝓠1 Q2 𝓠2 i :
  FromOr P Q1 Q2  MakeMonPredAt i Q1 𝓠1  MakeMonPredAt i Q2 𝓠2 
279
  FromOr (P i) 𝓠1 𝓠2.
280
Proof. rewrite /FromOr /MakeMonPredAt=> <- <- <-. by rewrite monPred_at_or. Qed.
281 282
Global Instance into_or_monPred_at P Q1 𝓠1 Q2 𝓠2 i :
  IntoOr P Q1 Q2  MakeMonPredAt i Q1 𝓠1  MakeMonPredAt i Q2 𝓠2 
283
  IntoOr (P i) 𝓠1 𝓠2.
284
Proof. rewrite /IntoOr /MakeMonPredAt=> -> <- <-. by rewrite monPred_at_or. Qed.
285

286 287
Global Instance from_exist_monPred_at {A} P (Φ : A  monPred) (Ψ : A  PROP) i :
  FromExist P Φ  ( a, MakeMonPredAt i (Φ a) (Ψ a))  FromExist (P i) Ψ.
288
Proof.
289 290
  rewrite /FromExist /MakeMonPredAt=><- H. setoid_rewrite <- H.
  by rewrite monPred_at_exist.
291
Qed.
292 293
Global Instance into_exist_monPred_at {A} P (Φ : A  monPred) (Ψ : A  PROP) i :
  IntoExist P Φ  ( a, MakeMonPredAt i (Φ a) (Ψ a))  IntoExist (P i) Ψ.
294
Proof.
295 296
  rewrite /IntoExist /MakeMonPredAt=>-> H. setoid_rewrite <- H.
  by rewrite monPred_at_exist.
297 298
Qed.

299 300
Global Instance foram_forall_monPred_at_plainly i P Φ :
  ( i, MakeMonPredAt i P (Φ i)) 
301
  FromForall (bi_plainly P i) (λ j, bi_plainly (Φ j)).
302 303 304 305
Proof.
  rewrite /FromForall /MakeMonPredAt=>H. rewrite monPred_at_plainly.
  by setoid_rewrite H.
Qed.
306 307
Global Instance into_forall_monPred_at_plainly i P Φ :
  ( i, MakeMonPredAt i P (Φ i)) 
308
  IntoForall (bi_plainly P i) (λ j, bi_plainly (Φ j)).
309 310 311 312
Proof.
  rewrite /IntoForall /MakeMonPredAt=>H. rewrite monPred_at_plainly.
  by setoid_rewrite H.
Qed.
313

314 315
Global Instance from_forall_monPred_at_absolutely P (Φ : I  PROP) i :
  ( i, MakeMonPredAt i P (Φ i))  FromForall (( P) i)%I Φ.
316
Proof.
317
  rewrite /FromForall /MakeMonPredAt monPred_at_absolutely=>H. by setoid_rewrite <- H.
318
Qed.
319 320
Global Instance into_forall_monPred_at_absolutely P (Φ : I  PROP) i :
  ( i, MakeMonPredAt i P (Φ i))  IntoForall (( P) i) Φ.
321
Proof.
322
  rewrite /IntoForall /MakeMonPredAt monPred_at_absolutely=>H. by setoid_rewrite <- H.
323
Qed.
324

325
Global Instance from_exist_monPred_at_ex P (Φ : I  PROP) i :
326
  ( i, MakeMonPredAt i P (Φ i))  FromExist (( P) i) Φ.
327
Proof.
328
  rewrite /FromExist /MakeMonPredAt monPred_at_ex=>H. by setoid_rewrite <- H.
329 330
Qed.
Global Instance into_exist_monPred_at_ex P (Φ : I  PROP) i :
331
  ( i, MakeMonPredAt i P (Φ i))  IntoExist (( P) i) Φ.
332
Proof.
333
  rewrite /IntoExist /MakeMonPredAt monPred_at_ex=>H. by setoid_rewrite <- H.
334 335
Qed.

336 337
Global Instance from_forall_monPred_at {A} P (Φ : A  monPred) (Ψ : A  PROP) i :
  FromForall P Φ  ( a, MakeMonPredAt i (Φ a) (Ψ a))  FromForall (P i) Ψ.
338
Proof.
339 340
  rewrite /FromForall /MakeMonPredAt=><- H. setoid_rewrite <- H.
  by rewrite monPred_at_forall.
341
Qed.
342 343
Global Instance into_forall_monPred_at {A} P (Φ : A  monPred) (Ψ : A  PROP) i :
  IntoForall P Φ  ( a, MakeMonPredAt i (Φ a) (Ψ a))  IntoForall (P i) Ψ.
344
Proof.
345 346
  rewrite /IntoForall /MakeMonPredAt=>-> H. setoid_rewrite <- H.
  by rewrite monPred_at_forall.
347 348
Qed.

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

368 369 370
Global Instance from_modal_monPred_at i P Q 𝓠 :
  FromModal P Q  MakeMonPredAt i Q 𝓠  FromModal (P i) 𝓠.
Proof. by rewrite /FromModal /MakeMonPredAt=> <- <-. Qed.
371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387

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).
388
Proof. by rewrite /ElimModal !monPred_at_bupd. Qed.
389 390 391
Global Instance elim_modal_at_bupd_hyp `{BUpdFacts PROP} P 𝓟' 𝓠 𝓠' i:
  ElimModal (|==> P i) 𝓟' 𝓠 𝓠' 
  ElimModal ((|==> P) i) 𝓟' 𝓠 𝓠'.
392
Proof. by rewrite /ElimModal monPred_at_bupd. Qed.
393 394 395

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

399
(* When P and/or Q are evars when doing typeclass search on [IntoWand
400
   (R i) P Q], we use [MakeMonPredAt] in order to normalize the
401 402
   result of unification. However, when they are not evars, we want to
   propagate the known information through typeclass search. Hence, we
403
   do not want to use [MakeMonPredAt].
404 405

   As a result, depending on P and Q being evars, we use a different
406 407
   version of [into_wand_monPred_at_xx_xx]. *)
Hint Extern 3 (IntoWand _ _ (monPred_at _ _) ?P ?Q) =>
408
     is_evar P; is_evar Q;
409
     eapply @into_wand_monPred_at_unknown_unknown
410
     : typeclass_instances.
411 412
Hint Extern 2 (IntoWand _ _ (monPred_at _ _) ?P (monPred_at ?Q _)) =>
     eapply @into_wand_monPred_at_unknown_known
413
     : typeclass_instances.
414 415
Hint Extern 2 (IntoWand _ _ (monPred_at _ _) (monPred_at ?P _) ?Q) =>
     eapply @into_wand_monPred_at_known_unknown_le
416
     : typeclass_instances.
417 418
Hint Extern 2 (IntoWand _ _ (monPred_at _ _) (monPred_at ?P _) ?Q) =>
     eapply @into_wand_monPred_at_known_unknown_ge
419
     : typeclass_instances.
420

421
Section sbi.
422
Context {I : biIndex} {PROP : sbi}.
423 424
Local Notation monPred := (monPred I PROP).
Implicit Types P Q R : monPred.
425
Implicit Types 𝓟 𝓠 𝓡 : PROP.
426 427 428
Implicit Types φ : Prop.
Implicit Types i j : I.

429
Global Instance is_except_0_monPred_at i P :
430
  IsExcept0 P  IsExcept0 (P i).
431
Proof. rewrite /IsExcept0=>- [/(_ i)]. by rewrite monPred_at_except_0. Qed.
432

433 434 435
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.
436 437
Global Instance make_monPred_at_except_0 i P 𝓠 :
  MakeMonPredAt i P 𝓠  MakeMonPredAt i ( P)%I ( 𝓠)%I.
438
Proof. by rewrite /MakeMonPredAt monPred_at_except_0=><-. Qed.
439 440
Global Instance make_monPred_at_later i P 𝓠 :
  MakeMonPredAt i P 𝓠  MakeMonPredAt i ( P)%I ( 𝓠)%I.
441
Proof. by rewrite /MakeMonPredAt monPred_at_later=><-. Qed.
442 443
Global Instance make_monPred_at_laterN i n P 𝓠 :
  MakeMonPredAt i P 𝓠  MakeMonPredAt i (^n P)%I (^n 𝓠)%I.
444
Proof. rewrite /MakeMonPredAt=> <-. elim n=>//= ? <-. by rewrite monPred_at_later. Qed.
445 446
Global Instance make_monPred_at_fupd `{FUpdFacts PROP} i E1 E2 P 𝓟 :
  MakeMonPredAt i P 𝓟  MakeMonPredAt i (|={E1,E2}=> P)%I (|={E1,E2}=> 𝓟)%I.
447
Proof. by rewrite /MakeMonPredAt monPred_at_fupd=> <-. Qed.
448

449 450 451 452
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.

453 454
Global Instance into_except_0_monPred_at_fwd i P Q 𝓠 :
  IntoExcept0 P Q  MakeMonPredAt i Q 𝓠  IntoExcept0 (P i) 𝓠.
455
Proof. rewrite /IntoExcept0 /MakeMonPredAt=> -> <-. by rewrite monPred_at_except_0. Qed.
456 457
Global Instance into_except_0_monPred_at_bwd i P 𝓟 Q :
  IntoExcept0 P Q  MakeMonPredAt i P 𝓟  IntoExcept0 𝓟 (Q i).
458
Proof. rewrite /IntoExcept0 /MakeMonPredAt=> H <-. by rewrite H monPred_at_except_0. Qed.
459

460 461
Global Instance into_later_monPred_at i n P Q 𝓠 :
  IntoLaterN n P Q  MakeMonPredAt i Q 𝓠  IntoLaterN n (P i) 𝓠.
462
Proof.
463 464
  rewrite /IntoLaterN /MakeMonPredAt=> -> <-. elim n=>//= ? <-.
   by rewrite monPred_at_later.
465
Qed.
466 467
Global Instance from_later_monPred_at i n P Q 𝓠 :
  FromLaterN n P Q  MakeMonPredAt i Q 𝓠  FromLaterN n (P i) 𝓠.
468 469 470 471
Proof.
  rewrite /FromLaterN /MakeMonPredAt=> <- <-. elim n=>//= ? ->.
  by rewrite monPred_at_later.
Qed.
472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488

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}=> 𝓠'.
Proof. by rewrite /ElimModal !monPred_fupd_embed. Qed.
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'.
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.

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).
489
Proof. by rewrite /ElimModal !monPred_at_fupd. Qed.
490 491 492
Global Instance elim_modal_at_fupd_hyp `{FUpdFacts PROP} E1 E2 P 𝓟' 𝓠 𝓠' i :
  ElimModal (|={E1,E2}=> P i) 𝓟' 𝓠 𝓠' 
  ElimModal ((|={E1,E2}=> P) i) 𝓟' 𝓠 𝓠'.
493
Proof. by rewrite /ElimModal monPred_at_fupd. Qed.
494 495 496

Global Instance add_modal_at_fupd_goal `{FUpdFacts PROP} E1 E2 𝓟 𝓟' Q i :
  AddModal 𝓟 𝓟' (|={E1,E2}=> Q i)  AddModal 𝓟 𝓟' ((|={E1,E2}=> Q) i).
497
Proof. by rewrite /AddModal !monPred_at_fupd. Qed.
498
End sbi.