From cd0b7f48af3be59a0ba477f35489af621273da77 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dan@covariant.me>
Date: Mon, 29 May 2017 18:49:43 +0200
Subject: [PATCH] Some map_zip/map_zip_with properties.

---
 theories/fin_maps.v | 81 ++++++++++++++++++++++++++++++++++++++++-----
 1 file changed, 73 insertions(+), 8 deletions(-)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 2cc3150a..3c94c790 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -843,14 +843,6 @@ Proof.
     rewrite elem_of_map_to_list in Hj; simplify_option_eq.
 Qed.
 
-(** Properties of the zip_with function *)
-Lemma map_lookup_zip_with {A B C} (f : A → B → C) m1 m2 i :
-  map_zip_with f m1 m2 !! i = x ← m1 !! i; y ← m2 !! i; Some (f x y).
-Proof.
-  unfold map_zip_with. rewrite lookup_merge by done.
-  by destruct (m1 !! i), (m2 !! i).
-Qed.
-
 (** ** Properties of conversion from collections *)
 Section map_of_to_collection.
   Context {A : Type} `{FinCollection B C}.
@@ -1136,6 +1128,79 @@ Lemma insert_merge_r m1 m2 i x z :
 Proof. by intros; apply partial_alter_merge_r. Qed.
 End more_merge.
 
+(** Properties of the zip_with function *)
+Lemma map_lookup_zip_with {A B C} (f : A → B → C) m1 m2 i :
+  map_zip_with f m1 m2 !! i = x ← m1 !! i; y ← m2 !! i; Some (f x y).
+Proof.
+  unfold map_zip_with. rewrite lookup_merge by done.
+  by destruct (m1 !! i), (m2 !! i).
+Qed.
+
+Lemma map_zip_with_empty {A B C} (f : A → B → C) :
+  map_zip_with f ∅ ∅ = ∅.
+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 m2 i x y z :
+  f y z = x →
+  <[i:=x]>(map_zip_with f m1 m2) = map_zip_with f (<[i:=y]>m1) (<[i:=z]>m2).
+Proof.
+  intros Hf. unfold map_zip_with.
+  erewrite insert_merge; [ auto | by compute | by rewrite Hf ].
+Qed.
+
+Lemma map_zip_with_fmap {A' A B' B C} (f : A → B → C)
+      (g1 : A' → A) (g2 : B' → B) m1 m2 :
+  map_zip_with f (g1 <$> m1) (g2 <$> m2) = map_zip_with (λ x y, f (g1 x) (g2 y)) m1 m2.
+Proof.
+  apply map_eq; intro i.
+  rewrite ?map_lookup_zip_with. rewrite ?lookup_fmap.
+  by destruct (m1 !! i), (m2 !! i).
+Qed.
+
+Lemma map_zip_with_fmap_1 {A' A B C} (f : A → B → C)
+      (g : A' → A) m1 m2 :
+  map_zip_with f (g <$> m1) m2 = map_zip_with (λ x y, f (g x) y) m1 m2.
+Proof.
+  rewrite <- (map_fmap_id m2) at 1.
+  by rewrite map_zip_with_fmap; simpl. 
+Qed.
+
+Lemma map_zip_with_fmap_2 {A B' B C} (f : A → B → C)
+      (g : B' → B) m1 m2 :
+  map_zip_with f m1 (g <$> m2) = map_zip_with (λ x y, f x (g y)) m1 m2.
+Proof.
+  rewrite <- (map_fmap_id m1) at 1.
+  by rewrite map_zip_with_fmap; simpl. 
+Qed.
+
+Lemma map_fmap_zip_with {A B C D} (f : A → B → C) (g : C → D) m1 m2 :
+  g <$> map_zip_with f m1 m2 = map_zip_with (λ x y, g (f x y)) m1 m2.
+Proof.
+  apply map_eq; intro i.
+  rewrite lookup_fmap. rewrite ?map_lookup_zip_with.
+  by destruct (m1 !! i), (m2 !! i).
+Qed.
+
+Lemma map_zip_with_map_zip {A B C} (f : A → B → C) m1 m2 :
+  map_zip_with f m1 m2 = curry f <$> map_zip m1 m2.
+Proof.
+  apply map_eq; intro i.
+  rewrite lookup_fmap; rewrite ?map_lookup_zip_with; rewrite ?lookup_fmap.
+  by destruct (m1 !! i), (m2 !! i).
+Qed.
+
+Lemma map_fmap_zip {A' A B' B} (g1 : A' → A) (g2 : B' → B) m1 m2 :
+  map_zip (fmap g1 m1) (fmap g2 m2)
+  = prod_map g1 g2 <$> map_zip m1 m2.
+Proof.
+  rewrite map_zip_with_fmap. 
+  rewrite map_zip_with_map_zip.
+  generalize (map_zip m1 m2); intro m. apply map_eq; intro i.
+  by rewrite ?lookup_fmap; destruct (m !! i) as [[x1 x2]|].
+Qed.
+
 (** ** Properties on the [map_relation] relation *)
 Section Forall2.
 Context {A B} (R : A → B → Prop) (P : A → Prop) (Q : B → Prop).
-- 
GitLab