From 91705526f7b5a6d9834e850e34fcb115e2ca6151 Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Tue, 20 Apr 2021 10:23:48 +0200
Subject: [PATCH] Generalize insert_difference

---
 theories/fin_maps.v | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index e40137df..b720debf 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2446,12 +2446,15 @@ Lemma map_difference_empty {A} (m : M A) : m ∖ ∅ = m.
 Proof. by rewrite (right_id _ _). Qed.
 
 Lemma insert_difference {A} (m1 m2 : M A) i x :
-  m2 !! i = None → <[i := x]> (m1 ∖ m2) = <[i := x]> m1 ∖ m2.
+  <[i := x]> (m1 ∖ m2) = <[i := x]> m1 ∖ delete i m2.
 Proof.
   intros. apply map_eq. intros j. apply option_eq. intros y.
-  rewrite lookup_insert_Some, !lookup_difference_Some, lookup_insert_Some.
+  rewrite lookup_insert_Some, !lookup_difference_Some, lookup_insert_Some, lookup_delete_None.
   naive_solver.
 Qed.
+Lemma insert_difference' {A} (m1 m2 : M A) i x :
+  m2 !! i = None → <[i := x]> (m1 ∖ m2) = <[i := x]> m1 ∖ m2.
+Proof. intros. by rewrite insert_difference, delete_notin. Qed.
 Lemma difference_insert {A} (m1 m2 : M A) i x1 x2 x3 :
   <[i := x1]> m1 ∖ <[i := x2]> m2 = m1 ∖ <[i := x3]> m2.
 Proof.
-- 
GitLab