From ad2105dc942c12cab201fe24af3acef0d15d9e6b Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Wed, 8 Apr 2026 14:01:49 +1000 Subject: [PATCH] feat: add `List.prod`, `Array.prod`, and `Vector.prod` (#13200) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR adds `prod` (multiplicative fold) for `List`, `Array`, and `Vector`, mirroring the existing `sum` API. Includes basic simp lemmas (`prod_nil`, `prod_cons`, `prod_append`, `prod_singleton`, `prod_reverse`, `prod_push`, `prod_eq_foldl`), Nat-specialized lemmas (`prod_pos_iff_forall_pos_nat`, `prod_eq_zero_iff_exists_zero_nat`, `prod_replicate_nat`), Int-specialized lemmas (`prod_replicate_int`), cross-type lemmas (`prod_toArray`, `prod_toList`), and `Perm.prod_nat` with grind patterns. The min/max pigeonhole-style bounds from the `sum` Nat/Int files are omitted as they don't have natural multiplicative analogues. 🤖 Prepared with Claude Code Co-authored-by: Claude Opus 4.6 (1M context) --- src/Init/Data/Array/Basic.lean | 11 +++++++ src/Init/Data/Array/Int.lean | 14 +++++++++ src/Init/Data/Array/Lemmas.lean | 41 ++++++++++++++++++++++++++ src/Init/Data/Array/Nat.lean | 21 ++++++++++++++ src/Init/Data/List/Basic.lean | 14 +++++++++ src/Init/Data/List/Int.lean | 1 + src/Init/Data/List/Int/Prod.lean | 31 ++++++++++++++++++++ src/Init/Data/List/Lemmas.lean | 23 +++++++++++++++ src/Init/Data/List/Nat.lean | 1 + src/Init/Data/List/Nat/Prod.lean | 50 ++++++++++++++++++++++++++++++++ src/Init/Data/List/Perm.lean | 10 +++++++ src/Init/Data/List/ToArray.lean | 3 ++ src/Init/Data/Vector/Basic.lean | 10 +++++++ src/Init/Data/Vector/Int.lean | 12 ++++++++ src/Init/Data/Vector/Lemmas.lean | 46 +++++++++++++++++++++++++++++ src/Init/Data/Vector/Nat.lean | 19 ++++++++++++ 16 files changed, 307 insertions(+) create mode 100644 src/Init/Data/List/Int/Prod.lean create mode 100644 src/Init/Data/List/Nat/Prod.lean diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index 17bb601808..458e74b51d 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -1085,6 +1085,17 @@ Examples: def sum {α} [Add α] [Zero α] : Array α → α := foldr (· + ·) 0 +/-- +Computes the product of the elements of an array. + +Examples: + * `#[a, b, c].prod = a * (b * (c * 1))` + * `#[1, 2, 5].prod = 10` +-/ +@[inline, expose] +def prod {α} [Mul α] [One α] : Array α → α := + foldr (· * ·) 1 + /-- Counts the number of elements in the array `as` that satisfy the Boolean predicate `p`. diff --git a/src/Init/Data/Array/Int.lean b/src/Init/Data/Array/Int.lean index d6ace84354..5491cddead 100644 --- a/src/Init/Data/Array/Int.lean +++ b/src/Init/Data/Array/Int.lean @@ -7,6 +7,7 @@ module prelude public import Init.Data.List.Int.Sum +public import Init.Data.List.Int.Prod public import Init.Data.Array.MinMax import Init.Data.Int.Lemmas @@ -74,4 +75,17 @@ theorem sum_div_length_le_max_of_max?_eq_some_int {xs : Array Int} (h : xs.max? simpa [List.max?_toArray, List.sum_toArray] using List.sum_div_length_le_max_of_max?_eq_some_int (by simpa using h) +@[simp] theorem prod_replicate_int {n : Nat} {a : Int} : (replicate n a).prod = a ^ n := by + rw [← List.toArray_replicate, List.prod_toArray] + simp + +theorem prod_append_int {as₁ as₂ : Array Int} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by + simp [prod_append] + +theorem prod_reverse_int (xs : Array Int) : xs.reverse.prod = xs.prod := by + simp [prod_reverse] + +theorem prod_eq_foldl_int {xs : Array Int} : xs.prod = xs.foldl (init := 1) (· * ·) := by + simp only [foldl_eq_foldr_reverse, Int.mul_comm, ← prod_eq_foldr, prod_reverse_int] + end Array diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index 0f1ef6d3df..34baad6c73 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -4380,6 +4380,47 @@ theorem sum_eq_foldl [Zero α] [Add α] [Std.Associative (α := α) (· + ·)] xs.sum = xs.foldl (init := 0) (· + ·) := by simp [← sum_toList, List.sum_eq_foldl] +/-! ### prod -/ + +@[simp, grind =] theorem prod_empty [Mul α] [One α] : (#[] : Array α).prod = 1 := rfl +theorem prod_eq_foldr [Mul α] [One α] {xs : Array α} : + xs.prod = xs.foldr (init := 1) (· * ·) := + rfl + +@[simp, grind =] +theorem prod_toList [Mul α] [One α] {as : Array α} : as.toList.prod = as.prod := by + cases as + simp [Array.prod, List.prod] + +@[simp, grind =] +theorem prod_append [One α] [Mul α] [Std.Associative (α := α) (· * ·)] + [Std.LawfulLeftIdentity (α := α) (· * ·) 1] + {as₁ as₂ : Array α} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by + simp [← prod_toList, List.prod_append] + +@[simp, grind =] +theorem prod_singleton [Mul α] [One α] [Std.LawfulRightIdentity (· * ·) (1 : α)] {x : α} : + #[x].prod = x := by + simp [Array.prod_eq_foldr, Std.LawfulRightIdentity.right_id x] + +@[simp, grind =] +theorem prod_push [Mul α] [One α] [Std.Associative (α := α) (· * ·)] + [Std.LawfulIdentity (· * ·) (1 : α)] {xs : Array α} {x : α} : + (xs.push x).prod = xs.prod * x := by + simp [Array.prod_eq_foldr, Std.LawfulRightIdentity.right_id, Std.LawfulLeftIdentity.left_id, + ← Array.foldr_assoc] + +@[simp, grind =] +theorem prod_reverse [One α] [Mul α] [Std.Associative (α := α) (· * ·)] + [Std.Commutative (α := α) (· * ·)] + [Std.LawfulLeftIdentity (α := α) (· * ·) 1] (xs : Array α) : xs.reverse.prod = xs.prod := by + simp [← prod_toList, List.prod_reverse] + +theorem prod_eq_foldl [One α] [Mul α] [Std.Associative (α := α) (· * ·)] + [Std.LawfulIdentity (· * ·) (1 : α)] {xs : Array α} : + xs.prod = xs.foldl (init := 1) (· * ·) := by + simp [← prod_toList, List.prod_eq_foldl] + theorem foldl_toList_eq_flatMap {l : List α} {acc : Array β} {F : Array β → α → Array β} {G : α → List β} (H : ∀ acc a, (F acc a).toList = acc.toList ++ G a) : diff --git a/src/Init/Data/Array/Nat.lean b/src/Init/Data/Array/Nat.lean index 419c79ad05..32fe8e22e1 100644 --- a/src/Init/Data/Array/Nat.lean +++ b/src/Init/Data/Array/Nat.lean @@ -8,6 +8,7 @@ module prelude public import Init.Data.Array.MinMax import Init.Data.List.Nat.Sum +import Init.Data.List.Nat.Prod import Init.Data.Array.Lemmas public section @@ -81,4 +82,24 @@ theorem sum_div_length_le_max_of_max?_eq_some_nat {xs : Array Nat} (h : xs.max? simpa [List.max?_toArray, List.sum_toArray] using List.sum_div_length_le_max_of_max?_eq_some_nat (by simpa using h) +protected theorem prod_pos_iff_forall_pos_nat {xs : Array Nat} : 0 < xs.prod ↔ ∀ x ∈ xs, 0 < x := by + simp [← prod_toList, List.prod_pos_iff_forall_pos_nat] + +protected theorem prod_eq_zero_iff_exists_zero_nat {xs : Array Nat} : + xs.prod = 0 ↔ ∃ x ∈ xs, x = 0 := by + simp [← prod_toList, List.prod_eq_zero_iff_exists_zero_nat] + +@[simp] theorem prod_replicate_nat {n : Nat} {a : Nat} : (replicate n a).prod = a ^ n := by + rw [← List.toArray_replicate, List.prod_toArray] + simp + +theorem prod_append_nat {as₁ as₂ : Array Nat} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by + simp [prod_append] + +theorem prod_reverse_nat (xs : Array Nat) : xs.reverse.prod = xs.prod := by + simp [prod_reverse] + +theorem prod_eq_foldl_nat {xs : Array Nat} : xs.prod = xs.foldl (init := 1) (· * ·) := by + simp only [foldl_eq_foldr_reverse, Nat.mul_comm, ← prod_eq_foldr, prod_reverse_nat] + end Array diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean index cd81857504..3f2a65a3fd 100644 --- a/src/Init/Data/List/Basic.lean +++ b/src/Init/Data/List/Basic.lean @@ -2056,6 +2056,20 @@ def sum {α} [Add α] [Zero α] : List α → α := @[simp, grind =] theorem sum_cons [Add α] [Zero α] {a : α} {l : List α} : (a::l).sum = a + l.sum := rfl theorem sum_eq_foldr [Add α] [Zero α] {l : List α} : l.sum = l.foldr (· + ·) 0 := rfl +/-- +Computes the product of the elements of a list. + +Examples: + * `[a, b, c].prod = a * (b * (c * 1))` + * `[1, 2, 5].prod = 10` +-/ +def prod {α} [Mul α] [One α] : List α → α := + foldr (· * ·) 1 + +@[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_eq_foldr [Mul α] [One α] {l : List α} : l.prod = l.foldr (· * ·) 1 := rfl + /-! ### range -/ /-- diff --git a/src/Init/Data/List/Int.lean b/src/Init/Data/List/Int.lean index 9fe180cae0..21435f1611 100644 --- a/src/Init/Data/List/Int.lean +++ b/src/Init/Data/List/Int.lean @@ -7,3 +7,4 @@ module prelude public import Init.Data.List.Int.Sum +public import Init.Data.List.Int.Prod diff --git a/src/Init/Data/List/Int/Prod.lean b/src/Init/Data/List/Int/Prod.lean new file mode 100644 index 0000000000..6131e6c83f --- /dev/null +++ b/src/Init/Data/List/Int/Prod.lean @@ -0,0 +1,31 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ +module + +prelude +import Init.Data.List.Lemmas +import Init.Data.Int.Lemmas +public import Init.Data.Int.Pow +public import Init.Data.List.Basic + +public section + +set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. +set_option linter.indexVariables true -- Enforce naming conventions for index variables. + +namespace List + +@[simp] +theorem prod_replicate_int {n : Nat} {a : Int} : (replicate n a).prod = a ^ n := by + induction n <;> simp_all [replicate_succ, Int.pow_succ, Int.mul_comm] + +theorem prod_append_int {l₁ l₂ : List Int} : (l₁ ++ l₂).prod = l₁.prod * l₂.prod := by + simp [prod_append] + +theorem prod_reverse_int (xs : List Int) : xs.reverse.prod = xs.prod := by + simp [prod_reverse] + +end List diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index 6db7245314..52c8db9bd3 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -1878,6 +1878,24 @@ theorem sum_reverse [Zero α] [Add α] [Std.Associative (α := α) (· + ·)] simp_all [sum_append, Std.Commutative.comm (α := α) _ 0, Std.LawfulLeftIdentity.left_id, Std.Commutative.comm] +@[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₁ generalizing l₂ <;> simp_all [Std.Associative.assoc, Std.LawfulLeftIdentity.left_id] + +@[simp, grind =] +theorem prod_singleton [Mul α] [One α] [Std.LawfulRightIdentity (· * ·) (1 : α)] {x : α} : + [x].prod = x := by + simp [List.prod_eq_foldr, Std.LawfulRightIdentity.right_id x] + +@[simp, grind =] +theorem prod_reverse [One α] [Mul α] [Std.Associative (α := α) (· * ·)] + [Std.Commutative (α := α) (· * ·)] + [Std.LawfulLeftIdentity (α := α) (· * ·) 1] (xs : List α) : xs.reverse.prod = xs.prod := by + induction xs <;> + simp_all [prod_append, Std.Commutative.comm (α := α) _ 1, + Std.LawfulLeftIdentity.left_id, Std.Commutative.comm] + /-! ### concat Note that `concat_eq_append` is a `@[simp]` lemma, so `concat` should usually not appear in goals. @@ -2784,6 +2802,11 @@ theorem sum_eq_foldl [Zero α] [Add α] [Std.Associative (α := α) (· + ·)] xs.sum = xs.foldl (init := 0) (· + ·) := by simp [sum_eq_foldr, foldl_eq_apply_foldr, Std.LawfulLeftIdentity.left_id] +theorem prod_eq_foldl [One α] [Mul α] [Std.Associative (α := α) (· * ·)] + [Std.LawfulIdentity (· * ·) (1 : α)] {xs : List α} : + xs.prod = xs.foldl (init := 1) (· * ·) := by + simp [prod_eq_foldr, foldl_eq_apply_foldr, Std.LawfulLeftIdentity.left_id] + -- The argument `f : α₁ → α₂` is intentionally explicit, as it is sometimes not found by unification. theorem foldl_hom (f : α₁ → α₂) {g₁ : α₁ → β → α₁} {g₂ : α₂ → β → α₂} {l : List β} {init : α₁} (H : ∀ x y, g₂ (f x) y = f (g₁ x y)) : l.foldl g₂ (f init) = f (l.foldl g₁ init) := by diff --git a/src/Init/Data/List/Nat.lean b/src/Init/Data/List/Nat.lean index dc0afa1a00..a9cf4abc96 100644 --- a/src/Init/Data/List/Nat.lean +++ b/src/Init/Data/List/Nat.lean @@ -13,6 +13,7 @@ public import Init.Data.List.Nat.Sublist public import Init.Data.List.Nat.TakeDrop public import Init.Data.List.Nat.Count public import Init.Data.List.Nat.Sum +public import Init.Data.List.Nat.Prod public import Init.Data.List.Nat.Erase public import Init.Data.List.Nat.Find public import Init.Data.List.Nat.BEq diff --git a/src/Init/Data/List/Nat/Prod.lean b/src/Init/Data/List/Nat/Prod.lean new file mode 100644 index 0000000000..b59ccd407a --- /dev/null +++ b/src/Init/Data/List/Nat/Prod.lean @@ -0,0 +1,50 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ +module + +prelude +import Init.Data.List.Lemmas +public import Init.BinderPredicates +public import Init.NotationExtra +import Init.Data.Nat.Lemmas + +public section + +set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. +set_option linter.indexVariables true -- Enforce naming conventions for index variables. + +namespace List + +protected theorem prod_eq_zero_iff_exists_zero_nat {l : List Nat} : l.prod = 0 ↔ ∃ x ∈ l, x = 0 := by + induction l with + | nil => simp + | cons x xs ih => + simp [Nat.mul_eq_zero, ih, eq_comm (a := (0 : Nat))] + +protected theorem prod_pos_iff_forall_pos_nat {l : List Nat} : 0 < l.prod ↔ ∀ x ∈ l, 0 < x := by + induction l with + | nil => simp + | cons x xs ih => + simp only [prod_cons, mem_cons, forall_eq_or_imp, ← ih] + constructor + · intro h + exact ⟨Nat.pos_of_mul_pos_right h, Nat.pos_of_mul_pos_left h⟩ + · exact fun ⟨hx, hxs⟩ => Nat.mul_pos hx hxs + +@[simp] +theorem prod_replicate_nat {n : Nat} {a : Nat} : (replicate n a).prod = a ^ n := by + induction n <;> simp_all [replicate_succ, Nat.pow_succ, Nat.mul_comm] + +theorem prod_append_nat {l₁ l₂ : List Nat} : (l₁ ++ l₂).prod = l₁.prod * l₂.prod := by + simp [prod_append] + +theorem prod_reverse_nat (xs : List Nat) : xs.reverse.prod = xs.prod := by + simp [prod_reverse] + +theorem prod_eq_foldl_nat {xs : List Nat} : xs.prod = xs.foldl (init := 1) (· * ·) := by + simp only [foldl_eq_foldr_reverse, Nat.mul_comm, ← prod_eq_foldr, prod_reverse_nat] + +end List diff --git a/src/Init/Data/List/Perm.lean b/src/Init/Data/List/Perm.lean index ceeef7d418..e8d49bb38e 100644 --- a/src/Init/Data/List/Perm.lean +++ b/src/Init/Data/List/Perm.lean @@ -606,6 +606,13 @@ theorem sum_nat {l₁ l₂ : List Nat} (h : l₁ ~ l₂) : l₁.sum = l₂.sum : | swap => simpa [List.sum_cons] using Nat.add_left_comm .. | trans _ _ ih₁ ih₂ => simp [ih₁, ih₂] +theorem prod_nat {l₁ l₂ : List Nat} (h : l₁ ~ l₂) : l₁.prod = l₂.prod := by + induction h with + | nil => simp + | cons _ _ ih => simp [ih] + | swap => simpa [List.prod_cons] using Nat.mul_left_comm .. + | trans _ _ ih₁ ih₂ => simp [ih₁, ih₂] + theorem all_eq {l₁ l₂ : List α} {f : α → Bool} (hp : l₁.Perm l₂) : l₁.all f = l₂.all f := by rw [Bool.eq_iff_iff]; simp [hp.mem_iff] @@ -615,6 +622,9 @@ theorem any_eq {l₁ l₂ : List α} {f : α → Bool} (hp : l₁.Perm l₂) : l grind_pattern Perm.sum_nat => l₁ ~ l₂, l₁.sum grind_pattern Perm.sum_nat => l₁ ~ l₂, l₂.sum +grind_pattern Perm.prod_nat => l₁ ~ l₂, l₁.prod +grind_pattern Perm.prod_nat => l₁ ~ l₂, l₂.prod + end Perm end List diff --git a/src/Init/Data/List/ToArray.lean b/src/Init/Data/List/ToArray.lean index 85da212ac4..dfec099a93 100644 --- a/src/Init/Data/List/ToArray.lean +++ b/src/Init/Data/List/ToArray.lean @@ -213,6 +213,9 @@ theorem forM_toArray [Monad m] (l : List α) (f : α → m PUnit) : @[simp, grind =] theorem sum_toArray [Add α] [Zero α] (l : List α) : l.toArray.sum = l.sum := by simp [Array.sum, List.sum] +@[simp, grind =] theorem prod_toArray [Mul α] [One α] (l : List α) : l.toArray.prod = l.prod := by + simp [Array.prod, List.prod] + @[simp, grind =] theorem append_toArray (l₁ l₂ : List α) : l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray := by apply ext' diff --git a/src/Init/Data/Vector/Basic.lean b/src/Init/Data/Vector/Basic.lean index 4ebd7925b9..ab5914c8b4 100644 --- a/src/Init/Data/Vector/Basic.lean +++ b/src/Init/Data/Vector/Basic.lean @@ -506,6 +506,16 @@ Examples: @[inline, expose] def sum [Add α] [Zero α] (xs : Vector α n) : α := xs.toArray.sum +/-- +Computes the product of the elements of a vector. + +Examples: + * `#v[a, b, c].prod = a * (b * (c * 1))` + * `#v[1, 2, 5].prod = 10` +-/ +@[inline, expose] def prod [Mul α] [One α] (xs : Vector α n) : α := + xs.toArray.prod + /-- Pad a vector on the left with a given element. diff --git a/src/Init/Data/Vector/Int.lean b/src/Init/Data/Vector/Int.lean index f1b4315b40..d711f332e2 100644 --- a/src/Init/Data/Vector/Int.lean +++ b/src/Init/Data/Vector/Int.lean @@ -30,4 +30,16 @@ theorem sum_reverse_int (xs : Vector Int n) : xs.reverse.sum = xs.sum := by theorem sum_eq_foldl_int {xs : Vector Int n} : xs.sum = xs.foldl (b := 0) (· + ·) := by simp only [foldl_eq_foldr_reverse, Int.add_comm, ← sum_eq_foldr, sum_reverse_int] +@[simp] theorem prod_replicate_int {n : Nat} {a : Int} : (replicate n a).prod = a ^ n := by + simp [← prod_toArray, Array.prod_replicate_int] + +theorem prod_append_int {as₁ as₂ : Vector Int n} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by + simp [← prod_toArray] + +theorem prod_reverse_int (xs : Vector Int n) : xs.reverse.prod = xs.prod := by + simp [prod_reverse] + +theorem prod_eq_foldl_int {xs : Vector Int n} : xs.prod = xs.foldl (b := 1) (· * ·) := by + simp only [foldl_eq_foldr_reverse, Int.mul_comm, ← prod_eq_foldr, prod_reverse_int] + end Vector diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean index 5b9b1841f6..a7aa6b58d1 100644 --- a/src/Init/Data/Vector/Lemmas.lean +++ b/src/Init/Data/Vector/Lemmas.lean @@ -278,6 +278,12 @@ theorem toArray_mk {xs : Array α} (h : xs.size = n) : (Vector.mk xs h).toArray @[simp, grind =] theorem sum_toArray [Add α] [Zero α] {xs : Vector α n} : xs.toArray.sum = xs.sum := rfl +@[simp] theorem prod_mk [Mul α] [One α] {xs : Array α} (h : xs.size = n) : + (Vector.mk xs h).prod = xs.prod := rfl + +@[simp, grind =] theorem prod_toArray [Mul α] [One α] {xs : Vector α n} : + xs.toArray.prod = xs.prod := rfl + @[simp] theorem eq_mk : xs = Vector.mk as h ↔ xs.toArray = as := by cases xs simp @@ -551,6 +557,10 @@ theorem toArray_toList {xs : Vector α n} : xs.toList.toArray = xs.toArray := rf xs.toList.sum = xs.sum := by rw [← toList_toArray, Array.sum_toList, sum_toArray] +@[simp, grind =] theorem prod_toList [Mul α] [One α] {xs : Vector α n} : + xs.toList.prod = xs.prod := by + rw [← toList_toArray, Array.prod_toList, prod_toArray] + @[simp] theorem getElem_toList {xs : Vector α n} {i : Nat} (h : i < xs.toList.length) : xs.toList[i] = xs[i]'(by simpa using h) := by cases xs @@ -3134,3 +3144,39 @@ theorem sum_eq_foldl [Zero α] [Add α] {xs : Vector α n} : xs.sum = xs.foldl (b := 0) (· + ·) := by simp [← sum_toList, List.sum_eq_foldl] + +/-! ### prod -/ + +@[simp, grind =] theorem prod_empty [Mul α] [One α] : (#v[] : Vector α 0).prod = 1 := rfl +theorem prod_eq_foldr [Mul α] [One α] {xs : Vector α n} : + xs.prod = xs.foldr (b := 1) (· * ·) := + rfl + +@[simp, grind =] +theorem prod_append [One α] [Mul α] [Std.Associative (α := α) (· * ·)] + [Std.LeftIdentity (α := α) (· * ·) 1] [Std.LawfulLeftIdentity (α := α) (· * ·) 1] + {as₁ as₂ : Vector α n} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by + simp [← prod_toList, List.prod_append] + +@[simp, grind =] +theorem prod_singleton [Mul α] [One α] [Std.LawfulRightIdentity (· * ·) (1 : α)] {x : α} : + #v[x].prod = x := by + simp [← prod_toList, Std.LawfulRightIdentity.right_id x] + +@[simp, grind =] +theorem prod_push [Mul α] [One α] [Std.Associative (α := α) (· * ·)] + [Std.LawfulIdentity (· * ·) (1 : α)] {xs : Vector α n} {x : α} : + (xs.push x).prod = xs.prod * x := by + simp [← prod_toArray] + +@[simp, grind =] +theorem prod_reverse [One α] [Mul α] [Std.Associative (α := α) (· * ·)] + [Std.Commutative (α := α) (· * ·)] + [Std.LawfulLeftIdentity (α := α) (· * ·) 1] (xs : Vector α n) : xs.reverse.prod = xs.prod := by + simp [← prod_toList, List.prod_reverse] + +theorem prod_eq_foldl [One α] [Mul α] + [Std.Associative (α := α) (· * ·)] [Std.LawfulIdentity (· * ·) (1 : α)] + {xs : Vector α n} : + xs.prod = xs.foldl (b := 1) (· * ·) := by + simp [← prod_toList, List.prod_eq_foldl] diff --git a/src/Init/Data/Vector/Nat.lean b/src/Init/Data/Vector/Nat.lean index 4824a37fd3..a30a53bc6a 100644 --- a/src/Init/Data/Vector/Nat.lean +++ b/src/Init/Data/Vector/Nat.lean @@ -37,4 +37,23 @@ theorem sum_reverse_nat (xs : Vector Nat n) : xs.reverse.sum = xs.sum := by theorem sum_eq_foldl_nat {xs : Vector Nat n} : xs.sum = xs.foldl (b := 0) (· + ·) := by simp only [foldl_eq_foldr_reverse, Nat.add_comm, ← sum_eq_foldr, sum_reverse_nat] +protected theorem prod_pos_iff_forall_pos_nat {xs : Vector Nat n} : 0 < xs.prod ↔ ∀ x ∈ xs, 0 < x := by + simp [← prod_toArray, Array.prod_pos_iff_forall_pos_nat] + +protected theorem prod_eq_zero_iff_exists_zero_nat {xs : Vector Nat n} : + xs.prod = 0 ↔ ∃ x ∈ xs, x = 0 := by + simp [← prod_toArray, Array.prod_eq_zero_iff_exists_zero_nat] + +@[simp] theorem prod_replicate_nat {n : Nat} {a : Nat} : (replicate n a).prod = a ^ n := by + simp [← prod_toArray, Array.prod_replicate_nat] + +theorem prod_append_nat {as₁ as₂ : Vector Nat n} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by + simp [← prod_toArray] + +theorem prod_reverse_nat (xs : Vector Nat n) : xs.reverse.prod = xs.prod := by + simp [prod_reverse] + +theorem prod_eq_foldl_nat {xs : Vector Nat n} : xs.prod = xs.foldl (b := 1) (· * ·) := by + simp only [foldl_eq_foldr_reverse, Nat.mul_comm, ← prod_eq_foldr, prod_reverse_nat] + end Vector