Skip to content

Fix divByMonicAux initial counter off-by-one #124

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
dhsorens merged 5 commits into from
Feb 27, 2026
Merged

Fix divByMonicAux initial counter off-by-one #124

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
5cebb11
fix(raw): correct divByMonic loop counter
eliasjudin Feb 26, 2026
4bdc87d
fix(raw): guard monic division when size drops below divisor
eliasjudin Feb 27, 2026
f440f7f
refactor(raw): use size-fuel recursion for monic division
eliasjudin Feb 27, 2026
f913dc1
ci(lint): bump Raw.lean line-count exception watermark
eliasjudin Feb 27, 2026
d79ce47
docs(raw): shorten divModByMonicAux docstring per review
eliasjudin Feb 27, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
43 changes: 34 additions & 9 deletions CompPoly/Univariate/Raw.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1588,19 +1588,22 @@ instance : IntCast (CPolynomial.Raw R) := ⟨fun n => C (n : R)⟩
/-- Division with remainder by a monic polynomial using polynomial long division. -/
def divModByMonicAux [Field R] (p : CPolynomial.Raw R) (q : CPolynomial.Raw R) :
CPolynomial.Raw R × CPolynomial.Raw R :=
go (p.size - q.size) p q
go p.size p q
where
go : Nat → CPolynomial.Raw R → CPolynomial.Raw R → CPolynomial.Raw R × CPolynomial.Raw R
| 0, p, _ => ⟨0, p⟩
| n+1, p, q =>
let k := p.size - q.size -- k should equal n, this is technically unneeded
let q' := C p.leadingCoeff * (q * X.pow k)
let p' := (p - q').trim
let (e, f) := go n p' q
-- p' = q * e + f
-- Thus p = p' + q' = q * e + f + p.leadingCoeff * q * X^n
-- = q * (e + p.leadingCoeff * X^n) + f
⟨e + C p.leadingCoeff * X^k, f⟩
if p.size < q.size then
⟨0, p⟩
else
let k := p.size - q.size
let q' := C p.leadingCoeff * (q * X.pow k)
let p' := (p - q').trim
let (e, f) := go n p' q
-- p' = q * e + f
-- Thus p = p' + q' = q * e + f + p.leadingCoeff * q * X^k
-- = q * (e + p.leadingCoeff * X^k) + f
⟨e + C p.leadingCoeff * X^k, f⟩

/-- Division of `p : CPolynomial.Raw R` by a monic `q : CPolynomial.Raw R`. -/
def divByMonic [Field R] (p : CPolynomial.Raw R) (q : CPolynomial.Raw R) :
Expand All @@ -1612,6 +1615,28 @@ def modByMonic [Field R] (p : CPolynomial.Raw R) (q : CPolynomial.Raw R) :
CPolynomial.Raw R :=
(divModByMonicAux p q).2

/-- Regression test for issue #115: `(X^2 - 1) / (X + 1) = X - 1` with zero remainder. -/
example :
divByMonic ((X : CPolynomial.Raw ℚ) ^ 2 - C 1) ((X : CPolynomial.Raw ℚ) + C 1)
= #[-(1 : ℚ), 1] := by
native_decide

Comment on lines +1618 to +1623
Copy link
Copy Markdown
Collaborator

@dhsorens dhsorens Feb 27, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

good call to include tests like this, and probably something we want more of. in the long run we won't want these here but let's keep them here right now

example :
modByMonic ((X : CPolynomial.Raw ℚ) ^ 2 - C 1) ((X : CPolynomial.Raw ℚ) + C 1)
= #[] := by
native_decide

/-- Regression test for review-thread case: `X^3 = (X^2 + 1) * X + (-X)`. -/
example :
divByMonic ((X : CPolynomial.Raw ℚ) ^ 3) ((X : CPolynomial.Raw ℚ) ^ 2 + C 1)
= #[(0 : ℚ), 1] := by
native_decide

example :
modByMonic ((X : CPolynomial.Raw ℚ) ^ 3) ((X : CPolynomial.Raw ℚ) ^ 2 + C 1)
= #[(0 : ℚ), -(1 : ℚ)] := by
native_decide

/-- Division of two `CPolynomial.Raw`s. -/
def div [Field R] (p q : CPolynomial.Raw R) : CPolynomial.Raw R :=
(C (q.leadingCoeff)⁻¹ • p).divByMonic (C (q.leadingCoeff)⁻¹ * q)
Expand Down
2 changes: 1 addition & 1 deletion scripts/style-exceptions.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ lakefile.lean : line 1 : ERR_MOD : Module docstring missing, or too late : ERR_M
lean-toolchain : line 1 : ERR_COP : Malformed or missing copyright header : ERR_COP
lean-toolchain : line 1 : ERR_MOD : Module docstring missing, or too late : ERR_MOD
lakefile.lean : line 1 : ERR_TAC2 : In the past, importing 'Lake' has led to dramatic slow-downs of the linter (see e.g. mathlib4#13779). Please consider carefully if this import is useful and make sure to benchmark it. If this is fine, feel free to allow this linter. : ERR_TAC2
CompPoly/Univariate/Raw.lean : line 1 : ERR_NUM_LIN : 1700 file contains 1691 lines, try to split it up : ERR_NUM_LIN
CompPoly/Univariate/Raw.lean : line 1 : ERR_NUM_LIN : 1900 file contains 1704 lines, try to split it up : ERR_NUM_LIN
CompPoly/Fields/Binary/Tower/Impl.lean : line 1 : ERR_NUM_LIN : 4100 file contains 3894 lines, try to split it up : ERR_NUM_LIN
CompPoly/Fields/Binary/Tower/Prelude.lean : line 1 : ERR_NUM_LIN : 1900 file contains 1756 lines, try to split it up : ERR_NUM_LIN
CompPoly/Fields/Binary/AdditiveNTT/AdditiveNTT.lean : line 1 : ERR_NUM_LIN : 3000 file contains 2826 lines, try to split it up : ERR_NUM_LIN
Expand Down