Commit e39f72fe authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Bundle type class for embedding.

This change is slightly more invasive than expected: in monPred we were
using the embedding before the BI was defined. With the new setup, this
is no longer possible, because in order to make an instance of the
embedding, we need to know that `monPred` is a BI. As such, we define
`emp`, `⌜ _ ⌝` and friends directly in the model of `monPred` and later
prove that they are equal to a version in terms of the embedding.
parent 6cad0bb1
......@@ -2,173 +2,207 @@ From iris.algebra Require Import monoid.
From iris.bi Require Import interface derived_laws big_op.
From stdpp Require Import hlist.
(* Embeddings are often used to *define* the connectives of the
domain BI. 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 Embed (A B : Type) := embed : A B.
Arguments embed {_ _ _} _%I : simpl never.
Notation "⎡ P ⎤" := (embed P) : bi_scope.
Instance: Params (@embed) 3.
Typeclasses Opaque embed.
Hint Mode Embed ! - : typeclass_instances.
Hint Mode Embed - ! : typeclass_instances.
Record BiEmbedMixin (PROP1 PROP2 : bi) `(Embed PROP1 PROP2) := {
bi_embed_mixin_ne : NonExpansive embed;
bi_embed_mixin_mono : Proper (() ==> ()) embed;
bi_embed_mixin_entails_inj :> Inj () () embed;
bi_embed_mixin_emp : emp emp;
bi_embed_mixin_impl_2 P Q : (P Q) P Q;
bi_embed_mixin_forall_2 A (Φ : A PROP1) : ( x, ⎡Φ x) x, Φ x;
bi_embed_mixin_exist_1 A (Φ : A PROP1) : x, Φ x x, ⎡Φ x;
bi_embed_mixin_sep P Q : P Q P Q;
bi_embed_mixin_wand_2 P Q : (P - Q) P - Q;
bi_embed_mixin_plainly P : bi_plainly P bi_plainly P;
bi_embed_mixin_persistently P : bi_persistently P bi_persistently P
}.
Class BiEmbed (PROP1 PROP2 : bi) := {
bi_embed_embed :> Embed PROP1 PROP2;
bi_embed_mixin : BiEmbedMixin PROP1 PROP2 bi_embed_embed;
}.
Hint Mode BiEmbed ! - : typeclass_instances.
Hint Mode BiEmbed - ! : typeclass_instances.
Arguments bi_embed_embed : simpl never.
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_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 SbiEmbed (PROP1 PROP2 : sbi) `{BiEmbed PROP1 PROP2} := {
embed_internal_eq_1 (A : ofeT) (x y : A) : x y x y;
embed_later P : ⎡▷ P P
}.
Class SbiEmbedding (PROP1 PROP2 : sbi) `{BiEmbed PROP1 PROP2} := {
sbi_embed_bi_embed :> BiEmbedding PROP1 PROP2;
sbi_embed_internal_eq_1 (A : ofeT) (x y : A) : x y x y;
sbi_embed_later P : ⎡▷ P P
}.
Section embed_laws.
Context `{BiEmbed PROP1 PROP2}.
Local Notation embed := (embed (A:=PROP1) (B:=PROP2)).
Local Notation "⎡ P ⎤" := (embed P) : bi_scope.
Implicit Types P : PROP1.
Global Instance embed_ne : NonExpansive embed.
Proof. eapply bi_embed_mixin_ne, bi_embed_mixin. Qed.
Global Instance embed_mono : Proper (() ==> ()) embed.
Proof. eapply bi_embed_mixin_mono, bi_embed_mixin. Qed.
Global Instance embed_entails_inj : Inj () () embed.
Proof. eapply bi_embed_mixin_entails_inj, bi_embed_mixin. Qed.
Lemma embed_emp : emp emp.
Proof. eapply bi_embed_mixin_emp, bi_embed_mixin. Qed.
Lemma embed_impl_2 P Q : (P Q) P Q.
Proof. eapply bi_embed_mixin_impl_2, bi_embed_mixin. Qed.
Lemma embed_forall_2 A (Φ : A PROP1) : ( x, ⎡Φ x) x, Φ x.
Proof. eapply bi_embed_mixin_forall_2, bi_embed_mixin. Qed.
Lemma embed_exist_1 A (Φ : A PROP1) : x, Φ x x, ⎡Φ x.
Proof. eapply bi_embed_mixin_exist_1, bi_embed_mixin. Qed.
Lemma embed_sep P Q : P Q P Q.
Proof. eapply bi_embed_mixin_sep, bi_embed_mixin. Qed.
Lemma embed_wand_2 P Q : (P - Q) P - Q.
Proof. eapply bi_embed_mixin_wand_2, bi_embed_mixin. Qed.
Lemma embed_plainly P : bi_plainly P bi_plainly P.
Proof. eapply bi_embed_mixin_plainly, bi_embed_mixin. Qed.
Lemma embed_persistently P : bi_persistently P bi_persistently P.
Proof. eapply bi_embed_mixin_persistently, bi_embed_mixin. Qed.
End embed_laws.
Section bi_embedding.
Context `{BiEmbedding PROP1 PROP2}.
Local Notation bi_embed := (bi_embed (A:=PROP1) (B:=PROP2)).
Local Notation "⎡ P ⎤" := (bi_embed P) : bi_scope.
Section embed.
Context `{BiEmbed PROP1 PROP2}.
Local Notation embed := (embed (A:=PROP1) (B:=PROP2)).
Local Notation "⎡ P ⎤" := (embed P) : bi_scope.
Implicit Types P Q R : PROP1.
Global Instance bi_embed_proper : Proper (() ==> ()) bi_embed.
Global Instance embed_proper : Proper (() ==> ()) embed.
Proof. apply (ne_proper _). Qed.
Global Instance bi_embed_flip_mono : Proper (flip () ==> flip ()) bi_embed.
Global Instance embed_flip_mono : Proper (flip () ==> flip ()) embed.
Proof. solve_proper. Qed.
Global Instance bi_embed_inj : Inj () () bi_embed.
Global Instance embed_inj : Inj () () embed.
Proof.
intros P Q EQ. apply bi.equiv_spec, conj; apply (inj bi_embed);
intros P Q EQ. apply bi.equiv_spec, conj; apply (inj embed);
rewrite EQ //.
Qed.
Lemma bi_embed_valid (P : PROP1) : P%I P.
Lemma embed_valid (P : PROP1) : P%I P.
Proof.
by rewrite /bi_valid -bi_embed_emp; split=>?; [apply (inj bi_embed)|f_equiv].
by rewrite /bi_valid -embed_emp; split=>?; [apply (inj embed)|f_equiv].
Qed.
Lemma bi_embed_forall A (Φ : A PROP1) : x, Φ x x, ⎡Φ x.
Lemma embed_forall A (Φ : A PROP1) : x, Φ x x, ⎡Φ x.
Proof.
apply bi.equiv_spec; split; [|apply bi_embed_forall_2].
apply bi.equiv_spec; split; [|apply embed_forall_2].
apply bi.forall_intro=>?. by rewrite bi.forall_elim.
Qed.
Lemma bi_embed_exist A (Φ : A PROP1) : x, Φ x x, ⎡Φ x.
Lemma embed_exist A (Φ : A PROP1) : x, Φ x x, ⎡Φ x.
Proof.
apply bi.equiv_spec; split; [apply bi_embed_exist_1|].
apply bi.equiv_spec; split; [apply embed_exist_1|].
apply bi.exist_elim=>?. by rewrite -bi.exist_intro.
Qed.
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).
Lemma embed_and P Q : P Q P Q.
Proof. rewrite !bi.and_alt embed_forall. by f_equiv=>-[]. Qed.
Lemma embed_or P Q : P Q P Q.
Proof. rewrite !bi.or_alt embed_exist. by f_equiv=>-[]. Qed.
Lemma embed_impl P Q : P Q (P Q).
Proof.
apply bi.equiv_spec; split; [|apply bi_embed_impl_2].
apply bi.impl_intro_l. by rewrite -bi_embed_and bi.impl_elim_r.
apply bi.equiv_spec; split; [|apply embed_impl_2].
apply bi.impl_intro_l. by rewrite -embed_and bi.impl_elim_r.
Qed.
Lemma bi_embed_wand P Q : P - Q (P - Q).
Lemma embed_wand P Q : P - Q (P - Q).
Proof.
apply bi.equiv_spec; split; [|apply bi_embed_wand_2].
apply bi.wand_intro_l. by rewrite -bi_embed_sep bi.wand_elim_r.
apply bi.equiv_spec; split; [|apply embed_wand_2].
apply bi.wand_intro_l. by rewrite -embed_sep bi.wand_elim_r.
Qed.
Lemma bi_embed_pure φ : ⎡⌜φ⌝⎤ ⌜φ⌝.
Lemma embed_pure φ : ⎡⌜φ⌝⎤ ⌜φ⌝.
Proof.
rewrite (@bi.pure_alt PROP1) (@bi.pure_alt PROP2) bi_embed_exist.
rewrite (@bi.pure_alt PROP1) (@bi.pure_alt PROP2) embed_exist.
do 2 f_equiv. apply bi.equiv_spec. split; [apply bi.True_intro|].
rewrite -(_ : (emp emp : PROP1) True) ?bi_embed_impl;
rewrite -(_ : (emp emp : PROP1) True) ?embed_impl;
last apply bi.True_intro.
apply bi.impl_intro_l. by rewrite right_id.
Qed.
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; simpl; auto using bi_embed_plainly. Qed.
Lemma bi_embed_persistently_if P b :
Lemma embed_iff P Q : P Q (P Q).
Proof. by rewrite embed_and !embed_impl. Qed.
Lemma embed_wand_iff P Q : P - Q (P - Q).
Proof. by rewrite embed_and !embed_wand. Qed.
Lemma embed_affinely P : bi_affinely P bi_affinely P.
Proof. by rewrite embed_and embed_emp. Qed.
Lemma embed_absorbingly P : bi_absorbingly P bi_absorbingly P.
Proof. by rewrite embed_sep embed_pure. Qed.
Lemma embed_plainly_if P b : bi_plainly_if b P bi_plainly_if b P.
Proof. destruct b; simpl; auto using embed_plainly. Qed.
Lemma embed_persistently_if P b :
bi_persistently_if b P bi_persistently_if b P.
Proof. destruct b; simpl; 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.
Global Instance bi_embed_and_homomorphism :
MonoidHomomorphism bi_and bi_and () bi_embed.
Proof. destruct b; simpl; auto using embed_persistently. Qed.
Lemma embed_affinely_if P b : bi_affinely_if b P bi_affinely_if b P.
Proof. destruct b; simpl; auto using embed_affinely. Qed.
Lemma embed_hforall {As} (Φ : himpl As PROP1):
bi_hforall Φ⎤ bi_hforall (hcompose embed Φ).
Proof. induction As=>//. rewrite /= embed_forall. by do 2 f_equiv. Qed.
Lemma embed_hexist {As} (Φ : himpl As PROP1):
bi_hexist Φ⎤ bi_hexist (hcompose embed Φ).
Proof. induction As=>//. rewrite /= embed_exist. by do 2 f_equiv. Qed.
Global Instance embed_plain P : Plain P Plain P.
Proof. intros ?. by rewrite /Plain -embed_plainly -plain. Qed.
Global Instance embed_persistent P : Persistent P Persistent P.
Proof. intros ?. by rewrite /Persistent -embed_persistently -persistent. Qed.
Global Instance embed_affine P : Affine P Affine P.
Proof. intros ?. by rewrite /Affine (affine P) embed_emp. Qed.
Global Instance embed_absorbing P : Absorbing P Absorbing P.
Proof. intros ?. by rewrite /Absorbing -embed_absorbingly absorbing. Qed.
Global Instance embed_and_homomorphism :
MonoidHomomorphism bi_and bi_and () embed.
Proof.
by split; [split|]; try apply _;
[setoid_rewrite bi_embed_and|rewrite bi_embed_pure].
[setoid_rewrite embed_and|rewrite embed_pure].
Qed.
Global Instance bi_embed_or_homomorphism :
MonoidHomomorphism bi_or bi_or () bi_embed.
Global Instance embed_or_homomorphism :
MonoidHomomorphism bi_or bi_or () embed.
Proof.
by split; [split|]; try apply _;
[setoid_rewrite bi_embed_or|rewrite bi_embed_pure].
[setoid_rewrite embed_or|rewrite embed_pure].
Qed.
Global Instance bi_embed_sep_homomorphism :
MonoidHomomorphism bi_sep bi_sep () bi_embed.
Global Instance embed_sep_homomorphism :
MonoidHomomorphism bi_sep bi_sep () embed.
Proof.
by split; [split|]; try apply _;
[setoid_rewrite bi_embed_sep|rewrite bi_embed_emp].
[setoid_rewrite embed_sep|rewrite embed_emp].
Qed.
Lemma bi_embed_big_sepL {A} (Φ : nat A PROP1) l :
Lemma embed_big_sepL {A} (Φ : nat A PROP1) l :
[ list] kx l, Φ k x [ list] kx l, ⎡Φ k x.
Proof. apply (big_opL_commute _). Qed.
Lemma bi_embed_big_sepM `{Countable K} {A} (Φ : K A PROP1) (m : gmap K A) :
Lemma embed_big_sepM `{Countable K} {A} (Φ : K A PROP1) (m : gmap K A) :
[ map] kx m, Φ k x [ map] kx m, ⎡Φ k x.
Proof. apply (big_opM_commute _). Qed.
Lemma bi_embed_big_sepS `{Countable A} (Φ : A PROP1) (X : gset A) :
Lemma embed_big_sepS `{Countable A} (Φ : A PROP1) (X : gset A) :
[ set] y X, Φ y [ set] y X, ⎡Φ y.
Proof. apply (big_opS_commute _). Qed.
Lemma bi_embed_big_sepMS `{Countable A} (Φ : A PROP1) (X : gmultiset A) :
Lemma embed_big_sepMS `{Countable A} (Φ : A PROP1) (X : gmultiset A) :
[ mset] y X, Φ y [ mset] y X, ⎡Φ y.
Proof. apply (big_opMS_commute _). Qed.
End bi_embedding.
End embed.
Section sbi_embedding.
Context `{SbiEmbedding PROP1 PROP2}.
Section sbi_embed.
Context `{SbiEmbed PROP1 PROP2}.
Implicit Types P Q R : PROP1.
Lemma sbi_embed_internal_eq (A : ofeT) (x y : A) : x y x y.
Lemma embed_internal_eq (A : ofeT) (x y : A) : x y x y.
Proof.
apply bi.equiv_spec; split; [apply sbi_embed_internal_eq_1|].
apply bi.equiv_spec; split; [apply 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_embed_pure.
rewrite -(bi.internal_eq_refl True%I) embed_pure.
eapply bi.impl_elim; [done|]. apply bi.True_intro.
Qed.
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.
Lemma embed_laterN n P : ⎡▷^n P ^n P.
Proof. induction n=>//=. rewrite embed_later. by f_equiv. Qed.
Lemma embed_except_0 P : ⎡◇ P P.
Proof. by rewrite embed_or embed_later embed_pure. Qed.
Global Instance sbi_embed_timeless P : Timeless P Timeless P.
Global Instance embed_timeless P : Timeless P Timeless P.
Proof.
intros ?. by rewrite /Timeless -sbi_embed_except_0 -sbi_embed_later timeless.
intros ?. by rewrite /Timeless -embed_except_0 -embed_later timeless.
Qed.
End sbi_embedding.
End sbi_embed.
......@@ -2,7 +2,6 @@ From stdpp Require Import coPset.
From iris.bi Require Import bi.
(** Definitions. *)
Structure biIndex :=
BiIndex
{ bi_index_type :> Type;
......@@ -128,14 +127,33 @@ Next Obligation. solve_proper. Qed.
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 (A:=PROP) = _ := seal_eq _.
Definition monPred_pure (φ : Prop) : monPred := tc_opaque ⎡⌜φ⌝⎤%I.
Definition monPred_emp : monPred := tc_opaque emp%I.
Definition monPred_plainly P : monPred := tc_opaque i, bi_plainly (P i)%I.
Definition monPred_absolutely (P : monPred) : monPred := tc_opaque i, P i%I.
Definition monPred_relatively (P : monPred) : monPred := tc_opaque i, P i%I.
Definition monPred_embed : Embed PROP monPred := unseal monPred_embed_aux.
Definition monPred_embed_eq : @embed _ _ monPred_embed = _ := seal_eq _.
Definition monPred_emp_def : monPred := MonPred (λ _, emp)%I _.
Definition monPred_emp_aux : seal (@monPred_emp_def). by eexists. Qed.
Definition monPred_emp := unseal monPred_emp_aux.
Definition monPred_emp_eq : @monPred_emp = _ := seal_eq _.
Definition monPred_pure_def (φ : Prop) : monPred := MonPred (λ _, ⌜φ⌝)%I _.
Definition monPred_pure_aux : seal (@monPred_pure_def). by eexists. Qed.
Definition monPred_pure := unseal monPred_pure_aux.
Definition monPred_pure_eq : @monPred_pure = _ := seal_eq _.
Definition monPred_plainly_def P : monPred := MonPred (λ _, i, bi_plainly (P i))%I _.
Definition monPred_plainly_aux : seal (@monPred_plainly_def). by eexists. Qed.
Definition monPred_plainly := unseal monPred_plainly_aux.
Definition monPred_plainly_eq : @monPred_plainly = _ := seal_eq _.
Definition monPred_absolutely_def P : monPred := MonPred (λ _, i, P i)%I _.
Definition monPred_absolutely_aux : seal (@monPred_absolutely_def). by eexists. Qed.
Definition monPred_absolutely := unseal monPred_absolutely_aux.
Definition monPred_absolutely_eq : @monPred_absolutely = _ := seal_eq _.
Definition monPred_relatively_def P : monPred := MonPred (λ _, i, P i)%I _.
Definition monPred_relatively_aux : seal (@monPred_relatively_def). by eexists. Qed.
Definition monPred_relatively := unseal monPred_relatively_aux.
Definition monPred_relatively_eq : @monPred_relatively = _ := seal_eq _.
Program Definition monPred_and_def P Q : monPred :=
MonPred (λ i, P i Q i)%I _.
......@@ -214,15 +232,16 @@ Arguments monPred_relatively {_ _} _%I.
Notation "'∀ᵢ' P" := (monPred_absolutely P) (at level 20, right associativity) : bi_scope.
Notation "'∃ᵢ' P" := (monPred_relatively P) (at level 20, right associativity) : bi_scope.
Typeclasses Opaque monPred_pure monPred_emp monPred_plainly.
Section Sbi.
Context {I : biIndex} {PROP : sbi}.
Implicit Types i : I.
Notation monPred := (monPred I PROP).
Implicit Types P Q : monPred.
Definition monPred_internal_eq (A : ofeT) (a b : A) : monPred := tc_opaque a b%I.
Definition monPred_internal_eq_def (A : ofeT) (a b : A) : monPred := MonPred (λ _, a b)%I _.
Definition monPred_internal_eq_aux : seal (@monPred_internal_eq_def). by eexists. Qed.
Definition monPred_internal_eq := unseal monPred_internal_eq_aux.
Definition monPred_internal_eq_eq : @monPred_internal_eq = _ := seal_eq _.
Program Definition monPred_later_def P : monPred := MonPred (λ i, (P i))%I _.
Next Obligation. solve_proper. Qed.
......@@ -246,18 +265,18 @@ Definition unseal_eqs :=
(@monPred_and_eq, @monPred_or_eq, @monPred_impl_eq,
@monPred_forall_eq, @monPred_exist_eq,
@monPred_sep_eq, @monPred_wand_eq,
@monPred_persistently_eq, @monPred_later_eq, @monPred_in_eq,
@monPred_embed_eq, @monPred_bupd_eq, @monPred_fupd_eq).
@monPred_persistently_eq, @monPred_later_eq, @monPred_internal_eq_eq, @monPred_in_eq,
@monPred_embed_eq, @monPred_emp_eq, @monPred_pure_eq, @monPred_plainly_eq,
@monPred_absolutely_eq, @monPred_relatively_eq, @monPred_bupd_eq, @monPred_fupd_eq).
Ltac unseal :=
unfold bi_affinely, bi_absorbingly, sbi_except_0, bi_pure, bi_emp,
monPred_absolutely, monPred_relatively, monPred_upclosed, bi_and, bi_or,
monPred_upclosed, bi_and, bi_or,
bi_impl, bi_forall, bi_exist, sbi_internal_eq, bi_sep, bi_wand,
bi_persistently, bi_affinely, bi_plainly, 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;
simpl;
unfold monPred_pure, monPred_emp, monPred_internal_eq, monPred_plainly; simpl;
rewrite !unseal_eqs /=.
End MonPred.
Import MonPred.
......@@ -322,7 +341,7 @@ Proof.
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 //.
- intros P. split=> i. apply bi.forall_intro=>_. by apply bi.plainly_emp_intro.
- 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.
......@@ -457,8 +476,7 @@ Global Instance monPred_in_absorbing i :
Absorbing (@monPred_in I PROP i).
Proof. unfold Absorbing. unseal. split=> ? /=. apply absorbing, _. Qed.
Global Instance monPred_bi_embedding : BiEmbedding PROP monPredI.
Definition monPred_embedding_mixin : BiEmbedMixin PROP monPredI monPred_embed.
Proof.
split; try apply _; unseal; try done.
- move =>?? /= [/(_ inhabitant) ?] //.
......@@ -469,61 +487,71 @@ Proof.
- intros ?. split => ? /=. apply bi.equiv_spec; split.
by apply bi.forall_intro. by rewrite bi.forall_elim.
Qed.
Global Instance monPred_bi_embed : BiEmbed PROP monPredI :=
{| bi_embed_mixin := monPred_embedding_mixin |}.
Lemma monPred_emp_unfold : emp%I = emp : PROP%I.
Proof. by unseal. Qed.
Lemma monPred_pure_unfold : bi_pure = λ φ, φ : PROP%I.
Proof. by unseal. Qed.
Lemma monPred_plainly_unfold : bi_plainly = λ P, i, bi_plainly (P i) %I.
Proof. by unseal. Qed.
Lemma monPred_absolutely_unfold : monPred_absolutely = λ P, i, P i%I.
Proof. by unseal. Qed.
Lemma monPred_relatively_unfold : monPred_relatively = λ P, i, P i%I.
Proof. by unseal. Qed.
Global Instance monPred_absolutely_ne : NonExpansive (@monPred_absolutely I PROP).
Proof. rewrite /monPred_absolutely /=. solve_proper. Qed.
Proof. rewrite monPred_absolutely_unfold. solve_proper. Qed.
Global Instance monPred_absolutely_proper : Proper (() ==> ()) (@monPred_absolutely I PROP).
Proof. apply (ne_proper _). Qed.
Lemma monPred_absolutely_mono P Q : (P Q) ( P Q).
Proof. rewrite /monPred_absolutely /=. solve_proper. Qed.
Proof. rewrite monPred_absolutely_unfold. solve_proper. Qed.
Global Instance monPred_absolutely_mono' : Proper (() ==> ()) (@monPred_absolutely I PROP).
Proof. rewrite /monPred_absolutely /=. solve_proper. Qed.
Proof. intros ???. by apply monPred_absolutely_mono. Qed.
Global Instance monPred_absolutely_flip_mono' :
Proper (flip () ==> flip ()) (@monPred_absolutely I PROP).
Proof. solve_proper. Qed.
Local Notation "'∀ᵢ' P" := (@monPred_absolutely I PROP P) : bi_scope.
Local Notation "'∃ᵢ' P" := (@monPred_relatively I PROP P) : bi_scope.
Proof. intros ???. by apply monPred_absolutely_mono. Qed.
Global Instance monPred_absolutely_plain P : Plain P Plain ( P).
Proof. rewrite /monPred_absolutely /=. apply _. Qed.
Proof. rewrite monPred_absolutely_unfold. apply _. Qed.
Global Instance monPred_absolutely_persistent P : Persistent P Persistent ( P).
Proof. rewrite /monPred_absolutely /=. apply _. Qed.
Proof. rewrite monPred_absolutely_unfold. apply _. Qed.
Global Instance monPred_absolutely_absorbing P : Absorbing P Absorbing ( P).
Proof. rewrite /monPred_absolutely /=. apply _. Qed.
Proof. rewrite monPred_absolutely_unfold. apply _. Qed.
Global Instance monPred_absolutely_affine P : Affine P Affine ( P).
Proof. rewrite /monPred_absolutely /=. apply _. Qed.
Proof. rewrite monPred_absolutely_unfold. apply _. Qed.
Global Instance monPred_relatively_ne : NonExpansive (@monPred_relatively I PROP).
Proof. rewrite /monPred_relatively /=. solve_proper. Qed.
Proof. rewrite monPred_relatively_unfold. solve_proper. Qed.
Global Instance monPred_relatively_proper : Proper (() ==> ()) (@monPred_relatively I PROP).
Proof. apply (ne_proper _). Qed.
Lemma monPred_relatively_mono P Q : (P Q) ( P Q).
Proof. rewrite /monPred_relatively /=. solve_proper. Qed.
Proof. rewrite monPred_relatively_unfold. solve_proper. Qed.
Global Instance monPred_relatively_mono' : Proper (() ==> ()) (@monPred_relatively I PROP).
Proof. rewrite /monPred_relatively /=. solve_proper. Qed.
Proof. intros ???. by apply monPred_relatively_mono. Qed.
Global Instance monPred_relatively_flip_mono' :
Proper (flip () ==> flip ()) (@monPred_relatively I PROP).
Proof. solve_proper. Qed.
Proof. intros ???. by apply monPred_relatively_mono. Qed.
Global Instance monPred_relatively_plain P : Plain P Plain ( P).
Proof. rewrite /monPred_relatively /=. apply _. Qed.
Proof. rewrite monPred_relatively_unfold. apply _. Qed.
Global Instance monPred_relatively_persistent P : Persistent P Persistent ( P).
Proof. rewrite /monPred_relatively /=. apply _. Qed.
Proof. rewrite monPred_relatively_unfold. apply _. Qed.
Global Instance monPred_relatively_absorbing P : Absorbing P Absorbing ( P).
Proof. rewrite /monPred_relatively /=. apply _. Qed.
Proof. rewrite monPred_relatively_unfold. apply _. Qed.
Global Instance monPred_relatively_affine P : Affine P Affine ( P).
Proof. rewrite /monPred_relatively /=. apply _. Qed.
Proof. rewrite monPred_relatively_unfold. apply _. Qed.
(** monPred_at unfolding laws *)
Lemma monPred_at_embed i (P : PROP) : monPred_at P i P.
Proof. by unseal. Qed.
Lemma monPred_at_pure i (φ : Prop) : monPred_at ⌜φ⌝ i ⌜φ⌝.
Proof. by apply monPred_at_embed. Qed.
Proof. by unseal. Qed.
Lemma monPred_at_emp i : monPred_at emp i emp.
Proof. by apply monPred_at_embed. Qed.