From af4ec931f107252a33a24a9b101dc09462a3fc26 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 14 Mar 2021 14:51:12 +0100
Subject: [PATCH] Add lemma `map_difference_delete`.

---
 theories/fin_maps.v | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 2d3ee4b0..ed47364b 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2390,13 +2390,21 @@ Qed.
 Global Instance map_difference_right_id {A} : RightId (=) (∅:M A) (∖) := _.
 Lemma map_difference_empty {A} (m : M A) : m ∖ ∅ = m.
 Proof. by rewrite (right_id _ _). Qed.
-Lemma map_difference_delete_insert {A} (m1 m2 : M A) i x :
+Lemma map_delete_difference {A} (m1 m2 : M A) i x :
   delete i (m1 ∖ m2) = m1 ∖ <[i:=x]> m2.
 Proof.
   apply map_eq. intros j. apply option_eq. intros y.
   rewrite lookup_delete_Some, !lookup_difference_Some, lookup_insert_None.
   naive_solver.
 Qed.
+Lemma map_difference_delete {A} (m1 m2 : M A) i x :
+  m1 !! i = Some x →
+  m1 ∖ delete i m2 = <[i:=x]> (m1 ∖ m2).
+Proof.
+  intros. apply map_eq. intros j. apply option_eq. intros y.
+  rewrite lookup_insert_Some, !lookup_difference_Some, lookup_delete_None.
+  destruct (decide (i = j)); naive_solver.
+Qed.
 End theorems.
 
 (** ** The seq operation *)
-- 
GitLab