From 0c78d5d9abbe89419b4fb36dd35580060672f79f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 14 Mar 2021 14:13:53 +0100
Subject: [PATCH] Add `insert_delete_union`, tweak notations.

---
 theories/fin_maps.v | 15 +++++++++++----
 1 file changed, 11 insertions(+), 4 deletions(-)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 67d77eaf..c861db2d 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2107,11 +2107,18 @@ Lemma delete_union {A} (m1 m2 : M A) i :
   delete i (m1 ∪ m2) = delete i m1 ∪ delete i m2.
 Proof. apply delete_union_with. Qed.
 Lemma delete_insert_union {A} (m1 m2 : M A) i x :
-  m1 !! i = Some x ->
-  delete i m1 ∪ <[i := x]> m2 = m1 ∪ m2.
+  m1 !! i = Some x →
+  delete i m1 ∪ <[i:=x]> m2 = m1 ∪ m2.
 Proof.
-  intros Hmi. rewrite <-insert_union_r by apply lookup_delete.
-  rewrite insert_union_l, insert_delete, insert_id; done.
+  intros. rewrite <-insert_union_r by apply lookup_delete.
+  by rewrite insert_union_l, insert_delete, insert_id by done.
+Qed.
+Lemma insert_delete_union {A} (m1 m2 : M A) i x :
+  m1 !! i = None → m2 !! i = Some x →
+  <[i:=x]> m1 ∪ delete i m2 = m1 ∪ m2.
+Proof.
+  intros. rewrite <-insert_union_l by apply lookup_delete.
+  by rewrite insert_union_r, insert_delete, insert_id by done.
 Qed.
 Lemma map_Forall_union_1_1 {A} (m1 m2 : M A) P :
   map_Forall P (m1 ∪ m2) → map_Forall P m1.
-- 
GitLab