Operations on Univariant Polynomials

[dhsorens]

This PR shows that the following operations on UniPoly descend into the quotient, QuotientUniPoly:

• smul
• nsmul
• mulPowX
• mulX
• mul
• pow

[github-actions]

🤖 Gemini PR Summary

This diff primarily enhances the formalization of univariate polynomials in Lean, focusing on defining algebraic operations on a quotient type.

Here is a summary of the key changes:

• Lifting Operations to the Quotient Type: The main goal of this change is to define standard polynomial operations (smul, nsmul, mul, pow, mulPowX) on the QuotientCPolynomial type. This type treats polynomials as equivalent if they only differ by trailing zeros.

• New Equivalence Lemmas: A large section of new lemmas is added to prove that the polynomial operations respect this equivalence relation. This is a crucial prerequisite for defining the operations on the quotient type. Key proofs show that addition and multiplication of equivalent polynomials result in equivalent polynomials.

• Proof Completion and Refinements:

  • The proof for add_coeff (calculating the coefficient of a sum) is completed, filling a previous sorry.
  • Several new helper lemmas are introduced to reason about coefficients after operations like scalar multiplication and list concatenation.
  • Some induction tactics were renamed for better clarity (e.g., last_none_zero_elim to last_nonzero_induct).

• File System Metadata: A macOS .DS_Store file was added to the repository, which is a non-functional change.

---

Analysis of Changes

Metric	Count
📝 Files Changed	2
✅ Lines Added	367
❌ Lines Removed	6

---

sorry Tracking

• ✅ Removed: 1 sorry(s)
  • theorem add_coeff {p q : CPolynomial Q} {i : ℕ} (hi : i < (add_raw p q).size) : in CompPoly/Univariate/Basic.lean
• ❌ Added: 1 sorry(s)
  • lemma mul_comm_equiv [LawfulBEq R] (a b : CPolynomial R) : in CompPoly/Univariate/Basic.lean

---

Last updated: 2026-01-05 10:24 UTC. See the main CI run for build status.

[github-actions]

🤖 Gemini PR Summary

Hello,

This PR extends the functionality of univariate quotient polynomials (QuotientUniPoly) by implementing several key algebraic operations. By proving that these operations on UniPoly respect the underlying polynomial equivalence relation, they have been successfully descended into the quotient.

Features

• Algebraic Operations on QuotientUniPoly: Implemented several core operations for quotient polynomials, ensuring they are well-defined:
  • Multiplication: Added support for standard multiplication (mul), as well as specific cases like multiplication by $X$ (mulX) and multiplication by powers of $X$ (mulPowX).
  • Scalar Multiplication: Enabled both standard scalar multiplication (smul) and natural number scalar multiplication (nsmul).
  • Exponentiation: Implemented the power operator (pow).

Fixes

• None.

Refactoring

• None.

Documentation

• None.

---

Analysis of Changes

Metric	Count
📝 Files Changed	1
✅ Lines Added	346
❌ Lines Removed	2

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📄 **Per-File Summaries**

• CompPoly/Univariate/Basic.lean: Implemented scalar multiplication, multiplication, and exponentiation for quotient polynomials by proving these operations respect polynomial equivalence.

---

Last updated: 2026-01-08 10:34 UTC.

[dhsorens]

sorrys have been eliminated. now I will clean up, rebase, etc.

[github-actions]

🤖 AI Review (with external context)

🤖 AI Review

Overall Summary:
The pull request correctly implements and formalizes the quotient structure for CPolynomial, rigorously proving that arithmetic operations descend soundly based on coefficient equivalence. While the logic and induction principle updates are robust, smul_equiv and nsmul_raw_equiv should be changed from def to lemma to align with standard Lean conventions for Prop-valued declarations.

---

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

This review covers the changes in CompPoly/Univariate/Basic.lean. The code has been reviewed for logical correctness, consistency with the provided context, and formalization best practices.

Verdict: Correct

The changes correctly implement the induction principle updates, the new coefficient lemmas, and the quotient structure for CPolynomial. The logic supporting the descent of arithmetic operations to the quotient is sound.

Detailed Analysis

1. Induction Principle Updates
The changes from last_none_zero_elim to last_nonzero_induct and Trim.elim to induct (lines 137, 157) align with the theorem definitions provided in the file content. This ensures the correct induction principles are utilized.

2. Coefficient Lemmas (concat_coeff, smul_equiv, mulPowX_equiv)

• concat_coeff₁ & concat_coeff₂: The indexing logic correctly handles the concatenation of arrays. concat_coeff₂ correctly computes the offset index i - p.size for the second array.
• smul_equiv & nsmul_raw_equiv: These correctly characterize scalar multiplication in terms of coefficients. The use of def instead of lemma for these Prop-valued declarations is stylistically non-standard but semantically valid and compiles correctly.
• mulPowX_equiv₁ & mulPowX_equiv₂: The logic for mulPowX (multiplication by $X^i$) is correct. It correctly identifies that coefficients with index j < i are zero (padding) and coefficients j ≥ i correspond to the shifted polynomial.

3. QuotientCPolynomial Formalization

• Equivalence Relation: equiv is defined as equality of all coefficients (∀ i, p.coeff i = q.coeff i), which is the correct setoid relation for polynomials represented by arrays with potential trailing zeros.
• Operation Descent: The file rigorously proves that operations (add, smul, neg, sub, mul, pow) respect this equivalence relation.
  • Addition: Relies on coefficient-wise addition, which trivially respects equivalence.
  • Multiplication: The proof correctly decomposes multiplication into mul_steps and uses induction on the list of coefficients (via foldl) to show that equivalent operands yield equivalent results (mul_equiv, mul_equiv₂).
  • Exponentiation: pow is defined via iterated multiplication. The proof pow_descends correctly utilizes mul_pow_assoc (iterated function application) and the congruence of multiplication.
• Lifting: The use of Quotient.lift and Quotient.lift₂ is applied correctly with the corresponding proofs of well-definedness (_descends lemmas).

Minor Stylistic Note

• Definition vs Lemma: smul_equiv (line 606) and nsmul_raw_equiv (line 612) are defined using def but return a Prop. In Lean 4, it is standard practice to use lemma or theorem for Prop-valued terms to avoid unnecessary code generation overhead and for clarity, though this does not affect correctness.

[alexanderlhicks]

(fixed the review bot)

[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 changes to CompPoly/Univariate/Basic.lean correctly formalize the QuotientCPolynomial type, successfully lifting arithmetic operations while rigorously respecting the equivalence relation for trailing zeros. The underlying index arithmetic and helper lemmas supporting these lifts are logically sound, with no off-by-one errors or recursion issues detected. While minor stylistic suggestions regarding lemma vs def usage were noted, the implementation is verified as correct and ready to merge.

---

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

This is a rigorous review of the changes in CompPoly/Univariate/Basic.lean.

Verdict

Correct.

The changes correctly formalize the QuotientCPolynomial type and lift the polynomial operations (add, smul, mul, pow, etc.) from CPolynomial. The logic respects the equivalence relation (invariance under trailing zeros), and the helper lemmas in the EquivalenceLemmas section provide the necessary arithmetic properties to justify these lifts.

Analysis of Changes

1. Helper Lemmas (concat_coeff, smul_equiv, mulPowX_equiv):

   • The index arithmetic for concatenated arrays (representing $p \cdot X^i$) is correct. concat_coeff₂ correctly maps indices $j \ge i$ in the result to $j-i$ in the original polynomial, and concat_coeff₁ correctly handles the zero-padding.
   • smul_equiv and nsmul_raw_equiv correctly characterize scalar multiplication properties, even in cases where trimming occurs (e.g., if a scalar annihilates the leading coefficient, both sides of the equality become 0).

2. Equivalence Properties:

   • add_equiv, mulPowX_equiv, and smul_equiv correctly establish that the basic building blocks of polynomial arithmetic preserve the quotient equivalence relation.
   • mul_equiv and mul_equiv₂ correctly prove that polynomial multiplication is well-defined on the quotient. The decomposition of multiplication into mul_step and foldl is logically sound, utilizing the distributivity of multiplication over addition.

3. Lifting Operations:

   • The Quotient.lift definitions for add, smul, mul, and pow are correctly guarded by their respective _descends lemmas.
   • The recursive definition of pow and its descending proof using mul_pow_succ handle the inductive step correctly.

4. Style & Minor Observations:

   • Definition types: Several properties (e.g., smul_equiv, nsmul_raw_equiv) are declared with def rather than lemma or theorem. While valid in Lean 4 (as they return Prop), using lemma is standard for properties to ensure proof irrelevance in all contexts. This does not affect correctness.
   • Redundancy: mulPowX_descends re-proves the equivalence preservation that was already established in mulPowX_equiv (inside QuotientCPolynomial). It could be simplified by applying Quotient.sound (mulPowX_equiv ...) directly, but the manual proof provided is correct.

Misformalization Checklist Results

• Off-by-One Errors: None found. Array indexing in concat_coeff and mulPowX logic is precise.
• Recursive Definitions: pow and foldl recursions are standard and terminate.
• Incorrect Assumptions: LawfulBEq is correctly required for operations involving coefficient trimming checks.
• Prop vs Type: Usage is correct.

The code is verified as a correct formalization of univariate polynomial quotient arithmetic.

[dhsorens]

This PR doesn't make many changes, doesn't introduce any sorrys, and extends work previously reviewed and merged. After the review bot suggestions, I think this is fine to merge. Can be easily undone if anyone has objections later on @alexanderlhicks @quangvdao