Computable API for canonical polynomails

[dhsorens]

This pull request adds a mathlib-style API to (canonical) univariate polynomials, along with proofs of correctness. The general style is:

1. define a computable function on polynomials in Basic.lean, then
2. prove that it is equivalent to the mathlib definition in ToPoly.lean.

still a WIP

[github-actions]

🤖 Gemini PR Summary

This PR introduces a computable API for canonical univariate polynomials (CPolynomial), designed to align with Mathlib's naming conventions and structure. The implementation follows a two-step pattern: defining computable operations on array-backed structures and subsequently proving their equivalence to Mathlib’s non-computable definitions.

Features

• Expanded CPolynomial API: Implements core polynomial operations including coefficient access, degree calculation, evaluation, and Euclidean division.
• Induction Principle: Adds a native induction principle for CPolynomial to facilitate easier proofs on the computable type.
• Raw API Enhancements: Expands CPolynomial.Raw with low-level lemmas for coefficients, power properties, and an erase operation for manipulating specific terms.
• Mathlib Integration (ToPoly): Adds correctness theorems proving that computable operations on CPolynomial are equivalent to their counterparts in Mathlib when mapped via the toPoly conversion function.

Fixes

• No specific bug fixes are identified in this PR; the focus is on feature expansion and API alignment.

Refactoring

• Standardized Naming: Renamed distributivity lemmas in CPolynomial.Raw and QuotientCPolynomial to mul_add and add_mul to adhere to standard Lean 4/Mathlib naming conventions.
• Instance Updates: Updated Semiring instances to reflect renamed lemmas and ensure consistency across the quotient and raw implementations.

Documentation

• Project Overview: Added CompPoly/Univariate/README.md, which provides high-level documentation on the array-backed implementation, the module's organizational structure, and how the library integrates with Mathlib.

---

Analysis of Changes

Metric	Count
📝 Files Changed	5
✅ Lines Added	902
❌ Lines Removed	85

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

🎨 **Style Guide Adherence**

The following lines violate the provided style guide:

• CompPoly/Univariate/Basic.lean:53: variable (p q r : CPolynomial R)
  • Violated Rule: "Variable Conventions: p, q, r, ... : Predicates and relations" (Polynomials are elements, which should use x, y, z).
• CompPoly/Univariate/Basic.lean:112: def coeff (p : CPolynomial R) (i : ℕ) : R := p.val.coeff i
  • Violated Rule: "Variable Conventions: i, j, k, ... : Integers" (Natural number indices should use m, n, k) and "p, q, r, ... : Predicates and relations" (Elements should use x, y, z).
• CompPoly/Univariate/Basic.lean:115: def C (r : R) : CPolynomial R := ⟨(Raw.C r).trim, by rw [Trim.trim_twice]⟩
  • Violated Rule: "Naming Conventions: Functions and Terms: lowerCamelCase" (The name C is capitalized) and "Variable Conventions: p, q, r, ... : Predicates and relations" (The element r should use x, y, or z).
• CompPoly/Univariate/Basic.lean:118: def X [Nontrivial R] : CPolynomial R := ⟨Raw.X, X_canonical⟩
  • Violated Rule: "Naming Conventions: Functions and Terms: lowerCamelCase" (The name X is capitalized).
• CompPoly/Univariate/Basic.lean:124: def monomial [DecidableEq R] (n : ℕ) (c : R) : CPolynomial R :=
  • Violated Rule: "Variable Conventions: a, b, c, ... : Propositions" (The element c should use x, y, or z).
• CompPoly/Univariate/Basic.lean:149: (Finset.range p.val.size).filter (fun i => p.val.coeff i != 0)
  • Violated Rule: "Syntax and Formatting: Functions: Prefer fun x ↦ ... over λ x, ..." (The => syntax is used instead of the preferred ↦ arrow).
• CompPoly/Univariate/Basic.lean:543: induction' n with n ih generalizing p;
  • Violated Rule: "Syntax and Formatting: Delimiters: Avoid using ; to separate tactics unless writing short, single-line tactic sequences."
• CompPoly/Univariate/Basic.lean:635: by_cases h_empty : p.val.size = 0;
  • Violated Rule: "Syntax and Formatting: Delimiters: Avoid using ; to separate tactics unless writing short, single-line tactic sequences."
• CompPoly/Univariate/Raw.lean:1141: convert zero_add_trim ( smul r q ) using 1
  • Violated Rule: "Syntax and Formatting: Delimiters: Avoid parentheses where possible." (And by extension, unnecessary padding spaces inside them).
• CompPoly/Univariate/ToPoly.lean:352: theorem C_toPoly [LawfulBEq R] (r : R) : (C r).toPoly = Polynomial.C r := by
  • Violated Rule: "Variable Conventions: p, q, r, ... : Predicates and relations" (The element r should use x, y, or z).

---

📄 **Per-File Summaries**

• CompPoly/Univariate/Basic.lean: This change expands the CPolynomial API by implementing fundamental polynomial properties and operations, including coefficients, degree, evaluation, an induction principle, and division.
• CompPoly/Univariate/Quotient.lean: Rename the distributivity lemmas for QuotientCPolynomial to mul_add and add_mul and update the corresponding Semiring instance.
• CompPoly/Univariate/README.md: Adds a README file documenting the univariate polynomial implementation, including its array-backed types, module structure, and integration with Mathlib.
• CompPoly/Univariate/Raw.lean: This update expands the CPolynomial.Raw API by adding basic coefficient-level lemmas, power properties, and the erase operation, while renaming distributivity theorems to follow standard Lean naming conventions.
• CompPoly/Univariate/ToPoly.lean: This update adds correctness theorems for several CPolynomial operations, proving they correspond to their Mathlib counterparts when converted via toPoly.

---

Last updated: 2026-02-13 15:29 UTC.

[dhsorens]

/review

External:

Internal:
CompPoly/Univariate/

Comments:
Please review and identify any possible issues or possible improvements. Be sure to address correctness and usability/ergonomics.

[github-actions]

🤖 AI Review (with external context)

🤖 AI Review

Overall Summary:
The pull request contains a critical soundness issue in Basic.lean, where the Nontrivial R assumption is incorrectly omitted from coeff_X and coeff_one, rendering them undefined for trivial rings where canonical forms do not exist. Additionally, ToPoly.lean relies on brittle, production-unsafe proof techniques, specifically the use of the exact? search tactic and references to auto-generated instance names (e.g., inst_1). These formalization errors and stability risks must be resolved before merging.

---

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

Based on the review of the provided diff for CompPoly/Univariate/Basic.lean, here are the findings.

The code generally implements polynomial operations and properties correctly, following a standard approach (e.g., Horner's method for induction, standard degree definitions). However, there is a Major misformalization issue regarding the use of omit [Nontrivial R] with definitions that fundamentally require the Nontrivial R instance.

1. Incorrect Assumption Handling in coeff_X and coeff_one (Major)

Issue:
The lemmas coeff_X and coeff_one are wrapped in omit [Nontrivial R] in, attempting to state these properties for a general Semiring (including trivial ones). However, the definitions of X and 1 (via the One instance) strictly depend on Nontrivial R.

• X: Defined as ⟨Raw.X, X_canonical⟩. Raw.X is usually #[0, 1]. For this to be canonical (trimmed), we must have 1 ≠ 0. If R is trivial, #[0, 1] becomes #[0, 0], which trims to #[]. Thus X_canonical (which asserts Trimmed #[0, 1]) cannot be proven without Nontrivial R. Consequently, X captures the Nontrivial R instance.
• 1: The One instance is defined as instance [Nontrivial R] : One ... and uses one_is_trimmed which also requires Nontrivial R.

Omitting Nontrivial R in coeff_X and coeff_one creates a context where X and 1 are either undefined or unelaborable. Even if the code compiles due to some artifact of the environment, the statements are semantically unsound for trivial rings where X and 1 as canonical forms #[0, 1] and #[1] do not exist.

Fix:
Remove omit [Nontrivial R] in for these specific lemmas. They hold fundamentally because the ring is nontrivial.

-- Remove 'omit [Nontrivial R] in'
/-- Coefficient of the variable `X`. -/
lemma coeff_X (i : ℕ) : coeff X i = if i = 1 then 1 else 0 := by
  simp only [X, coeff]; rw [Raw.coeff_X]

-- Remove 'omit [LawfulBEq R] [Nontrivial R] in' (keep LawfulBEq if needed/supported, but Nontrivial is required)
/-- Coefficient of the constant polynomial `1`. -/
lemma coeff_one (i : ℕ) :
    coeff (1 : CPolynomial R) i = if i = 0 then 1 else 0 := by
  simp only [coeff]
  change Raw.coeff 1 i = if i = 0 then 1 else 0
  rw [Raw.coeff_one]

2. Ambiguity in omit usage for C (Minor)

Observation:
coeff_C also uses omit [Nontrivial R]. Unlike X, C r is defined as (Raw.C r).trim. Since trim handles the zero case (returning #[] if r=0), C can be defined generally for any ring. Assuming Lean 4 correctly prunes the unused [Nontrivial R] variable from the definition of C, coeff_C is correct to omit it. If C captures the variable, this omit would also be problematic, but functionally C is valid in trivial rings.

3. Verdict

The formalization logic (induction, degree, operations) is correct. The off-by-one checks for tail, extract, and degree look correct. The primary issue is the misuse of omit for constants that don't exist in trivial rings.

Correctness: Incorrect (due to omit usage on X and 1).

Checklist Results:

• Off-by-One Errors: None found.
• Recursive Definitions: induction_on and tail logic are correct.
• Incorrect Assumptions: Yes, coeff_X and coeff_one incorrectly omit Nontrivial R.
• Prop vs Type: Correct.
• Universe Levels: Correct.

Recommended Changes

Apply the following patch to fix the assumption errors:

diff --git a/CompPoly/Univariate/Basic.lean b/CompPoly/Univariate/Basic.lean
index ...
--- a/CompPoly/Univariate/Basic.lean
+++ b/CompPoly/Univariate/Basic.lean
@@ -165,7 +165,7 @@
   rw [Trim.coeff_eq_coeff, Raw.coeff_C]
 
-/-- Coefficient of the variable `X`. -/
+-- Removed omit [Nontrivial R] as X depends on it
 lemma coeff_X (i : ℕ) : coeff X i = if i = 1 then 1 else 0 := by
   simp only [X, coeff]; rw [Raw.coeff_X]
 
@@ -179,7 +179,7 @@
 lemma coeff_zero (i : ℕ) : coeff (0 : CPolynomial R) i = 0 := by
   simp; rfl
 
-/-- Coefficient of the constant polynomial `1`. -/
+-- Removed omit [Nontrivial R] as 1 depends on it
 lemma coeff_one (i : ℕ) :
     coeff (1 : CPolynomial R) i = if i = 0 then 1 else 0 := by
   simp only [coeff]

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

The review of the changes in CompPoly/Univariate/Raw.lean reveals that the formalization is correct.

The changes primarily involve:

1. Refactoring and Cleanup: Updating the coeff signature to use the standard ring variable R instead of Q, and removing unnecessary namespace qualifications.
2. New Lemmas: Adding standard polynomial identities concerning coefficients (coeff_C, coeff_X, etc.), multiplication properties (C_mul_eq_smul_trim, X_mul_eq_mulX_trim), and powers (pow_succ, X_pow_eq_monomial_one).
3. New Definitions: Defining erase to remove a term from a polynomial.

Detailed Analysis:

• coeff Signature Update (Line 47): Changing (p : CPolynomial.Raw Q) to (p : CPolynomial.Raw R) fixes a likely inconsistency, aligning the function with the rest of the file which uses R as the base ring.
• Coefficient Lemmas (Lines 742+): The new lemmas coeff_C, coeff_X, coeff_zero, and coeff_one correctly characterize the coefficients of basic polynomials based on the underlying array implementations. For instance, C r is #[r], so coeff 0 is r and others are 0.
• Multiplication & Action Lemmas (Lines 1184+):
  • C_mul_eq_smul_trim correctly identifies that multiplying by a constant polynomial is equivalent to scalar multiplication followed by trimming (to maintain canonical form).
  • X_mul_eq_mulX_trim correctly relates multiplication by X to the mulX (shift) operation with trimming.
  • The lemmas regarding monomial and pow correctly bridge the gap between repeated multiplication and direct monomial construction.
• erase Definition (Line 1641): erase n p is defined as p - monomial n (p.coeff n). This correctly zeroes out the $n$-th coefficient using the sub operation, which handles the necessary arithmetic and trimming.
• sub_coeff (Line 1664): This lemma correctly derives the coefficient of a difference from the additivity of coefficients and the negation of coefficients.

No off-by-one errors, incorrect logical assumptions, or type misuses were found.

Verdict:
The formalization is correct.

-- No corrections required.

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

Based on the review of the changes in CompPoly/Univariate/ToPoly.lean, here is the assessment:

Verdict: Incorrect / Incomplete Formalization

The code contains development artifacts (exact?) and brittle proof techniques that are not suitable for a stable codebase, despite the fact that they compile.

Issues Found:

1. Unfinished Proof (exact?):
   In erase_toPoly, the tactic exact? is used. This is a "search" tactic intended for interactive development to find a lemma from the library. It relies on the current state of the environment and caches, making the proof potentially slow or fragile. It should be replaced by the explicit lemma it discovers (likely Raw.toPoly_add or a property of eval₂).

2. Variable Shadowing:
   In erase_toPoly, the hypothesis h_erase_toPoly is defined, and then immediately redefined inside its own proof block:

   have h_erase_toPoly : ... := by
     intros p q;
     have h_erase_toPoly : ... := by ... -- Shadowing happens here

   This is confusing and poor style.

3. Brittle Proof Script:
   In X_toPoly, the proof uses (expose_names; exact inst_1).
   Referencing an auto-generated name like inst_1 is highly brittle. If the type class resolution order changes or a new instance is added to the context in the future, inst_1 may refer to something else, breaking the proof.

Recommended Fixes:

Below is the corrected code for the affected sections.

Fix for erase_toPoly:
Replace exact? with the appropriate lemma (assuming toPoly is built on eval₂ which is a homomorphism, or simply using simp if toPoly definitions allow) and rename the inner hypothesis.

theorem erase_toPoly [LawfulBEq R] [DecidableEq R] (n : ℕ) (p : CPolynomial R) :
    (erase n p).toPoly = p.toPoly.erase n := by
  have h_erase_def : (CompPoly.CPolynomial.erase n p).toPoly
      = p.toPoly - Polynomial.monomial n (p.val.coeff n) := by
    -- Rename inner hypothesis to avoid shadowing
    have h_sub_toPoly : ∀ (p q : CompPoly.CPolynomial.Raw R),
        (p - q).toPoly = p.toPoly - q.toPoly := by
      intros p q
      -- Assuming toPoly is defined via eval₂ or similar hom, 
      -- simp usually handles this if definitions are unfolded.
      -- If exact? found a lemma, it is likely related to eval₂_sub or map_sub.
      simp [Raw.toPoly, Raw.sub_def] -- Adjust tactics based on library definitions
      -- OR if a specific lemma exists: apply Raw.toPoly_sub
    convert h_sub_toPoly _ _
    convert monomial_toPoly n (p.val.coeff n) |> Eq.symm
  convert h_erase_def using 1
  ext m
  simp [Polynomial.coeff_monomial]
  by_cases h : n = m <;> simp [h]
  · rw [eq_comm, sub_eq_zero]
    convert Raw.coeff_toPoly using 1
    exact Eq.symm Array.getD_eq_getD_getElem?
  · rw [Polynomial.coeff_erase]; aesop

Fix for X_toPoly:
Replace the manual instance reference with infer_instance or proper context management.

theorem X_toPoly [LawfulBEq R] [Nontrivial R] :
    (X : CPolynomial R).toPoly = Polynomial.X := by
  convert Raw.toPoly_X using 1
  infer_instance -- Correctly infers Nontrivial R if that is what inst_1 was

[dhsorens]

The bot's feedback on assumptions is wrong, as the proofs compile with the omit ... tags; it made good points on the proof quality

[dhsorens]

This PR is done for now, still some API work to be done from the roadmap but for now all the key theorems and lemmas are proved, and the key API functions on canonical polynomials defined. TODO next on this is to refactor the raw polynomials for more readability, etc.

merging