From 8f69a15947335a4fafd2ab285081758c918e27e3 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 19 Jan 2021 10:40:40 +0100
Subject: [PATCH] add zip_with_diag and zip_diag

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

diff --git a/theories/list.v b/theories/list.v
index 71b761b1..71304355 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -4191,6 +4191,10 @@ Section zip_with.
 
 End zip_with.
 
+Lemma zip_with_diag {A C} (f : A → A → C) l :
+  zip_with f l l = (λ x, f x x) <$> l.
+Proof. induction l as [|?? IH]; [done|]. simpl. rewrite IH. done. Qed.
+
 Lemma zip_with_sublist_alter {A B} (f : A → B → A) g l k i n l' k' :
   length l = length k →
   sublist_lookup i n l = Some l' → sublist_lookup i n k = Some k' →
@@ -4237,6 +4241,10 @@ Section zip.
   Proof. intros ?%elem_of_zip_with. naive_solver. Qed.
 End zip.
 
+Lemma zip_diag {A} (l : list A) :
+  zip l l = (λ x, (x, x)) <$> l.
+Proof. apply zip_with_diag. Qed.
+
 Lemma elem_of_zipped_map {A B} (f : list A → list A → A → B) l k x :
   x ∈ zipped_map f l k ↔
     ∃ k' k'' y, k = k' ++ [y] ++ k'' ∧ x = f (reverse k' ++ l) k'' y.
-- 
GitLab