From ff3837451f65a8fe341c6de0e6e3f543dfce3e2d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 16 Jan 2020 20:47:42 +0100
Subject: [PATCH] Add lemma `lookup_zip_with_Some`.

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

diff --git a/theories/list.v b/theories/list.v
index 8bcead87..aa5618a1 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -3770,6 +3770,10 @@ Section zip_with.
     revert k i. induction l; intros [|??] [|?]; f_equal/=; auto.
     by destruct (_ !! _).
   Qed.
+  Lemma lookup_zip_with_Some l k i z :
+    zip_with f l k !! i = Some z
+    ↔ ∃ x y, z = f x y ∧ l !! i = Some x ∧ k !! i = Some y.
+  Proof. rewrite lookup_zip_with. destruct (l !! i), (k !! i); naive_solver. Qed.
   Lemma insert_zip_with l k i x y :
     <[i:=f x y]>(zip_with f l k) = zip_with f (<[i:=x]>l) (<[i:=y]>k).
   Proof. revert i k. induction l; intros [|?] [|??]; f_equal/=; auto. Qed.
-- 
GitLab