Add computable versions of div and mod

[tomaz1502]

This PR replaces the old version of CPolynomial.div and CPolynomial.mod by one that is closer to the one defined in mathlib. It also proves their termination and that they are equivalent to Polynomial.div and Polynomial.mod with respect to CPolynomial.toPoly.

Note that it was necessary to prove some toPoly equivalence lemmas about CPolynomial.Raw. Maybe these could be incorporated in the file CompPoly/Univariate/ToPoly.lean.

Solves #115.

Co-authored-by: Aristotle (Harmonic) aristotle-harmonic@harmonic.fun

[github-actions]

🤖 Gemini PR Summary

Mathematical Formalization

• Implements computable univariate polynomial division (div, mod) and specialized versions for monic polynomials (divByMonic, modByMonic).
• Proves termination of the division algorithm using well-founded recursion based on polynomial size.
• Establishes formal correctness by proving equivalence between CPolynomial operations and Mathlib's Polynomial.div and Polynomial.mod via the CPolynomial.toPoly mapping.
• Introduces lemmas for CPolynomial.Raw connecting internal representation attributes, such as leadingCoeff and natDegree, to their corresponding values in Polynomial.

Structural and API Changes

• Replaces legacy CPolynomial.div and CPolynomial.mod implementations with versions structurally aligned with Mathlib's definitions.
• Updates Div and Mod typeclass instances for CPolynomial to use the new computable definitions.
• Migrates division logic to a dedicated module: CompPoly/Univariate/Division.lean.
• Adds technical equivalence lemmas for CPolynomial.Raw, with a note regarding potential future migration to CompPoly/Univariate/ToPoly.lean.

---

Statistics

Metric	Count
📝 Files Changed	3
✅ Lines Added	497
❌ Lines Removed	47

---

Lean Declarations

✏️ **Removed:** 5 declaration(s)

• def mod [Field R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) : CPolynomial R in CompPoly/Univariate/Basic.lean
• instance [Field R] [BEq R] [LawfulBEq R] : Mod (CPolynomial R) in CompPoly/Univariate/Basic.lean
• def div [Field R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) : CPolynomial R in CompPoly/Univariate/Basic.lean
• def divByMonic [Field R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) : CPolynomial R in CompPoly/Univariate/Basic.lean
• def modByMonic [Field R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) : CPolynomial R in CompPoly/Univariate/Basic.lean

✏️ **Added:** 34 declaration(s)

• lemma leadingCoeff_toPoly (p : CPolynomial.Raw R) : in CompPoly/Univariate/Raw/Division.lean
• lemma toPoly_sub (p q : CPolynomial.Raw R) : in CompPoly/Univariate/Raw/Division.lean
• lemma modByMonic_unfold_step (p q : CPolynomial.Raw R) (hq : q.toPoly.Monic) in CompPoly/Univariate/Raw/Division.lean
• lemma toPoly_mul (p q : CPolynomial.Raw R) : in CompPoly/Univariate/Raw/Division.lean
• theorem div_toPoly (p q : CPolynomial.Raw R) : in CompPoly/Univariate/Raw/Division.lean
• def div (p q : CPolynomial R) : CPolynomial R in CompPoly/Univariate/Division.lean
• def mod (p q : CPolynomial R) : CPolynomial R in CompPoly/Univariate/Division.lean
• lemma toPoly_pow (p : CPolynomial.Raw R) (n : ℕ) : in CompPoly/Univariate/Raw/Division.lean
• theorem modByMonic_toPoly (p q : CPolynomial.Raw R) (hq : q.monic = true) : in CompPoly/Univariate/Raw/Division.lean
• lemma trim_size_eq_natDegree_succ (p : CPolynomial.Raw R) (hp : p.toPoly ≠ 0) : in CompPoly/Univariate/Raw/Division.lean
• lemma divByMonic_unfold_step (p q : CPolynomial.Raw R) (hq : q.toPoly.Monic) in CompPoly/Univariate/Raw/Division.lean
• lemma natDegree_eq_toPoly_natDegree (p : CPolynomial.Raw R) (hp : p.toPoly ≠ 0) : in CompPoly/Univariate/Raw/Division.lean
• def divByMonic (p q : CPolynomial R) : CPolynomial R in CompPoly/Univariate/Division.lean
• lemma divModByMonic_of_not_cond (p q : CPolynomial.Raw R) (hq : q.toPoly.Monic) in CompPoly/Univariate/Raw/Division.lean
• theorem mod_toPoly (p q : CPolynomial R) (hq : q ≠ 0) : in CompPoly/Univariate/Division.lean
• lemma divModByMonicAux_go_unfold_2 (p q : CPolynomial.Raw R) (hq : q.monic = true) : in CompPoly/Univariate/Raw/Division.lean
• lemma degree_le_of_trim_size_le (p q : CPolynomial.Raw R) in CompPoly/Univariate/Raw/Division.lean
• lemma divModByMonicAux_go_toPoly_1 (p q : CPolynomial.Raw R) in CompPoly/Univariate/Raw/Division.lean
• lemma divModByMonicAux_go_unfold_1 (p q : CPolynomial.Raw R) (hq : q.monic = true) : in CompPoly/Univariate/Raw/Division.lean
• lemma div_step_degree_lt (p q : CPolynomial.Raw R) in CompPoly/Univariate/Raw/Division.lean
• theorem div_toPoly (p q : CPolynomial R) : in CompPoly/Univariate/Division.lean
• lemma size_cond_iff_degree_cond (p q : CPolynomial.Raw R) (hq : q.toPoly.Monic) : in CompPoly/Univariate/Raw/Division.lean
• lemma divByMonic_wf_termination (p q : CPolynomial.Raw R) in CompPoly/Univariate/Raw/Division.lean
• lemma trim_size_zero_iff_toPoly_zero (p : CPolynomial.Raw R) : in CompPoly/Univariate/Raw/Division.lean
• theorem divByMonic_toPoly (p q : CPolynomial.Raw R) (hq : q.monic = true) : in CompPoly/Univariate/Raw/Division.lean
• lemma divModByMonicAux_go_toPoly_2 (p q : CPolynomial.Raw R) (hq : q.monic = true) : in CompPoly/Univariate/Raw/Division.lean
• lemma trim_size_pos_iff_toPoly_ne_zero (p : CPolynomial.Raw R) : in CompPoly/Univariate/Raw/Division.lean
• lemma toPoly_neg (p : CPolynomial.Raw R) : in CompPoly/Univariate/Raw/Division.lean
• def modByMonic (p q : CPolynomial R) : CPolynomial R in CompPoly/Univariate/Division.lean
• lemma z_toPoly_eq (p q : CPolynomial.Raw R) (hp : p.toPoly ≠ 0) : in CompPoly/Univariate/Raw/Division.lean
• lemma monic_iff_toPoly_monic (q : CPolynomial.Raw R) : in CompPoly/Univariate/Raw/Division.lean
• lemma Polynomial.C_mul_divByMonic_eq (a : R) (p q : Polynomial R) (hq : q.Monic) : in CompPoly/Univariate/Raw/Division.lean
• theorem mod_toPoly (p q : CPolynomial.Raw R) (hq : q.toPoly ≠ 0) : in CompPoly/Univariate/Raw/Division.lean
• lemma trim_size_lt_of_degree_lt (r p : CPolynomial.Raw R) in CompPoly/Univariate/Raw/Division.lean

✏️ **Affected:** 3 declaration(s) (line number changed)

• def divByMonic (p q : CPolynomial.Raw R) : CPolynomial.Raw R in CompPoly/Univariate/Raw/Division.lean moved from L42 to L223
• def modByMonic (p q : CPolynomial.Raw R) : CPolynomial.Raw R in CompPoly/Univariate/Raw/Division.lean moved from L47 to L227
• def divModByMonicAux (p q : CPolynomial.Raw R) : CPolynomial.Raw R × CPolynomial.Raw R in CompPoly/Univariate/Raw/Division.lean moved from L25 to L207

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

🎨 **Style Guide Adherence**

There are 29 violations of the style guide in this diff. They are grouped by rule below:

• Avoid empty lines inside definitions or proofs. (10 violations)

  • CompPoly/Univariate/Raw/Division.lean: Line 77 (empty line inside proof of trim_size_eq_natDegree_succ)
  • CompPoly/Univariate/Raw/Division.lean: Line 97 (empty line inside proof of leadingCoeff_toPoly)
  • CompPoly/Univariate/Raw/Division.lean: Line 321 (empty line inside proof of divByMonic_unfold_step)

• Use backticks for Lean names: `List.map`. (10 violations)

  • CompPoly/Univariate/Raw/Division.lean: Line 23 (unquoted CPolynomial.Raw.divModByMonicAux in section comment)
  • CompPoly/Univariate/Raw/Division.lean: Line 125 (unquoted toPoly and divModByMonicAux in docstring)
  • CompPoly/Univariate/Raw/Division.lean: Line 250 (unquoted Polynomial.divModByMonicAux in docstring)

• Use the where syntax for defining instances and structures. (4 violations)

  • CompPoly/Univariate/Division.lean: Line 29 (instance : Div (CPolynomial R) := ⟨div⟩)
  • CompPoly/Univariate/Division.lean: Line 30 (instance : Mod (CPolynomial R) := ⟨mod⟩)
  • CompPoly/Univariate/Raw/Division.lean: Line 236 (instance [Field R] : Div (CPolynomial.Raw R) := ⟨div⟩)

• Use standard file headers including copyright, license (Apache 2.0), and authors. (1 violation)

  • CompPoly/Univariate/Division.lean: Line 1 (file header is entirely missing)

• Each file should start with a /-! ... -/ block containing a title, summary, notation, and references. (1 violation)

  • CompPoly/Univariate/Division.lean: Line 1 (module docstring is entirely missing)

• Keep lines under 100 characters. (1 violation)

  • CompPoly/Univariate/Raw/Division.lean: Line 126 (104 characters)

• Avoid using ; to separate tactics unless writing short, single-line tactic sequences. (1 violation)

  • CompPoly/Univariate/Raw/Division.lean: Line 60 (unfold toPoly at *; aesop)

• Prefer fun x ↦ ... over λ x, .... (1 violation)

  • CompPoly/Univariate/Raw/Division.lean: Line 128 (uses => instead of ↦ in fun p q => toPoly_mul p q)

---

📄 **Per-File Summaries**

• CompPoly/Univariate/Basic.lean: This change removes the polynomial division operations and their associated Div and Mod instances, including divByMonic and modByMonic, from the univariate polynomial implementation. No new theorems or definitions were added, and no sorry or admit placeholders were introduced.
• CompPoly/Univariate/Division.lean: This new file defines univariate polynomial division and remainder operations for the CPolynomial type, including both general (div, mod) and monic-specific (divByMonic, modByMonic) variants. It implements standard Div and Mod instances and provides correctness theorems (div_toPoly, mod_toPoly) to verify that these operations match Mathlib's Polynomial division.
• CompPoly/Univariate/Raw/Division.lean: This PR refactors divModByMonicAux to use well-founded recursion based on polynomial size and introduces a suite of theorems proving that Raw division and modulus operations are consistent with mathlib's Polynomial API. It adds several technical lemmas relating Raw attributes—such as leadingCoeff, natDegree, and monic—to their polynomial counterparts to facilitate these correctness proofs. No sorry or admit placeholders were introduced.

---

Last updated: 2026-04-08 17:54 UTC.

[dhsorens]

@tomaz1502 this is a good pull request, apologies for the delay as we have had some travel for conferences. I think it's a good idea to have DivMod.lean as you have it, and I like how the relevant operations are proved correct wrt the Mathlib specs

There has been a refactor of the Univariate directory so this needs to be refactored, but I'm happy with it since it preserves all the operations already there, and builds off of them. Are you okay doing the refactor? we can then look at merging it.

Reviewed for:

• correctness
• style
• backwards compatibility

[tomaz1502]

@tomaz1502 this is a good pull request, apologies for the delay as we have had some travel for conferences. I think it's a good idea to have DivMod.lean as you have it, and I like how the relevant operations are proved correct wrt the Mathlib specs

There has been a refactor of the Univariate directory so this needs to be refactored, but I'm happy with it since it preserves all the operations already there, and builds off of them. Are you okay doing the refactor? we can then look at merging it.

Reviewed for:

• correctness
• style
• backwards compatibility

Ok! I will take a look in the next few days.