From 741641e38bbf75b8c0e2a98099426030c9b23141 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 1 Mar 2018 15:35:23 +0100
Subject: [PATCH] Replace elim_inv_embed_inv  by the more generic instance
 elim_inv_embed.

---
 theories/base_logic/lib/invariants.v | 9 ---------
 theories/proofmode/monpred.v         | 9 +++++++++
 2 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index 2c6fa9bb9..b18cb809f 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -104,15 +104,6 @@ Proof.
   iApply (Helim with "[$H2]"); first done.
   iMod (inv_open _ N with "[#]") as "(HP&Hclose)"; auto with iFrame.
 Qed.
-Global Instance elim_inv_embed_inv {PROP' : sbi} `{SbiEmbedding _ PROP'}
-       E N (P : iProp Σ) (Q Q' : PROP') :
-  (∀ R, ElimModal True ⎡|={E,E∖↑N}=> R⎤ ⎡R⎤ Q Q') →
-  ElimInv (↑N ⊆ E) ⎡inv N P⎤ True (⎡▷ P⎤) (⎡▷ P ={E∖↑N,E}=∗ True⎤) Q Q'.
-Proof.
-  rewrite /ElimInv /ElimModal. iIntros (Helim ?) "(#H1&TRUE&H2)".
-  rewrite -bi_embed_sep. iApply (Helim with "[$H2 $TRUE]"); first done.
-  iModIntro. iMod (inv_open _ N with "[#]") as "(HP&Hclose)"; auto with iFrame.
-Qed.
 
 Lemma inv_open_timeless E N P `{!Timeless P} :
   ↑N ⊆ E → inv N P ={E,E∖↑N}=∗ P ∗ (P ={E∖↑N,E}=∗ True).
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index fd1e7e056..cfec41ed6 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -490,4 +490,13 @@ Proof. by rewrite /ElimModal monPred_at_fupd. Qed.
 Global Instance add_modal_at_fupd_goal `{FUpdFacts PROP} E1 E2 𝓟 𝓟' Q i :
   AddModal 𝓟 𝓟' (|={E1,E2}=> Q i) → AddModal 𝓟 𝓟' ((|={E1,E2}=> Q) i).
 Proof. by rewrite /AddModal !monPred_at_fupd. Qed.
+
+Global Instance elim_inv_embed φ 𝓟inv 𝓟in 𝓟out 𝓟close Pin Pout Pclose Q Q' :
+  (∀ i, ElimInv φ 𝓟inv 𝓟in 𝓟out 𝓟close (Q i) (Q' i)) →
+  MakeEmbed 𝓟in Pin → MakeEmbed 𝓟out Pout → MakeEmbed 𝓟close Pclose →
+  ElimInv φ ⎡𝓟inv⎤ Pin Pout Pclose Q Q'.
+Proof.
+  rewrite /MakeEmbed /ElimInv=>H <- <- <- ?. iStartProof PROP.
+  iIntros (?) "(?&?&HQ')". iApply H; [done|]. iFrame. iIntros "?". by iApply "HQ'".
+Qed.
 End sbi.
-- 
GitLab