From 6b94ffb4f831ab24e778b3bb04a2fe720cf3488f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 23 Jun 2021 14:33:05 +0200
Subject: [PATCH] add {fst,snd}_map_zip

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 8167e863..d4a63cb7 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1713,6 +1713,16 @@ Lemma map_zip_diag {A} (m : M A) :
   map_zip m m = (λ x, (x, x)) <$> m.
 Proof. apply map_zip_with_diag. Qed.
 
+Lemma fst_map_zip {A B} (m1 : M A) (m2 : M B) :
+  (∀ k : K, is_Some (m1 !! k) → is_Some (m2 !! k)) →
+  fst <$> map_zip m1 m2 = m1.
+Proof. intros ?. by apply map_fmap_zip_with_l. Qed.
+
+Lemma snd_map_zip {A B} (m1 : M A) (m2 : M B) :
+  (∀ k : K, is_Some (m2 !! k) → is_Some (m1 !! k)) →
+  snd <$> map_zip m1 m2 = m2.
+Proof. intros ?. by apply map_fmap_zip_with_r. Qed.
+
 (** ** Properties on the [map_relation] relation *)
 Section Forall2.
   Context {A B} (R : A → B → Prop) (P : A → Prop) (Q : B → Prop).
-- 
GitLab