From 851230d970c349f9aa4a271de1d66a4f2faab89b Mon Sep 17 00:00:00 2001
From: Kimaya Bedarkar <kbedarka@mpi-sws.org>
Date: Tue, 14 Jan 2025 14:14:18 +0100
Subject: [PATCH] add some zip lemmas

---
 CHANGELOG.md |  4 +++-
 stdpp/list.v | 17 ++++++++++++++++-
 2 files changed, 19 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 1c0b56f1..53817951 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -11,6 +11,8 @@ API-breaking change is listed.
   automatically adds `_` until the given lemma takes no more arguments.
 - Rename `map_filter_empty_iff` to `map_empty_filter` and add
   `map_empty_filter_1` and `map_empty_filter_2`. (by Michael Sammler)
+- Add lemma about `zip_with`: `lookup_zip_with_None` and add lemmas for `zip`:
+  `length_zip`, `zip_nil_inv`, `lookup_zip_Some`,`lookup_zip_None` (by Kimaya Bedarkar)
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
@@ -108,7 +110,7 @@ and Yiyun Liu. Thanks a lot to everyone involved!
 - Add `gmultiset_map` and associated lemmas. (by Marijn van Wezel)
 - Add `CProd` type class for Cartesian products; with instances for `list`,
   `gset`, `boolset`, `MonadSet` (i.e., `propset`, `listset`); and `set_solver`
-  tactic support. (by Thibaut Pérami)
+	tactic support. (by Thibaut Pérami)
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
diff --git a/stdpp/list.v b/stdpp/list.v
index 64096df6..4a96bd88 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -4915,6 +4915,10 @@ Section zip_with.
     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 lookup_zip_with_None l k i  :
+    zip_with f l k !! i = None
+    ↔ l !! i = None ∨ k !! i = None.
+  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.
@@ -5054,10 +5058,21 @@ Section zip.
   Lemma elem_of_zip_l x1 x2 l k :
     (x1, x2) ∈ zip l k → x1 ∈ l.
   Proof. intros ?%elem_of_zip_with. naive_solver. Qed.
-
   Lemma elem_of_zip_r x1 x2 l k :
     (x1, x2) ∈ zip l k → x2 ∈ k.
   Proof. intros ?%elem_of_zip_with. naive_solver. Qed.
+  Lemma length_zip l k :
+    length (zip l k) = min (length l) (length k).
+  Proof. by rewrite length_zip_with. Qed.
+  Lemma zip_nil_inv l k :
+    zip l k = [] → l = [] ∨ k = [].
+  Proof. intros. by eapply zip_with_nil_inv. Qed.
+  Lemma lookup_zip_Some l k i x y :
+    zip l k !! i = Some (x, y) ↔ l !! i = Some x ∧ k !! i = Some y.
+  Proof. rewrite lookup_zip_with_Some. naive_solver. Qed.
+  Lemma lookup_zip_None l k i :
+    zip l k !! i = None ↔ l !! i = None ∨ k !! i = None.
+  Proof. by rewrite lookup_zip_with_None. Qed.
 End zip.
 
 Lemma zip_diag {A} (l : list A) :
-- 
GitLab