From 1dc2aecd9c22db954cbfbca2c6ab8a0535e5abdc Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 24 May 2020 18:50:48 +0200
Subject: [PATCH] Add lemma `inv_combine_dup_l`.

Thanks to @tchajed for the initial version of this proof.
---
 theories/base_logic/lib/invariants.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index 0f9673414..fc4d9fb37 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -145,6 +145,18 @@ Section inv.
     iMod "Hclose" as %_. iMod ("HcloseQ" with "HQ") as %_. by iApply "HcloseP".
   Qed.
 
+  Lemma inv_combine_dup_l N P Q :
+    □ (P -∗ P ∗ P) -∗
+    inv N P -∗ inv N Q -∗ inv N (P ∗ Q).
+  Proof.
+    rewrite inv_eq. iIntros "#HPdup #HinvP #HinvQ !#" (E ?).
+    iMod ("HinvP" with "[//]") as "[HP HcloseP]".
+    iDestruct ("HPdup" with "HP") as "[$ HP]".
+    iMod ("HcloseP" with "HP") as %_.
+    iMod ("HinvQ" with "[//]") as "[$ HcloseQ]".
+    iIntros "!> [HP HQ]". by iApply "HcloseQ".
+  Qed.
+
   (** ** Proof mode integration *)
   Global Instance into_inv_inv N P : IntoInv (inv N P) N := {}.
 
-- 
GitLab