Proofs for typeclass instances of CPolynomial

[desmondcoles1]

This PR does a refactoring of Raw.Lean to allow for the case when R is a Semiring. This PR also fills in the proofs for the typeclass instances in Basic.Lean. This PR should close issues #37 #38 #39 #40 #41.

TODO:

• Double check section variables in Raw.Lean and Basic.Lean I am afraid that I may have overloaded some of the notation which can cause unnecessary issues with typeclasses in proofs.
• Fill in sorries for npow n p and npow_succ
• Fix issues in Equiv.Lean, it is not compiling for some reason.

[github-actions]

🤖 Gemini PR Summary

This PR generalizes the CPolynomial framework to support Semirings and completes the formal algebraic hierarchy for the univariate polynomial implementation. It addresses and closes issues #37, #38, #39, #40, and #41.

Features

• Algebraic Instance Completion: Successfully implemented and proved typeclass instances for CPolynomial, including:
  • Semiring
  • CommSemiring
  • Ring
  • CommRing
• Type Generalization: Expanded the CPolynomial type to support coefficients from any semiring R, moving away from stricter ring/field requirements where possible.

Refactoring

• Raw.Lean Restructuring:
  • Generalized basic polynomial operations to work at the semiring level.
  • Reorganized the codebase to clearly separate definitions into ring-specific and field-specific sections, improving modularity and typeclass resolution.
• Notation & Variables: Initial cleanup of section variables to ensure consistent notation across Raw.Lean and Basic.Lean.

Documentation & Maintenance

• Issue Resolution: This PR provides the necessary proofs to close five outstanding issues (Prove multiplicative properties for CPolynomialC R #37–Complete Ring instance proofs for CPolynomialC R #41) related to missing typeclass instances.

---

⚠️ Work in Progress / Known Issues

As per the author's notes, the following items require attention before merging:

1. Missing Proofs: npow n p and npow_succ currently contain sorry placeholders and need to be completed.
2. Regression in Equiv.Lean: The changes have caused compilation errors in Equiv.Lean that are currently being debugged.
3. Typeclass Ambiguity: A final audit of section variables is needed to ensure that notation overloading isn't causing performance hits or resolution failures in the typeclass inference system.

---

Analysis of Changes

Metric	Count
📝 Files Changed	2
✅ Lines Added	201
❌ Lines Removed	123

---

sorry Tracking

✅ **Removed:** 10 `sorry`(s)

• lemma zero_mul (p : CPolynomial R) : 0 * p = 0 in CompPoly/Univariate/Basic.lean
• instance [LawfulBEq R] [Nontrivial R] : Ring (CPolynomial R) where in CompPoly/Univariate/Basic.lean
• lemma one_mul (p : CPolynomial R) : 1 * p = p in CompPoly/Univariate/Basic.lean
• lemma mul_assoc (p q r : CPolynomial R) : (p * q) * r = p * (q * r) in CompPoly/Univariate/Basic.lean
• lemma right_distrib (p q r : CPolynomial R) : (p + q) * r = p * r + q * r in CompPoly/Univariate/Basic.lean
• def monomialC [DecidableEq R] (n : ℕ) (c : R) : CPolynomial R in CompPoly/Univariate/Basic.lean
• lemma mul_zero (p : CPolynomial R) : p * 0 = 0 in CompPoly/Univariate/Basic.lean
• lemma left_distrib (p q r : CPolynomial R) : p * (q + r) = p * q + p * r in CompPoly/Univariate/Basic.lean
• lemma mul_one (p : CPolynomial R) : p * 1 = p in CompPoly/Univariate/Basic.lean
• instance [CommSemiring R] [LawfulBEq R] [Nontrivial R] : CommSemiring (CPolynomial R) where in CompPoly/Univariate/Basic.lean

---

🎨 **Style Guide Adherence**

Review of Code Changes for CompPoly

CompPoly/Univariate/Basic.lean

• Line 153: rw[this, one_mul_trim] — "We aim to adhere to the Lean community's contribution guidelines." (Missing space after rw).
• Line 153: (1: CPolynomial.Raw R) — "Put spaces on both sides of :, :=, and infix operators."
• Line 159: rw[this, mul_one_trim] — "We aim to adhere to the Lean community's contribution guidelines." (Missing space after rw).
• Line 159: (1: CPolynomial.Raw R) — "Put spaces on both sides of :, :=, and infix operators."
• Line 214: right_distrib := by intro p q r; exact right_distrib p q r — "We aim to adhere to the Lean community's contribution guidelines." (Extra whitespace after by).
• Line 258: have dist_lhs : (-p + p).val = ((-p).val + p.val) := rfl — "We aim to adhere to the Lean community's contribution guidelines." (Extra whitespace before =).

CompPoly/Univariate/Raw.lean

• Line 1367: def neg (p : CPolynomial.Raw R) : CPolynomial.Raw R := p.map (fun a => -a) — "Every definition and major theorem should have a docstring."
• Line 1367: (fun a => -a) — "Prefer fun x ↦ ... over λ x, ...." (Use of => instead of ↦).
• Line 1371: def sub (p q : CPolynomial.Raw R) : CPolynomial.Raw R := p.add q.neg — "Every definition and major theorem should have a docstring."
• Line 1373: instance : Neg (CPolynomial.Raw R) := ⟨CPolynomial.Raw.neg⟩ — "Use the where syntax for defining instances and structures."
• Line 1374: instance : Sub (CPolynomial.Raw R) := ⟨CPolynomial.Raw.sub⟩ — "Use the where syntax for defining instances and structures."
• Line 1375: instance : IntCast (CPolynomial.Raw R) := ⟨fun n => CPolynomial.Raw.C (n : R)⟩ — "Use the where syntax for defining instances and structures."
• Line 1375: (fun n => ...) — "Prefer fun x ↦ ... over λ x, ...." (Use of => instead of ↦).
• Line 1378: def divModByMonicAux [Field R] ... — "Every definition and major theorem should have a docstring."
• Line 1395: def divByMonic [Field R] ... — "Every definition and major theorem should have a docstring."
• Line 1400: def modByMonic [Field R] ... — "Every definition and major theorem should have a docstring."
• Line 1405: def div [Field R] ... — "Every definition and major theorem should have a docstring."
• Line 1409: def mod [Field R] ... — "Every definition and major theorem should have a docstring."
• Line 1411: instance [Field R] : Div (CPolynomial.Raw R) := ⟨div⟩ — "Use the where syntax for defining instances and structures."
• Line 1412: instance [Field R] : Mod (CPolynomial.Raw R) := ⟨mod⟩ — "Use the where syntax for defining instances and structures."
• Line 1414: lemma neg_coeff : ∀ (p : CPolynomial.Raw R) (i : ℕ), ... — "Every definition and major theorem should have a docstring."
• Line 1414: lemma neg_coeff : ∀ (p : CPolynomial.Raw R) (i : ℕ), ... — "Prefer placing hypotheses to the left of the colon (e.g., (h : P) : Q) rather than using arrows (: P → Q) when the proof introduces them." (Use of ∀ instead of variables left of colon).

---

📄 **Per-File Summaries**

• CompPoly/Univariate/Basic.lean: Generalized the CPolynomial type to support semirings and completed the proofs for its algebraic hierarchy, including Semiring, CommSemiring, Ring, and CommRing instances.
• CompPoly/Univariate/Raw.lean: Generalize basic polynomial operations to semirings and reorganize ring- and field-specific definitions into dedicated sections.

---

Last updated: 2026-02-05 18:42 UTC.

[dhsorens]

I'm encountering some weird typeclass issues after the refactor that look like might be a problem for you here as well - I wonder if we should revert the refactor, fill in the sorrys for canonical polynomials, and then I can do the refactor again but more carefully?

[dhsorens]

I opened #74 to have a reverted branch available - feel free to write a pull request into that branch if this one is giving too many problems and then I'll merge there and redo the refactor (hopefully in a way that doesn't cause weird problems for us in future) -- equally if the problems you're facing don't have anything to do with the refactor then feel free to keep going here and we'll sort things out!

[dhsorens]

sorry to spam with comments - I opened #75 off of the refactored (main) branch and things seem to be fine, even though names are somewhat awkward still. the awkward naming doesn't have to be resolved now or in this PR