From 995f46d387d99ea32d0243886c60b3ec61006289 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 31 May 2016 03:25:33 +0200
Subject: [PATCH] Strengthen big_sepM_insert_override and use it.

---
 algebra/upred_big_op.v | 4 ++--
 program_logic/boxes.v  | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/algebra/upred_big_op.v b/algebra/upred_big_op.v
index c7bc183b6..d25e6fd85 100644
--- a/algebra/upred_big_op.v
+++ b/algebra/upred_big_op.v
@@ -180,9 +180,9 @@ Section gmap.
     f_equiv; apply reflexive_eq, list_fmap_ext. by intros []. done.
   Qed.
 
-  Lemma big_sepM_insert_override (Φ : K → uPred M) m i x :
+  Lemma big_sepM_insert_override (Φ : K → uPred M) m i x y :
     m !! i = Some x →
-    ([★ map] k↦_ ∈ <[i:=x]> m, Φ k) ⊣⊢ ([★ map] k↦_ ∈ m, Φ k).
+    ([★ map] k↦_ ∈ <[i:=y]> m, Φ k) ⊣⊢ ([★ map] k↦_ ∈ m, Φ k).
   Proof.
     intros. rewrite -insert_delete big_sepM_insert ?lookup_delete //.
     by rewrite -big_sepM_delete.
diff --git a/program_logic/boxes.v b/program_logic/boxes.v
index 6e3f3f461..625ac17de 100644
--- a/program_logic/boxes.v
+++ b/program_logic/boxes.v
@@ -144,7 +144,7 @@ Proof.
     as "[Hγ Hγ']"; first by iFrame "Hγ".
   iPvsIntro; iNext; iSplitL "Hγ HQ"; first (iExists true; by iFrame "Hγ HQ").
   iExists Φ; iSplit.
-  - by rewrite -insert_delete big_sepM_insert ?lookup_delete // big_sepM_delete.
+  - by rewrite big_sepM_insert_override.
   - rewrite -insert_delete big_sepM_insert ?lookup_delete //.
     iFrame "Hγ'". by repeat iSplit.
 Qed.
@@ -165,7 +165,7 @@ Proof.
     as "[Hγ Hγ']"; first by iFrame "Hγ".
   iPvsIntro; iNext; iSplitL "Hγ"; first (iExists false; by repeat iSplit).
   iExists Φ; iSplit.
-  - by rewrite -insert_delete big_sepM_insert ?lookup_delete // big_sepM_delete.
+  - by rewrite big_sepM_insert_override.
   - rewrite -insert_delete big_sepM_insert ?lookup_delete //.
     iFrame "Hγ'". by repeat iSplit.
 Qed.
-- 
GitLab