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 a P φ i : FromPure a P φ  FromPure a (P i) φ.
Proof. rewrite /FromPure=><-. by rewrite monPred_at_affinely_if 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 af : @FromPure PROP af (monPred_in i j) (i  j).
Proof. by rewrite /FromPure monPred_at_in bi.affinely_if_elim. 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.