monpred.v 29.4 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
19
20
21
22
23
24
25
(** Frame [𝓡] into the goal [monPred_at P i] and determine the remainder [𝓠].
    Used when framing encounters a monPred_at in the goal. *)
Class FrameMonPredAt {I : biIndex} {PROP : bi} (p : bool) (i : I)
      (𝓡 : PROP) (P : monPred I PROP) (𝓠 : PROP) :=
  frame_monPred_at : ?p 𝓡  𝓠 - P i.
Arguments FrameMonPredAt {_ _} _ _ _%I _%I _%I.
Hint Mode FrameMonPredAt + + + + ! ! - : typeclass_instances.

26
Section modalities.
27
  Context {I : biIndex} {PROP : bi}.
28

29
30
31
  Lemma modality_objectively_mixin :
    modality_mixin (@monPred_objectively I PROP)
      (MIEnvFilter Objective) (MIEnvFilter Objective).
32
  Proof.
33
34
    split; simpl; split_and?; intros;
      try match goal with H : TCDiag _ _ _ |- _ => destruct H end;
35
36
37
      eauto using bi.equiv_entails_sym, objective_objectively,
        monPred_objectively_mono, monPred_objectively_and,
        monPred_objectively_sep_2 with typeclass_instances.
38
  Qed.
39
40
  Definition modality_objectively :=
    Modality _ modality_objectively_mixin.
41
End modalities.
42

43
Section bi.
44
Context {I : biIndex} {PROP : bi}.
Robbert Krebbers's avatar
Robbert Krebbers committed
45
Local Notation monPredI := (monPredI I PROP).
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
Global Instance from_modal_objectively P :
Robbert Krebbers's avatar
Robbert Krebbers committed
54
  FromModal modality_objectively (<obj> P) (<obj> P) P | 1.
55
Proof. by rewrite /FromModal. Qed.
56
Global Instance from_modal_subjectively P :
Robbert Krebbers's avatar
Robbert Krebbers committed
57
  FromModal modality_id (<subj> P) (<subj> P) P | 1.
58
Proof. by rewrite /FromModal /= -monPred_subjectively_intro. Qed.
59

60
61
62
63
64
65
66
67
68
69
70
71
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.
72
Global Instance from_modal_intuitionistically_monPred_at `(sel : A) P Q 𝓠 i :
73
74
  FromModal modality_intuitionistically sel P Q  MakeMonPredAt i Q 𝓠 
  FromModal modality_intuitionistically sel (P i) 𝓠 | 0.
75
76
77
78
79
80
81
82
83
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.

84
Global Instance make_monPred_at_pure φ i : MakeMonPredAt i ⌜φ⌝ ⌜φ⌝.
85
Proof. by rewrite /MakeMonPredAt monPred_at_pure. Qed.
86
Global Instance make_monPred_at_emp i : MakeMonPredAt i emp emp.
87
Proof. by rewrite /MakeMonPredAt monPred_at_emp. Qed.
88
89
90
Global Instance make_monPred_at_sep i P 𝓟 Q 𝓠 :
  MakeMonPredAt i P 𝓟  MakeMonPredAt i Q 𝓠 
  MakeMonPredAt i (P  Q) (𝓟  𝓠).
91
Proof. by rewrite /MakeMonPredAt monPred_at_sep=><-<-. Qed.
92
93
94
Global Instance make_monPred_at_and i P 𝓟 Q 𝓠 :
  MakeMonPredAt i P 𝓟  MakeMonPredAt i Q 𝓠 
  MakeMonPredAt i (P  Q) (𝓟  𝓠).
95
Proof. by rewrite /MakeMonPredAt monPred_at_and=><-<-. Qed.
96
97
98
Global Instance make_monPred_at_or i P 𝓟 Q 𝓠 :
  MakeMonPredAt i P 𝓟  MakeMonPredAt i Q 𝓠 
  MakeMonPredAt i (P  Q) (𝓟  𝓠).
99
Proof. by rewrite /MakeMonPredAt monPred_at_or=><-<-. Qed.
100
101
Global Instance make_monPred_at_forall {A} i (Φ : A  monPred) (Ψ : A  PROP) :
  ( a, MakeMonPredAt i (Φ a) (Ψ a))  MakeMonPredAt i ( a, Φ a) ( a, Ψ a).
102
Proof. rewrite /MakeMonPredAt monPred_at_forall=>H. by setoid_rewrite <- H. Qed.
103
104
Global Instance make_monPred_at_exists {A} i (Φ : A  monPred) (Ψ : A  PROP) :
  ( a, MakeMonPredAt i (Φ a) (Ψ a))  MakeMonPredAt i ( a, Φ a) ( a, Ψ a).
105
Proof. rewrite /MakeMonPredAt monPred_at_exist=>H. by setoid_rewrite <- H. Qed.
106
Global Instance make_monPred_at_persistently i P 𝓟 :
107
  MakeMonPredAt i P 𝓟  MakeMonPredAt i (<pers> P) (<pers> 𝓟).
108
Proof. by rewrite /MakeMonPredAt monPred_at_persistently=><-. Qed.
109
Global Instance make_monPred_at_affinely i P 𝓟 :
110
  MakeMonPredAt i P 𝓟  MakeMonPredAt i (<affine> P) (<affine> 𝓟).
111
Proof. by rewrite /MakeMonPredAt monPred_at_affinely=><-. Qed.
112
113
114
Global Instance make_monPred_at_intuitionistically i P 𝓟 :
  MakeMonPredAt i P 𝓟  MakeMonPredAt i ( P) ( 𝓟).
Proof. by rewrite /MakeMonPredAt monPred_at_intuitionistically=><-. Qed.
115
Global Instance make_monPred_at_absorbingly i P 𝓟 :
116
  MakeMonPredAt i P 𝓟  MakeMonPredAt i (<absorb> P) (<absorb> 𝓟).
117
Proof. by rewrite /MakeMonPredAt monPred_at_absorbingly=><-. Qed.
118
119
Global Instance make_monPred_at_persistently_if i P 𝓟 p :
  MakeMonPredAt i P 𝓟 
120
  MakeMonPredAt i (<pers>?p P) (<pers>?p 𝓟).
121
Proof. destruct p; simpl; apply _. Qed.
122
123
Global Instance make_monPred_at_affinely_if i P 𝓟 p :
  MakeMonPredAt i P 𝓟 
124
  MakeMonPredAt i (<affine>?p P) (<affine>?p 𝓟).
125
Proof. destruct p; simpl; apply _. Qed.
126
127
128
129
Global Instance make_monPred_at_intuitionistically_if i P 𝓟 p :
  MakeMonPredAt i P 𝓟 
  MakeMonPredAt i (?p P) (?p 𝓟).
Proof. destruct p; simpl; apply _. Qed.
130
131
Global Instance make_monPred_at_embed i 𝓟 : MakeMonPredAt i ⎡𝓟⎤ 𝓟.
Proof. by rewrite /MakeMonPredAt monPred_at_embed. Qed.
132
Global Instance make_monPred_at_in i j : MakeMonPredAt j (monPred_in i) i  j.
133
Proof. by rewrite /MakeMonPredAt monPred_at_in. Qed.
134
135
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
136
137
138
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.
139

140
Global Instance from_assumption_make_monPred_at_l p i j P 𝓟 :
141
  MakeMonPredAt i P 𝓟  IsBiIndexRel j i  KnownLFromAssumption p (P j) 𝓟.
142
Proof.
143
  rewrite /MakeMonPredAt /KnownLFromAssumption /FromAssumption /IsBiIndexRel=><- ->.
144
  apply  bi.intuitionistically_if_elim.
145
Qed.
146
Global Instance from_assumption_make_monPred_at_r p i j P 𝓟 :
147
  MakeMonPredAt i P 𝓟  IsBiIndexRel i j  KnownRFromAssumption p 𝓟 (P j).
148
Proof.
149
  rewrite /MakeMonPredAt /KnownRFromAssumption /FromAssumption /IsBiIndexRel=><- ->.
150
  apply  bi.intuitionistically_if_elim.
151
152
Qed.

153
Global Instance from_assumption_make_monPred_objectively P Q :
154
  FromAssumption p P Q  KnownLFromAssumption p (<obj> P) Q.
155
156
Proof.
  intros ?.
157
  by rewrite /KnownLFromAssumption /FromAssumption monPred_objectively_elim.
158
Qed.
159
Global Instance from_assumption_make_monPred_subjectively P Q :
160
  FromAssumption p P Q  KnownRFromAssumption p P (<subj> Q).
161
162
Proof.
  intros ?.
163
  by rewrite /KnownRFromAssumption /FromAssumption -monPred_subjectively_intro.
164
Qed.
165

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

195
196
Global Instance into_pure_monPred_at P φ i : IntoPure P φ  IntoPure (P i) φ.
Proof. rewrite /IntoPure=>->. by rewrite monPred_at_pure. Qed.
197
198
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.
199
200
Global Instance into_pure_monPred_in i j : @IntoPure PROP (monPred_in i j) (i  j).
Proof. by rewrite /IntoPure monPred_at_in. Qed.
201
202
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.
203

204
205
Global Instance into_persistent_monPred_at p P Q 𝓠 i :
  IntoPersistent p P Q  MakeMonPredAt i Q 𝓠  IntoPersistent p (P i) 𝓠 | 0.
206
Proof.
207
208
  rewrite /IntoPersistent /MakeMonPredAt  =>-[/(_ i) ?] <-.
  by rewrite -monPred_at_persistently -monPred_at_persistently_if.
209
Qed.
210

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

241
242
243
244
245
246
247
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.

248
249
Global Instance from_forall_monPred_at_wand P Q (Φ Ψ : I  PROP) i :
  ( j, MakeMonPredAt j P (Φ j))  ( j, MakeMonPredAt j Q (Ψ j)) 
250
251
  FromForall ((P - Q) i)%I (λ j, i  j  Φ j - Ψ j)%I.
Proof.
252
  rewrite /FromForall /MakeMonPredAt monPred_at_wand=> H1 H2. do 2 f_equiv.
253
  by rewrite H1 H2.
254
Qed.
255
256
Global Instance from_forall_monPred_at_impl P Q (Φ Ψ : I  PROP) i :
  ( j, MakeMonPredAt j P (Φ j))  ( j, MakeMonPredAt j Q (Ψ j)) 
257
258
  FromForall ((P  Q) i)%I (λ j, i  j  Φ j  Ψ j)%I.
Proof.
259
  rewrite /FromForall /MakeMonPredAt monPred_at_impl=> H1 H2. do 2 f_equiv.
260
  by rewrite H1 H2 bi.pure_impl_forall.
261
262
Qed.

263
Global Instance into_forall_monPred_at_index P i :
264
265
266
267
268
  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.
269

270
271
Global Instance from_and_monPred_at P Q1 𝓠1 Q2 𝓠2 i :
  FromAnd P Q1 Q2  MakeMonPredAt i Q1 𝓠1  MakeMonPredAt i Q2 𝓠2 
272
  FromAnd (P i) 𝓠1 𝓠2.
273
274
275
276
Proof.
  rewrite /FromAnd /MakeMonPredAt /MakeMonPredAt=> <- <- <-.
  by rewrite monPred_at_and.
Qed.
277
278
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 
279
  IntoAnd p (P i) 𝓠1 𝓠2.
280
Proof.
281
  rewrite /IntoAnd /MakeMonPredAt /bi_affinely_if /bi_persistently_if.
282
283
  destruct p=>-[/(_ i) H] <- <-; revert H;
  by rewrite ?monPred_at_affinely ?monPred_at_persistently monPred_at_and.
284
285
Qed.

286
287
Global Instance from_sep_monPred_at P Q1 𝓠1 Q2 𝓠2 i :
  FromSep P Q1 Q2  MakeMonPredAt i Q1 𝓠1  MakeMonPredAt i Q2 𝓠2 
288
  FromSep (P i) 𝓠1 𝓠2.
289
Proof. rewrite /FromSep /MakeMonPredAt=> <- <- <-. by rewrite monPred_at_sep. Qed.
290
291
Global Instance into_sep_monPred_at P Q1 𝓠1 Q2 𝓠2 i :
  IntoSep P Q1 Q2  MakeMonPredAt i Q1 𝓠1  MakeMonPredAt i Q2 𝓠2 
292
  IntoSep (P i) 𝓠1 𝓠2.
293
Proof. rewrite /IntoSep /MakeMonPredAt=> -> <- <-. by rewrite monPred_at_sep. Qed.
294
295
Global Instance from_or_monPred_at P Q1 𝓠1 Q2 𝓠2 i :
  FromOr P Q1 Q2  MakeMonPredAt i Q1 𝓠1  MakeMonPredAt i Q2 𝓠2 
296
  FromOr (P i) 𝓠1 𝓠2.
297
Proof. rewrite /FromOr /MakeMonPredAt=> <- <- <-. by rewrite monPred_at_or. Qed.
298
299
Global Instance into_or_monPred_at P Q1 𝓠1 Q2 𝓠2 i :
  IntoOr P Q1 Q2  MakeMonPredAt i Q1 𝓠1  MakeMonPredAt i Q2 𝓠2 
300
  IntoOr (P i) 𝓠1 𝓠2.
301
Proof. rewrite /IntoOr /MakeMonPredAt=> -> <- <-. by rewrite monPred_at_or. Qed.
302

303
304
Global Instance from_exist_monPred_at {A} P (Φ : A  monPred) (Ψ : A  PROP) i :
  FromExist P Φ  ( a, MakeMonPredAt i (Φ a) (Ψ a))  FromExist (P i) Ψ.
305
Proof.
306
307
  rewrite /FromExist /MakeMonPredAt=><- H. setoid_rewrite <- H.
  by rewrite monPred_at_exist.
308
Qed.
309
310
Global Instance into_exist_monPred_at {A} P (Φ : A  monPred) (Ψ : A  PROP) i :
  IntoExist P Φ  ( a, MakeMonPredAt i (Φ a) (Ψ a))  IntoExist (P i) Ψ.
311
Proof.
312
313
  rewrite /IntoExist /MakeMonPredAt=>-> H. setoid_rewrite <- H.
  by rewrite monPred_at_exist.
314
315
Qed.

316
Global Instance from_forall_monPred_at_objectively P (Φ : I  PROP) i :
Robbert Krebbers's avatar
Robbert Krebbers committed
317
  ( i, MakeMonPredAt i P (Φ i))  FromForall ((<obj> P) i)%I Φ.
318
Proof.
319
  rewrite /FromForall /MakeMonPredAt monPred_at_objectively=>H. by setoid_rewrite <- H.
320
Qed.
321
Global Instance into_forall_monPred_at_objectively P (Φ : I  PROP) i :
Robbert Krebbers's avatar
Robbert Krebbers committed
322
  ( i, MakeMonPredAt i P (Φ i))  IntoForall ((<obj> P) i) Φ.
323
Proof.
324
  rewrite /IntoForall /MakeMonPredAt monPred_at_objectively=>H. by setoid_rewrite <- H.
325
Qed.
326

327
Global Instance from_exist_monPred_at_ex P (Φ : I  PROP) i :
Robbert Krebbers's avatar
Robbert Krebbers committed
328
  ( i, MakeMonPredAt i P (Φ i))  FromExist ((<subj> P) i) Φ.
329
Proof.
330
  rewrite /FromExist /MakeMonPredAt monPred_at_subjectively=>H. by setoid_rewrite <- H.
331
332
Qed.
Global Instance into_exist_monPred_at_ex P (Φ : I  PROP) i :
Robbert Krebbers's avatar
Robbert Krebbers committed
333
  ( i, MakeMonPredAt i P (Φ i))  IntoExist ((<subj> P) i) Φ.
334
Proof.
335
  rewrite /IntoExist /MakeMonPredAt monPred_at_subjectively=>H. by setoid_rewrite <- H.
336
337
Qed.

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

351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
(* Framing. *)
Global Instance frame_monPred_at_enter p i 𝓡 P 𝓠 :
  FrameMonPredAt p i 𝓡 P 𝓠  Frame p 𝓡 (P i) 𝓠.
Proof. intros. done. Qed.
Global Instance frame_monPred_at_here p P i j :
  IsBiIndexRel i j  FrameMonPredAt p j (P i) P emp | 0.
Proof.
  rewrite /FrameMonPredAt /IsBiIndexRel right_id bi.intuitionistically_if_elim=> -> //.
Qed.

Global Instance frame_monPred_at_embed p 𝓡 𝓠 𝓟 i :
  Frame p 𝓡 𝓟 𝓠  FrameMonPredAt p i 𝓡 (embed (B:=monPredI) 𝓟) 𝓠.
Proof. rewrite /Frame /FrameMonPredAt=> ->. by rewrite monPred_at_embed. Qed.
Global Instance frame_monPred_at_sep p P Q 𝓡 𝓠 i :
  Frame p 𝓡 (P i  Q i) 𝓠  FrameMonPredAt p i 𝓡 (P  Q) 𝓠.
Proof. rewrite /Frame /FrameMonPredAt=> ->. by rewrite monPred_at_sep. Qed.
Global Instance frame_monPred_at_and p P Q 𝓡 𝓠 i :
  Frame p 𝓡 (P i  Q i) 𝓠  FrameMonPredAt p i 𝓡 (P  Q) 𝓠.
Proof. rewrite /Frame /FrameMonPredAt=> ->. by rewrite monPred_at_and. Qed.
Global Instance frame_monPred_at_or p P Q 𝓡 𝓠 i :
  Frame p 𝓡 (P i  Q i) 𝓠  FrameMonPredAt p i 𝓡 (P  Q) 𝓠.
Proof. rewrite /Frame /FrameMonPredAt=> ->. by rewrite monPred_at_or. Qed.
Global Instance frame_monPred_at_wand p P R Q1 Q2 i :
  Frame p R Q1 Q2  FrameMonPredAt p i (R i) (P - Q1) ((P - Q2) i).
Proof.
  rewrite /Frame /FrameMonPredAt=>Hframe.
  rewrite -monPred_at_intuitionistically_if -monPred_at_sep. apply monPred_in_entails.
  change ((?p R  (P - Q2)) - P - Q1). apply bi.wand_intro_r.
  rewrite -assoc bi.wand_elim_l. done.
Qed.
Global Instance frame_monPred_at_impl P R Q1 Q2 i :
  Frame true R Q1 Q2  FrameMonPredAt true i (R i) (P  Q1) ((P  Q2) i).
Proof.
  rewrite /Frame /FrameMonPredAt=>Hframe.
  rewrite -monPred_at_intuitionistically_if -monPred_at_sep. apply monPred_in_entails.
  change (( R  (P  Q2)) - P  Q1).
  rewrite -bi.persistently_and_intuitionistically_sep_l. apply bi.impl_intro_r.
  rewrite -assoc bi.impl_elim_l bi.persistently_and_intuitionistically_sep_l. done.
Qed.
Global Instance frame_monPred_at_forall {X : Type} p (Ψ : X  monPred) 𝓡 𝓠 i :
  Frame p 𝓡 ( x, Ψ x i) 𝓠  FrameMonPredAt p i 𝓡 ( x, Ψ x) 𝓠.
Proof. rewrite /Frame /FrameMonPredAt=> ->. by rewrite monPred_at_forall. Qed.
Global Instance frame_monPred_at_exist {X : Type} p (Ψ : X  monPred) 𝓡 𝓠 i :
  Frame p 𝓡 ( x, Ψ x i) 𝓠  FrameMonPredAt p i 𝓡 ( x, Ψ x) 𝓠.
Proof. rewrite /Frame /FrameMonPredAt=> ->. by rewrite monPred_at_exist. Qed.

Global Instance frame_monPred_at_absorbingly p P 𝓡 𝓠 i :
  Frame p 𝓡 (<absorb> P i) 𝓠  FrameMonPredAt p i 𝓡 (<absorb> P) 𝓠.
Proof. rewrite /Frame /FrameMonPredAt=> ->. by rewrite monPred_at_absorbingly. Qed.
Global Instance frame_monPred_at_affinely p P 𝓡 𝓠 i :
  Frame p 𝓡 (<affine> P i) 𝓠  FrameMonPredAt p i 𝓡 (<affine> P) 𝓠.
Proof. rewrite /Frame /FrameMonPredAt=> ->. by rewrite monPred_at_affinely. Qed.
Global Instance frame_monPred_at_persistently p P 𝓡 𝓠 i :
  Frame p 𝓡 (<pers> P i) 𝓠  FrameMonPredAt p i 𝓡 (<pers> P) 𝓠.
Proof. rewrite /Frame /FrameMonPredAt=> ->. by rewrite monPred_at_persistently. Qed.
Global Instance frame_monPred_at_intuitionistically p P 𝓡 𝓠 i :
  Frame p 𝓡 ( P i) 𝓠  FrameMonPredAt p i 𝓡 ( P) 𝓠.
Proof. rewrite /Frame /FrameMonPredAt=> ->. by rewrite monPred_at_intuitionistically. Qed.
Global Instance frame_monPred_at_objectively p P 𝓡 𝓠 i :
  Frame p 𝓡 ( i, P i) 𝓠  FrameMonPredAt p i 𝓡 (<obj> P) 𝓠.
Proof. rewrite /Frame /FrameMonPredAt=> ->. by rewrite monPred_at_objectively. Qed.
Global Instance frame_monPred_at_subjectively p P 𝓡 𝓠 i :
  Frame p 𝓡 ( i, P i) 𝓠  FrameMonPredAt p i 𝓡 (<subj> P) 𝓠.
Proof. rewrite /Frame /FrameMonPredAt=> ->. by rewrite monPred_at_subjectively. Qed.
Global Instance frame_monPred_at_bupd `{BiBUpd PROP} p P 𝓡 𝓠 i :
  Frame p 𝓡 (|==> P i) 𝓠  FrameMonPredAt p i 𝓡 (|==> P) 𝓠.
Proof. rewrite /Frame /FrameMonPredAt=> ->. by rewrite monPred_at_bupd. Qed.
418

419
420
Global Instance into_embed_objective P :
  Objective P  IntoEmbed P ( i, P i).
421
422
Proof.
  rewrite /IntoEmbed=> ?.
423
  by rewrite {1}(objective_objectively P) monPred_objectively_unfold.
424
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
425

426
427
428
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
429
Proof. by rewrite /ElimModal !monPred_at_bupd. Qed.
430
Global Instance elim_modal_at_bupd_hyp `{BiBUpd PROP} φ p p' P 𝓟 𝓟' 𝓠 𝓠' i:
431
  MakeMonPredAt i P 𝓟 
432
433
  ElimModal φ p p' (|==> 𝓟) 𝓟' 𝓠 𝓠' 
  ElimModal φ p p' ((|==> P) i) 𝓟' 𝓠 𝓠'.
434
Proof. by rewrite /MakeMonPredAt /ElimModal monPred_at_bupd=><-. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
435
436
437
438

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.
439
440
End bi.

441
(* When P and/or Q are evars when doing typeclass search on [IntoWand
442
   (R i) P Q], we use [MakeMonPredAt] in order to normalize the
443
444
   result of unification. However, when they are not evars, we want to
   propagate the known information through typeclass search. Hence, we
445
   do not want to use [MakeMonPredAt].
446
447

   As a result, depending on P and Q being evars, we use a different
448
449
   version of [into_wand_monPred_at_xx_xx]. *)
Hint Extern 3 (IntoWand _ _ (monPred_at _ _) ?P ?Q) =>
450
     is_evar P; is_evar Q;
451
     eapply @into_wand_monPred_at_unknown_unknown
452
     : typeclass_instances.
453
454
Hint Extern 2 (IntoWand _ _ (monPred_at _ _) ?P (monPred_at ?Q _)) =>
     eapply @into_wand_monPred_at_unknown_known
455
     : typeclass_instances.
456
457
Hint Extern 2 (IntoWand _ _ (monPred_at _ _) (monPred_at ?P _) ?Q) =>
     eapply @into_wand_monPred_at_known_unknown_le
458
     : typeclass_instances.
459
460
Hint Extern 2 (IntoWand _ _ (monPred_at _ _) (monPred_at ?P _) ?Q) =>
     eapply @into_wand_monPred_at_known_unknown_ge
461
     : typeclass_instances.
462

463
Section sbi.
464
Context {I : biIndex} {PROP : sbi}.
465
466
Local Notation monPred := (monPred I PROP).
Implicit Types P Q R : monPred.
467
Implicit Types 𝓟 𝓠 𝓡 : PROP.
468
469
470
Implicit Types φ : Prop.
Implicit Types i j : I.

Robbert Krebbers's avatar
Robbert Krebbers committed
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
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.

486
Global Instance is_except_0_monPred_at i P :
487
  IsExcept0 P  IsExcept0 (P i).
488
Proof. rewrite /IsExcept0=>- [/(_ i)]. by rewrite monPred_at_except_0. Qed.
489

490
491
492
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.
493
494
Global Instance make_monPred_at_except_0 i P 𝓠 :
  MakeMonPredAt i P 𝓠  MakeMonPredAt i ( P)%I ( 𝓠)%I.
495
Proof. by rewrite /MakeMonPredAt monPred_at_except_0=><-. Qed.
496
497
Global Instance make_monPred_at_later i P 𝓠 :
  MakeMonPredAt i P 𝓠  MakeMonPredAt i ( P)%I ( 𝓠)%I.
498
Proof. by rewrite /MakeMonPredAt monPred_at_later=><-. Qed.
499
500
Global Instance make_monPred_at_laterN i n P 𝓠 :
  MakeMonPredAt i P 𝓠  MakeMonPredAt i (^n P)%I (^n 𝓠)%I.
501
Proof. rewrite /MakeMonPredAt=> <-. elim n=>//= ? <-. by rewrite monPred_at_later. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
502
Global Instance make_monPred_at_fupd `{BiFUpd PROP} i E1 E2 P 𝓟 :
503
  MakeMonPredAt i P 𝓟  MakeMonPredAt i (|={E1,E2}=> P)%I (|={E1,E2}=> 𝓟)%I.
504
Proof. by rewrite /MakeMonPredAt monPred_at_fupd=> <-. Qed.
505

506
507
508
509
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.

510
511
Global Instance into_except_0_monPred_at_fwd i P Q 𝓠 :
  IntoExcept0 P Q  MakeMonPredAt i Q 𝓠  IntoExcept0 (P i) 𝓠.
512
Proof. rewrite /IntoExcept0 /MakeMonPredAt=> -> <-. by rewrite monPred_at_except_0. Qed.
513
514
Global Instance into_except_0_monPred_at_bwd i P 𝓟 Q :
  IntoExcept0 P Q  MakeMonPredAt i P 𝓟  IntoExcept0 𝓟 (Q i).
515
Proof. rewrite /IntoExcept0 /MakeMonPredAt=> H <-. by rewrite H monPred_at_except_0. Qed.
516

517
Global Instance maybe_into_later_monPred_at i n P Q 𝓠 :
518
519
  IntoLaterN false n P Q  MakeMonPredAt i Q 𝓠 
  IntoLaterN false n (P i) 𝓠.
520
Proof.
521
  rewrite /IntoLaterN /MaybeIntoLaterN /MakeMonPredAt=> -> <-. elim n=>//= ? <-.
522
  by rewrite monPred_at_later.
523
Qed.
524
525
526
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) 𝓠.
527
Proof.
528
  rewrite /FromModal /MakeMonPredAt=> <- <-. elim n=>//= ? ->.
529
530
  by rewrite monPred_at_later.
Qed.
531

532
533
534
535
536
537
538
539
540
541
Global Instance frame_monPred_at_later p P 𝓡 𝓠 i :
  Frame p 𝓡 ( P i) 𝓠  FrameMonPredAt p i 𝓡 ( P) 𝓠.
Proof. rewrite /Frame /FrameMonPredAt=> ->. by rewrite monPred_at_later. Qed.
Global Instance frame_monPred_at_laterN p n P 𝓡 𝓠 i :
  Frame p 𝓡 (^n P i) 𝓠  FrameMonPredAt p i 𝓡 (^n P) 𝓠.
Proof. rewrite /Frame /FrameMonPredAt=> ->. by rewrite monPred_at_laterN. Qed.
Global Instance frame_monPred_at_fupd `{BiFUpd PROP} E1 E2 p P 𝓡 𝓠 i :
  Frame p 𝓡 (|={E1,E2}=> P i) 𝓠  FrameMonPredAt p i 𝓡 (|={E1,E2}=> P) 𝓠.
Proof. rewrite /Frame /FrameMonPredAt=> ->. by rewrite monPred_at_fupd. Qed.

542
543
544
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).
545
Proof. by rewrite /ElimModal !monPred_at_fupd. Qed.
546
Global Instance elim_modal_at_fupd_hyp `{BiFUpd PROP} φ p p' E1 E2 P 𝓟 𝓟' 𝓠 𝓠' i :
547
  MakeMonPredAt i P 𝓟 
548
549
  ElimModal φ p p' (|={E1,E2}=> 𝓟) 𝓟' 𝓠 𝓠' 
  ElimModal φ p p' ((|={E1,E2}=> P) i) 𝓟' 𝓠 𝓠'.
550
Proof. by rewrite /MakeMonPredAt /ElimModal monPred_at_fupd=><-. Qed.
551

Ralf Jung's avatar
Ralf Jung committed
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
(* This instances are awfully specific, but that's what is needed. *)
Global Instance elim_acc_at_fupd `{BiFUpd PROP} {X : Type} E1 E2 E
       M1 M2 α β mγ Q (Q' : X  monPred) i :
  ElimAcc (X:=X) M1 M2 α β mγ (|={E1,E}=> Q i)
          (λ x, |={E2}=> β x  (coq_tactics.maybe_wand (mγ x) (|={E1,E}=> Q' x i)))%I 
  ElimAcc (X:=X) M1 M2 α β mγ ((|={E1,E}=> Q) i)
          (λ x, (|={E2}=> ⎡β x 
                         (coq_tactics.maybe_wand
                            (match mγ x with Some 𝓟 => Some ⎡𝓟⎤ | None => None end)
                            (|={E1,E}=> Q' x))) i)%I
  | 1.
Proof.
  rewrite /ElimAcc monPred_at_fupd=><-. apply bi.forall_mono=>x.
  destruct (mγ x); simpl.
  - rewrite monPred_at_fupd monPred_at_sep monPred_wand_force monPred_at_fupd !monPred_at_embed //.
  - rewrite monPred_at_fupd monPred_at_sep monPred_at_fupd !monPred_at_embed //.
Qed.
(* A separate, higher-priority instance for unit because otherwise unification
fails. *)
Global Instance elim_acc_at_fupd_unit `{BiFUpd PROP} E1 E2 E
       M1 M2 α β mγ Q Q' i :
  ElimAcc (X:=unit) M1 M2 α β mγ (|={E1,E}=> Q i)
          (λ x, |={E2}=> β x  (coq_tactics.maybe_wand (mγ x) (|={E1,E}=> Q' i)))%I 
  ElimAcc (X:=unit) M1 M2 α β mγ ((|={E1,E}=> Q) i)
          (λ x, (|={E2}=> ⎡β x 
                         (coq_tactics.maybe_wand
                            (match mγ x with Some 𝓟 => Some ⎡𝓟⎤ | None => None end)
                            (|={E1,E}=> Q'))) i)%I
  | 0.
Proof. exact: elim_acc_at_fupd. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
583
Global Instance add_modal_at_fupd_goal `{BiFUpd PROP} E1 E2 𝓟 𝓟' Q i :
584
  AddModal 𝓟 𝓟' (|={E1,E2}=> Q i)  AddModal 𝓟 𝓟' ((|={E1,E2}=> Q) i).
585
Proof. by rewrite /AddModal !monPred_at_fupd. Qed.
586

Ralf Jung's avatar
Ralf Jung committed
587
588
(* This hard-codes the fact that ElimInv with_close returns a
   [(λ _, ...)] as Q'. *)
589
590
591
Global Instance elim_inv_embed_with_close {X : Type} φ
       𝓟inv 𝓟in (𝓟out 𝓟close : X  PROP)
       Pin (Pout Pclose : X  monPred)
Ralf Jung's avatar
Ralf Jung committed
592
593
       Q Q' :
  ( i, ElimInv φ 𝓟inv 𝓟in 𝓟out (Some 𝓟close) (Q i) (λ _, Q' i)) 
594
595
  MakeEmbed 𝓟in Pin  ( x, MakeEmbed (𝓟out x) (Pout x)) 
  ( x, MakeEmbed (𝓟close x) (Pclose x)) 
Ralf Jung's avatar
Ralf Jung committed
596
  ElimInv (X:=X) φ ⎡𝓟inv Pin Pout (Some Pclose) Q (λ _, Q').
597
598
599
600
601
602
603
604
605
606
607
608
609
610
Proof.
  rewrite /MakeEmbed /ElimInv=>H <- Hout Hclose ?. iStartProof PROP.
  setoid_rewrite <-Hout. setoid_rewrite <-Hclose.
  iIntros (?) "(?&?&HQ')". iApply H; [done|]. iFrame. iIntros (x) "?". by iApply "HQ'".
Qed.
Global Instance elim_inv_embed_without_close  {X : Type}
       φ 𝓟inv 𝓟in (𝓟out : X  PROP) Pin (Pout : X  monPred) Q (Q' : X  monPred) :
  ( i, ElimInv φ 𝓟inv 𝓟in 𝓟out None (Q i) (λ x, Q' x i)) 
  MakeEmbed 𝓟in Pin  ( x, MakeEmbed (𝓟out x) (Pout x)) 
  ElimInv (X:=X) φ ⎡𝓟inv Pin Pout None Q Q'.
Proof.
  rewrite /MakeEmbed /ElimInv=>H <-Hout ?. iStartProof PROP.
  setoid_rewrite <-Hout.
  iIntros (?) "(?&?&HQ')". iApply H; [done|]. iFrame. iIntros (x) "?". by iApply "HQ'".
611
Qed.
612

613
End sbi.