Adding algebraic properties of CPolynomial in Basic.lean

[desmondcoles1]

This PR will address the underlying problem of issues: #33 #34 #35 #36 and should provide helpful theorems and lemmas for resolving issues: #37 #38 #39 #40 #41 #42. The issue CPolynomial R does not in general form a semiring or ring because it lacks additive and multiplicative identity, but facts about arithmetic in CPolynomial R are still needed to provide proofs that related types are a certain typeclass instance. The aim is to verifying which properties hold and state the correct analogues of things that don't hold. For example we should have:
theorem mul_assoc [LawfulBEq R] (p q r : CPolynomial R) : p * q * r = p * (q * r) and while it is not true that p+0=0+p=p we do have that:
theorem zero_add_trim [LawfulBEq R] (p : CPolynomial R) : 0 + p = p.trim

• zero_add_trim
• add_zero_trim
• one_mul_trimmed
• mul_one_trim
• left_distrib
• right_distrib
• mul_assoc
• mul_comm
• zero_mul
• mul_zero

This PR would also change the definition of mul. The multiplication function was changed so that the initial accumulator is now the empty array and not [0]. When the initial accumulator is [0] this causes odd behavior with multiplication, for example [0]*[]=[] but []*[0]=[0] when the initial accumulator is [0]. This change is necessary for some of the algebraic properties to hold.

def mul (p q : CPolynomial R) : CPolynomial R :=
  p.zipIdx.foldl (fun acc ⟨a, i⟩ => acc.add <| (smul a q).mulPowX i) (mk #[])

This PR would also include a definition for natDegree:

def natDegree (p : CPolynomial R) : ℕ :=
    match p.lastNonzero with
    | none => 0
    | some i => i.val + 1

[github-actions]

🤖 Gemini PR Summary

This Pull Request focuses on formalizing the algebraic properties of the CPolynomial type. Since CPolynomial lacks standard additive and multiplicative identities to qualify as a full semiring, this PR introduces "trimmed" versions of algebraic laws (e.g., p + 0 = p.trim) and formalizes core properties like associativity and commutativity. This work is foundational for resolving several downstream issues related to typeclass instances.

Features

• Algebraic Proofs: Added formal proofs for key properties of polynomial arithmetic, including:
  • Associativity (mul_assoc) and Commutativity (mul_comm).
  • Distributivity (left_distrib, right_distrib).
  • Multiplication by zero (zero_mul, mul_zero).
  • Identity-like behavior with trimming (zero_add_trim, add_zero_trim, one_mul_trimmed, mul_one_trim).
• Degree Calculation: Introduced the natDegree function to compute the degree of a polynomial based on its last non-zero coefficient.

Refactoring

• Multiplication Logic Update: Modified the mul function to use an empty array (mk #[]) as the initial accumulator instead of a zero-initialized array ([0]). This change resolves an inconsistency where [0] * [] resulted in [] while [] * [0] resulted in [0], ensuring that algebraic properties like commutativity hold.
• Consistency Updates: Synchronized lemmas in CompPoly/Univariate/Quotient.lean to reflect the updated mul implementation and its new accumulator behavior.

Fixes

• Placeholder Replacement: Replaced existing placeholders in CompPoly/Univariate/Basic.lean with formal, verified proofs for core algebraic operations.
• Multiplication Asymmetry: Fixed edge-case bugs in polynomial multiplication involving empty or zero-valued polynomials.

Documentation

• Updated internal documentation and theorem statements to clarify the relationship between CPolynomial arithmetic and standard ring theory, specifically explaining why "trimming" is necessary in the absence of traditional identity elements.

---

Analysis of Changes

Metric	Count
📝 Files Changed	2
✅ Lines Added	682
❌ Lines Removed	76

---

sorry Tracking

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

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

✏️ **Affected:** 1 `sorry`(s) (line number changed)

• def natDegree (p : CPolynomial R) : ℕ in CompPoly/Univariate/Basic.lean moved from L98 to L97

---

🎨 **Style Guide Adherence**

Based on the provided style guide, here are the specific lines that violate the guidelines:

• Lines 600, 704, 708, 841, 845, 856, 869, 1121, 1131, 1141, 1155, 1176, 1221, 1274, 1307: Missing docstrings.
  • "Every definition and major theorem should have a docstring."
• Lines 603-610, 729-733, 744-762, 861-867, 895-903, 918-919, 939-952, 994-1013, 1180-1215, 1231-1272: Indentation does not use 2 spaces (many lines use 4 or 6 space increments).
  • "Use 2 spaces for indentation."
• Lines 606, 740, 880, 882, 908, 912, 926, 938, 986, 993, 1020, 1201, 1225, 1228: Use of => in function definitions.
  • "Prefer fun x ↦ ... over λ x, ...." (Note: In Lean 4, the standard for this preference is the ↦ symbol).
• Line 608: rw[h_add, ←h_trim_coeff]
  • "Put spaces on both sides of :, :=, and infix operators." (Missing space after rw and ←).
• Line 755, 862, 929, 1011, 1046, 1102, 1205: Use of ; to separate tactics.
  • "Avoid using ; to separate tactics unless writing short, single-line tactic sequences."
• Line 806: (Finset.range p.size).sum (fun i => if k < i then 0 else p.coeff i * q.coeff (k - i)) =
  • "Keep lines under 100 characters." (Line is 102 characters).
• Line 1162: a.mul b = (a.zipIdx.foldl (fun acc ⟨a', i⟩ => acc.add ((smul a' b).mulPowX i)) (mk #[])) :=
  • "Keep lines under 100 characters." (Line is 104 characters).
• Line 1172: rw[this, zero_add_trim]
  • "Put spaces on both sides of :, :=, and infix operators." (Missing space after rw).
• Line 1311: section AddCommSemiroup
  • "Spelling: Use American English for declaration names." (Typo: "Semiroup" should be "Semigroup").
• Quotient.lean: Line 217: a.mul b = (a.zipIdx.foldl (fun acc ⟨a', i⟩ => acc.add ((smul a' b).mulPowX i)) (mk #[])) :=
  • "Keep lines under 100 characters." (Line is 102 characters).

---

📄 **Per-File Summaries**

• CompPoly/Univariate/Basic.lean: This update implements and proves the core algebraic properties of CPolynomial multiplication—including associativity, distributivity, and commutativity—replacing previous placeholders with formal proofs.
• CompPoly/Univariate/Quotient.lean: Update the initial accumulator from C 0 to mk #[] in multiplication lemmas to ensure consistency with the underlying implementation of the mul operation.

---

Last updated: 2026-02-03 18:17 UTC.

[desmondcoles1]

At this point the major theorems have been added, the file is sorry free and has been organized. I think that the issues related to typelcasses in CPolynomial can be closed and that the issues opened regarding typeclasses instances for CPolynomialC should be easier to tackle. I am going to going to finalize this PR now.

[dhsorens]

@desmondcoles1 this looks great to me - the organization is good, the lemmas proved will be really nice for both the Quotient and the Canonical typeclasses; as you pointed out Canonical is a natural next step. Note the one comment on the misformalized lemma.

Something to consider (not necessarily for this PR) - a lot of these lemmas are the core computational primitives for raw polynomials and ideally we can automate use of them in future proofs. You'll probably find that the best way to go about doing things is to add them to the simp or grindset so that typeclass instance proofs in Canonical are mostly done by grind. Ideally we build up a good set of lemmas that grind can use so that the more obvious aspects of proofs of computation over the polynomials are done with grind.

[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:
The pull request cannot be approved due to a critical misformalization in CompPoly/Univariate/Basic.lean, where natDegree contains an off-by-one error that calculates the coefficient array length rather than the polynomial degree. While the updates to the mul definition and the removal of Ring instances are logically sound and correctly synchronized with CompPoly/Univariate/Quotient.lean, the definition of degree contradicts both standard mathematical conventions and the function's own docstring. Please correct natDegree to return the index of the last non-zero coefficient before merging.

---

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

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

Verdict

Incorrect. The code contains a critical misformalization in the definition of natDegree that contradicts its documentation and standard mathematical definitions.

---

Critical Issues

1. Off-by-One Error in natDegree

• Location: def natDegree
• Problem: The function is defined as i.val + 1 when lastNonzero is some i.
  • The docstring states this "Matches Mathlib's Polynomial.natDegree API".
  • In Mathlib (and standard mathematics), the degree of a non-zero polynomial is the index of the highest non-zero coefficient. For example, for a constant polynomial $p(x) = c$ ($c \neq 0$), the index is 0, so the degree is 0.
  • The current implementation returns 0 + 1 = 1 for a constant polynomial. It essentially calculates the "order" or "length of the active prefix" rather than the degree.
• Correct Formalization:

  def natDegree (p : CPolynomial R) : ℕ :=
    match p.lastNonzero with
    | none => 0
    | some i => i.val

Other Observations (Non-Critical)

1. Removal of Ring Instances
The diff shows the removal of Semiring, Ring, etc., instances, replacing them with AddCommSemigroup.

• Analysis: This is likely correct for this specific data structure. The type CPolynomial appears to be a raw array wrapper. Without a quotient or subtype ensuring canonical forms (trimmed arrays), the axiom add_zero ($p + 0 = p$) fails because $0 + p$ returns the trimmed version of $p$. If $p$ has trailing zeros, $0 + p \neq p$.
• Feedback: Restricting the instance to AddCommSemigroup correctly reflects the algebraic properties of the raw type.

2. mul Definition

• Change: Initializing the fold accumulator with mk #[] instead of C 0.
• Analysis: This is correct and ensures the calculation starts with the canonical empty polynomial.

3. Proofs and Lemmas

• Analysis: The extensive addition of lemmas (mul_assoc, left_distrib, right_distrib, etc.) appears methodologically sound, utilizing convolution sums and index manipulation to prove ring properties at the coefficient level.

Summary

The file is well-structured regarding the algebraic proofs, but the natDegree definition is factually incorrect and must be fixed to align with the provided specification (Mathlib API compatibility).

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

Review of CompPoly/Univariate/Quotient.lean

General Assessment
The changes in this file replace instances of C 0 (representing the constant polynomial $0$) with mk #[] (representing a polynomial with an empty coefficient array) in the context of the mul function's definition and accumulator.

These changes appear to be maintenance updates aligning the proof scripts with a refactor in the definition of CPolynomial.mul. Specifically, the use of rfl (reflexivity) to prove h_mul_def in mul_equiv₂ confirms that the definition of mul definitionally starts with mk #[].

Detailed Check

1. Logic and Consistency (Hunks 1 & 2):

   • Change: have h_mul_def ... (C 0) $\to$ have h_mul_def ... (mk #[]).
   • Analysis: The proof strategy uses unfold mul followed by Eq.symm (in mul_trim_equiv) and rfl (in mul_equiv₂). This strictly requires the term in the have statement to match the body of the mul definition exactly. The change indicates mul initializes its accumulator with an empty array. This is a correct and standard implementation technique for sparse or computational polynomials.
   • Verdict: Correct.

2. Accumulator State (Hunk 3):

   • Change: convert h_foldl_equiv ... (C 0) $\to$ convert h_foldl_equiv ... (mk #[]).
   • Analysis: This step applies the helper lemma h_foldl_equiv to the specific case of the multiplication fold. Since the fold starts with mk #[] (as established in the previous points), passing mk #[] as the initial accumulator acc is logically consistent.
   • Verdict: Correct.

Misformalization Checklist

• Off-by-One Errors: None. The change concerns the initial state (empty) rather than boundary indices.
• Recursive Definitions: The foldl structure is preserved. The base case for the fold is the zero polynomial. mk #[] is a valid representation of zero in this structure.
• Incorrect Assumptions: The changes do not weaken or strengthen assumptions; they only adjust the proof terms to match definitions.
• Prop vs. Type: No misuse observed.
• Universe Levels: No changes to universe levels.

Verdict & Feedback

Formalization Correct.
The changes correctly update the proofs to reflect that CPolynomial.mul is defined using mk #[] as the initial accumulator. This ensures the proofs rely on the actual definitional equality of the function, which is required for tactics like rfl and unfold to behave as expected.

[dhsorens]

I think the AI is right - that this should actually be some i => i.val. e.g. C r has degree zero and (C r).lastNonzero returns 0. I recognize that the definition of degree is probably wrong. Do you agree @quangvdao ?

[desmondcoles1]

I looked into this and I think this issue has a little more going than just indexing. I do agree that the indexing is wrong, but this is a simple fix.

More significantly though, as in the docstrings, we want to mirror mathlib's definitions. So I believe that we should use the following definitions for degree and natdDegree:

/-- Return the degree of a `CPolynomial`. -/
def degree (p : CPolynomial R) : WithBot ℕ :=
  match p.lastNonzero with
  | none => ⊥
  | some i => i.val

/-- Natural number degree of a `CPolynomial`.

  Returns the degree as a natural number. For the zero polynomial, returns `0`.
  This matches Mathlib's `Polynomial.natDegree` API.
-/
def natDegree (p : CPolynomial R) : ℕ := 
  match p.lastNonzero with
  | none => 0
  | some i => i.val

This change causes a few issues, and I want to have some time to investigate them, and of course I want input for both of you. This issue about the definition of degree is also not important for the rest of the content of this PR. My suggestion for proceeding: I am going to remove this definition of natDegree and keep degree the way it is in the current version of the main branch. I will open a separate PR to deal with this issue, so at least we can close this PR.

[dhsorens]

yeah that sounds good, agreed with you here

[dhsorens]

great, I'm happy with this! merging