From 50efdf9c25c163bea884a3dfbbe79db5d7b1e914 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 16 Jan 2020 21:25:10 +0100
Subject: [PATCH] Add lemma `map_lookup_zip_with_Some`.

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index f065292b..707fea31 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1336,6 +1336,10 @@ Proof.
   unfold map_zip_with. rewrite lookup_merge by done.
   by destruct (m1 !! i), (m2 !! i).
 Qed.
+Lemma map_lookup_zip_with_Some {A B C} (f : A → B → C) (m1 : M A) (m2 : M B) i z :
+  map_zip_with f m1 m2 !! i = Some z ↔
+    ∃ x y, z = f x y ∧ m1 !! i = Some x ∧ m2 !! i = Some y.
+Proof. rewrite map_lookup_zip_with. destruct (m1 !! i), (m2 !! i); naive_solver. Qed.
 
 Lemma map_zip_with_empty {A B C} (f : A → B → C) :
   map_zip_with f (∅ : M A) (∅ : M B) = ∅.
-- 
GitLab