Issue 55 - CommRing instance for CMvPolynomial, resolution of circular dependency

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

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,53 +157,13 @@ 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.
 -/
 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

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

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, Dimitris Mitsios
+-/
+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

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
 
 /-!

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`