From 7442a17ae060fdcbf61a6028cfe35fcae27211cb Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 11 Jun 2019 13:42:15 +0200
Subject: [PATCH] add a lemma to easily combine two arbitrary mapsto (with
 different values)

---
 theories/base_logic/lib/gen_heap.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index e2ff44a25..a3b687fea 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -204,6 +204,13 @@ Section gen_heap.
     by intros [_ ?%agree_op_invL'].
   Qed.
 
+  Lemma mapsto_combine l q1 q2 v1 v2 :
+    l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ l ↦{q1 + q2} v1 ∗ ⌜v1 = v2⌝.
+  Proof.
+    iIntros "Hl1 Hl2". iDestruct (mapsto_agree with "Hl1 Hl2") as %->.
+    iCombine "Hl1 Hl2" as "Hl". eauto with iFrame.
+  Qed.
+
   Global Instance ex_mapsto_fractional l : Fractional (λ q, l ↦{q} -)%I.
   Proof.
     intros p q. iSplit.
-- 
GitLab