From ef06857c84f2415e5d099c2d363f04f60a2a4209 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Sun, 17 Dec 2017 10:52:31 +0100
Subject: [PATCH] MonoidHommomorphism instances for embeddings.

---
 theories/bi/embedding.v | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index ac2ad7bf6..b9ce2aedc 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -1,3 +1,4 @@
+From iris.algebra Require Import monoid.
 From iris.bi Require Import interface derived_laws.
 From stdpp Require Import hlist.
 
@@ -117,6 +118,25 @@ Section bi_embedding.
   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.
+    by split; [split|]; try apply _;
+      [setoid_rewrite bi_embed_and|rewrite bi_embed_pure].
+  Qed.
+  Global Instance bi_embed_or_homomorphism :
+    MonoidHomomorphism bi_or bi_or (≡) bi_embed.
+  Proof.
+    by split; [split|]; try apply _;
+      [setoid_rewrite bi_embed_or|rewrite bi_embed_pure].
+  Qed.
+  Global Instance bi_embed_sep_homomorphism :
+    MonoidHomomorphism bi_sep bi_sep (≡) bi_embed.
+  Proof.
+    by split; [split|]; try apply _;
+      [setoid_rewrite bi_embed_sep|rewrite bi_embed_emp].
+  Qed.
 End bi_embedding.
 
 Section sbi_embedding.
-- 
GitLab