Embedding stuff in a separated file.

_CoqProject

@@ -36,6 +36,7 @@ theories/bi/fractional.v
 theories/bi/counter_examples.v
 theories/bi/fixpoint.v
 theories/bi/monpred.v
+theories/bi/embedding.v
 theories/base_logic/upred.v
 theories/base_logic/derived.v
 theories/base_logic/base_logic.v

theories/bi/bi.v

-From iris.bi Require Export derived_laws big_op updates.
+From iris.bi Require Export derived_laws big_op updates embedding.
 Set Default Proof Using "Type".
 
 Module Import bi.

theories/bi/derived_laws.v

@@ -2296,107 +2296,3 @@ To avoid that, we declare it using a [Hint Immediate], so that it will
 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 embeddings *)
-Section bi_embedding.
-  Context `{BiEmbedding PROP1 PROP2}.
-
-  Global Instance bi_embed_proper : Proper ((≡) ==> (≡)) bi_embed.
-  Proof. apply (ne_proper _). Qed.
-  Global Instance bi_embed_mono_flip : Proper (flip (⊢) ==> flip (⊢)) bi_embed.
-  Proof. solve_proper. Qed.
-  Global Instance bi_embed_inj : Inj (≡) (≡) bi_embed.
-  Proof.
-    intros ?? EQ. apply bi.equiv_spec, conj; apply (inj bi_embed);
-    rewrite EQ //.
-  Qed.
-
-  Lemma bi_embed_valid (P : PROP1) : @bi_embed PROP1 PROP2 _ P ↔ P.
-  Proof.
-    by rewrite /bi_valid -bi_embed_emp; split=>?; [apply (inj bi_embed)|f_equiv].
-  Qed.
-
-  Lemma bi_embed_forall A (Φ : A → PROP1) : ⎡∀ x, Φ x⎤ ⊣⊢ ∀ x, ⎡Φ x⎤.
-  Proof.
-    apply bi.equiv_spec; split; [|apply bi_embed_forall_2].
-    apply bi.forall_intro=>?. by rewrite bi.forall_elim.
-  Qed.
-  Lemma bi_embed_exist A (Φ : A → PROP1) : ⎡∃ x, Φ x⎤ ⊣⊢ ∃ x, ⎡Φ x⎤.
-  Proof.
-    apply bi.equiv_spec; split; [apply bi_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⎤).
-  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.
-  Qed.
-  Lemma bi_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.
-  Qed.
-  Lemma bi_embed_pure φ : ⎡⌜φ⌝⎤ ⊣⊢ ⌜φ⌝.
-  Proof.
-    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_embed_impl;
-      last apply bi.True_intro.
-    apply bi.impl_intro_l. by rewrite right_id.
-  Qed.
-  Lemma bi_embed_internal_eq (A : ofeT) (x y : A) : ⎡x ≡ y⎤ ⊣⊢ x ≡ y.
-  Proof.
-    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_embed_pure.
-    eapply bi.impl_elim; [done|]. apply bi.True_intro.
-  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; 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_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_embed_except_0 -sbi_embed_later timeless.
-  Qed.
-End sbi_embedding.
\ No newline at end of file

theories/bi/embedding.v

+From iris.bi Require Import interface derived_laws.
+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 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 SbiEmbedding (PROP1 PROP2 : sbi) `{BiEmbed PROP1 PROP2} := {
+  sbi_embed_bi_embed :> BiEmbedding PROP1 PROP2;
+  sbi_embed_later P : ⎡▷ P⎤ ⊣⊢ ▷ ⎡P⎤
+}.
+
+Section bi_embedding.
+  Context `{BiEmbedding PROP1 PROP2}.
+
+  Global Instance bi_embed_proper : Proper ((≡) ==> (≡)) bi_embed.
+  Proof. apply (ne_proper _). Qed.
+  Global Instance bi_embed_mono_flip : Proper (flip (⊢) ==> flip (⊢)) bi_embed.
+  Proof. solve_proper. Qed.
+  Global Instance bi_embed_inj : Inj (≡) (≡) bi_embed.
+  Proof.
+    intros ?? EQ. apply bi.equiv_spec, conj; apply (inj bi_embed);
+    rewrite EQ //.
+  Qed.
+
+  Lemma bi_embed_valid (P : PROP1) : @bi_embed PROP1 PROP2 _ P ↔ P.
+  Proof.
+    by rewrite /bi_valid -bi_embed_emp; split=>?; [apply (inj bi_embed)|f_equiv].
+  Qed.
+
+  Lemma bi_embed_forall A (Φ : A → PROP1) : ⎡∀ x, Φ x⎤ ⊣⊢ ∀ x, ⎡Φ x⎤.
+  Proof.
+    apply bi.equiv_spec; split; [|apply bi_embed_forall_2].
+    apply bi.forall_intro=>?. by rewrite bi.forall_elim.
+  Qed.
+  Lemma bi_embed_exist A (Φ : A → PROP1) : ⎡∃ x, Φ x⎤ ⊣⊢ ∃ x, ⎡Φ x⎤.
+  Proof.
+    apply bi.equiv_spec; split; [apply bi_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⎤).
+  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.
+  Qed.
+  Lemma bi_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.
+  Qed.
+  Lemma bi_embed_pure φ : ⎡⌜φ⌝⎤ ⊣⊢ ⌜φ⌝.
+  Proof.
+    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_embed_impl;
+      last apply bi.True_intro.
+    apply bi.impl_intro_l. by rewrite right_id.
+  Qed.
+  Lemma bi_embed_internal_eq (A : ofeT) (x y : A) : ⎡x ≡ y⎤ ⊣⊢ x ≡ y.
+  Proof.
+    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_embed_pure.
+    eapply bi.impl_elim; [done|]. apply bi.True_intro.
+  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; 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_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_embed_except_0 -sbi_embed_later timeless.
+  Qed.
+End sbi_embedding.

theories/bi/interface.v

@@ -524,31 +524,3 @@ Proof. eapply sbi_mixin_later_false_em, sbi_sbi_mixin. Qed.
 End sbi_laws.
 
 End bi.
-
-(* Typically, embeddings are used to *define* the destination 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 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 SbiEmbedding (PROP1 PROP2 : sbi) `{BiEmbed PROP1 PROP2} := {
-  sbi_embed_bi_embed :> BiEmbedding PROP1 PROP2;
-  sbi_embed_later P : ⎡▷ P⎤ ⊣⊢ ▷ ⎡P⎤
-}.

theories/bi/monpred.v

-From iris.bi Require Import derived_laws.
+From iris.bi Require Import bi.
 
 (** Definitions. *)