feat(data/list/zip): distributive lemmas (#7312)

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/data/list/zip.lean

@@ -195,6 +195,20 @@ by { rw ←zip_map', congr, exact map_id _ }
 lemma map_prod_right_eq_zip {l : list α} (f : α → β) : l.map (λ x, (f x, x)) = (l.map f).zip l :=
 by { rw ←zip_map', congr, exact map_id _ }
 
+lemma zip_with_comm (f : α → α → β) (comm : ∀ (x y : α), f x y = f y x)
+  (l l' : list α) :
+  zip_with f l l' = zip_with f l' l :=
+begin
+  induction l with hd tl hl generalizing l',
+  { simp },
+  { cases l',
+    { simp },
+    { simp [comm, hl] } }
+end
+
+instance (f : α → α → β) [is_symm_op α β f] : is_symm_op (list α) (list β) (zip_with f) :=
+⟨zip_with_comm f is_symm_op.symm_op⟩
+
 @[simp] theorem length_revzip (l : list α) : length (revzip l) = length l :=
 by simp only [revzip, length_zip, length_reverse, min_self]
 
@@ -297,4 +311,64 @@ begin
     { simp [hl, mul_add] } }
 end
 
+section distrib
+
+/-! ### Operations that can be applied before or after a `zip_with` -/
+
+variables (f : α → β → γ) (l : list α) (l' : list β) (n : ℕ)
+
+lemma zip_with_distrib_take :
+  (zip_with f l l').take n = zip_with f (l.take n) (l'.take n) :=
+begin
+  induction l with hd tl hl generalizing l' n,
+  { simp },
+  { cases l',
+    { simp },
+    { cases n,
+      { simp },
+      { simp [hl] } } }
+end
+
+lemma zip_with_distrib_drop :
+  (zip_with f l l').drop n = zip_with f (l.drop n) (l'.drop n) :=
+begin
+  induction l with hd tl hl generalizing l' n,
+  { simp },
+  { cases l',
+    { simp },
+    { cases n,
+      { simp },
+      { simp [hl] } } }
+end
+
+lemma zip_with_distrib_tail :
+  (zip_with f l l').tail = zip_with f l.tail l'.tail :=
+by simp_rw [←drop_one, zip_with_distrib_drop]
+
+lemma zip_with_append (f : α → β → γ) (l la : list α) (l' lb : list β) (h : l.length = l'.length) :
+  zip_with f (l ++ la) (l' ++ lb) = zip_with f l l' ++ zip_with f la lb :=
+begin
+  induction l with hd tl hl generalizing l',
+  { have : l' = [] := eq_nil_of_length_eq_zero (by simpa using h.symm),
+    simp [this], },
+  { cases l',
+    { simpa using h },
+    { simp only [add_left_inj, length] at h,
+      simp [hl _ h] } }
+end
+
+lemma zip_with_distrib_reverse (h : l.length = l'.length) :
+  (zip_with f l l').reverse = zip_with f l.reverse l'.reverse :=
+begin
+  induction l with hd tl hl generalizing l',
+  { simp },
+  { cases l' with hd' tl',
+    { simp },
+    { simp only [add_left_inj, length] at h,
+      have : tl.reverse.length = tl'.reverse.length := by simp [h],
+      simp [hl _ h, zip_with_append _ _ _ _ _ this] } }
+end
+
+end distrib
+
 end list