monpred.v 22.1 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
Section Ofe_Cofe.
14
Context {I : bi_index} {PROP : bi}.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
15 16 17
Implicit Types i : I.

Record monPred :=
18
  MonPred { monPred_car :> I  PROP;
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
19
            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> PROP | 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> PROP | 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

56
  Global Instance monPred_cofe `{Cofe PROP} : Cofe monPred_ofe.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
57
  Proof.
58
    unshelve refine (iso_cofe_subtype (A:=I-c>PROP) _ MonPred monPred_car _ _ _);
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
59
      [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
End Ofe_Cofe_def.

65
Lemma monPred_sig_monPred (P' : { f : I -c> PROP | Proper (() ==> ()) f }) :
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
66 67 68 69 70 71 72 73 74 75 76 77 78
  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
Section Bi.
105
Context {I : bi_index} {PROP : bi}.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
106
Implicit Types i : I.
107
Notation monPred := (monPred I PROP).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
108 109 110
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.

114
Program Definition monPred_upclosed (Φ : I  PROP) : monPred :=
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
115
  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

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

123 124
Definition monPred_pure (φ : Prop) : monPred := ⎡⌜φ⌝⎤%I.
Definition monPred_emp : monPred := 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 _.

186
Definition monPred_plainly P : monPred :=  i, bi_plainly (P i)%I.
187

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

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

202 203
Typeclasses Opaque monPred_pure monPred_emp monPred_plainly.

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

211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227
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
228
Section canonical_bi.
229
Context (I : bi_index) (PROP : bi).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
230

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

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
312
Canonical Structure monPredI : bi :=
313
  Bi (monPred I PROP) monPred_dist monPred_equiv monPred_entails monPred_emp
314 315
     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
316 317 318 319
     monPred_persistently monPred_ofe_mixin monPred_bi_mixin.
End canonical_bi.

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

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
322
Lemma monPred_sbi_mixin :
323
  SbiMixin (PROP:=monPred I PROP) monPred_entails monPred_pure monPred_or
324 325
           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
326
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346
  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
347
Qed.
348

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
349
Canonical Structure monPredSI : sbi :=
350
  Sbi (monPred I PROP) monPred_dist monPred_equiv monPred_entails monPred_emp
351 352 353
      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
354 355
      (bi_bi_mixin _) monPred_sbi_mixin.
End canonical_sbi.
356 357 358

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

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

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

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

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
384
Global Instance monPred_in_proper (R : relation I) :
385
  Proper (R ==> R ==> iff) ()  Reflexive R 
386
  Proper (R ==> ()) (@monPred_in I PROP).
387
Proof. unseal. split. solve_proper. Qed.
388
Global Instance monPred_in_mono : Proper (flip () ==> ()) (@monPred_in I PROP).
389
Proof. unseal. split. solve_proper. Qed.
390
Global Instance monPred_in_mono_flip : Proper (() ==> flip ()) (@monPred_in I PROP).
391 392
Proof. solve_proper. Qed.

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

403
Global Instance monPred_positive : BiPositive PROP  BiPositive (monPredI I PROP).
404
Proof. split => ?. unseal. apply bi_positive. Qed.
405
Global Instance monPred_affine : BiAffine PROP  BiAffine (monPredI I PROP).
406 407
Proof. split => ?. unseal. by apply affine. Qed.

408 409 410 411
(* (∀ x, bottom ⊑ x) cannot be infered using typeclasses. So this is
  not an instance. One should explicitely make an instance from this
  lemma for each instantiation of monPred. *)
Lemma monPred_plainly_exist (bottom : I) :
412
  ( x, bottom  x)  BiPlainlyExist PROP  BiPlainlyExist (monPredI I PROP).
413 414 415 416 417 418
Proof.
  intros ????. unseal. split=>? /=.
  rewrite (bi.forall_elim bottom) plainly_exist_1. do 2 f_equiv.
  apply bi.forall_intro=>?. by do 2 f_equiv.
Qed.

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

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

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
425
Lemma monPred_persistently_if_eq p P i:
426 427 428
  (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
429
Lemma monPred_affinely_if_eq p P i:
430 431 432
  (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.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
433
Global Instance monPred_car_persistent P i : Persistent P  Persistent (P i).
434
Proof. move => [] /(_ i). by unseal. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
435
Global Instance monPred_car_plain P i : Plain P  Plain (P i).
436
Proof. move => [] /(_ i). unfold Plain. unseal. rewrite bi.forall_elim //. Qed.
437 438 439 440
Global Instance monPred_car_absorbing P i : Absorbing P  Absorbing (P i).
Proof. move => [] /(_ i). unfold Absorbing. by unseal. Qed.
Global Instance monPred_car_affine P i : Affine P  Affine (P i).
Proof. move => [] /(_ i). unfold Affine. by unseal. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
441

442 443
Global Instance monPred_ipure_plain (P : PROP) :
  Plain P  @Plain (monPredI I PROP) P%I.
444
Proof. split => ? /=. unseal. apply bi.forall_intro=>?. apply (plain _). Qed.
445 446
Global Instance monPred_ipure_persistent (P : PROP) :
  Persistent P  @Persistent (monPredI I PROP) P%I.
447
Proof. split => ? /=. unseal. exact: H. Qed.
448 449
Global Instance monPred_ipure_absorbing (P : PROP) :
  Absorbing P  @Absorbing (monPredI I PROP) P%I.
450
Proof. unfold Absorbing. split => ? /=. by unseal. Qed.
451 452
Global Instance monPred_ipure_affine (P : PROP) :
  Affine P  @Affine (monPredI I PROP) P%I.
453
Proof. unfold Affine. split => ? /=. by unseal. Qed.
454 455 456

(* Note that monPred_in is *not* Plain, because it does depend on the
   index. *)
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
457
Global Instance monPred_in_persistent V :
458
  Persistent (@monPred_in I PROP V).
459
Proof. unfold Persistent. unseal; split => ?. by apply bi.pure_persistent. Qed.
460
Global Instance monPred_in_absorbing V :
461
  Absorbing (@monPred_in I PROP V).
462
Proof. unfold Absorbing. unseal. split=> ? /=. apply absorbing, _. Qed.
463

464
Global Instance monPred_all_plain P : Plain P  Plain (@monPred_all I PROP P).
465 466 467 468 469
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
470
Global Instance monPred_all_persistent P :
471
  Persistent P  Persistent (@monPred_all I PROP P).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
472
Proof.
473 474
  move=>[]. unfold Persistent. unseal=>Hp. split => ?.
  by apply persistent, bi.forall_persistent.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
475
Qed.
476
Global Instance monPred_all_absorbing P :
477
  Absorbing P  Absorbing (@monPred_all I PROP P).
478 479 480 481 482
Proof.
  move=>[]. unfold Absorbing. unseal=>Hp. split => ?.
  by apply absorbing, bi.forall_absorbing.
Qed.
Global Instance monPred_all_affine P :
483
  Inhabited I  Affine P  Affine (@monPred_all I PROP P).
484 485 486 487
Proof.
  move=>? []. unfold Affine. unseal=>Hp. split => ?.
  by apply affine, bi.forall_affine.
Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
488 489 490
End bi_facts.

Section sbi_facts.
491
Context {I : bi_index} {PROP : sbi}.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
492
Implicit Types i : I.
493
Implicit Types P Q : monPred I PROP.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
494 495 496

Global Instance monPred_car_timeless P i : Timeless P  Timeless (P i).
Proof. move => [] /(_ i). unfold Timeless. by unseal. Qed.
497 498
Global Instance monPred_ipure_timeless (P : PROP) :
  Timeless P  @Timeless (monPredSI I PROP) P%I.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
499
Proof. intros. split => ? /=. unseal. exact: H. Qed.
500
Global Instance monPred_in_timeless V : Timeless (@monPred_in I PROP V).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
501 502
Proof. split => ? /=. unseal. apply timeless, _. Qed.
Global Instance monPred_all_timeless P :
503
  Timeless P  Timeless (@monPred_all I PROP P).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
504 505 506 507 508
Proof.
  move=>[]. unfold Timeless. unseal=>Hti. split=> ? /=.
  by apply timeless, bi.forall_timeless.
Qed.
End sbi_facts.