Typeclass Instances for the Quotient Polynomial

[dhsorens]

This pull request adds the following typeclass(es) for QuotientPolynomialC:

• AddCommGroup
• Semiring
• CommSemiring
• Ring
• CommRing

This is related to the conversation on #33 pointing out that the only interesting algebraic structure on CPolynomial R will probably be a commutative semigroup

UPDATE: this is now sorry-free but needs refactoring, simplifying, and improved ergonomics

[github-actions]

🤖 Gemini PR Summary

This pull request implements key algebraic typeclass instances for QuotientCPolynomial, establishing the foundational mathematical structures required for more complex operations. This work directly addresses feedback regarding the algebraic limitations of the base CPolynomial type by focusing on the quotient structure.

Features

• Algebraic Typeclass Instances: Successfully implemented several standard algebraic structures for QuotientCPolynomial, including:
  • AddCommGroup
  • Semiring
  • Ring / CommRing
• Supporting Lemmas: Added necessary lemmas and proofs to support these instances, specifically focusing on polynomial multiplication coefficients and array folding utilities.

Refactoring

• Code Cleanup: Removed several incomplete or placeholder algebraic structure instances in CompPoly/Univariate/Basic.lean to maintain library integrity.
• Utility Improvements: Added utility lemmas for array folding to streamline internal logic.

Fixes

• Namespace Ambiguity: Qualified calls to coeff_add within the Polynomial namespace in Equiv.lean to resolve potential name collisions and improve build stability.

Documentation

• No specific documentation changes were noted in this PR.

---

Analysis of Changes

Metric	Count
📝 Files Changed	3
✅ Lines Added	986
❌ Lines Removed	85

---

sorry Tracking

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

• instance [CommSemiring R] [LawfulBEq R] : CommSemiring (CPolynomial R) where in CompPoly/Univariate/Basic.lean
• instance [Ring R] [LawfulBEq R] : Ring (CPolynomial R) where in CompPoly/Univariate/Basic.lean
• instance [LawfulBEq R] : AddCommGroup (CPolynomial R) where in CompPoly/Univariate/Basic.lean
• instance [Semiring R] [LawfulBEq R] : Semiring (CPolynomial R) where in CompPoly/Univariate/Basic.lean

---

🎨 **Style Guide Adherence**

This code review follows the provided CompPoly Style Guide.

Naming and Variable Conventions

• Lines 412, 420, 436, 694, 715, 725, 739, 772, 781, 789, 806, 821, 855 (Basic.lean); 516, 529, 663 (Quotient.lean): These lines use i or j as a variable for a ℕ (natural number).
  • Rule: "Variable Conventions: m, n, k, ... : Natural numbers; i, j, k, ... : Integers"
• Lines 694, 701, 715, 725, 739, 772, 781, 789, 821, 855 (Basic.lean); 218 (Quotient.lean): These lines use p, q, a, or b as variables for polynomial terms.
  • Rule: "Variable Conventions: x, y, z, ... : Elements of a generic type; a, b, c, ... : Propositions; p, q, r, ... : Predicates and relations"
• Line 222 (Quotient.lean): Uses l as a variable for a List.
  • Rule: "Variable Conventions: s, t, ... : Sets or Lists"
• Line 440 (Basic.lean): theorem Array.zipIdx_size.
  • Rule: "Theorems and Proofs: snake_case" (should be zip_idx_size).
• Lines 701, 772, 781, 789, 806 (Basic.lean): Theorem names like mulPowX_coeff, smul_mulPowX_coeff, coeff_add_smul_mulPowX, and mul_coeff_partial_fold_step_getElem use CamelCase.
  • Rule: "Theorems and Proofs: snake_case"
• Line 68 (Quotient.lean): lemma eq_to_equiv.
  • Rule: "Symbol Naming Dictionary: → | of / imp" (should be equiv_of_eq).

Syntax and Formatting

• Line 413 (Basic.lean): Uses rfl.
  • Rule: "Use manual dot notation for logical connectives and equality (e.g., And.intro, Eq.refl, Iff.mp)."
• Line 690 (Basic.lean): Uses -- Multiplication coefficient lemmas.
  • Rule: "Sectioning Comments: Use /-! ### Title -/ to structure large files into sections."
• Lines 790, 808 (Basic.lean): Uses arrows (→) for hypotheses in a theorem statement.
  • Rule: "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."
• Lines 812, 814 (Basic.lean); 550, 563 (Quotient.lean): Contains empty lines inside a proof block.
  • Rule: "Empty Lines: Avoid empty lines inside definitions or proofs."
• Lines 422–432 (Quotient.lean): Defines instances using := ⟨...⟩.
  • Rule: "Instances: Use the where syntax for defining instances and structures."
• Line 516 (Quotient.lean): Uses i > 0 in a theorem statement.
  • Rule: "standardize on ≤ (le) and < (lt). Avoid ≥ (ge) and > (gt) in theorem statements unless necessary for argument ordering."

Documentation

• Lines 412, 415, 420, 436, 440, 694, 701, 715, 725, 739, 772, 781, 789, 806, 821, 855 (Basic.lean); 68, 516, 522, 527, 529, 539, 545, 555 (Quotient.lean): Newly added theorems and lemmas lack docstrings.
  • Rule: "Every definition and major theorem should have a docstring."

---

📄 **Per-File Summaries**

• CompPoly/Univariate/Basic.lean: Added utility lemmas for array folding and proved theorems regarding polynomial multiplication coefficients while removing several incomplete algebraic structure instances.
• CompPoly/Univariate/Equiv.lean: Qualify calls to coeff_add with the Polynomial namespace to resolve potential name ambiguity.
• CompPoly/Univariate/Quotient.lean: Defined standard algebraic structure instances for QuotientCPolynomial—including AddCommGroup, Semiring, and CommRing—along with their necessary supporting lemmas and proofs.

---

Last updated: 2026-01-29 18:34 UTC.

[dhsorens]

mul_comm and mul_assoc are the only two remaining sorry's for this PR. substantial cleanup will need to happen as well to organize the code and break results into useful lemmas for other projects