From 5a128055c9a14b9e5c757060c2d0f7fb36f27ff9 Mon Sep 17 00:00:00 2001 From: Dimitris Date: Tue, 24 Feb 2026 19:14:04 +0200 Subject: [PATCH 1/2] feat: circular dependency fix for CMvPolynomial and MvPolyEquiv chore: fixed wrong imports and erroneous proofs chore: cleaned up documentation chore: elaborated comments and some proof variations chore: comments and authorship chore: rename files according to PR review guidelines feat: created a new file Operations for extended poly ops fix: restrict functions were re-added --- CompPoly.lean | 1 + CompPoly/Multivariate/CMvPolynomial.lean | 145 ++++------------------- CompPoly/Multivariate/MvPolyEquiv.lean | 38 +++++- CompPoly/Multivariate/Operations.lean | 123 +++++++++++++++++++ CompPoly/Multivariate/Rename.lean | 2 +- CompPoly/Multivariate/Restrict.lean | 2 +- 6 files changed, 186 insertions(+), 125 deletions(-) create mode 100644 CompPoly/Multivariate/Operations.lean diff --git a/CompPoly.lean b/CompPoly.lean index 95805bd..a7caf97 100644 --- a/CompPoly.lean +++ b/CompPoly.lean @@ -12,6 +12,7 @@ import CompPoly.Multilinear.Basic import CompPoly.Multilinear.Equiv import CompPoly.Multivariate.CMvMonomial import CompPoly.Multivariate.CMvPolynomial +import CompPoly.Multivariate.Operations import CompPoly.Multivariate.CMvPolynomialEvalLemmas import CompPoly.Multivariate.Restrict import CompPoly.Multivariate.VarsDegrees diff --git a/CompPoly/Multivariate/CMvPolynomial.lean b/CompPoly/Multivariate/CMvPolynomial.lean index 7b7e14a..4f3fae3 100644 --- a/CompPoly/Multivariate/CMvPolynomial.lean +++ b/CompPoly/Multivariate/CMvPolynomial.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2025 CompPoly. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Frantisek Silvasi, Julian Sutherland, Andrei Burdușa, Derek Sorensen +Authors: Frantisek Silvasi, Julian Sutherland, Andrei Burdușa, Derek Sorensen, Dimitris Mitsios -/ import CompPoly.Multivariate.Lawful import CompPoly.Univariate.Basic @@ -17,10 +17,22 @@ and `mᵢ` is a `CMvMonomial`. This is implemented as a wrapper around `CPoly.Lawful`, which ensures that all stored coefficients are non-zero. +This file contains the core type definition and basic operations. Higher-level definitions +that depend on ring instances (monomial orders, `rename`, `aeval`, etc.) are in +`CMvPolynomial.lean`. The `CommSemiring` and `CommRing` instances are in `MvPolyEquiv.lean`. + ## Main definitions * `CPoly.CMvPolynomial n R`: The type of multivariate polynomials in `n` variables with coefficients in `R`. +* `CPoly.CMvPolynomial.C`: Constant polynomial constructor. +* `CPoly.CMvPolynomial.X`: Variable polynomial constructor. +* `CPoly.CMvPolynomial.monomial`: Monomial constructor. +* `CPoly.CMvPolynomial.coeff`: Extract the coefficient of a monomial. +* `CPoly.CMvPolynomial.eval₂`, `CPoly.CMvPolynomial.eval`: Polynomial evaluation. +* `CPoly.CMvPolynomial.support`, `CPoly.CMvPolynomial.totalDegree`, + `CPoly.CMvPolynomial.degreeOf`, `CPoly.CMvPolynomial.degrees`, + `CPoly.CMvPolynomial.vars`: Degree and support queries. -/ namespace CPoly @@ -145,39 +157,6 @@ def monomial {n : ℕ} {R : Type} [BEq R] [LawfulBEq R] [Zero R] (m : CMvMonomial n) (c : R) : CMvPolynomial n R := if c == 0 then 0 else Lawful.fromUnlawful <| Unlawful.ofList [(m, c)] -/-- Monomial ordering typeclass for `n` variables. - - Provides a way to compare monomials for determining leading terms. --/ -class MonomialOrder (n : ℕ) where - compare : CMvMonomial n → CMvMonomial n → Ordering - -- TODO: Add ordering axioms (transitivity, etc.) - -/-- Degree of a monomial according to a monomial order. - - Returns the degree of a monomial as determined by the ordering. - The exact meaning depends on the specific monomial order implementation - (e.g., total degree for graded orders, weighted degree, etc.). --/ -def MonomialOrder.degree {n : ℕ} [MonomialOrder n] (m : CMvMonomial n) : ℕ := - sorry - -/-- Leading monomial of a polynomial according to a monomial order. - - Returns `none` for the zero polynomial. --/ -def leadingMonomial {n : ℕ} {R : Type} [Zero R] [MonomialOrder n] - (p : CMvPolynomial n R) : Option (CMvMonomial n) := - sorry - -/-- Leading coefficient of a polynomial according to a monomial order. - - Returns `0` for the zero polynomial. --/ -def leadingCoeff {n : ℕ} {R : Type} [Zero R] [MonomialOrder n] - (p : CMvPolynomial n R) : R := - sorry - /-- Multiset of all variable degrees appearing in the polynomial. Each variable `i` appears `degreeOf i p` times in the multiset. @@ -185,13 +164,6 @@ def leadingCoeff {n : ℕ} {R : Type} [Zero R] [MonomialOrder n] def degrees {n : ℕ} {R : Type} [Zero R] (p : CMvPolynomial n R) : Multiset (Fin n) := Finset.univ.sum fun i => Multiset.replicate (p.degreeOf i) i -/-- Extract the set of variables that appear in a polynomial. - - Returns the set of variable indices `i : Fin n` such that `degreeOf i p > 0`. --/ -def vars {n : ℕ} {R : Type} [Zero R] (p : CMvPolynomial n R) : Finset (Fin n) := - Finset.univ.filter fun i => 0 < p.degreeOf i - /-- `degreeOf` is the multiplicity of a variable in `degrees`. -/ lemma degreeOf_eq_count_degrees {n : ℕ} {R : Type} [Zero R] (i : Fin n) (p : CMvPolynomial n R) : @@ -210,15 +182,23 @@ lemma degreeOf_eq_count_degrees {n : ℕ} {R : Type} [Zero R] _ = p.degreeOf i := by simp -/-- Restrict polynomial to monomials with total degree ≤ d. +/-- Extract the set of variables that appear in a polynomial. - Filters out all monomials where `m.totalDegree > d`. + Returns the set of variable indices `i : Fin n` such that `degreeOf i p > 0`. -/ +def vars {n : ℕ} {R : Type} [Zero R] (p : CMvPolynomial n R) : Finset (Fin n) := + Finset.univ.filter fun i => 0 < p.degreeOf i + +/-- Filter a polynomial, keeping only monomials for which `keep m` is true. -/ def restrictBy {n : ℕ} {R : Type} [BEq R] [LawfulBEq R] [Zero R] (keep : CMvMonomial n → Prop) [DecidablePred keep] (p : CMvPolynomial n R) : CMvPolynomial n R := Lawful.fromUnlawful <| p.1.filter (fun m _ => decide (keep m)) +/-- Restrict polynomial to monomials with total degree ≤ d. + + Filters out all monomials where `m.totalDegree > d`. +-/ def restrictTotalDegree {n : ℕ} {R : Type} [BEq R] [LawfulBEq R] [Zero R] (d : ℕ) (p : CMvPolynomial n R) : CMvPolynomial n R := restrictBy (fun m => m.totalDegree ≤ d) p @@ -231,85 +211,6 @@ def restrictDegree {n : ℕ} {R : Type} [BEq R] [LawfulBEq R] [Zero R] (d : ℕ) (p : CMvPolynomial n R) : CMvPolynomial n R := restrictBy (fun m => ∀ i : Fin n, m.degreeOf i ≤ d) p -/-- Algebra evaluation: evaluates polynomial in an algebra. - - Given an algebra `σ` over `R` and a function `f : Fin n → σ`, evaluates the polynomial. --/ -def aeval {n : ℕ} {R σ : Type} [CommSemiring R] [CommSemiring σ] [Algebra R σ] - (f : Fin n → σ) (p : CMvPolynomial n R) : σ := - sorry - -/-- Substitution: substitutes polynomials for variables. - - Given `f : Fin n → CMvPolynomial m R`, substitutes `f i` for variable `X i`. --/ -def bind₁ {n m : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] - (f : Fin n → CMvPolynomial m R) (p : CMvPolynomial n R) : CMvPolynomial m R := - sorry - -/-- Rename variables using a function. - - Given `f : Fin n → Fin m`, renames variable `X i` to `X (f i)`. --/ -def rename {n m : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] - (f : Fin n → Fin m) (p : CMvPolynomial n R) : CMvPolynomial m R := - let renameMonomial (mono : CMvMonomial n) : CMvMonomial m := - Vector.ofFn (fun j => (Finset.univ.filter (fun i => f i = j)).sum (fun i => mono.get i)) - ExtTreeMap.foldl (fun acc mono c => acc + monomial (renameMonomial mono) c) 0 p.1 - --- `renameEquiv` is defined in `CompPoly.Multivariate.Rename` - -/-- `CMvPolynomial n R` forms a commutative ring when `R` is a commutative ring. - - Extends the `CommSemiring` structure with subtraction. - - TODO: Requires `CommSemiring` instance (defined in MvPolyEquiv.lean). - TODO: Verify Neg/Sub operations exist in Lawful.lean. - Note: Cannot import MvPolyEquiv.lean due to circular dependency, so all fields are `sorry`. --/ -instance {n : ℕ} {R : Type} [CommRing R] [BEq R] [LawfulBEq R] : - CommRing (CMvPolynomial n R) where - add_assoc := sorry - zero_add := sorry - add_zero := sorry - nsmul := sorry - nsmul_zero := sorry - nsmul_succ := sorry - add_comm := sorry - left_distrib := sorry - right_distrib := sorry - zero_mul := sorry - mul_zero := sorry - mul_assoc := sorry - one_mul := sorry - mul_one := sorry - npow := sorry - npow_zero := sorry - npow_succ := sorry - zsmul := sorry - zsmul_zero' := sorry - zsmul_succ' := sorry - zsmul_neg' := sorry - neg_add_cancel := sorry - mul_comm := sorry - -/-- Convert sum representation to iterative form. - - TODO: Clarify intended behavior - may be related to converting between different - polynomial representations or evaluation strategies. --/ -def sumToIter {n : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] - (p : CMvPolynomial n R) : CMvPolynomial n R := - sorry - end CMvPolynomial --- TODO: Phase 1 items requiring Semiring/CommSemiring instances from MvPolyEquiv.lean --- (circular dependency): --- TODO: `Algebra R (CMvPolynomial n R)` instance --- TODO: `Module R (CMvPolynomial n R)` instance --- TODO: `finSuccEquiv` - Equivalence between (n+1)-variable and n-variable polynomials --- TODO: `optionEquivLeft` - Equivalence for option-indexed variables --- See MvPolyEquiv.lean for: eval₂Hom, isEmptyRingEquiv, SMulZeroClass - end CPoly diff --git a/CompPoly/Multivariate/MvPolyEquiv.lean b/CompPoly/Multivariate/MvPolyEquiv.lean index 4eb6e43..169846d 100644 --- a/CompPoly/Multivariate/MvPolyEquiv.lean +++ b/CompPoly/Multivariate/MvPolyEquiv.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2025 CompPoly. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Frantisek Silvasi, Julian Sutherland, Andrei Burdușa +Authors: Frantisek Silvasi, Julian Sutherland, Andrei Burdușa, Dimitris Mitsios -/ import Batteries.Data.Vector.Lemmas import CompPoly.Multivariate.CMvPolynomial @@ -398,6 +398,42 @@ instance {n : ℕ} : CommSemiring (CPoly.CMvPolynomial n R) where npow_succ := by intro n x; simp [npowRecAuto, npowRec] mul_comm := by aesop (add safe apply _root_.mul_comm) +section CommRingBridge + +variable {n : ℕ} {R : Type} [CommRing R] [BEq R] [LawfulBEq R] + +@[simp] +lemma map_neg (a : CMvPolynomial n R) : + fromCMvPolynomial (-a) = -fromCMvPolynomial a := by + ext m + simp only [MvPolynomial.coeff_neg, coeff_eq] + unfold CMvPolynomial.coeff + unfold_projs + unfold Lawful.neg Unlawful.neg Lawful.fromUnlawful + simp only [ExtTreeMap.get?_eq_getElem?, Unlawful.zero_eq_zero] + erw [Unlawful.filter_get, ExtTreeMap.getElem?_map] + cases h : (a.1)[CMvMonomial.ofFinsupp m]? with + | none => simp + | some v => simp + +lemma map_sub (a b : CMvPolynomial n R) : + fromCMvPolynomial (Sub.sub a b) = fromCMvPolynomial a - fromCMvPolynomial b := by + unfold Sub.sub Lawful.instSub Lawful.sub + rw [map_add, map_neg, sub_eq_add_neg] + +instance : CommRing (CPoly.CMvPolynomial n R) where + neg_add_cancel a := by + apply fromCMvPolynomial_injective + simp [map_neg, map_add, map_zero] + mul_comm := by + aesop (add safe apply _root_.mul_comm) + zsmul := zsmulRec + zsmul_zero' := fun _ => rfl + zsmul_succ' := fun _ _ => rfl + zsmul_neg' := fun _ _ => rfl + +end CommRingBridge + noncomputable def polyRingEquiv : RingEquiv (CPoly.CMvPolynomial n R) (MvPolynomial (Fin n) R) where toEquiv := CPoly.polyEquiv diff --git a/CompPoly/Multivariate/Operations.lean b/CompPoly/Multivariate/Operations.lean new file mode 100644 index 0000000..5d18388 --- /dev/null +++ b/CompPoly/Multivariate/Operations.lean @@ -0,0 +1,123 @@ +/- +Copyright (c) 2025 CompPoly. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Frantisek Silvasi, Julian Sutherland, Andrei Burdușa, Derek Sorensen +-/ +import CompPoly.Multivariate.MvPolyEquiv + +/-! +# Computable multivariate polynomials (extended operations) + +Operations on `CMvPolynomial` that depend on ring instances from `MvPolyEquiv.lean`, +such as monomial orders, leading terms, restriction, variable renaming, and substitution. + +The core type and basic operations (`CMvPolynomial`, `C`, `X`, `coeff`, `eval`, etc.) +are in `CMvPolynomial.lean`. The `CommSemiring` and `CommRing` instances are in +`MvPolyEquiv.lean`. + +## Main definitions + +* `MonomialOrder`: Typeclass for comparing monomials. +* `leadingMonomial`, `leadingCoeff`: Leading term according to a monomial order. +* `rename`: Rename variables using a function `Fin n → Fin m`. +* `aeval`: Algebra evaluation. +* `bind₁`: Substitution of polynomials for variables. +-/ +namespace CPoly + +open Std + +variable {R : Type} + +namespace CMvPolynomial + +/-- Monomial ordering typeclass for `n` variables. + + Provides a way to compare monomials for determining leading terms. +-/ +class MonomialOrder (n : ℕ) where + compare : CMvMonomial n → CMvMonomial n → Ordering + -- TODO: Add ordering axioms (transitivity, etc.) + +/-- Degree of a monomial according to a monomial order. + + Returns the degree of a monomial as determined by the ordering. + The exact meaning depends on the specific monomial order implementation + (e.g., total degree for graded orders, weighted degree, etc.). +-/ +def MonomialOrder.degree {n : ℕ} [MonomialOrder n] (m : CMvMonomial n) : ℕ := + sorry + +/-- Leading monomial of a polynomial according to a monomial order. + + Returns `none` for the zero polynomial. +-/ +def leadingMonomial {n : ℕ} {R : Type} [Zero R] [MonomialOrder n] + (p : CMvPolynomial n R) : Option (CMvMonomial n) := + sorry + +/-- Leading coefficient of a polynomial according to a monomial order. + + Returns `0` for the zero polynomial. +-/ +def leadingCoeff {n : ℕ} {R : Type} [Zero R] [MonomialOrder n] + (p : CMvPolynomial n R) : R := + sorry + +/-- Algebra evaluation: evaluates polynomial in an algebra. + + Given an algebra `σ` over `R` and a function `f : Fin n → σ`, evaluates the polynomial. +-/ +def aeval {n : ℕ} {R σ : Type} [CommSemiring R] [CommSemiring σ] [Algebra R σ] + (f : Fin n → σ) (p : CMvPolynomial n R) : σ := + sorry + +/-- Substitution: substitutes polynomials for variables. + + Given `f : Fin n → CMvPolynomial m R`, substitutes `f i` for variable `X i`. +-/ +def bind₁ {n m : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] + (f : Fin n → CMvPolynomial m R) (p : CMvPolynomial n R) : CMvPolynomial m R := + sorry + +/-- Rename variables using a function. + + Given `f : Fin n → Fin m`, renames variable `X i` to `X (f i)`. +-/ +def rename {n m : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] + (f : Fin n → Fin m) (p : CMvPolynomial n R) : CMvPolynomial m R := + let renameMonomial (mono : CMvMonomial n) : CMvMonomial m := + Vector.ofFn (fun j => (Finset.univ.filter (fun i => f i = j)).sum (fun i => mono.get i)) + ExtTreeMap.foldl (fun acc mono c => acc + monomial (renameMonomial mono) c) 0 p.1 + +-- `renameEquiv` is defined in `CompPoly.Multivariate.Rename` + +/-- Scalar multiplication with zero handling. + + This is automatically provided by `Module`, but we list it for completeness. + + TODO: Requires `Module` instance (see above). +-/ +instance {n : ℕ} {R : Type} [Zero R] [BEq R] [LawfulBEq R] : SMulZeroClass R (CMvPolynomial n R) := + sorry + +/-- Convert sum representation to iterative form. + + TODO: Clarify intended behavior - may be related to converting between different + polynomial representations or evaluation strategies. +-/ +def sumToIter {n : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] + (p : CMvPolynomial n R) : CMvPolynomial n R := + sorry + +end CMvPolynomial + +-- TODO: Phase 1 items requiring Semiring/CommSemiring instances from MvPolyEquiv.lean: +-- TODO: `Algebra R (CMvPolynomial n R)` instance +-- TODO: `Module R (CMvPolynomial n R)` instance +-- TODO: `eval₂Hom` - Ring homomorphism for evaluation +-- TODO: `finSuccEquiv` - Equivalence between (n+1)-variable and n-variable polynomials +-- TODO: `optionEquivLeft` - Equivalence for option-indexed variables +-- TODO: `isEmptyAlgEquiv` - Algebra equivalence for empty variable set + +end CPoly diff --git a/CompPoly/Multivariate/Rename.lean b/CompPoly/Multivariate/Rename.lean index 6be9efa..e104ec4 100644 --- a/CompPoly/Multivariate/Rename.lean +++ b/CompPoly/Multivariate/Rename.lean @@ -3,7 +3,7 @@ Copyright (c) 2025 CompPoly. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Dimitris Mitsios -/ -import CompPoly.Multivariate.MvPolyEquiv +import CompPoly.Multivariate.Operations import Mathlib.Algebra.MvPolynomial.Rename /-! diff --git a/CompPoly/Multivariate/Restrict.lean b/CompPoly/Multivariate/Restrict.lean index c00d079..5bd4917 100644 --- a/CompPoly/Multivariate/Restrict.lean +++ b/CompPoly/Multivariate/Restrict.lean @@ -3,7 +3,7 @@ Copyright (c) 2025 CompPoly. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Fawad Haider -/ -import CompPoly.Multivariate.CMvPolynomial +import CompPoly.Multivariate.Operations /-! # Lemmas for `CMvPolynomial.restrictBy`, `restrictTotalDegree`, and `restrictDegree` From e222544a34bf1131ea8dbb49743a615ed805a5ef Mon Sep 17 00:00:00 2001 From: Dimitris Date: Sat, 28 Feb 2026 11:58:19 +0200 Subject: [PATCH 2/2] chore: added authorship to Operations --- CompPoly/Multivariate/Operations.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CompPoly/Multivariate/Operations.lean b/CompPoly/Multivariate/Operations.lean index 5d18388..e8d7741 100644 --- a/CompPoly/Multivariate/Operations.lean +++ b/CompPoly/Multivariate/Operations.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2025 CompPoly. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Frantisek Silvasi, Julian Sutherland, Andrei Burdușa, Derek Sorensen +Authors: Frantisek Silvasi, Julian Sutherland, Andrei Burdușa, Derek Sorensen, Dimitris Mitsios -/ import CompPoly.Multivariate.MvPolyEquiv