monpred.v 20.3 KB
Newer Older
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
1
2
From iris.bi Require Import derived_laws.

3
4
(** Definitions. *)

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

Existing Instances bi_index_rel bi_index_rel_preorder.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
13
14
15
16
17
18
19
Section Ofe_Cofe.
Context {I : bi_index} {B : bi}.
Implicit Types i : I.

Record monPred :=
  MonPred { monPred_car :> I -> B;
            monPred_mono : Proper (() ==> ()) monPred_car }.
20
Local Existing Instance monPred_mono.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
21

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
22
Implicit Types P Q : monPred.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
23

24
(** Ofe + Cofe instances  *)
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
25

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
26
27
Section Ofe_Cofe_def.
  Inductive monPred_equiv' P Q : Prop :=
28
    { monPred_in_equiv i : P i  Q i } .
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
29
30
  Instance monPred_equiv : Equiv monPred := monPred_equiv'.
  Inductive monPred_dist' (n : nat) (P Q : monPred) : Prop :=
31
    { monPred_in_dist i : P i {n} Q i }.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
32
  Instance monPred_dist : Dist monPred := monPred_dist'.
33
34

  Definition monPred_sig P : { f : I -c> B | Proper (() ==> ()) f } :=
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
35
36
    exist _ (monPred_car P) (monPred_mono P).

37
  Definition sig_monPred (P' : { f : I -c> B | Proper (() ==> ()) f })
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
38
39
    : monPred :=
    MonPred (proj1_sig P') (proj2_sig P').
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
40

41
42
43
44
  (* 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
45
     P Q, P  Q  monPred_sig P  monPred_sig Q.
46
47
  Proof. by split; [intros []|]. Qed.
  Let monPred_sig_dist:
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
48
     n,  P Q : monPred, P {n} Q  monPred_sig P {n} monPred_sig Q.
49
  Proof. by split; [intros []|]. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
50

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

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
54
  Canonical Structure monPred_ofe := OfeT monPred monPred_ofe_mixin.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
55

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
56
  Global Instance monPred_cofe `{Cofe B} : Cofe monPred_ofe.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
57
  Proof.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
58
59
    unshelve refine (iso_cofe_subtype (A:=I-c>B) _ MonPred monPred_car _ _ _);
      [apply _|by apply monPred_sig_dist|done|].
60
61
    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
62
  Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
End Ofe_Cofe_def.

Lemma monPred_sig_monPred (P' : { f : I -c> B | Proper (() ==> ()) f }) :
  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.
79
80
81
82
83
84

(* 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 (⊑). *)
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
85
Global Instance monPred_car_ne (R : relation I) :
86
  Proper (R ==> R ==> iff) ()  Reflexive R 
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
87
   n, Proper (dist n ==> R ==> dist n) monPred_car.
88
89
90
91
Proof.
  intros ????? [Hd] ?? HR. rewrite Hd.
  apply equiv_dist, bi.equiv_spec; split; f_equiv; rewrite ->HR; done.
Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
92
Global Instance monPred_car_proper (R : relation I) :
93
  Proper (R ==> R ==> iff) ()  Reflexive R 
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
94
  Proper (() ==> R ==> ()) monPred_car.
95
Proof. repeat intro. apply equiv_dist=>?. f_equiv=>//. by apply equiv_dist. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
96
97
98
99
100
End Ofe_Cofe.

Arguments monPred _ _ : clear implicits.
Local Existing Instance monPred_mono.
Arguments monPred_ofe _ _ : clear implicits.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
101

102
103
(** BI and SBI structures. *)

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
104
105
106
107
108
109
110
Section Bi.
Context {I : bi_index} {B : bi}.
Implicit Types i : I.
Notation monPred := (monPred I B).
Implicit Types P Q : monPred.

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

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
114
115
Program Definition monPred_upclosed (Φ : I  B) : monPred :=
  MonPred (λ i, ( j, i  j  Φ j)%I) _.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
116
Next Obligation. solve_proper. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
117

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
118
Definition monPred_ipure_def (P : B) : monPred := MonPred (λ _, P) _.
119
Definition monPred_ipure_aux : seal (@monPred_ipure_def). by eexists. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
120
Definition monPred_ipure := unseal monPred_ipure_aux.
121
Definition monPred_ipure_eq : @monPred_ipure = _ := seal_eq _.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
122

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
123
124
Definition monPred_pure (φ : Prop) : monPred := monPred_ipure (bi_pure φ).
Definition monPred_emp : monPred := monPred_ipure emp%I.
125

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
126
127
Program Definition monPred_and_def P Q : monPred :=
  MonPred (λ i, P i  Q i)%I _.
128
Next Obligation. solve_proper. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
129
Definition monPred_and_aux : seal (@monPred_and_def). by eexists. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
130
Definition monPred_and := unseal (@monPred_and_aux).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
131
132
Definition monPred_and_eq : @monPred_and = _ := seal_eq _.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
133
134
Program Definition monPred_or_def P Q : monPred :=
  MonPred (λ i, P i  Q i)%I _.
135
Next Obligation. solve_proper. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
136
Definition monPred_or_aux : seal (@monPred_or_def). by eexists. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
137
Definition monPred_or := unseal (@monPred_or_aux).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
138
139
Definition monPred_or_eq : @monPred_or = _ := seal_eq _.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
140
Definition monPred_impl_def P Q : monPred :=
141
  monPred_upclosed (λ i, P i  Q i)%I.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
142
Definition monPred_impl_aux : seal (@monPred_impl_def). by eexists. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
143
Definition monPred_impl := unseal (@monPred_impl_aux).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
144
145
Definition monPred_impl_eq : @monPred_impl = _ := seal_eq _.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
146
147
Program Definition monPred_forall_def A (Φ : A  monPred) : monPred :=
  MonPred (λ i,  x : A, Φ x i)%I _.
148
Next Obligation. solve_proper. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
149
Definition monPred_forall_aux : seal (@monPred_forall_def). by eexists. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
150
Definition monPred_forall := unseal (@monPred_forall_aux).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
151
152
Definition monPred_forall_eq : @monPred_forall = _ := seal_eq _.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
153
154
Program Definition monPred_exist_def A (Φ : A  monPred) : monPred :=
  MonPred (λ i,  x : A, Φ x i)%I _.
155
Next Obligation. solve_proper. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
156
Definition monPred_exist_aux : seal (@monPred_exist_def). by eexists. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
157
Definition monPred_exist := unseal (@monPred_exist_aux).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
158
159
Definition monPred_exist_eq : @monPred_exist = _ := seal_eq _.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
160
161
Definition monPred_internal_eq_def (A : ofeT) (a b : A) : monPred :=
  MonPred (λ _, bi_internal_eq a b) _.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
162
Definition monPred_internal_eq_aux : seal (@monPred_internal_eq_def). by eexists. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
163
Definition monPred_internal_eq := unseal (@monPred_internal_eq_aux).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
164
165
Definition monPred_internal_eq_eq : @monPred_internal_eq = _ := seal_eq _.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
166
167
Program Definition monPred_sep_def P Q : monPred :=
  MonPred (λ i, P i  Q i)%I _.
168
Next Obligation. solve_proper. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
169
Definition monPred_sep_aux : seal (@monPred_sep_def). by eexists. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
170
Definition monPred_sep := unseal monPred_sep_aux.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
171
172
Definition monPred_sep_eq : @monPred_sep = _ := seal_eq _.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
173
Definition monPred_wand_def P Q : monPred :=
174
  monPred_upclosed (λ i, P i - Q i)%I.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
175
Definition monPred_wand_aux : seal (@monPred_wand_def). by eexists. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
176
Definition monPred_wand := unseal monPred_wand_aux.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
177
178
Definition monPred_wand_eq : @monPred_wand = _ := seal_eq _.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
179
180
Program Definition monPred_persistently_def P : monPred :=
  MonPred (λ i, bi_persistently (P i)) _.
181
Next Obligation. solve_proper. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
182
Definition monPred_persistently_aux : seal (@monPred_persistently_def). by eexists. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
183
Definition monPred_persistently := unseal monPred_persistently_aux.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
184
185
Definition monPred_persistently_eq : @monPred_persistently = _ := seal_eq _.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
186
Definition monPred_plainly P : monPred :=
187
188
  monPred_ipure ( i, bi_plainly (P i))%I.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
189
190
Program Definition monPred_in_def (i_0 : I) : monPred :=
  MonPred (λ i : I, i_0  i%I) _.
191
Next Obligation. solve_proper. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
192
Definition monPred_in_aux : seal (@monPred_in_def). by eexists. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
193
Definition monPred_in := unseal (@monPred_in_aux).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
194
195
Definition monPred_in_eq : @monPred_in = _ := seal_eq _.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
196
197
Definition monPred_all_def (P : monPred) : monPred :=
  MonPred (λ _ : I,  i, P i)%I _.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
198
Definition monPred_all_aux : seal (@monPred_all_def). by eexists. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
199
Definition monPred_all := unseal (@monPred_all_aux).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
200
Definition monPred_all_eq : @monPred_all = _ := seal_eq _.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
201
202
203
204
205
206
207
208
End Bi.

Program Definition monPred_later_def {I : bi_index} {B : sbi}
        (P : monPred I B) : monPred I B := MonPred (λ i,  (P i))%I _.
Next Obligation. solve_proper. Qed.
Definition monPred_later_aux {I B} : seal (@monPred_later_def I B). by eexists. Qed.
Definition monPred_later {I B} := unseal (@monPred_later_aux I B).
Definition monPred_later_eq {I B} : @monPred_later I B = _ := seal_eq _.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
209

210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
Definition unseal_eqs :=
  (@monPred_and_eq, @monPred_or_eq, @monPred_impl_eq,
   @monPred_forall_eq, @monPred_exist_eq, @monPred_internal_eq_eq,
   @monPred_sep_eq, @monPred_wand_eq,
   @monPred_persistently_eq, @monPred_later_eq,
   @monPred_in_eq, @monPred_all_eq, @monPred_ipure_eq).
Ltac unseal :=
  unfold bi_affinely, bi_absorbingly, sbi_except_0, bi_pure, bi_emp,
         monPred_upclosed, bi_and, bi_or, bi_impl, bi_forall, bi_exist,
         bi_internal_eq, bi_sep, bi_wand, bi_persistently, bi_affinely,
         sbi_later; simpl;
  unfold sbi_emp, sbi_pure, sbi_and, sbi_or, sbi_impl, sbi_forall, sbi_exist,
         sbi_internal_eq, sbi_sep, sbi_wand, sbi_persistently, sbi_plainly,
         bi_plainly; simpl;
  unfold monPred_pure, monPred_emp, monPred_plainly; simpl;
  rewrite !unseal_eqs /=.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
227
228
229
230
Section canonical_bi.
Context (I : bi_index) (B : bi).

Lemma monPred_bi_mixin : BiMixin (@monPred_ofe_mixin I B)
231
232
233
  monPred_entails monPred_emp monPred_pure monPred_and monPred_or
  monPred_impl monPred_forall monPred_exist monPred_internal_eq
  monPred_sep monPred_wand monPred_plainly monPred_persistently.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
234
Proof.
235
  split; try unseal;
Robbert Krebbers's avatar
Robbert Krebbers committed
236
    try by (repeat intro; split=> ? /=; repeat f_equiv).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
237
  - split.
Robbert Krebbers's avatar
Robbert Krebbers committed
238
239
    + intros P. by split.
    + intros P Q R [H1] [H2]. split => ?. by rewrite H1 H2.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
240
  - split.
241
242
    + 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
243
244
245
246
247
248
249
250
251
252
253
254
255
256
  - 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 //.
257
    apply bi.impl_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
258
259
260
261
262
263
264
  - 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 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 => ?.
265
    erewrite (bi.internal_eq_rewrite _ _ (flip Ψ _)) => //=. solve_proper.
Robbert Krebbers's avatar
Robbert Krebbers committed
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
  - 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 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.
282
    rewrite -bi.plainly_idemp_2. f_equiv. by apply bi.forall_intro=>_.
Robbert Krebbers's avatar
Robbert Krebbers committed
283
284
  - intros A Ψ. split=> i /=. apply bi.forall_intro=> j.
    rewrite bi.plainly_forall. apply bi.forall_intro=> a.
285
    by rewrite !bi.forall_elim.
Robbert Krebbers's avatar
Robbert Krebbers committed
286
287
288
289
  - 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
290
            !bi.forall_elim //.
Robbert Krebbers's avatar
Robbert Krebbers committed
291
  - intros P Q. split=> i /=. repeat setoid_rewrite bi.pure_impl_forall.
292
293
294
    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
295
296
  - intros P Q. split=> i /=.
    repeat setoid_rewrite bi.pure_impl_forall. rewrite 2!bi.forall_elim //.
297
298
299
    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
300
301
302
303
304
305
306
307
308
  - 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 P. split=> i /=. by setoid_rewrite bi.plainly_persistently_1.
  - 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.
309
Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
310

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
311
Canonical Structure monPredI : bi :=
312
313
314
  Bi (monPred I B) monPred_dist monPred_equiv monPred_entails monPred_emp
     monPred_pure monPred_and monPred_or monPred_impl monPred_forall
     monPred_exist monPred_internal_eq monPred_sep monPred_wand monPred_plainly
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
315
316
317
318
319
     monPred_persistently monPred_ofe_mixin monPred_bi_mixin.
End canonical_bi.

Section canonical_sbi.
Context (I : bi_index) (B : sbi).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
320

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
321
Lemma monPred_sbi_mixin :
322
323
324
  SbiMixin (PROP:=monPred I B) monPred_entails monPred_pure monPred_or
           monPred_impl monPred_forall monPred_exist monPred_internal_eq
           monPred_sep monPred_plainly monPred_persistently monPred_later.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
325
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
  split; unseal.
  - intros n P Q HPQ. split=> i /=.
    apply bi.later_contractive. destruct n as [|n]=> //. by apply HPQ.
  - 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
346
Qed.
347

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
348
Canonical Structure monPredSI : sbi :=
349
350
351
352
  Sbi (monPred I B) monPred_dist monPred_equiv monPred_entails monPred_emp
      monPred_pure monPred_and monPred_or monPred_impl monPred_forall
      monPred_exist monPred_internal_eq monPred_sep monPred_wand monPred_plainly
      monPred_persistently monPred_later monPred_ofe_mixin
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
353
354
      (bi_bi_mixin _) monPred_sbi_mixin.
End canonical_sbi.
355
356
357

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

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
358
359
360
361
362
363
364
Section bi_facts.
Context {I : bi_index} {B : bi}.
Implicit Types i : I.
Implicit Types P Q : monPred I B.

Global Instance monPred_car_mono :
  Proper (() ==> () ==> ()) (@monPred_car I B).
365
Proof. by move=> ?? [?] ?? ->. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
366
Global Instance monPred_car_mono_flip :
367
368
369
  Proper (flip () ==> flip () ==> flip ()) (@monPred_car I B).
Proof. solve_proper. Qed.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
370
Global Instance monPred_ipure_ne : NonExpansive (@monPred_ipure I B).
371
Proof. unseal. by split. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
372
Global Instance monPred_ipure_proper : Proper (() ==> ()) (@monPred_ipure I B).
373
Proof. apply (ne_proper _). Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
374
Global Instance monPred_ipure_mono : Proper (() ==> ()) (@monPred_ipure I B).
375
Proof. unseal. by split. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
376
Global Instance monPred_ipure_mono_flip :
377
378
379
  Proper (flip () ==> flip ()) (@monPred_ipure I B).
Proof. solve_proper. Qed.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
380
Global Instance monPred_in_proper (R : relation I) :
381
382
383
  Proper (R ==> R ==> iff) ()  Reflexive R 
  Proper (R ==> ()) (@monPred_in I B).
Proof. unseal. split. solve_proper. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
384
Global Instance monPred_in_mono : Proper (flip () ==> ()) (@monPred_in I B).
385
Proof. unseal. split. solve_proper. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
386
Global Instance monPred_in_mono_flip : Proper (() ==> flip ()) (@monPred_in I B).
387
388
Proof. solve_proper. Qed.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
389
Global Instance monPred_all_ne : NonExpansive (@monPred_all I B).
390
Proof. unseal. split. solve_proper. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
391
Global Instance monPred_all_proper : Proper (() ==> ()) (@monPred_all I B).
392
Proof. apply (ne_proper _). Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
393
Global Instance monPred_all_mono : Proper (() ==> ()) (@monPred_all I B).
394
Proof. unseal. split. solve_proper. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
395
Global Instance monPred_all_mono_flip :
396
397
398
  Proper (flip () ==> flip ()) (@monPred_all I B).
Proof. solve_proper. Qed.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
399
Global Instance monPred_affine : BiAffine B  BiAffine (monPredI I B).
400
401
Proof. split => ?. unseal. by apply affine. Qed.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
402
Lemma monPred_wand_force P Q i : (P - Q) i - (P i - Q i).
403
404
Proof. unseal. rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim //. Qed.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
405
Lemma monPred_impl_force P Q i : (P  Q) i - (P i  Q i).
406
407
Proof. unseal. rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim //. Qed.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
408
Lemma monPred_persistently_if_eq p P i:
409
410
411
  (bi_persistently_if p P) i = bi_persistently_if p (P i).
Proof. rewrite /bi_persistently_if. unseal. by destruct p. Qed.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
412
Lemma monPred_affinely_if_eq p P i:
413
414
415
416
417
418
  (bi_affinely_if p P) i = bi_affinely_if p (P i).
Proof. rewrite /bi_affinely_if. destruct p => //. rewrite /bi_affinely. by unseal. Qed.

(* TODO : if we use this for linear BIs, we should additionally define
   Absorbing and Affine instances. *)

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
419
Global Instance monPred_car_persistent P i : Persistent P  Persistent (P i).
420
Proof. move => [] /(_ i). by unseal. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
421
Global Instance monPred_car_plain P i : Plain P  Plain (P i).
422
Proof. move => [] /(_ i). unfold Plain. unseal. rewrite bi.forall_elim //. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
423
424
425

(* Notation "☐ P" := (monPred_ipure P%I) *)
(*   (at level 20, right associativity) : bi_scope. *)
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
426
Global Instance monPred_ipure_plain (P : B) :
427
428
  Plain P  Plain (@monPred_ipure I B P).
Proof. intros. split => ? /=. unseal. apply bi.forall_intro=>?. apply (plain _). Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
429
Global Instance monPred_ipure_persistent (P : B) :
430
431
432
433
434
  Persistent P  Persistent (@monPred_ipure I B P).
Proof. intros. split => ? /=. unseal. exact: H. Qed.

(* Note that monPred_in is *not* Plain, because it does depend on the
   index. *)
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
435
Global Instance monPred_in_persistent V :
436
437
438
  Persistent (@monPred_in I B V).
Proof. unfold Persistent. unseal; split => ?. by apply bi.pure_persistent. Qed.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
439
Global Instance monPred_all_plain P : Plain P  Plain (@monPred_all I B P).
440
441
442
443
444
Proof.
  move=>[]. unfold Plain. unseal=>Hp. split=>? /=.
  apply bi.forall_intro=>i. rewrite {1}(bi.forall_elim i) Hp.
  by rewrite bi.plainly_forall.
Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
445
Global Instance monPred_all_persistent P :
446
  Persistent P  Persistent (@monPred_all I B P).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
447
Proof.
448
449
  move=>[]. unfold Persistent. unseal=>Hp. split => ?.
  by apply persistent, bi.forall_persistent.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
450
Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
End bi_facts.

Section sbi_facts.
Context {I : bi_index} {B : sbi}.
Implicit Types i : I.
Implicit Types P Q : monPred I B.

Global Instance monPred_car_timeless P i : Timeless P  Timeless (P i).
Proof. move => [] /(_ i). unfold Timeless. by unseal. Qed.
Global Instance monPred_ipure_timeless (P : B) :
  Timeless P  Timeless (@monPred_ipure I B P).
Proof. intros. split => ? /=. unseal. exact: H. Qed.
Global Instance monPred_in_timeless V : Timeless (@monPred_in I B V).
Proof. split => ? /=. unseal. apply timeless, _. Qed.
Global Instance monPred_all_timeless P :
  Timeless P  Timeless (@monPred_all I B P).
Proof.
  move=>[]. unfold Timeless. unseal=>Hti. split=> ? /=.
  by apply timeless, bi.forall_timeless.
Qed.
End sbi_facts.