feat: implements issue #50 #51, Implement variable and degree utilities: …

[FawadHa1der]

the new degrees implementation could be slower since its using degreesOf implementation repeatedly, but trying to stay close to the ticket description.

the other implementation could be

def degrees {n : ℕ} {R : Type} [Zero R] (p : CMvPolynomial n R) : Multiset (Fin n) :=
Finset.sup (List.toFinset (List.map CMvMonomial.toFinsupp (Lawful.monomials p)))
Finsupp.toMultiset

[github-actions]

🤖 Gemini PR Summary

This Pull Request implements variable and degree utility functions for the CMvPolynomial type, addressing issues #50 and #51. The changes introduce fundamental properties and restriction operations necessary for more advanced multivariate polynomial manipulation.

Features

• Variable & Degree Utilities: Implemented degrees and vars functions for CMvPolynomial to track monomial exponents and active variables.
• Degree Restriction: Added functionality to restrict polynomials based on specific monomial degree constraints.
• Property Verification: Introduced a suite of foundational properties and correctness lemmas in CMvPolynomialLemmas.lean covering evaluation, variable tracking, and degree-restriction operations.

Refactoring

• Lemma Consolidation: Deleted CMvPolynomialEvalLemmas.lean and migrated/expanded its contents into the renamed CMvPolynomialLemmas.lean to provide a more comprehensive entry point for polynomial proofs.
• Namespace/Import Cleanup: Updated CompPoly.lean to reflect the updated file structure and naming conventions.
• Implementation Note: The degrees function was implemented using a repeated degreesOf approach to align with the ticket specification. While the author noted a potential performance trade-off compared to a Finsupp.toMultiset approach, the current implementation prioritizes spec-compliance.

Documentation

• The PR body includes technical notes regarding alternative implementation strategies for the degrees utility for future optimization considerations.

---

Analysis of Changes

Metric	Count
📝 Files Changed	4
✅ Lines Added	356
❌ Lines Removed	45

---

sorry Tracking

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

• def vars {n : ℕ} {R : Type} [Zero R] (p : CMvPolynomial n R) : Finset (Fin n) in CompPoly/Multivariate/CMvPolynomial.lean
• def restrictDegree {n : ℕ} {R : Type} [BEq R] [LawfulBEq R] [Zero R] in CompPoly/Multivariate/CMvPolynomial.lean
• def degrees {n : ℕ} {R : Type} [Zero R] (p : CMvPolynomial n R) : Multiset (Fin n) in CompPoly/Multivariate/CMvPolynomial.lean

---

🎨 **Style Guide Adherence**

Based on the provided style guide, the following lines violate the guidelines:

CompPoly/Multivariate/CMvPolynomial.lean

• Lines 131, 135, 183, 192, 196, 216, 221: CMvPolynomial, CMvMonomial
  • Rule: "Acronyms: Treat as words (e.g., HtmlParser not HTMLParser)." (Should be CmvPolynomial, CmvMonomial).
• Lines 131, 135, 183, 192, 196, 216, 221: {R : Type}, [Zero R]
  • Rule: "Variable Conventions: α, β, γ, ... : Generic types."
• Line 132: (fun s => Finsupp.sum s (fun _ e => e))
  • Rule: "Functions: Prefer fun x ↦ ... over λ x, ...."
  • Rule: "Variable Conventions: s, t, ... : Sets or Lists." (s is used here for a Finsupp element).
• Lines 135, 137, 184, 186, 193, 198: (i : Fin n)
  • Rule: "Variable Conventions: i, j, k, ... : Integers." (Indices of Fin n are natural numbers and should follow m, n, k).
• Lines 138, 184, 186, 193: fun p =>, fun i =>
  • Rule: "Functions: Prefer fun x ↦ ... over λ x, ...."
• Lines 138, 183, 192, 198: (p : CMvPolynomial n R)
  • Rule: "Variable Conventions: p, q, r, ... : Predicates and relations." (Terms/Elements should be x, y, z).
• Line 196: lemma degreeOf_eq_count_degrees {n : ℕ} {R : Type} [Zero R]
  • Rule: "Documentation Standards: Every definition and major theorem should have a docstring."
• Line 216: def restrictBy {n : ℕ} {R : Type} [BEq R] [LawfulBEq R] [Zero R]
  • Rule: "Documentation Standards: Every definition and major theorem should have a docstring."
• Line 217: (keep : CMvMonomial n → Prop)
  • Rule: "Variable Conventions: p, q, r, ... : Predicates and relations."
• Line 221: def restrictTotalDegree {n : ℕ} {R : Type} [BEq R] [LawfulBEq R] [Zero R]
  • Rule: "Documentation Standards: Every definition and major theorem should have a docstring."
• Line 222: (d : ℕ)
  • Rule: "Variable Conventions: m, n, k, ... : Natural numbers."

CompPoly/Multivariate/CMvPolynomialLemmas.lean

• Line 22: variable {n : ℕ} {R : Type}
  • Rule: "Variable Conventions: α, β, γ, ... : Generic types."
• Line 23: variable (vals : Fin n → R)
  • Rule: "Variable Conventions: x, y, z, ... : Elements of a generic type."
• Line 27, 44, 49, 56: (p q : CMvPolynomial n R)
  • Rule: "Variable Conventions: p, q, r, ... : Predicates and relations."
• Line 44, 69: (i : Fin n)
  • Rule: "Variable Conventions: i, j, k, ... : Integers."
• Line 115, 125, 130: (m : CMvMonomial n)
  • Rule: "Variable Conventions: m, n, k, ... : Natural numbers."
• Line 125, 130, 152, 203: (d : ℕ)
  • Rule: "Variable Conventions: m, n, k, ... : Natural numbers."
• Line 132: change ((Std.ExtTreeMap.filter (fun _ c => c != (0 : R)) (Std.ExtTreeMap.filter (fun m' _ => decide (keep m')) p.1))[m]?.getD 0) = if keep m then p.1[m]?.getD 0 else 0
  • Rule: "Line Length: Keep lines under 100 characters."
• Line 240: have hfin_get : (∑ x : Fin (List.ofFn s).length, s ⟨x.1, by simpa [List.length_ofFn] using x.2⟩) = (List.ofFn s).sum := by
  • Rule: "Line Length: Keep lines under 100 characters."

---

📄 **Per-File Summaries**

• CompPoly.lean: Updates the import statement to reflect the renaming of CMvPolynomialEvalLemmas to CMvPolynomialLemmas.
• CompPoly/Multivariate/CMvPolynomial.lean: This update implements variable and degree properties (degrees, vars) and adds functionality to restrict polynomials based on monomial degree constraints.
• CompPoly/Multivariate/CMvPolynomialEvalLemmas.lean: Delete the CompPoly/Multivariate/CMvPolynomialEvalLemmas.lean file, which contained simplification and automation lemmas for multivariate polynomial evaluation.
• CompPoly/Multivariate/CMvPolynomialLemmas.lean: Provides foundational properties and correctness lemmas for CMvPolynomial evaluation, variables, degrees, and degree-restriction operations.

---

Last updated: 2026-02-11 21:18 UTC.

[dhsorens]

Nice, thank you for this @FawadHa1der !! This looks very good to me. The typeclass change [CommSemiring R] to [Zero R] makes it more general, which is always welcome! :)

To avoid having too many "lemmas" files could we merge CMvPolynomialEvalLemmas.lean and CMvPolynomialVarsDegreesLemmas.lean into one file -- e.g. CMvPolynomialLemmas.lean -- for correctness lemmas and for the simp/grind set? It also might be worth marking mem_vars_iff_degreeOf_pos, degrees_zero, vars_zero, and degreeOf_zero with @[simp]. Mathlib also has a lemma degrees_one : degrees (1 : MvPolynomial σ R) = 0 that is marked with @[simp] - if it's easy to add, that would be nice (I can add it later, too).

And lastly re ticket guidelines - I would say on these tickets, treat them as guidelines but we are open to improvements to them, as long as they are computable and especially if they are more efficient/elegant! If there's a good reason for deviating from the ticket, am always open to it. In this case, I am happy with the alternative you suggest (I think it slightly matches mathlib better too):

def degrees {n : ℕ} {R : Type} [Zero R] (p : CMvPolynomial n R) : Multiset (Fin n) :=
    Finset.sup (List.toFinset (List.map CMvMonomial.toFinsupp (Lawful.monomials p))) Finsupp.toMultiset

I'll also request the review of @Julek on this one since he has an interest in the multivariate polynomial implementation here

[FawadHa1der]

Done, feedback incorporated. Please do check the application of the grind attribute. I understand the simp but not entirely clear on the application of grind.
I am also adding the restrictDegree and restrictDegrees implementation here.

Thanks for answering my simplistic questions since I am relatively new to Lean but this should improve over time.

[dhsorens]

no worries! This looks good to me, I'll give @Julek a few more days to review and okay before I merge. The simp/grind application looks good to me for now; building the right grind-set will probably be something that we do as we use these lemmas in the wild. There's a balance of adding enough to simplify proofs without adding so many that the tactic becomes slow.

thanks! I'll close #50 and #51 now

[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 is approved as logically correct, successfully refactoring the library structure and rigorously implementing new functionality for polynomial degrees, variable sets, and restriction filtering. The formalization effectively bridges computable representations with Mathlib's abstract theory, ensuring operations like evaluation are sound. A minor stylistic note for future improvements is to adopt universe polymorphism (Type u) rather than the current restriction to Type 0.

---

📄 **Review for `CompPoly.lean`**

Implementation Analysis

Hunk 1: Lines 7-13

 import CompPoly.Multivariate.CMvMonomial
 import CompPoly.Multivariate.CMvPolynomial
-import CompPoly.Multivariate.CMvPolynomialEvalLemmas
+import CompPoly.Multivariate.CMvPolynomialLemmas
 import CompPoly.Multivariate.Lawful
 import CompPoly.Multivariate.MvPolyEquiv
 import CompPoly.Multivariate.Unlawful

• Analysis: The import statement is updated from CompPoly.Multivariate.CMvPolynomialEvalLemmas to CompPoly.Multivariate.CMvPolynomialLemmas.
• Context: This file appears to be a "barrel" or facade file, aggregating imports for the library CompPoly.
• Logic: This change implies a refactoring in the library structure where CMvPolynomialEvalLemmas has either been renamed to CMvPolynomialLemmas (suggesting a broader scope of lemmas) or subsumed by it.
• Correctness: Since the instructions state the code compiles, the new module CompPoly.Multivariate.CMvPolynomialLemmas resolves correctly. This is a structural change consistent with library maintenance (renaming or grouping modules).

Misformalization Checklist

• Off-by-One Errors: N/A (Import change only).
• Recursive Definitions: N/A.
• Incorrect Assumptions/Side-Conditions: N/A.
• Prop vs. Type: N/A.
• Universe Levels: N/A.

Verdict & Feedback

Verdict: Correct

The change is a straightforward update to the module dependency graph. As the code compiles, the new import path is valid. This change indicates a refactor of the underlying file structure (likely renaming EvalLemmas to Lemmas to accommodate a wider range of theorems), which is syntactically and semantically safe for this aggregation file.

No changes are required.

📄 **Review for `CompPoly/Multivariate/CMvPolynomial.lean`**

This review focuses on the changes in CompPoly/Multivariate/CMvPolynomial.lean.

Verdict: The formalization is Correct. The changes are logically sound, consistent with the documentation, and adhere to standard patterns for polynomial libraries in Lean (e.g., behaving similarly to Mathlib.MvPolynomial).

The following points detail the review findings:

1. Typeclass Relaxation for degreeOf

• Change: [CommSemiring R] $\to$ [Zero R].
• Assessment: Correct.
• Reasoning: The definition of degreeOf relies on Lawful.monomials, List.map, and Finset.sup. Determining the support of a polynomial and the exponents of its monomials only requires knowing which coefficients are non-zero. It does not require multiplication or addition structure on R. This generalization makes the function applicable in more contexts.

2. Definition of degrees and vars

• Implementation:
  • degrees: $\sum_{i \in \text{univ}} \text{replicate}(p.\text{degreeOf } i, i)$
  • vars: ${ i \mid 0 < p.\text{degreeOf } i }$
• Assessment: Correct.
• Reasoning:
  • The definition of degrees explicitly constructs a multiset where the multiplicity of variable i equals its maximum degree in the polynomial (degreeOf i). This is consistent with the standard behavior of MvPolynomial.degrees in Mathlib.
  • The lemma degreeOf_eq_count_degrees correctly proves the relationship between degreeOf and degrees, verifying the definition's intent.
  • vars correctly identifies variables that have a non-zero degree in the polynomial, serving as the support of the degrees multiset.

3. Restriction Functions (restrictBy, restrictTotalDegree, restrictDegree)

• Implementation: Filtering the underlying monomial structure based on decidable predicates.
• Assessment: Correct.
• Reasoning:
  • Logic: restrictBy filters the underlying list of monomials (p.1). By taking a predicate keep : CMvMonomial n → Prop, it correctly retains only those terms satisfying the condition.
  • Decidability: restrictDegree uses the predicate fun m => ∀ i : Fin n, m.degreeOf i ≤ d. Since Fin n is a Fintype, the universal quantifier is decidable, allowing the use of decide within the filter function.
  • Semantics: restrictDegree correctly implements "Filter out ... > d" by keeping "... $\le$ d".

4. Minor Observation: Universe Polymorphism

• Issue: The definitions use {R : Type} explicitly (implying Type 0), rather than {R : Type u}.
• Severity: Minor / Stylistic.
• Note: While this restricts the library to types in the lowest universe, this pattern appears consistent with the existing code in the file (visible in the context). It is not a bug introduced by this PR, but adopting Type u or Type* is generally preferred for library code.

Summary

The code correctly formalizes the concepts of polynomial degrees, variable sets, and filtering by degree bounds. No logic errors, off-by-one errors, or incorrect assumptions were found.

📄 **Review for `CompPoly/Multivariate/CMvPolynomialEvalLemmas.lean`**

This PR deletes the file CompPoly/Multivariate/CMvPolynomialEvalLemmas.lean. As the code has been confirmed to compile, the deletion does not break build dependencies.

However, from a formalization perspective, I have reviewed the code being removed to identify why it might have been deleted or if its removal leaves a gap in the library's reasoning capabilities.

Verdict

Correct (The deletion is valid).
Note: The code being deleted contained formalization issues (Universe restrictions) which justify its removal or rewrite.

Impact Analysis of Deletion

The deletion removes the @[simp] and [grind] lemmas eval_add and eval_mul.

• Risk: These lemmas establish that CMvPolynomial.eval is a ring homomorphism (respects addition and multiplication). Removing them will likely disable proof automation (simp) for expressions like (p + q).eval vals.
• Recommendation: Ensure these lemmas are proven elsewhere (e.g., in MvPolyEquiv) or that CMvPolynomial is being deprecated in favor of a type where these properties are automatic.

Retrospective Review of Deleted Code

Upon reviewing the content of the file being deleted, I identified specific misformalization issues. These defects may explain why the file is being removed.

1. Universe Levels (Restrictive)

• Issue: The line variable {n : ℕ} {R : Type} restricts the ring R to Type 0.
• Misformalization: This prevents the lemmas from being used with rings in other universes (e.g., Type u), which is standard practice in Lean libraries.
• Correct Approach (for future reference):

  variable {n : ℕ} {R : Type u} -- Use universe polymorphism

2. Typeclass Assumptions (Potentially Too Strong)

• Issue: The variables include [BEq R] [LawfulBEq R].
• Misformalization: While CMvPolynomial (computable polynomials) likely requires BEq for operations like addition (to merge monomials), the mathematical statement of evaluation commutativity eval (p + q) = eval p + eval q typically holds in the logic without requiring decidable equality, provided the evaluation function is defined. Standard MvPolynomial does not require DecidableEq for eval.
• Implication: The deleted lemmas imposed stricter conditions on the ring R than mathematically necessary for the property being stated.

Summary

The deletion is technically correct. The removal is likely positive as the deleted code was restricted to Type 0 and carried strong assumptions. Ensure the homomorphism properties of eval are preserved in the remaining codebase to maintain automation.

📄 **Review for `CompPoly/Multivariate/CMvPolynomialLemmas.lean`**

Here is the review of the changes in CompPoly/Multivariate/CMvPolynomialLemmas.lean.

Verdict

Correct.
The implementation of the lemmas for CMvPolynomial (computable multivariate polynomials) is logically sound and correctly bridges the gap between the computable representation and the abstract MvPolynomial theory found in Mathlib.

Analysis

1. Logic and Correctness:

   • Evaluation: The eval_add and eval_mul lemmas correctly utilize the eval_equiv property, relying on the homomorphism properties of fromCMvPolynomial.
   • Variables and Degrees: The connections between CMvPolynomial.vars, degreeOf, and their MvPolynomial counterparts (vars_equiv, degrees_equiv) are rigorously proven using ext and congruence lemmas.
   • Restriction: The restriction lemmas (restrictBy, restrictTotalDegree, restrictDegree) correctly define the coefficient behavior (zeroing out terms that do not satisfy the predicate). The proofs for the interactions of these restrictions (e.g., commutativity, idempotence with min) are exhaustive and handle the logic correctly.
   • Sums: The private helpers converting between List/Vector sums and Finset.sum are correct and necessary for relating internal representations to MvPolynomial definitions.

2. Implementation Details:

   • The code interacts with an underlying tree map implementation (via Std.ExtTreeMap and Lawful namespace). The usage of Lawful.monomials and Lawful.fromUnlawful appears consistent with the expected behavior of a verified data structure.
   • The use of decide (keep m) inside restrictBy correctly leverages the [DecidablePred keep] instance, which is standard for computable definitions.

3. Checklist Assessment:

   • Off-by-One Errors: None found.
   • Recursive Definitions: N/A (mostly lemmas about existing definitions).
   • Assumptions: The type class assumptions [CommSemiring R], [BEq R], [LawfulBEq R] are appropriate for the computable setting.
   • Prop vs Type: Prop and Bool are handled correctly, specifically in coeff_restrictBy.

Suggestions (Minor)

Universe Polymorphism:
The file declares variables with R : Type.

variable {n : ℕ} {R : Type} ...

In formal library design (like Mathlib), it is standard practice to use universe polymorphism (R : Type u) to allow the algebraic structures to reside in any universe level. Unless CompPoly is strictly restricted to Type 0 by design or by its dependencies (e.g., if CMvPolynomial is not universe polymorphic), consider generalizing this to:

variable {n : ℕ} {R : Type u} ...

Conclusion:
The file is approved. The formalization is correct and robust.