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

[github-actions]

🤖 Gemini PR Summary

This pull request implements the core algebraic hierarchy for quotient polynomials, transitioning the structure from a basic semigroup to a full commutative ring. This work addresses requirements identified in issue #33 regarding the algebraic properties of CPolynomial R.

Features

• Algebraic Typeclass Instances: Establishes QuotientCPolynomial as a member of the following standard algebraic structures:
  • AddCommGroup
  • Semiring & CommSemiring
  • Ring & CommRing
• Foundational Lemmas: Adds several supporting lemmas within CompPoly/Univariate/Quotient.lean necessary to satisfy the axioms of the aforementioned typeclasses.

Refactoring

• Status Update: While the implementation is now sorry-free, the author has noted that the current code requires further simplification and improvements to ergonomics. Future iterations may focus on streamlining the proofs and API surface.

Documentation

• Contextual Alignment: This PR directly addresses architectural discussions from issue Complete AddCommGroup instance proofs for CPolynomial R #33 regarding the intended algebraic structure of commutative polynomials.

---

Analysis of Changes

Metric	Count
📝 Files Changed	1
✅ Lines Added	326
❌ Lines Removed	1

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

🎨 **Style Guide Adherence**

• Lines 422–431, 432, 442, 452, 462, 471, 480, 489, 496, 503, 511, 519, 527, 535, 543, 551, 562, 574, 588, 603, 621, 629, 668, 684: "Every definition and major theorem should have a docstring."
• Lines 422–431: "Instances: Use the where syntax for defining instances and structures."
• Lines 430, 431: "Functions: Prefer fun x ↦ ... over λ x, ...."
• Line 637: "Delimiters: Avoid parentheses where possible. Use <| (pipe left) and |> (pipe right) to reduce nesting."
• Line 668: "Operators: Put spaces on both sides of :, :=, and infix operators."
• Line 694: "Tactic Mode: Place by at the end of the line preceding the tactic block. Indent the tactic block."

---

📄 **Per-File Summaries**

• CompPoly/Univariate/Quotient.lean: Defines standard algebraic instances for QuotientCPolynomial, establishing its structure as an AddCommGroup, Semiring, and CommRing through several supporting lemmas.

---

Last updated: 2026-02-04 10:55 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

[dhsorens]

/review

External:

Internal:
CompPoly/Univariate/

Comments:
Please review and identify any possible issues or possible improvements.

[github-actions]

🤖 AI Review (with external context)

🤖 AI Review

Overall Summary:
While the namespace refactoring in CompPoly/Univariate/Equiv.lean is correct and robust, the changes in CompPoly/Univariate/Quotient.lean are incorrect and block this PR. The Ring and Semiring instances rely on invalid proofs, specifically attempting to use rfl for non-definitional equalities in zsmul_succ' and misapplying rw to Setoid equivalences in natCast_succ. These proofs must be rewritten to explicitly handle Quotient.sound and underlying setoid properties rather than assuming definitional equality.

---

📄 **Review for `CompPoly/Univariate/Equiv.lean`**

Analysis of CompPoly/Univariate/Equiv.lean

The changes in this PR involve namespace qualifications for the lemma coeff_add. Specifically, coeff_add is replaced with Polynomial.coeff_add in two locations.

1. Hunk 1: lemma coeff_toPoly

• Diff:

  -  rw [this, coeff_add, coeff_C_mul, coeff_X_pow, mul_ite, mul_one, mul_zero, h]
  +  rw [this, Polynomial.coeff_add, coeff_C_mul, coeff_X_pow, mul_ite, mul_one, mul_zero, h]

• Context: This lemma relates the coefficients of the computable polynomial structure (CPolynomial) to the Mathlib Polynomial produced by toPoly.
• Assessment: The rewrite rw [..., coeff_add, ...] operates on terms involving Polynomial addition (implied by toPoly and the usage of coeff_C_mul/coeff_X_pow). Explicitly using Polynomial.coeff_add ensures the correct lemma for the Polynomial type is applied. This prevents potential ambiguity with other coefficient lemmas (e.g., if a coeff_add exists for CPolynomial) and aligns with standard Mathlib usage.
• Logic: Correct.

2. Hunk 2: theorem toPoly_add

• Diff:

  -  rw [coeff_add, coeff_toPoly, coeff_toPoly, coeff_toPoly, add_coeff?]
  +  rw [Polynomial.coeff_add, coeff_toPoly, coeff_toPoly, coeff_toPoly, add_coeff?]

• Context: This theorem proves that toPoly is a homomorphism with respect to addition: (addRaw p q).toPoly = p.toPoly + q.toPoly.
• Assessment: The proof uses ext n, transforming the goal into an equality of coefficients. The RHS is (p.toPoly + q.toPoly).coeff n. The lemma Polynomial.coeff_add is the standard Mathlib theorem stating (f + g).coeff n = f.coeff n + g.coeff n. Using the fully qualified name is correct and makes the proof robust against namespace changes.
• Logic: Correct.

Misformalization Checklist:

• Off-by-One Errors: None.
• Recursive Definitions: Not applicable (changes are in proof scripts).
• Incorrect Assumptions: None.
• Prop vs. Type: No issues.
• Universe Levels: No issues.

Verdict
The changes are strictly non-functional refactorings that improve the robustness and clarity of the proof scripts by explicitly namespacing the coeff_add lemma. The formalization remains correct.

Status: Correct

📄 **Review for `CompPoly/Univariate/Quotient.lean`**

This review covers the changes in CompPoly/Univariate/Quotient.lean.

Verdict

Incorrect Formalization

The Ring and Semiring instances contain proof scripts that are logically invalid for the defined structures, specifically regarding zsmul_succ', natCast_succ, and likely zsmul_zero'. While the definitions aim to lift polynomial operations to the quotient, the proofs assume definitional equalities that do not hold for quotient types or rely on tactics (rw) unsuitable for Setoid equivalence without auxiliary lemmas.

Issues Identified

1. Incorrect rfl in zsmul_succ' (Critical)

In the Ring instance, the field zsmul_succ' is proved using rfl.

zsmul_succ' := by intros _ _; rfl

• Analysis: The zsmul field is defined as zsmulRec, which delegates to nsmul for non-negative integers. nsmul on QuotientCPolynomial is lifted from CPolynomial.nsmul.
• Reasoning: The goal is (n + 1) • a = n • a + a. For rfl to work, the Left Hand Side (LHS) nsmul (n + 1) a must be definitionally equal to the Right Hand Side (RHS) nsmul n a + a.
  • LHS reduces to Quotient.mk (CPolynomial.nsmul (n+1) x).
  • RHS reduces to Quotient.mk (CPolynomial.nsmul n x + x).
  • Since CPolynomial operations are typically array-based, map (*(n+1)) arr is not definitionally equal to map (*n) arr + arr. The fact that nsmul_succ requires a non-trivial proof (using Quotient.inductionOn and Quotient.sound) confirms this is not a definitional equality.
• Correction: Use the nsmul_succ lemma explicitly.

2. Invalid rw with Equivalence in natCast_succ (Major)

In the Semiring instance:

natCast_succ := by
  intro n
  apply Quotient.sound
  intro i; rw [const_sum (n : R) (1 : R)]; simp

• Analysis: The goal after apply Quotient.sound is p ≈ q (setoid equivalence).
• Reasoning: const_sum proves (C n).add (C 1) ≈ C (n + 1). The tactic rw works with equality (=) or iff (↔), but not automatically with setoid equivalence (≈) unless specific setoid rewriting is set up, which appears absent or misused here. Furthermore, intro i suggests attempting to prove equality of coefficients, but const_sum is an equivalence of the whole polynomial structure. You cannot rewrite a global polynomial equivalence inside a coefficient quantifier.
• Correction: Use Setoid transitivity or simply apply the equivalence.

3. Fragile convert usage in intCast_negSucc (Minor)

convert h_neg_succ
convert Quotient.eq using 1

• Analysis: h_neg_succ is an equality of integers (Int.negSucc n = ...). The goal is an equality of quotient polynomials.
• Reasoning: Using convert with a term of a completely different type is highly fragile and relies on the tactic guessing that you mean to map the equality through IntCast. While it might work if the stars align, it's bad practice.
• Correction: A cleaner proof using Quotient.sound and properties of C (e.g., C (-n) = - C n) is preferred.

Corrected Code Snippets

Here are the corrected instance definitions:

-- In section Semiring
instance [Semiring R] [LawfulBEq R] : Semiring (QuotientCPolynomial R) where
  -- ... (other fields)
  natCast_succ := by
    intro n
    apply Quotient.sound
    -- C (n + 1) ≈ C n + C 1
    apply Setoid.symm
    exact const_sum n 1

-- In section Ring
instance [LawfulBEq R] : Ring (QuotientCPolynomial R) where
  -- ... (other fields)
  zsmul_succ' := by
    intros n a
    exact nsmul_succ n a
  zsmul_zero' := by
    intro a
    simp [zsmulRec]
    exact nsmul_zero a
  intCast_negSucc := by
    intro n
    apply Quotient.sound
    -- Need to show C (Int.negSucc n) ≈ - C (n + 1)
    -- This relies on C (-x) = - C x and Int casting rules
    change C (Int.cast (Int.negSucc n)) ≈ - C (Int.cast (n + 1))
    simp only [Int.cast_negSucc, Int.cast_add, Int.cast_one]
    -- Assuming C_neg and C_add exist or simps solve it:
    simp [CPolynomial.C, CPolynomial.neg]
  -- ...

[dhsorens]

Between this and #64 this takes care of issues #33 #34 #35 and #36

The Ai review is .. kind of nonsensical.