monpred.v 22.8 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 44 45
Global Instance from_modal_absolutely P :
  FromModal modality_absolutely ( P) P | 1.
Proof. by rewrite /FromModal. Qed.
46 47 48
Global Instance from_modal_relatively P :
  FromModal modality_id ( P) P | 1.
Proof. by rewrite /FromModal /= -monPred_relatively_intro. Qed.
49

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

96 97
Global Instance from_assumption_make_monPred_at_l p i j P 𝓟 :
  MakeMonPredAt i P 𝓟  IsBiIndexRel j i  FromAssumption p (P j) 𝓟.
98
Proof.
99
  rewrite /MakeMonPredAt /FromAssumption /IsBiIndexRel=><- ->.
100 101
  apply  bi.affinely_persistently_if_elim.
Qed.
102 103
Global Instance from_assumption_make_monPred_at_r p i j P 𝓟 :
  MakeMonPredAt i P 𝓟  IsBiIndexRel i j  FromAssumption p 𝓟 (P j).
104
Proof.
105
  rewrite /MakeMonPredAt /FromAssumption /IsBiIndexRel=><- ->.
106 107 108
  apply  bi.affinely_persistently_if_elim.
Qed.

109 110 111 112 113 114
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.
115

116
Global Instance as_valid_monPred_at φ P (Φ : I  PROP) :
117
  AsValid0 φ P  ( i, MakeMonPredAt i P (Φ i))  AsValid φ ( i, Φ i) | 100.
118
Proof.
119
  rewrite /MakeMonPredAt /AsValid0 /AsValid /bi_valid=> -> EQ.
120 121 122
  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 //.
123
Qed.
124
Global Instance as_valid_monPred_at_wand φ P Q (Φ Ψ : I  PROP) :
125
  AsValid0 φ (P - Q) 
126
  ( i, MakeMonPredAt i P (Φ i))  ( i, MakeMonPredAt i Q (Ψ i)) 
127
  AsValid φ ( i, Φ i - Ψ i).
128
Proof.
129
  rewrite /AsValid0 /AsValid /MakeMonPredAt. intros -> EQ1 EQ2.
130
  setoid_rewrite <-EQ1. setoid_rewrite <-EQ2. split.
131 132
  - move=>/bi.wand_entails HP. setoid_rewrite HP. by iIntros (i) "$".
  - move=>HP. apply bi.entails_wand. split=>i. iIntros "H". by iApply HP.
133
Qed.
134
Global Instance as_valid_monPred_at_equiv φ P Q (Φ Ψ : I  PROP) :
135
  AsValid0 φ (P - Q) 
136
  ( i, MakeMonPredAt i P (Φ i))  ( i, MakeMonPredAt i Q (Ψ i)) 
137
  AsValid φ ( i, Φ i - Ψ i).
138
Proof.
139
  rewrite /AsValid0 /AsValid /MakeMonPredAt. intros -> EQ1 EQ2.
140
  setoid_rewrite <-EQ1. setoid_rewrite <-EQ2. split.
141 142
  - 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.
143
Qed.
144

145 146
Global Instance into_pure_monPred_at P φ i : IntoPure P φ  IntoPure (P i) φ.
Proof. rewrite /IntoPure=>->. by rewrite monPred_at_pure. Qed.
147 148
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.
149 150
Global Instance into_pure_monPred_in i j : @IntoPure PROP (monPred_in i j) (i  j).
Proof. by rewrite /IntoPure monPred_at_in. Qed.
151 152
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.
153

154 155
Global Instance into_persistent_monPred_at p P Q 𝓠 i :
  IntoPersistent p P Q  MakeMonPredAt i Q 𝓠  IntoPersistent p (P i) 𝓠 | 0.
156
Proof.
157 158
  rewrite /IntoPersistent /MakeMonPredAt  =>-[/(_ i) ?] <-.
  by rewrite -monPred_at_persistently -monPred_at_persistently_if.
159
Qed.
160

161 162 163
Global Instance from_modal_affinely_monPred_at P Q 𝓠 i :
  FromModal modality_affinely P Q  MakeMonPredAt i Q 𝓠 
  FromModal modality_affinely (P i) 𝓠 | 0.
164
Proof.
165
  rewrite /FromModal /MakeMonPredAt /==> <- <-. by rewrite monPred_at_affinely.
Robbert Krebbers's avatar
Robbert Krebbers committed
166
Qed.
167 168 169
Global Instance from_modal_persistently_monPred_at P Q 𝓠 i :
  FromModal modality_persistently P Q  MakeMonPredAt i Q 𝓠 
  FromModal modality_persistently (P i) 𝓠 | 0.
Robbert Krebbers's avatar
Robbert Krebbers committed
170
Proof.
171
  rewrite /FromModal /MakeMonPredAt /==> <- <-. by rewrite monPred_at_persistently.
Robbert Krebbers's avatar
Robbert Krebbers committed
172
Qed.
173 174 175
Global Instance from_modal_affinely_persistently_monPred_at P Q 𝓠 i :
  FromModal modality_affinely_persistently P Q  MakeMonPredAt i Q 𝓠 
  FromModal modality_affinely_persistently (P i) 𝓠 | 0.
Robbert Krebbers's avatar
Robbert Krebbers committed
176
Proof.
177
  rewrite /FromModal /MakeMonPredAt /==> <- <-.
Robbert Krebbers's avatar
Robbert Krebbers committed
178
  by rewrite monPred_at_affinely monPred_at_persistently.
179 180
Qed.

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

211 212 213 214 215 216 217
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.

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

233
Global Instance into_forall_monPred_at_index P i :
234 235 236 237 238
  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.
239

240 241
Global Instance from_and_monPred_at P Q1 𝓠1 Q2 𝓠2 i :
  FromAnd P Q1 Q2  MakeMonPredAt i Q1 𝓠1  MakeMonPredAt i Q2 𝓠2 
242
  FromAnd (P i) 𝓠1 𝓠2.
243 244 245 246
Proof.
  rewrite /FromAnd /MakeMonPredAt /MakeMonPredAt=> <- <- <-.
  by rewrite monPred_at_and.
Qed.
247 248
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 
249
  IntoAnd p (P i) 𝓠1 𝓠2.
250
Proof.
251
  rewrite /IntoAnd /MakeMonPredAt /bi_affinely_if /bi_persistently_if.
252 253
  destruct p=>-[/(_ i) H] <- <-; revert H;
  by rewrite ?monPred_at_affinely ?monPred_at_persistently monPred_at_and.
254 255
Qed.

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

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

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

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

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

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

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

355
Global Instance from_modal_monPred_at i P Q 𝓠 :
356
  FromModal modality_id P Q  MakeMonPredAt i Q 𝓠  FromModal modality_id (P i) 𝓠.
357
Proof. by rewrite /FromModal /MakeMonPredAt=> <- <-. Qed.
358 359 360
Global Instance into_embed_absolute P :
  Absolute P  IntoEmbed P ( i, P i).
Proof. rewrite /IntoEmbed=> ?. by rewrite {1}(absolute_absolutely P). Qed.
361 362
End bi.

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

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

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

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

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

416 417 418 419
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.

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

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

Ralf Jung's avatar
Ralf Jung committed
441 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
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.

467 468 469
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}=> 𝓠'.
470
Proof. by rewrite /ElimModal !monPred_fupd_embed. Qed.
471 472 473
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'.
474 475 476 477 478 479
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.

480 481 482
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).
483
Proof. by rewrite /ElimModal !monPred_at_fupd. Qed.
484 485 486
Global Instance elim_modal_at_fupd_hyp `{FUpdFacts PROP} φ E1 E2 P 𝓟' 𝓠 𝓠' i :
  ElimModal φ (|={E1,E2}=> P i) 𝓟' 𝓠 𝓠' 
  ElimModal φ ((|={E1,E2}=> P) i) 𝓟' 𝓠 𝓠'.
487
Proof. by rewrite /ElimModal monPred_at_fupd. Qed.
488 489 490

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