From 63695f81ed5572323a3c5ed3e29107ededf297e6 Mon Sep 17 00:00:00 2001 From: Dimitris Date: Sun, 19 Apr 2026 11:24:44 +0300 Subject: [PATCH 1/9] eval2_eq_eval2Horner lemma, no proof yet --- CompPoly/Univariate/Raw/Ops.lean | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/CompPoly/Univariate/Raw/Ops.lean b/CompPoly/Univariate/Raw/Ops.lean index 1299f71..ada5846 100644 --- a/CompPoly/Univariate/Raw/Ops.lean +++ b/CompPoly/Univariate/Raw/Ops.lean @@ -32,6 +32,21 @@ variable {S : Type*} def eval₂ [Semiring R] [Semiring S] (f : R →+* S) (x : S) (p : CPolynomial.Raw R) : S := p.zipIdx.foldl (fun acc ⟨a, i⟩ => acc + f a * x ^ i) 0 +def eval₂Horner [Semiring R] [Semiring S] (f : R →+* S) (x : S) (p : CPolynomial.Raw R) : S := + p.foldr (fun a acc => acc * x + f a) 0 + +theorem eval₂_eq_eval₂Horner [Semiring R] [Semiring S] (f : R →+* S) (x : S) (p : CPolynomial.Raw R) : + eval₂ f x p = eval₂Horner f x p := by + unfold eval₂ eval₂Horner + rw [← Array.foldl_toList, ← Array.foldr_toList, Array.toList_zipIdx] + induction p.toList with + | nil => simp + | cons head tail tail_ih => + + + +private lemma + /-- Evaluates a `CPolynomial.Raw` at a given value -/ @[inline, specialize] def eval [Semiring R] (x : R) (p : CPolynomial.Raw R) : R := From 11db6b53ea43dcc4726df5a417da63b251081053 Mon Sep 17 00:00:00 2001 From: Dimitris Date: Sun, 19 Apr 2026 18:42:37 +0300 Subject: [PATCH 2/9] helper lemma and horner correctness proof added --- CompPoly/Univariate/Raw/Ops.lean | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/CompPoly/Univariate/Raw/Ops.lean b/CompPoly/Univariate/Raw/Ops.lean index ada5846..e8077a7 100644 --- a/CompPoly/Univariate/Raw/Ops.lean +++ b/CompPoly/Univariate/Raw/Ops.lean @@ -35,6 +35,15 @@ def eval₂ [Semiring R] [Semiring S] (f : R →+* S) (x : S) (p : CPolynomial.R def eval₂Horner [Semiring R] [Semiring S] (f : R →+* S) (x : S) (p : CPolynomial.Raw R) : S := p.foldr (fun a acc => acc * x + f a) 0 +lemma foldl_zipIdx_eq_foldr_pow_k [Semiring R] [Semiring S] (f : R →+* S) (x : S) (init : S) (k : Nat) (l : List R) : + List.foldl (fun acc a => acc + (f a.1) * x ^ a.2) init (l.zipIdx k) = List.foldr (fun a acc => acc * x + f a) 0 l * x ^ k + init := by + induction l generalizing init k with + | nil => simp + | cons head tail tail_ih => + simp only [List.foldr_cons, List.zipIdx_cons, List.foldl_cons] + rw [tail_ih] + rw [add_mul, mul_assoc, ← pow_succ', add_comm init, add_assoc] + theorem eval₂_eq_eval₂Horner [Semiring R] [Semiring S] (f : R →+* S) (x : S) (p : CPolynomial.Raw R) : eval₂ f x p = eval₂Horner f x p := by unfold eval₂ eval₂Horner @@ -42,10 +51,9 @@ theorem eval₂_eq_eval₂Horner [Semiring R] [Semiring S] (f : R →+* S) (x : induction p.toList with | nil => simp | cons head tail tail_ih => - - - -private lemma + simp + rw [foldl_zipIdx_eq_foldr_pow_k] + simp /-- Evaluates a `CPolynomial.Raw` at a given value -/ @[inline, specialize] From 2312d6aa7e45abc94fefd093eb263f06f088eebc Mon Sep 17 00:00:00 2001 From: Dimitris Date: Sun, 19 Apr 2026 18:48:39 +0300 Subject: [PATCH 3/9] proof simplification --- CompPoly/Univariate/Raw/Ops.lean | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/CompPoly/Univariate/Raw/Ops.lean b/CompPoly/Univariate/Raw/Ops.lean index e8077a7..3068e03 100644 --- a/CompPoly/Univariate/Raw/Ops.lean +++ b/CompPoly/Univariate/Raw/Ops.lean @@ -48,12 +48,8 @@ theorem eval₂_eq_eval₂Horner [Semiring R] [Semiring S] (f : R →+* S) (x : eval₂ f x p = eval₂Horner f x p := by unfold eval₂ eval₂Horner rw [← Array.foldl_toList, ← Array.foldr_toList, Array.toList_zipIdx] - induction p.toList with - | nil => simp - | cons head tail tail_ih => - simp - rw [foldl_zipIdx_eq_foldr_pow_k] - simp + have := foldl_zipIdx_eq_foldr_pow_k f x 0 0 p.toList + simpa using this /-- Evaluates a `CPolynomial.Raw` at a given value -/ @[inline, specialize] From 37750a7dba91ab12fd56c576bc322f668e09a665 Mon Sep 17 00:00:00 2001 From: Dimitris Date: Sun, 19 Apr 2026 18:49:27 +0300 Subject: [PATCH 4/9] eval uses Horner's method --- CompPoly/Univariate/Raw/Ops.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CompPoly/Univariate/Raw/Ops.lean b/CompPoly/Univariate/Raw/Ops.lean index 3068e03..f10afb7 100644 --- a/CompPoly/Univariate/Raw/Ops.lean +++ b/CompPoly/Univariate/Raw/Ops.lean @@ -54,7 +54,7 @@ theorem eval₂_eq_eval₂Horner [Semiring R] [Semiring S] (f : R →+* S) (x : /-- Evaluates a `CPolynomial.Raw` at a given value -/ @[inline, specialize] def eval [Semiring R] (x : R) (p : CPolynomial.Raw R) : R := - p.eval₂ (RingHom.id R) x + p.eval₂Horner (RingHom.id R) x /-- Raw addition: pointwise sum of coefficient arrays (padded to equal length). From 88d727d8466bd21b265874c65a456e1e39debf39 Mon Sep 17 00:00:00 2001 From: Dimitris Date: Sun, 19 Apr 2026 19:30:14 +0300 Subject: [PATCH 5/9] fixed docstrings, eval uses eval\2 as reference --- CompPoly/Univariate/Raw/Ops.lean | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/CompPoly/Univariate/Raw/Ops.lean b/CompPoly/Univariate/Raw/Ops.lean index f10afb7..a50c700 100644 --- a/CompPoly/Univariate/Raw/Ops.lean +++ b/CompPoly/Univariate/Raw/Ops.lean @@ -26,17 +26,18 @@ variable {S : Type*} /-- Evaluates a `CPolynomial.Raw` at `x : S` using a ring homomorphism `f : R →+* S`. - Computes `f(a₀) + f(a₁) * x + f(a₂) * x² + ...` where `aᵢ` are the coefficients. - - TODO: define an efficient version of this with caching -/ + Computes `f(a₀) + f(a₁) * x + f(a₂) * x² + ...` where `aᵢ` are the coefficients. -/ def eval₂ [Semiring R] [Semiring S] (f : R →+* S) (x : S) (p : CPolynomial.Raw R) : S := p.zipIdx.foldl (fun acc ⟨a, i⟩ => acc + f a * x ^ i) 0 +@[inline, specialize] def eval₂Horner [Semiring R] [Semiring S] (f : R →+* S) (x : S) (p : CPolynomial.Raw R) : S := p.foldr (fun a acc => acc * x + f a) 0 -lemma foldl_zipIdx_eq_foldr_pow_k [Semiring R] [Semiring S] (f : R →+* S) (x : S) (init : S) (k : Nat) (l : List R) : - List.foldl (fun acc a => acc + (f a.1) * x ^ a.2) init (l.zipIdx k) = List.foldr (fun a acc => acc * x + f a) 0 l * x ^ k + init := by +private lemma foldl_zipIdx_eq_foldr_pow_k [Semiring R] [Semiring S] + (f : R →+* S) (x : S) (init : S) (k : Nat) (l : List R) : + List.foldl (fun acc a => acc + (f a.1) * x ^ a.2) init (l.zipIdx k) = + List.foldr (fun a acc => acc * x + f a) 0 l * x ^ k + init := by induction l generalizing init k with | nil => simp | cons head tail tail_ih => @@ -44,8 +45,9 @@ lemma foldl_zipIdx_eq_foldr_pow_k [Semiring R] [Semiring S] (f : R →+* S) (x : rw [tail_ih] rw [add_mul, mul_assoc, ← pow_succ', add_comm init, add_assoc] -theorem eval₂_eq_eval₂Horner [Semiring R] [Semiring S] (f : R →+* S) (x : S) (p : CPolynomial.Raw R) : - eval₂ f x p = eval₂Horner f x p := by +theorem eval₂_eq_eval₂Horner [Semiring R] [Semiring S] + (f : R →+* S) (x : S) (p : CPolynomial.Raw R) : + eval₂ f x p = eval₂Horner f x p := by unfold eval₂ eval₂Horner rw [← Array.foldl_toList, ← Array.foldr_toList, Array.toList_zipIdx] have := foldl_zipIdx_eq_foldr_pow_k f x 0 0 p.toList @@ -54,7 +56,7 @@ theorem eval₂_eq_eval₂Horner [Semiring R] [Semiring S] (f : R →+* S) (x : /-- Evaluates a `CPolynomial.Raw` at a given value -/ @[inline, specialize] def eval [Semiring R] (x : R) (p : CPolynomial.Raw R) : R := - p.eval₂Horner (RingHom.id R) x + p.eval₂ (RingHom.id R) x /-- Raw addition: pointwise sum of coefficient arrays (padded to equal length). From 898f3617b898467b96b096dce35833c3fbe26e11 Mon Sep 17 00:00:00 2001 From: Dimitris Date: Sun, 19 Apr 2026 19:58:24 +0300 Subject: [PATCH 6/9] added myself to the author list --- CompPoly/Univariate/Raw/Ops.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CompPoly/Univariate/Raw/Ops.lean b/CompPoly/Univariate/Raw/Ops.lean index a50c700..1bcb84b 100644 --- a/CompPoly/Univariate/Raw/Ops.lean +++ b/CompPoly/Univariate/Raw/Ops.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2025 CompPoly. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Quang Dao, Gregor Mitscha-Baude, Derek Sorensen, Desmond Coles, Natalie Klaus +Authors: Quang Dao, Gregor Mitscha-Baude, Derek Sorensen, Desmond Coles, Natalie Klaus, Dimitris Mitsios -/ import CompPoly.Univariate.Raw.Core From 6950b7610e21a85913405bb97c91e321b03c6d1e Mon Sep 17 00:00:00 2001 From: Dimitris Date: Sun, 19 Apr 2026 20:17:24 +0300 Subject: [PATCH 7/9] fix: wrap long authors line to stay under 100 chars Co-Authored-By: Claude Opus 4.6 --- CompPoly/Univariate/Raw/Ops.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/CompPoly/Univariate/Raw/Ops.lean b/CompPoly/Univariate/Raw/Ops.lean index 1bcb84b..6c2d866 100644 --- a/CompPoly/Univariate/Raw/Ops.lean +++ b/CompPoly/Univariate/Raw/Ops.lean @@ -1,7 +1,8 @@ /- Copyright (c) 2025 CompPoly. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Quang Dao, Gregor Mitscha-Baude, Derek Sorensen, Desmond Coles, Natalie Klaus, Dimitris Mitsios +Authors: Quang Dao, Gregor Mitscha-Baude, Derek Sorensen, Desmond Coles, + Natalie Klaus, Dimitris Mitsios -/ import CompPoly.Univariate.Raw.Core From a5566042156f76cc714b0afc73e393b2b81bee55 Mon Sep 17 00:00:00 2001 From: Dimitris Date: Sun, 19 Apr 2026 20:19:22 +0300 Subject: [PATCH 8/9] =?UTF-8?q?docs:=20add=20docstrings=20for=20eval?= =?UTF-8?q?=E2=82=82Horner=20and=20eval=E2=82=82=5Feq=5Feval=E2=82=82Horne?= =?UTF-8?q?r?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 4.6 --- CompPoly/Univariate/Raw/Ops.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/CompPoly/Univariate/Raw/Ops.lean b/CompPoly/Univariate/Raw/Ops.lean index 6c2d866..24efa62 100644 --- a/CompPoly/Univariate/Raw/Ops.lean +++ b/CompPoly/Univariate/Raw/Ops.lean @@ -31,6 +31,9 @@ variable {S : Type*} def eval₂ [Semiring R] [Semiring S] (f : R →+* S) (x : S) (p : CPolynomial.Raw R) : S := p.zipIdx.foldl (fun acc ⟨a, i⟩ => acc + f a * x ^ i) 0 +/-- Evaluates a `CPolynomial.Raw` at `x : S` using Horner's method. + + Computes `f(aₙ) + x * (f(aₙ₋₁) + x * (... + x * f(a₀)))` via a right fold. -/ @[inline, specialize] def eval₂Horner [Semiring R] [Semiring S] (f : R →+* S) (x : S) (p : CPolynomial.Raw R) : S := p.foldr (fun a acc => acc * x + f a) 0 @@ -46,6 +49,7 @@ private lemma foldl_zipIdx_eq_foldr_pow_k [Semiring R] [Semiring S] rw [tail_ih] rw [add_mul, mul_assoc, ← pow_succ', add_comm init, add_assoc] +/-- Horner evaluation agrees with the sum-of-powers evaluation. -/ theorem eval₂_eq_eval₂Horner [Semiring R] [Semiring S] (f : R →+* S) (x : S) (p : CPolynomial.Raw R) : eval₂ f x p = eval₂Horner f x p := by From db10879fded05752647ba656baa3a23c177279e9 Mon Sep 17 00:00:00 2001 From: Dimitris Date: Wed, 29 Apr 2026 17:25:14 +0300 Subject: [PATCH 9/9] fix: moved proofs from Ops.lean to Proofs.lean --- CompPoly/Univariate/Raw/Ops.lean | 20 ------------------- CompPoly/Univariate/Raw/Proofs.lean | 31 ++++++++++++++++++++++++++++- 2 files changed, 30 insertions(+), 21 deletions(-) diff --git a/CompPoly/Univariate/Raw/Ops.lean b/CompPoly/Univariate/Raw/Ops.lean index 24efa62..ce40096 100644 --- a/CompPoly/Univariate/Raw/Ops.lean +++ b/CompPoly/Univariate/Raw/Ops.lean @@ -38,26 +38,6 @@ def eval₂ [Semiring R] [Semiring S] (f : R →+* S) (x : S) (p : CPolynomial.R def eval₂Horner [Semiring R] [Semiring S] (f : R →+* S) (x : S) (p : CPolynomial.Raw R) : S := p.foldr (fun a acc => acc * x + f a) 0 -private lemma foldl_zipIdx_eq_foldr_pow_k [Semiring R] [Semiring S] - (f : R →+* S) (x : S) (init : S) (k : Nat) (l : List R) : - List.foldl (fun acc a => acc + (f a.1) * x ^ a.2) init (l.zipIdx k) = - List.foldr (fun a acc => acc * x + f a) 0 l * x ^ k + init := by - induction l generalizing init k with - | nil => simp - | cons head tail tail_ih => - simp only [List.foldr_cons, List.zipIdx_cons, List.foldl_cons] - rw [tail_ih] - rw [add_mul, mul_assoc, ← pow_succ', add_comm init, add_assoc] - -/-- Horner evaluation agrees with the sum-of-powers evaluation. -/ -theorem eval₂_eq_eval₂Horner [Semiring R] [Semiring S] - (f : R →+* S) (x : S) (p : CPolynomial.Raw R) : - eval₂ f x p = eval₂Horner f x p := by - unfold eval₂ eval₂Horner - rw [← Array.foldl_toList, ← Array.foldr_toList, Array.toList_zipIdx] - have := foldl_zipIdx_eq_foldr_pow_k f x 0 0 p.toList - simpa using this - /-- Evaluates a `CPolynomial.Raw` at a given value -/ @[inline, specialize] def eval [Semiring R] (x : R) (p : CPolynomial.Raw R) : R := diff --git a/CompPoly/Univariate/Raw/Proofs.lean b/CompPoly/Univariate/Raw/Proofs.lean index 7e8a8ed..a70d868 100644 --- a/CompPoly/Univariate/Raw/Proofs.lean +++ b/CompPoly/Univariate/Raw/Proofs.lean @@ -1,7 +1,8 @@ /- Copyright (c) 2025 CompPoly. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Quang Dao, Gregor Mitscha-Baude, Derek Sorensen, Desmond Coles, Natalie Klaus +Authors: Quang Dao, Gregor Mitscha-Baude, Derek Sorensen, Desmond Coles, + Natalie Klaus, Dimitris Mitsios -/ import CompPoly.Univariate.Raw.Ops @@ -905,6 +906,34 @@ protected theorem mul_assoc [LawfulBEq R] (p q r : CPolynomial.Raw R) : end MulTheorems +section EvalTheorems + +variable [Semiring S] + +omit [BEq R] in +private lemma foldl_zipIdx_eq_foldr_pow_k + (f : R →+* S) (x : S) (init : S) (k : Nat) (l : List R) : + List.foldl (fun acc a => acc + (f a.1) * x ^ a.2) init (l.zipIdx k) = + List.foldr (fun a acc => acc * x + f a) 0 l * x ^ k + init := by + induction l generalizing init k with + | nil => simp + | cons head tail tail_ih => + simp only [List.foldr_cons, List.zipIdx_cons, List.foldl_cons] + rw [tail_ih] + rw [add_mul, mul_assoc, ← pow_succ', _root_.add_comm init, _root_.add_assoc] + +omit [BEq R] in +/-- Horner evaluation agrees with the sum-of-powers evaluation. -/ +theorem eval₂_eq_eval₂Horner + (f : R →+* S) (x : S) (p : CPolynomial.Raw R) : + eval₂ f x p = eval₂Horner f x p := by + unfold eval₂ eval₂Horner + rw [← Array.foldl_toList, ← Array.foldr_toList, Array.toList_zipIdx] + have := foldl_zipIdx_eq_foldr_pow_k f x 0 0 p.toList + simpa using this + +end EvalTheorems + end Semiring section CommutativeSemiring