From c90d55ae7fd9a67a9d5a9a39b47bdfa791a1c7c5 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 1 Mar 2018 10:47:58 +0100
Subject: [PATCH] Add instance elim_inv_embed_inv.

---
 theories/base_logic/lib/invariants.v | 9 +++++++++
 theories/proofmode/class_instances.v | 4 ++++
 2 files changed, 13 insertions(+)

diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index b18cb809f..2c6fa9bb9 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -104,6 +104,15 @@ 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/class_instances.v b/theories/proofmode/class_instances.v
index 3268cc849..9a0e3db9b 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -849,6 +849,10 @@ Global Instance from_forall_embed `{BiEmbedding PROP PROP'} {A} P (Φ : A → PR
   FromForall P Φ → FromForall ⎡P⎤%I (λ a, ⎡Φ a⎤%I).
 Proof. by rewrite /FromForall -bi_embed_forall => <-. Qed.
 
+(* IntoInv *)
+Global Instance into_inv_embed {PROP' : bi} `{BiEmbed PROP PROP'} P N :
+  IntoInv P N → IntoInv ⎡P⎤ N.
+
 (* ElimModal *)
 Global Instance elim_modal_wand φ P P' Q Q' R :
   ElimModal φ P P' Q Q' → ElimModal φ P P' (R -∗ Q) (R -∗ Q').
-- 
GitLab