Commit cedd9645 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Force all the BI morphisms to use the ⎡P⎤ notation.

parent 9c68a663
......@@ -2299,38 +2299,38 @@ Hint Immediate bi.plain_persistent : typeclass_instances.
(* BI morphisms *)
Section bi_morphims.
Context `{@BiMorphism PROP1 PROP2 mor}.
Context `{BiMorphism PROP1 PROP2}.
Global Instance bi_mor_proper : Proper (() ==> ()) mor.
Global Instance bi_mor_proper : Proper (() ==> ()) bi_embedding.
Proof. apply (ne_proper _). Qed.
Global Instance bi_mor_mono_flip : Proper (flip () ==> flip ()) mor.
Global Instance bi_mor_mono_flip : Proper (flip () ==> flip ()) bi_embedding.
Proof. solve_proper. Qed.
Lemma bi_mor_forall A (Φ : A PROP1) : mor ( x, Φ x) ( x, mor (Φ x)).
Lemma bi_mor_forall A (Φ : A PROP1) : x, Φ x x, ⎡Φ x.
Proof.
apply bi.equiv_spec; split; [|apply bi_mor_forall_2].
apply bi.forall_intro=>?. by rewrite bi.forall_elim.
Qed.
Lemma bi_mor_exist A (Φ : A PROP1) : mor ( x, Φ x) ( x, mor (Φ x)).
Lemma bi_mor_exist A (Φ : A PROP1) : x, Φ x x, ⎡Φ x.
Proof.
apply bi.equiv_spec; split; [apply bi_mor_exist_1|].
apply bi.exist_elim=>?. by rewrite -bi.exist_intro.
Qed.
Lemma bi_mor_and P Q : mor (P Q) mor P mor Q.
Lemma bi_mor_and P Q : P Q P Q.
Proof. rewrite !bi.and_alt bi_mor_forall. by f_equiv=>-[]. Qed.
Lemma bi_mor_or P Q : mor (P Q) mor P mor Q.
Lemma bi_mor_or P Q : P Q P Q.
Proof. rewrite !bi.or_alt bi_mor_exist. by f_equiv=>-[]. Qed.
Lemma bi_mor_impl P Q : mor (P Q) (mor P mor Q).
Lemma bi_mor_impl P Q : P Q (P Q).
Proof.
apply bi.equiv_spec; split; [|apply bi_mor_impl_2].
apply bi.impl_intro_l. by rewrite -bi_mor_and bi.impl_elim_r.
Qed.
Lemma bi_mor_wand P Q : mor (P - Q) (mor P - mor Q).
Lemma bi_mor_wand P Q : P - Q (P - Q).
Proof.
apply bi.equiv_spec; split; [|apply bi_mor_wand_2].
apply bi.wand_intro_l. by rewrite -bi_mor_sep bi.wand_elim_r.
Qed.
Lemma bi_mor_pure φ : mor ⌜φ⌝ ⌜φ⌝.
Lemma bi_mor_pure φ : ⎡⌜φ⌝⎤ ⌜φ⌝.
Proof.
rewrite (@bi.pure_alt PROP1) (@bi.pure_alt PROP2) bi_mor_exist.
do 2 f_equiv. apply bi.equiv_spec. split; [apply bi.True_intro|].
......@@ -2338,56 +2338,54 @@ Section bi_morphims.
last apply bi.True_intro.
apply bi.impl_intro_l. by rewrite right_id.
Qed.
Lemma bi_mor_internal_eq (A : ofeT) (x y : A) : mor (x y) (x y).
Lemma bi_mor_internal_eq (A : ofeT) (x y : A) : x y x y.
Proof.
apply bi.equiv_spec; split; [apply bi_mor_internal_eq_1|].
rewrite (bi.internal_eq_rewrite x y (λ y, mor (x y)%I) _); [|solve_proper].
etrans; [apply (bi.internal_eq_rewrite x y (λ y, x y%I)); solve_proper|].
rewrite -(bi.internal_eq_refl True%I) bi_mor_pure.
eapply bi.impl_elim; [done|]. apply bi.True_intro.
Qed.
Lemma bi_mor_iff P Q : mor (P Q) (mor P mor Q).
Lemma bi_mor_iff P Q : P Q (P Q).
Proof. by rewrite bi_mor_and !bi_mor_impl. Qed.
Lemma bi_mor_wand_iff P Q : mor (P - Q) (mor P - mor Q).
Lemma bi_mor_wand_iff P Q : P - Q (P - Q).
Proof. by rewrite bi_mor_and !bi_mor_wand. Qed.
Lemma bi_mor_affinely P : mor (bi_affinely P) bi_affinely (mor P).
Lemma bi_mor_affinely P : bi_affinely P bi_affinely P.
Proof. by rewrite bi_mor_and bi_mor_emp. Qed.
Lemma bi_mor_absorbingly P : mor (bi_absorbingly P) bi_absorbingly (mor P).
Lemma bi_mor_absorbingly P : bi_absorbingly P bi_absorbingly P.
Proof. by rewrite bi_mor_sep bi_mor_pure. Qed.
Lemma bi_mor_plainly_if P b :
mor (bi_plainly_if b P) bi_plainly_if b (mor P).
Lemma bi_mor_plainly_if P b : bi_plainly_if b P bi_plainly_if b P.
Proof. destruct b; auto using bi_mor_plainly. Qed.
Lemma bi_mor_persistently_if P b :
mor (bi_persistently_if b P) bi_persistently_if b (mor P).
bi_persistently_if b P bi_persistently_if b P.
Proof. destruct b; auto using bi_mor_persistently. Qed.
Lemma bi_mor_affinely_if P b :
mor (bi_affinely_if b P) bi_affinely_if b (mor P).
Lemma bi_mor_affinely_if P b : bi_affinely_if b P bi_affinely_if b P.
Proof. destruct b; simpl; auto using bi_mor_affinely. Qed.
Lemma bi_mor_hforall {As} (Φ : himpl As PROP1):
mor (bi_hforall Φ) bi_hforall (hcompose mor Φ).
bi_hforall Φ⎤ bi_hforall (hcompose bi_embedding Φ).
Proof. induction As=>//. rewrite /= bi_mor_forall. by do 2 f_equiv. Qed.
Lemma bi_mor_hexist {As} (Φ : himpl As PROP1):
mor (bi_hexist Φ) bi_hexist (hcompose mor Φ).
bi_hexist Φ⎤ bi_hexist (hcompose bi_embedding Φ).
Proof. induction As=>//. rewrite /= bi_mor_exist. by do 2 f_equiv. Qed.
Global Instance bi_mor_plain P : Plain P Plain (mor P).
Global Instance bi_mor_plain P : Plain P Plain P.
Proof. intros ?. by rewrite /Plain -bi_mor_plainly -plain. Qed.
Global Instance bi_mor_persistent P : Persistent P Persistent (mor P).
Global Instance bi_mor_persistent P : Persistent P Persistent P.
Proof. intros ?. by rewrite /Persistent -bi_mor_persistently -persistent. Qed.
Global Instance bi_mor_affine P : Affine P Affine (mor P).
Global Instance bi_mor_affine P : Affine P Affine P.
Proof. intros ?. by rewrite /Affine (affine P) bi_mor_emp. Qed.
Global Instance bi_mor_absorbing P : Absorbing P Absorbing (mor P).
Global Instance bi_mor_absorbing P : Absorbing P Absorbing P.
Proof. intros ?. by rewrite /Absorbing -bi_mor_absorbingly absorbing. Qed.
End bi_morphims.
Section sbi_morphims.
Context `{@SbiMorphism PROP1 PROP2 mor}.
Context `{SbiMorphism PROP1 PROP2}.
Lemma sbi_mor_laterN n P : mor (^n P) ^n (mor P).
Lemma sbi_mor_laterN n P : ⎡▷^n P ^n P.
Proof. induction n=>//=. rewrite sbi_mor_later. by f_equiv. Qed.
Lemma sbi_mor_except_0 P : mor ( P) (mor P).
Lemma sbi_mor_except_0 P : ⎡◇ P P.
Proof. by rewrite bi_mor_or sbi_mor_later bi_mor_pure. Qed.
Global Instance sbi_mor_timeless P : Timeless P Timeless (mor P).
Global Instance sbi_mor_timeless P : Timeless P Timeless P.
Proof.
intros ?. by rewrite /Timeless -sbi_mor_except_0 -sbi_mor_later timeless.
Qed.
......
......@@ -526,28 +526,28 @@ End sbi_laws.
End bi.
(* Typically, embeddings are used to *define* the destination BI.
Hence we cannot ask B to be a BI. *)
Hence we cannot ask it to be a morphism. *)
Class BiEmbedding (A B : Type) := bi_embedding : A B.
Arguments bi_embedding {_ _ _} _%I : simpl never.
Notation "⎡ P ⎤" := (bi_embedding P) : bi_scope.
Instance: Params (@bi_embedding) 3.
Typeclasses Opaque bi_embedding.
Class BiMorphism {PROP1 PROP2 : bi} (f : PROP1 PROP2) := {
bi_mor_ne :> NonExpansive f;
bi_mor_mono :> Proper (() ==> ()) f;
bi_mor_emp : f emp emp;
bi_mor_impl_2 P Q : (f P f Q)%I f (P Q)%I;
bi_mor_forall_2 A (Φ : A PROP1) : ( x, f (Φ x)) f ( x, Φ x);
bi_mor_exist_1 A (Φ : A PROP1) : f ( x, Φ x) x, f (Φ x);
bi_mor_internal_eq_1 (A : ofeT) (x y : A) : f (x y) (x y);
bi_mor_sep P Q : f (P Q) (f P f Q);
bi_mor_wand_2 P Q : (f P - f Q) f (P - Q);
bi_mor_plainly P : f (bi_plainly P) bi_plainly (f P);
bi_mor_persistently P : f (bi_persistently P) bi_persistently (f P)
Class BiMorphism (PROP1 PROP2 : bi) `{BiEmbedding PROP1 PROP2} := {
bi_mor_ne :> NonExpansive bi_embedding;
bi_mor_mono :> Proper (() ==> ()) bi_embedding;
bi_mor_emp : emp emp;
bi_mor_impl_2 P Q : (P Q) P Q;
bi_mor_forall_2 A (Φ : A PROP1) : ( x, ⎡Φ x) x, Φ x;
bi_mor_exist_1 A (Φ : A PROP1) : x, Φ x x, ⎡Φ x;
bi_mor_internal_eq_1 (A : ofeT) (x y : A) : x y x y;
bi_mor_sep P Q : P Q P Q;
bi_mor_wand_2 P Q : (P - Q) P - Q;
bi_mor_plainly P : bi_plainly P bi_plainly P;
bi_mor_persistently P : bi_persistently P bi_persistently P
}.
Class SbiMorphism {PROP1 PROP2 : sbi} (f : PROP1 PROP2) := {
sbi_mor_bi_mor :> BiMorphism f;
sbi_mor_later P : f ( P) f P
Class SbiMorphism (PROP1 PROP2 : sbi) `{BiEmbedding PROP1 PROP2} := {
sbi_mor_bi_mor :> BiMorphism PROP1 PROP2;
sbi_mor_later P : ⎡▷ P P
}.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment