Commit 39967f22 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Renaming : morphism -> embedding.

parent 858d6407
......@@ -2297,106 +2297,106 @@ only be used at the leaves of the proof search tree, i.e. when the
premise of the hint can be derived from just the current context. *)
Hint Immediate bi.plain_persistent : typeclass_instances.
(* BI morphisms *)
Section bi_morphims.
Context `{BiMorphism PROP1 PROP2}.
(* BI embeddings *)
Section bi_embedding.
Context `{BiEmbedding PROP1 PROP2}.
Global Instance bi_mor_proper : Proper (() ==> ()) bi_embedding.
Global Instance bi_embed_proper : Proper (() ==> ()) bi_embed.
Proof. apply (ne_proper _). Qed.
Global Instance bi_mor_mono_flip : Proper (flip () ==> flip ()) bi_embedding.
Global Instance bi_embed_mono_flip : Proper (flip () ==> flip ()) bi_embed.
Proof. solve_proper. Qed.
Global Instance bi_mor_inj : Inj () () bi_embedding.
Global Instance bi_embed_inj : Inj () () bi_embed.
Proof.
intros ?? EQ. apply bi.equiv_spec, conj; apply (inj bi_embedding);
intros ?? EQ. apply bi.equiv_spec, conj; apply (inj bi_embed);
rewrite EQ //.
Qed.
Lemma bi_mor_valid (P : PROP1) : @bi_embedding PROP1 PROP2 _ P P.
Lemma bi_embed_valid (P : PROP1) : @bi_embed PROP1 PROP2 _ P P.
Proof.
by rewrite /bi_valid -bi_mor_emp; split=>?; [apply (inj bi_embedding)|f_equiv].
by rewrite /bi_valid -bi_embed_emp; split=>?; [apply (inj bi_embed)|f_equiv].
Qed.
Lemma bi_mor_forall A (Φ : A PROP1) : x, Φ x x, ⎡Φ x.
Lemma bi_embed_forall A (Φ : A PROP1) : x, Φ x x, ⎡Φ x.
Proof.
apply bi.equiv_spec; split; [|apply bi_mor_forall_2].
apply bi.equiv_spec; split; [|apply bi_embed_forall_2].
apply bi.forall_intro=>?. by rewrite bi.forall_elim.
Qed.
Lemma bi_mor_exist A (Φ : A PROP1) : x, Φ x x, ⎡Φ x.
Lemma bi_embed_exist A (Φ : A PROP1) : x, Φ x x, ⎡Φ x.
Proof.
apply bi.equiv_spec; split; [apply bi_mor_exist_1|].
apply bi.equiv_spec; split; [apply bi_embed_exist_1|].
apply bi.exist_elim=>?. by rewrite -bi.exist_intro.
Qed.
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 : P Q P Q.
Proof. rewrite !bi.or_alt bi_mor_exist. by f_equiv=>-[]. Qed.
Lemma bi_mor_impl P Q : P Q (P Q).
Lemma bi_embed_and P Q : P Q P Q.
Proof. rewrite !bi.and_alt bi_embed_forall. by f_equiv=>-[]. Qed.
Lemma bi_embed_or P Q : P Q P Q.
Proof. rewrite !bi.or_alt bi_embed_exist. by f_equiv=>-[]. Qed.
Lemma bi_embed_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.
apply bi.equiv_spec; split; [|apply bi_embed_impl_2].
apply bi.impl_intro_l. by rewrite -bi_embed_and bi.impl_elim_r.
Qed.
Lemma bi_mor_wand P Q : P - Q (P - Q).
Lemma bi_embed_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.
apply bi.equiv_spec; split; [|apply bi_embed_wand_2].
apply bi.wand_intro_l. by rewrite -bi_embed_sep bi.wand_elim_r.
Qed.
Lemma bi_mor_pure φ : ⎡⌜φ⌝⎤ ⌜φ⌝.
Lemma bi_embed_pure φ : ⎡⌜φ⌝⎤ ⌜φ⌝.
Proof.
rewrite (@bi.pure_alt PROP1) (@bi.pure_alt PROP2) bi_mor_exist.
rewrite (@bi.pure_alt PROP1) (@bi.pure_alt PROP2) bi_embed_exist.
do 2 f_equiv. apply bi.equiv_spec. split; [apply bi.True_intro|].
rewrite -(_ : (emp emp : PROP1) True) ?bi_mor_impl;
rewrite -(_ : (emp emp : PROP1) True) ?bi_embed_impl;
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) : x y x y.
Lemma bi_embed_internal_eq (A : ofeT) (x y : A) : x y x y.
Proof.
apply bi.equiv_spec; split; [apply bi_mor_internal_eq_1|].
apply bi.equiv_spec; split; [apply bi_embed_internal_eq_1|].
etrans; [apply (bi.internal_eq_rewrite x y (λ y, x y%I)); solve_proper|].
rewrite -(bi.internal_eq_refl True%I) bi_mor_pure.
rewrite -(bi.internal_eq_refl True%I) bi_embed_pure.
eapply bi.impl_elim; [done|]. apply bi.True_intro.
Qed.
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 : P - Q (P - Q).
Proof. by rewrite bi_mor_and !bi_mor_wand. Qed.
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 : bi_absorbingly P bi_absorbingly P.
Proof. by rewrite bi_mor_sep bi_mor_pure. Qed.
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 :
Lemma bi_embed_iff P Q : P Q (P Q).
Proof. by rewrite bi_embed_and !bi_embed_impl. Qed.
Lemma bi_embed_wand_iff P Q : P - Q (P - Q).
Proof. by rewrite bi_embed_and !bi_embed_wand. Qed.
Lemma bi_embed_affinely P : bi_affinely P bi_affinely P.
Proof. by rewrite bi_embed_and bi_embed_emp. Qed.
Lemma bi_embed_absorbingly P : bi_absorbingly P bi_absorbingly P.
Proof. by rewrite bi_embed_sep bi_embed_pure. Qed.
Lemma bi_embed_plainly_if P b : bi_plainly_if b P bi_plainly_if b P.
Proof. destruct b; auto using bi_embed_plainly. Qed.
Lemma bi_embed_persistently_if P b :
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 : 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):
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):
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 P.
Proof. intros ?. by rewrite /Plain -bi_mor_plainly -plain. Qed.
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 P.
Proof. intros ?. by rewrite /Affine (affine P) bi_mor_emp. Qed.
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}.
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 : ⎡◇ P P.
Proof. by rewrite bi_mor_or sbi_mor_later bi_mor_pure. Qed.
Global Instance sbi_mor_timeless P : Timeless P Timeless P.
Proof. destruct b; auto using bi_embed_persistently. Qed.
Lemma bi_embed_affinely_if P b : bi_affinely_if b P bi_affinely_if b P.
Proof. destruct b; simpl; auto using bi_embed_affinely. Qed.
Lemma bi_embed_hforall {As} (Φ : himpl As PROP1):
bi_hforall Φ⎤ bi_hforall (hcompose bi_embed Φ).
Proof. induction As=>//. rewrite /= bi_embed_forall. by do 2 f_equiv. Qed.
Lemma bi_embed_hexist {As} (Φ : himpl As PROP1):
bi_hexist Φ⎤ bi_hexist (hcompose bi_embed Φ).
Proof. induction As=>//. rewrite /= bi_embed_exist. by do 2 f_equiv. Qed.
Global Instance bi_embed_plain P : Plain P Plain P.
Proof. intros ?. by rewrite /Plain -bi_embed_plainly -plain. Qed.
Global Instance bi_embed_persistent P : Persistent P Persistent P.
Proof. intros ?. by rewrite /Persistent -bi_embed_persistently -persistent. Qed.
Global Instance bi_embed_affine P : Affine P Affine P.
Proof. intros ?. by rewrite /Affine (affine P) bi_embed_emp. Qed.
Global Instance bi_embed_absorbing P : Absorbing P Absorbing P.
Proof. intros ?. by rewrite /Absorbing -bi_embed_absorbingly absorbing. Qed.
End bi_embedding.
Section sbi_embedding.
Context `{SbiEmbedding PROP1 PROP2}.
Lemma sbi_embed_laterN n P : ⎡▷^n P ^n P.
Proof. induction n=>//=. rewrite sbi_embed_later. by f_equiv. Qed.
Lemma sbi_embed_except_0 P : ⎡◇ P P.
Proof. by rewrite bi_embed_or sbi_embed_later bi_embed_pure. Qed.
Global Instance sbi_embed_timeless P : Timeless P Timeless P.
Proof.
intros ?. by rewrite /Timeless -sbi_mor_except_0 -sbi_mor_later timeless.
intros ?. by rewrite /Timeless -sbi_embed_except_0 -sbi_embed_later timeless.
Qed.
End sbi_morphims.
\ No newline at end of file
End sbi_embedding.
\ No newline at end of file
......@@ -526,29 +526,29 @@ End sbi_laws.
End bi.
(* Typically, embeddings are used to *define* the destination 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) `{BiEmbedding PROP1 PROP2} := {
bi_mor_ne :> NonExpansive bi_embedding;
bi_mor_mono :> Proper (() ==> ()) bi_embedding;
bi_mor_entails_inj :> Inj () () 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
Hence we cannot ask it to verify the properties of embeddings. *)
Class BiEmbed (A B : Type) := bi_embed : A B.
Arguments bi_embed {_ _ _} _%I : simpl never.
Notation "⎡ P ⎤" := (bi_embed P) : bi_scope.
Instance: Params (@bi_embed) 3.
Typeclasses Opaque bi_embed.
Class BiEmbedding (PROP1 PROP2 : bi) `{BiEmbed PROP1 PROP2} := {
bi_embed_ne :> NonExpansive bi_embed;
bi_embed_mono :> Proper (() ==> ()) bi_embed;
bi_embed_entails_inj :> Inj () () bi_embed;
bi_embed_emp : emp emp;
bi_embed_impl_2 P Q : (P Q) P Q;
bi_embed_forall_2 A (Φ : A PROP1) : ( x, ⎡Φ x) x, Φ x;
bi_embed_exist_1 A (Φ : A PROP1) : x, Φ x x, ⎡Φ x;
bi_embed_internal_eq_1 (A : ofeT) (x y : A) : x y x y;
bi_embed_sep P Q : P Q P Q;
bi_embed_wand_2 P Q : (P - Q) P - Q;
bi_embed_plainly P : bi_plainly P bi_plainly P;
bi_embed_persistently P : bi_persistently P bi_persistently P
}.
Class SbiMorphism (PROP1 PROP2 : sbi) `{BiEmbedding PROP1 PROP2} := {
sbi_mor_bi_mor :> BiMorphism PROP1 PROP2;
sbi_mor_later P : ⎡▷ P P
Class SbiEmbedding (PROP1 PROP2 : sbi) `{BiEmbed PROP1 PROP2} := {
sbi_embed_bi_embed :> BiEmbedding PROP1 PROP2;
sbi_embed_later P : ⎡▷ P P
}.
......@@ -116,10 +116,10 @@ Program Definition monPred_upclosed (Φ : I → PROP) : monPred :=
MonPred (λ i, ( j, i j Φ j)%I) _.
Next Obligation. solve_proper. Qed.
Definition monPred_ipure_def (P : PROP) : monPred := MonPred (λ _, P) _.
Definition monPred_ipure_aux : seal (@monPred_ipure_def). by eexists. Qed.
Global Instance monPred_ipure : BiEmbedding PROP monPred := unseal monPred_ipure_aux.
Definition monPred_ipure_eq : bi_embedding = _ := seal_eq _.
Definition monPred_embed_def (P : PROP) : monPred := MonPred (λ _, P) _.
Definition monPred_embed_aux : seal (@monPred_embed_def). by eexists. Qed.
Global Instance monPred_embed : BiEmbed PROP monPred := unseal monPred_embed_aux.
Definition monPred_embed_eq : bi_embed = _ := seal_eq _.
Definition monPred_pure (φ : Prop) : monPred := ⎡⌜φ⌝⎤%I.
Definition monPred_emp : monPred := emp%I.
......@@ -215,7 +215,7 @@ Definition unseal_eqs :=
@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).
@monPred_in_eq, @monPred_all_eq, @monPred_embed_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,
......@@ -464,8 +464,8 @@ Proof.
by apply affine, bi.forall_affine.
Qed.
Global Instance monPred_ipure_bi_mor :
Inhabited I @BiMorphism PROP (monPredI I PROP) bi_embedding.
Global Instance monPred_bi_embedding :
Inhabited I @BiEmbedding PROP (monPredI I PROP) bi_embed.
Proof.
split; try apply _; unseal; try done.
- move =>?? /= [/(_ inhabitant) ?] //.
......@@ -485,7 +485,7 @@ Implicit Types P Q : monPred I PROP.
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 : PROP) :
Global Instance monPred_embed_timeless (P : PROP) :
Timeless P @Timeless (monPredSI I PROP) P%I.
Proof. intros. split => ? /=. by unseal. Qed.
Global Instance monPred_in_timeless i0 : Timeless (@monPred_in I PROP i0).
......@@ -497,7 +497,7 @@ Proof.
by apply timeless, bi.forall_timeless.
Qed.
Global Instance monPred_ipure_sbi_mor :
Inhabited I @SbiMorphism PROP (monPredSI I PROP) bi_embedding.
Global Instance monPred_sbi_embedding :
Inhabited I @SbiEmbedding PROP (monPredSI I PROP) bi_embed.
Proof. split; try apply _. by unseal. Qed.
End sbi_facts.
......@@ -115,9 +115,9 @@ Proof. rewrite /IntoPure=> ->. apply: plainly_elim. Qed.
Global Instance into_pure_persistently P φ :
IntoPure P φ IntoPure (bi_persistently P) φ.
Proof. rewrite /IntoPure=> ->. apply: persistently_elim. Qed.
Global Instance into_pure_morphism `{BiMorphism PROP PROP'} P φ :
Global Instance into_pure_embed `{BiEmbedding PROP PROP'} P φ :
IntoPure P φ IntoPure P φ.
Proof. rewrite /IntoPure=> ->. by rewrite bi_mor_pure. Qed.
Proof. rewrite /IntoPure=> ->. by rewrite bi_embed_pure. Qed.
(* FromPure *)
Global Instance from_pure_pure φ : @FromPure PROP ⌜φ⌝ φ.
......@@ -164,9 +164,9 @@ Global Instance from_pure_affinely P φ `{!Affine P} :
Proof. by rewrite /FromPure affine_affinely. Qed.
Global Instance from_pure_absorbingly P φ : FromPure P φ FromPure (bi_absorbingly P) φ.
Proof. rewrite /FromPure=> <-. by rewrite absorbingly_pure. Qed.
Global Instance from_pure_morphism `{BiMorphism PROP PROP'} P φ :
Global Instance from_pure_embed `{BiEmbedding PROP PROP'} P φ :
FromPure P φ FromPure P φ.
Proof. rewrite /FromPure=> <-. by rewrite bi_mor_pure. Qed.
Proof. rewrite /FromPure=> <-. by rewrite bi_embed_pure. Qed.
(* IntoInternalEq *)
Global Instance into_internal_eq_internal_eq {A : ofeT} (x y : A) :
......@@ -184,10 +184,10 @@ Proof. rewrite /IntoInternalEq=> ->. by rewrite plainly_elim. Qed.
Global Instance into_internal_eq_persistently {A : ofeT} (x y : A) P :
IntoInternalEq P x y IntoInternalEq (bi_persistently P) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite persistently_elim. Qed.
Global Instance into_internal_eq_morphism
`{BiMorphism PROP PROP'} {A : ofeT} (x y : A) P :
Global Instance into_internal_eq_embed
`{BiEmbedding PROP PROP'} {A : ofeT} (x y : A) P :
IntoInternalEq P x y IntoInternalEq P x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite bi_mor_internal_eq. Qed.
Proof. rewrite /IntoInternalEq=> ->. by rewrite bi_embed_internal_eq. Qed.
(* IntoPersistent *)
Global Instance into_persistent_persistently p P Q :
......@@ -199,10 +199,10 @@ Qed.
Global Instance into_persistent_affinely p P Q :
IntoPersistent p P Q IntoPersistent p (bi_affinely P) Q | 0.
Proof. rewrite /IntoPersistent /= => <-. by rewrite affinely_elim. Qed.
Global Instance into_persistent_morphism `{BiMorphism PROP PROP'} p P Q :
Global Instance into_persistent_embed `{BiEmbedding PROP PROP'} p P Q :
IntoPersistent p P Q IntoPersistent p P Q | 0.
Proof.
rewrite /IntoPersistent -bi_mor_persistently -bi_mor_persistently_if=> -> //.
rewrite /IntoPersistent -bi_embed_persistently -bi_embed_persistently_if=> -> //.
Qed.
Global Instance into_persistent_here P : IntoPersistent true P P | 1.
Proof. by rewrite /IntoPersistent. Qed.
......@@ -231,11 +231,11 @@ Global Instance from_always_affinely a pe pl P Q :
Proof.
rewrite /FromAlways /= => <-. destruct a; by rewrite /= ?affinely_idemp.
Qed.
Global Instance from_always_morphism `{BiMorphism PROP PROP'} a pe pl P Q :
Global Instance from_always_embed `{BiEmbedding PROP PROP'} a pe pl P Q :
FromAlways a pe pl P Q FromAlways a pe pl P Q | 0.
Proof.
rewrite /FromAlways=><-.
by rewrite bi_mor_affinely_if bi_mor_persistently_if bi_mor_plainly_if.
by rewrite bi_embed_affinely_if bi_embed_persistently_if bi_embed_plainly_if.
Qed.
(* IntoWand *)
......@@ -323,11 +323,11 @@ Proof. by rewrite /IntoWand /= persistently_idemp. Qed.
Global Instance into_wand_persistently_false `{!BiAffine PROP} q R P Q :
IntoWand false q R P Q IntoWand false q (bi_persistently R) P Q.
Proof. by rewrite /IntoWand persistently_elim. Qed.
Global Instance into_wand_Morphism `{BiMorphism PROP PROP'} p q R P Q :
Global Instance into_wand_embed `{BiEmbedding PROP PROP'} p q R P Q :
IntoWand p q R P Q IntoWand p q R P Q.
Proof.
rewrite /IntoWand -!bi_mor_persistently_if -!bi_mor_affinely_if
-bi_mor_wand => -> //.
rewrite /IntoWand -!bi_embed_persistently_if -!bi_embed_affinely_if
-bi_embed_wand => -> //.
Qed.
(* FromAnd *)
......@@ -370,9 +370,9 @@ Global Instance from_and_persistently_sep P Q1 Q2 :
FromAnd (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2) | 11.
Proof. rewrite /FromAnd=> <-. by rewrite -persistently_and persistently_and_sep. Qed.
Global Instance from_and_morphism `{BiMorphism PROP PROP'} P Q1 Q2 :
Global Instance from_and_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
FromAnd P Q1 Q2 FromAnd P Q1 Q2.
Proof. by rewrite /FromAnd -bi_mor_and => <-. Qed.
Proof. by rewrite /FromAnd -bi_embed_and => <-. Qed.
Global Instance from_and_big_sepL_cons_persistent {A} (Φ : nat A PROP) x l :
Persistent (Φ 0 x)
......@@ -410,9 +410,9 @@ Global Instance from_sep_persistently P Q1 Q2 :
FromSep (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Proof. rewrite /FromSep=> <-. by rewrite persistently_sep_2. Qed.
Global Instance from_sep_morphism `{BiMorphism PROP PROP'} P Q1 Q2 :
Global Instance from_sep_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
FromSep P Q1 Q2 FromSep P Q1 Q2.
Proof. by rewrite /FromSep -bi_mor_sep => <-. Qed.
Proof. by rewrite /FromSep -bi_embed_sep => <-. Qed.
Global Instance from_sep_big_sepL_cons {A} (Φ : nat A PROP) x l :
FromSep ([ list] k y x :: l, Φ k y) (Φ 0 x) ([ list] k y l, Φ (S k) y).
......@@ -471,11 +471,11 @@ Proof.
- by rewrite -persistently_and !persistently_idemp.
- intros ->. by rewrite persistently_and.
Qed.
Global Instance into_and_morphism `{BiMorphism PROP PROP'} p P Q1 Q2 :
Global Instance into_and_embed `{BiEmbedding PROP PROP'} p P Q1 Q2 :
IntoAnd p P Q1 Q2 IntoAnd p P Q1 Q2.
Proof.
rewrite /IntoAnd -bi_mor_and -!bi_mor_persistently_if
-!bi_mor_affinely_if=> -> //.
rewrite /IntoAnd -bi_embed_and -!bi_embed_persistently_if
-!bi_embed_affinely_if=> -> //.
Qed.
(* IntoSep *)
......@@ -510,9 +510,9 @@ Qed.
Global Instance into_sep_pure φ ψ : @IntoSep PROP ⌜φ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /IntoSep pure_and persistent_and_sep_1. Qed.
Global Instance into_sep_morphism `{BiMorphism PROP PROP'} P Q1 Q2 :
Global Instance into_sep_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
IntoSep P Q1 Q2 IntoSep P Q1 Q2.
Proof. rewrite /IntoSep -bi_mor_sep=> -> //. Qed.
Proof. rewrite /IntoSep -bi_embed_sep=> -> //. Qed.
(* FIXME: This instance is kind of strange, it just gets rid of the bi_affinely. Also, it
overlaps with `into_sep_affinely_later`, and hence has lower precedence. *)
......@@ -560,9 +560,9 @@ Global Instance from_or_persistently P Q1 Q2 :
FromOr P Q1 Q2
FromOr (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Proof. rewrite /FromOr=> <-. by rewrite persistently_or. Qed.
Global Instance from_or_morphism `{BiMorphism PROP PROP'} P Q1 Q2 :
Global Instance from_or_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
FromOr P Q1 Q2 FromOr P Q1 Q2.
Proof. by rewrite /FromOr -bi_mor_or => <-. Qed.
Proof. by rewrite /FromOr -bi_embed_or => <-. Qed.
(* IntoOr *)
Global Instance into_or_or P Q : IntoOr (P Q) P Q.
......@@ -582,9 +582,9 @@ Global Instance into_or_persistently P Q1 Q2 :
IntoOr P Q1 Q2
IntoOr (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Proof. rewrite /IntoOr=>->. by rewrite persistently_or. Qed.
Global Instance into_or_morphism `{BiMorphism PROP PROP'} P Q1 Q2 :
Global Instance into_or_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
IntoOr P Q1 Q2 IntoOr P Q1 Q2.
Proof. by rewrite /IntoOr -bi_mor_or => <-. Qed.
Proof. by rewrite /IntoOr -bi_embed_or => <-. Qed.
(* FromExist *)
Global Instance from_exist_exist {A} (Φ : A PROP): FromExist ( a, Φ a) Φ.
......@@ -604,9 +604,9 @@ Proof. rewrite /FromExist=> <-. by rewrite -plainly_exist_2. Qed.
Global Instance from_exist_persistently {A} P (Φ : A PROP) :
FromExist P Φ FromExist (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
Proof. rewrite /FromExist=> <-. by rewrite persistently_exist. Qed.
Global Instance from_exist_morphism `{BiMorphism PROP PROP'} {A} P (Φ : A PROP) :
Global Instance from_exist_embed `{BiEmbedding PROP PROP'} {A} P (Φ : A PROP) :
FromExist P Φ FromExist P (λ a, ⎡Φ a%I).
Proof. by rewrite /FromExist -bi_mor_exist => <-. Qed.
Proof. by rewrite /FromExist -bi_embed_exist => <-. Qed.
(* IntoExist *)
Global Instance into_exist_exist {A} (Φ : A PROP) : IntoExist ( a, Φ a) Φ.
......@@ -639,9 +639,9 @@ Proof. rewrite /IntoExist=> HP. by rewrite HP plainly_exist. Qed.
Global Instance into_exist_persistently {A} P (Φ : A PROP) :
IntoExist P Φ IntoExist (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
Proof. rewrite /IntoExist=> HP. by rewrite HP persistently_exist. Qed.
Global Instance into_exist_morphism `{BiMorphism PROP PROP'} {A} P (Φ : A PROP) :
Global Instance into_exist_embed `{BiEmbedding PROP PROP'} {A} P (Φ : A PROP) :
IntoExist P Φ IntoExist P (λ a, ⎡Φ a%I).
Proof. by rewrite /IntoExist -bi_mor_exist => <-. Qed.
Proof. by rewrite /IntoExist -bi_embed_exist => <-. Qed.
(* IntoForall *)
Global Instance into_forall_forall {A} (Φ : A PROP) : IntoForall ( a, Φ a) Φ.
......@@ -655,9 +655,9 @@ Proof. rewrite /IntoForall=> HP. by rewrite HP plainly_forall. Qed.
Global Instance into_forall_persistently {A} P (Φ : A PROP) :
IntoForall P Φ IntoForall (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
Proof. rewrite /IntoForall=> HP. by rewrite HP persistently_forall. Qed.
Global Instance into_forall_morphism `{BiMorphism PROP PROP'} {A} P (Φ : A PROP) :
Global Instance into_forall_embed `{BiEmbedding PROP PROP'} {A} P (Φ : A PROP) :
IntoForall P Φ IntoForall P (λ a, ⎡Φ a%I).
Proof. by rewrite /IntoForall -bi_mor_forall => <-. Qed.
Proof. by rewrite /IntoForall -bi_embed_forall => <-. Qed.
(* FromForall *)
Global Instance from_forall_forall {A} (Φ : A PROP) :
......@@ -695,9 +695,9 @@ Proof. rewrite /FromForall=> <-. by rewrite plainly_forall. Qed.
Global Instance from_forall_persistently {A} P (Φ : A PROP) :
FromForall P Φ FromForall (bi_persistently P)%I (λ a, bi_persistently (Φ a))%I.
Proof. rewrite /FromForall=> <-. by rewrite persistently_forall. Qed.
Global Instance from_forall_morphism `{BiMorphism PROP PROP'} {A} P (Φ : A PROP) :
Global Instance from_forall_embed `{BiEmbedding PROP PROP'} {A} P (Φ : A PROP) :
FromForall P Φ FromForall P%I (λ a, ⎡Φ a%I).
Proof. by rewrite /FromForall -bi_mor_forall => <-. Qed.
Proof. by rewrite /FromForall -bi_embed_forall => <-. Qed.
(* ElimModal *)
Global Instance elim_modal_wand P P' Q Q' R :
......@@ -736,24 +736,24 @@ Proof.
rewrite /FromPure /Frame=> <-. by rewrite affinely_persistently_if_elim sep_elim_l.
Qed.
Class MakeMorphism `{BiMorphism PROP PROP'} P (Q : PROP') :=
make_morphism : P Q.
Class MakeMorphism `{BiEmbedding PROP PROP'} P (Q : PROP') :=
make_embed : P Q.
Arguments MakeMorphism {_ _ _} _%I _%I.
Global Instance make_morphism_true `{BiMorphism PROP PROP'} :
Global Instance make_embed_true `{BiEmbedding PROP PROP'} :
MakeMorphism True True.
Proof. by rewrite /MakeMorphism bi_mor_pure. Qed.
Global Instance make_morphism_emp `{BiMorphism PROP PROP'} :
Proof. by rewrite /MakeMorphism bi_embed_pure. Qed.
Global Instance make_embed_emp `{BiEmbedding PROP PROP'} :
MakeMorphism emp emp.
Proof. by rewrite /MakeMorphism bi_mor_emp. Qed.
Global Instance make_morphism_default `{BiMorphism PROP PROP'} :
Proof. by rewrite /MakeMorphism bi_embed_emp. Qed.
Global Instance make_embed_default `{BiEmbedding PROP PROP'} :
MakeMorphism P P | 100.
Proof. by rewrite /MakeMorphism. Qed.
Global Instance frame_morphism `{BiMorphism PROP PROP'} p P Q (Q' : PROP') R :
Global Instance frame_embed `{BiEmbedding PROP PROP'} p P Q (Q' : PROP') R :
Frame p R P Q MakeMorphism Q Q' Frame p R P Q'.