From 09ae320631c839632036548685f507a513a566a3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 4 Apr 2018 21:42:37 +0200
Subject: [PATCH] =?UTF-8?q?Separate=20type=20class=20for=20`=E2=96=A0=20?=
 =?UTF-8?q?=E2=8E=A1P=E2=8E=A4=20=E2=8A=A2=20=E2=8E=A1=E2=96=A0=20P?=
 =?UTF-8?q?=E2=8E=A4`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/bi/embedding.v                  | 27 ++++++++++++++++++------
 theories/bi/monpred.v                    |  4 ++++
 theories/proofmode/class_instances_sbi.v |  2 +-
 3 files changed, 25 insertions(+), 8 deletions(-)

diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index b73514844..def2c522d 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -62,6 +62,13 @@ Class BiEmbedFUpd (PROP1 PROP2 : sbi)
 Hint Mode BiEmbedFUpd - ! - - - : typeclass_instances.
 Hint Mode BiEmbedFUpd ! - - - - : typeclass_instances.
 
+Class BiEmbedPlainly (PROP1 PROP2 : sbi)
+      `{BiEmbed PROP1 PROP2, BiPlainly PROP1, BiPlainly PROP2} := {
+  embed_plainly_2 (P : PROP1) : ■ ⎡P⎤ ⊢ (⎡■ P⎤ : PROP2)
+}.
+Hint Mode BiEmbedPlainly - ! - - - : typeclass_instances.
+Hint Mode BiEmbedPlainly ! - - - - : typeclass_instances.
+
 Section embed_laws.
   Context `{BiEmbed PROP1 PROP2}.
   Local Notation embed := (embed (A:=PROP1) (B:=PROP2)).
@@ -270,6 +277,14 @@ Section sbi_embed.
   Lemma embed_except_0 P : ⎡◇ P⎤ ⊣⊢ ◇ ⎡P⎤.
   Proof. by rewrite embed_or embed_later embed_pure. Qed.
 
+  (* Not an instance, since it may cause overlap *)
+  Lemma bi_embed_plainly_emp `{!BiPlainly PROP1, !BiPlainly PROP2} :
+    BiEmbedEmp PROP1 PROP2 → BiEmbedPlainly PROP1 PROP2.
+  Proof.
+    intros. constructor=> P. rewrite !plainly_alt embed_internal_eq.
+    by rewrite -embed_affinely -embed_emp embed_interal_inj.
+  Qed.
+
   Lemma embed_plainly_1 `{!BiPlainly PROP1, !BiPlainly PROP2} P : ⎡■ P⎤ ⊢ ■ ⎡P⎤.
   Proof.
     assert (∀ P, <affine> ⎡ P ⎤ ⊣⊢ (<affine> ⎡ <affine> P ⎤ : PROP2)) as Hhelp.
@@ -282,16 +297,14 @@ Section sbi_embed.
       - apply bi.and_intro; auto using embed_emp_2. }
     rewrite !plainly_alt embed_internal_eq. by rewrite Hhelp -Hemp -!bi.f_equiv.
   Qed.
-  Lemma embed_plainly `{!BiEmbedEmp PROP1 PROP2,
-    !BiPlainly PROP1, !BiPlainly PROP2} P : ⎡■ P⎤ ⊣⊢ ■ ⎡P⎤.
+  Lemma embed_plainly `{!BiPlainly PROP1, !BiPlainly PROP2,
+    !BiEmbedPlainly PROP1 PROP2} P : ⎡■ P⎤ ⊣⊢ ■ ⎡P⎤.
   Proof.
-    apply (anti_symm _); first by apply embed_plainly_1.
-    rewrite !plainly_alt embed_internal_eq.
-    by rewrite -embed_affinely -embed_emp embed_interal_inj.
+    apply (anti_symm _). by apply embed_plainly_1. by apply embed_plainly_2.
   Qed.
 
-  Lemma embed_plainly_if `{!BiEmbedEmp PROP1 PROP2,
-    !BiPlainly PROP1, !BiPlainly PROP2} p P : ⎡■?p P⎤ ⊣⊢ ■?p ⎡P⎤.
+  Lemma embed_plainly_if `{!BiPlainly PROP1, !BiPlainly PROP2,
+    !BiEmbedPlainly PROP1 PROP2} p P : ⎡■?p P⎤ ⊣⊢ ■?p ⎡P⎤.
   Proof. destruct p; simpl; auto using embed_plainly. Qed.
   Lemma embed_plainly_if_1 `{!BiPlainly PROP1, !BiPlainly PROP2} p P :
     ⎡■?p P⎤ ⊢ ■?p ⎡P⎤.
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index b94e69f60..69e84c9d5 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -933,6 +933,10 @@ Proof.
   apply bi.forall_intro=>?. by do 2 f_equiv.
 Qed.
 
+Global Instance monPred_bi_embed_plainly `{BiPlainly PROP} :
+  BiEmbedPlainly PROP monPredSI.
+Proof. apply bi_embed_plainly_emp, _. Qed.
+
 Lemma monPred_plainly_unfold `{BiPlainly PROP} : plainly = λ P, ⎡ ∀ i, ■ (P i) ⎤%I.
 Proof. by rewrite monPred_plainly_eq monPred_embed_eq. Qed.
 Lemma monPred_at_plainly `{BiPlainly PROP} i P : (■ P) i ⊣⊢ ∀ j, ■ (P j).
diff --git a/theories/proofmode/class_instances_sbi.v b/theories/proofmode/class_instances_sbi.v
index adf0bc699..f8045f913 100644
--- a/theories/proofmode/class_instances_sbi.v
+++ b/theories/proofmode/class_instances_sbi.v
@@ -417,7 +417,7 @@ Global Instance from_modal_plainly `{BiPlainly PROP} P :
 Proof. by rewrite /FromModal. Qed.
 
 Global Instance from_modal_plainly_embed `{BiPlainly PROP, BiPlainly PROP',
-    BiEmbedEmp PROP PROP', !SbiEmbed PROP PROP'} `(sel : A) P Q :
+    BiEmbedPlainly PROP PROP', !SbiEmbed PROP PROP'} `(sel : A) P Q :
   FromModal modality_plainly sel P Q →
   FromModal modality_plainly sel ⎡P⎤ ⎡Q⎤ | 100.
 Proof. rewrite /FromModal /= =><-. by rewrite embed_plainly. Qed.
-- 
GitLab