From a5b6db8b16da9735008ad23af5f948a725f4af39 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Sun, 3 Feb 2019 17:21:56 +0100
Subject: [PATCH] Add `big_sepM_insert_acc`.

---
 CHANGELOG.md         |  1 +
 theories/bi/big_op.v | 11 +++++++++++
 2 files changed, 12 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index f7b0037ea..c4dfd5f2c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -99,6 +99,7 @@ Changes in Coq:
 * A new tactic, `wp_pures`, executes as many pure steps as possible, excluding
   steps that would require unlocking subterms. Every impure wp_ tactic executes
   this tactic before doing anything else.
+* Add `big_sepM_insert_acc`.
 
 ## Iris 3.1.0 (released 2017-12-19)
 
diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 8149b201f..9ff0864e0 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -628,6 +628,17 @@ Section gmap.
     rewrite -insert_delete big_sepM_insert ?lookup_delete //.
   Qed.
 
+  Lemma big_sepM_insert_acc Φ m i x :
+    m !! i = Some x →
+    ([∗ map] k↦y ∈ m, Φ k y) ⊢
+      Φ i x ∗ (∀ x', Φ i x' -∗ ([∗ map] k↦y ∈ <[i:=x']> m, Φ k y)).
+  Proof.
+    intros ?. rewrite {1}big_sepM_delete //. apply sep_mono; [done|].
+    apply forall_intro=> x'.
+    rewrite -insert_delete big_sepM_insert ?lookup_delete //.
+    by apply wand_intro_l.
+  Qed.
+
   Lemma big_sepM_fn_insert {B} (Ψ : K → A → B → PROP) (f : K → B) m i x b :
     m !! i = None →
        ([∗ map] k↦y ∈ <[i:=x]> m, Ψ k y (<[i:=b]> f k))
-- 
GitLab