monpred.v 43.3 KB
Newer Older
1
From stdpp Require Import coPset.
2
From iris.bi Require Import bi.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
3

4
5
(** Definitions. *)

6
Structure biIndex :=
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
7
8
  BiIndex
    { bi_index_type :> Type;
9
      bi_index_inhabited : Inhabited bi_index_type;
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
10
11
      bi_index_rel : SqSubsetEq bi_index_type;
      bi_index_rel_preorder : PreOrder () }.
12
Existing Instances bi_index_inhabited bi_index_rel bi_index_rel_preorder.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
13

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
14
15
16
17
(* We may want to instantiate monPred with the reflexivity relation in
   the case where there is no relevent order. In that case, there is
   no bottom element, so that we do not want to force any BI index to
   have one. *)
18
19
20
Class BiIndexBottom {I : biIndex} (bot : I) :=
  bi_index_bot i : bot  i.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
21
Section Ofe_Cofe.
22
Context {I : biIndex} {PROP : bi}.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
23
24
25
Implicit Types i : I.

Record monPred :=
26
27
  MonPred { monPred_at :> I  PROP;
            monPred_mono : Proper (() ==> ()) monPred_at }.
28
Local Existing Instance monPred_mono.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
29

30
31
Bind Scope monPred with bi.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
32
Implicit Types P Q : monPred.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
33

34
(** Ofe + Cofe instances  *)
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
35

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
36
37
Section Ofe_Cofe_def.
  Inductive monPred_equiv' P Q : Prop :=
38
    { monPred_in_equiv i : P i  Q i } .
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
39
40
  Instance monPred_equiv : Equiv monPred := monPred_equiv'.
  Inductive monPred_dist' (n : nat) (P Q : monPred) : Prop :=
41
    { monPred_in_dist i : P i {n} Q i }.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
42
  Instance monPred_dist : Dist monPred := monPred_dist'.
43

44
  Definition monPred_sig P : { f : I -c> PROP | Proper (() ==> ()) f } :=
45
    exist _ (monPred_at P) (monPred_mono P).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
46

47
  Definition sig_monPred (P' : { f : I -c> PROP | Proper (() ==> ()) f })
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
48
49
    : monPred :=
    MonPred (proj1_sig P') (proj2_sig P').
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
50

51
52
53
54
  (* These two lemma use the wrong Equiv and Dist instance for
    monPred. so we make sure they are not accessible outside of the
    section by using Let. *)
  Let monPred_sig_equiv:
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
55
     P Q, P  Q  monPred_sig P  monPred_sig Q.
56
57
  Proof. by split; [intros []|]. Qed.
  Let monPred_sig_dist:
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
58
     n,  P Q : monPred, P {n} Q  monPred_sig P {n} monPred_sig Q.
59
  Proof. by split; [intros []|]. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
60

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
61
  Definition monPred_ofe_mixin : OfeMixin monPred.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
62
63
  Proof. by apply (iso_ofe_mixin monPred_sig monPred_sig_equiv monPred_sig_dist). Qed.

64
  Canonical Structure monPredC := OfeT monPred monPred_ofe_mixin.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
65

66
  Global Instance monPred_cofe `{Cofe PROP} : Cofe monPredC.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
67
  Proof.
68
    unshelve refine (iso_cofe_subtype (A:=I-c>PROP) _ MonPred monPred_at _ _ _);
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
69
      [apply _|by apply monPred_sig_dist|done|].
70
71
    intros c i j Hij. apply @limit_preserving;
      [by apply bi.limit_preserving_entails; intros ??|]=>n. by rewrite Hij.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
72
  Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
73
74
End Ofe_Cofe_def.

75
Lemma monPred_sig_monPred (P' : { f : I -c> PROP | Proper (() ==> ()) f }) :
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
76
77
78
79
80
81
82
83
84
85
86
87
88
  monPred_sig (sig_monPred P')  P'.
Proof. by change (P'  P'). Qed.
Lemma sig_monPred_sig P : sig_monPred (monPred_sig P)  P.
Proof. done. Qed.

Global Instance monPred_sig_ne : NonExpansive monPred_sig.
Proof. move=> ??? [?] ? //=. Qed.
Global Instance monPred_sig_proper : Proper (() ==> ()) monPred_sig.
Proof. eapply (ne_proper _). Qed.
Global Instance sig_monPred_ne : NonExpansive (@sig_monPred).
Proof. split=>? //=. Qed.
Global Instance sig_monPred_proper : Proper (() ==> ()) sig_monPred.
Proof. eapply (ne_proper _). Qed.
89
90
91
92
93
94

(* We generalize over the relation R which is morally the equivalence
   relation over B. That way, the BI index can use equality as an
   equivalence relation (and Coq is able to infer the Proper and
   Reflexive instances properly), or any other equivalence relation,
   provided it is compatible with (⊑). *)
95
Global Instance monPred_at_ne (R : relation I) :
96
  Proper (R ==> R ==> iff) ()  Reflexive R 
97
   n, Proper (dist n ==> R ==> dist n) monPred_at.
98
99
100
101
Proof.
  intros ????? [Hd] ?? HR. rewrite Hd.
  apply equiv_dist, bi.equiv_spec; split; f_equiv; rewrite ->HR; done.
Qed.
102
Global Instance monPred_at_proper (R : relation I) :
103
  Proper (R ==> R ==> iff) ()  Reflexive R 
104
  Proper (() ==> R ==> ()) monPred_at.
105
Proof. repeat intro. apply equiv_dist=>?. f_equiv=>//. by apply equiv_dist. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
106
107
108
End Ofe_Cofe.

Arguments monPred _ _ : clear implicits.
109
Arguments monPred_at {_ _} _%I _.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
110
Local Existing Instance monPred_mono.
111
Arguments monPredC _ _ : clear implicits.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
112

113
114
(** BI and SBI structures. *)

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
115
Section Bi.
116
Context {I : biIndex} {PROP : bi}.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
117
Implicit Types i : I.
118
Notation monPred := (monPred I PROP).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
119
120
121
Implicit Types P Q : monPred.

Inductive monPred_entails (P1 P2 : monPred) : Prop :=
122
  { monPred_in_entails i : P1 i  P2 i }.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
123
124
Hint Immediate monPred_in_entails.

125
Program Definition monPred_upclosed (Φ : I  PROP) : monPred :=
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
126
  MonPred (λ i, ( j, i  j  Φ j)%I) _.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
127
Next Obligation. solve_proper. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
128

129
130
131
Definition monPred_embed_def (P : PROP) : monPred := MonPred (λ _, P) _.
Definition monPred_embed_aux : seal (@monPred_embed_def). by eexists. Qed.
Global Instance monPred_embed : BiEmbed PROP monPred := unseal monPred_embed_aux.
132
Definition monPred_embed_eq : bi_embed (A:=PROP) = _ := seal_eq _.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
133

134
135
136
Definition monPred_pure (φ : Prop) : monPred := tc_opaque ⎡⌜φ⌝⎤%I.
Definition monPred_emp : monPred := tc_opaque emp%I.
Definition monPred_plainly P : monPred := tc_opaque  i, bi_plainly (P i)%I.
137
138
Definition monPred_absolutely (P : monPred) : monPred := tc_opaque  i, P i%I.
Definition monPred_relatively (P : monPred) : monPred := tc_opaque  i, P i%I.
139

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
140
141
Program Definition monPred_and_def P Q : monPred :=
  MonPred (λ i, P i  Q i)%I _.
142
Next Obligation. solve_proper. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
143
Definition monPred_and_aux : seal (@monPred_and_def). by eexists. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
144
Definition monPred_and := unseal (@monPred_and_aux).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
145
146
Definition monPred_and_eq : @monPred_and = _ := seal_eq _.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
147
148
Program Definition monPred_or_def P Q : monPred :=
  MonPred (λ i, P i  Q i)%I _.
149
Next Obligation. solve_proper. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
150
Definition monPred_or_aux : seal (@monPred_or_def). by eexists. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
151
Definition monPred_or := unseal (@monPred_or_aux).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
152
153
Definition monPred_or_eq : @monPred_or = _ := seal_eq _.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
154
Definition monPred_impl_def P Q : monPred :=
155
  monPred_upclosed (λ i, P i  Q i)%I.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
156
Definition monPred_impl_aux : seal (@monPred_impl_def). by eexists. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
157
Definition monPred_impl := unseal (@monPred_impl_aux).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
158
159
Definition monPred_impl_eq : @monPred_impl = _ := seal_eq _.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
160
161
Program Definition monPred_forall_def A (Φ : A  monPred) : monPred :=
  MonPred (λ i,  x : A, Φ x i)%I _.
162
Next Obligation. solve_proper. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
163
Definition monPred_forall_aux : seal (@monPred_forall_def). by eexists. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
164
Definition monPred_forall := unseal (@monPred_forall_aux).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
165
166
Definition monPred_forall_eq : @monPred_forall = _ := seal_eq _.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
167
168
Program Definition monPred_exist_def A (Φ : A  monPred) : monPred :=
  MonPred (λ i,  x : A, Φ x i)%I _.
169
Next Obligation. solve_proper. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
170
Definition monPred_exist_aux : seal (@monPred_exist_def). by eexists. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
171
Definition monPred_exist := unseal (@monPred_exist_aux).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
172
173
Definition monPred_exist_eq : @monPred_exist = _ := seal_eq _.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
174
175
Program Definition monPred_sep_def P Q : monPred :=
  MonPred (λ i, P i  Q i)%I _.
176
Next Obligation. solve_proper. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
177
Definition monPred_sep_aux : seal (@monPred_sep_def). by eexists. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
178
Definition monPred_sep := unseal monPred_sep_aux.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
179
180
Definition monPred_sep_eq : @monPred_sep = _ := seal_eq _.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
181
Definition monPred_wand_def P Q : monPred :=
182
  monPred_upclosed (λ i, P i - Q i)%I.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
183
Definition monPred_wand_aux : seal (@monPred_wand_def). by eexists. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
184
Definition monPred_wand := unseal monPred_wand_aux.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
185
186
Definition monPred_wand_eq : @monPred_wand = _ := seal_eq _.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
187
188
Program Definition monPred_persistently_def P : monPred :=
  MonPred (λ i, bi_persistently (P i)) _.
189
Next Obligation. solve_proper. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
190
Definition monPred_persistently_aux : seal (@monPred_persistently_def). by eexists. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
191
Definition monPred_persistently := unseal monPred_persistently_aux.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
192
193
Definition monPred_persistently_eq : @monPred_persistently = _ := seal_eq _.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
194
195
Program Definition monPred_in_def (i0 : I) : monPred :=
  MonPred (λ i : I, i0  i%I) _.
196
Next Obligation. solve_proper. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
197
Definition monPred_in_aux : seal (@monPred_in_def). by eexists. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
198
Definition monPred_in := unseal (@monPred_in_aux).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
199
200
Definition monPred_in_eq : @monPred_in = _ := seal_eq _.

201
202
203
204
205
206
207
208
209
Definition monPred_bupd_def `{BUpd PROP} (P : monPred) : monPred :=
  (* monPred_upclosed is not actually needed, since bupd is always
     monotone. However, this depends on BUpdFacts, and we do not want
     this definition to depend on BUpdFacts to avoid having proofs
     terms in logical terms. *)
  monPred_upclosed (λ i, |==> P i)%I.
Definition monPred_bupd_aux `{BUpd PROP} : seal monPred_bupd_def. by eexists. Qed.
Global Instance monPred_bupd `{BUpd PROP} : BUpd _ := unseal monPred_bupd_aux.
Definition monPred_bupd_eq `{BUpd PROP} : @bupd monPred _ = _ := seal_eq _.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
210
211
End Bi.

212
213
Arguments monPred_absolutely {_ _} _%I.
Arguments monPred_relatively {_ _} _%I.
214
215
216
Notation "'∀ᵢ' P" := (monPred_absolutely P) (at level 20, right associativity) : bi_scope.
Notation "'∃ᵢ' P" := (monPred_relatively P) (at level 20, right associativity) : bi_scope.

217
218
Typeclasses Opaque monPred_pure monPred_emp monPred_plainly.

219
220
221
222
223
224
Section Sbi.
Context {I : biIndex} {PROP : sbi}.
Implicit Types i : I.
Notation monPred := (monPred I PROP).
Implicit Types P Q : monPred.

225
226
Definition monPred_internal_eq (A : ofeT) (a b : A) : monPred := tc_opaque a  b%I.

227
Program Definition monPred_later_def P : monPred := MonPred (λ i,  (P i))%I _.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
228
Next Obligation. solve_proper. Qed.
229
230
231
232
233
234
235
236
237
238
239
240
241
242
Definition monPred_later_aux : seal monPred_later_def. by eexists. Qed.
Definition monPred_later := unseal monPred_later_aux.
Definition monPred_later_eq : monPred_later = _ := seal_eq _.

Definition monPred_fupd_def `{FUpd PROP} (E1 E2 : coPset) (P : monPred) : monPred :=
  (* monPred_upclosed is not actually needed, since fupd is always
     monotone. However, this depends on FUpdFacts, and we do not want
     this definition to depend on FUpdFacts to avoid having proofs
     terms in logical terms. *)
  monPred_upclosed (λ i, |={E1,E2}=> P i)%I.
Definition monPred_fupd_aux `{FUpd PROP} : seal monPred_fupd_def. by eexists. Qed.
Global Instance monPred_fupd `{FUpd PROP} : FUpd _ := unseal monPred_fupd_aux.
Definition monPred_fupd_eq `{FUpd PROP} : @fupd monPred _ = _ := seal_eq _.
End Sbi.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
243

244
Module MonPred.
245
246
Definition unseal_eqs :=
  (@monPred_and_eq, @monPred_or_eq, @monPred_impl_eq,
247
   @monPred_forall_eq, @monPred_exist_eq,
248
   @monPred_sep_eq, @monPred_wand_eq,
249
250
   @monPred_persistently_eq, @monPred_later_eq, @monPred_in_eq,
   @monPred_embed_eq, @monPred_bupd_eq, @monPred_fupd_eq).
251
252
Ltac unseal :=
  unfold bi_affinely, bi_absorbingly, sbi_except_0, bi_pure, bi_emp,
253
         monPred_absolutely, monPred_relatively, monPred_upclosed, bi_and, bi_or,
254
         bi_impl, bi_forall, bi_exist, sbi_internal_eq, bi_sep, bi_wand,
Ralf Jung's avatar
Ralf Jung committed
255
         bi_persistently, bi_affinely, bi_plainly, sbi_later;
256
  simpl;
257
  unfold sbi_emp, sbi_pure, sbi_and, sbi_or, sbi_impl, sbi_forall, sbi_exist,
Ralf Jung's avatar
Ralf Jung committed
258
259
         sbi_internal_eq, sbi_sep, sbi_wand, sbi_persistently, sbi_plainly;
  simpl;
260
  unfold monPred_pure, monPred_emp, monPred_internal_eq, monPred_plainly; simpl;
261
  rewrite !unseal_eqs /=.
262
263
End MonPred.
Import MonPred.
264

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
265
Section canonical_bi.
266
Context (I : biIndex) (PROP : bi).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
267

268
Lemma monPred_bi_mixin : BiMixin (PROP:=monPred I PROP)
269
  monPred_entails monPred_emp monPred_pure monPred_and monPred_or
270
271
  monPred_impl monPred_forall monPred_exist monPred_sep monPred_wand
  monPred_plainly monPred_persistently.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
272
Proof.
273
  split; try unseal; try by (split=> ? /=; repeat f_equiv).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
274
  - split.
Robbert Krebbers's avatar
Robbert Krebbers committed
275
276
    + intros P. by split.
    + intros P Q R [H1] [H2]. split => ?. by rewrite H1 H2.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
277
  - split.
278
279
    + intros [HPQ]. split; split => i; move: (HPQ i); by apply bi.equiv_spec.
    + intros [[] []]. split=>i. by apply bi.equiv_spec.
Robbert Krebbers's avatar
Robbert Krebbers committed
280
281
282
283
284
285
286
287
288
289
290
291
292
293
  - intros P φ ?. split=> i. by apply bi.pure_intro.
  - intros φ P HP. split=> i. apply bi.pure_elim'=> ?. by apply HP.
  - intros A φ. split=> i. by apply bi.pure_forall_2.
  - intros P Q. split=> i. by apply bi.and_elim_l.
  - intros P Q. split=> i. by apply bi.and_elim_r.
  - intros P Q R [?] [?]. split=> i. by apply bi.and_intro.
  - intros P Q. split=> i. by apply bi.or_intro_l.
  - intros P Q. split=> i. by apply bi.or_intro_r.
  - intros P Q R [?] [?]. split=> i. by apply bi.or_elim.
  - intros P Q R [HR]. split=> i /=. setoid_rewrite bi.pure_impl_forall.
    apply bi.forall_intro=> j. apply bi.forall_intro=> Hij.
    apply bi.impl_intro_r. by rewrite -HR /= !Hij.
  - intros P Q R [HR]. split=> i /=.
     rewrite HR /= bi.forall_elim bi.pure_impl_forall bi.forall_elim //.
294
    apply bi.impl_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
  - intros A P Ψ HΨ. split=> i. apply bi.forall_intro => ?. by apply HΨ.
  - intros A Ψ. split=> i. by apply: bi.forall_elim.
  - intros A Ψ a. split=> i. by rewrite /= -bi.exist_intro.
  - intros A Ψ Q HΨ. split=> i. apply bi.exist_elim => a. by apply HΨ.
  - intros P P' Q Q' [?] [?]. split=> i. by apply bi.sep_mono.
  - intros P. split=> i. by apply bi.emp_sep_1.
  - intros P. split=> i. by apply bi.emp_sep_2.
  - intros P Q. split=> i. by apply bi.sep_comm'.
  - intros P Q R. split=> i. by apply bi.sep_assoc'.
  - intros P Q R [HR]. split=> i /=. setoid_rewrite bi.pure_impl_forall.
    apply bi.forall_intro=> j. apply bi.forall_intro=> Hij.
    apply bi.wand_intro_r. by rewrite -HR /= !Hij.
  - intros P Q R [HP]. split=> i. apply bi.wand_elim_l'.
    rewrite HP /= bi.forall_elim bi.pure_impl_forall bi.forall_elim //.
  - intros P Q [?]. split=> i /=. by do 3 f_equiv.
  - intros P. split=> i /=. by rewrite bi.forall_elim bi.plainly_elim_persistently.
  - intros P. split=> i /=. repeat setoid_rewrite <-bi.plainly_forall.
312
    rewrite -bi.plainly_idemp_2. f_equiv. by apply bi.forall_intro=>_.
Robbert Krebbers's avatar
Robbert Krebbers committed
313
314
  - intros A Ψ. split=> i /=. apply bi.forall_intro=> j.
    rewrite bi.plainly_forall. apply bi.forall_intro=> a.
315
    by rewrite !bi.forall_elim.
Robbert Krebbers's avatar
Robbert Krebbers committed
316
  - intros P Q. split=> i /=. repeat setoid_rewrite bi.pure_impl_forall.
317
318
319
    repeat setoid_rewrite <-bi.plainly_forall.
    repeat setoid_rewrite bi.persistently_forall. do 4 f_equiv.
    apply bi.persistently_impl_plainly.
Robbert Krebbers's avatar
Robbert Krebbers committed
320
321
  - intros P Q. split=> i /=.
    repeat setoid_rewrite bi.pure_impl_forall. rewrite 2!bi.forall_elim //.
322
323
324
    repeat setoid_rewrite <-bi.plainly_forall.
    setoid_rewrite bi.plainly_impl_plainly. f_equiv.
    do 3 apply bi.forall_intro => ?. f_equiv. rewrite bi.forall_elim //.
Robbert Krebbers's avatar
Robbert Krebbers committed
325
326
327
328
329
330
331
332
  - intros P. split=> i. apply bi.forall_intro=>_. by apply bi.plainly_emp_intro.
  - intros P Q. split=> i. apply bi.sep_elim_l, _.
  - intros P Q [?]. split=> i /=. by f_equiv.
  - intros P. split=> i. by apply bi.persistently_idemp_2.
  - intros A Ψ. split=> i. by apply bi.persistently_forall_2.
  - intros A Ψ. split=> i. by apply bi.persistently_exist_1.
  - intros P Q. split=> i. apply bi.sep_elim_l, _.
  - intros P Q. split=> i. by apply bi.persistently_and_sep_elim.
333
Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
334

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
335
Canonical Structure monPredI : bi :=
336
  Bi (monPred I PROP) monPred_dist monPred_equiv monPred_entails monPred_emp
337
     monPred_pure monPred_and monPred_or monPred_impl monPred_forall
338
339
     monPred_exist monPred_sep monPred_wand monPred_plainly monPred_persistently
     monPred_ofe_mixin monPred_bi_mixin.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
340
341
342
End canonical_bi.

Section canonical_sbi.
343
Context (I : biIndex) (PROP : sbi).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
344

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
345
Lemma monPred_sbi_mixin :
346
347
  SbiMixin (PROP:=monPred I PROP) monPred_ofe_mixin monPred_entails monPred_pure
           monPred_and monPred_or monPred_impl monPred_forall monPred_exist
348
349
           monPred_sep monPred_wand monPred_plainly monPred_persistently
           monPred_internal_eq monPred_later.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
350
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
351
352
353
  split; unseal.
  - intros n P Q HPQ. split=> i /=.
    apply bi.later_contractive. destruct n as [|n]=> //. by apply HPQ.
354
355
356
357
358
359
360
361
362
363
364
365
366
  - by split=> ? /=; repeat f_equiv.
  - intros A P a. split=> i. by apply bi.internal_eq_refl.
  - intros A a b Ψ ?. split=> i /=.
    setoid_rewrite bi.pure_impl_forall. do 2 apply bi.forall_intro => ?.
    erewrite (bi.internal_eq_rewrite _ _ (flip Ψ _)) => //=. solve_proper.
  - intros A1 A2 f g. split=> i. by apply bi.fun_ext.
  - intros A P x y. split=> i. by apply bi.sig_eq.
  - intros A a b ?. split=> i. by apply bi.discrete_eq_1.
  - intros P Q. split=> i /=.
    rewrite <-(sig_monPred_sig P), <-(sig_monPred_sig Q), <-(bi.f_equiv _).
    rewrite -bi.sig_equivI /= -bi.fun_ext. f_equiv=> j.
    rewrite -bi.prop_ext !(bi.forall_elim j) !bi.pure_impl_forall
            !bi.forall_elim //.
Robbert Krebbers's avatar
Robbert Krebbers committed
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
  - intros A x y. split=> i. by apply bi.later_eq_1.
  - intros A x y. split=> i. by apply bi.later_eq_2.
  - intros P Q [?]. split=> i. by apply bi.later_mono.
  - intros P. split=> i /=.
    setoid_rewrite bi.pure_impl_forall. rewrite /= !bi.forall_elim //. by apply bi.löb.
  - intros A Ψ. split=> i. by apply bi.later_forall_2.
  - intros A Ψ. split=> i. by apply bi.later_exist_false.
  - intros P Q. split=> i. by apply bi.later_sep_1.
  - intros P Q. split=> i. by apply bi.later_sep_2.
  - intros P. split=> i /=.
    rewrite bi.later_forall. f_equiv=> j. by rewrite -bi.later_plainly_1.
  - intros P. split=> i /=.
    rewrite bi.later_forall. f_equiv=> j. by rewrite -bi.later_plainly_2.
  - intros P. split=> i. by apply bi.later_persistently_1.
  - intros P. split=> i. by apply bi.later_persistently_2.
  - intros P. split=> i /=. rewrite -bi.forall_intro. apply bi.later_false_em.
    intros j. rewrite bi.pure_impl_forall. apply bi.forall_intro=> Hij. by rewrite Hij.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
384
Qed.
385

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
386
Canonical Structure monPredSI : sbi :=
387
  Sbi (monPred I PROP) monPred_dist monPred_equiv monPred_entails monPred_emp
388
      monPred_pure monPred_and monPred_or monPred_impl monPred_forall
389
390
      monPred_exist monPred_sep monPred_wand monPred_plainly
      monPred_persistently monPred_internal_eq monPred_later monPred_ofe_mixin
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
391
      (bi_bi_mixin _) monPred_sbi_mixin.
392

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
393
End canonical_sbi.
394

395
Class Absolute {I : biIndex} {PROP : bi} (P : monPred I PROP) :=
396
  absolute_at i j : P i - P j.
397
398
399
400
401
Arguments Absolute {_ _} _%I.
Arguments absolute_at {_ _} _%I {_}.
Hint Mode Absolute + + ! : typeclass_instances.
Instance: Params (@Absolute) 2.

402
403
(** Primitive facts that cannot be deduced from the BI structure. *)

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
404
Section bi_facts.
405
Context {I : biIndex} {PROP : bi}.
406
Local Notation monPred := (monPred I PROP).
407
408
Local Notation monPredI := (monPredI I PROP).
Local Notation monPred_at := (@monPred_at I PROP).
409
Local Notation BiIndexBottom := (@BiIndexBottom I).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
410
Implicit Types i : I.
411
Implicit Types P Q : monPred.
412
413

(** Instances *)
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
414

415
Global Instance monPred_at_mono :
416
  Proper (() ==> () ==> ()) monPred_at.
417
Proof. by move=> ?? [?] ?? ->. Qed.
418
Global Instance monPred_at_flip_mono :
419
  Proper (flip () ==> flip () ==> flip ()) monPred_at.
420
421
Proof. solve_proper. Qed.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
422
Global Instance monPred_in_proper (R : relation I) :
423
  Proper (R ==> R ==> iff) ()  Reflexive R 
424
  Proper (R ==> ()) (@monPred_in I PROP).
425
Proof. unseal. split. solve_proper. Qed.
426
Global Instance monPred_in_mono : Proper (flip () ==> ()) (@monPred_in I PROP).
427
Proof. unseal. split. solve_proper. Qed.
428
Global Instance monPred_in_flip_mono : Proper (() ==> flip ()) (@monPred_in I PROP).
429
430
Proof. solve_proper. Qed.

431
Global Instance monPred_positive : BiPositive PROP  BiPositive monPredI.
432
Proof. split => ?. unseal. apply bi_positive. Qed.
433
Global Instance monPred_affine : BiAffine PROP  BiAffine monPredI.
434
435
Proof. split => ?. unseal. by apply affine. Qed.

436
437
Global Instance monPred_plainly_exist `{BiIndexBottom bot} :
  BiPlainlyExist PROP  BiPlainlyExist monPredI.
438
Proof.
439
  split=>?/=. unseal. rewrite (bi.forall_elim bot) plainly_exist_1. do 2 f_equiv.
440
441
442
  apply bi.forall_intro=>?. by do 2 f_equiv.
Qed.

443
Global Instance monPred_at_persistent P i : Persistent P  Persistent (P i).
444
Proof. move => [] /(_ i). by unseal. Qed.
445
Global Instance monPred_at_plain P i : Plain P  Plain (P i).
446
Proof. move => [] /(_ i). unfold Plain. unseal. rewrite bi.forall_elim //. Qed.
447
Global Instance monPred_at_absorbing P i : Absorbing P  Absorbing (P i).
448
Proof. move => [] /(_ i). unfold Absorbing. by unseal. Qed.
449
Global Instance monPred_at_affine P i : Affine P  Affine (P i).
450
Proof. move => [] /(_ i). unfold Affine. by unseal. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
451

452
453
(* Note that monPred_in is *not* Plain, because it does depend on the
   index. *)
454
455
Global Instance monPred_in_persistent i :
  Persistent (@monPred_in I PROP i).
456
Proof. unfold Persistent. unseal; split => ?. by apply bi.pure_persistent. Qed.
457
458
Global Instance monPred_in_absorbing i :
  Absorbing (@monPred_in I PROP i).
459
Proof. unfold Absorbing. unseal. split=> ? /=. apply absorbing, _. Qed.
460

461

462
Global Instance monPred_bi_embedding : BiEmbedding PROP monPredI.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
463
464
Proof.
  split; try apply _; unseal; try done.
465
  - move =>?? /= [/(_ inhabitant) ?] //.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
466
467
468
469
470
471
472
  - split=>? /=.
    by rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim.
  - split=>? /=.
    by rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim.
  - intros ?. split => ? /=. apply bi.equiv_spec; split.
    by apply bi.forall_intro. by rewrite bi.forall_elim.
Qed.
473

474
475
476
Global Instance monPred_absolutely_ne : NonExpansive (@monPred_absolutely I PROP).
Proof. rewrite /monPred_absolutely /=. solve_proper. Qed.
Global Instance monPred_absolutely_proper : Proper (() ==> ()) (@monPred_absolutely I PROP).
477
Proof. apply (ne_proper _). Qed.
478
Lemma monPred_absolutely_mono P Q : (P  Q)  ( P   Q).
479
Proof. rewrite /monPred_absolutely /=. solve_proper. Qed.
480
481
482
Global Instance monPred_absolutely_mono' : Proper (() ==> ()) (@monPred_absolutely I PROP).
Proof. rewrite /monPred_absolutely /=. solve_proper. Qed.
Global Instance monPred_absolutely_flip_mono' :
483
  Proper (flip () ==> flip ()) (@monPred_absolutely I PROP).
484
485
Proof. solve_proper. Qed.

486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
Local Notation "'∀ᵢ' P" := (@monPred_absolutely I PROP P) : bi_scope.
Local Notation "'∃ᵢ' P" := (@monPred_relatively I PROP P) : bi_scope.

Global Instance monPred_absolutely_plain P : Plain P  Plain ( P).
Proof. rewrite /monPred_absolutely /=. apply _. Qed.
Global Instance monPred_absolutely_persistent P : Persistent P  Persistent ( P).
Proof. rewrite /monPred_absolutely /=. apply _. Qed.
Global Instance monPred_absolutely_absorbing P : Absorbing P  Absorbing ( P).
Proof. rewrite /monPred_absolutely /=. apply _. Qed.
Global Instance monPred_absolutely_affine P : Affine P  Affine ( P).
Proof. rewrite /monPred_absolutely /=. apply _. Qed.

Global Instance monPred_relatively_ne : NonExpansive (@monPred_relatively I PROP).
Proof. rewrite /monPred_relatively /=. solve_proper. Qed.
Global Instance monPred_relatively_proper : Proper (() ==> ()) (@monPred_relatively I PROP).
501
Proof. apply (ne_proper _). Qed.
502
503
504
Lemma monPred_relatively_mono P Q : (P  Q)  ( P   Q).
Proof. rewrite /monPred_relatively /=. solve_proper. Qed.
Global Instance monPred_relatively_mono' : Proper (() ==> ()) (@monPred_relatively I PROP).
505
Proof. rewrite /monPred_relatively /=. solve_proper. Qed.
506
Global Instance monPred_relatively_flip_mono' :
507
  Proper (flip () ==> flip ()) (@monPred_relatively I PROP).
508
509
Proof. solve_proper. Qed.

510
511
512
513
514
515
516
517
Global Instance monPred_relatively_plain P : Plain P  Plain ( P).
Proof. rewrite /monPred_relatively /=. apply _. Qed.
Global Instance monPred_relatively_persistent P : Persistent P  Persistent ( P).
Proof. rewrite /monPred_relatively /=. apply _. Qed.
Global Instance monPred_relatively_absorbing P : Absorbing P  Absorbing ( P).
Proof. rewrite /monPred_relatively /=. apply _. Qed.
Global Instance monPred_relatively_affine P : Affine P  Affine ( P).
Proof. rewrite /monPred_relatively /=. apply _. Qed.
518

519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
(** monPred_at unfolding laws *)
Lemma monPred_at_embed i (P : PROP) : monPred_at P i  P.
Proof. by unseal. Qed.
Lemma monPred_at_pure i (φ : Prop) : monPred_at ⌜φ⌝ i  ⌜φ⌝.
Proof. by apply monPred_at_embed. Qed.
Lemma monPred_at_emp i : monPred_at emp i  emp.
Proof. by apply monPred_at_embed. Qed.
Lemma monPred_at_plainly i P : bi_plainly P i   j, bi_plainly (P j).
Proof. by apply monPred_at_embed. Qed.
Lemma monPred_at_and i P Q : (P  Q) i  P i  Q i.
Proof. by unseal. Qed.
Lemma monPred_at_or i P Q : (P  Q) i  P i  Q i.
Proof. by unseal. Qed.
Lemma monPred_at_impl i P Q : (P  Q) i   j, i  j  P j  Q j.
Proof. by unseal. Qed.
534
Lemma monPred_at_forall {A} i (Φ : A  monPred) : ( x, Φ x) i   x, Φ x i.
535
Proof. by unseal. Qed.
536
Lemma monPred_at_exist {A} i (Φ : A  monPred) : ( x, Φ x) i   x, Φ x i.
537
538
539
540
541
542
543
544
545
Proof. by unseal. Qed.
Lemma monPred_at_sep i P Q : (P  Q) i  P i  Q i.
Proof. by unseal. Qed.
Lemma monPred_at_wand i P Q : (P - Q) i   j, i  j  P j - Q j.
Proof. by unseal. Qed.
Lemma monPred_at_persistently i P : bi_persistently P i  bi_persistently (P i).
Proof. by unseal. Qed.
Lemma monPred_at_in i j : monPred_at (monPred_in j) i  j  i.
Proof. by unseal. Qed.
546
Lemma monPred_at_absolutely i P : ( P) i   j, P j.
547
Proof. by unseal. Qed.
548
Lemma monPred_at_ex i P : ( P) i   j, P j.
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
Proof. by unseal. Qed.
Lemma monPred_at_persistently_if i p P :
  bi_persistently_if p P i  bi_persistently_if p (P i).
Proof. destruct p=>//=. apply monPred_at_persistently. Qed.
Lemma monPred_at_affinely i P : bi_affinely P i  bi_affinely (P i).
Proof. by rewrite /bi_affinely monPred_at_and monPred_at_emp. Qed.
Lemma monPred_at_affinely_if i p P :
  bi_affinely_if p P i  bi_affinely_if p (P i).
Proof. destruct p=>//=. apply monPred_at_affinely. Qed.
Lemma monPred_at_absorbingly i P : bi_absorbingly P i  bi_absorbingly (P i).
Proof. by rewrite /bi_absorbingly monPred_at_sep monPred_at_pure. Qed.

Lemma monPred_wand_force i P Q : (P - Q) i - (P i - Q i).
Proof. unseal. rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim //. Qed.
Lemma monPred_impl_force i P Q : (P  Q) i - (P i  Q i).
Proof. unseal. rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim //. Qed.

566
567
(* Laws for monPred_absolutely and of Absolute. *)
Lemma monPred_absolutely_elim P :  P  P.
568
Proof. unseal. split=>?. apply bi.forall_elim. Qed.
569
Lemma monPred_absolutely_idemp P :  ( P)   P.
570
Proof.
571
  apply bi.equiv_spec; split; [by apply monPred_absolutely_elim|].
572
573
574
  unseal. split=>i /=. by apply bi.forall_intro=>_.
Qed.

575
576
577
578
579
Lemma monPred_absolutely_forall {A} (Φ : A  monPred) :  ( x, Φ x)   x,  (Φ x).
Proof.
  unseal. split=>i. apply bi.equiv_spec; split=>/=;
    do 2 apply bi.forall_intro=>?; by do 2 rewrite bi.forall_elim.
Qed.
580
Lemma monPred_absolutely_and P Q :  (P  Q)   P   Q.
581
582
583
584
585
Proof.
  unseal. split=>i. apply bi.equiv_spec; split=>/=.
  - apply bi.and_intro; do 2 f_equiv. apply bi.and_elim_l. apply bi.and_elim_r.
  - apply bi.forall_intro=>?. by rewrite !bi.forall_elim.
Qed.
586
587
588
589
590
591
Lemma monPred_absolutely_exist {A} (Φ : A  monPred) :
  ( x,  (Φ x))   ( x, (Φ x)).
Proof. apply bi.exist_elim=>?. f_equiv. apply bi.exist_intro. Qed.
Lemma monPred_absolutely_or P Q : ( P)  ( Q)   (P  Q).
Proof. apply bi.or_elim; f_equiv. apply bi.or_intro_l. apply bi.or_intro_r. Qed.

592
Lemma monPred_absolutely_sep_2 P Q :  P   Q   (P  Q).
593
Proof. unseal. split=>i /=. apply bi.forall_intro=>?. by rewrite !bi.forall_elim. Qed.
594
Lemma monPred_absolutely_sep `{BiIndexBottom bot} P Q :  (P  Q)   P   Q.
595
Proof.
596
  apply bi.equiv_spec, conj, monPred_absolutely_sep_2. unseal. split=>i /=.
597
598
  rewrite (bi.forall_elim bot). by f_equiv; apply bi.forall_intro=>j; f_equiv.
Qed.
599
Lemma monPred_absolutely_embed (P : PROP) :  P  P.
600
601
602
603
604
Proof.
  apply bi.equiv_spec; split; unseal; split=>i /=.
  by rewrite (bi.forall_elim inhabitant). by apply bi.forall_intro.
Qed.

605
Lemma monPred_relatively_intro P : P   P.
606
Proof. unseal. split=>?. apply bi.exist_intro. Qed.
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627

Lemma monPred_relatively_forall {A} (Φ : A  monPred) :
  ( ( x, Φ x))   x,  (Φ x).
Proof. apply bi.forall_intro=>?. f_equiv. apply bi.forall_elim. Qed.
Lemma monPred_relatively_and P Q :  (P  Q)  ( P)  ( Q).
Proof. apply bi.and_intro; f_equiv. apply bi.and_elim_l. apply bi.and_elim_r. Qed.
Lemma monPred_relatively_exist {A} (Φ : A  monPred) :  ( x, Φ x)   x,  (Φ x).
Proof.
  unseal. split=>i. apply bi.equiv_spec; split=>/=;
    do 2 apply bi.exist_elim=>?; by do 2 rewrite -bi.exist_intro.
Qed.
Lemma monPred_relatively_or P Q :  (P  Q)   P   Q.
Proof.
  unseal. split=>i. apply bi.equiv_spec; split=>/=.
  - apply bi.exist_elim=>?. by rewrite -!bi.exist_intro.
  - apply bi.or_elim; do 2 f_equiv. apply bi.or_intro_l. apply bi.or_intro_r.
Qed.

Lemma monPred_relatively_sep P Q :  (P  Q)   P   Q.
Proof. unseal. split=>i /=. apply bi.exist_elim=>?. by rewrite -!bi.exist_intro. Qed.

628
Lemma monPred_relatively_idemp P :  ( P)   P.
629
Proof.
630
  apply bi.equiv_spec; split; [|by apply monPred_relatively_intro].
631
632
633
  unseal. split=>i /=. by apply bi.exist_elim=>_.
Qed.

634
Lemma absolute_absolutely P `{!Absolute P} : P   P.
635
636
637
638
Proof.
  rewrite /monPred_absolutely /= bi_embed_forall. apply bi.forall_intro=>?.
  split=>?. unseal. apply absolute_at, _.
Qed.
639
Lemma absolute_relatively P `{!Absolute P} :  P  P.
640
641
642
643
644
Proof.
  rewrite /monPred_relatively /= bi_embed_exist. apply bi.exist_elim=>?.
  split=>?. unseal. apply absolute_at, _.
Qed.

645
Global Instance emb_absolute (P : PROP) : @Absolute I PROP P.
646
Proof. intros ??. by unseal. Qed.
647
Global Instance pure_absolute φ : @Absolute I PROP ⌜φ⌝.
648
Proof. apply emb_absolute. Qed.
649
Global Instance emp_absolute : @Absolute I PROP emp.
650
651
652
653
654
Proof. apply emb_absolute. Qed.
Global Instance plainly_absolute P : Absolute (bi_plainly P).
Proof. apply emb_absolute. Qed.
Global Instance absolutely_absolute P : Absolute ( P).
Proof. apply emb_absolute. Qed.
655
Global Instance relatively_absolute P : Absolute ( P).
656
657
Proof. apply emb_absolute. Qed.

658
Global Instance and_absolute P Q `{!Absolute P, !Absolute Q} : Absolute (P  Q).
659
Proof. intros i j. unseal. by rewrite !(absolute_at _ i j). Qed.
660
Global Instance or_absolute P Q `{!Absolute P, !Absolute Q} : Absolute (P  Q).
661
Proof. intros i j. by rewrite !monPred_at_or !(absolute_at _ i j). Qed.
662
Global Instance impl_absolute P Q `{!Absolute P, !Absolute Q} : Absolute (P  Q).
663
Proof.
664
665
  intros i j. unseal. rewrite (bi.forall_elim i) bi.pure_impl_forall.
  rewrite bi.forall_elim //. apply bi.forall_intro=> k.
666
  rewrite bi.pure_impl_forall. apply bi.forall_intro=>_.
667
  rewrite (absolute_at Q i). by rewrite (absolute_at P k).
668
669
Qed.
Global Instance forall_absolute {A} Φ {H :  x : A, Absolute (Φ x)} :
670
  @Absolute I PROP ( x, Φ x)%I.
671
Proof. intros i j. unseal. do 2 f_equiv. by apply absolute_at. Qed.
672
Global Instance exists_absolute {A} Φ {H :  x : A, Absolute (Φ x)} :
673
  @Absolute I PROP ( x, Φ x)%I.
674
Proof. intros i j. unseal. do 2 f_equiv. by apply absolute_at. Qed.
675

676
Global Instance sep_absolute P Q `{!Absolute P, !Absolute Q} : Absolute (P  Q).
677
Proof. intros i j. unseal. by rewrite !(absolute_at _ i j). Qed.
678
Global Instance wand_absolute P Q `{!Absolute P, !Absolute Q} : Absolute (P - Q).
679
Proof.
680
681
  intros i j. unseal. rewrite (bi.forall_elim i) bi.pure_impl_forall.
  rewrite bi.forall_elim //. apply bi.forall_intro=> k.
682
  rewrite bi.pure_impl_forall. apply bi.forall_intro=>_.
683
  rewrite (absolute_at Q i). by rewrite (absolute_at P k).
684
Qed.
685
Global Instance persistently_absolute P `{!Absolute P} :
686
  Absolute (bi_persistently P).
687
Proof. intros i j. unseal. by rewrite absolute_at. Qed.
688

689
Global Instance affinely_absolute P `{!Absolute P} : Absolute (bi_affinely P).
690
Proof. rewrite /bi_affinely. apply _. Qed.
691
Global Instance absorbingly_absolute P `{!Absolute P} :
692
693
  Absolute (bi_absorbingly P).
Proof. rewrite /bi_absorbingly. apply _. Qed.
694
Global Instance plainly_if_absolute P p `{!Absolute P} :
695
696
  Absolute (bi_plainly_if p P).
Proof. rewrite /bi_plainly_if. destruct p; apply _. Qed.
697
Global Instance persistently_if_absolute P p `{!Absolute P} :
698
699
  Absolute (bi_persistently_if p P).
Proof. rewrite /bi_persistently_if. destruct p; apply _. Qed.
700
Global Instance affinely_if_absolute P p `{!Absolute P} :
701
702
703
704
  Absolute (bi_affinely_if p P).
Proof. rewrite /bi_affinely_if. destruct p; apply _. Qed.

(** monPred_in *)
705
706
707
708
709
Lemma monPred_in_intro P : P   i, monPred_in i  P i.
Proof.
  unseal. split=>i /=.
  rewrite /= -(bi.exist_intro i). apply bi.and_intro=>//. by apply bi.pure_intro.
Qed.
710
Lemma monPred_in_elim P i : monPred_in i - P i  P .
711
Proof.
712
  apply bi.impl_intro_r. unseal. split=>i' /=.
713
714
  eapply bi.pure_elim; [apply bi.and_elim_l|]=>?. rewrite bi.and_elim_r. by f_equiv.
Qed.