monpred.v 46.9 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
(** Definitions. *)
5
Structure biIndex :=
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
6
7
  BiIndex
    { bi_index_type :> Type;
8
      bi_index_inhabited : Inhabited bi_index_type;
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
9
      bi_index_rel : SqSubsetEq bi_index_type;
10
      bi_index_rel_preorder : PreOrder (@{bi_index_type}) }.
11
Existing Instances bi_index_inhabited bi_index_rel bi_index_rel_preorder.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
12

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
13
14
15
16
(* 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. *)
17
18
19
Class BiIndexBottom {I : biIndex} (bot : I) :=
  bi_index_bot i : bot  i.

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

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

Ralf Jung's avatar
Ralf Jung committed
29
Declare Scope monPred.
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 -d> 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 -d> 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 monPredO := OfeT monPred monPred_ofe_mixin.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
65

66
  Global Instance monPred_cofe `{Cofe PROP} : Cofe monPredO.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
67
  Proof.
68
    unshelve refine (iso_cofe_subtype (A:=I-d>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 -d> 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 monPredO _ _ : clear implicits.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
112

113
(** BI canonical structure *)
114

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 }.
Tej Chajed's avatar
Tej Chajed committed
123
Hint Immediate monPred_in_entails : core.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
124

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
Definition monPred_embed_def (P : PROP) : monPred := MonPred (λ _, P) _.
130
Definition monPred_embed_aux : seal (@monPred_embed_def). Proof. by eexists. Qed.
131
132
Definition monPred_embed : Embed PROP monPred := monPred_embed_aux.(unseal).
Definition monPred_embed_eq : @embed _ _ monPred_embed = _ := monPred_embed_aux.(seal_eq).
133
134

Definition monPred_emp_def : monPred := MonPred (λ _, emp)%I _.
135
Definition monPred_emp_aux : seal (@monPred_emp_def). Proof. by eexists. Qed.
136
137
Definition monPred_emp := monPred_emp_aux.(unseal).
Definition monPred_emp_eq : @monPred_emp = _ := monPred_emp_aux.(seal_eq).
138
139

Definition monPred_pure_def (φ : Prop) : monPred := MonPred (λ _, ⌜φ⌝)%I _.
140
Definition monPred_pure_aux : seal (@monPred_pure_def). Proof. by eexists. Qed.
141
142
Definition monPred_pure := monPred_pure_aux.(unseal).
Definition monPred_pure_eq : @monPred_pure = _ := monPred_pure_aux.(seal_eq).
143

144
Definition monPred_objectively_def P : monPred := MonPred (λ _,  i, P i)%I _.
145
Definition monPred_objectively_aux : seal (@monPred_objectively_def). Proof. by eexists. Qed.
146
147
Definition monPred_objectively := monPred_objectively_aux.(unseal).
Definition monPred_objectively_eq : @monPred_objectively = _ := monPred_objectively_aux.(seal_eq).
148

149
Definition monPred_subjectively_def P : monPred := MonPred (λ _,  i, P i)%I _.
150
Definition monPred_subjectively_aux : seal (@monPred_subjectively_def). Proof. by eexists. Qed.
151
152
Definition monPred_subjectively := monPred_subjectively_aux.(unseal).
Definition monPred_subjectively_eq : @monPred_subjectively = _ := monPred_subjectively_aux.(seal_eq).
153

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
154
155
Program Definition monPred_and_def P Q : monPred :=
  MonPred (λ i, P i  Q i)%I _.
156
Next Obligation. solve_proper. Qed.
157
Definition monPred_and_aux : seal (@monPred_and_def). Proof. by eexists. Qed.
158
159
Definition monPred_and := monPred_and_aux.(unseal).
Definition monPred_and_eq : @monPred_and = _ := monPred_and_aux.(seal_eq).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
160

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
161
162
Program Definition monPred_or_def P Q : monPred :=
  MonPred (λ i, P i  Q i)%I _.
163
Next Obligation. solve_proper. Qed.
164
Definition monPred_or_aux : seal (@monPred_or_def). Proof. by eexists. Qed.
165
166
Definition monPred_or := monPred_or_aux.(unseal).
Definition monPred_or_eq : @monPred_or = _ := monPred_or_aux.(seal_eq).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
167

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
168
Definition monPred_impl_def P Q : monPred :=
169
  monPred_upclosed (λ i, P i  Q i)%I.
170
Definition monPred_impl_aux : seal (@monPred_impl_def). Proof. by eexists. Qed.
171
172
Definition monPred_impl := monPred_impl_aux.(unseal).
Definition monPred_impl_eq : @monPred_impl = _ := monPred_impl_aux.(seal_eq).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
173

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
174
175
Program Definition monPred_forall_def A (Φ : A  monPred) : monPred :=
  MonPred (λ i,  x : A, Φ x i)%I _.
176
Next Obligation. solve_proper. Qed.
177
Definition monPred_forall_aux : seal (@monPred_forall_def). Proof. by eexists. Qed.
178
179
Definition monPred_forall := monPred_forall_aux.(unseal).
Definition monPred_forall_eq : @monPred_forall = _ := monPred_forall_aux.(seal_eq).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
180

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
181
182
Program Definition monPred_exist_def A (Φ : A  monPred) : monPred :=
  MonPred (λ i,  x : A, Φ x i)%I _.
183
Next Obligation. solve_proper. Qed.
184
Definition monPred_exist_aux : seal (@monPred_exist_def). Proof. by eexists. Qed.
185
186
Definition monPred_exist := monPred_exist_aux.(unseal).
Definition monPred_exist_eq : @monPred_exist = _ := monPred_exist_aux.(seal_eq).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
187

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
188
189
Program Definition monPred_sep_def P Q : monPred :=
  MonPred (λ i, P i  Q i)%I _.
190
Next Obligation. solve_proper. Qed.
191
Definition monPred_sep_aux : seal (@monPred_sep_def). Proof. by eexists. Qed.
192
193
Definition monPred_sep := monPred_sep_aux.(unseal).
Definition monPred_sep_eq : @monPred_sep = _ := monPred_sep_aux.(seal_eq).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
194

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
195
Definition monPred_wand_def P Q : monPred :=
196
  monPred_upclosed (λ i, P i - Q i)%I.
197
Definition monPred_wand_aux : seal (@monPred_wand_def). Proof. by eexists. Qed.
198
199
Definition monPred_wand := monPred_wand_aux.(unseal).
Definition monPred_wand_eq : @monPred_wand = _ := monPred_wand_aux.(seal_eq).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
200

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
201
Program Definition monPred_persistently_def P : monPred :=
202
  MonPred (λ i, <pers> (P i))%I _.
203
Next Obligation. solve_proper. Qed.
204
Definition monPred_persistently_aux : seal (@monPred_persistently_def). Proof. by eexists. Qed.
205
206
Definition monPred_persistently := monPred_persistently_aux.(unseal).
Definition monPred_persistently_eq : @monPred_persistently = _ := monPred_persistently_aux.(seal_eq).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
207

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
208
209
Program Definition monPred_in_def (i0 : I) : monPred :=
  MonPred (λ i : I, i0  i%I) _.
210
Next Obligation. solve_proper. Qed.
211
Definition monPred_in_aux : seal (@monPred_in_def). Proof. by eexists. Qed.
212
213
Definition monPred_in := monPred_in_aux.(unseal).
Definition monPred_in_eq : @monPred_in = _ := monPred_in_aux.(seal_eq).
214

215
Program Definition monPred_later_def P : monPred := MonPred (λ i,  (P i))%I _.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
216
Next Obligation. solve_proper. Qed.
217
Definition monPred_later_aux : seal monPred_later_def. Proof. by eexists. Qed.
218
219
Definition monPred_later := monPred_later_aux.(unseal).
Definition monPred_later_eq : monPred_later = _ := monPred_later_aux.(seal_eq).
220
221
222
223
224
225
End Bi.

Arguments monPred_objectively {_ _} _%I.
Arguments monPred_subjectively {_ _} _%I.
Notation "'<obj>' P" := (monPred_objectively P) : bi_scope.
Notation "'<subj>' P" := (monPred_subjectively P) : bi_scope.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
226

227
Module MonPred.
228
229
Definition unseal_eqs :=
  (@monPred_and_eq, @monPred_or_eq, @monPred_impl_eq,
230
   @monPred_forall_eq, @monPred_exist_eq, @monPred_sep_eq, @monPred_wand_eq,
231
   @monPred_persistently_eq, @monPred_later_eq, @monPred_in_eq,
232
233
   @monPred_embed_eq, @monPred_emp_eq, @monPred_pure_eq,
   @monPred_objectively_eq, @monPred_subjectively_eq).
234
Ltac unseal :=
235
  unfold bi_affinely, bi_absorbingly, bi_except_0, bi_pure, bi_emp,
236
         monPred_upclosed, bi_and, bi_or,
237
         bi_impl, bi_forall, bi_exist, bi_sep, bi_wand,
238
         bi_persistently, bi_affinely, bi_later;
Ralf Jung's avatar
Ralf Jung committed
239
  simpl;
240
  rewrite !unseal_eqs /=.
241
242
End MonPred.
Import MonPred.
243

244
Section canonical.
245
Context (I : biIndex) (PROP : bi).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
246

247
Lemma monPred_bi_mixin : BiMixin (PROP:=monPred I PROP)
248
  monPred_entails monPred_emp monPred_pure monPred_and monPred_or
249
  monPred_impl monPred_forall monPred_exist monPred_sep monPred_wand
Robbert Krebbers's avatar
Robbert Krebbers committed
250
  monPred_persistently.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
251
Proof.
252
  split; try unseal; try by (split=> ? /=; repeat f_equiv).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
253
  - split.
Robbert Krebbers's avatar
Robbert Krebbers committed
254
255
    + intros P. by split.
    + intros P Q R [H1] [H2]. split => ?. by rewrite H1 H2.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
256
  - split.
257
258
    + 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
259
260
261
262
263
264
265
266
267
268
269
270
271
272
  - 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 //.
273
    apply bi.impl_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
  - 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 f_equiv.
  - intros P. split=> i. by apply bi.persistently_idemp_2.
290
  - split=> i. by apply bi.persistently_emp_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
291
292
293
294
  - 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.
295
Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
296

297
298
299
300
Lemma monPred_bi_later_mixin :
  BiLaterMixin (PROP:=monPred I PROP) monPred_entails monPred_pure
               monPred_or monPred_impl monPred_forall monPred_exist
               monPred_sep monPred_persistently monPred_later.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
301
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
302
  split; unseal.
303
  - by split=> ? /=; repeat f_equiv.
Robbert Krebbers's avatar
Robbert Krebbers committed
304
  - intros P Q [?]. split=> i. by apply bi.later_mono.
305
  - intros P. split=> i /=. by apply bi.later_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
306
307
308
309
310
311
312
313
  - 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. 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
314
Qed.
315

316
317
Canonical Structure monPredI : bi :=
  {| bi_ofe_mixin := monPred_ofe_mixin; bi_bi_mixin := monPred_bi_mixin;
318
     bi_bi_later_mixin := monPred_bi_later_mixin |}.
319
End canonical.
320

321
322
323
324
325
Class Objective {I : biIndex} {PROP : bi} (P : monPred I PROP) :=
  objective_at i j : P i - P j.
Arguments Objective {_ _} _%I.
Arguments objective_at {_ _} _%I {_}.
Hint Mode Objective + + ! : typeclass_instances.
326
Instance: Params (@Objective) 2 := {}.
327

328
329
(** Primitive facts that cannot be deduced from the BI structure. *)

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
330
Section bi_facts.
331
Context {I : biIndex} {PROP : bi}.
332
Local Notation monPred := (monPred I PROP).
333
334
Local Notation monPredI := (monPredI I PROP).
Local Notation monPred_at := (@monPred_at I PROP).
335
Local Notation BiIndexBottom := (@BiIndexBottom I).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
336
Implicit Types i : I.
337
Implicit Types P Q : monPred.
338

339
340
341
342
343
344
345
346
347
348
349
350
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
(** monPred_at unfolding laws *)
Lemma monPred_at_pure i (φ : Prop) : monPred_at ⌜φ⌝ i  ⌜φ⌝.
Proof. by unseal. Qed.
Lemma monPred_at_emp i : monPred_at emp i  emp.
Proof. by unseal. 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.
Lemma monPred_at_forall {A} i (Φ : A  monPred) : ( x, Φ x) i   x, Φ x i.
Proof. by unseal. Qed.
Lemma monPred_at_exist {A} i (Φ : A  monPred) : ( x, Φ x) i   x, Φ x i.
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 : (<pers> P) i  <pers> (P i).
Proof. by unseal. Qed.
Lemma monPred_at_in i j : monPred_at (monPred_in j) i  j  i.
Proof. by unseal. Qed.
Lemma monPred_at_objectively i P : (<obj> P) i   j, P j.
Proof. by unseal. Qed.
Lemma monPred_at_subjectively i P : (<subj> P) i   j, P j.
Proof. by unseal. Qed.
Lemma monPred_at_persistently_if i p P : (<pers>?p P) i  <pers>?p (P i).
Proof. destruct p=>//=. apply monPred_at_persistently. Qed.
Lemma monPred_at_affinely i P : (<affine> P) i  <affine> (P i).
Proof. by rewrite /bi_affinely monPred_at_and monPred_at_emp. Qed.
Lemma monPred_at_affinely_if i p P : (<affine>?p P) i  <affine>?p (P i).
Proof. destruct p=>//=. apply monPred_at_affinely. Qed.
Lemma monPred_at_intuitionistically i P : ( P) i   (P i).
Proof. by rewrite /bi_intuitionistically monPred_at_affinely monPred_at_persistently. Qed.
Lemma monPred_at_intuitionistically_if i p P : (?p P) i  ?p (P i).
Proof. destruct p=>//=. apply monPred_at_intuitionistically. Qed.

Lemma monPred_at_absorbingly i P : (<absorb> P) i  <absorb> (P i).
Proof. by rewrite /bi_absorbingly monPred_at_sep monPred_at_pure. Qed.
Lemma monPred_at_absorbingly_if i p P : (<absorb>?p P) i  <absorb>?p (P i).
Proof. destruct p=>//=. apply monPred_at_absorbingly. 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.

387
(** Instances *)
388
Global Instance monPred_at_mono :
389
  Proper (() ==> () ==> ()) monPred_at.
390
Proof. by move=> ?? [?] ?? ->. Qed.
391
Global Instance monPred_at_flip_mono :
392
  Proper (flip () ==> flip () ==> flip ()) monPred_at.
393
394
Proof. solve_proper. Qed.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
395
Global Instance monPred_in_proper (R : relation I) :
396
  Proper (R ==> R ==> iff) ()  Reflexive R 
397
  Proper (R ==> ()) (@monPred_in I PROP).
398
Proof. unseal. split. solve_proper. Qed.
399
Global Instance monPred_in_mono : Proper (flip () ==> ()) (@monPred_in I PROP).
400
Proof. unseal. split. solve_proper. Qed.
401
Global Instance monPred_in_flip_mono : Proper (() ==> flip ()) (@monPred_in I PROP).
402
403
Proof. solve_proper. Qed.

404
Global Instance monPred_later_contractive :
405
  BiLaterContractive PROP  BiLaterContractive monPredI.
406
407
Proof. unseal=> ? n P Q HPQ. split=> i /=. f_contractive. apply HPQ. Qed.
Global Instance monPred_bi_löb : BiLöb PROP  BiLöb monPredI.
408
Proof. rewrite {2}/BiLöb; unseal=> ? P HP; split=> i /=. apply löb_weak, HP. Qed.
409
Global Instance monPred_bi_positive : BiPositive PROP  BiPositive monPredI.
410
Proof. split => ?. unseal. apply bi_positive. Qed.
411
Global Instance monPred_bi_affine : BiAffine PROP  BiAffine monPredI.
412
413
Proof. split => ?. unseal. by apply affine. Qed.

414
415
416
417
418
419
420
Lemma monPred_persistent P : ( i, Persistent (P i))  Persistent P.
Proof. intros HP. constructor=> i. unseal. apply HP. Qed.
Lemma monPred_absorbing P : ( i, Absorbing (P i))  Absorbing P.
Proof. intros HP. constructor=> i. unseal. apply HP. Qed.
Lemma monPred_affine P : ( i, Affine (P i))  Affine P.
Proof. intros HP. constructor=> i. unseal. apply HP. Qed.

421
Global Instance monPred_at_persistent P i : Persistent P  Persistent (P i).
422
Proof. move => [] /(_ i). by unseal. Qed.
423
Global Instance monPred_at_absorbing P i : Absorbing P  Absorbing (P i).
424
Proof. move => [] /(_ i). unfold Absorbing. by unseal. Qed.
425
Global Instance monPred_at_affine P i : Affine P  Affine (P i).
426
Proof. move => [] /(_ i). unfold Affine. by unseal. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
427

428
429
(** Note that [monPred_in] is *not* [Plain], because it depends on the index. *)
Global Instance monPred_in_persistent i : Persistent (@monPred_in I PROP i).
430
Proof. apply monPred_persistent=> j. rewrite monPred_at_in. apply _. Qed.
431
Global Instance monPred_in_absorbing i : Absorbing (@monPred_in I PROP i).
432
Proof. apply monPred_absorbing=> j. rewrite monPred_at_in. apply _. Qed.
433

434
Definition monPred_embedding_mixin : BiEmbedMixin PROP monPredI monPred_embed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
435
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
436
437
  split; try apply _; rewrite /bi_emp_valid; unseal; try done.
  - move=> P /= [/(_ inhabitant) ?] //.
438
439
440
441
  - intros PROP' ? P Q.
    set (f P := monPred_at P inhabitant).
    assert (NonExpansive f) by solve_proper.
    apply (f_equivI f).
Robbert Krebbers's avatar
Robbert Krebbers committed
442
  - intros P Q. split=> i /=.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
443
    by rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim.
Robbert Krebbers's avatar
Robbert Krebbers committed
444
  - intros P Q. split=> i /=.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
445
446
    by rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim.
Qed.
447
448
Global Instance monPred_bi_embed : BiEmbed PROP monPredI :=
  {| bi_embed_mixin := monPred_embedding_mixin |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
449
450
Global Instance monPred_bi_embed_emp : BiEmbedEmp PROP monPredI.
Proof. split. by unseal. Qed.
451

452
453
454
Lemma monPred_at_embed i (P : PROP) : monPred_at P i  P.
Proof. by unseal. Qed.

455
456
457
458
Lemma monPred_emp_unfold : emp%I = emp : PROP%I.
Proof. by unseal. Qed.
Lemma monPred_pure_unfold : bi_pure = λ φ,   φ  : PROP%I.
Proof. by unseal. Qed.
459
Lemma monPred_objectively_unfold : monPred_objectively = λ P,  i, P i%I.
460
Proof. by unseal. Qed.
461
Lemma monPred_subjectively_unfold : monPred_subjectively = λ P,  i, P i%I.
462
Proof. by unseal. Qed.
463

464
465
466
Global Instance monPred_objectively_ne : NonExpansive (@monPred_objectively I PROP).
Proof. rewrite monPred_objectively_unfold. solve_proper. Qed.
Global Instance monPred_objectively_proper : Proper (() ==> ()) (@monPred_objectively I PROP).
467
Proof. apply (ne_proper _). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
468
Lemma monPred_objectively_mono P Q : (P  Q)  (<obj> P  <obj> Q).
469
470
471
472
473
474
475
Proof. rewrite monPred_objectively_unfold. solve_proper. Qed.
Global Instance monPred_objectively_mono' : Proper (() ==> ()) (@monPred_objectively I PROP).
Proof. intros ???. by apply monPred_objectively_mono. Qed.
Global Instance monPred_objectively_flip_mono' :
  Proper (flip () ==> flip ()) (@monPred_objectively I PROP).
Proof. intros ???. by apply monPred_objectively_mono. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
476
Global Instance monPred_objectively_persistent P : Persistent P  Persistent (<obj> P).
477
Proof. rewrite monPred_objectively_unfold. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
478
Global Instance monPred_objectively_absorbing P : Absorbing P  Absorbing (<obj> P).
479
Proof. rewrite monPred_objectively_unfold. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
480
Global Instance monPred_objectively_affine P : Affine P  Affine (<obj> P).
481
482
483
484
485
Proof. rewrite monPred_objectively_unfold. apply _. Qed.

Global Instance monPred_subjectively_ne : NonExpansive (@monPred_subjectively I PROP).
Proof. rewrite monPred_subjectively_unfold. solve_proper. Qed.
Global Instance monPred_subjectively_proper : Proper (() ==> ()) (@monPred_subjectively I PROP).
486
Proof. apply (ne_proper _). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
487
Lemma monPred_subjectively_mono P Q : (P  Q)  <subj> P  <subj> Q.
488
489
490
491
492
493
494
Proof. rewrite monPred_subjectively_unfold. solve_proper. Qed.
Global Instance monPred_subjectively_mono' : Proper (() ==> ()) (@monPred_subjectively I PROP).
Proof. intros ???. by apply monPred_subjectively_mono. Qed.
Global Instance monPred_subjectively_flip_mono' :
  Proper (flip () ==> flip ()) (@monPred_subjectively I PROP).
Proof. intros ???. by apply monPred_subjectively_mono. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
495
Global Instance monPred_subjectively_persistent P : Persistent P  Persistent (<subj> P).
496
Proof. rewrite monPred_subjectively_unfold. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
497
Global Instance monPred_subjectively_absorbing P : Absorbing P  Absorbing (<subj> P).
498
Proof. rewrite monPred_subjectively_unfold. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
499
Global Instance monPred_subjectively_affine P : Affine P  Affine (<subj> P).
500
Proof. rewrite monPred_subjectively_unfold. apply _. Qed.
501

502
(* Laws for monPred_objectively and of Objective. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
503
Lemma monPred_objectively_elim P : <obj> P  P.
504
Proof. rewrite monPred_objectively_unfold. unseal. split=>?. apply bi.forall_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
505
Lemma monPred_objectively_idemp P : <obj> <obj> P  <obj> P.
506
Proof.
507
  apply bi.equiv_spec; split; [by apply monPred_objectively_elim|].
508
509
510
  unseal. split=>i /=. by apply bi.forall_intro=>_.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
511
Lemma monPred_objectively_forall {A} (Φ : A  monPred) : <obj> ( x, Φ x)   x, <obj> (Φ x).
512
513
514
515
Proof.
  unseal. split=>i. apply bi.equiv_spec; split=>/=;
    do 2 apply bi.forall_intro=>?; by do 2 rewrite bi.forall_elim.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
516
Lemma monPred_objectively_and P Q : <obj> (P  Q)  <obj> P  <obj> Q.
517
518
519
520
521
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.
522
Lemma monPred_objectively_exist {A} (Φ : A  monPred) :
Robbert Krebbers's avatar
Robbert Krebbers committed
523
  ( x, <obj> (Φ x))  <obj> ( x, (Φ x)).
524
Proof. apply bi.exist_elim=>?. f_equiv. apply bi.exist_intro. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
525
Lemma monPred_objectively_or P Q : <obj> P  <obj> Q  <obj> (P  Q).
526
527
Proof. apply bi.or_elim; f_equiv. apply bi.or_intro_l. apply bi.or_intro_r. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
528
Lemma monPred_objectively_sep_2 P Q : <obj> P  <obj> Q  <obj> (P  Q).
529
Proof. unseal. split=>i /=. apply bi.forall_intro=>?. by rewrite !bi.forall_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
530
Lemma monPred_objectively_sep `{BiIndexBottom bot} P Q : <obj> (P  Q)  <obj> P  <obj> Q.
531
Proof.
532
  apply bi.equiv_spec, conj, monPred_objectively_sep_2. unseal. split=>i /=.
533
534
  rewrite (bi.forall_elim bot). by f_equiv; apply bi.forall_intro=>j; f_equiv.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
535
Lemma monPred_objectively_embed (P : PROP) : <obj> P  P.
536
537
538
539
Proof.
  apply bi.equiv_spec; split; unseal; split=>i /=.
  by rewrite (bi.forall_elim inhabitant). by apply bi.forall_intro.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
540
Lemma monPred_objectively_emp : <obj> (emp : monPred)  emp.
541
Proof. rewrite monPred_emp_unfold. apply monPred_objectively_embed. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
542
Lemma monPred_objectively_pure φ : <obj> ( φ  : monPred)   φ .
543
Proof. rewrite monPred_pure_unfold. apply monPred_objectively_embed. Qed.
544

Robbert Krebbers's avatar
Robbert Krebbers committed
545
Lemma monPred_subjectively_intro P : P  <subj> P.
546
Proof. unseal. split=>?. apply bi.exist_intro. Qed.
547

548
Lemma monPred_subjectively_forall {A} (Φ : A  monPred) :
Robbert Krebbers's avatar
Robbert Krebbers committed
549
  (<subj> ( x, Φ x))   x, <subj> (Φ x).
550
Proof. apply bi.forall_intro=>?. f_equiv. apply bi.forall_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
551
Lemma monPred_subjectively_and P Q : <subj> (P  Q)  <subj> P  <subj> Q.
552
Proof. apply bi.and_intro; f_equiv. apply bi.and_elim_l. apply bi.and_elim_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
553
Lemma monPred_subjectively_exist {A} (Φ : A  monPred) : <subj> ( x, Φ x)   x, <subj> (Φ x).
554
555
556
557
Proof.
  unseal. split=>i. apply bi.equiv_spec; split=>/=;
    do 2 apply bi.exist_elim=>?; by do 2 rewrite -bi.exist_intro.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
558
Lemma monPred_subjectively_or P Q : <subj> (P  Q)  <subj> P  <subj> Q.
559
560
561
562
563
564
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.

Robbert Krebbers's avatar
Robbert Krebbers committed
565
Lemma monPred_subjectively_sep P Q : <subj> (P  Q)  <subj> P  <subj> Q.
566
567
Proof. unseal. split=>i /=. apply bi.exist_elim=>?. by rewrite -!bi.exist_intro. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
568
Lemma monPred_subjectively_idemp P : <subj> <subj> P  <subj> P.
569
Proof.
570
  apply bi.equiv_spec; split; [|by apply monPred_subjectively_intro].
571
572
573
  unseal. split=>i /=. by apply bi.exist_elim=>_.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
574
Lemma objective_objectively P `{!Objective P} : P  <obj> P.
575
Proof.
576
577
  rewrite monPred_objectively_unfold /= embed_forall. apply bi.forall_intro=>?.
  split=>?. unseal. apply objective_at, _.
578
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
579
Lemma objective_subjectively P `{!Objective P} : <subj> P  P.
580
Proof.
581
582
  rewrite monPred_subjectively_unfold /= embed_exist. apply bi.exist_elim=>?.
  split=>?. unseal. apply objective_at, _.
583
584
Qed.

585
Global Instance embed_objective (P : PROP) : @Objective I PROP P.
586
Proof. intros ??. by unseal. Qed.
587
Global Instance pure_objective φ : @Objective I PROP ⌜φ⌝.
588
Proof. intros ??. by unseal. Qed.
589
Global Instance emp_objective : @Objective I PROP emp.
590
Proof. intros ??. by unseal. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
591
Global Instance objectively_objective P : Objective (<obj> P).
592
Proof. intros ??. by unseal. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
593
Global Instance subjectively_objective P : Objective (<subj> P).
594
Proof. intros ??. by unseal. Qed.
595

596
597
598
599
600
Global Instance and_objective P Q `{!Objective P, !Objective Q} : Objective (P  Q).
Proof. intros i j. unseal. by rewrite !(objective_at _ i j). Qed.
Global Instance or_objective P Q `{!Objective P, !Objective Q} : Objective (P  Q).
Proof. intros i j. by rewrite !monPred_at_or !(objective_at _ i j). Qed.
Global Instance impl_objective P Q `{!Objective P, !Objective Q} : Objective (P  Q).
601
Proof.
602
603
  intros i j. unseal. rewrite (bi.forall_elim i) bi.pure_impl_forall.
  rewrite bi.forall_elim //. apply bi.forall_intro=> k.
604
  rewrite bi.pure_impl_forall. apply bi.forall_intro=>_.
605
  rewrite (objective_at Q i). by rewrite (objective_at P k).
606
Qed.
607
608
609
610
611
612
Global Instance forall_objective {A} Φ {H :  x : A, Objective (Φ x)} :
  @Objective I PROP ( x, Φ x)%I.
Proof. intros i j. unseal. do 2 f_equiv. by apply objective_at. Qed.
Global Instance exists_objective {A} Φ {H :  x : A, Objective (Φ x)} :
  @Objective I PROP ( x, Φ x)%I.
Proof. intros i j. unseal. do 2 f_equiv. by apply objective_at. Qed.
613

614
615
616
Global Instance sep_objective P Q `{!Objective P, !Objective Q} : Objective (P  Q).
Proof. intros i j. unseal. by rewrite !(objective_at _ i j). Qed.
Global Instance wand_objective P Q `{!Objective P, !Objective Q} : Objective (P - Q).
617
Proof.
618
619
  intros i j. unseal. rewrite (bi.forall_elim i) bi.pure_impl_forall.
  rewrite bi.forall_elim //. apply bi.forall_intro=> k.
620
  rewrite bi.pure_impl_forall. apply bi.forall_intro=>_.
621
  rewrite (objective_at Q i). by rewrite (objective_at P k).
622
Qed.
623
Global Instance persistently_objective P `{!Objective P} : Objective (<pers> P).
624
Proof. intros i j. unseal. by rewrite objective_at. Qed.
625

626
Global Instance affinely_objective P `{!Objective P} : Objective (<affine> P).
627
Proof. rewrite /bi_affinely. apply _. Qed.
628
629
Global Instance intuitionistically_objective P `{!Objective P} : Objective ( P).
Proof. rewrite /bi_intuitionistically. apply _. Qed.
630
Global Instance absorbingly_objective P `{!Objective P} : Objective (<absorb> P).
631
Proof. rewrite /bi_absorbingly. apply _. Qed.
632
Global Instance persistently_if_objective P p `{!Objective P} : Objective (<pers>?p P).
633
Proof. rewrite /bi_persistently_if. destruct p; apply _. Qed.
634
Global Instance affinely_if_objective P p `{!Objective P} : Objective (<affine>?p P).
635
Proof. rewrite /bi_affinely_if. destruct p; apply _. Qed.
636
637
Global Instance absorbingly_if_objective P p `{!Objective P} : Objective (<absorb>?p P).
Proof. rewrite /bi_absorbingly_if. destruct p; apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
638