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

Replaces legacy CPolynomial.div and CPolynomial.mod implementations with versions aligned with Mathlib's definitions, ensuring computational efficiency and mathematical consistency.

Mathematical Verification

• Termination Proofs: Includes explicit termination proofs for div and mod, ensuring they are fully computable within the Lean kernel.
• Mathlib Equivalence: Establishes formal equivalence to Polynomial.div and Polynomial.mod via the CPolynomial.toPoly mapping (e.g., div_toPoly and mod_toPoly).
• Raw Representation Lemmas: Introduces equivalence lemmas for CPolynomial.Raw to bridge low-level representations with high-level abstract polynomials.

Refactoring & API Organization

• Consolidation: Moves division and modulo logic from Basic.lean and Raw.lean to a dedicated DivMod.lean module.
• Cleanup: Removes deprecated, non-standard versions of div, mod, divByMonic, and modByMonic.
• Standard Instances: Implements type class instances to provide a standard interface for polynomial division and modulo operations.
• Library Integration: Updates the main CompPoly.lean entry point to expose these computable versions by default.

Impact

• Resolves Issue on CPolynomial.divByMonic #115.
• Co-authored-by: Aristotle (Harmonic) aristotle-harmonic@harmonic.fun

---

Analysis of Changes

Metric	Count
📝 Files Changed	4
✅ Lines Added	549
❌ Lines Removed	89

---

Lean Declarations

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

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

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

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

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

🎨 **Style Guide Adherence**

The following review identifies violations of the CompPoly style guide in the provided diff.

CompPoly/Univariate/DivMod.lean

• Lines 14–28: The module docstring is missing required sections for ## Notation and ## References.
  • Violation: "Each file should start with a /-! ... -/ block containing a title, summary, notation, and references."
• Lines 15–26: Content inside the module docstring is indented.
  • Violation: "Use standard file headers including copyright, license (Apache 2.0), and authors." (Following Lean community standards referenced in the guide).
• Line 42: Sectioning docstring is missing the ### title prefix.
  • Violation: "Use /-! ### Title -/ to structure large files into sections."
• Line 85: Use of |>.2 projection notation for an Iff result.
  • Violation: "Use manual dot notation for logical connectives and equality (e.g., And.intro, Eq.refl, Iff.mp)."
• Line 87: Use of |>.1 projection notation for an Iff result.
  • Violation: "Use manual dot notation for logical connectives and equality (e.g., And.intro, Eq.refl, Iff.mp)."
• Line 106: Use of |>.2 projection notation for an Iff result.
  • Violation: "Use manual dot notation for logical connectives and equality (e.g., And.intro, Eq.refl, Iff.mp)."
• Line 106: Use of => instead of ↦ in a function definition.
  • Violation: "Prefer fun x ↦ ... over λ x, ...."
• Line 117: Use of |>.1 projection notation for an Iff result.
  • Violation: "Use manual dot notation for logical connectives and equality (e.g., And.intro, Eq.refl, Iff.mp)."
• Line 171: Use of => instead of ↦ in a function definition.
  • Violation: "Prefer fun x ↦ ... over λ x, ...."
• Line 173: Sectioning docstring is missing the ### title prefix.
  • Violation: "Use /-! ### Title -/ to structure large files into sections."
• Line 184: Use of |>.2 projection notation for an Iff result.
  • Violation: "Use manual dot notation for logical connectives and equality (e.g., And.intro, Eq.refl, Iff.mp)."
• Line 330: Sectioning docstring is missing the ### title prefix.
  • Violation: "Use /-! ### Title -/ to structure large files into sections."
• Line 474: Theorem name Polynomial.C_mul_divByMonic_eq contains an uppercase C.
  • Violation: "Theorems and Proofs: snake_case (e.g., add_comm, list_reverse_id)."

---

📄 **Per-File Summaries**

• CompPoly.lean: Exposes univariate polynomial division and modulo functionality by adding the CompPoly.Univariate.DivMod import to the main library file.
• CompPoly/Univariate/Basic.lean: This change removes the definitions and associated type class instances for polynomial division and remainder operations (div, mod, divByMonic, and modByMonic) for the CPolynomial type.
• CompPoly/Univariate/Raw.lean: This Lean file update removes the definitions, instances, and regression tests for polynomial division and remainder, specifically divByMonic and modByMonic, from the CPolynomial.Raw structure.
• CompPoly/Univariate/DivMod.lean: This file introduces computable definitions and instances for polynomial division and modulus and establishes several theorems, such as div_toPoly and mod_toPoly, to prove their equivalence with Mathlib’s abstract polynomial operations.

---

Last updated: 2026-02-27 16:17 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