feat: move lemmas about lists from mathlib + add lemmas about Array.zipWith

Std/Data/Array/Lemmas.lean

@@ -218,6 +218,8 @@ theorem mapIdx_induction' (as : Array α) (f : Fin as.size → α → β)
     (a.mapIdx f)[i]'h = f ⟨i, this⟩ a[i] :=
   (mapIdx_induction' _ _ (fun i b => b = f i a[i]) fun _ => rfl).2 i _
 
+theorem size_eq_length_data (as : Array α) : as.size = as.data.length := rfl
+
 @[simp] theorem size_swap! (a : Array α) (i j) (hi : i < a.size) (hj : j < a.size) :
     (a.swap! i j).size = a.size := by simp [swap!, hi, hj]
 
@@ -336,3 +338,78 @@ theorem forIn_eq_data_forIn [Monad m]
       simp [← this]; congr; funext x; congr; funext b
       rw [loop (i := i)]; rw [← ij, Nat.succ_add]; rfl
   simp [forIn, Array.forIn]; rw [loop (Nat.zero_add _)]; rfl
+
+/-! ### zipWith / zip -/
+
+theorem zipWith_eq_zipWith_data (f : α → β → γ) (as : Array α) (bs : Array β) :
+    (as.zipWith bs f).data = as.data.zipWith f bs.data := by
+  let rec loop : ∀ (i : Nat) cs, i ≤ as.size → i ≤ bs.size →
+      (zipWithAux f as bs i cs).data = cs.data ++ (as.data.drop i).zipWith f (bs.data.drop i) := by
+    intro i cs hia hib
+    unfold zipWithAux
+    by_cases h : i = as.size ∨ i = bs.size
+    case pos =>
+      have : ¬(i < as.size) ∨ ¬(i < bs.size) := by
+        cases h <;> simp_all only [Nat.not_lt, Nat.le_refl, true_or, or_true]
+      -- Cleaned up aesop output below
+      simp_all only [Nat.not_lt]
+      cases h <;> [(cases this); (cases this)]
+      · simp_all only [Nat.le_refl, Nat.lt_irrefl, dite_false, List.drop_length,
+                      List.zipWith_nil_left, List.append_nil]
+      · simp_all only [Nat.le_refl, Nat.lt_irrefl, dite_false, List.drop_length,
+                      List.zipWith_nil_left, List.append_nil]
+      · simp_all only [Nat.le_refl, Nat.lt_irrefl, dite_false, List.drop_length,
+                      List.zipWith_nil_right, List.append_nil]
+        split <;> simp_all only [Nat.not_lt]
+      · simp_all only [Nat.le_refl, Nat.lt_irrefl, dite_false, List.drop_length,
+                      List.zipWith_nil_right, List.append_nil]
+        split <;> simp_all only [Nat.not_lt]
+    case neg =>
+      rw [not_or] at h
+      have has : i < as.size := Nat.lt_of_le_of_ne hia h.1
+      have hbs : i < bs.size := Nat.lt_of_le_of_ne hib h.2
+      simp only [has, hbs, dite_true]
+      rw [loop (i+1) _ has hbs, Array.push_data]
+      have h₁ : [f as[i] bs[i]] = List.zipWith f [as[i]] [bs[i]] := rfl
+      let i_as : Fin as.data.length := ⟨i, has⟩
+      let i_bs : Fin bs.data.length := ⟨i, hbs⟩
+      rw [h₁, List.append_assoc]
+      congr
+      rw [← List.zipWith_append (h := by simp), getElem_eq_data_get, getElem_eq_data_get]
+      show List.zipWith f ((List.get as.data i_as) :: List.drop (i_as + 1) as.data)
+        ((List.get bs.data i_bs) :: List.drop (i_bs + 1) bs.data) =
+        List.zipWith f (List.drop i as.data) (List.drop i bs.data)
+      simp only [List.get_cons_drop]
+  simp [zipWith, loop 0 #[] (by simp) (by simp)]
+termination_by loop i _ _ _ => as.size - i
+
+theorem size_zipWith (as : Array α) (bs : Array β) (f : α → β → γ) :
+    (as.zipWith bs f).size = min as.size bs.size := by
+  simp [size_eq_length_data, zipWith_eq_zipWith_data, List.length_zipWith]
+
+theorem size_zipWith_left (as : Array α) (bs : Array β) (h : as.size ≤ bs.size)
+    (f : α → β → γ) : (as.zipWith bs f).size = as.size := by
+  rw [size_zipWith, Nat.min_eq_left h]
+
+theorem size_zipWith_right (as : Array α) (bs : Array β) (h : bs.size ≤ as.size)
+    (f : α → β → γ) : (as.zipWith bs f).size = bs.size := by
+  rw [size_zipWith, Nat.min_eq_right h]
+
+theorem zip_eq_zip_data (as : Array α) (bs : Array β) :
+    (as.zip bs).data = as.data.zip bs.data :=
+  zipWith_eq_zipWith_data Prod.mk as bs
+
+theorem size_zip (as : Array α) (bs : Array β) :
+    (as.zip bs).size = min as.size bs.size :=
+  as.size_zipWith bs Prod.mk
+
+theorem size_zip_left (as : Array α) (bs : Array β) (h : as.size ≤ bs.size) :
+    (as.zip bs).size = as.size := by
+  rw [size_zip, Nat.min_eq_left h]
+
+theorem size_zip_right (as : Array α) (bs : Array β) (h : bs.size ≤ as.size) :
+    (as.zip bs).size = bs.size := by
+  rw [size_zip, Nat.min_eq_right h]
+
+@[simp] theorem size_zipWithIndex (as : Array α) : as.zipWithIndex.size = as.size :=
+  Array.size_mapIdx _ _

Std/Data/List/Lemmas.lean

@@ -99,6 +99,29 @@ theorem not_mem_cons_of_ne_of_not_mem {a y : α} {l : List α} : a ≠ y → a 
 theorem ne_and_not_mem_of_not_mem_cons {a y : α} {l : List α} : a ∉ y::l → a ≠ y ∧ a ∉ l :=
   fun p => ⟨ne_of_not_mem_cons p, not_mem_of_not_mem_cons p⟩
 
+/-! ### drop -/
+
+@[simp]
+theorem drop_one : ∀ l : List α, drop 1 l = tail l
+  | [] | _ :: _ => rfl
+
+theorem drop_add : ∀ (m n) (l : List α), drop (m + n) l = drop m (drop n l)
+  | _, 0, _ => rfl
+  | _, _ + 1, [] => drop_nil.symm
+  | m, n + 1, _ :: _ => drop_add m n _
+
+@[simp]
+theorem drop_left : ∀ l₁ l₂ : List α, drop (length l₁) (l₁ ++ l₂) = l₂
+  | [], _ => rfl
+  | _ :: l₁, l₂ => drop_left l₁ l₂
+
+theorem drop_left' {l₁ l₂ : List α} {n} (h : length l₁ = n) : drop n (l₁ ++ l₂) = l₂ := by
+  rw [← h]; apply drop_left
+
+theorem drop_eq_get_cons : ∀ {n} {l : List α} (h), drop n l = get l ⟨n, h⟩ :: drop (n + 1) l
+  | 0, _ :: _, _ => rfl
+  | n + 1, _ :: _, _ => drop_eq_get_cons (n := n) _
+
 /-! ### append -/
 
 theorem append_eq_append : List.append l₁ l₂ = l₁ ++ l₂ := rfl
@@ -206,6 +229,66 @@ theorem zipWith_get? {f : α → β → γ} :
     | nil => simp
     | cons b bs => cases i <;> simp_all
 
+@[simp]
+theorem zipWith_eq_nil_iff {f : α → β → γ} {l l'} : zipWith f l l' = [] ↔ l = [] ∨ l' = [] := by
+  cases l <;> cases l' <;> simp
+
+theorem lt_length_left_of_zipWith {f : α → β → γ} {i : Nat} {l : List α} {l' : List β}
+    (h : i < (zipWith f l l').length) : i < l.length := by
+  rw [length_zipWith, Nat.lt_min] at h
+  exact h.left
+
+theorem lt_length_right_of_zipWith {f : α → β → γ} {i : Nat} {l : List α} {l' : List β}
+    (h : i < (zipWith f l l').length) : i < l'.length := by
+  rw [length_zipWith, Nat.lt_min] at h
+  exact h.right
+
+theorem map_zipWith {δ : Type _} (f : α → β) (g : γ → δ → α) (l : List γ) (l' : List δ) :
+    map f (zipWith g l l') = zipWith (fun x y => f (g x y)) l l' := by
+  induction l generalizing l' with
+  | nil => simp
+  | cons hd tl hl =>
+    · cases l'
+      · simp
+      · simp [hl]
+
+theorem zipWith_distrib_take : (zipWith f l l').take n = zipWith f (l.take n) (l'.take n) := by
+  induction l generalizing l' n with
+  | nil => simp
+  | cons hd tl hl =>
+    cases l'
+    · simp
+    · cases n
+      · simp
+      · simp [hl]
+
+theorem zipWith_distrib_drop : (zipWith f l l').drop n = zipWith f (l.drop n) (l'.drop n) := by
+  induction l generalizing l' n with
+  | nil => simp
+  | cons hd tl hl =>
+    · cases l'
+      · simp
+      · cases n
+        · simp
+        · simp [hl]
+
+theorem zipWith_distrib_tail : (zipWith f l l').tail = zipWith f l.tail l'.tail := by
+  rw [← drop_one]; simp [zipWith_distrib_drop]
+
+theorem zipWith_append (f : α → β → γ) (l la : List α) (l' lb : List β)
+    (h : l.length = l'.length) :
+    zipWith f (l ++ la) (l' ++ lb) = zipWith f l l' ++ zipWith f la lb := by
+  induction l generalizing l' with
+  | nil =>
+    have : l' = [] := eq_nil_of_length_eq_zero (by simpa using h.symm)
+    simp [this]
+  | cons hl tl ih =>
+    cases l' with
+    | nil => simp at h
+    | cons head tail =>
+      simp only [length_cons, Nat.succ.injEq] at h
+      simp [ih _ h]
+
 /-! ### zipWithAll -/
 
 theorem zipWithAll_get? {f : Option α → Option β → γ} :
@@ -240,6 +323,55 @@ theorem zip_map_left (f : α → γ) (l₁ : List α) (l₂ : List β) :
 theorem zip_map_right (f : β → γ) (l₁ : List α) (l₂ : List β) :
     zip l₁ (l₂.map f) = (zip l₁ l₂).map (Prod.map id f) := by rw [← zip_map, map_id]
 
+theorem lt_length_left_of_zip {i : Nat} {l : List α} {l' : List β} (h : i < (zip l l').length) :
+    i < l.length :=
+  lt_length_left_of_zipWith h
+
+theorem lt_length_right_of_zip {i : Nat} {l : List α} {l' : List β} (h : i < (zip l l').length) :
+    i < l'.length :=
+  lt_length_right_of_zipWith h
+
+theorem zip_append :
+    ∀ {l₁ r₁ : List α} {l₂ r₂ : List β} (_h : length l₁ = length l₂),
+      zip (l₁ ++ r₁) (l₂ ++ r₂) = zip l₁ l₂ ++ zip r₁ r₂
+  | [], r₁, l₂, r₂, h => by simp only [eq_nil_of_length_eq_zero h.symm]; rfl
+  | l₁, r₁, [], r₂, h => by simp only [eq_nil_of_length_eq_zero h]; rfl
+  | a :: l₁, r₁, b :: l₂, r₂, h => by
+    simp only [cons_append, zip_cons_cons, zip_append (Nat.succ.inj h)]
+
+theorem zip_map' (f : α → β) (g : α → γ) :
+    ∀ l : List α, zip (l.map f) (l.map g) = l.map fun a => (f a, g a)
+  | [] => rfl
+  | a :: l => by simp only [map, zip_cons_cons, zip_map']
+
+theorem mem_zip {a b} : ∀ {l₁ : List α} {l₂ : List β}, (a, b) ∈ zip l₁ l₂ → a ∈ l₁ ∧ b ∈ l₂
+  | _ :: l₁, _ :: l₂, h => by
+    cases h
+    case head => simp
+    case tail h =>
+    · have := mem_zip h
+      exact ⟨Mem.tail _ this.1, Mem.tail _ this.2⟩
+
+theorem map_fst_zip :
+    ∀ (l₁ : List α) (l₂ : List β), l₁.length ≤ l₂.length → map Prod.fst (zip l₁ l₂) = l₁
+  | [], bs, _ => rfl
+  | _ :: as, _ :: bs, h => by
+    simp [Nat.succ_le_succ_iff] at h
+    show _ :: map Prod.fst (zip as bs) = _ :: as
+    rw [map_fst_zip as bs h]
+  | a :: as, [], h => by simp at h
+
+theorem map_snd_zip :
+    ∀ (l₁ : List α) (l₂ : List β), l₂.length ≤ l₁.length → map Prod.snd (zip l₁ l₂) = l₂
+  | _, [], _ => by
+    rw [zip_nil_right]
+    rfl
+  | [], b :: bs, h => by simp at h
+  | a :: as, b :: bs, h => by
+    simp [Nat.succ_le_succ_iff] at h
+    show _ :: map Prod.snd (zip as bs) = _ :: bs
+    rw [map_snd_zip as bs h]
+
 /-! ### join -/
 
 theorem mem_join : ∀ {L : List (List α)}, a ∈ L.join ↔ ∃ l, l ∈ L ∧ a ∈ l