From fc52ac5385fd6a22d781c92b2fe306f3da332ac5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 17 Jan 2021 13:31:00 +0100
Subject: [PATCH] Add lemmas `map_fmap_zip_with_{l,r}`.

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index f07fdbb4..d23895b0 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1564,6 +1564,27 @@ Proof.
   by rewrite !lookup_fmap; destruct (m !! i) as [[x1 x2]|].
 Qed.
 
+Lemma map_fmap_zip_with_l
+    {A B C} (f : A → B → C) (g : C → A) (m1 : M A) (m2 : M B) :
+  (∀ x y, g (f x y) = x) →
+  (∀ k, is_Some (m1 !! k) → is_Some (m2 !! k)) →
+  g <$> map_zip_with f m1 m2 = m1.
+Proof.
+  intros ? Hm. apply map_eq; intros k. rewrite lookup_fmap, map_lookup_zip_with.
+  destruct (m1 !! _) as [x|] eqn:?; simpl; [|done].
+  destruct (Hm k) as [y ->]; [by eauto|]. by f_equal/=.
+Qed.
+Lemma map_fmap_zip_with_r
+    {A B C} (f : A → B → C) (g : C → B) (m1 : M A) (m2 : M B) :
+  (∀ x y, g (f x y) = y) →
+  (∀ k, is_Some (m2 !! k) → is_Some (m1 !! k)) →
+  g <$> map_zip_with f m1 m2 = m2.
+Proof.
+  intros ? Hm. apply map_eq; intros k. rewrite lookup_fmap, map_lookup_zip_with.
+  destruct (m2 !! _) as [x|] eqn:?; simpl; [|by destruct (m1 !! _)].
+  destruct (Hm k) as [y ->]; [by eauto|]. by f_equal/=.
+Qed.
+
 (** ** Properties on the [map_relation] relation *)
 Section Forall2.
   Context {A B} (R : A → B → Prop) (P : A → Prop) (Q : B → Prop).
-- 
GitLab