Refactor: Basic => Raw / Canonical => Basic

[dhsorens]

This pull request addresses the comment previously in Univariate/Canonical.lean and enshrines the "canonical" type of CPolynomial to be the subtype of trimmed (raw) coefficient arrays. This will make the primary interface into computable polynomials a subtype, which should be much easier to work with as opposed to the Quotient type.

[github-actions]

🤖 Gemini PR Summary

This pull request executes a significant structural refactor of the CPolynomial library. The primary goal is to shift the library’s main interface from a Quotient-based type to a Subtype of "trimmed" arrays. This change simplifies the development and usage of computable polynomials by providing a unique canonical representation that is easier to reason about than quotient types.

Refactoring

• Core Type Redefinition: Promoted the "Canonical" polynomial (a subtype of trimmed raw arrays) to be the primary CPolynomial type in CompPoly/Univariate/Basic.lean.
• Namespace Migration: Renamed the previous raw array implementation to CPolynomial.Raw to clearly distinguish between unvalidated raw data and the validated canonical type.
• File Restructuring:
  • Deleted CompPoly/Univariate/Canonical.lean, merging its logic into the new Basic.lean structure.
  • Updated CompPoly/Univariate/Equiv.lean to reflect the renaming of CPolynomialC to CPolynomial.
  • Updated CompPoly/Univariate/Lagrange.lean and CompPoly/Univariate/Quotient.lean to consume the new CPolynomial.Raw API.
• Import Optimization: Reorganized imports in the top-level CompPoly.lean to reflect the new hierarchy.

Features

• New Raw Representation: Introduced CompPoly/Univariate/Raw.lean, which explicitly defines the array-based computable representation for univariate polynomials and implements its core algebraic operations. This provides a clean foundation for the higher-level CPolynomial subtype.

Summary of Naming Changes

Old Name	New Name	Description
CPolynomial (Legacy)	CPolynomial.Raw	Raw array-based coefficient storage.
CPolynomialC / Canonical	CPolynomial	The primary interface; a subtype of Raw representing trimmed/unique polynomials.

---

Analysis of Changes

Metric	Count
📝 Files Changed	7
✅ Lines Added	1761
❌ Lines Removed	1721

---

sorry Tracking

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

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

❌ **Added:** 12 `sorry`(s)

• instance : Mul (CPolynomial R) where in CompPoly/Univariate/Basic.lean
• lemma mul_one (p : CPolynomial R) : p * 1 = p 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 one_mul (p : CPolynomial R) : 1 * p = p in CompPoly/Univariate/Basic.lean
• instance [Ring R] [LawfulBEq R] [Nontrivial R] : Ring (CPolynomial R) where in CompPoly/Univariate/Basic.lean
• instance [Semiring R] [LawfulBEq R] [Nontrivial R] : Semiring (CPolynomial R) where in CompPoly/Univariate/Basic.lean
• lemma zero_mul (p : CPolynomial R) : 0 * p = 0 in CompPoly/Univariate/Basic.lean
• instance [CommSemiring R] [LawfulBEq R] [Nontrivial R] : CommSemiring (CPolynomial R) where 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_zero (p : CPolynomial R) : p * 0 = 0 in CompPoly/Univariate/Basic.lean
• lemma mul_assoc (p q r : CPolynomial R) : (p * q) * r = p * (q * r) in CompPoly/Univariate/Basic.lean

---

🎨 **Style Guide Adherence**

The following code changes violate the CompPoly Style and Naming Guidelines:

CompPoly/Univariate/Basic.lean

• Line 32: instance : Inhabited (CPolynomial R) := ⟨#[], Trim.canonical_empty⟩
  • "Use the where syntax for defining instances and structures."
• Line 34: variable {R : Type*} [Ring R] [BEq R] [LawfulBEq R]
  • "Variable Conventions: α, β, γ, ... : Generic types"
• Line 35: variable {Q : Type*} [Ring Q]
  • "Variable Conventions: α, β, γ, ... : Generic types"
• Line 75: instance : Zero (CPolynomial R) := ⟨0, zero_canonical⟩
  • "Use the where syntax for defining instances and structures."
• Line 140: def monomialC [DecidableEq R] (n : ℕ) (c : R) : CPolynomial R :=
  • "Naming Conventions: Functions and Terms: lowerCamelCase (e.g., binarySearch, isPrime)." (Should be monomialc or monomial).

CompPoly/Univariate/Raw.lean

• Line 145: theorem lastNonzero_none [LawfulBEq R] {p : CPolynomial.Raw R} :
  • "Documentation Standards: Every definition and major theorem should have a docstring."
• Line 238: theorem size_eq_degree_plus_one (p : CPolynomial.Raw R) (h_trim: p.trim ≠ (mk #[])) :
  • "Symbol Naming Dictionary: + | add" (Should be add_one).
  • "Theorem Naming Logic: Hypotheses: Use _of_ to separate hypotheses, listed in the order they appear."
  • "Documentation Standards: Every definition and major theorem should have a docstring."
• Line 523: def smul (r : R) (p : CPolynomial.Raw R) : CPolynomial.Raw R := .mk (Array.map (fun a => r * a) p)
  • "Functions: Prefer fun x ↦ ... over λ x, ...."
• Line 563: instance : Zero (CPolynomial.Raw R) := ⟨#[]⟩
  • "Use the where syntax for defining instances and structures."
• Line 790: lemma foldl_preserves_canonical {α : Type*} (f : CPolynomial.Raw R → α → CPolynomial.Raw R) (z : CPolynomial.Raw R) (as : Array α) (hz : z.trim = z) (hf : ∀ acc x, (f acc x).trim = f acc x) : (as.foldl f z).trim = as.foldl f z := by
  • "Line Length: Keep lines under 100 characters."
• Line 858: (Empty line between induction cases)
  • "Empty Lines: Avoid empty lines inside definitions or proofs."
• Line 1146: lemma mul_comm_equiv [LawfulBEq R] (p q : CPolynomial.Raw R) :
  • "Documentation Standards: Every definition and major theorem should have a docstring."

CompPoly/Univariate/Lagrange.lean

• Line 30: def interpolate {R : Type*} [Field R] [BEq R] (n : ℕ) (ω : R) (r : Vector R n) : CPolynomial.Raw R :=
  • "Variable Conventions: p, q, r, ... : Predicates and relations" (Variable r is used for a vector/list, which should be s or t).
  • "Variable Conventions: α, β, γ, ... : Generic types" (Using R for Type).

---

📄 **Per-File Summaries**

• CompPoly.lean: Updates the univariate polynomial module imports by adding Raw, removing Canonical, and reordering Quotient.
• CompPoly/Univariate/Basic.lean: Redefines CPolynomial as a subtype of trimmed raw polynomials to ensure a unique canonical representation and establishes its core algebraic typeclass instances.
• CompPoly/Univariate/Canonical.lean: This file, which defined the subtype and algebraic structure for canonical (trimmed) univariate polynomials, has been deleted.
• CompPoly/Univariate/Equiv.lean: Renames CPolynomial to CPolynomial.Raw and CPolynomialC to CPolynomial to clarify the distinction between raw array representations and canonical polynomials.
• CompPoly/Univariate/Lagrange.lean: Refactor Lagrange interpolation functions to use the CPolynomial.Raw type and namespace.
• CompPoly/Univariate/Quotient.lean: Updates the QuotientCPolynomial definitions and proofs to use the renamed CPolynomial.Raw representation instead of CPolynomial.
• CompPoly/Univariate/Raw.lean: Defines CPolynomial.Raw R as an array-based computable representation for univariate polynomials and implements its core algebraic operations and properties.

---

Last updated: 2026-02-05 09:48 UTC.

[dhsorens]

@quangvdao @Julek from our conversations previously, for the Univariate case it probably makes sense for what was previously the "Canonical" trimmed subtype of CPolynomial to be the CPolynomial type, and to set the untrimmed type to CPolynomial.Raw

This PR does that,

• renaming CPolynomialC to CPolynomial, and Canonical.lean to Basic.lean,
• renaming CPolynomial to CPolynomial.Raw and Basic.lean to Raw.lean

Any comments are welcome, will probably merge this refactor fairly soon if there are no objections.

[quangvdao]

Sounds good to me

[dhsorens]

great, merging