monpred.v 22.8 KB
Newer Older
1
From iris.bi Require Export monpred.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
From iris.bi Require Import plainly.
3
From iris.proofmode Require Import tactics modality_instances.
4

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

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

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

21
22
23
  Lemma modality_objectively_mixin :
    modality_mixin (@monPred_objectively I PROP)
      (MIEnvFilter Objective) (MIEnvFilter Objective).
24
  Proof.
25
26
    split; simpl; split_and?; intros;
      try match goal with H : TCDiag _ _ _ |- _ => destruct H end;
27
28
29
      eauto using bi.equiv_entails_sym, objective_objectively,
        monPred_objectively_mono, monPred_objectively_and,
        monPred_objectively_sep_2 with typeclass_instances.
30
  Qed.
31
32
  Definition modality_objectively :=
    Modality _ modality_objectively_mixin.
33
End modalities.
34

35
Section bi.
36
Context {I : biIndex} {PROP : bi}.
Robbert Krebbers's avatar
Robbert Krebbers committed
37
Local Notation monPredI := (monPredI I PROP).
38
Local Notation monPred := (monPred I PROP).
39
Local Notation MakeMonPredAt := (@MakeMonPredAt I PROP).
40
Implicit Types P Q R : monPred.
41
Implicit Types 𝓟 𝓠 𝓡 : PROP.
42
43
44
Implicit Types φ : Prop.
Implicit Types i j : I.

45
Global Instance from_modal_objectively P :
Robbert Krebbers's avatar
Robbert Krebbers committed
46
  FromModal modality_objectively (<obj> P) (<obj> P) P | 1.
47
Proof. by rewrite /FromModal. Qed.
48
Global Instance from_modal_subjectively P :
Robbert Krebbers's avatar
Robbert Krebbers committed
49
  FromModal modality_id (<subj> P) (<subj> P) P | 1.
50
Proof. by rewrite /FromModal /= -monPred_subjectively_intro. Qed.
51

52
53
54
55
56
57
58
59
60
61
62
63
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.
64
Global Instance from_modal_intuitionistically_monPred_at `(sel : A) P Q 𝓠 i :
65
66
  FromModal modality_intuitionistically sel P Q  MakeMonPredAt i Q 𝓠 
  FromModal modality_intuitionistically sel (P i) 𝓠 | 0.
67
68
69
70
71
72
73
74
75
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.

76
Global Instance make_monPred_at_pure φ i : MakeMonPredAt i ⌜φ⌝ ⌜φ⌝.
77
Proof. by rewrite /MakeMonPredAt monPred_at_pure. Qed.
78
Global Instance make_monPred_at_emp i : MakeMonPredAt i emp emp.
79
Proof. by rewrite /MakeMonPredAt monPred_at_emp. Qed.
80
81
82
Global Instance make_monPred_at_sep i P 𝓟 Q 𝓠 :
  MakeMonPredAt i P 𝓟  MakeMonPredAt i Q 𝓠 
  MakeMonPredAt i (P  Q) (𝓟  𝓠).
83
Proof. by rewrite /MakeMonPredAt monPred_at_sep=><-<-. Qed.
84
85
86
Global Instance make_monPred_at_and i P 𝓟 Q 𝓠 :
  MakeMonPredAt i P 𝓟  MakeMonPredAt i Q 𝓠 
  MakeMonPredAt i (P  Q) (𝓟  𝓠).
87
Proof. by rewrite /MakeMonPredAt monPred_at_and=><-<-. Qed.
88
89
90
Global Instance make_monPred_at_or i P 𝓟 Q 𝓠 :
  MakeMonPredAt i P 𝓟  MakeMonPredAt i Q 𝓠 
  MakeMonPredAt i (P  Q) (𝓟  𝓠).
91
Proof. by rewrite /MakeMonPredAt monPred_at_or=><-<-. Qed.
92
93
Global Instance make_monPred_at_forall {A} i (Φ : A  monPred) (Ψ : A  PROP) :
  ( a, MakeMonPredAt i (Φ a) (Ψ a))  MakeMonPredAt i ( a, Φ a) ( a, Ψ a).
94
Proof. rewrite /MakeMonPredAt monPred_at_forall=>H. by setoid_rewrite <- H. Qed.
95
96
Global Instance make_monPred_at_exists {A} i (Φ : A  monPred) (Ψ : A  PROP) :
  ( a, MakeMonPredAt i (Φ a) (Ψ a))  MakeMonPredAt i ( a, Φ a) ( a, Ψ a).
97
Proof. rewrite /MakeMonPredAt monPred_at_exist=>H. by setoid_rewrite <- H. Qed.
98
Global Instance make_monPred_at_persistently i P 𝓟 :
99
  MakeMonPredAt i P 𝓟  MakeMonPredAt i (<pers> P) (<pers> 𝓟).
100
Proof. by rewrite /MakeMonPredAt monPred_at_persistently=><-. Qed.
101
Global Instance make_monPred_at_affinely i P 𝓟 :
102
  MakeMonPredAt i P 𝓟  MakeMonPredAt i (<affine> P) (<affine> 𝓟).
103
Proof. by rewrite /MakeMonPredAt monPred_at_affinely=><-. Qed.
104
105
106
Global Instance make_monPred_at_intuitionistically i P 𝓟 :
  MakeMonPredAt i P 𝓟  MakeMonPredAt i ( P) ( 𝓟).
Proof. by rewrite /MakeMonPredAt monPred_at_intuitionistically=><-. Qed.
107
Global Instance make_monPred_at_absorbingly i P 𝓟 :
108
  MakeMonPredAt i P 𝓟  MakeMonPredAt i (<absorb> P) (<absorb> 𝓟).
109
Proof. by rewrite /MakeMonPredAt monPred_at_absorbingly=><-. Qed.
110
111
Global Instance make_monPred_at_persistently_if i P 𝓟 p :
  MakeMonPredAt i P 𝓟 
112
  MakeMonPredAt i (<pers>?p P) (<pers>?p 𝓟).
113
Proof. destruct p; simpl; apply _. Qed.
114
115
Global Instance make_monPred_at_affinely_if i P 𝓟 p :
  MakeMonPredAt i P 𝓟 
116
  MakeMonPredAt i (<affine>?p P) (<affine>?p 𝓟).
117
Proof. destruct p; simpl; apply _. Qed.
118
119
120
121
Global Instance make_monPred_at_intuitionistically_if i P 𝓟 p :
  MakeMonPredAt i P 𝓟 
  MakeMonPredAt i (?p P) (?p 𝓟).
Proof. destruct p; simpl; apply _. Qed.
122
123
Global Instance make_monPred_at_embed i 𝓟 : MakeMonPredAt i ⎡𝓟⎤ 𝓟.
Proof. by rewrite /MakeMonPredAt monPred_at_embed. Qed.
124
Global Instance make_monPred_at_in i j : MakeMonPredAt j (monPred_in i) i  j.
125
Proof. by rewrite /MakeMonPredAt monPred_at_in. Qed.
126
127
Global Instance make_monPred_at_default i P : MakeMonPredAt i P (P i) | 100.
Proof. by rewrite /MakeMonPredAt. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
128
129
130
Global Instance make_monPred_at_bupd `{BiBUpd PROP} i P 𝓟 :
  MakeMonPredAt i P 𝓟  MakeMonPredAt i (|==> P)%I (|==> 𝓟)%I.
Proof. by rewrite /MakeMonPredAt monPred_at_bupd=> <-. Qed.
131

132
Global Instance from_assumption_make_monPred_at_l p i j P 𝓟 :
133
  MakeMonPredAt i P 𝓟  IsBiIndexRel j i  KnownLFromAssumption p (P j) 𝓟.
134
Proof.
135
  rewrite /MakeMonPredAt /KnownLFromAssumption /FromAssumption /IsBiIndexRel=><- ->.
136
  apply  bi.intuitionistically_if_elim.
137
Qed.
138
Global Instance from_assumption_make_monPred_at_r p i j P 𝓟 :
139
  MakeMonPredAt i P 𝓟  IsBiIndexRel i j  KnownRFromAssumption p 𝓟 (P j).
140
Proof.
141
  rewrite /MakeMonPredAt /KnownRFromAssumption /FromAssumption /IsBiIndexRel=><- ->.
142
  apply  bi.intuitionistically_if_elim.
143
144
Qed.

145
Global Instance from_assumption_make_monPred_objectively P Q :
146
  FromAssumption p P Q  KnownLFromAssumption p (<obj> P) Q.
147
148
Proof.
  intros ?.
149
  by rewrite /KnownLFromAssumption /FromAssumption monPred_objectively_elim.
150
Qed.
151
Global Instance from_assumption_make_monPred_subjectively P Q :
152
  FromAssumption p P Q  KnownRFromAssumption p P (<subj> Q).
153
154
Proof.
  intros ?.
155
  by rewrite /KnownRFromAssumption /FromAssumption -monPred_subjectively_intro.
156
Qed.
157

Ralf Jung's avatar
Ralf Jung committed
158
159
Global Instance as_emp_valid_monPred_at φ P (Φ : I  PROP) :
  AsEmpValid0 φ P  ( i, MakeMonPredAt i P (Φ i))  AsEmpValid φ ( i, Φ i) | 100.
160
Proof.
Ralf Jung's avatar
Ralf Jung committed
161
  rewrite /MakeMonPredAt /AsEmpValid0 /AsEmpValid /bi_emp_valid=> -> EQ.
162
163
164
  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 //.
165
Qed.
Ralf Jung's avatar
Ralf Jung committed
166
167
Global Instance as_emp_valid_monPred_at_wand φ P Q (Φ Ψ : I  PROP) :
  AsEmpValid0 φ (P - Q) 
168
  ( i, MakeMonPredAt i P (Φ i))  ( i, MakeMonPredAt i Q (Ψ i)) 
Ralf Jung's avatar
Ralf Jung committed
169
  AsEmpValid φ ( i, Φ i - Ψ i).
170
Proof.
Ralf Jung's avatar
Ralf Jung committed
171
  rewrite /AsEmpValid0 /AsEmpValid /MakeMonPredAt. intros -> EQ1 EQ2.
172
  setoid_rewrite <-EQ1. setoid_rewrite <-EQ2. split.
173
174
  - move=>/bi.wand_entails HP. setoid_rewrite HP. by iIntros (i) "$".
  - move=>HP. apply bi.entails_wand. split=>i. iIntros "H". by iApply HP.
175
Qed.
Ralf Jung's avatar
Ralf Jung committed
176
177
Global Instance as_emp_valid_monPred_at_equiv φ P Q (Φ Ψ : I  PROP) :
  AsEmpValid0 φ (P - Q) 
178
  ( i, MakeMonPredAt i P (Φ i))  ( i, MakeMonPredAt i Q (Ψ i)) 
Ralf Jung's avatar
Ralf Jung committed
179
  AsEmpValid φ ( i, Φ i - Ψ i).
180
Proof.
Ralf Jung's avatar
Ralf Jung committed
181
  rewrite /AsEmpValid0 /AsEmpValid /MakeMonPredAt. intros -> EQ1 EQ2.
182
  setoid_rewrite <-EQ1. setoid_rewrite <-EQ2. split.
183
184
  - 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.
185
Qed.
186

187
188
Global Instance into_pure_monPred_at P φ i : IntoPure P φ  IntoPure (P i) φ.
Proof. rewrite /IntoPure=>->. by rewrite monPred_at_pure. Qed.
189
190
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.
191
192
Global Instance into_pure_monPred_in i j : @IntoPure PROP (monPred_in i j) (i  j).
Proof. by rewrite /IntoPure monPred_at_in. Qed.
193
194
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.
195

196
197
Global Instance into_persistent_monPred_at p P Q 𝓠 i :
  IntoPersistent p P Q  MakeMonPredAt i Q 𝓠  IntoPersistent p (P i) 𝓠 | 0.
198
Proof.
199
200
  rewrite /IntoPersistent /MakeMonPredAt  =>-[/(_ i) ?] <-.
  by rewrite -monPred_at_persistently -monPred_at_persistently_if.
201
Qed.
202

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

233
234
235
236
237
238
239
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.

240
241
Global Instance from_forall_monPred_at_wand P Q (Φ Ψ : I  PROP) i :
  ( j, MakeMonPredAt j P (Φ j))  ( j, MakeMonPredAt j Q (Ψ j)) 
242
243
  FromForall ((P - Q) i)%I (λ j, i  j  Φ j - Ψ j)%I.
Proof.
244
  rewrite /FromForall /MakeMonPredAt monPred_at_wand=> H1 H2. do 2 f_equiv.
245
  by rewrite H1 H2.
246
Qed.
247
248
Global Instance from_forall_monPred_at_impl P Q (Φ Ψ : I  PROP) i :
  ( j, MakeMonPredAt j P (Φ j))  ( j, MakeMonPredAt j Q (Ψ j)) 
249
250
  FromForall ((P  Q) i)%I (λ j, i  j  Φ j  Ψ j)%I.
Proof.
251
  rewrite /FromForall /MakeMonPredAt monPred_at_impl=> H1 H2. do 2 f_equiv.
252
  by rewrite H1 H2 bi.pure_impl_forall.
253
254
Qed.

255
Global Instance into_forall_monPred_at_index P i :
256
257
258
259
260
  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.
261

262
263
Global Instance from_and_monPred_at P Q1 𝓠1 Q2 𝓠2 i :
  FromAnd P Q1 Q2  MakeMonPredAt i Q1 𝓠1  MakeMonPredAt i Q2 𝓠2 
264
  FromAnd (P i) 𝓠1 𝓠2.
265
266
267
268
Proof.
  rewrite /FromAnd /MakeMonPredAt /MakeMonPredAt=> <- <- <-.
  by rewrite monPred_at_and.
Qed.
269
270
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 
271
  IntoAnd p (P i) 𝓠1 𝓠2.
272
Proof.
273
  rewrite /IntoAnd /MakeMonPredAt /bi_affinely_if /bi_persistently_if.
274
275
  destruct p=>-[/(_ i) H] <- <-; revert H;
  by rewrite ?monPred_at_affinely ?monPred_at_persistently monPred_at_and.
276
277
Qed.

278
279
Global Instance from_sep_monPred_at P Q1 𝓠1 Q2 𝓠2 i :
  FromSep P Q1 Q2  MakeMonPredAt i Q1 𝓠1  MakeMonPredAt i Q2 𝓠2 
280
  FromSep (P i) 𝓠1 𝓠2.
281
Proof. rewrite /FromSep /MakeMonPredAt=> <- <- <-. by rewrite monPred_at_sep. Qed.
282
283
Global Instance into_sep_monPred_at P Q1 𝓠1 Q2 𝓠2 i :
  IntoSep P Q1 Q2  MakeMonPredAt i Q1 𝓠1  MakeMonPredAt i Q2 𝓠2 
284
  IntoSep (P i) 𝓠1 𝓠2.
285
Proof. rewrite /IntoSep /MakeMonPredAt=> -> <- <-. by rewrite monPred_at_sep. Qed.
286
287
Global Instance from_or_monPred_at P Q1 𝓠1 Q2 𝓠2 i :
  FromOr P Q1 Q2  MakeMonPredAt i Q1 𝓠1  MakeMonPredAt i Q2 𝓠2 
288
  FromOr (P i) 𝓠1 𝓠2.
289
Proof. rewrite /FromOr /MakeMonPredAt=> <- <- <-. by rewrite monPred_at_or. Qed.
290
291
Global Instance into_or_monPred_at P Q1 𝓠1 Q2 𝓠2 i :
  IntoOr P Q1 Q2  MakeMonPredAt i Q1 𝓠1  MakeMonPredAt i Q2 𝓠2 
292
  IntoOr (P i) 𝓠1 𝓠2.
293
Proof. rewrite /IntoOr /MakeMonPredAt=> -> <- <-. by rewrite monPred_at_or. Qed.
294

295
296
Global Instance from_exist_monPred_at {A} P (Φ : A  monPred) (Ψ : A  PROP) i :
  FromExist P Φ  ( a, MakeMonPredAt i (Φ a) (Ψ a))  FromExist (P i) Ψ.
297
Proof.
298
299
  rewrite /FromExist /MakeMonPredAt=><- H. setoid_rewrite <- H.
  by rewrite monPred_at_exist.
300
Qed.
301
302
Global Instance into_exist_monPred_at {A} P (Φ : A  monPred) (Ψ : A  PROP) i :
  IntoExist P Φ  ( a, MakeMonPredAt i (Φ a) (Ψ a))  IntoExist (P i) Ψ.
303
Proof.
304
305
  rewrite /IntoExist /MakeMonPredAt=>-> H. setoid_rewrite <- H.
  by rewrite monPred_at_exist.
306
307
Qed.

308
Global Instance from_forall_monPred_at_objectively P (Φ : I  PROP) i :
Robbert Krebbers's avatar
Robbert Krebbers committed
309
  ( i, MakeMonPredAt i P (Φ i))  FromForall ((<obj> P) i)%I Φ.
310
Proof.
311
  rewrite /FromForall /MakeMonPredAt monPred_at_objectively=>H. by setoid_rewrite <- H.
312
Qed.
313
Global Instance into_forall_monPred_at_objectively P (Φ : I  PROP) i :
Robbert Krebbers's avatar
Robbert Krebbers committed
314
  ( i, MakeMonPredAt i P (Φ i))  IntoForall ((<obj> P) i) Φ.
315
Proof.
316
  rewrite /IntoForall /MakeMonPredAt monPred_at_objectively=>H. by setoid_rewrite <- H.
317
Qed.
318

319
Global Instance from_exist_monPred_at_ex P (Φ : I  PROP) i :
Robbert Krebbers's avatar
Robbert Krebbers committed
320
  ( i, MakeMonPredAt i P (Φ i))  FromExist ((<subj> P) i) Φ.
321
Proof.
322
  rewrite /FromExist /MakeMonPredAt monPred_at_subjectively=>H. by setoid_rewrite <- H.
323
324
Qed.
Global Instance into_exist_monPred_at_ex P (Φ : I  PROP) i :
Robbert Krebbers's avatar
Robbert Krebbers committed
325
  ( i, MakeMonPredAt i P (Φ i))  IntoExist ((<subj> P) i) Φ.
326
Proof.
327
  rewrite /IntoExist /MakeMonPredAt monPred_at_subjectively=>H. by setoid_rewrite <- H.
328
329
Qed.

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

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

362
363
Global Instance into_embed_objective P :
  Objective P  IntoEmbed P ( i, P i).
364
365
Proof.
  rewrite /IntoEmbed=> ?.
366
  by rewrite {1}(objective_objectively P) monPred_objectively_unfold.
367
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
368

369
370
371
Global Instance elim_modal_at_bupd_goal `{BiBUpd PROP} φ p p' 𝓟 𝓟' Q Q' i :
  ElimModal φ p p' 𝓟 𝓟' (|==> Q i) (|==> Q' i) 
  ElimModal φ p p' 𝓟 𝓟' ((|==> Q) i) ((|==> Q') i).
Robbert Krebbers's avatar
Robbert Krebbers committed
372
Proof. by rewrite /ElimModal !monPred_at_bupd. Qed.
373
Global Instance elim_modal_at_bupd_hyp `{BiBUpd PROP} φ p p' P 𝓟 𝓟' 𝓠 𝓠' i:
374
  MakeMonPredAt i P 𝓟 
375
376
  ElimModal φ p p' (|==> 𝓟) 𝓟' 𝓠 𝓠' 
  ElimModal φ p p' ((|==> P) i) 𝓟' 𝓠 𝓠'.
377
Proof. by rewrite /MakeMonPredAt /ElimModal monPred_at_bupd=><-. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
378
379
380
381

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

384
(* When P and/or Q are evars when doing typeclass search on [IntoWand
385
   (R i) P Q], we use [MakeMonPredAt] in order to normalize the
386
387
   result of unification. However, when they are not evars, we want to
   propagate the known information through typeclass search. Hence, we
388
   do not want to use [MakeMonPredAt].
389
390

   As a result, depending on P and Q being evars, we use a different
391
392
   version of [into_wand_monPred_at_xx_xx]. *)
Hint Extern 3 (IntoWand _ _ (monPred_at _ _) ?P ?Q) =>
393
     is_evar P; is_evar Q;
394
     eapply @into_wand_monPred_at_unknown_unknown
395
     : typeclass_instances.
396
397
Hint Extern 2 (IntoWand _ _ (monPred_at _ _) ?P (monPred_at ?Q _)) =>
     eapply @into_wand_monPred_at_unknown_known
398
     : typeclass_instances.
399
400
Hint Extern 2 (IntoWand _ _ (monPred_at _ _) (monPred_at ?P _) ?Q) =>
     eapply @into_wand_monPred_at_known_unknown_le
401
     : typeclass_instances.
402
403
Hint Extern 2 (IntoWand _ _ (monPred_at _ _) (monPred_at ?P _) ?Q) =>
     eapply @into_wand_monPred_at_known_unknown_ge
404
     : typeclass_instances.
405

406
Section sbi.
407
Context {I : biIndex} {PROP : sbi}.
408
409
Local Notation monPred := (monPred I PROP).
Implicit Types P Q R : monPred.
410
Implicit Types 𝓟 𝓠 𝓡 : PROP.
411
412
413
Implicit Types φ : Prop.
Implicit Types i j : I.

Robbert Krebbers's avatar
Robbert Krebbers committed
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
Global Instance from_forall_monPred_at_plainly `{BiPlainly PROP} i P Φ :
  ( i, MakeMonPredAt i P (Φ i)) 
  FromForall (( P) i) (λ j,  (Φ j))%I.
Proof.
  rewrite /FromForall /MakeMonPredAt=>HPΦ. rewrite monPred_at_plainly.
  by setoid_rewrite HPΦ.
Qed.
Global Instance into_forall_monPred_at_plainly `{BiPlainly PROP} i P Φ :
  ( i, MakeMonPredAt i P (Φ i)) 
  IntoForall (( P) i) (λ j,  (Φ j))%I.
Proof.
  rewrite /IntoForall /MakeMonPredAt=>HPΦ. rewrite monPred_at_plainly.
  by setoid_rewrite HPΦ.
Qed.

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.
Robbert Krebbers's avatar
Robbert Krebbers committed
445
Global Instance make_monPred_at_fupd `{BiFUpd PROP} i E1 E2 P 𝓟 :
446
  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
Global Instance maybe_into_later_monPred_at i n P Q 𝓠 :
461
462
  IntoLaterN false n P Q  MakeMonPredAt i Q 𝓠 
  IntoLaterN false n (P i) 𝓠.
463
Proof.
464
  rewrite /IntoLaterN /MaybeIntoLaterN /MakeMonPredAt=> -> <-. elim n=>//= ? <-.
465
  by rewrite monPred_at_later.
466
Qed.
467
468
469
Global Instance from_later_monPred_at i `(sel : A) n P Q 𝓠 :
  FromModal (modality_laterN n) sel P Q  MakeMonPredAt i Q 𝓠 
  FromModal (modality_laterN n) sel (P i) 𝓠.
470
Proof.
471
  rewrite /FromModal /MakeMonPredAt=> <- <-. elim n=>//= ? ->.
472
473
  by rewrite monPred_at_later.
Qed.
474

475
476
477
Global Instance elim_modal_at_fupd_goal `{BiFUpd PROP} φ p p' E1 E2 E3 𝓟 𝓟' Q Q' i :
  ElimModal φ p p' 𝓟 𝓟' (|={E1,E3}=> Q i) (|={E2,E3}=> Q' i) 
  ElimModal φ p p' 𝓟 𝓟' ((|={E1,E3}=> Q) i) ((|={E2,E3}=> Q') i).
478
Proof. by rewrite /ElimModal !monPred_at_fupd. Qed.
479
Global Instance elim_modal_at_fupd_hyp `{BiFUpd PROP} φ p p' E1 E2 P 𝓟 𝓟' 𝓠 𝓠' i :
480
  MakeMonPredAt i P 𝓟 
481
482
  ElimModal φ p p' (|={E1,E2}=> 𝓟) 𝓟' 𝓠 𝓠' 
  ElimModal φ p p' ((|={E1,E2}=> P) i) 𝓟' 𝓠 𝓠'.
483
Proof. by rewrite /MakeMonPredAt /ElimModal monPred_at_fupd=><-. Qed.
484

Robbert Krebbers's avatar
Robbert Krebbers committed
485
Global Instance add_modal_at_fupd_goal `{BiFUpd PROP} E1 E2 𝓟 𝓟' Q i :
486
  AddModal 𝓟 𝓟' (|={E1,E2}=> Q i)  AddModal 𝓟 𝓟' ((|={E1,E2}=> Q) i).
487
Proof. by rewrite /AddModal !monPred_at_fupd. Qed.
488
489
490
491
492
493
494
495
496

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.
497
End sbi.