Commit 2f4e9922 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

monpred : renamings.

parent 2883e242
......@@ -35,7 +35,7 @@ theories/bi/tactics.v
theories/bi/fractional.v
theories/bi/counter_examples.v
theories/bi/fixpoint.v
theories/bi/monfun.v
theories/bi/monpred.v
theories/base_logic/upred.v
theories/base_logic/derived.v
theories/base_logic/base_logic.v
......
......@@ -6,224 +6,227 @@ Structure bi_index :=
bi_index_rel : SqSubsetEq bi_index_type;
bi_index_rel_preorder : PreOrder () }.
Local Notation mono R P := (Proper (R ==> ()) P).
Local Existing Instances bi_index_rel bi_index_rel_preorder.
Local Notation mono R P := (Proper (R ==> bi_entails) P).
Existing Instances bi_index_rel bi_index_rel_preorder.
Structure funbi_ty (I : bi_index) (B : bi) :=
Record monPred (I : bi_index) (B : bi) :=
FUN
{ funbi_car :> I -c> B;
funbi_mono :> mono () funbi_car }.
{ monPred_car :> I -c> B;
monPred_mono :> mono () monPred_car }.
Arguments funbi_ty _ _ : clear implicits.
Arguments monPred _ _ : clear implicits.
Arguments FUN [_ _] _ _.
Arguments funbi_car [_ _] _ _.
Arguments funbi_mono [_ _] _ _ _ _ .
Arguments monPred_car [_ _] _ _.
Arguments monPred_mono [_ _] _ _ _ _ .
Notation funbi_upclose I B := (λ (P : bi_index_type I B), (λ i, ( j (_ : i j), (P j)))%I).
Notation monPred_upclose I B :=
(λ (P : bi_index_type I B) i, ( j (_ : i j), (P j))%I).
Instance funbi_upclose_mono I (B : bi) (P : bi_index_type I B) : mono () (funbi_upclose I B (P)).
Instance monPred_upclose_mono I (B : bi) (P : bi_index_type I B) :
mono () (monPred_upclose I B (P)).
Proof.
repeat intro. do !apply bi.forall_intro => ?.
rewrite !bi.forall_elim; [reflexivity|by etransitivity].
Qed.
Notation funbi_upclosed I B P := (@FUN I B%type (funbi_upclose I B P%function) (funbi_upclose_mono I B%type P%function)).
Notation monPred_upclosed I B P :=
(@FUN I B%type (monPred_upclose I B P%function) (monPred_upclose_mono I B%type P%function)).
Instance funbi_dist {I B} : Dist (funbi_ty I B) := λ n P1 P2, dist n (funbi_car P1) (funbi_car P2).
Instance funbi_equiv {I B} : Equiv (funbi_ty I B) := λ P1 P2, (funbi_car P1) (funbi_car P2).
Instance monPred_dist {I B} : Dist (monPred I B) := λ n P1 P2, dist n (monPred_car P1) (monPred_car P2).
Instance monPred_equiv {I B} : Equiv (monPred I B) := λ P1 P2, (monPred_car P1) (monPred_car P2).
Global Instance funbi_car_ne I B : NonExpansive (@funbi_car I B).
Global Instance monPred_car_ne I B : NonExpansive (@monPred_car I B).
Proof.
rewrite /funbi_car. move => n [f /= fm] [g gm].
by rewrite {1}/dist /= /funbi_dist /=.
rewrite /monPred_car. move => n [f /= fm] [g gm].
by rewrite {1}/dist /= /monPred_dist /=.
Qed.
Section Ofe_Cofe.
Context {I : bi_index} {B : bi}.
Implicit Types i : I.
Implicit Types P : funbi_ty I B.
Implicit Types P : monPred I B.
Definition funbi_sig P:
sig (fun f : I -c> B => mono (bi_index_rel I) f) :=
exist _ (funbi_car P) (funbi_mono P).
Definition monPred_sig P:
sig (fun f : I -c> B => mono () f) :=
exist _ (monPred_car P) (monPred_mono P).
Definition sig_funbi
(P' : sig (fun f : I -c> B => mono (bi_index_rel I) f)):
funbi_ty I B :=
Definition sig_monPred
(P' : sig (fun f : I -c> B => mono () f)):
monPred I B :=
FUN (proj1_sig P') (proj2_sig P').
Lemma funbi_sig_equiv:
P Q, P Q funbi_sig P funbi_sig Q.
Lemma monPred_sig_equiv:
P Q, P Q monPred_sig P monPred_sig Q.
Proof. done. Qed.
Lemma funbi_sig_dist:
n, P Q : funbi_ty I B, P {n} Q funbi_sig P {n} funbi_sig Q.
Lemma monPred_sig_dist:
n, P Q : monPred I B, P {n} Q monPred_sig P {n} monPred_sig Q.
Proof. done. Qed.
Definition funbi_ofe_mixin : OfeMixin (funbi_ty I B).
Proof. by apply (iso_ofe_mixin funbi_sig funbi_sig_equiv funbi_sig_dist). Qed.
Definition monPred_ofe_mixin : OfeMixin (monPred I B).
Proof. by apply (iso_ofe_mixin monPred_sig monPred_sig_equiv monPred_sig_dist). Qed.
Canonical Structure funbi_ofe := OfeT (funbi_ty I B) (funbi_ofe_mixin).
Canonical Structure monPred_ofe := OfeT (monPred I B) (monPred_ofe_mixin).
Instance funbi_cofe
Instance monPred_cofe
{C : Cofe B}
{limit_preserving_entails :
cP cQ : chain B, ( n, cP n cQ n) compl cP compl cQ}
: Cofe (funbi_ofe).
: Cofe (monPred_ofe).
Proof.
unshelve refine (iso_cofe_subtype (A:=I-c>B)
(fun f => mono (bi_index_rel I) f)
(fun f => mono () f)
(@FUN _ _)
(@funbi_car _ _) _ _ _);
(@monPred_car _ _) _ _ _);
[done|done|].
intros c i j Hij.
apply limit_preserving_entails.
intros. by apply funbi_mono.
intros. by apply monPred_mono.
Qed.
End Ofe_Cofe.
Inductive funbi_entails {I B} (P1 P2 : funbi_ty I B) : Prop := funbi_in_entails : ( i, bi_entails (funbi_car P1 i) (funbi_car P2 i)) funbi_entails P1 P2.
Lemma funbi_entails_eq {I B} P1 P2 : @funbi_entails I B P1 P2 ( i, bi_entails (funbi_car P1 i) (funbi_car P2 i)).
Inductive monPred_entails {I B} (P1 P2 : monPred I B) : Prop := monPred_in_entails : ( i, bi_entails (monPred_car P1 i) (monPred_car P2 i)) monPred_entails P1 P2.
Lemma monPred_entails_eq {I B} P1 P2 : @monPred_entails I B P1 P2 ( i, bi_entails (monPred_car P1 i) (monPred_car P2 i)).
Proof. split=>[[]//|//]. Qed.
Hint Immediate funbi_in_entails.
Hint Immediate monPred_in_entails.
Program Definition funbi_pure_def {I B} : Prop funbi_ty I B := λ P, FUN (λ _, bi_pure P) _.
Definition funbi_pure_aux : seal (@funbi_pure_def). by eexists. Qed.
Definition funbi_pure {I B} := unseal (@funbi_pure_aux) I B.
Definition funbi_pure_eq : @funbi_pure = _ := seal_eq _.
Program Definition monPred_pure_def {I B} : Prop monPred I B := λ P, FUN (λ _, bi_pure P) _.
Definition monPred_pure_aux : seal (@monPred_pure_def). by eexists. Qed.
Definition monPred_pure {I B} := unseal (@monPred_pure_aux) I B.
Definition monPred_pure_eq : @monPred_pure = _ := seal_eq _.
Program Definition funbi_emp {I B} := @FUN I B (λ _, emp)%I _.
Program Definition monPred_emp {I B} := @FUN I B (λ _, emp)%I _.
Program Definition funbi_and_def {I B} := λ (P Q : funbi_ty I B), @FUN I B (λ i, funbi_car P i funbi_car Q i)%I _.
Program Definition monPred_and_def {I B} := λ (P Q : monPred I B), @FUN I B (λ i, monPred_car P i monPred_car Q i)%I _.
Next Obligation.
intros I B P Q V1 V2 HV.
by apply bi.and_mono; apply funbi_mono.
by apply bi.and_mono; apply monPred_mono.
Qed.
Definition funbi_and_aux : seal (@funbi_and_def). by eexists. Qed.
Definition funbi_and {I B} := unseal (@funbi_and_aux) I B.
Definition funbi_and_eq : @funbi_and = _ := seal_eq _.
Definition monPred_and_aux : seal (@monPred_and_def). by eexists. Qed.
Definition monPred_and {I B} := unseal (@monPred_and_aux) I B.
Definition monPred_and_eq : @monPred_and = _ := seal_eq _.
Program Definition funbi_or_def {I B} := λ (P Q : funbi_ty I B), @FUN I B (λ i, funbi_car P i funbi_car Q i)%I _.
Program Definition monPred_or_def {I B} := λ (P Q : monPred I B), @FUN I B (λ i, monPred_car P i monPred_car Q i)%I _.
Next Obligation.
intros I B P Q V1 V2 HV.
by apply bi.or_mono; apply funbi_mono.
by apply bi.or_mono; apply monPred_mono.
Qed.
Definition funbi_or_aux : seal (@funbi_or_def). by eexists. Qed.
Definition funbi_or {I B} := unseal (@funbi_or_aux) I B.
Definition funbi_or_eq : @funbi_or = _ := seal_eq _.
Definition monPred_or_aux : seal (@monPred_or_def). by eexists. Qed.
Definition monPred_or {I B} := unseal (@monPred_or_aux) I B.
Definition monPred_or_eq : @monPred_or = _ := seal_eq _.
Program Definition funbi_impl_def {I B} := λ (P Q : funbi_ty I B), funbi_upclosed I B (λ i, funbi_car P i funbi_car Q i)%I.
Definition funbi_impl_aux : seal (@funbi_impl_def). by eexists. Qed.
Definition funbi_impl {I B} := unseal (@funbi_impl_aux) I B.
Definition funbi_impl_eq : @funbi_impl = _ := seal_eq _.
Program Definition monPred_impl_def {I B} := λ (P Q : monPred I B), monPred_upclosed I B (λ i, monPred_car P i monPred_car Q i)%I.
Definition monPred_impl_aux : seal (@monPred_impl_def). by eexists. Qed.
Definition monPred_impl {I B} := unseal (@monPred_impl_aux) I B.
Definition monPred_impl_eq : @monPred_impl = _ := seal_eq _.
Program Definition funbi_forall_def {I B} A := λ (Φ : A -> funbi_ty I B), @FUN I B (λ i, x : A, funbi_car (Φ x) i)%I _.
Program Definition monPred_forall_def {I B} A := λ (Φ : A -> monPred I B), @FUN I B (λ i, x : A, monPred_car (Φ x) i)%I _.
Next Obligation.
intros I B P Q V1 V2 HV.
by apply bi.forall_mono; intros; apply funbi_mono.
by apply bi.forall_mono; intros; apply monPred_mono.
Qed.
Definition funbi_forall_aux : seal (@funbi_forall_def). by eexists. Qed.
Definition funbi_forall {I B} := unseal (@funbi_forall_aux) I B.
Definition funbi_forall_eq : @funbi_forall = _ := seal_eq _.
Definition monPred_forall_aux : seal (@monPred_forall_def). by eexists. Qed.
Definition monPred_forall {I B} := unseal (@monPred_forall_aux) I B.
Definition monPred_forall_eq : @monPred_forall = _ := seal_eq _.
Program Definition funbi_exist_def {I B} A := λ (Φ : A -> funbi_ty I B), FUN (λ i, x : A, funbi_car (Φ x) i)%I _.
Program Definition monPred_exist_def {I B} A := λ (Φ : A -> monPred I B), FUN (λ i, x : A, monPred_car (Φ x) i)%I _.
Next Obligation.
intros I B P Q V1 V2 HV.
by apply bi.exist_mono; intros; apply funbi_mono.
by apply bi.exist_mono; intros; apply monPred_mono.
Qed.
Definition funbi_exist_aux : seal (@funbi_exist_def). by eexists. Qed.
Definition funbi_exist {I B} := unseal (@funbi_exist_aux) I B.
Definition funbi_exist_eq : @funbi_exist = _ := seal_eq _.
Definition monPred_exist_aux : seal (@monPred_exist_def). by eexists. Qed.
Definition monPred_exist {I B} := unseal (@monPred_exist_aux) I B.
Definition monPred_exist_eq : @monPred_exist = _ := seal_eq _.
Definition funbi_internal_eq_def {I B} A := λ a b, @FUN I B (λ _, @bi_internal_eq B A a b) _.
Definition funbi_internal_eq_aux : seal (@funbi_internal_eq_def). by eexists. Qed.
Definition funbi_internal_eq {I B} := unseal (@funbi_internal_eq_aux) I B.
Definition funbi_internal_eq_eq : @funbi_internal_eq = _ := seal_eq _.
Definition monPred_internal_eq_def {I B} A := λ a b, @FUN I B (λ _, @bi_internal_eq B A a b) _.
Definition monPred_internal_eq_aux : seal (@monPred_internal_eq_def). by eexists. Qed.
Definition monPred_internal_eq {I B} := unseal (@monPred_internal_eq_aux) I B.
Definition monPred_internal_eq_eq : @monPred_internal_eq = _ := seal_eq _.
Program Definition funbi_sep_def {I B} := λ (P Q : funbi_ty I B), FUN (λ i, funbi_car P i funbi_car Q i)%I _.
Program Definition monPred_sep_def {I B} := λ (P Q : monPred I B), FUN (λ i, monPred_car P i monPred_car Q i)%I _.
Next Obligation.
intros I B P Q V1 V2 HV.
by apply bi.sep_mono; intros; apply funbi_mono.
by apply bi.sep_mono; intros; apply monPred_mono.
Qed.
Definition funbi_sep_aux : seal (@funbi_sep_def). by eexists. Qed.
Definition funbi_sep {I B} := unseal funbi_sep_aux I B.
Definition funbi_sep_eq : @funbi_sep = _ := seal_eq _.
Definition monPred_sep_aux : seal (@monPred_sep_def). by eexists. Qed.
Definition monPred_sep {I B} := unseal monPred_sep_aux I B.
Definition monPred_sep_eq : @monPred_sep = _ := seal_eq _.
Program Definition funbi_wand_def {I B} := λ (P Q : funbi_ty I B), funbi_upclosed I B (λ i, funbi_car P i - funbi_car Q i)%I.
Definition funbi_wand_aux : seal (@funbi_wand_def). by eexists. Qed.
Definition funbi_wand {I B} := unseal funbi_wand_aux I B.
Definition funbi_wand_eq : @funbi_wand = _ := seal_eq _.
Program Definition monPred_wand_def {I B} := λ (P Q : monPred I B), monPred_upclosed I B (λ i, monPred_car P i - monPred_car Q i)%I.
Definition monPred_wand_aux : seal (@monPred_wand_def). by eexists. Qed.
Definition monPred_wand {I B} := unseal monPred_wand_aux I B.
Definition monPred_wand_eq : @monPred_wand = _ := seal_eq _.
Program Definition funbi_persistently_def {I B} : funbi_ty I B funbi_ty I B := λ P, FUN (λ i, bi_persistently (funbi_car P i)) _.
Program Definition monPred_persistently_def {I B} : monPred I B monPred I B := λ P, FUN (λ i, bi_persistently (monPred_car P i)) _.
Next Obligation.
intros I B P V1 V2 HV.
by apply bi.persistently_mono; intros; apply funbi_mono.
by apply bi.persistently_mono; intros; apply monPred_mono.
Qed.
Definition funbi_persistently_aux : seal (@funbi_persistently_def). by eexists. Qed.
Definition funbi_persistently {I B} := unseal funbi_persistently_aux I B.
Definition funbi_persistently_eq : @funbi_persistently = _ := seal_eq _.
Definition monPred_persistently_aux : seal (@monPred_persistently_def). by eexists. Qed.
Definition monPred_persistently {I B} := unseal monPred_persistently_aux I B.
Definition monPred_persistently_eq : @monPred_persistently = _ := seal_eq _.
Program Definition funbi_plainly_def {I B} : funbi_ty I B funbi_ty I B := λ P, FUN (λ i, bi_plainly (funbi_car P i)) _.
Program Definition monPred_plainly_def {I B} : monPred I B monPred I B := λ P, FUN (λ i, bi_plainly (monPred_car P i)) _.
Next Obligation.
intros I B P V1 V2 HV.
by apply bi.plainly_mono; intros; apply funbi_mono.
by apply bi.plainly_mono; intros; apply monPred_mono.
Qed.
Definition funbi_plainly_aux : seal (@funbi_plainly_def). by eexists. Qed.
Definition funbi_plainly {I B} := unseal funbi_plainly_aux I B.
Definition funbi_plainly_eq : @funbi_plainly = _ := seal_eq _.
Definition monPred_plainly_aux : seal (@monPred_plainly_def). by eexists. Qed.
Definition monPred_plainly {I B} := unseal monPred_plainly_aux I B.
Definition monPred_plainly_eq : @monPred_plainly = _ := seal_eq _.
Program Definition funbi_later_def {I} {B : sbi} (P : funbi_ty I B) : funbi_ty I B := FUN (λ i, (funbi_car P i))%I _.
Program Definition monPred_later_def {I} {B : sbi} (P : monPred I B) : monPred I B := FUN (λ i, (monPred_car P i))%I _.
Next Obligation.
intros I B P V1 V2 HV.
by apply bi.later_mono; intros; apply funbi_mono.
by apply bi.later_mono; intros; apply monPred_mono.
Qed.
Definition funbi_later_aux : seal (@funbi_later_def). by eexists. Qed.
Definition funbi_later {I B} := unseal funbi_later_aux I B.
Definition funbi_later_eq : @funbi_later = _ := seal_eq _.
Definition monPred_later_aux : seal (@monPred_later_def). by eexists. Qed.
Definition monPred_later {I B} := unseal monPred_later_aux I B.
Definition monPred_later_eq : @monPred_later = _ := seal_eq _.
Program Definition funbi_in_def {I B} (i_0 : bi_index_type I) : funbi_ty I B := FUN (λ i : I, i_0 i%I) _.
Program Definition monPred_in_def {I B} (i_0 : bi_index_type I) : monPred I B := FUN (λ i : I, i_0 i%I) _.
Next Obligation.
intros I B V V1 V2 HV.
by apply bi.pure_mono; intros; etrans.
Qed.
Definition funbi_in_aux : seal (@funbi_in_def). by eexists. Qed.
Definition funbi_in {I B} := unseal (@funbi_in_aux) I B.
Definition funbi_in_eq : @funbi_in = _ := seal_eq _.
Definition monPred_in_aux : seal (@monPred_in_def). by eexists. Qed.
Definition monPred_in {I B} := unseal (@monPred_in_aux) I B.
Definition monPred_in_eq : @monPred_in = _ := seal_eq _.
Lemma funbi_all_def_mono {I B} (P : funbi_ty I B) : mono () (λ _ : I, i, funbi_car P i)%I.
Lemma monPred_all_def_mono {I B} (P : monPred I B) : mono () (λ _ : I, i, monPred_car P i)%I.
Proof. apply _. Qed.
Program Definition funbi_all_def {I B} := λ (P : funbi_ty I B), FUN (λ _ : I, i, funbi_car P i)%I (funbi_all_def_mono P).
Definition funbi_all_aux : seal (@funbi_all_def). by eexists. Qed.
Definition funbi_all {I B} := unseal (@funbi_all_aux) I B.
Definition funbi_all_eq : @funbi_all = _ := seal_eq _.
Program Definition monPred_all_def {I B} := λ (P : monPred I B), FUN (λ _ : I, i, monPred_car P i)%I (monPred_all_def_mono P).
Definition monPred_all_aux : seal (@monPred_all_def). by eexists. Qed.
Definition monPred_all {I B} := unseal (@monPred_all_aux) I B.
Definition monPred_all_eq : @monPred_all = _ := seal_eq _.
Program Definition funbi_ipure_def {I B} P : funbi_ty I B := FUN (λ _, P) _.
Definition funbi_ipure_aux : seal (@funbi_ipure_def). by eexists. Qed.
Definition funbi_ipure {I B} := unseal funbi_ipure_aux I B.
Definition funbi_ipure_eq : @funbi_ipure = _ := seal_eq _.
Program Definition monPred_ipure_def {I B} P : monPred I B := FUN (λ _, P) _.
Definition monPred_ipure_aux : seal (@monPred_ipure_def). by eexists. Qed.
Definition monPred_ipure {I B} := unseal monPred_ipure_aux I B.
Definition monPred_ipure_eq : @monPred_ipure = _ := seal_eq _.
Local Definition unseal_eqs :=
(@funbi_pure_eq, @funbi_and_eq, @funbi_or_eq, @funbi_impl_eq, @funbi_forall_eq,
@funbi_exist_eq, @funbi_internal_eq_eq, @funbi_sep_eq, @funbi_wand_eq, @funbi_persistently_eq,
@funbi_plainly_eq,
@funbi_entails_eq, @funbi_later_eq, @funbi_in_eq, @funbi_all_eq, @funbi_ipure_eq
(@monPred_pure_eq, @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_plainly_eq,
@monPred_entails_eq, @monPred_later_eq, @monPred_in_eq, @monPred_all_eq, @monPred_ipure_eq
).
Lemma funbi_mixin I B :
BiMixin (@funbi_ofe_mixin I B) funbi_entails funbi_emp funbi_pure funbi_and funbi_or funbi_impl funbi_forall funbi_exist funbi_internal_eq funbi_sep funbi_wand funbi_plainly funbi_persistently.
Lemma monPred_bi_mixin I B :
BiMixin (@monPred_ofe_mixin I B) 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.
Proof.
rewrite !unseal_eqs.
split;
(* repeat setoid_rewrite funbi_entails_eq; repeat intro. *)
repeat (match goal with | [|- funbi_entails _ _ -> _] => intros [] end
(* repeat setoid_rewrite monPred_entails_eq; repeat intro. *)
repeat (match goal with | [|- monPred_entails _ _ -> _] => intros [] end
|| intro
);
try match goal with | [ |- funbi_entails _ _] => split => ? end.
try match goal with | [ |- monPred_entails _ _] => split => ? end.
- split.
+ intros ?. by econstructor.
+ intros ? ? ? [e1] [e2]. constructor => ?. by rewrite e1 e2.
......@@ -251,7 +254,7 @@ Proof.
- by apply bi.or_intro_r.
- by apply bi.or_elim.
- do 2!apply bi.forall_intro => ?.
rewrite -H funbi_mono //.
rewrite -H monPred_mono //.
apply: bi.impl_intro_l.
by rewrite (comm ()%I).
- do !setoid_rewrite bi.forall_elim in H; last reflexivity.
......@@ -262,7 +265,7 @@ Proof.
- apply bi.exist_elim => ?. by apply H.
- by apply bi.internal_eq_refl.
- do 2!apply bi.forall_intro => ? /=.
erewrite (bi.internal_eq_rewrite _ _ (λ c, funbi_car (Ψ c) _)) => //.
erewrite (bi.internal_eq_rewrite _ _ (λ c, monPred_car (Ψ c) _)) => //.
intros ? ? ? ?. by apply H.
- by apply bi.fun_ext.
- by apply bi.sig_eq.
......@@ -275,7 +278,7 @@ Proof.
- apply bi.forall_intro => ?.
apply bi.forall_intro => M.
apply bi.wand_intro_r.
rewrite (funbi_mono _ _ _ M). by apply H.
rewrite (monPred_mono _ _ _ M). by apply H.
- apply bi.wand_elim_l'.
by do !setoid_rewrite bi.forall_elim in H; last reflexivity.
- by apply bi.plainly_mono.
......@@ -308,14 +311,14 @@ Proof.
Admitted.
Canonical Structure funbi I B : bi :=
Bi (funbi_ty I B) funbi_dist funbi_equiv funbi_entails funbi_emp funbi_pure funbi_and funbi_or funbi_impl funbi_forall funbi_exist funbi_internal_eq funbi_sep funbi_wand funbi_plainly funbi_persistently funbi_ofe_mixin (funbi_mixin _ _).
Canonical Structure monPredI I B : bi :=
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 monPred_persistently monPred_ofe_mixin (monPred_bi_mixin _ _).
Instance funbi_affine I B : BiAffine B BiAffine (funbi I B).
Instance monPred_affine I B : BiAffine B BiAffine (monPredI I B).
Proof. split => ?. by apply affine. Qed.
Arguments funbi_ofe _ _ : clear implicits.
Arguments funbi _ _ : clear implicits.
Arguments monPred_ofe _ _ : clear implicits.
Arguments monPred _ _ : clear implicits.
Module Prelim.
Ltac unseal := rewrite
......@@ -329,32 +332,32 @@ Module Prelim.
!unseal_eqs /=.
End Prelim.
Lemma funbi_wand_force I B (P Q : funbi I B) i:
funbi_car (P - Q) i - (funbi_car P i - funbi_car Q i).
Lemma monPred_wand_force I B (P Q : monPred I B) i:
monPred_car (P - Q) i - (monPred_car P i - monPred_car Q i).
Proof. Prelim.unseal. by rewrite !bi.forall_elim. Qed.
Lemma funbi_impl_force I B (P Q : funbi I B) i:
funbi_car (P Q) i - (funbi_car P i funbi_car Q i).
Lemma monPred_impl_force I B (P Q : monPred I B) i:
monPred_car (P Q) i - (monPred_car P i monPred_car Q i).
Proof. Prelim.unseal. by rewrite !bi.forall_elim. Qed.
Lemma funbi_persistently_if_eq I B p (P : funbi I B) i:
funbi_car (bi_persistently_if p P) i = bi_persistently_if p (funbi_car P i).
Lemma monPred_persistently_if_eq I B p (P : monPred I B) i:
monPred_car (bi_persistently_if p P) i = bi_persistently_if p (monPred_car P i).
Proof. rewrite /bi_persistently_if. Prelim.unseal. by destruct p. Qed.
Lemma funbi_plainly_if_eq I B p (P : funbi I B) i:
funbi_car (bi_plainly_if p P) i = bi_plainly_if p (funbi_car P i).
Lemma monPred_plainly_if_eq I B p (P : monPred I B) i:
monPred_car (bi_plainly_if p P) i = bi_plainly_if p (monPred_car P i).
Proof. rewrite /bi_plainly_if. Prelim.unseal. by destruct p. Qed.
Lemma funbi_affinely_if_eq I B p (P : funbi I B) i:
funbi_car (bi_affinely_if p P) i = bi_affinely_if p (funbi_car P i).
Lemma monPred_affinely_if_eq I B p (P : monPred I B) i:
monPred_car (bi_affinely_if p P) i = bi_affinely_if p (monPred_car P i).
Proof. rewrite /bi_affinely_if. destruct p => //. rewrite /bi_affinely. by Prelim.unseal. Qed.
Lemma funsbi_mixin I (B : sbi) :
SbiMixin (PROP:=funbi I B) funbi_entails funbi_pure funbi_or funbi_impl funbi_forall funbi_exist funbi_internal_eq funbi_sep funbi_plainly funbi_persistently funbi_later.
Lemma monPred_sbi_mixin I (B : sbi) :
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.
Proof.
intros.
Prelim.unseal.
split; repeat setoid_rewrite funbi_entails_eq; repeat intro.
split; repeat setoid_rewrite monPred_entails_eq; repeat intro.
- apply bi.later_contractive. rewrite /dist_later in H. destruct n => //. by apply H.
- by apply bi.later_eq_1.
- by apply bi.later_eq_2.
......@@ -370,62 +373,65 @@ Proof.
- by apply bi.later_persistently_2.
- rewrite /= -bi.forall_intro. apply bi.later_false_em.
intros. rewrite <-bi.forall_intro. reflexivity.
intros. by rewrite funbi_mono.
intros. by rewrite monPred_mono.
Qed.
Canonical Structure funsbi I (B : sbi) : sbi :=
Sbi (funbi_ty I B) funbi_dist funbi_equiv funbi_entails funbi_emp funbi_pure funbi_and funbi_or funbi_impl funbi_forall funbi_exist funbi_internal_eq funbi_sep funbi_wand funbi_plainly funbi_persistently funbi_later funbi_ofe_mixin (bi_bi_mixin _) (funsbi_mixin _ _).
Ltac unseal := rewrite
/(@sbi_except_0 (funsbi _ _))
/(@bi_emp (funbi _ _)) /=
/(@bi_pure (funbi _ _))
/(@bi_and (funbi _ _))
/(@bi_or (funbi _ _))
/(@bi_impl (funbi _ _))
/(@bi_forall (funbi _ _))
/(@bi_exist (funbi _ _))
/(@bi_internal_eq (funbi _ _))
/(@bi_sep (funbi _ _))
/(@bi_wand (funbi _ _))
/(@bi_persistently (funbi _ _))
/(@sbi_later (funsbi _ _)) /=
/(@sbi_emp (funsbi _ _))
/(@sbi_pure (funsbi _ _))
/(@sbi_and (funsbi _ _))
/(@sbi_or (funsbi _ _))
/(@sbi_impl (funsbi _ _))
/(@sbi_forall (funsbi _ _))
/(@sbi_exist (funsbi _ _))
/(@sbi_internal_eq (funsbi _ _))
/(@sbi_sep (funsbi _ _))
/(@sbi_wand (funsbi _ _))
/(@sbi_persistently (funsbi _ _))
Canonical Structure monPredSI I (B : sbi) : sbi :=