From af40bc7b2bd2d693a3981658540e45daf8901198 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Tue, 26 Mar 2019 18:49:15 +0100
Subject: [PATCH] Add `map_delete_zip_with`.

---
 theories/fin_maps.v | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 9ba1fb34..63daffbe 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1250,6 +1250,9 @@ Lemma insert_merge (m1 : M A) (m2 : M B) i x y z :
   f (Some y) (Some z) = Some x →
   <[i:=x]>(merge f m1 m2) = merge f (<[i:=y]>m1) (<[i:=z]>m2).
 Proof. by intros; apply partial_alter_merge. Qed.
+Lemma delete_merge (m1 : M A) (m2 : M B) i :
+  delete i (merge f m1 m2) = merge f (delete i m1) (delete i m2).
+Proof. by intros; apply partial_alter_merge. Qed.
 Lemma merge_singleton i x y z :
   f (Some y) (Some z) = Some x →
   merge f ({[i := y]} : M A) ({[i := z]} : M B) = {[i := x]}.
@@ -1280,6 +1283,9 @@ Proof. unfold map_zip_with. by rewrite merge_empty by done. Qed.
 Lemma map_insert_zip_with {A B C} (f : A → B → C) (m1 : M A) (m2 : M B) i y z :
   <[i:=f y z]>(map_zip_with f m1 m2) = map_zip_with f (<[i:=y]>m1) (<[i:=z]>m2).
 Proof. unfold map_zip_with. by erewrite insert_merge by done. Qed.
+Lemma map_delete_zip_with {A B C} (f : A → B → C) (m1 : M A) (m2 : M B) i :
+  delete i (map_zip_with f m1 m2) = map_zip_with f (delete i m1) (delete i m2).
+Proof. unfold map_zip_with. by rewrite delete_merge. Qed.
 Lemma map_zip_with_singleton {A B C} (f : A → B → C) i x y :
   map_zip_with f ({[ i := x ]} : M A) ({[ i := y ]} : M B) = {[ i := f x y ]}.
 Proof. unfold map_zip_with. by erewrite merge_singleton. Qed.
-- 
GitLab