Merge main into nightly-testing

Author: leanprover-community-mathlib4-bot

Batteries/Data/List/Basic.lean

@@ -1066,3 +1066,14 @@ where
   | a :: as, acc => match (a :: as).dropPrefix? i with
     | none => go as (a :: acc)
     | some s => (acc.reverse, s)
+
+/--
+Computes the product of the elements of a list.
+
+Examples:
+
+[a, b, c].prod = a * (b * (c * 1))
+[2, 3, 5].prod = 30
+-/
+@[expose] def prod [Mul α] [One α] (xs : List α) : α :=
+  xs.foldr (· * ·) 1

Batteries/Data/List/Lemmas.lean

@@ -660,3 +660,88 @@ theorem append_eq_of_isPrefixOf?_eq_some [BEq α] [LawfulBEq α] {xs ys zs : Lis
 
 theorem append_eq_of_isSuffixOf?_eq_some [BEq α] [LawfulBEq α] {xs ys zs : List α}
     (h : xs.isSuffixOf? ys = some zs) : zs ++ xs = ys := by simp_all
+
+/-! ### sum/prod -/
+
+private theorem foldr_eq_foldl_aux (f : α → α → α) (init : α) [Std.Associative f]
+    [Std.LawfulIdentity f init] {l : List α} :
+    l.foldl f a = f a (l.foldl f init) := by
+  induction l generalizing a with
+  | nil => simp [Std.LawfulRightIdentity.right_id]
+  | cons b l ih =>
+    simp [Std.LawfulLeftIdentity.left_id, ih (a := f a b), ih (a := b), Std.Associative.assoc]
+
+theorem foldr_eq_foldl (f : α → α → α) (init : α) [Std.Associative f]
+    [Std.LawfulIdentity f init] {l : List α} :
+    l.foldr f init = l.foldl f init := by
+  induction l with
+  | nil => rfl
+  | cons a l ih => simp [ih, Std.LawfulLeftIdentity.left_id, foldr_eq_foldl_aux (a := a)]
+
+@[simp, grind =]
+theorem prod_nil [Mul α] [One α] : ([] : List α).prod = 1 := rfl
+
+@[simp, grind =]
+theorem prod_cons [Mul α] [One α] {a : α} {l : List α} : (a :: l).prod = a * l.prod := rfl
+
+theorem prod_one_cons [Mul α] [One α] [Std.LawfulLeftIdentity (α := α) (· * ·) 1] {l : List α} :
+    (1 :: l).prod = l.prod := by simp [Std.LawfulLeftIdentity.left_id]
+
+theorem prod_singleton [Mul α] [One α] [Std.LawfulRightIdentity (α := α) (· * ·) 1] {a : α} :
+  [a].prod = a := by simp [Std.LawfulRightIdentity.right_id]
+
+theorem prod_pair [Mul α] [One α] [Std.LawfulRightIdentity (α := α) (· * ·) 1] {a b : α} :
+  [a, b].prod = a * b := by simp [Std.LawfulRightIdentity.right_id]
+
+@[simp, grind =]
+theorem prod_append [Mul α] [One α] [Std.LawfulLeftIdentity (α := α) (· * ·) 1]
+    [Std.Associative (α := α) (· * ·)] {l₁ l₂ : List α} : (l₁ ++ l₂).prod = l₁.prod * l₂.prod := by
+  induction l₁ with simp [Std.LawfulLeftIdentity.left_id, Std.Associative.assoc, *]
+
+theorem prod_concat [Mul α] [One α] [Std.LawfulIdentity (α := α) (· * ·) 1]
+    [Std.Associative (α := α) (· * ·)] {l : List α} {a : α} :
+    (l.concat a).prod = l.prod * a := by simp [Std.LawfulRightIdentity.right_id]
+
+@[simp, grind =]
+theorem prod_flatten [Mul α] [One α] [Std.LawfulIdentity (α := α) (· * ·) 1]
+    [Std.Associative (α := α) (· * ·)] {l : List (List α)} :
+    l.flatten.prod = (l.map prod).prod := by
+  induction l with simp [*]
+
+theorem prod_eq_foldr [Mul α] [One α] {l : List α} :
+    l.prod = l.foldr (· * ·) 1 := rfl
+
+theorem prod_eq_foldl [Mul α] [One α] [Std.Associative (α := α) (· * ·)]
+    [Std.LawfulIdentity (α := α) (· * ·) 1] {l : List α} :
+    l.prod = l.foldl (· * ·) 1 := foldr_eq_foldl ..
+
+theorem sum_zero_cons [Add α] [Zero α] [Std.LawfulLeftIdentity (α := α) (· + ·) 0] {l : List α} :
+    (0 :: l).sum = l.sum := by simp [Std.LawfulLeftIdentity.left_id]
+
+theorem sum_singleton [Add α] [Zero α] [Std.LawfulRightIdentity (α := α) (· + ·) 0] {a : α} :
+  [a].sum = a := by simp [Std.LawfulRightIdentity.right_id]
+
+theorem sum_pair [Add α] [Zero α] [Std.LawfulRightIdentity (α := α) (· + ·) 0] {a b : α} :
+  [a, b].sum = a + b := by simp [Std.LawfulRightIdentity.right_id]
+
+@[simp, grind =]
+theorem sum_append [Add α] [Zero α] [Std.LawfulLeftIdentity (α := α) (· + ·) 0]
+    [Std.Associative (α := α) (· + ·)] {l₁ l₂ : List α} : (l₁ ++ l₂).sum = l₁.sum + l₂.sum := by
+  induction l₁ with simp [Std.LawfulLeftIdentity.left_id, Std.Associative.assoc, *]
+
+theorem sum_concat [Add α] [Zero α] [Std.LawfulIdentity (α := α) (· + ·) 0]
+    [Std.Associative (α := α) (· + ·)] {l : List α} {a : α} :
+    (l.concat a).sum = l.sum + a := by simp [Std.LawfulRightIdentity.right_id]
+
+@[simp, grind =]
+theorem sum_flatten [Add α] [Zero α] [Std.LawfulIdentity (α := α) (· + ·) 0]
+    [Std.Associative (α := α) (· + ·)] {l : List (List α)} :
+    l.flatten.sum = (l.map sum).sum := by
+  induction l with simp [*]
+
+theorem sum_eq_foldr [Add α] [Zero α] {l : List α} :
+    l.sum = l.foldr (· + ·) 0 := rfl
+
+theorem sum_eq_foldl [Add α] [Zero α] [Std.Associative (α := α) (· + ·)]
+    [Std.LawfulIdentity (α := α) (· + ·) 0] {l : List α} :
+    l.sum = l.foldl (· + ·) 0 := foldr_eq_foldl ..