monpred.v 30.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
  make_monPred_at : P i  𝓟.
Arguments MakeMonPredAt {_ _} _ _%I _%I.
9 10 11 12
(** Since [MakeMonPredAt] is used by [AsEmpValid] to import lemmas into the
proof mode, the index [I] and BI [PROP] often contain evars. Hence, it is
important to use the mode [!] also for the first two arguments. *)
Hint Mode MakeMonPredAt ! ! - ! - : typeclass_instances.
13

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

21 22 23 24 25 26
(** 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.
27
Hint Mode FrameMonPredAt + + + - ! ! - : typeclass_instances.
28

29
Section modalities.
30
  Context {I : biIndex} {PROP : bi}.
31

32 33 34
  Lemma modality_objectively_mixin :
    modality_mixin (@monPred_objectively I PROP)
      (MIEnvFilter Objective) (MIEnvFilter Objective).
35
  Proof.
36
    split; simpl; split_and?; intros;
Ralf Jung's avatar
Ralf Jung committed
37
      try select (TCDiag _ _ _) (fun H => destruct H);
38 39 40
      eauto using bi.equiv_entails_sym, objective_objectively,
        monPred_objectively_mono, monPred_objectively_and,
        monPred_objectively_sep_2 with typeclass_instances.
41
  Qed.
42 43
  Definition modality_objectively :=
    Modality _ modality_objectively_mixin.
44
End modalities.
45

46
Section bi.
47
Context {I : biIndex} {PROP : bi}.
Robbert Krebbers's avatar
Robbert Krebbers committed
48
Local Notation monPredI := (monPredI I PROP).
49
Local Notation monPred := (monPred I PROP).
50
Local Notation MakeMonPredAt := (@MakeMonPredAt I PROP).
51
Implicit Types P Q R : monPred.
52
Implicit Types 𝓟 𝓠 𝓡 : PROP.
53 54 55
Implicit Types φ : Prop.
Implicit Types i j : I.

56
Global Instance from_modal_objectively P :
Robbert Krebbers's avatar
Robbert Krebbers committed
57
  FromModal modality_objectively (<obj> P) (<obj> P) P | 1.
58
Proof. by rewrite /FromModal. Qed.
59
Global Instance from_modal_subjectively P :
Robbert Krebbers's avatar
Robbert Krebbers committed
60
  FromModal modality_id (<subj> P) (<subj> P) P | 1.
61
Proof. by rewrite /FromModal /= -monPred_subjectively_intro. Qed.
62

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

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

147
Global Instance from_assumption_make_monPred_at_l p i j P 𝓟 :
148
  MakeMonPredAt i P 𝓟  IsBiIndexRel j i  KnownLFromAssumption p (P j) 𝓟.
149
Proof.
150
  rewrite /MakeMonPredAt /KnownLFromAssumption /FromAssumption /IsBiIndexRel=><- ->.
151
  apply  bi.intuitionistically_if_elim.
152
Qed.
153
Global Instance from_assumption_make_monPred_at_r p i j P 𝓟 :
154
  MakeMonPredAt i P 𝓟  IsBiIndexRel i j  KnownRFromAssumption p 𝓟 (P j).
155
Proof.
156
  rewrite /MakeMonPredAt /KnownRFromAssumption /FromAssumption /IsBiIndexRel=><- ->.
157
  apply  bi.intuitionistically_if_elim.
158 159
Qed.

160
Global Instance from_assumption_make_monPred_objectively P Q :
161
  FromAssumption p P Q  KnownLFromAssumption p (<obj> P) Q.
162 163
Proof.
  intros ?.
164
  by rewrite /KnownLFromAssumption /FromAssumption monPred_objectively_elim.
165
Qed.
166
Global Instance from_assumption_make_monPred_subjectively P Q :
167
  FromAssumption p P Q  KnownRFromAssumption p P (<subj> Q).
168 169
Proof.
  intros ?.
170
  by rewrite /KnownRFromAssumption /FromAssumption -monPred_subjectively_intro.
171
Qed.
172

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

202 203
Global Instance into_pure_monPred_at P φ i : IntoPure P φ  IntoPure (P i) φ.
Proof. rewrite /IntoPure=>->. by rewrite monPred_at_pure. Qed.
204 205
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.
206 207
Global Instance into_pure_monPred_in i j : @IntoPure PROP (monPred_in i j) (i  j).
Proof. by rewrite /IntoPure monPred_at_in. Qed.
208 209
Global Instance from_pure_monPred_in i j : @FromPure PROP false (monPred_in i j) (i  j).
Proof. by rewrite /FromPure monPred_at_in. Qed.
210

211 212
Global Instance into_persistent_monPred_at p P Q 𝓠 i :
  IntoPersistent p P Q  MakeMonPredAt i Q 𝓠  IntoPersistent p (P i) 𝓠 | 0.
213
Proof.
214 215
  rewrite /IntoPersistent /MakeMonPredAt  =>-[/(_ i) ?] <-.
  by rewrite -monPred_at_persistently -monPred_at_persistently_if.
216
Qed.
217

218
Lemma into_wand_monPred_at_unknown_unknown p q R P 𝓟 Q 𝓠 i :
Robbert Krebbers's avatar
Robbert Krebbers committed
219
  IntoWand p q R P Q  MakeMonPredAt i P 𝓟  MakeMonPredAt i Q 𝓠 
220
  IntoWand p q (R i) 𝓟 𝓠.
221
Proof.
222
  rewrite /IntoWand /MakeMonPredAt /bi_affinely_if /bi_persistently_if.
223
  destruct p, q=> /bi.wand_elim_l' [/(_ i) H] <- <-; apply bi.wand_intro_r;
224
  revert H; by rewrite monPred_at_sep ?monPred_at_affinely ?monPred_at_persistently.
225
Qed.
226
Lemma into_wand_monPred_at_unknown_known p q R P 𝓟 Q i j :
227
  IsBiIndexRel i j  IntoWand p q R P Q 
228
  MakeMonPredAt j P 𝓟  IntoWand p q (R i) 𝓟 (Q 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_le 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 i) (P j) 𝓠.
236
Proof.
237 238
  rewrite /IntoWand /IsBiIndexRel /MakeMonPredAt=>-> ? ?.
  eapply into_wand_monPred_at_unknown_unknown=>//. apply _.
239
Qed.
240
Lemma into_wand_monPred_at_known_unknown_ge p q R P Q 𝓠 i j :
241
  IsBiIndexRel i j  IntoWand p q R P Q 
242
  MakeMonPredAt j Q 𝓠  IntoWand p q (R j) (P i) 𝓠.
243
Proof.
244 245
  rewrite /IntoWand /IsBiIndexRel /MakeMonPredAt=>-> ? ?.
  eapply into_wand_monPred_at_unknown_unknown=>//. apply _.
246
Qed.
247

248 249 250 251 252 253 254
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.

255 256
Global Instance from_forall_monPred_at_wand P Q (Φ Ψ : I  PROP) i :
  ( j, MakeMonPredAt j P (Φ j))  ( j, MakeMonPredAt j Q (Ψ j)) 
257
  FromForall ((P - Q) i)%I (λ j, i  j  Φ j - Ψ j)%I (to_ident_name idx).
258
Proof.
259
  rewrite /FromForall /MakeMonPredAt monPred_at_wand=> H1 H2. do 2 f_equiv.
260
  by rewrite H1 H2.
261
Qed.
262 263
Global Instance from_forall_monPred_at_impl P Q (Φ Ψ : I  PROP) i :
  ( j, MakeMonPredAt j P (Φ j))  ( j, MakeMonPredAt j Q (Ψ j)) 
264
  FromForall ((P  Q) i)%I (λ j, i  j  Φ j  Ψ j)%I (to_ident_name idx).
265
Proof.
266
  rewrite /FromForall /MakeMonPredAt monPred_at_impl=> H1 H2. do 2 f_equiv.
267
  by rewrite H1 H2 bi.pure_impl_forall.
268 269
Qed.

270
Global Instance into_forall_monPred_at_index P i :
271 272 273 274 275
  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.
276

277 278
Global Instance from_and_monPred_at P Q1 𝓠1 Q2 𝓠2 i :
  FromAnd P Q1 Q2  MakeMonPredAt i Q1 𝓠1  MakeMonPredAt i Q2 𝓠2 
279
  FromAnd (P i) 𝓠1 𝓠2.
280 281 282 283
Proof.
  rewrite /FromAnd /MakeMonPredAt /MakeMonPredAt=> <- <- <-.
  by rewrite monPred_at_and.
Qed.
284 285
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 
286
  IntoAnd p (P i) 𝓠1 𝓠2.
287
Proof.
288
  rewrite /IntoAnd /MakeMonPredAt /bi_affinely_if /bi_persistently_if.
289 290
  destruct p=>-[/(_ i) H] <- <-; revert H;
  by rewrite ?monPred_at_affinely ?monPred_at_persistently monPred_at_and.
291 292
Qed.

293 294
Global Instance from_sep_monPred_at P Q1 𝓠1 Q2 𝓠2 i :
  FromSep P Q1 Q2  MakeMonPredAt i Q1 𝓠1  MakeMonPredAt i Q2 𝓠2 
295
  FromSep (P i) 𝓠1 𝓠2.
296
Proof. rewrite /FromSep /MakeMonPredAt=> <- <- <-. by rewrite monPred_at_sep. Qed.
297 298
Global Instance into_sep_monPred_at P Q1 𝓠1 Q2 𝓠2 i :
  IntoSep P Q1 Q2  MakeMonPredAt i Q1 𝓠1  MakeMonPredAt i Q2 𝓠2 
299
  IntoSep (P i) 𝓠1 𝓠2.
300
Proof. rewrite /IntoSep /MakeMonPredAt=> -> <- <-. by rewrite monPred_at_sep. Qed.
301 302
Global Instance from_or_monPred_at P Q1 𝓠1 Q2 𝓠2 i :
  FromOr P Q1 Q2  MakeMonPredAt i Q1 𝓠1  MakeMonPredAt i Q2 𝓠2 
303
  FromOr (P i) 𝓠1 𝓠2.
304
Proof. rewrite /FromOr /MakeMonPredAt=> <- <- <-. by rewrite monPred_at_or. Qed.
305 306
Global Instance into_or_monPred_at P Q1 𝓠1 Q2 𝓠2 i :
  IntoOr P Q1 Q2  MakeMonPredAt i Q1 𝓠1  MakeMonPredAt i Q2 𝓠2 
307
  IntoOr (P i) 𝓠1 𝓠2.
308
Proof. rewrite /IntoOr /MakeMonPredAt=> -> <- <-. by rewrite monPred_at_or. Qed.
309

310 311
Global Instance from_exist_monPred_at {A} P (Φ : A  monPred) (Ψ : A  PROP) i :
  FromExist P Φ  ( a, MakeMonPredAt i (Φ a) (Ψ a))  FromExist (P i) Ψ.
312
Proof.
313 314
  rewrite /FromExist /MakeMonPredAt=><- H. setoid_rewrite <- H.
  by rewrite monPred_at_exist.
315
Qed.
316 317
Global Instance into_exist_monPred_at {A} P (Φ : A  monPred) name (Ψ : A  PROP) i :
  IntoExist P Φ name  ( a, MakeMonPredAt i (Φ a) (Ψ a))  IntoExist (P i) Ψ name.
318
Proof.
319 320
  rewrite /IntoExist /MakeMonPredAt=>-> H. setoid_rewrite <- H.
  by rewrite monPred_at_exist.
321 322
Qed.

323
Global Instance from_forall_monPred_at_objectively P (Φ : I  PROP) i :
324
  ( i, MakeMonPredAt i P (Φ i))  FromForall ((<obj> P) i)%I Φ (to_ident_name idx).
325
Proof.
326
  rewrite /FromForall /MakeMonPredAt monPred_at_objectively=>H. by setoid_rewrite <- H.
327
Qed.
328
Global Instance into_forall_monPred_at_objectively P (Φ : I  PROP) i :
Robbert Krebbers's avatar
Robbert Krebbers committed
329
  ( i, MakeMonPredAt i P (Φ i))  IntoForall ((<obj> P) i) Φ.
330
Proof.
331
  rewrite /IntoForall /MakeMonPredAt monPred_at_objectively=>H. by setoid_rewrite <- H.
332
Qed.
333

334
Global Instance from_exist_monPred_at_ex P (Φ : I  PROP) i :
Robbert Krebbers's avatar
Robbert Krebbers committed
335
  ( i, MakeMonPredAt i P (Φ i))  FromExist ((<subj> P) i) Φ.
336
Proof.
337
  rewrite /FromExist /MakeMonPredAt monPred_at_subjectively=>H. by setoid_rewrite <- H.
338
Qed.
339 340 341
(* TODO: this implementation uses [idx] as the automatic name for the index. In
theory a monPred could define an appropriate metavariable for indices with an
[ident_name] argument to [MakeMonPredAt], but this is not implemented. *)
342
Global Instance into_exist_monPred_at_ex P (Φ : I  PROP) i :
343
  ( i, MakeMonPredAt i P (Φ i))  IntoExist ((<subj> P) i) Φ (to_ident_name idx).
344
Proof.
345
  rewrite /IntoExist /MakeMonPredAt monPred_at_subjectively=>H. by setoid_rewrite <- H.
346 347
Qed.

348 349
Global Instance from_forall_monPred_at {A} P (Φ : A  monPred) name (Ψ : A  PROP) i :
  FromForall P Φ name  ( a, MakeMonPredAt i (Φ a) (Ψ a))  FromForall (P i) Ψ name.
350
Proof.
351 352
  rewrite /FromForall /MakeMonPredAt=><- H. setoid_rewrite <- H.
  by rewrite monPred_at_forall.
353
Qed.
354 355
Global Instance into_forall_monPred_at {A} P (Φ : A  monPred) (Ψ : A  PROP) i :
  IntoForall P Φ  ( a, MakeMonPredAt i (Φ a) (Ψ a))  IntoForall (P i) Ψ.
356
Proof.
357 358
  rewrite /IntoForall /MakeMonPredAt=>-> H. setoid_rewrite <- H.
  by rewrite monPred_at_forall.
359 360
Qed.

361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382
(* 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.
383 384 385 386
Global Instance frame_monPred_at_wand p P R Q1 Q2 i j :
  IsBiIndexRel i j 
  Frame p R Q1 Q2 
  FrameMonPredAt p j (R i) (P - Q1) ((P - Q2) i).
387
Proof.
388
  rewrite /Frame /FrameMonPredAt=>-> Hframe.
389 390 391 392
  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.
393 394 395 396
Global Instance frame_monPred_at_impl P R Q1 Q2 i j :
  IsBiIndexRel i j 
  Frame true R Q1 Q2 
  FrameMonPredAt true j (R i) (P  Q1) ((P  Q2) i).
397
Proof.
398
  rewrite /Frame /FrameMonPredAt=>-> Hframe.
399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431
  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.
432

433 434
Global Instance into_embed_objective P :
  Objective P  IntoEmbed P ( i, P i).
435 436
Proof.
  rewrite /IntoEmbed=> ?.
437
  by rewrite {1}(objective_objectively P) monPred_objectively_unfold.
438
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
439

440 441 442
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
443
Proof. by rewrite /ElimModal !monPred_at_bupd. Qed.
444
Global Instance elim_modal_at_bupd_hyp `{BiBUpd PROP} φ p p' P 𝓟 𝓟' 𝓠 𝓠' i:
445
  MakeMonPredAt i P 𝓟 
446 447
  ElimModal φ p p' (|==> 𝓟) 𝓟' 𝓠 𝓠' 
  ElimModal φ p p' ((|==> P) i) 𝓟' 𝓠 𝓠'.
448
Proof. by rewrite /MakeMonPredAt /ElimModal monPred_at_bupd=><-. Qed.
449 450 451 452 453 454 455
Global Instance elim_modal_at φ p p' 𝓟 𝓟' P P' V:
  ElimModal φ p p' ⎡𝓟⎤ ⎡𝓟' P P'  ElimModal φ p p' 𝓟 𝓟' (P V) (P' V).
Proof.
  rewrite /ElimModal -!embed_intuitionistically_if.
  iIntros (HH Hφ) "[? HP]". iApply HH; [done|]. iFrame. iIntros (? <-) "?".
  by iApply "HP".
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
456 457 458 459

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.
460

Robbert Krebbers's avatar
Robbert Krebbers committed
461 462
Global Instance from_forall_monPred_at_plainly `{BiPlainly PROP} i P Φ :
  ( i, MakeMonPredAt i P (Φ i)) 
463
  FromForall (( P) i) (λ j,  (Φ j))%I (to_ident_name idx).
Robbert Krebbers's avatar
Robbert Krebbers committed
464 465 466 467 468 469 470 471 472 473 474 475
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.

476
Global Instance is_except_0_monPred_at i P :
477
  IsExcept0 P  IsExcept0 (P i).
478
Proof. rewrite /IsExcept0=>- [/(_ i)]. by rewrite monPred_at_except_0. Qed.
479

480
Global Instance make_monPred_at_internal_eq `{!BiInternalEq PROP} {A : ofeT} (x y : A) i :
481
  MakeMonPredAt i (x  y) (x  y).
482
Proof. by rewrite /MakeMonPredAt monPred_at_internal_eq. Qed.
483 484
Global Instance make_monPred_at_except_0 i P 𝓠 :
  MakeMonPredAt i P 𝓠  MakeMonPredAt i ( P)%I ( 𝓠)%I.
485
Proof. by rewrite /MakeMonPredAt monPred_at_except_0=><-. Qed.
486 487
Global Instance make_monPred_at_later i P 𝓠 :
  MakeMonPredAt i P 𝓠  MakeMonPredAt i ( P)%I ( 𝓠)%I.
488
Proof. by rewrite /MakeMonPredAt monPred_at_later=><-. Qed.
489 490
Global Instance make_monPred_at_laterN i n P 𝓠 :
  MakeMonPredAt i P 𝓠  MakeMonPredAt i (^n P)%I (^n 𝓠)%I.
491
Proof. rewrite /MakeMonPredAt=> <-. elim n=>//= ? <-. by rewrite monPred_at_later. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
492
Global Instance make_monPred_at_fupd `{BiFUpd PROP} i E1 E2 P 𝓟 :
493
  MakeMonPredAt i P 𝓟  MakeMonPredAt i (|={E1,E2}=> P)%I (|={E1,E2}=> 𝓟)%I.
494
Proof. by rewrite /MakeMonPredAt monPred_at_fupd=> <-. Qed.
495

496 497
Global Instance into_internal_eq_monPred_at `{!BiInternalEq PROP}
    {A : ofeT} (x y : A) P i :
498 499 500
  IntoInternalEq P x y  IntoInternalEq (P i) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite monPred_at_internal_eq. Qed.

501 502
Global Instance into_except_0_monPred_at_fwd i P Q 𝓠 :
  IntoExcept0 P Q  MakeMonPredAt i Q 𝓠  IntoExcept0 (P i) 𝓠.
503
Proof. rewrite /IntoExcept0 /MakeMonPredAt=> -> <-. by rewrite monPred_at_except_0. Qed.
504 505
Global Instance into_except_0_monPred_at_bwd i P 𝓟 Q :
  IntoExcept0 P Q  MakeMonPredAt i P 𝓟  IntoExcept0 𝓟 (Q i).
506
Proof. rewrite /IntoExcept0 /MakeMonPredAt=> H <-. by rewrite H monPred_at_except_0. Qed.
507

508
Global Instance maybe_into_later_monPred_at i n P Q 𝓠 :
509 510
  IntoLaterN false n P Q  MakeMonPredAt i Q 𝓠 
  IntoLaterN false n (P i) 𝓠.
511
Proof.
512
  rewrite /IntoLaterN /MaybeIntoLaterN /MakeMonPredAt=> -> <-. elim n=>//= ? <-.
513
  by rewrite monPred_at_later.
514
Qed.
515 516 517
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) 𝓠.
518
Proof.
519
  rewrite /FromModal /MakeMonPredAt=> <- <-. elim n=>//= ? ->.
520 521
  by rewrite monPred_at_later.
Qed.
522

523 524 525 526 527 528 529 530 531
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.
532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561
End bi.
(* When P and/or Q are evars when doing typeclass search on [IntoWand
   (R i) P Q], we use [MakeMonPredAt] in order to normalize the
   result of unification. However, when they are not evars, we want to
   propagate the known information through typeclass search. Hence, we
   do not want to use [MakeMonPredAt].

   As a result, depending on P and Q being evars, we use a different
   version of [into_wand_monPred_at_xx_xx]. *)
Hint Extern 3 (IntoWand _ _ (monPred_at _ _) ?P ?Q) =>
     is_evar P; is_evar Q;
     eapply @into_wand_monPred_at_unknown_unknown
     : typeclass_instances.
Hint Extern 2 (IntoWand _ _ (monPred_at _ _) ?P (monPred_at ?Q _)) =>
     eapply @into_wand_monPred_at_unknown_known
     : typeclass_instances.
Hint Extern 2 (IntoWand _ _ (monPred_at _ _) (monPred_at ?P _) ?Q) =>
     eapply @into_wand_monPred_at_known_unknown_le
     : typeclass_instances.
Hint Extern 2 (IntoWand _ _ (monPred_at _ _) (monPred_at ?P _) ?Q) =>
     eapply @into_wand_monPred_at_known_unknown_ge
     : typeclass_instances.

Section modal.
Context {I : biIndex} {PROP : bi}.
Local Notation monPred := (monPred I PROP).
Implicit Types P Q R : monPred.
Implicit Types 𝓟 𝓠 𝓡 : PROP.
Implicit Types φ : Prop.
Implicit Types i j : I.
562

563 564 565
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).
566
Proof. by rewrite /ElimModal !monPred_at_fupd. Qed.
567
Global Instance elim_modal_at_fupd_hyp `{BiFUpd PROP} φ p p' E1 E2 P 𝓟 𝓟' 𝓠 𝓠' i :
568
  MakeMonPredAt i P 𝓟 
569 570
  ElimModal φ p p' (|={E1,E2}=> 𝓟) 𝓟' 𝓠 𝓠' 
  ElimModal φ p p' ((|={E1,E2}=> P) i) 𝓟' 𝓠 𝓠'.
571
Proof. by rewrite /MakeMonPredAt /ElimModal monPred_at_fupd=><-. Qed.
572

573
Global Instance elim_acc_at_None `{BiFUpd PROP} {X} E1 E2 E3 E4 α α' β β' P P'x i :
574 575
  ( x, MakeEmbed (α x) (α' x))  ( x, MakeEmbed (β x) (β' x)) 
  ElimAcc (X:=X) (fupd E1 E2) (fupd E3 E4) α' β' (λ _, None) P P'x 
576
  ElimAcc (X:=X) (fupd E1 E2) (fupd E3 E4) α β (λ _, None) (P i) (λ x, P'x x i).
577 578 579 580 581 582 583
Proof.
  rewrite /ElimAcc /MakeEmbed. iIntros (Hα Hβ HEA) "Hinner Hacc".
  iApply (HEA with "[Hinner]").
  - iIntros (x).  iSpecialize ("Hinner" $! x). rewrite -Hα. by iIntros (? <-).
  - iMod "Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]". iModIntro. iExists x.
    rewrite -Hα -Hβ. iFrame. iIntros (? _) "Hβ". by iApply "Hclose".
Qed.
584
Global Instance elim_acc_at_Some `{BiFUpd PROP} {X} E1 E2 E3 E4 α α' β β' γ γ' P P'x i :
585 586 587 588
  ( x, MakeEmbed (α x) (α' x)) 
  ( x, MakeEmbed (β x) (β' x)) 
  ( x, MakeEmbed (γ x) (γ' x)) 
  ElimAcc (X:=X) (fupd E1 E2) (fupd E3 E4) α' β' (λ x, Some (γ' x)) P P'x 
589
  ElimAcc (X:=X) (fupd E1 E2) (fupd E3 E4) α β (λ x, Some (γ x)) (P i) (λ x, P'x x i).
590 591 592 593 594 595 596
Proof.
  rewrite /ElimAcc /MakeEmbed. iIntros (Hα Hβ Hγ HEA) "Hinner Hacc".
  iApply (HEA with "[Hinner]").
  - iIntros (x).  iSpecialize ("Hinner" $! x). rewrite -Hα. by iIntros (? <-).
  - iMod "Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]". iModIntro. iExists x.
    rewrite -Hα -Hβ -Hγ. iFrame. iIntros (? _) "Hβ /=". by iApply "Hclose".
Qed.
Ralf Jung's avatar
Ralf Jung committed
597

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

Ralf Jung's avatar
Ralf Jung committed
602 603
(* This hard-codes the fact that ElimInv with_close returns a
   [(λ _, ...)] as Q'. *)
604
Global Instance elim_inv_embed_with_close {X : Type} φ
605 606 607
    𝓟inv 𝓟in (𝓟out 𝓟close : X  PROP)
    Pin (Pout Pclose : X  monPred)
    Q Q' :
Ralf Jung's avatar
Ralf Jung committed
608
  ( i, ElimInv φ 𝓟inv 𝓟in 𝓟out (Some 𝓟close) (Q i) (λ _, Q' i)) 
609 610
  MakeEmbed 𝓟in Pin  ( x, MakeEmbed (𝓟out x) (Pout x)) 
  ( x, MakeEmbed (𝓟close x) (Pclose x)) 
Ralf Jung's avatar
Ralf Jung committed
611
  ElimInv (X:=X) φ ⎡𝓟inv Pin Pout (Some Pclose) Q (λ _, Q').
612 613 614
Proof.
  rewrite /MakeEmbed /ElimInv=>H <- Hout Hclose ?. iStartProof PROP.
  setoid_rewrite <-Hout. setoid_rewrite <-Hclose.
615 616
  iIntros (?) "(?&?&HQ')". iApply H; [done|]. iFrame. iIntros (x) "?".
  by iApply "HQ'".
617 618
Qed.
Global Instance elim_inv_embed_without_close  {X : Type}
619
    φ 𝓟inv 𝓟in (𝓟out : X  PROP) Pin (Pout : X  monPred) Q (Q' : X  monPred) :
620 621 622 623 624 625
  ( 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.
626 627
  iIntros (?) "(?&?&HQ')". iApply H; [done|]. iFrame. iIntros (x) "?".
  by iApply "HQ'".
628
Qed.
629
End modal.