diff --git a/CompPoly/Bivariate/CMvEquiv.lean b/CompPoly/Bivariate/CMvEquiv.lean index b088d972..f62b60a3 100644 --- a/CompPoly/Bivariate/CMvEquiv.lean +++ b/CompPoly/Bivariate/CMvEquiv.lean @@ -63,7 +63,7 @@ lemma isEmptyRingEquiv_symm_apply @[simp] lemma finSuccEquiv_symm_C {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] - {n : ℕ} (x : CMvPolynomial n R) : + {n : ℕ} (x : CMvPolynomial (Fin n) R) : CMvPolynomial.finSuccEquiv.symm (Polynomial.C x) = CMvPolynomial.rename Fin.succ x := by apply fromCMvPolynomial_injective @@ -95,8 +95,8 @@ lemma finSuccEquiv_symm_X {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] {n : ℕ} : CMvPolynomial.finSuccEquiv.symm - (Polynomial.X : Polynomial (CMvPolynomial n R)) = - CMvPolynomial.X 0 := by + (Polynomial.X : Polynomial (CMvPolynomial (Fin n) R)) = + CMvPolynomial.X (0 : Fin (n + 1)) := by rw [finSuccEquiv, polyRingEquiv.symm_trans_apply, polyRingEquiv.symm_apply_eq, RingEquiv.symm_trans_apply] simp only [RingEquiv.symm_symm] @@ -123,7 +123,7 @@ variable [CommRing R] [BEq R] [LawfulBEq R] [Nontrivial R] /-- Ring equivalence between `CBivariate R` and `CMvPolynomial 2 R`. -/ noncomputable def bivariateEquiv : - CBivariate R ≃+* CMvPolynomial 2 R := + CBivariate R ≃+* CMvPolynomial (Fin 2) R := let toPolyEquiv := CBivariate.ringEquiv let embedCoeffs := Polynomial.mapEquiv (Polynomial.mapEquiv CMvPolynomial.isEmptyRingEquiv.symm) @@ -162,14 +162,14 @@ lemma bivariateEquiv_CC (r : R) : /-- `bivariateEquiv` maps `CBivariate.X` to the second variable. -/ lemma bivariateEquiv_X : bivariateEquiv (CBivariate.X : CBivariate R) = - CMvPolynomial.X 1 := by + CMvPolynomial.X (1 : Fin 2) := by -- `finSuccEquiv_symm_X` is applied here by `simp` simp [bivariateEquiv, ringEquiv, X_toPoly] /-- `bivariateEquiv` maps `CBivariate.Y` to the first variable. -/ lemma bivariateEquiv_Y : bivariateEquiv (CBivariate.Y : CBivariate R) = - CMvPolynomial.X 0 := by + CMvPolynomial.X (0 : Fin 2) := by -- `finSuccEquiv_symm_X` is applied here by `simp` simp [bivariateEquiv, ringEquiv, Y_toPoly] @@ -182,14 +182,14 @@ lemma bivariateEquiv_symm_C (r : R) : /-- `bivariateEquiv.symm` maps the first variable to `CBivariate.Y`. -/ lemma bivariateEquiv_symm_X0 : - bivariateEquiv.symm (CMvPolynomial.X 0 : CMvPolynomial 2 R) = + bivariateEquiv.symm (CMvPolynomial.X (0 : Fin 2) : CMvPolynomial (Fin 2) R) = CBivariate.Y := by apply bivariateEquiv.injective simp [bivariateEquiv_Y] /-- `bivariateEquiv.symm` maps the second variable to `CBivariate.X`. -/ lemma bivariateEquiv_symm_X1 : - bivariateEquiv.symm (CMvPolynomial.X 1 : CMvPolynomial 2 R) = + bivariateEquiv.symm (CMvPolynomial.X (1 : Fin 2) : CMvPolynomial (Fin 2) R) = CBivariate.X := by apply bivariateEquiv.injective simp [bivariateEquiv_X] diff --git a/CompPoly/Multivariate/CMvMonomial.lean b/CompPoly/Multivariate/CMvMonomial.lean index 1ee327df..278da417 100644 --- a/CompPoly/Multivariate/CMvMonomial.lean +++ b/CompPoly/Multivariate/CMvMonomial.lean @@ -8,8 +8,9 @@ import Mathlib.Algebra.Group.Finsupp import Mathlib.Algebra.Group.TypeTags.Basic import Mathlib.Algebra.GroupWithZero.Nat import Mathlib.Algebra.Ring.Defs -import Mathlib.Data.Nat.Lattice +import Mathlib.Data.FinEnum import Batteries.Data.Vector.Basic +import Batteries.Data.Vector.Lemmas /-! # Computable monomials @@ -17,18 +18,24 @@ import Batteries.Data.Vector.Basic Monomials of the form `X₀ᵃ * X₁ᵇ * ... * Xₖᶻ`. These are represented as vectors of natural numbers, where each element corresponds to the exponent of a variable. +The variables are indexed by a type `σ` carrying a `FinEnum σ` instance. The exponents are stored +in a `Vector ℕ (FinEnum.card σ)` indexed through the enumeration `FinEnum.equiv : σ ≃ Fin (card σ)`. + ## Main definitions -* `CPoly.CMvMonomial n`: The type of monomials in `n` variables, implemented as `Vector ℕ n`. +* `CPoly.CMvMonomial σ`: The type of monomials in variables `σ`, implemented as + `Vector ℕ (FinEnum.card σ)`. -/ namespace CPoly +open FinEnum + /-- - Monomial in `n` variables. - - `#v[e₀, e₁, e₂]` denotes X₀^e₀ * X₁^e₁ * X₂^e₂ + Monomial in variables `σ`. + - `#v[e₀, e₁, e₂]` denotes X₀^e₀ * X₁^e₁ * X₂^e₂ (with the variables in enumeration order). -/ @[grind =] -def CMvMonomial (n : ℕ) : Type := Vector ℕ n +def CMvMonomial (σ : Type*) [FinEnum σ] : Type := Vector ℕ (FinEnum.card σ) syntax "#m[" withoutPosition(term,*,?) "]" : term @@ -36,9 +43,9 @@ open Lean in macro_rules | `(#m[$elems,*]) => `(#v[$elems,*]) -variable {n : ℕ} +variable {σ : Type*} [FinEnum σ] -instance : Repr (CMvMonomial n) where +instance : Repr (CMvMonomial σ) where reprPrec m _ := let indexed := (Array.range m.size).zip m.1 let toFormat : Std.ToFormat (ℕ × ℕ) := @@ -47,69 +54,59 @@ instance : Repr (CMvMonomial n) where section Instances -instance : GetElem (CMvMonomial n) ℕ ℕ fun _ idx ↦ idx < n := - inferInstanceAs (GetElem (Vector ℕ n) ℕ ℕ _) +instance : GetElem (CMvMonomial σ) ℕ ℕ fun _ idx ↦ idx < FinEnum.card σ := + inferInstanceAs (GetElem (Vector ℕ (FinEnum.card σ)) ℕ ℕ _) -instance : GetElem? (CMvMonomial n) ℕ ℕ fun _ idx ↦ idx < n := - inferInstanceAs (GetElem? (Vector ℕ n) ℕ ℕ _) +instance : GetElem? (CMvMonomial σ) ℕ ℕ fun _ idx ↦ idx < FinEnum.card σ := + inferInstanceAs (GetElem? (Vector ℕ (FinEnum.card σ)) ℕ ℕ _) -instance : DecidableEq (CMvMonomial n) := - inferInstanceAs (DecidableEq (Vector ℕ n)) +instance : DecidableEq (CMvMonomial σ) := + inferInstanceAs (DecidableEq (Vector ℕ (FinEnum.card σ))) -instance : Ord (CMvMonomial n) := - inferInstanceAs (Ord (Vector ℕ n)) +instance : Ord (CMvMonomial σ) := + inferInstanceAs (Ord (Vector ℕ (FinEnum.card σ))) -instance : Std.TransCmp (Ord.compare (α := CMvMonomial n)) := - inferInstanceAs (Std.TransCmp (Ord.compare (α := Vector ℕ n))) +instance : Std.TransCmp (Ord.compare (α := CMvMonomial σ)) := + inferInstanceAs (Std.TransCmp (Ord.compare (α := Vector ℕ (FinEnum.card σ)))) -instance : Std.LawfulEqCmp (Ord.compare (α := CMvMonomial n)) := - inferInstanceAs (Std.LawfulEqCmp (Ord.compare (α := Vector ℕ n))) +instance : Std.LawfulEqCmp (Ord.compare (α := CMvMonomial σ)) := + inferInstanceAs (Std.LawfulEqCmp (Ord.compare (α := Vector ℕ (FinEnum.card σ)))) end Instances namespace CMvMonomial -variable {m m₁ m₂ : CMvMonomial n} +variable {m m₁ m₂ : CMvMonomial σ} @[ext, grind ext] -protected theorem ext (h : (i : Nat) → (_ : i < n) → m₁[i] = m₂[i]) : m₁ = m₂ := +protected theorem ext (h : (i : Nat) → (_ : i < FinEnum.card σ) → m₁[i] = m₂[i]) : m₁ = m₂ := Vector.ext h -/-- Extend a monomial to a larger number of variables by padding with zeros. -/ -def extend (n' : ℕ) (m : CMvMonomial n) : CMvMonomial (max n n') := - cast (have : n + (n' - n) = n ⊔ n' := - if h : n' ≤ n - then by simp [h] - else by have := le_of_lt (not_le.1 h) - rw [sup_of_le_right this, Nat.add_sub_cancel' this] - this ▸ rfl) - (m.append (Vector.replicate (n' - n) 0)) - /-- The total degree of a monomial (sum of all exponents). -/ -def totalDegree (m : CMvMonomial n) : ℕ := m.sum +def totalDegree (m : CMvMonomial σ) : ℕ := m.sum -/-- The degree of the $i$-th variable in the monomial. -/ -def degreeOf (m : CMvMonomial n) (i : Fin n) : ℕ := m.get i +/-- The degree of the variable `i` in the monomial. -/ +def degreeOf (m : CMvMonomial σ) (i : σ) : ℕ := m.get (FinEnum.equiv i) /-- The zero monomial (all exponents are zero). -/ -def zero : CMvMonomial n := Vector.replicate n 0 +def zero : CMvMonomial σ := Vector.replicate (FinEnum.card σ) 0 -instance : Zero (CMvMonomial n) := ⟨zero⟩ +instance : Zero (CMvMonomial σ) := ⟨zero⟩ /-- Monomial multiplication (adds exponents element-wise). -/ -def add : CMvMonomial n → CMvMonomial n → CMvMonomial n := +def add : CMvMonomial σ → CMvMonomial σ → CMvMonomial σ := Vector.zipWith .add -instance : Add (CMvMonomial n) := ⟨add⟩ +instance : Add (CMvMonomial σ) := ⟨add⟩ @[simp] lemma add_zero : m + 0 = m := by unfold_projs; dsimp [add, zero, CMvMonomial]; grind /-- Check if $m_1$ divides $m_2$ (true if all exponents of $m_1$ are $\le$ those of $m_2$). -/ -def divides (m₁ m₂ : CMvMonomial n) : Bool := +def divides (m₁ m₂ : CMvMonomial σ) : Bool := Vector.all (Vector.zipWith (flip Nat.ble) m₁ m₂) (· == true) -instance : Dvd (CMvMonomial n) := ⟨fun m₁ m₂ ↦ divides m₁ m₂⟩ +instance : Dvd (CMvMonomial σ) := ⟨fun m₁ m₂ ↦ divides m₁ m₂⟩ instance : Decidable (m₁ ∣ m₂) := by dsimp [(·∣·)]; infer_instance @@ -118,85 +115,96 @@ instance : Decidable (m₁ ∣ m₂) := by dsimp [(·∣·)]; infer_instance The result makes sense assuming `m₂ | m₁`. -/ -def div (m₁ m₂ : CMvMonomial n) : CMvMonomial n := +def div (m₁ m₂ : CMvMonomial σ) : CMvMonomial σ := Vector.zipWith Nat.sub m₁ m₂ -instance : Div (CMvMonomial n) := ⟨div⟩ - -instance : Decidable (m₁ ∣ m₂) := by dsimp [(·∣·)]; infer_instance +instance : Div (CMvMonomial σ) := ⟨div⟩ /-- Convert a `CMvMonomial` to a `Finsupp`. -/ -def toFinsupp (m : CMvMonomial n) : Fin n →₀ ℕ := - ⟨{i : Fin n | m[i] ≠ 0}, m.get, by aesop⟩ +def toFinsupp (m : CMvMonomial σ) : σ →₀ ℕ := + ⟨Finset.univ.filter (fun i => m.get (FinEnum.equiv i) ≠ 0), + fun i => m.get (FinEnum.equiv i), + by intro i; simp⟩ /-- Convert a `Finsupp` to a `CMvMonomial`. -/ -def ofFinsupp (m : Fin n →₀ ℕ) : CPoly.CMvMonomial n := Vector.ofFn m +def ofFinsupp (m : σ →₀ ℕ) : CPoly.CMvMonomial σ := Vector.ofFn (fun k => m (FinEnum.equiv.symm k)) @[grind =, simp] theorem ofFinsupp_toFinsupp : ofFinsupp m.toFinsupp = m := by - unfold toFinsupp ofFinsupp + unfold ofFinsupp ext i hi erw [Vector.getElem_ofFn] + simp only [toFinsupp, Finsupp.coe_mk, Equiv.apply_symm_apply] rfl @[grind =, simp] -theorem toFinsupp_ofFinsupp {m : Fin n →₀ ℕ} : (ofFinsupp m).toFinsupp = m := by - ext i; aesop (add simp [CMvMonomial.toFinsupp, CMvMonomial.ofFinsupp, Vector.get]) +theorem toFinsupp_ofFinsupp {m : σ →₀ ℕ} : (ofFinsupp m).toFinsupp = m := by + ext i + simp only [toFinsupp, ofFinsupp, Finsupp.coe_mk] + rw [Vector.get_ofFn, Equiv.symm_apply_apply] -lemma injective_ofFinsupp : Function.Injective (ofFinsupp (n := n)) := +lemma injective_ofFinsupp : Function.Injective (ofFinsupp (σ := σ)) := Function.HasLeftInverse.injective ⟨toFinsupp, fun _ ↦ toFinsupp_ofFinsupp⟩ -lemma injective_toFinsupp : Function.Injective (toFinsupp (n := n)) := +lemma injective_toFinsupp : Function.Injective (toFinsupp (σ := σ)) := Function.HasLeftInverse.injective ⟨ofFinsupp, fun _ ↦ ofFinsupp_toFinsupp⟩ -def equivFinsupp : CMvMonomial n ≃ (Fin n →₀ ℕ) where +def equivFinsupp : CMvMonomial σ ≃ (σ →₀ ℕ) where toFun := toFinsupp invFun := ofFinsupp left_inv := fun _ ↦ ofFinsupp_toFinsupp right_inv := fun _ ↦ toFinsupp_ofFinsupp @[simp, grind =] -lemma map_mul {m₁ m₂ : Multiplicative (Fin n →₀ ℕ)} : +lemma map_mul {m₁ m₂ : Multiplicative (σ →₀ ℕ)} : ofFinsupp (m₁ * m₂) = (ofFinsupp m₁) + (ofFinsupp m₂) := by unfold_projs; ext erw [Vector.getElem_ofFn, Vector.getElem_zipWith] simp [Multiplicative.toAdd, Multiplicative.ofAdd, ofFinsupp] +@[simp, grind =] +theorem ofFinsupp_zero : ofFinsupp (0 : σ →₀ ℕ) = (zero : CMvMonomial σ) := by + unfold ofFinsupp zero + ext i hi + erw [Vector.getElem_ofFn, Vector.getElem_replicate] + simp + end CMvMonomial -abbrev MonoR (n : ℕ) (R : Type*) := CMvMonomial n × R +abbrev MonoR (σ : Type*) [FinEnum σ] (R : Type*) := CMvMonomial σ × R namespace MonoR -variable {n : ℕ} {R : Type*} +variable {σ : Type*} [FinEnum σ] {R : Type*} -instance [DecidableEq R] : DecidableEq (CMvMonomial n × R) := +instance [DecidableEq R] : DecidableEq (CMvMonomial σ × R) := instDecidableEqProd section -instance [Repr R] : Repr (MonoR n R) where +instance [Repr R] : Repr (MonoR σ R) where reprPrec | (m, c), _ => repr c ++ " * " ++ repr m @[simp, grind=] -def C (c : R) : MonoR n R := (CMvMonomial.zero, c) +def C (c : R) : MonoR σ R := (CMvMonomial.zero, c) variable [CommSemiring R] [HMod R R R] [BEq R] -def divides (t₁ t₂ : MonoR n R) : Bool := +def divides (t₁ t₂ : MonoR σ R) : Bool := t₁.1 ∣ t₂.1 ∧ t₁.2 % t₂.2 == 0 -instance : Dvd (MonoR n R) := ⟨fun t₁ t₂ ↦ divides t₁ t₂⟩ +instance : Dvd (MonoR σ R) := ⟨fun t₁ t₂ ↦ divides t₁ t₂⟩ -instance {t₁ t₂ : MonoR n R} : Decidable (t₁ ∣ t₂) := by +instance {t₁ t₂ : MonoR σ R} : Decidable (t₁ ∣ t₂) := by dsimp [(·∣·)] infer_instance end -def evalMonomial {R : Type*} {n : ℕ} [CommSemiring R] : (Fin n → R) → CMvMonomial n → R := - fun vals m => ∏ (i : Fin n), (vals i) ^ m.get i +def evalMonomial {R : Type*} {σ : Type*} [FinEnum σ] [CommSemiring R] : + (σ → R) → CMvMonomial σ → R := + fun vals m => ∏ (i : σ), (vals i) ^ m.get (FinEnum.equiv i) end MonoR diff --git a/CompPoly/Multivariate/CMvPolynomial.lean b/CompPoly/Multivariate/CMvPolynomial.lean index c31d5e24..a5760d30 100644 --- a/CompPoly/Multivariate/CMvPolynomial.lean +++ b/CompPoly/Multivariate/CMvPolynomial.lean @@ -23,7 +23,7 @@ that depend on ring instances (monomial orders, `rename`, `aeval`, etc.) are in ## Main definitions -* `CPoly.CMvPolynomial n R`: The type of multivariate polynomials in `n` variables +* `CPoly.CMvPolynomial σ R`: The type of multivariate polynomials in variables `σ` with coefficients in `R`. * `CPoly.CMvPolynomial.C`: Constant polynomial constructor. * `CPoly.CMvPolynomial.X`: Variable polynomial constructor. @@ -40,32 +40,34 @@ namespace CPoly open Std -/-- A computable multivariate polynomial in `n` variables with coefficients in `R`. -/ -abbrev CMvPolynomial (n : ℕ) (R : Type*) [Zero R] : Type _ := Lawful n R +/-- A computable multivariate polynomial in variables `σ` with coefficients in `R`. -/ +abbrev CMvPolynomial (σ : Type*) [FinEnum σ] (R : Type*) [Zero R] : Type _ := Lawful σ R variable {R : Type*} namespace CMvPolynomial /-- Construct a constant polynomial. -/ -def C {n : ℕ} {R : Type*} [BEq R] [LawfulBEq R] [Zero R] (c : R) : CMvPolynomial n R := - Lawful.C (n := n) (R := R) c +def C {σ : Type*} [FinEnum σ] {R : Type*} [BEq R] [LawfulBEq R] [Zero R] (c : R) : + CMvPolynomial σ R := + Lawful.C (σ := σ) (R := R) c /-- Construct the polynomial $X_i$. -/ -def X {n : ℕ} {R : Type*} [Zero R] [One R] [BEq R] [LawfulBEq R] - (i : Fin n) : CMvPolynomial n R := - let monomial : CMvMonomial n := Vector.ofFn (fun j => if j = i then 1 else 0) +def X {σ : Type*} [FinEnum σ] {R : Type*} [Zero R] [One R] [BEq R] [LawfulBEq R] + (i : σ) : CMvPolynomial σ R := + let monomial : CMvMonomial σ := Vector.ofFn (fun j => if j = FinEnum.equiv i then 1 else 0) Lawful.fromUnlawful <| .ofList [(monomial, (1 : R))] /-- Extract the coefficient of a monomial. -/ -def coeff {R : Type*} {n : ℕ} [Zero R] (m : CMvMonomial n) (p : CMvPolynomial n R) : R := +def coeff {R : Type*} {σ : Type*} [FinEnum σ] [Zero R] (m : CMvMonomial σ) (p : CMvPolynomial σ R) : + R := p.1[m]?.getD 0 attribute [grind =] coeff.eq_def /-- Extensionality: two polynomials are equal if all their coefficients are equal. -/ @[ext, grind ext] -theorem ext {n : ℕ} [Zero R] (p q : CMvPolynomial n R) +theorem ext {σ : Type*} [FinEnum σ] [Zero R] (p q : CMvPolynomial σ R) (h : ∀ m, coeff m p = coeff m q) : p = q := by unfold coeff at h rcases p with ⟨p, hp⟩; rcases q with ⟨q, hq⟩ @@ -81,11 +83,12 @@ section variable [BEq R] [LawfulBEq R] @[simp, grind =] -lemma fromUnlawful_zero {n : ℕ} [Zero R] : Lawful.fromUnlawful 0 = (0 : Lawful n R) := by +lemma fromUnlawful_zero {σ : Type*} [FinEnum σ] [Zero R] : + Lawful.fromUnlawful 0 = (0 : Lawful σ R) := by unfold Lawful.fromUnlawful grind -variable {n : ℕ} [CommSemiring R] {m : CMvMonomial n} {p q : CMvPolynomial n R} +variable {σ : Type*} [FinEnum σ] [CommSemiring R] {m : CMvMonomial σ} {p q : CMvPolynomial σ R} @[simp, grind =] lemma add_getD? : (p + q).val[m]?.getD 0 = p.val[m]?.getD 0 + q.val[m]?.getD 0 := by @@ -97,8 +100,8 @@ lemma coeff_add : coeff m (p + q) = coeff m p + coeff m q := by simp only [coeff /-- Auxiliary lemma showing that conversion from unlawful polynomials respects the sum fold. -/ lemma fromUnlawful_fold_eq_fold_fromUnlawful₀ - {t : List (CMvMonomial n × R)} {f : CMvMonomial n → R → Unlawful n R} : - ∀ init : Unlawful n R, + {t : List (CMvMonomial σ × R)} {f : CMvMonomial σ → R → Unlawful σ R} : + ∀ init : Unlawful σ R, Lawful.fromUnlawful (List.foldl (fun u term => (f term.1 term.2) + u) init t) = List.foldl (fun l term => (Lawful.fromUnlawful (f term.1 term.2)) + l) (Lawful.fromUnlawful init) t := by @@ -114,8 +117,8 @@ lemma fromUnlawful_fold_eq_fold_fromUnlawful₀ /-- Auxiliary lemma showing that conversion from unlawful polynomials respects the fold over terms. -/ -lemma fromUnlawful_fold_eq_fold_fromUnlawful {t : Unlawful n R} - {f : CMvMonomial n → R → Unlawful n R} : +lemma fromUnlawful_fold_eq_fold_fromUnlawful {t : Unlawful σ R} + {f : CMvMonomial σ → R → Unlawful σ R} : Lawful.fromUnlawful (ExtTreeMap.foldl (fun u m c => (f m c) + u) 0 t) = ExtTreeMap.foldl (fun l m c => (Lawful.fromUnlawful (f m c)) + l) 0 t := by simp only [CMvMonomial.eq_1, ExtTreeMap.foldl_eq_foldl_toList] @@ -127,24 +130,24 @@ end /-- Evaluate a polynomial at a point given by a ring homomorphism `f` and variable assignments `vs`. -/ -def eval₂ {R S : Type*} {n : ℕ} [Semiring R] [CommSemiring S] : - (R →+* S) → (Fin n → S) → CMvPolynomial n R → S := +def eval₂ {R S : Type*} {σ : Type*} [FinEnum σ] [Semiring R] [CommSemiring S] : + (R →+* S) → (σ → S) → CMvPolynomial σ R → S := fun f vs p => ExtTreeMap.foldl (fun s m c => (f c * MonoR.evalMonomial vs m) + s) 0 p.1 /-- Term representation used by the fixed-order multivariate Horner evaluator. -/ -abbrev HornerTerm (n : ℕ) (S : Type*) := CMvMonomial n × S +abbrev HornerTerm (σ : Type*) [FinEnum σ] (S : Type*) := CMvMonomial σ × S /-- Terms grouped by one variable exponent. -/ -abbrev HornerGroup (n : ℕ) (S : Type*) := ℕ × List (HornerTerm n S) +abbrev HornerGroup (σ : Type*) [FinEnum σ] (S : Type*) := ℕ × List (HornerTerm σ S) /-- Read the exponent for a variable index represented as a natural number. -/ -def hornerExponent {n : ℕ} (k : ℕ) (m : CMvMonomial n) : ℕ := +def hornerExponent {σ : Type*} [FinEnum σ] (k : ℕ) (m : CMvMonomial σ) : ℕ := m[k]?.getD 0 /-- Add a term to an association list keyed by the current variable exponent. -/ -def insertHornerTerm {n : ℕ} {S : Type*} - (exponent : ℕ) (term : HornerTerm n S) : - List (HornerGroup n S) → List (HornerGroup n S) +def insertHornerTerm {σ : Type*} [FinEnum σ] {S : Type*} + (exponent : ℕ) (term : HornerTerm σ S) : + List (HornerGroup σ S) → List (HornerGroup σ S) | [] => [(exponent, [term])] | group :: groups => if group.1 = exponent then @@ -153,8 +156,8 @@ def insertHornerTerm {n : ℕ} {S : Type*} group :: insertHornerTerm exponent term groups /-- Insert an exponent group into descending exponent order. -/ -def insertHornerGroupDesc {n : ℕ} {S : Type*} - (group : HornerGroup n S) : List (HornerGroup n S) → List (HornerGroup n S) +def insertHornerGroupDesc {σ : Type*} [FinEnum σ] {S : Type*} + (group : HornerGroup σ S) : List (HornerGroup σ S) → List (HornerGroup σ S) | [] => [group] | group' :: groups => if group'.1 < group.1 then @@ -163,19 +166,19 @@ def insertHornerGroupDesc {n : ℕ} {S : Type*} group' :: insertHornerGroupDesc group groups /-- Collect terms into association-list groups keyed by the current variable exponent. -/ -def collectHornerGroups {n : ℕ} {S : Type*} - (k : ℕ) (terms : List (HornerTerm n S)) : List (HornerGroup n S) := +def collectHornerGroups {σ : Type*} [FinEnum σ] {S : Type*} + (k : ℕ) (terms : List (HornerTerm σ S)) : List (HornerGroup σ S) := terms.foldl (fun groups term ↦ insertHornerTerm (hornerExponent k term.1) term groups) [] /-- Sort exponent groups from high exponent to low exponent. -/ -def sortHornerGroups {n : ℕ} {S : Type*} - (groups : List (HornerGroup n S)) : List (HornerGroup n S) := +def sortHornerGroups {σ : Type*} [FinEnum σ] {S : Type*} + (groups : List (HornerGroup σ S)) : List (HornerGroup σ S) := groups.foldl (fun sorted group ↦ insertHornerGroupDesc group sorted) [] /-- Group terms by the current variable exponent, sorted from high to low exponent. -/ -def hornerGroups {n : ℕ} {S : Type*} - (k : ℕ) (terms : List (HornerTerm n S)) : List (HornerGroup n S) := +def hornerGroups {σ : Type*} [FinEnum σ] {S : Type*} + (k : ℕ) (terms : List (HornerTerm σ S)) : List (HornerGroup σ S) := sortHornerGroups (collectHornerGroups k terms) /-- Sparse Horner fold for already-evaluated coefficient groups. -/ @@ -192,9 +195,9 @@ def evalSparseHornerGroups {S : Type*} [CommSemiring S] group state.2 * x ^ state.1 -/-- Evaluate sparse multivariate terms by fixed-order Horner in variables `0, 1, ..., n-1`. -/ -def eval₂HornerTerms {n : ℕ} {S : Type*} [CommSemiring S] - (xs : ℕ → S) : ℕ → ℕ → List (HornerTerm n S) → S +/-- Evaluate sparse multivariate terms by fixed-order Horner in variables `0, 1, ..., card σ-1`. -/ +def eval₂HornerTerms {σ : Type*} [FinEnum σ] {S : Type*} [CommSemiring S] + (xs : ℕ → S) : ℕ → ℕ → List (HornerTerm σ S) → S | 0, _, terms => terms.foldl (fun acc term ↦ acc + term.2) 0 | fuel + 1, k, terms => let groups := hornerGroups k terms @@ -203,97 +206,91 @@ def eval₂HornerTerms {n : ℕ} {S : Type*} [CommSemiring S] evalSparseHornerGroups (xs k) evaluatedGroups /-- Evaluate a polynomial using fixed-order multivariate Horner evaluation. -/ -def eval₂Horner {R S : Type*} {n : ℕ} [Semiring R] [CommSemiring S] : - (R →+* S) → (Fin n → S) → CMvPolynomial n R → S := +def eval₂Horner {R S : Type*} {σ : Type*} [FinEnum σ] [Semiring R] [CommSemiring S] : + (R →+* S) → (σ → S) → CMvPolynomial σ R → S := fun f vs p ↦ - let xs : ℕ → S := fun k ↦ if h : k < n then vs ⟨k, h⟩ else 0 + let xs : ℕ → S := fun k ↦ if h : k < FinEnum.card σ then vs (FinEnum.equiv.symm ⟨k, h⟩) else 0 let terms := p.1.toList.map fun term ↦ (term.1, f term.2) - eval₂HornerTerms xs n 0 terms + eval₂HornerTerms xs (FinEnum.card σ) 0 terms /-- Evaluate a polynomial at a given point. -/ -def eval {R : Type*} {n : ℕ} [CommSemiring R] : (Fin n → R) → CMvPolynomial n R → R := +def eval {R : Type*} {σ : Type*} [FinEnum σ] [CommSemiring R] : (σ → R) → CMvPolynomial σ R → R := eval₂ (RingHom.id _) /-- Evaluate a polynomial at a given point using fixed-order multivariate Horner evaluation. -/ -def evalHorner {R : Type*} {n : ℕ} [CommSemiring R] : - (Fin n → R) → CMvPolynomial n R → R := +def evalHorner {R : Type*} {σ : Type*} [FinEnum σ] [CommSemiring R] : + (σ → R) → CMvPolynomial σ R → R := eval₂Horner (RingHom.id _) /-- The support of a polynomial (set of monomials with non-zero coefficients), represented as Finsupps. -/ -def support {R : Type*} {n : ℕ} [Zero R] (p : CMvPolynomial n R) : Finset (Fin n →₀ ℕ) := +def support {R : Type*} {σ : Type*} [FinEnum σ] [Zero R] (p : CMvPolynomial σ R) : + Finset (σ →₀ ℕ) := (Lawful.monomials p).map CMvMonomial.toFinsupp |>.toFinset /-- The total degree of a polynomial (maximum total degree of its monomials). -/ -def totalDegree {R : Type*} {n : ℕ} [Zero R] : CMvPolynomial n R → ℕ := +def totalDegree {R : Type*} {σ : Type*} [FinEnum σ] [Zero R] : CMvPolynomial σ R → ℕ := fun p => Finset.sup (List.toFinset (List.map CMvMonomial.toFinsupp (Lawful.monomials p))) (fun s => Finsupp.sum s (fun _ e => e)) /-- The degree of a polynomial in a specific variable. -/ -def degreeOf {R : Type*} {n : ℕ} [Zero R] (i : Fin n) : CMvPolynomial n R → ℕ := +def degreeOf {R : Type*} {σ : Type*} [FinEnum σ] [Zero R] (i : σ) : CMvPolynomial σ R → ℕ := fun p => Finset.sup (Lawful.monomials p).toFinset (fun m => m.degreeOf i) -/-- Construct a monomial `c * m` as a `CMvPolynomial n R`. +/-- Construct a monomial `c * m` as a `CMvPolynomial σ R`. Creates a polynomial with a single monomial term. If `c = 0`, returns the zero polynomial. -/ -def monomial {n : ℕ} {R : Type*} [BEq R] [LawfulBEq R] [Zero R] - (m : CMvMonomial n) (c : R) : CMvPolynomial n R := +def monomial {σ : Type*} [FinEnum σ] {R : Type*} [BEq R] [LawfulBEq R] [Zero R] + (m : CMvMonomial σ) (c : R) : CMvPolynomial σ R := if c == 0 then 0 else Lawful.fromUnlawful <| Unlawful.ofList [(m, c)] /-- 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) := +def degrees {σ : Type*} [FinEnum σ] {R : Type*} [Zero R] (p : CMvPolynomial σ R) : Multiset σ := Finset.univ.sum fun i => Multiset.replicate (p.degreeOf i) 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) : +lemma degreeOf_eq_count_degrees {σ : Type*} [FinEnum σ] {R : Type*} [Zero R] + (i : σ) (p : CMvPolynomial σ R) : p.degreeOf i = Multiset.count i p.degrees := by classical unfold CMvPolynomial.degrees - symm - calc - Multiset.count i (∑ j, Multiset.replicate (p.degreeOf j) j) - = ∑ j ∈ Finset.univ, Multiset.count i (Multiset.replicate (p.degreeOf j) j) := by - simpa [Finset.sum] using - (Multiset.count_sum' (s := Finset.univ) - (a := i) (f := fun j => Multiset.replicate (p.degreeOf j) j)) - _ = ∑ j ∈ Finset.univ, if j = i then p.degreeOf j else 0 := by - simp [Multiset.count_replicate, eq_comm] - _ = p.degreeOf i := by - simp + rw [Multiset.count_sum'] + simp only [Multiset.count_replicate] + rw [Finset.sum_ite_eq' Finset.univ i (fun j => p.degreeOf j)] + simp /-- 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`. + Returns the set of variable indices `i : σ` such that `degreeOf i p > 0`. -/ -def vars {n : ℕ} {R : Type*} [Zero R] (p : CMvPolynomial n R) : Finset (Fin n) := +def vars {σ : Type*} [FinEnum σ] {R : Type*} [Zero R] (p : CMvPolynomial σ R) : Finset σ := 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 := +def restrictBy {σ : Type*} [FinEnum σ] {R : Type*} [BEq R] [LawfulBEq R] [Zero R] + (keep : CMvMonomial σ → Prop) [DecidablePred keep] + (p : CMvPolynomial σ R) : CMvPolynomial σ 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 := +def restrictTotalDegree {σ : Type*} [FinEnum σ] {R : Type*} [BEq R] [LawfulBEq R] [Zero R] + (d : ℕ) (p : CMvPolynomial σ R) : CMvPolynomial σ R := restrictBy (fun m => m.totalDegree ≤ d) p /-- Restrict polynomial to monomials whose degree in each variable is ≤ d. Filters out all monomials where `m.degreeOf i > d` for some variable `i`. -/ -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 +def restrictDegree {σ : Type*} [FinEnum σ] {R : Type*} [BEq R] [LawfulBEq R] [Zero R] + (d : ℕ) (p : CMvPolynomial σ R) : CMvPolynomial σ R := + restrictBy (fun m => ∀ i : σ, m.degreeOf i ≤ d) p end CMvPolynomial diff --git a/CompPoly/Multivariate/CMvPolynomialEvalLemmas.lean b/CompPoly/Multivariate/CMvPolynomialEvalLemmas.lean index 56fd6134..dfb9e345 100644 --- a/CompPoly/Multivariate/CMvPolynomialEvalLemmas.lean +++ b/CompPoly/Multivariate/CMvPolynomialEvalLemmas.lean @@ -24,31 +24,31 @@ open CMvPolynomial section -variable {n : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] -variable (vals : Fin n → R) +variable {σ : Type*} [FinEnum σ] {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] +variable (vals : σ → R) @[simp] -lemma eval_zero : (0 : CMvPolynomial n R).eval vals = 0 := by +lemma eval_zero : (0 : CMvPolynomial σ R).eval vals = 0 := by simpa [eval₂Hom_apply] using (eval₂Hom (RingHom.id R) vals).map_zero @[simp] -lemma eval_one : (1 : CMvPolynomial n R).eval vals = 1 := by +lemma eval_one : (1 : CMvPolynomial σ R).eval vals = 1 := by simpa [eval₂Hom_apply] using (eval₂Hom (RingHom.id R) vals).map_one @[simp] -lemma eval_C (c : R) : (CMvPolynomial.C c : CMvPolynomial n R).eval vals = c := by +lemma eval_C (c : R) : (CMvPolynomial.C c : CMvPolynomial σ R).eval vals = c := by simp [eval_equiv, fromCMvPolynomial_C] @[simp] -lemma eval_add (p q : CMvPolynomial n R) : +lemma eval_add (p q : CMvPolynomial σ R) : (p + q).eval vals = p.eval vals + q.eval vals := by simp [eval_equiv] @[simp] -lemma eval_mul (p q : CMvPolynomial n R) : +lemma eval_mul (p q : CMvPolynomial σ R) : (p * q).eval vals = p.eval vals * q.eval vals := by simp [eval_equiv] @[simp] -lemma eval_pow (p : CMvPolynomial n R) (k : ℕ) : +lemma eval_pow (p : CMvPolynomial σ R) (k : ℕ) : (p ^ k).eval vals = (p.eval vals) ^ k := by simpa [eval₂Hom_apply] using (eval₂Hom (RingHom.id R) vals).map_pow p k @@ -56,16 +56,16 @@ end section -variable {n : ℕ} {R : Type} [CommRing R] [BEq R] [LawfulBEq R] -variable (vals : Fin n → R) +variable {σ : Type*} [FinEnum σ] {R : Type} [CommRing R] [BEq R] [LawfulBEq R] +variable (vals : σ → R) @[simp] -lemma eval_neg (p : CMvPolynomial n R) : +lemma eval_neg (p : CMvPolynomial σ R) : (-p).eval vals = -(p.eval vals) := by simpa [eval₂Hom_apply] using (eval₂Hom (RingHom.id R) vals).map_neg p @[simp] -lemma eval_sub (p q : CMvPolynomial n R) : +lemma eval_sub (p q : CMvPolynomial σ R) : (p - q).eval vals = p.eval vals - q.eval vals := by simpa [eval₂Hom_apply] using (eval₂Hom (RingHom.id R) vals).map_sub p q @@ -90,7 +90,7 @@ typically have a degree bound on the difference polynomial, not on `p` and `q` individually. -/ theorem CMvPolynomial.eval_ext_univariate [CommRing R] [DecidableEq R] [BEq R] [LawfulBEq R] [IsDomain R] - {p q : CMvPolynomial 1 R} {d : ℕ} {S : Finset R} + {p q : CMvPolynomial (Fin 1) R} {d : ℕ} {S : Finset R} (hdeg : (fromCMvPolynomial p - fromCMvPolynomial q).degreeOf 0 ≤ d) (hagree : d < (S.filter diff --git a/CompPoly/Multivariate/FinSuccEquiv.lean b/CompPoly/Multivariate/FinSuccEquiv.lean index adcf3e1c..f5ee66e7 100644 --- a/CompPoly/Multivariate/FinSuccEquiv.lean +++ b/CompPoly/Multivariate/FinSuccEquiv.lean @@ -46,7 +46,7 @@ namespace CPoly /-- `Polynomial.mapEquiv` through the CMvPolynomial ↔ MvPolynomial bridge. -/ noncomputable def polynomialCMvPolyEquiv : - Polynomial (CMvPolynomial n R) ≃+* Polynomial (MvPolynomial (Fin n) R) := + Polynomial (CMvPolynomial (Fin n) R) ≃+* Polynomial (MvPolynomial (Fin n) R) := Polynomial.mapEquiv polyRingEquiv end CPoly @@ -56,37 +56,37 @@ namespace CMvPolynomial /-! ### `finSuccEquiv` -/ /-- Ring equivalence splitting off the first variable: - `CMvPolynomial (n+1) R ≃+* Polynomial (CMvPolynomial n R)`. + `CMvPolynomial (Fin (n+1)) R ≃+* Polynomial (CMvPolynomial (Fin n) R)`. This mirrors `MvPolynomial.finSuccEquiv R n`. The 0-th variable becomes the univariate indeterminate `Polynomial.X`, and variables `1, …, n` become - the multivariate variables of the coefficient ring `CMvPolynomial n R`. -/ + the multivariate variables of the coefficient ring `CMvPolynomial (Fin n) R`. -/ noncomputable def finSuccEquiv : - CMvPolynomial (n + 1) R ≃+* Polynomial (CMvPolynomial n R) := - (polyRingEquiv (n := n + 1)).trans <| + CMvPolynomial (Fin (n + 1)) R ≃+* Polynomial (CMvPolynomial (Fin n) R) := + (polyRingEquiv (σ := Fin (n + 1))).trans <| (MvPolynomial.finSuccEquiv R n).toRingEquiv.trans polynomialCMvPolyEquiv.symm /-- The equivalence is a left inverse: applying the inverse then forward is the identity. -/ @[simp] -theorem finSuccEquiv_symm_apply_apply (p : CMvPolynomial (n + 1) R) : +theorem finSuccEquiv_symm_apply_apply (p : CMvPolynomial (Fin (n + 1)) R) : finSuccEquiv.symm (finSuccEquiv p) = p := finSuccEquiv.symm_apply_apply p /-- The equivalence is a right inverse: applying forward then the inverse is the identity. -/ @[simp] theorem finSuccEquiv_apply_symm_apply - (q : Polynomial (CMvPolynomial n R)) : + (q : Polynomial (CMvPolynomial (Fin n) R)) : finSuccEquiv (finSuccEquiv.symm q) = q := finSuccEquiv.apply_symm_apply q /-- `finSuccEquiv` preserves addition. -/ -theorem finSuccEquiv_add (p q : CMvPolynomial (n + 1) R) : +theorem finSuccEquiv_add (p q : CMvPolynomial (Fin (n + 1)) R) : finSuccEquiv (p + q) = finSuccEquiv p + finSuccEquiv q := finSuccEquiv.map_add p q /-- `finSuccEquiv` preserves multiplication. -/ -theorem finSuccEquiv_mul (p q : CMvPolynomial (n + 1) R) : +theorem finSuccEquiv_mul (p q : CMvPolynomial (Fin (n + 1)) R) : finSuccEquiv (p * q) = finSuccEquiv p * finSuccEquiv q := finSuccEquiv.map_mul p q @@ -94,13 +94,13 @@ theorem finSuccEquiv_mul (p q : CMvPolynomial (n + 1) R) : /-- `finSuccEquiv` maps zero to zero. -/ @[simp] theorem finSuccEquiv_zero : - finSuccEquiv (0 : CMvPolynomial (n + 1) R) = 0 := + finSuccEquiv (0 : CMvPolynomial (Fin (n + 1)) R) = 0 := RingEquiv.map_zero (finSuccEquiv (n := n) (R := R)) /-- `finSuccEquiv` maps one to one. -/ @[simp] theorem finSuccEquiv_one : - finSuccEquiv (1 : CMvPolynomial (n + 1) R) = 1 := + finSuccEquiv (1 : CMvPolynomial (Fin (n + 1)) R) = 1 := RingEquiv.map_one (finSuccEquiv (n := n) (R := R)) end CMvPolynomial diff --git a/CompPoly/Multivariate/HornerLemmas.lean b/CompPoly/Multivariate/HornerLemmas.lean index ada7d936..7f002c86 100644 --- a/CompPoly/Multivariate/HornerLemmas.lean +++ b/CompPoly/Multivariate/HornerLemmas.lean @@ -22,26 +22,26 @@ namespace CMvPolynomial /-! ### Mathematical specifications for Horner helper functions -/ /-- Term-level specification: multiply the coefficient by the remaining variable powers. -/ -private def eval₂HornerTermSpec {n : ℕ} {S : Type*} [CommSemiring S] - (xs : ℕ → S) : ℕ → ℕ → HornerTerm n S → S +private def eval₂HornerTermSpec {σ : Type*} [FinEnum σ] {S : Type*} [CommSemiring S] + (xs : ℕ → S) : ℕ → ℕ → HornerTerm σ S → S | 0, _, term => term.2 | fuel + 1, k, term => eval₂HornerTermSpec xs fuel (k + 1) term * xs k ^ hornerExponent k term.1 /-- List-level specification for evaluating Horner terms as a commutative sum. -/ -private def eval₂HornerTermsSpec {n : ℕ} {S : Type*} [CommSemiring S] - (xs : ℕ → S) (fuel k : ℕ) (terms : List (HornerTerm n S)) : S := +private def eval₂HornerTermsSpec {σ : Type*} [FinEnum σ] {S : Type*} [CommSemiring S] + (xs : ℕ → S) (fuel k : ℕ) (terms : List (HornerTerm σ S)) : S := (terms.map (eval₂HornerTermSpec xs fuel k)).sum /-- Specification for one exponent group after its coefficient terms are evaluated. -/ -private def groupWeightedSpec {n : ℕ} {S : Type*} [CommSemiring S] - (weight : HornerTerm n S → S) (x : S) (group : HornerGroup n S) : S := +private def groupWeightedSpec {σ : Type*} [FinEnum σ] {S : Type*} [CommSemiring S] + (weight : HornerTerm σ S → S) (x : S) (group : HornerGroup σ S) : S := (group.2.map weight).sum * x ^ group.1 /-- Specification for a raw list of terms weighted by one variable exponent. -/ -private def termsWeightedSpec {n : ℕ} {S : Type*} [CommSemiring S] - (k : ℕ) (weight : HornerTerm n S → S) (x : S) - (terms : List (HornerTerm n S)) : S := +private def termsWeightedSpec {σ : Type*} [FinEnum σ] {S : Type*} [CommSemiring S] + (k : ℕ) (weight : HornerTerm σ S → S) (x : S) + (terms : List (HornerTerm σ S)) : S := (terms.map fun term ↦ weight term * x ^ hornerExponent k term.1).sum /-- Specification for evaluated exponent groups as a sparse sum of powers. -/ @@ -73,8 +73,8 @@ private lemma foldl_add_eq_add_sum {α S : Type*} [CommSemiring S] /-! ### Group sorting invariants -/ -private lemma mem_insertHornerGroupDesc {n : ℕ} {S : Type*} - (group x : HornerGroup n S) : +private lemma mem_insertHornerGroupDesc {σ : Type*} [FinEnum σ] {S : Type*} + (group x : HornerGroup σ S) : ∀ groups, x ∈ insertHornerGroupDesc group groups ↔ x = group ∨ x ∈ groups := by intro groups induction groups with @@ -85,8 +85,8 @@ private lemma mem_insertHornerGroupDesc {n : ℕ} {S : Type*} · simp [insertHornerGroupDesc, h] · simp [insertHornerGroupDesc, h, ih, or_left_comm] -private lemma insertHornerGroupDesc_pairwise {n : ℕ} {S : Type*} - (group : HornerGroup n S) : +private lemma insertHornerGroupDesc_pairwise {σ : Type*} [FinEnum σ] {S : Type*} + (group : HornerGroup σ S) : ∀ groups, descendingByExponent groups → descendingByExponent (insertHornerGroupDesc group groups) := by intro groups @@ -115,12 +115,12 @@ private lemma insertHornerGroupDesc_pairwise {n : ℕ} {S : Type*} · exact Nat.le_of_not_gt hlt · exact hsorted.1 y hy -private lemma sortHornerGroups_descending {n : ℕ} {S : Type*} - (groups : List (HornerGroup n S)) : +private lemma sortHornerGroups_descending {σ : Type*} [FinEnum σ] {S : Type*} + (groups : List (HornerGroup σ S)) : descendingByExponent (sortHornerGroups groups) := by unfold sortHornerGroups have hsort : - ∀ (groups sorted : List (HornerGroup n S)), + ∀ (groups sorted : List (HornerGroup σ S)), descendingByExponent sorted → descendingByExponent (groups.foldl (fun sorted group ↦ insertHornerGroupDesc group sorted) sorted) := by @@ -136,17 +136,17 @@ private lemma sortHornerGroups_descending {n : ℕ} {S : Type*} (insertHornerGroupDesc_pairwise group sorted hsorted) exact hsort groups [] (by simp [descendingByExponent]) -private lemma hornerGroups_descending {n : ℕ} {S : Type*} - (k : ℕ) (terms : List (HornerTerm n S)) : +private lemma hornerGroups_descending {σ : Type*} [FinEnum σ] {S : Type*} + (k : ℕ) (terms : List (HornerTerm σ S)) : descendingByExponent (hornerGroups k terms) := by unfold hornerGroups exact sortHornerGroups_descending (collectHornerGroups k terms) /-! ### Grouping preserves weighted sums -/ -private lemma groupWeightedSpec_insertHornerGroupDesc {n : ℕ} {S : Type*} - [CommSemiring S] (weight : HornerTerm n S → S) (x : S) - (group : HornerGroup n S) : +private lemma groupWeightedSpec_insertHornerGroupDesc {σ : Type*} [FinEnum σ] {S : Type*} + [CommSemiring S] (weight : HornerTerm σ S → S) (x : S) + (group : HornerGroup σ S) : ∀ groups, ((insertHornerGroupDesc group groups).map (groupWeightedSpec weight x)).sum = groupWeightedSpec weight x group + (groups.map (groupWeightedSpec weight x)).sum := by @@ -161,9 +161,9 @@ private lemma groupWeightedSpec_insertHornerGroupDesc {n : ℕ} {S : Type*} rw [ih] simp [add_assoc, add_left_comm, add_comm] -private lemma groupWeightedSpec_sortGroups {n : ℕ} {S : Type*} - [CommSemiring S] (weight : HornerTerm n S → S) (x : S) : - ∀ (groups sorted : List (HornerGroup n S)), +private lemma groupWeightedSpec_sortGroups {σ : Type*} [FinEnum σ] {S : Type*} + [CommSemiring S] (weight : HornerTerm σ S → S) (x : S) : + ∀ (groups sorted : List (HornerGroup σ S)), ((groups.foldl (fun sorted group ↦ insertHornerGroupDesc group sorted) sorted).map (groupWeightedSpec weight x)).sum = (groups.map (groupWeightedSpec weight x)).sum + @@ -180,9 +180,9 @@ private lemma groupWeightedSpec_sortGroups {n : ℕ} {S : Type*} rw [groupWeightedSpec_insertHornerGroupDesc] simp [add_left_comm, add_comm] -private lemma groupWeightedSpec_insertHornerTerm {n : ℕ} {S : Type*} - [CommSemiring S] (k : ℕ) (weight : HornerTerm n S → S) (x : S) - (term : HornerTerm n S) : +private lemma groupWeightedSpec_insertHornerTerm {σ : Type*} [FinEnum σ] {S : Type*} + [CommSemiring S] (k : ℕ) (weight : HornerTerm σ S → S) (x : S) + (term : HornerTerm σ S) : ∀ groups, ((insertHornerTerm (hornerExponent k term.1) term groups).map (groupWeightedSpec weight x)).sum = @@ -204,9 +204,9 @@ private lemma groupWeightedSpec_insertHornerTerm {n : ℕ} {S : Type*} rw [ih] simp [add_assoc, add_comm] -private lemma groupWeightedSpec_groupTerms {n : ℕ} {S : Type*} - [CommSemiring S] (k : ℕ) (weight : HornerTerm n S → S) (x : S) : - ∀ (terms : List (HornerTerm n S)) groups, +private lemma groupWeightedSpec_groupTerms {σ : Type*} [FinEnum σ] {S : Type*} + [CommSemiring S] (k : ℕ) (weight : HornerTerm σ S → S) (x : S) : + ∀ (terms : List (HornerTerm σ S)) groups, (((terms.foldl (fun groups term ↦ insertHornerTerm (hornerExponent k term.1) term groups) groups).map (groupWeightedSpec weight x)).sum) = @@ -224,27 +224,27 @@ private lemma groupWeightedSpec_groupTerms {n : ℕ} {S : Type*} simp [termsWeightedSpec] simp [add_assoc, add_left_comm, add_comm] -private lemma groupWeightedSpec_sortHornerGroups {n : ℕ} {S : Type*} - [CommSemiring S] (weight : HornerTerm n S → S) (x : S) - (groups : List (HornerGroup n S)) : +private lemma groupWeightedSpec_sortHornerGroups {σ : Type*} [FinEnum σ] {S : Type*} + [CommSemiring S] (weight : HornerTerm σ S → S) (x : S) + (groups : List (HornerGroup σ S)) : ((sortHornerGroups groups).map (groupWeightedSpec weight x)).sum = (groups.map (groupWeightedSpec weight x)).sum := by unfold sortHornerGroups rw [groupWeightedSpec_sortGroups] simp -private lemma groupWeightedSpec_collectHornerGroups {n : ℕ} {S : Type*} - [CommSemiring S] (k : ℕ) (weight : HornerTerm n S → S) (x : S) - (terms : List (HornerTerm n S)) : +private lemma groupWeightedSpec_collectHornerGroups {σ : Type*} [FinEnum σ] {S : Type*} + [CommSemiring S] (k : ℕ) (weight : HornerTerm σ S → S) (x : S) + (terms : List (HornerTerm σ S)) : ((collectHornerGroups k terms).map (groupWeightedSpec weight x)).sum = termsWeightedSpec k weight x terms := by unfold collectHornerGroups rw [groupWeightedSpec_groupTerms] simp -private lemma groupWeightedSpec_hornerGroups {n : ℕ} {S : Type*} - [CommSemiring S] (k : ℕ) (weight : HornerTerm n S → S) (x : S) - (terms : List (HornerTerm n S)) : +private lemma groupWeightedSpec_hornerGroups {σ : Type*} [FinEnum σ] {S : Type*} + [CommSemiring S] (k : ℕ) (weight : HornerTerm σ S → S) (x : S) + (terms : List (HornerTerm σ S)) : ((hornerGroups k terms).map (groupWeightedSpec weight x)).sum = termsWeightedSpec k weight x terms := by unfold hornerGroups @@ -333,13 +333,13 @@ private lemma descendingByExponent_map {α β : Type*} (f : α → β) : rcases hy with ⟨group', hgroup', rfl⟩ exact hsorted.1 group' hgroup' -private lemma eval₂HornerTerms_eq_eval₂HornerTermsSpec {n : ℕ} {S : Type*} +private lemma eval₂HornerTerms_eq_eval₂HornerTermsSpec {σ : Type*} [FinEnum σ] {S : Type*} [CommSemiring S] (xs : ℕ → S) : - ∀ fuel k (terms : List (HornerTerm n S)), + ∀ fuel k (terms : List (HornerTerm σ S)), eval₂HornerTerms xs fuel k terms = eval₂HornerTermsSpec xs fuel k terms | 0, k, terms => by simp only [eval₂HornerTerms, eval₂HornerTermsSpec, eval₂HornerTermSpec] - rw [foldl_add_eq_add_sum (fun term : HornerTerm n S ↦ term.2)] + rw [foldl_add_eq_add_sum (fun term : HornerTerm σ S ↦ term.2)] simp | fuel + 1, k, terms => by unfold eval₂HornerTerms @@ -354,7 +354,7 @@ private lemma eval₂HornerTerms_eq_eval₂HornerTermsSpec {n : ℕ} {S : Type*} = ((hornerGroups k terms).map (groupWeightedSpec - (fun term : HornerTerm n S ↦ + (fun term : HornerTerm σ S ↦ eval₂HornerTermSpec xs fuel (k + 1) term) (xs k))).sum := by apply congrArg List.sum @@ -365,10 +365,10 @@ private lemma eval₂HornerTerms_eq_eval₂HornerTermsSpec {n : ℕ} {S : Type*} rw [eval₂HornerTerms_eq_eval₂HornerTermsSpec xs fuel (k + 1) group.2] rfl _ = termsWeightedSpec k - (fun term : HornerTerm n S ↦ eval₂HornerTermSpec xs fuel (k + 1) term) + (fun term : HornerTerm σ S ↦ eval₂HornerTermSpec xs fuel (k + 1) term) (xs k) terms := by exact groupWeightedSpec_hornerGroups k - (fun term : HornerTerm n S ↦ + (fun term : HornerTerm σ S ↦ eval₂HornerTermSpec xs fuel (k + 1) term) (xs k) terms _ = (List.map (eval₂HornerTermSpec xs (fuel + 1) k) terms).sum := by @@ -378,9 +378,9 @@ private lemma eval₂HornerTerms_eq_eval₂HornerTermsSpec {n : ℕ} {S : Type*} (fun terms ↦ eval₂HornerTerms xs fuel (k + 1) terms) (hornerGroups k terms) (hornerGroups_descending k terms) -private lemma eval₂HornerTermSpec_eq_product {n : ℕ} {S : Type*} [CommSemiring S] +private lemma eval₂HornerTermSpec_eq_product {σ : Type*} [FinEnum σ] {S : Type*} [CommSemiring S] (xs : ℕ → S) : - ∀ fuel k (term : HornerTerm n S), + ∀ fuel k (term : HornerTerm σ S), eval₂HornerTermSpec xs fuel k term = term.2 * ∏ i : Fin fuel, xs (k + (i : ℕ)) ^ hornerExponent (k + (i : ℕ)) term.1 @@ -404,29 +404,35 @@ private lemma eval₂HornerTermSpec_eq_product {n : ℕ} {S : Type*} [CommSemiri rw [hprod] ac_rfl -private lemma eval₂HornerTermSpec_eq_evalMonomial {S : Type*} {n : ℕ} - [CommSemiring S] (vs : Fin n → S) (m : CMvMonomial n) (c : S) : +private lemma eval₂HornerTermSpec_eq_evalMonomial {σ : Type*} [FinEnum σ] {S : Type*} + [CommSemiring S] (vs : σ → S) (m : CMvMonomial σ) (c : S) : eval₂HornerTermSpec - (fun k ↦ if h : k < n then vs ⟨k, h⟩ else 0) n 0 (m, c) = + (fun k ↦ if h : k < FinEnum.card σ then vs (FinEnum.equiv.symm ⟨k, h⟩) else 0) + (FinEnum.card σ) 0 (m, c) = c * MonoR.evalMonomial vs m := by rw [eval₂HornerTermSpec_eq_product] congr 1 unfold MonoR.evalMonomial - apply Finset.prod_congr rfl - intro i _ + rw [← Equiv.prod_comp FinEnum.equiv.symm (fun j => vs j ^ Vector.get m (FinEnum.equiv j))] + refine Finset.prod_congr rfl (fun i _ => ?_) + have hi : (0 + (↑i : ℕ)) = ↑i := Nat.zero_add _ + have hlt : 0 + (↑i : ℕ) < FinEnum.card σ := by rw [hi]; exact i.2 + have hfin : (⟨0 + ↑i, hlt⟩ : Fin (FinEnum.card σ)) = i := by apply Fin.ext; exact hi + rw [dif_pos hlt, Equiv.apply_symm_apply, hfin] congr 1 - · simp - · unfold hornerExponent - simp [Vector.get] - rfl - -private lemma eval₂HornerTerms_fold_eq_eval₂_fold {R S : Type*} {n : ℕ} - [Semiring R] [CommSemiring S] (f : R →+* S) (vs : Fin n → S) : - ∀ (terms : List (CMvMonomial n × R)) (init : S), + unfold hornerExponent + rw [hi] + simp [Vector.get] + rfl + +private lemma eval₂HornerTerms_fold_eq_eval₂_fold {R S : Type*} {σ : Type*} [FinEnum σ] + [Semiring R] [CommSemiring S] (f : R →+* S) (vs : σ → S) : + ∀ (terms : List (CMvMonomial σ × R)) (init : S), (terms.map fun term ↦ (term.1, f term.2)).foldl (fun acc term ↦ acc + eval₂HornerTermSpec - (fun k ↦ if h : k < n then vs ⟨k, h⟩ else 0) n 0 term) + (fun k ↦ if h : k < FinEnum.card σ then vs (FinEnum.equiv.symm ⟨k, h⟩) else 0) + (FinEnum.card σ) 0 term) init = terms.foldl (fun acc term ↦ f term.2 * MonoR.evalMonomial vs term.1 + acc) @@ -444,8 +450,8 @@ private lemma eval₂HornerTerms_fold_eq_eval₂_fold {R S : Type*} {n : ℕ} exact ih (f term.2 * MonoR.evalMonomial vs term.1 + init) /-- Fixed-order multivariate Horner evaluation agrees with ordinary evaluation. -/ -theorem eval₂Horner_eq_eval₂ {R S : Type*} {n : ℕ} [Semiring R] [CommSemiring S] - (f : R →+* S) (vs : Fin n → S) (p : CMvPolynomial n R) : +theorem eval₂Horner_eq_eval₂ {R S : Type*} {σ : Type*} [FinEnum σ] [Semiring R] [CommSemiring S] + (f : R →+* S) (vs : σ → S) (p : CMvPolynomial σ R) : eval₂Horner f vs p = eval₂ f vs p := by unfold eval₂Horner eval₂ rw [eval₂HornerTerms_eq_eval₂HornerTermsSpec] @@ -453,26 +459,29 @@ theorem eval₂Horner_eq_eval₂ {R S : Type*} {n : ℕ} [Semiring R] [CommSemir have hfold : (List.map (eval₂HornerTermSpec - (fun k ↦ if h : k < n then vs ⟨k, h⟩ else 0) n 0) + (fun k ↦ if h : k < FinEnum.card σ then vs (FinEnum.equiv.symm ⟨k, h⟩) else 0) + (FinEnum.card σ) 0) (p.1.toList.map fun term ↦ (term.1, f term.2))).sum = (p.1.toList.map fun term ↦ (term.1, f term.2)).foldl (fun acc term ↦ acc + eval₂HornerTermSpec - (fun k ↦ if h : k < n then vs ⟨k, h⟩ else 0) n 0 term) + (fun k ↦ if h : k < FinEnum.card σ then vs (FinEnum.equiv.symm ⟨k, h⟩) else 0) + (FinEnum.card σ) 0 term) 0 := by simpa using (foldl_add_eq_add_sum - (fun term : HornerTerm n S ↦ + (fun term : HornerTerm σ S ↦ eval₂HornerTermSpec - (fun k ↦ if h : k < n then vs ⟨k, h⟩ else 0) n 0 term) + (fun k ↦ if h : k < FinEnum.card σ then vs (FinEnum.equiv.symm ⟨k, h⟩) else 0) + (FinEnum.card σ) 0 term) (p.1.toList.map fun term ↦ (term.1, f term.2)) 0).symm rw [hfold] rw [ExtTreeMap.foldl_eq_foldl_toList] exact eval₂HornerTerms_fold_eq_eval₂_fold f vs p.1.toList 0 /-- Fixed-order multivariate Horner evaluation agrees with ordinary evaluation. -/ -theorem evalHorner_eq_eval {R : Type*} {n : ℕ} [CommSemiring R] - (vs : Fin n → R) (p : CMvPolynomial n R) : +theorem evalHorner_eq_eval {R : Type*} {σ : Type*} [FinEnum σ] [CommSemiring R] + (vs : σ → R) (p : CMvPolynomial σ R) : evalHorner vs p = eval vs p := by exact eval₂Horner_eq_eval₂ (RingHom.id R) vs p diff --git a/CompPoly/Multivariate/Lawful.lean b/CompPoly/Multivariate/Lawful.lean index 003856bd..b1e60893 100644 --- a/CompPoly/Multivariate/Lawful.lean +++ b/CompPoly/Multivariate/Lawful.lean @@ -16,7 +16,7 @@ computable multivariate polynomials. ## Main definitions -* `CPoly.Lawful n R`: The subtype of `Unlawful n R` with no zero coefficients. +* `CPoly.Lawful σ R`: The subtype of `Unlawful σ R` with no zero coefficients. -/ set_option allowUnsafeReducibility true in attribute [local reducible] instDecidableEqOfLawfulBEq @@ -27,26 +27,26 @@ namespace CPoly open Std /-- The subtype of polynomials with no zero coefficients. -/ -def Lawful (n : ℕ) (R : Type*) [Zero R] : Type _ := - {p : Unlawful n R // p.isNoZeroCoef} +def Lawful (σ : Type*) [FinEnum σ] (R : Type*) [Zero R] : Type _ := + {p : Unlawful σ R // p.isNoZeroCoef} -variable {n : ℕ} {R : Type*} [Zero R] +variable {σ : Type*} [FinEnum σ] {R : Type*} [Zero R] section Instances @[grind=] -instance instEmptyCol : EmptyCollection (Lawful n R) := ⟨∅, by grind⟩ +instance instEmptyCol : EmptyCollection (Lawful σ R) := ⟨∅, by grind⟩ -instance : GetElem (Lawful n R) (CMvMonomial n) R (fun lp m ↦ m ∈ lp.1) := +instance : GetElem (Lawful σ R) (CMvMonomial σ) R (fun lp m ↦ m ∈ lp.1) := ⟨fun lp m h ↦ lp.1[m]'h⟩ -instance : GetElem? (Lawful n R) (CMvMonomial n) R (fun lp m ↦ m ∈ lp.1) := +instance : GetElem? (Lawful σ R) (CMvMonomial σ) R (fun lp m ↦ m ∈ lp.1) := ⟨fun lp m ↦ lp.1[m]?, fun lp m ↦ lp.1[m]!⟩ -instance : Membership (CMvMonomial n) (Lawful n R) := +instance : Membership (CMvMonomial σ) (Lawful σ R) := ⟨fun lp m ↦ m ∈ lp.1⟩ -instance : LawfulGetElem (Lawful n R) (CMvMonomial n) R (fun lp m ↦ m ∈ lp) := +instance : LawfulGetElem (Lawful σ R) (CMvMonomial σ) R (fun lp m ↦ m ∈ lp) := ⟨ fun ⟨c, hc⟩ i _ ↦ by have := getElem?_def c i; aesop, fun ⟨c, hc⟩ i ↦ by have := getElem!_def c i; aesop @@ -56,7 +56,7 @@ end Instances namespace Lawful -variable {p : Lawful n R} {m x : CMvMonomial n} +variable {p : Lawful σ R} {m x : CMvMonomial σ} @[simp, grind _=_] lemma getElem?_eq_val_getElem? : p[m]? = p.1[m]? := rfl @@ -85,35 +85,35 @@ lemma getElem_eq_getElem (h : m ∈ p) : p[m] = p.1[m] := by rfl variable [BEq R] [LawfulBEq R] /-- Convert an `Unlawful` polynomial to a `Lawful` one by filtering out zero coefficients. -/ -def fromUnlawful (p : Unlawful n R) : Lawful n R := +def fromUnlawful (p : Unlawful σ R) : Lawful σ R := { val := p.filter fun _ c ↦ c != 0 property _ := by aesop (add simp ExtTreeMap.getElem?_filter) (add safe (by grind)) } @[grind←] -protected lemma grind_fromUnlawful_congr {p₁ p₂ : Unlawful n R} +protected lemma grind_fromUnlawful_congr {p₁ p₂ : Unlawful σ R} (h : p₁ = p₂) : Lawful.fromUnlawful p₁ = Lawful.fromUnlawful p₂ := by grind /-- Construct a constant polynomial. -/ -def C (c : R) : Lawful n R := +def C (c : R) : Lawful σ R := ⟨Unlawful.C c, by grind⟩ -instance instOfNat_zero : OfNat (Lawful n R) 0 := ⟨C 0⟩ +instance instOfNat_zero : OfNat (Lawful σ R) 0 := ⟨C 0⟩ -lemma zero_def : Zero.zero (α := Lawful n R) = C 0 := rfl +lemma zero_def : Zero.zero (α := Lawful σ R) = C 0 := rfl -instance instOfNat {m : ℕ} [NeZero m] [NatCast R] : OfNat (Lawful n R) m := ⟨C m⟩ +instance instOfNat {m : ℕ} [NeZero m] [NatCast R] : OfNat (Lawful σ R) m := ⟨C m⟩ @[simp, grind =] -lemma C_zero : C (n := n) (0 : R) = 0 := rfl +lemma C_zero : C (σ := σ) (0 : R) = 0 := rfl @[simp, grind =] -lemma C_zero' : C (n := n) (0 : ℕ) = 0 := rfl +lemma C_zero' : C (σ := σ) (0 : ℕ) = 0 := rfl -lemma zero_eq_zero : (0 : Lawful n R) = ⟨0, by grind⟩ := rfl +lemma zero_eq_zero : (0 : Lawful σ R) = ⟨0, by grind⟩ := rfl -lemma zero_eq_empty : (0 : Lawful n R) = ∅ := by +lemma zero_eq_empty : (0 : Lawful σ R) = ∅ := by unfold_projs simp [C, Unlawful.zero_eq_empty] @@ -121,7 +121,7 @@ lemma zero_eq_empty : (0 : Lawful n R) = ∅ := by lemma not_mem_C_zero : x ∉ C 0 := by simp [zero_eq_empty]; unfold_projs; grind @[simp, grind .] -lemma not_mem_zero : x ∉ (0 : Lawful n R) := by rw [zero_eq_zero]; exact Unlawful.not_mem_zero +lemma not_mem_zero : x ∉ (0 : Lawful σ R) := by rw [zero_eq_zero]; exact Unlawful.not_mem_zero @[simp] lemma cast_fromUnlawful : (fromUnlawful p.1).1 = p.1 := by @@ -132,39 +132,35 @@ lemma cast_fromUnlawful : (fromUnlawful p.1).1 = p.1 := by section -/-- Extend the number of variables in a polynomial. -/ -def extend (n' : ℕ) (p : Lawful n R) : Lawful (max n n') R := - fromUnlawful <| p.val.extend n' - /-- Addition of polynomials (results in a lawful polynomial). -/ -def add [Add R] (p₁ p₂ : Lawful n R) : Lawful n R := +def add [Add R] (p₁ p₂ : Lawful σ R) : Lawful σ R := fromUnlawful <| p₁.val + p₂.val -instance [Add R] : Add (Lawful n R) := ⟨add⟩ +instance [Add R] : Add (Lawful σ R) := ⟨add⟩ @[grind=] -protected lemma grind_add_skip [Add R] {p₁ p₂ : Lawful n R} : +protected lemma grind_add_skip [Add R] {p₁ p₂ : Lawful σ R} : p₁ + p₂ = Lawful.fromUnlawful (p₁.1.add p₂.1) := rfl /-- Note to self: This goes too far. -/ @[grind=] -protected lemma grind_add_skip_aggressive [Add R] {p₁ p₂ : Lawful n R} : +protected lemma grind_add_skip_aggressive [Add R] {p₁ p₂ : Lawful σ R} : p₁ + p₂ = fromUnlawful (ExtTreeMap.mergeWith (fun _ c₁ c₂ => c₁ + c₂) p₁.1 p₂.1) := rfl /-- Multiplication of polynomials (results in a lawful polynomial). -/ -def mul [Mul R] [Add R] (p₁ p₂ : Lawful n R) : Lawful n R := +def mul [Mul R] [Add R] (p₁ p₂ : Lawful σ R) : Lawful σ R := fromUnlawful <| p₁.val * p₂.val -instance [Mul R] [Add R] [Zero R] : Mul (Lawful n R) := ⟨mul⟩ +instance [Mul R] [Add R] [Zero R] : Mul (Lawful σ R) := ⟨mul⟩ /-- Polynomial exponentiation via repeated multiplication. `O(k)` multiplications. This is the specification; `npowBySq` is the efficient `O(log k)` implementation used by the `NatPow` instance once the equivalence with this naive form has been proven. -/ -def npow [NatCast R] [Add R] [Mul R] : ℕ → Lawful n R → Lawful n R +def npow [NatCast R] [Add R] [Mul R] : ℕ → Lawful σ R → Lawful σ R | .zero , _ => 1 | .succ n, p => (npow n p) * p @@ -177,7 +173,7 @@ For `k > 0`, computes `p ^ k` by recursing on `k / 2`: Equivalent to `npow` (see `npowBySq_eq_npow`). -/ @[inline, specialize] -def npowBySq [NatCast R] [Add R] [Mul R] (p : Lawful n R) : ℕ → Lawful n R +def npowBySq [NatCast R] [Add R] [Mul R] (p : Lawful σ R) : ℕ → Lawful σ R | 0 => 1 | k + 1 => let half := npowBySq p ((k + 1) / 2) @@ -185,29 +181,29 @@ def npowBySq [NatCast R] [Add R] [Mul R] (p : Lawful n R) : ℕ → Lawful n R if (k + 1) % 2 = 0 then sq else p * sq decreasing_by omega -instance [NatCast R] [Add R] [Mul R] : NatPow (Lawful n R) := ⟨fun e b ↦ npow b e⟩ +instance [NatCast R] [Add R] [Mul R] : NatPow (Lawful σ R) := ⟨fun e b ↦ npow b e⟩ /-- The list of monomials in a polynomial. -/ -abbrev monomials (p : Lawful n R) : List (CMvMonomial n) := +abbrev monomials (p : Lawful σ R) : List (CMvMonomial σ) := p.1.monomials /-- Check if a polynomial is a non-zero constant. -/ -def NzConst {n : ℕ} {R : Type*} [Zero R] (p : Lawful n R) : Prop := +def NzConst {σ : Type*} [FinEnum σ] {R : Type*} [Zero R] (p : Lawful σ R) : Prop := p.val.size = 1 ∧ p.val.contains CMvMonomial.zero omit [BEq R] [LawfulBEq R] in @[simp, grind _=_] -lemma mem_monomials_iff {w : CMvMonomial n} : w ∈ Lawful.monomials p ↔ w ∈ p := by +lemma mem_monomials_iff {w : CMvMonomial σ} : w ∈ Lawful.monomials p ↔ w ∈ p := by grind -instance {p : Lawful n R} : Decidable (NzConst p) := by +instance {p : Lawful σ R} : Decidable (NzConst p) := by dsimp [NzConst] infer_instance end @[simp, grind=] -lemma fromUnlawful_cast {p : Lawful n R} : fromUnlawful p.1 = p := by +lemma fromUnlawful_cast {p : Lawful σ R} : fromUnlawful p.1 = p := by unfold fromUnlawful congr rcases p with ⟨p, hp⟩ @@ -219,77 +215,24 @@ section variable [BEq R] [LawfulBEq R] /-- Negation of a polynomial. -/ -def neg [Neg R] (p : Lawful n R) : Lawful n R := +def neg [Neg R] (p : Lawful σ R) : Lawful σ R := fromUnlawful p.1.neg -instance [Neg R] : Neg (Lawful n R) := ⟨neg⟩ +instance [Neg R] : Neg (Lawful σ R) := ⟨neg⟩ /-- Subtraction of polynomials. -/ -def sub [Add R] [Neg R] (p₁ p₂ : Lawful n R) : Lawful n R := +def sub [Add R] [Neg R] (p₁ p₂ : Lawful σ R) : Lawful σ R := p₁ + (-p₂) -instance [Add R] [Neg R] : Sub (Lawful n R) := ⟨sub⟩ +instance [Add R] [Neg R] : Sub (Lawful σ R) := ⟨sub⟩ -instance instDecidableEq [DecidableEq R] : DecidableEq (Lawful n R) := fun x y ↦ +instance instDecidableEq [DecidableEq R] : DecidableEq (Lawful σ R) := fun x y ↦ if h : x.1.toList = y.1.toList then Decidable.isTrue (by have := ExtTreeMap.ext_toList (t₁ := x.1) (t₂ := y.1) simp_rw [Subtype.val_inj] at this grind) else Decidable.isFalse (by grind) -/-- The $i$-th variable as a polynomial. -/ -def X (i : ℕ) : Lawful (i + 1) ℤ := - let monomial : CMvMonomial (i + 1) := Vector.replicate i 0 |>.push 1 - Lawful.fromUnlawful <| .ofList [(monomial, (1 : ℤ))] - -section - -variable {n₁ n₂ : ℕ} - -/-- Align two polynomials by extending them to have the same number of variables. -/ -def align - (p₁ : Lawful n₁ R) (p₂ : Lawful n₂ R) : - Lawful (n₁ ⊔ n₂) R × Lawful (n₁ ⊔ n₂) R := - letI sup := n₁ ⊔ n₂ - ( - cast (by congr 1; grind) (p₁.extend sup), - cast (by congr 1; grind) (p₂.extend sup) - ) - -/-- Lift a binary polynomial operation to handle polynomials with different numbers of variables. -/ -def liftPoly - (f : Lawful (n₁ ⊔ n₂) R → - Lawful (n₁ ⊔ n₂) R → - Lawful (n₁ ⊔ n₂) R) - (p₁ : Lawful n₁ R) (p₂ : Lawful n₂ R) : Lawful (n₁ ⊔ n₂) R := - Function.uncurry f (align p₁ p₂) - -def polyCoe (p : Lawful n R) : Lawful (n + 1) R := cast (by simp) (p.extend n.succ) - -instance : Coe (Lawful n R) (Lawful (n + 1) R) := ⟨polyCoe⟩ - -section - --- Mixed-arity fallbacks: keep these low-priority so same-arity `Add`/`Sub`/`Mul` --- instances win when both operands already live in `Lawful n R`. --- We intentionally do not add an `HPow` fallback here: exponentiation is unary, preserves --- arity, and is already handled above by the same-arity `NatPow (Lawful n R)` instance. -instance (priority := low) [Add R] : - HAdd (Lawful n₁ R) (Lawful n₂ R) (Lawful (n₁ ⊔ n₂) R) := - ⟨fun p₁ p₂ ↦ liftPoly (·+·) p₁ p₂⟩ - -instance (priority := low) [Add R] [Neg R] : - HSub (Lawful n₁ R) (Lawful n₂ R) (Lawful (n₁ ⊔ n₂) R) := - ⟨fun p₁ p₂ ↦ liftPoly (·-·) p₁ p₂⟩ - -instance (priority := low) [Add R] [Mul R] : - HMul (Lawful n₁ R) (Lawful n₂ R) (Lawful (n₁ ⊔ n₂) R) := - ⟨fun p₁ p₂ ↦ liftPoly (·*·) p₁ p₂⟩ - -end - -end - end end Lawful diff --git a/CompPoly/Multivariate/MvPolyEquiv/Core.lean b/CompPoly/Multivariate/MvPolyEquiv/Core.lean index 37f12aac..2a27ced0 100644 --- a/CompPoly/Multivariate/MvPolyEquiv/Core.lean +++ b/CompPoly/Multivariate/MvPolyEquiv/Core.lean @@ -25,15 +25,15 @@ open CMvPolynomial section -variable {n : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] +variable {σ : Type*} [FinEnum σ] {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] -def fromCMvPolynomial (p : CMvPolynomial n R) : MvPolynomial (Fin n) R := - let support : List (Fin n →₀ ℕ) := p.monomials.map CMvMonomial.toFinsupp - let toFun (f : Fin n →₀ ℕ) : R := p[CMvMonomial.ofFinsupp f]?.getD 0 - let mem_support_fun {a : Fin n →₀ ℕ} : a ∈ support ↔ toFun a ≠ 0 := by grind +def fromCMvPolynomial (p : CMvPolynomial σ R) : MvPolynomial σ R := + let support : List (σ →₀ ℕ) := p.monomials.map CMvMonomial.toFinsupp + let toFun (f : σ →₀ ℕ) : R := p[CMvMonomial.ofFinsupp f]?.getD 0 + let mem_support_fun {a : σ →₀ ℕ} : a ∈ support ↔ toFun a ≠ 0 := by grind Finsupp.mk support.toFinset toFun (by simp [mem_support_fun]) -noncomputable def toCMvPolynomial (p : MvPolynomial (Fin n) R) : CMvPolynomial n R := +noncomputable def toCMvPolynomial (p : MvPolynomial σ R) : CMvPolynomial σ R := let ⟨s, f, _⟩ := p let unlawful := .ofList <| s.toList.map fun m ↦ (CMvMonomial.ofFinsupp m, f m) ⟨ @@ -61,11 +61,12 @@ noncomputable def toCMvPolynomial (p : MvPolynomial (Fin n) R) : CMvPolynomial n grind ⟩ -instance {n : ℕ} {R : Type*} : Membership (Vector ℕ n) (Unlawful n R) := inferInstance +instance {σ : Type*} [FinEnum σ] {R : Type*} : + Membership (Vector ℕ (FinEnum.card σ)) (Unlawful σ R) := inferInstance omit [BEq R] [LawfulBEq R] in @[grind =, simp] -theorem toCMvPolynomial_fromCMvPolynomial {p : CMvPolynomial n R} : +theorem toCMvPolynomial_fromCMvPolynomial {p : CMvPolynomial σ R} : toCMvPolynomial (fromCMvPolynomial p) = p := by unfold fromCMvPolynomial toCMvPolynomial dsimp @@ -83,7 +84,7 @@ theorem toCMvPolynomial_fromCMvPolynomial {p : CMvPolynomial n R} : omit [BEq R] [LawfulBEq R] in @[grind =, simp] -theorem fromCMvPolynomial_toCMvPolynomial {p : MvPolynomial (Fin n) R} : +theorem fromCMvPolynomial_toCMvPolynomial {p : MvPolynomial σ R} : fromCMvPolynomial (toCMvPolynomial p) = p := by dsimp [fromCMvPolynomial, toCMvPolynomial, toCMvPolynomial, fromCMvPolynomial] ext m; simp [MvPolynomial.coeff] @@ -107,26 +108,27 @@ theorem fromCMvPolynomial_toCMvPolynomial {p : MvPolynomial (Fin n) R} : · have : ∀ x ∈ s, CMvMonomial.ofFinsupp x ≠ CMvMonomial.ofFinsupp m := by aesop grind -lemma fromCMvPolynomial_injective : Function.Injective (@fromCMvPolynomial n R _) := by +lemma fromCMvPolynomial_injective : + Function.Injective (fromCMvPolynomial (σ := σ) (R := R)) := by rw [Function.injective_iff_hasLeftInverse] exists toCMvPolynomial apply toCMvPolynomial_fromCMvPolynomial omit [BEq R] [LawfulBEq R] in -lemma coeff_eq {m} (a : CMvPolynomial n R) : +lemma coeff_eq {m} (a : CMvPolynomial σ R) : MvPolynomial.coeff m (fromCMvPolynomial a) = a.coeff (CMvMonomial.ofFinsupp m) := rfl @[aesop simp] -lemma eq_iff_fromCMvPolynomial {u v: CMvPolynomial n R} : +lemma eq_iff_fromCMvPolynomial {u v: CMvPolynomial σ R} : u = v ↔ fromCMvPolynomial u = fromCMvPolynomial v := by constructor · intro h exact congrArg fromCMvPolynomial h · intro h - exact (fromCMvPolynomial_injective (n := n) (R := R)) h + exact (fromCMvPolynomial_injective (σ := σ) (R := R)) h noncomputable def polyEquiv : - Equiv (CMvPolynomial n R) (MvPolynomial (Fin n) R) where + Equiv (CMvPolynomial σ R) (MvPolynomial σ R) where toFun := fromCMvPolynomial invFun := toCMvPolynomial left_inv := fun _ ↦ toCMvPolynomial_fromCMvPolynomial diff --git a/CompPoly/Multivariate/MvPolyEquiv/Eval.lean b/CompPoly/Multivariate/MvPolyEquiv/Eval.lean index 2fcf8f2d..637f5aa7 100644 --- a/CompPoly/Multivariate/MvPolyEquiv/Eval.lean +++ b/CompPoly/Multivariate/MvPolyEquiv/Eval.lean @@ -19,11 +19,11 @@ open CMvPolynomial section -variable {n : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] +variable {σ : Type*} [FinEnum σ] {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] omit [BEq R] [LawfulBEq R] in -lemma eval₂_equiv {S : Type*} {p : CMvPolynomial n R} [CommSemiring S] {f : (R →+* S)} - {vals : Fin n → S} : p.eval₂ f vals = (fromCMvPolynomial p).eval₂ f vals := by +lemma eval₂_equiv {S : Type*} {p : CMvPolynomial σ R} [CommSemiring S] {f : (R →+* S)} + {vals : σ → S} : p.eval₂ f vals = (fromCMvPolynomial p).eval₂ f vals := by unfold CMvPolynomial.eval₂ MvPolynomial.eval₂ rw [foldl_eq_sum] congr 1 @@ -39,25 +39,26 @@ lemma eval₂_equiv {S : Type*} {p : CMvPolynomial n R} [CommSemiring S] {f : (R simp only [Finset.mem_sdiff, Finset.mem_univ, Finsupp.mem_support_iff, ne_eq, Decidable.not_not, true_and] at h unfold CMvMonomial.ofFinsupp + rw [Vector.get_ofFn, Equiv.symm_apply_apply] simp [h] · intros x _ congr 1 unfold CMvMonomial.ofFinsupp - simp + rw [Vector.get_ofFn, Equiv.symm_apply_apply] omit [BEq R] [LawfulBEq R] in -lemma eval_equiv {p : CMvPolynomial n R} {vals : Fin n → R} : +lemma eval_equiv {p : CMvPolynomial σ R} {vals : σ → R} : p.eval vals = (fromCMvPolynomial p).eval vals := by unfold CMvPolynomial.eval MvPolynomial.eval MvPolynomial.eval₂Hom simp only [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk] exact eval₂_equiv omit [BEq R] [LawfulBEq R] in -lemma totalDegree_equiv {S : Type*} {p : CMvPolynomial n R} [CommSemiring S] : +lemma totalDegree_equiv {S : Type*} {p : CMvPolynomial σ R} [CommSemiring S] : p.totalDegree = (fromCMvPolynomial p).totalDegree := by rfl omit [BEq R] [LawfulBEq R] in -lemma degreeOf_equiv {S : Type*} {p : CMvPolynomial n R} [CommSemiring S] : +lemma degreeOf_equiv {S : Type*} {p : CMvPolynomial σ R} [CommSemiring S] : p.degreeOf = (fromCMvPolynomial p).degreeOf := by ext i rw [MvPolynomial.degreeOf_eq_sup] @@ -78,11 +79,11 @@ end namespace CMvPolynomial -variable {n : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] +variable {σ : Type*} [FinEnum σ] {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] /-- `eval₂` as a ring homomorphism. -/ def eval₂Hom {S : Type*} [CommSemiring S] - (f : R →+* S) (vs : Fin n → S) : CMvPolynomial n R →+* S where + (f : R →+* S) (vs : σ → S) : CMvPolynomial σ R →+* S where toFun := eval₂ f vs map_zero' := by simp [eval₂_equiv] map_one' := by simp [eval₂_equiv] @@ -91,7 +92,7 @@ def eval₂Hom {S : Type*} [CommSemiring S] @[simp] lemma eval₂Hom_apply {S : Type*} [CommSemiring S] - (f : R →+* S) (vs : Fin n → S) (p : CMvPolynomial n R) : + (f : R →+* S) (vs : σ → S) (p : CMvPolynomial σ R) : eval₂Hom f vs p = eval₂ f vs p := rfl end CMvPolynomial diff --git a/CompPoly/Multivariate/MvPolyEquiv/Instances.lean b/CompPoly/Multivariate/MvPolyEquiv/Instances.lean index a20962c4..5a5ff88a 100644 --- a/CompPoly/Multivariate/MvPolyEquiv/Instances.lean +++ b/CompPoly/Multivariate/MvPolyEquiv/Instances.lean @@ -19,10 +19,10 @@ open CMvPolynomial section -variable {n : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] +variable {σ : Type*} [FinEnum σ] {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] @[simp] -lemma map_add (a b : CMvPolynomial n R) : +lemma map_add (a b : CMvPolynomial σ R) : fromCMvPolynomial (a + b) = fromCMvPolynomial a + fromCMvPolynomial b := by ext m rw [MvPolynomial.coeff_add, coeff_eq, coeff_eq, coeff_eq] @@ -72,7 +72,7 @@ lemma map_add (a b : CMvPolynomial n R) : rfl @[simp] -lemma map_zero : fromCMvPolynomial (0 : CMvPolynomial n R) = 0 := by +lemma map_zero : fromCMvPolynomial (0 : CMvPolynomial σ R) = 0 := by ext m rw [MvPolynomial.coeff_zero] unfold fromCMvPolynomial @@ -88,12 +88,13 @@ instance : TransCmp (fun x y ↦ compareOfLessAndEq (α := ℕ) x y) where eq_swap {a b} := by apply compareOfLessAndEq_eq_swap <;> omega isLE_trans {a b c} h₁ h₂ := by rw [isLE_compareOfLessAndEq] at * <;> omega -instance {n : ℕ} : TransCmp (α := CMvMonomial n) - (Vector.compareLex (n := n) fun x y => compareOfLessAndEq (α := ℕ) x y) := - inferInstanceAs (TransCmp (Vector.compareLex (n := n) fun x y => compareOfLessAndEq (α := ℕ) x y)) +instance {σ : Type*} [FinEnum σ] : TransCmp (α := CMvMonomial σ) + (Vector.compareLex (n := FinEnum.card σ) fun x y => compareOfLessAndEq (α := ℕ) x y) := + inferInstanceAs (TransCmp (Vector.compareLex (n := FinEnum.card σ) + fun x y => compareOfLessAndEq (α := ℕ) x y)) @[simp] -lemma map_one : fromCMvPolynomial (1 : CMvPolynomial n R) = 1 := by +lemma map_one : fromCMvPolynomial (1 : CMvPolynomial σ R) = 1 := by ext m have : MvPolynomial.coeff m 1 = if m = 0 then 1 else (0 : R) := by unfold MvPolynomial.coeff @@ -121,35 +122,24 @@ lemma map_one : fromCMvPolynomial (1 : CMvPolynomial n R) = 1 := by · rw [Nat.cast_one] at g; apply triv_lem g · rw [Nat.cast_one] at g; apply triv_lem g · have finsupp_m_eq_one : CMvMonomial.ofFinsupp m = CMvMonomial.zero := by - rw [g'] - unfold CMvMonomial.ofFinsupp CMvMonomial.zero - ext i hi - show (Vector.ofFn (⇑(0 : Fin n →₀ ℕ)))[i] = (Vector.replicate n 0)[i] - simp only [Finsupp.coe_zero, Pi.zero_apply, Vector.getElem_ofFn, Vector.getElem_replicate] + rw [g']; exact CMvMonomial.ofFinsupp_zero rw [finsupp_m_eq_one] have one_one_get₁ : - ({(CMvMonomial.zero, 1)} : Unlawful n R)[(@CMvMonomial.zero n)]?.getD 0 = One.one := by + ({(CMvMonomial.zero, 1)} : Unlawful σ R)[(CMvMonomial.zero (σ := σ))]?.getD 0 = One.one := by unfold_projs; simp only [ExtTreeMap.empty_eq_emptyc, ExtTreeMap.get?_eq_getElem?, ExtTreeMap.getElem?_insert_self, Unlawful.zero_eq_zero, Option.getD_some] convert one_one_get₁ · have hne : CMvMonomial.ofFinsupp m ≠ CMvMonomial.zero := by - unfold CMvMonomial.ofFinsupp CMvMonomial.zero - intros h - have {i} : (Vector.ofFn m).get i = (Vector.replicate n 0).get i := by - rw [h] - apply g' - ext i - simp only [Finsupp.coe_mk] - simp only [Vector.get_ofFn, Vector.get_replicate] at this - exact this - show ((Unlawful.ofList [(MonoR.C (1 : R) : MonoR n R)])[CMvMonomial.ofFinsupp m]?.getD 0 : R) + rw [← CMvMonomial.ofFinsupp_zero] + exact fun h => g' (CMvMonomial.injective_ofFinsupp h) + show ((Unlawful.ofList [(MonoR.C (1 : R) : MonoR σ R)])[CMvMonomial.ofFinsupp m]?.getD 0 : R) = 0 erw [ExtTreeMap.getElem?_ofList_of_contains_eq_false (by simp [hne])] rfl attribute [local grind=] Unlawful.add Lawful.add Unlawful.mul Lawful.mul -instance {n : ℕ} : AddCommSemigroup (CPoly.CMvPolynomial n R) where +instance {σ : Type*} [FinEnum σ] : AddCommSemigroup (CPoly.CMvPolynomial σ R) where add_assoc a b c := by apply fromCMvPolynomial_injective simp [add_assoc] @@ -157,7 +147,7 @@ instance {n : ℕ} : AddCommSemigroup (CPoly.CMvPolynomial n R) where apply fromCMvPolynomial_injective simp [add_comm] -instance {n : ℕ} : AddMonoid (CPoly.CMvPolynomial n R) where +instance {σ : Type*} [FinEnum σ] : AddMonoid (CPoly.CMvPolynomial σ R) where zero_add a := by apply fromCMvPolynomial_injective simp @@ -166,7 +156,7 @@ instance {n : ℕ} : AddMonoid (CPoly.CMvPolynomial n R) where simp nsmul := nsmulRec -instance {n : ℕ} : AddCommMonoid (CPoly.CMvPolynomial n R) where +instance {σ : Type*} [FinEnum σ] : AddCommMonoid (CPoly.CMvPolynomial σ R) where toAddMonoid := inferInstance add_comm a b := by apply fromCMvPolynomial_injective @@ -174,8 +164,8 @@ instance {n : ℕ} : AddCommMonoid (CPoly.CMvPolynomial n R) where omit [BEq R] [LawfulBEq R] in lemma toList_pairs_monomial_coeff {β : Type*} [AddCommMonoid β] - {t : Unlawful n R} - {f : CMvMonomial n → R → β} : + {t : Unlawful σ R} + {f : CMvMonomial σ → R → β} : t.toList.map (fun term => f term.1 term.2) = t.monomials.map (fun m => f m (t.coeff m)) := by unfold Unlawful.monomials Unlawful.coeff @@ -185,8 +175,8 @@ lemma toList_pairs_monomial_coeff {β : Type*} [AddCommMonoid β] omit [BEq R] [LawfulBEq R] in lemma foldl_eq_sum {β : Type*} [AddCommMonoid β] - {t : CMvPolynomial n R} - {f : CMvMonomial n → R → β} : + {t : CMvPolynomial σ R} + {f : CMvMonomial σ → R → β} : ExtTreeMap.foldl (fun x m c => (f m c) + x) 0 t.1 = Finsupp.sum (fromCMvPolynomial t) (f ∘ CMvMonomial.ofFinsupp) := by unfold Finsupp.sum Finset.sum @@ -206,8 +196,8 @@ lemma foldl_eq_sum {β : Type*} [AddCommMonoid β] lemma coeff_sum [AddCommMonoid α] (s : Finset α) - (f : α → CMvPolynomial n R) - (m : CMvMonomial n) : + (f : α → CMvPolynomial σ R) + (m : CMvMonomial σ) : coeff m (∑ x ∈ s, f x) = ∑ x ∈ s, coeff m (f x) := by rw [←Finset.sum_map_toList s, ←Finset.sum_map_toList s] induction' s.toList with h t ih @@ -216,31 +206,31 @@ lemma coeff_sum [AddCommMonoid α] congr lemma fromCMvPolynomial_sum_eq_sum_fromCMvPolynomial - {f : (Fin n →₀ ℕ) → R → Lawful n R } - {a : CMvPolynomial n R} : + {f : (σ →₀ ℕ) → R → Lawful σ R } + {a : CMvPolynomial σ R} : fromCMvPolynomial (Finsupp.sum (fromCMvPolynomial a) f) = Finsupp.sum (fromCMvPolynomial a) (fun m c ↦ fromCMvPolynomial (f m c)) := by unfold Finsupp.sum; ext simp [MvPolynomial.coeff_sum, coeff_eq, coeff_sum] @[simp] -lemma map_mul (a b : CMvPolynomial n R) : +lemma map_mul (a b : CMvPolynomial σ R) : fromCMvPolynomial (a * b) = fromCMvPolynomial a * fromCMvPolynomial b := by dsimp only [HMul.hMul, Mul.mul, Lawful.mul, Unlawful.mul] simp only [CMvPolynomial.fromUnlawful_fold_eq_fold_fromUnlawful] unfold MonoidAlgebra.mul' rw [foldl_eq_sum]; simp_rw [foldl_eq_sum] - let F₀ (p q) : CMvMonomial n → R → Lawful n R := + let F₀ (p q) : CMvMonomial σ → R → Lawful σ R := fun p_1 q_1 ↦ Lawful.fromUnlawful {(p + p_1 , q * q_1)} - set F₁ : (Fin n →₀ ℕ) → R → Lawful n R := + set F₁ : (σ →₀ ℕ) → R → Lawful σ R := (fun p q ↦ Finsupp.sum (fromCMvPolynomial b) (F₀ p q ∘ CMvMonomial.ofFinsupp)) ∘ CMvMonomial.ofFinsupp with eqF₁ let F₂ a₁ b₁ : - Multiplicative (Fin n →₀ ℕ) → R → MonoidAlgebra R (Multiplicative (Fin n →₀ ℕ)) := + Multiplicative (σ →₀ ℕ) → R → MonoidAlgebra R (Multiplicative (σ →₀ ℕ)) := fun a₂ b₂ ↦ MonoidAlgebra.single (a₁ * a₂) (b₁ * b₂) - set F₃ : Multiplicative (Fin n →₀ ℕ) → R → MvPolynomial (Fin n) R := + set F₃ : Multiplicative (σ →₀ ℕ) → R → MvPolynomial σ R := fun a₁ b₁ ↦ Finsupp.sum (fromCMvPolynomial b) (F₂ a₁ b₁) with eqF₃ - have fromCMvPolynomial_F₁_eq_F₃ {m₁ : Multiplicative (Fin n →₀ ℕ)} {c₁ : R} : + have fromCMvPolynomial_F₁_eq_F₃ {m₁ : Multiplicative (σ →₀ ℕ)} {c₁ : R} : fromCMvPolynomial (F₁ m₁ c₁) = F₃ m₁ c₁ := by dsimp only [Function.comp_apply, F₁, F₀, F₃, F₂] rw [fromCMvPolynomial_sum_eq_sum_fromCMvPolynomial] @@ -273,11 +263,11 @@ lemma map_mul (a b : CMvPolynomial n R) : -- Lean 4.29 may beta-reduce F₃; fold it back then rewrite change fromCMvPolynomial (Finsupp.sum (fromCMvPolynomial a) F₁) = Finsupp.sum (fromCMvPolynomial a) F₃ - rw [show F₃ = fun σ x ↦ fromCMvPolynomial (F₁ σ x) from by + rw [show F₃ = fun m x ↦ fromCMvPolynomial (F₁ m x) from by ext x; rw [fromCMvPolynomial_F₁_eq_F₃]] rw [fromCMvPolynomial_sum_eq_sum_fromCMvPolynomial] -instance {n : ℕ} : MonoidWithZero (CPoly.CMvPolynomial n R) where +instance {σ : Type*} [FinEnum σ] : MonoidWithZero (CPoly.CMvPolynomial σ R) where zero_mul a := by apply fromCMvPolynomial_injective simp @@ -294,7 +284,7 @@ instance {n : ℕ} : MonoidWithZero (CPoly.CMvPolynomial n R) where apply fromCMvPolynomial_injective simp -instance {n : ℕ} : Semiring (CPoly.CMvPolynomial n R) where +instance {σ : Type*} [FinEnum σ] : Semiring (CPoly.CMvPolynomial σ R) where left_distrib {p q r} := by simp_all only [eq_iff_fromCMvPolynomial, map_mul, map_add] apply mul_add @@ -302,7 +292,7 @@ instance {n : ℕ} : Semiring (CPoly.CMvPolynomial n R) where simp_all only [eq_iff_fromCMvPolynomial, map_mul, map_add] apply add_mul -instance {n : ℕ} : CommSemiring (CPoly.CMvPolynomial n R) where +instance {σ : Type*} [FinEnum σ] : CommSemiring (CPoly.CMvPolynomial σ R) where natCast_zero := rfl natCast_succ := by intro n; simp npow_zero := by intro x; simp [npowRecAuto, npowRec] @@ -313,10 +303,10 @@ instance {n : ℕ} : CommSemiring (CPoly.CMvPolynomial n R) where section CommRing -variable {n : ℕ} {R : Type*} [CommRing R] [BEq R] [LawfulBEq R] +variable {σ : Type*} [FinEnum σ] {R : Type*} [CommRing R] [BEq R] [LawfulBEq R] @[simp] -lemma map_neg (a : CMvPolynomial n R) : +lemma map_neg (a : CMvPolynomial σ R) : fromCMvPolynomial (-a) = -fromCMvPolynomial a := by ext m simp only [MvPolynomial.coeff_neg, coeff_eq] @@ -329,13 +319,13 @@ lemma map_neg (a : CMvPolynomial n R) : | none => simp | some v => simp -lemma map_sub (a b : CMvPolynomial n R) : +lemma map_sub (a b : CMvPolynomial σ R) : fromCMvPolynomial (Sub.sub a b) = fromCMvPolynomial a - fromCMvPolynomial b := by change fromCMvPolynomial (Lawful.sub a b) = fromCMvPolynomial a - fromCMvPolynomial b unfold Lawful.sub rw [map_add, map_neg, sub_eq_add_neg] -instance : CommRing (CMvPolynomial n R) where +instance : CommRing (CMvPolynomial σ R) where neg_add_cancel a := by apply fromCMvPolynomial_injective simp [map_neg, map_add, map_zero] @@ -350,7 +340,7 @@ instance : CommRing (CMvPolynomial n R) where end CommRing noncomputable def polyRingEquiv : - RingEquiv (CPoly.CMvPolynomial n R) (MvPolynomial (Fin n) R) where + RingEquiv (CPoly.CMvPolynomial σ R) (MvPolynomial σ R) where toEquiv := CPoly.polyEquiv map_mul' := map_mul map_add' := map_add @@ -359,53 +349,48 @@ end namespace CMvPolynomial -variable {n : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] +variable {σ : Type*} [FinEnum σ] {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] -/-- Ring equivalence between `CMvPolynomial 0 R` and `R`. -/ -noncomputable def isEmptyRingEquiv : CMvPolynomial 0 R ≃+* R := - polyRingEquiv.trans (MvPolynomial.isEmptyAlgEquiv R (Fin 0)).toRingEquiv +/-- Ring equivalence between `CMvPolynomial (Fin 0) R` and `R`. -/ +noncomputable def isEmptyRingEquiv : CMvPolynomial (Fin 0) R ≃+* R := + (polyRingEquiv (σ := Fin 0)).trans (MvPolynomial.isEmptyAlgEquiv R (Fin 0)).toRingEquiv -instance instSMul : SMul R (CMvPolynomial n R) where +instance instSMul : SMul R (CMvPolynomial σ R) where smul r p := C r * p -instance instSMulZeroClass : SMulZeroClass R (CMvPolynomial n R) where +instance instSMulZeroClass : SMulZeroClass R (CMvPolynomial σ R) where smul_zero r := mul_zero (C r) @[simp] -lemma smul_def (r : R) (p : CMvPolynomial n R) : r • p = C r * p := rfl +lemma smul_def (r : R) (p : CMvPolynomial σ R) : r • p = C r * p := rfl section Algebra lemma fromCMvPolynomial_C (r : R) : - fromCMvPolynomial (C r : CMvPolynomial n R) = MvPolynomial.C r := by + fromCMvPolynomial (C r : CMvPolynomial σ R) = MvPolynomial.C r := by by_cases hr : r = 0 · subst hr - have : (C 0 : CMvPolynomial n R) = 0 := by show Lawful.C 0 = Lawful.C 0; rfl + have : (C 0 : CMvPolynomial σ R) = 0 := by show Lawful.C 0 = Lawful.C 0; rfl rw [this, CPoly.map_zero, MvPolynomial.C_0] · ext m rw [coeff_eq, MvPolynomial.coeff_C] unfold C Lawful.C coeff Unlawful.C MonoR.C simp only [hr, ite_false] - have ofFinsupp_zero : CMvMonomial.ofFinsupp (0 : Fin n →₀ ℕ) = CMvMonomial.zero := by - unfold CMvMonomial.ofFinsupp CMvMonomial.zero; ext i hi - show (Vector.ofFn (⇑(0 : Fin n →₀ ℕ)))[i] = (Vector.replicate n 0)[i] - simp only [Finsupp.coe_zero, Pi.zero_apply, Vector.getElem_ofFn, Vector.getElem_replicate] - by_cases hm : (0 : Fin n →₀ ℕ) = m + by_cases hm : (0 : σ →₀ ℕ) = m · subst hm; rw [if_pos rfl] erw [ExtTreeMap.getElem?_ofList_of_mem (k := CMvMonomial.zero) (k' := CMvMonomial.ofFinsupp 0) - (by rw [ofFinsupp_zero]; exact compare_self) + (by rw [CMvMonomial.ofFinsupp_zero]; exact compare_self) (v := r) (by simp) (by simp)] simp · rw [if_neg hm] have hne : CMvMonomial.ofFinsupp m ≠ CMvMonomial.zero := by - intro h; apply hm; ext i - have hi := congr_fun (congr_arg Vector.get h) i - simp [CMvMonomial.ofFinsupp, CMvMonomial.zero] at hi; exact hi.symm + rw [← CMvMonomial.ofFinsupp_zero] + exact fun h => hm ((CMvMonomial.injective_ofFinsupp h).symm) erw [ExtTreeMap.getElem?_ofList_of_contains_eq_false (by simp [hne])] rfl -noncomputable def CRingHom : R →+* CMvPolynomial n R where +noncomputable def CRingHom : R →+* CMvPolynomial σ R where toFun := C map_one' := by rw [eq_iff_fromCMvPolynomial] @@ -420,7 +405,7 @@ noncomputable def CRingHom : R →+* CMvPolynomial n R where rw [eq_iff_fromCMvPolynomial] simp [fromCMvPolynomial_C, CPoly.map_add] -noncomputable instance instAlgebra : Algebra R (CMvPolynomial n R) := +noncomputable instance instAlgebra : Algebra R (CMvPolynomial σ R) := Algebra.mk (toSMul := instSMul) CRingHom (fun r x => mul_comm (C r) x) (fun _ _ => rfl) diff --git a/CompPoly/Multivariate/Operations.lean b/CompPoly/Multivariate/Operations.lean index a33c0d62..2791c530 100644 --- a/CompPoly/Multivariate/Operations.lean +++ b/CompPoly/Multivariate/Operations.lean @@ -21,7 +21,7 @@ are in `CMvPolynomial.lean`. The `CommSemiring` and `CommRing` instances are in * `MonomialOrder`: Typeclass for comparing monomials. * `leadingMonomial`, `leadingCoeff`, `leadingTerm`: Leading term operations according to a monomial order. -* `rename`: Rename variables using a function `Fin n → Fin m`. +* `rename`: Rename variables using a function `σ → τ`. * `aeval`: Algebra evaluation. * `bind₁`: Substitution of polynomials for variables. -/ @@ -35,12 +35,12 @@ namespace CMvPolynomial /-! ## Leading-term operations -/ -/-- Monomial ordering typeclass for `n` variables. +/-- Monomial ordering typeclass for variables `σ`. Provides a way to compare monomials for determining leading terms. -/ -class MonomialOrder (n : ℕ) where - compare : CMvMonomial n → CMvMonomial n → Ordering +class MonomialOrder (σ : Type*) [FinEnum σ] where + compare : CMvMonomial σ → CMvMonomial σ → Ordering -- TODO: Add ordering axioms (transitivity, etc.) /-- Baseline degree of a monomial. @@ -48,15 +48,15 @@ class MonomialOrder (n : ℕ) where Currently this is the ordinary total degree and is independent of `MonomialOrder.compare`. -/ -def MonomialOrder.degree {n : ℕ} (m : CMvMonomial n) : ℕ := +def MonomialOrder.degree {σ : Type*} [FinEnum σ] (m : CMvMonomial σ) : ℕ := m.totalDegree /-- 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) := +def leadingMonomial {σ : Type*} [FinEnum σ] {R : Type*} [Zero R] [MonomialOrder σ] + (p : CMvPolynomial σ R) : Option (CMvMonomial σ) := ExtTreeMap.foldl (fun acc m _ => match acc with @@ -72,8 +72,8 @@ def leadingMonomial {n : ℕ} {R : Type*} [Zero R] [MonomialOrder n] Returns `0` for the zero polynomial, and otherwise returns the monomial with leading monomial and leading coefficient. -/ -def leadingTerm {n : ℕ} {R : Type*} [Zero R] [BEq R] [LawfulBEq R] [MonomialOrder n] - (p : CMvPolynomial n R) : CMvPolynomial n R := +def leadingTerm {σ : Type*} [FinEnum σ] {R : Type*} [Zero R] [BEq R] [LawfulBEq R] [MonomialOrder σ] + (p : CMvPolynomial σ R) : CMvPolynomial σ R := match leadingMonomial p with | none => 0 | some m => monomial m (coeff m p) @@ -82,38 +82,38 @@ def leadingTerm {n : ℕ} {R : Type*} [Zero R] [BEq R] [LawfulBEq R] [MonomialOr Returns `0` for the zero polynomial. -/ -def leadingCoeff {n : ℕ} {R : Type*} [Zero R] [MonomialOrder n] - (p : CMvPolynomial n R) : R := +def leadingCoeff {σ : Type*} [FinEnum σ] {R : Type*} [Zero R] [MonomialOrder σ] + (p : CMvPolynomial σ R) : R := match leadingMonomial p with | none => 0 | some m => coeff m p @[simp] lemma leadingCoeff_eq_zero_of_leadingMonomial_eq_none - {n : ℕ} {R : Type*} [Zero R] [MonomialOrder n] {p : CMvPolynomial n R} + {σ : Type*} [FinEnum σ] {R : Type*} [Zero R] [MonomialOrder σ] {p : CMvPolynomial σ R} (h : leadingMonomial p = none) : leadingCoeff p = 0 := by simp [leadingCoeff, h] lemma leadingCoeff_eq_coeff_of_leadingMonomial_eq_some - {n : ℕ} {R : Type*} [Zero R] [MonomialOrder n] {p : CMvPolynomial n R} - {m : CMvMonomial n} (h : leadingMonomial p = some m) : leadingCoeff p = coeff m p := by + {σ : Type*} [FinEnum σ] {R : Type*} [Zero R] [MonomialOrder σ] {p : CMvPolynomial σ R} + {m : CMvMonomial σ} (h : leadingMonomial p = some m) : leadingCoeff p = coeff m p := by simp [leadingCoeff, h] /-- Packaged form of `leadingCoeff`: it is the coefficient at the optional leading monomial, defaulting to `0` when no leading monomial exists. -/ lemma leadingCoeff_eq_coeff_leadingMonomial - {n : ℕ} {R : Type*} [Zero R] [MonomialOrder n] (p : CMvPolynomial n R) : + {σ : Type*} [FinEnum σ] {R : Type*} [Zero R] [MonomialOrder σ] (p : CMvPolynomial σ R) : leadingCoeff p = (leadingMonomial p).elim 0 (fun m => coeff m p) := by grind [leadingCoeff] @[simp] lemma leadingTerm_eq_zero_of_leadingMonomial_eq_none - {n : ℕ} {R : Type*} [Zero R] [BEq R] [LawfulBEq R] [MonomialOrder n] - {p : CMvPolynomial n R} (h : leadingMonomial p = none) : + {σ : Type*} [FinEnum σ] {R : Type*} [Zero R] [BEq R] [LawfulBEq R] [MonomialOrder σ] + {p : CMvPolynomial σ R} (h : leadingMonomial p = none) : leadingTerm p = 0 := by grind [leadingTerm] @[simp] lemma leadingTerm_eq_monomial_of_leadingMonomial_eq_some - {n : ℕ} {R : Type*} [Zero R] [BEq R] [LawfulBEq R] [MonomialOrder n] - {p : CMvPolynomial n R} {m : CMvMonomial n} (h : leadingMonomial p = some m) : + {σ : Type*} [FinEnum σ] {R : Type*} [Zero R] [BEq R] [LawfulBEq R] [MonomialOrder σ] + {p : CMvPolynomial σ R} {m : CMvMonomial σ} (h : leadingMonomial p = some m) : leadingTerm p = monomial m (coeff m p) := by grind [leadingTerm] @@ -121,153 +121,173 @@ lemma leadingCoeff_eq_coeff_leadingMonomial /-- Algebra evaluation: evaluates polynomial in an algebra. - Given an algebra `σ` over `R` and a function `f : Fin n → σ`, evaluates the polynomial. + Given an algebra `S` over `R` and a function `f : σ → S`, evaluates the polynomial. -/ -def aeval {n : ℕ} {R σ : Type*} [CommSemiring R] [CommSemiring σ] [Algebra R σ] - (f : Fin n → σ) (p : CMvPolynomial n R) : σ := - eval₂ (algebraMap R σ) f p +def aeval {σ : Type*} [FinEnum σ] {R S : Type*} [CommSemiring R] [CommSemiring S] [Algebra R S] + (f : σ → S) (p : CMvPolynomial σ R) : S := + eval₂ (algebraMap R S) f p -@[simp] lemma aeval_eq_eval₂ {n : ℕ} {R σ : Type*} - [CommSemiring R] [CommSemiring σ] [Algebra R σ] - (f : Fin n → σ) (p : CMvPolynomial n R) : - aeval f p = eval₂ (algebraMap R σ) f p := rfl +@[simp] lemma aeval_eq_eval₂ {σ : Type*} [FinEnum σ] {R S : Type*} + [CommSemiring R] [CommSemiring S] [Algebra R S] + (f : σ → S) (p : CMvPolynomial σ R) : + aeval f p = eval₂ (algebraMap R S) f p := rfl -@[simp] lemma aeval_C {n : ℕ} {R σ : Type*} +@[simp] lemma aeval_C {σ : Type*} [FinEnum σ] {R S : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] - [CommSemiring σ] [Algebra R σ] - (f : Fin n → σ) (c : R) : - aeval f (CMvPolynomial.C (n := n) c) = algebraMap R σ c := by + [CommSemiring S] [Algebra R S] + (f : σ → S) (c : R) : + aeval f (CMvPolynomial.C (σ := σ) c) = algebraMap R S c := by unfold aeval - rw [eval₂_equiv (p := CMvPolynomial.C (n := n) c) (f := algebraMap R σ) (vals := f)] + rw [eval₂_equiv (p := CMvPolynomial.C (σ := σ) c) (f := algebraMap R S) (vals := f)] simp [CMvPolynomial.fromCMvPolynomial_C] -@[simp] lemma aeval_add {n : ℕ} {R σ : Type*} +@[simp] lemma aeval_add {σ : Type*} [FinEnum σ] {R S : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] - [CommSemiring σ] [Algebra R σ] - (f : Fin n → σ) (p q : CMvPolynomial n R) : + [CommSemiring S] [Algebra R S] + (f : σ → S) (p q : CMvPolynomial σ R) : aeval f (p + q) = aeval f p + aeval f q := by unfold aeval simpa [CMvPolynomial.eval₂Hom_apply] using - (CMvPolynomial.eval₂Hom (S := σ) (algebraMap R σ) f).map_add p q + (CMvPolynomial.eval₂Hom (S := S) (algebraMap R S) f).map_add p q -@[simp] lemma aeval_mul {n : ℕ} {R σ : Type*} +@[simp] lemma aeval_mul {σ : Type*} [FinEnum σ] {R S : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] - [CommSemiring σ] [Algebra R σ] - (f : Fin n → σ) (p q : CMvPolynomial n R) : + [CommSemiring S] [Algebra R S] + (f : σ → S) (p q : CMvPolynomial σ R) : aeval f (p * q) = aeval f p * aeval f q := by unfold aeval simpa [CMvPolynomial.eval₂Hom_apply] using - (CMvPolynomial.eval₂Hom (S := σ) (algebraMap R σ) f).map_mul p q + (CMvPolynomial.eval₂Hom (S := S) (algebraMap R S) f).map_mul p q -@[simp] lemma aeval_zero {n : ℕ} {R σ : Type*} +@[simp] lemma aeval_zero {σ : Type*} [FinEnum σ] {R S : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] - [CommSemiring σ] [Algebra R σ] - (f : Fin n → σ) : - aeval f (0 : CMvPolynomial n R) = 0 := by + [CommSemiring S] [Algebra R S] + (f : σ → S) : + aeval f (0 : CMvPolynomial σ R) = 0 := by unfold aeval simpa [CMvPolynomial.eval₂Hom_apply] using - (CMvPolynomial.eval₂Hom (S := σ) (algebraMap R σ) f).map_zero + (CMvPolynomial.eval₂Hom (S := S) (algebraMap R S) f).map_zero -@[simp] lemma aeval_one {n : ℕ} {R σ : Type*} +@[simp] lemma aeval_one {σ : Type*} [FinEnum σ] {R S : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] - [CommSemiring σ] [Algebra R σ] - (f : Fin n → σ) : - aeval f (1 : CMvPolynomial n R) = 1 := by + [CommSemiring S] [Algebra R S] + (f : σ → S) : + aeval f (1 : CMvPolynomial σ R) = 1 := by unfold aeval simpa [CMvPolynomial.eval₂Hom_apply] using - (CMvPolynomial.eval₂Hom (S := σ) (algebraMap R σ) f).map_one + (CMvPolynomial.eval₂Hom (S := S) (algebraMap R S) f).map_one -@[simp] lemma aeval_pow {n : ℕ} {R σ : Type*} +@[simp] lemma aeval_pow {σ : Type*} [FinEnum σ] {R S : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] - [CommSemiring σ] [Algebra R σ] - (f : Fin n → σ) (p : CMvPolynomial n R) (k : ℕ) : + [CommSemiring S] [Algebra R S] + (f : σ → S) (p : CMvPolynomial σ R) (k : ℕ) : aeval f (p ^ k) = (aeval f p) ^ k := by unfold aeval simpa [CMvPolynomial.eval₂Hom_apply] using - (CMvPolynomial.eval₂Hom (S := σ) (algebraMap R σ) f).map_pow p k + (CMvPolynomial.eval₂Hom (S := S) (algebraMap R S) f).map_pow p k -@[simp] lemma aeval_neg {n : ℕ} {R σ : Type*} +@[simp] lemma aeval_neg {σ : Type*} [FinEnum σ] {R S : Type*} [CommRing R] [BEq R] [LawfulBEq R] - [CommRing σ] [Algebra R σ] - (f : Fin n → σ) (p : CMvPolynomial n R) : + [CommRing S] [Algebra R S] + (f : σ → S) (p : CMvPolynomial σ R) : aeval f (-p) = -(aeval f p) := by unfold aeval simpa [CMvPolynomial.eval₂Hom_apply] using - (CMvPolynomial.eval₂Hom (S := σ) (algebraMap R σ) f).map_neg p + (CMvPolynomial.eval₂Hom (S := S) (algebraMap R S) f).map_neg p -@[simp] lemma aeval_sub {n : ℕ} {R σ : Type*} +@[simp] lemma aeval_sub {σ : Type*} [FinEnum σ] {R S : Type*} [CommRing R] [BEq R] [LawfulBEq R] - [CommRing σ] [Algebra R σ] - (f : Fin n → σ) (p q : CMvPolynomial n R) : + [CommRing S] [Algebra R S] + (f : σ → S) (p q : CMvPolynomial σ R) : aeval f (p - q) = aeval f p - aeval f q := by unfold aeval simpa [CMvPolynomial.eval₂Hom_apply] using - (CMvPolynomial.eval₂Hom (S := σ) (algebraMap R σ) f).map_sub p q + (CMvPolynomial.eval₂Hom (S := S) (algebraMap R S) f).map_sub p q /-- Substitution: substitutes polynomials for variables. - Given `f : Fin n → CMvPolynomial m R`, substitutes `f i` for variable `X i`. + Given `f : σ → CMvPolynomial τ 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 := +def bind₁ {σ τ : Type*} [FinEnum σ] [FinEnum τ] {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] + (f : σ → CMvPolynomial τ R) (p : CMvPolynomial σ R) : CMvPolynomial τ R := ExtTreeMap.foldl - (fun acc mono c => CMvPolynomial.C (n := m) c * MonoR.evalMonomial f mono + acc) + (fun acc mono c => CMvPolynomial.C (σ := τ) c * MonoR.evalMonomial f mono + acc) 0 p.1 /-- The computable substitution `bind₁` agrees with algebraic evaluation. -/ -lemma bind₁_eq_aeval {n m : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] - (f : Fin n → CMvPolynomial m R) (p : CMvPolynomial n R) : - bind₁ f p = aeval (σ := CMvPolynomial m R) f p := by +lemma bind₁_eq_aeval {σ τ : Type*} [FinEnum σ] [FinEnum τ] {R : Type*} + [CommSemiring R] [BEq R] [LawfulBEq R] + (f : σ → CMvPolynomial τ R) (p : CMvPolynomial σ R) : + bind₁ f p = aeval (S := CMvPolynomial τ R) f p := by have hmap : ∀ c : R, - (algebraMap R (CMvPolynomial m R)) c = CMvPolynomial.C (n := m) c := by + (algebraMap R (CMvPolynomial τ R)) c = CMvPolynomial.C (σ := τ) c := by intro c rfl unfold bind₁ aeval CMvPolynomial.eval₂ simp [hmap] -@[simp] lemma bind₁_C {n m : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] - (f : Fin n → CMvPolynomial m R) (c : R) : - bind₁ f (CMvPolynomial.C (n := n) c) = CMvPolynomial.C (n := m) c := by +@[simp] lemma bind₁_C {σ τ : Type*} [FinEnum σ] [FinEnum τ] {R : Type*} + [CommSemiring R] [BEq R] [LawfulBEq R] + (f : σ → CMvPolynomial τ R) (c : R) : + bind₁ f (CMvPolynomial.C (σ := σ) c) = CMvPolynomial.C (σ := τ) c := by rw [bind₁_eq_aeval] - simpa using (aeval_C (n := n) (R := R) (σ := CMvPolynomial m R) f c) + simpa using (aeval_C (σ := σ) (R := R) (S := CMvPolynomial τ R) f c) -@[simp] lemma bind₁_add {n m : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] - (f : Fin n → CMvPolynomial m R) (p q : CMvPolynomial n R) : +@[simp] lemma bind₁_add {σ τ : Type*} [FinEnum σ] [FinEnum τ] {R : Type*} + [CommSemiring R] [BEq R] [LawfulBEq R] + (f : σ → CMvPolynomial τ R) (p q : CMvPolynomial σ R) : bind₁ f (p + q) = bind₁ f p + bind₁ f q := by repeat rw [bind₁_eq_aeval] - simpa using (aeval_add (n := n) (R := R) (σ := CMvPolynomial m R) f p q) + simpa using (aeval_add (σ := σ) (R := R) (S := CMvPolynomial τ R) f p q) -@[simp] lemma bind₁_mul {n m : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] - (f : Fin n → CMvPolynomial m R) (p q : CMvPolynomial n R) : +@[simp] lemma bind₁_mul {σ τ : Type*} [FinEnum σ] [FinEnum τ] {R : Type*} + [CommSemiring R] [BEq R] [LawfulBEq R] + (f : σ → CMvPolynomial τ R) (p q : CMvPolynomial σ R) : bind₁ f (p * q) = bind₁ f p * bind₁ f q := by repeat rw [bind₁_eq_aeval] - simpa using (aeval_mul (n := n) (R := R) (σ := CMvPolynomial m R) f p q) + simpa using (aeval_mul (σ := σ) (R := R) (S := CMvPolynomial τ R) f p q) /-! ## Core operations -/ /-- Rename variables using a function. - Given `f : Fin n → Fin m`, renames variable `X i` to `X (f i)`. + Given `f : σ → τ`, renames variable `X i` to `X (f i)`. -/ -def rename {n m : ℕ} {R : Type*} [Zero R] [Add 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)) +def rename {σ τ : Type*} [FinEnum σ] [FinEnum τ] {R : Type*} [Zero R] [Add R] [BEq R] [LawfulBEq R] + (f : σ → τ) (p : CMvPolynomial σ R) : CMvPolynomial τ R := + let renameMonomial (mono : CMvMonomial σ) : CMvMonomial τ := + Vector.ofFn (fun k => (Finset.univ.filter (fun i : σ => FinEnum.equiv (f i) = k)).sum + (fun i => mono.get (FinEnum.equiv i))) ExtTreeMap.foldl (fun acc mono c => acc + monomial (renameMonomial mono) c) 0 p.1 -- `renameEquiv` is defined in `CompPoly.Multivariate.Rename` +/-- Embed the variables of a polynomial into a larger variable type along an +injection `f : σ ↪ τ`. This is the disjoint-sum-friendly replacement for the old +numeric `extend`/`polyCoe` machinery. The caller supplies the embedding explicitly, +so there is no hidden assumption about how the variable sets are combined. + +We deliberately do *not* provide mixed-arity `HAdd`/`HMul`/`HSub` instances that +silently combine `CMvPolynomial σ R` and `CMvPolynomial τ R` into +`CMvPolynomial (σ ⊕ τ) R`: the order in which the two variable sets are joined is a +convention the caller should make explicit (e.g. via `rename`/`embedDomain`) rather +than have baked into instance resolution. -/ +def embedDomain {σ τ : Type*} [FinEnum σ] [FinEnum τ] {R : Type*} + [Zero R] [Add R] [BEq R] [LawfulBEq R] + (f : σ ↪ τ) (p : CMvPolynomial σ R) : CMvPolynomial τ R := + rename f p + /-- Iterative reconstruction of a polynomial by folding over terms. -/ -def sumToIter {n : ℕ} {R : Type*} [Zero R] [Add R] [BEq R] [LawfulBEq R] - (p : CMvPolynomial n R) : CMvPolynomial n R := +def sumToIter {σ : Type*} [FinEnum σ] {R : Type*} [Zero R] [Add R] [BEq R] [LawfulBEq R] + (p : CMvPolynomial σ R) : CMvPolynomial σ R := ExtTreeMap.foldl (fun acc m c => acc + monomial m c) 0 p.1 /-! ## Bridge and transport lemmas (technical) -/ -lemma X_eq_monomial {k : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] - (i : Fin k) : +lemma X_eq_monomial {σ : Type*} [FinEnum σ] {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] + (i : σ) : CMvPolynomial.X (R := R) i = CMvPolynomial.monomial - (Vector.ofFn (fun j => if j = i then 1 else 0)) + (Vector.ofFn (fun j => if j = FinEnum.equiv i then 1 else 0)) (1 : R) := by unfold CMvPolynomial.X CMvPolynomial.monomial by_cases h : (1 : R) = 0 @@ -276,18 +296,20 @@ lemma X_eq_monomial {k : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] · simp only [show ((1 : R) == 0) = false from by simp [h]] exact (if_neg (by decide)).symm -lemma toFinsupp_unitMono {k : ℕ} - (i : Fin k) : +lemma toFinsupp_unitMono {σ : Type*} [FinEnum σ] + (i : σ) : CMvMonomial.toFinsupp - (Vector.ofFn (fun j : Fin k => - if j = i then 1 else 0)) = + (Vector.ofFn (fun j : Fin (FinEnum.card σ) => + if j = FinEnum.equiv i then 1 else 0)) = Finsupp.single i 1 := by ext j - simp [CMvMonomial.toFinsupp, Vector.get, - Finsupp.single_apply, eq_comm] + simp only [CMvMonomial.toFinsupp, Finsupp.coe_mk, Finsupp.single_apply] + rw [Vector.get_ofFn] + simp only [EmbeddingLike.apply_eq_iff_eq, eq_comm] -lemma fromCMvPolynomial_monomial {k : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] - (mono : CMvMonomial k) (c : R) : +lemma fromCMvPolynomial_monomial {σ : Type*} [FinEnum σ] {R : Type*} + [CommSemiring R] [BEq R] [LawfulBEq R] + (mono : CMvMonomial σ) (c : R) : fromCMvPolynomial (CMvPolynomial.monomial mono c) = MvPolynomial.monomial (CMvMonomial.toFinsupp mono) c := by by_cases hc : c = 0 @@ -313,82 +335,84 @@ lemma fromCMvPolynomial_monomial {k : ℕ} {R : Type*} [CommSemiring R] [BEq R] (by simp [hne])] rfl -lemma fromCMvPolynomial_X {k : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] - (i : Fin k) : +lemma fromCMvPolynomial_X {σ : Type*} [FinEnum σ] {R : Type*} + [CommSemiring R] [BEq R] [LawfulBEq R] + (i : σ) : fromCMvPolynomial (CMvPolynomial.X (R := R) i) = MvPolynomial.X i := by rw [X_eq_monomial, fromCMvPolynomial_monomial, toFinsupp_unitMono] rfl -@[simp] lemma aeval_X {n : ℕ} {R σ : Type*} +@[simp] lemma aeval_X {σ : Type*} [FinEnum σ] {R S : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] - [CommSemiring σ] [Algebra R σ] - (f : Fin n → σ) (i : Fin n) : + [CommSemiring S] [Algebra R S] + (f : σ → S) (i : σ) : aeval f (CMvPolynomial.X (R := R) i) = f i := by unfold aeval - rw [eval₂_equiv (p := CMvPolynomial.X (R := R) i) (f := algebraMap R σ) (vals := f)] + rw [eval₂_equiv (p := CMvPolynomial.X (R := R) i) (f := algebraMap R S) (vals := f)] simp [fromCMvPolynomial_X] -@[simp] lemma bind₁_X {n m : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] - (f : Fin n → CMvPolynomial m R) (i : Fin n) : +@[simp] lemma bind₁_X {σ τ : Type*} [FinEnum σ] [FinEnum τ] {R : Type*} + [CommSemiring R] [BEq R] [LawfulBEq R] + (f : σ → CMvPolynomial τ R) (i : σ) : bind₁ f (CMvPolynomial.X (R := R) i) = f i := by rw [bind₁_eq_aeval] - simpa using (aeval_X (n := n) (R := R) (σ := CMvPolynomial m R) f i) + simpa using (aeval_X (σ := σ) (R := R) (S := CMvPolynomial τ R) f i) -@[simp] lemma bind₁_id {n : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] - (p : CMvPolynomial n R) : +@[simp] lemma bind₁_id {σ : Type*} [FinEnum σ] {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] + (p : CMvPolynomial σ R) : bind₁ (fun i => CMvPolynomial.X (R := R) i) p = p := by rw [bind₁_eq_aeval] unfold aeval - apply (CPoly.polyRingEquiv (n := n) (R := R)).injective - rw [eval₂_equiv (p := p) (f := algebraMap R (CMvPolynomial n R)) + apply (CPoly.polyRingEquiv (σ := σ) (R := R)).injective + rw [eval₂_equiv (p := p) (f := algebraMap R (CMvPolynomial σ R)) (vals := fun i => CMvPolynomial.X (R := R) i)] have hmap := MvPolynomial.map_eval₂Hom - (f := algebraMap R (CMvPolynomial n R)) + (f := algebraMap R (CMvPolynomial σ R)) (g := fun i => CMvPolynomial.X (R := R) i) - (φ := (CPoly.polyRingEquiv (n := n) (R := R)).toRingHom) + (φ := (CPoly.polyRingEquiv (σ := σ) (R := R)).toRingHom) (p := fromCMvPolynomial p) have hcomp : - ((CPoly.polyRingEquiv (n := n) (R := R)).toRingHom).comp - (algebraMap R (CMvPolynomial n R)) = MvPolynomial.C := by + ((CPoly.polyRingEquiv (σ := σ) (R := R)).toRingHom).comp + (algebraMap R (CMvPolynomial σ R)) = MvPolynomial.C := by ext r m rw [RingHom.comp_apply] - rw [show (algebraMap R (CMvPolynomial n R)) r = CMvPolynomial.C (n := n) r from rfl] + rw [show (algebraMap R (CMvPolynomial σ R)) r = CMvPolynomial.C (σ := σ) r from rfl] simpa using congrArg (fun q => MvPolynomial.coeff m q) - (CMvPolynomial.fromCMvPolynomial_C (n := n) (R := R) r) + (CMvPolynomial.fromCMvPolynomial_C (σ := σ) (R := R) r) have hcomp' : - ((CPoly.polyRingEquiv (n := n) (R := R) : CMvPolynomial n R →+* MvPolynomial (Fin n) R).comp - (algebraMap R (CMvPolynomial n R))) = MvPolynomial.C := by + ((CPoly.polyRingEquiv (σ := σ) (R := R) : CMvPolynomial σ R →+* MvPolynomial σ R).comp + (algebraMap R (CMvPolynomial σ R))) = MvPolynomial.C := by simpa using hcomp have hvars : - (fun i => CPoly.polyRingEquiv (n := n) (R := R) (CMvPolynomial.X (R := R) i)) = + (fun i => CPoly.polyRingEquiv (σ := σ) (R := R) (CMvPolynomial.X (R := R) i)) = (fun i => MvPolynomial.X i) := by funext i exact fromCMvPolynomial_X (R := R) i have hmap' : - CPoly.polyRingEquiv (n := n) (R := R) - (MvPolynomial.eval₂ (algebraMap R (CMvPolynomial n R)) + CPoly.polyRingEquiv (σ := σ) (R := R) + (MvPolynomial.eval₂ (algebraMap R (CMvPolynomial σ R)) (fun i => CMvPolynomial.X (R := R) i) (fromCMvPolynomial p)) = MvPolynomial.eval₂ - (((CPoly.polyRingEquiv (n := n) (R := R)).toRingHom).comp - (algebraMap R (CMvPolynomial n R))) + (((CPoly.polyRingEquiv (σ := σ) (R := R)).toRingHom).comp + (algebraMap R (CMvPolynomial σ R))) (fun i => MvPolynomial.X i) (fromCMvPolynomial p) := by simpa [MvPolynomial.eval₂Hom, hvars] using hmap have hmap'' : - CPoly.polyRingEquiv (n := n) (R := R) - (MvPolynomial.eval₂ (algebraMap R (CMvPolynomial n R)) + CPoly.polyRingEquiv (σ := σ) (R := R) + (MvPolynomial.eval₂ (algebraMap R (CMvPolynomial σ R)) (fun i => CMvPolynomial.X (R := R) i) (fromCMvPolynomial p)) = MvPolynomial.eval₂ MvPolynomial.C MvPolynomial.X (fromCMvPolynomial p) := by simpa [hcomp'] using hmap' calc - CPoly.polyRingEquiv (n := n) (R := R) - (MvPolynomial.eval₂ (algebraMap R (CMvPolynomial n R)) + CPoly.polyRingEquiv (σ := σ) (R := R) + (MvPolynomial.eval₂ (algebraMap R (CMvPolynomial σ R)) (fun i => CMvPolynomial.X (R := R) i) (fromCMvPolynomial p)) = MvPolynomial.eval₂ MvPolynomial.C MvPolynomial.X (fromCMvPolynomial p) := hmap'' _ = fromCMvPolynomial p := by simp [MvPolynomial.eval₂_eta (p := fromCMvPolynomial p)] - _ = CPoly.polyRingEquiv (n := n) (R := R) p := rfl + _ = CPoly.polyRingEquiv (σ := σ) (R := R) p := rfl lemma list_foldl_add_comm {β K V : Type*} [AddCommMonoid β] (g : K → V → β) (l : List (K × V)) (init : β) : @@ -401,17 +425,18 @@ lemma list_foldl_add_comm {β K V : Type*} [AddCommMonoid β] rw [show init + g h.1 h.2 = g h.1 h.2 + init from add_comm _ _] exact ih _ -lemma foldl_add_comm {β : Type*} [AddCommMonoid β] {k : ℕ} - {R' : Type*} (g : CMvMonomial k → R' → β) - (t : Std.ExtTreeMap (CMvMonomial k) R') : +lemma foldl_add_comm {β : Type*} [AddCommMonoid β] {σ : Type*} [FinEnum σ] + {R' : Type*} (g : CMvMonomial σ → R' → β) + (t : Std.ExtTreeMap (CMvMonomial σ) R') : Std.ExtTreeMap.foldl (fun acc m c => acc + g m c) (0 : β) t = Std.ExtTreeMap.foldl (fun acc m c => g m c + acc) (0 : β) t := by simp only [Std.ExtTreeMap.foldl_eq_foldl_toList] exact list_foldl_add_comm g t.toList 0 -lemma fromCMvPolynomial_finsupp_sum {n k : ℕ} [CommSemiring R] [BEq R] [LawfulBEq R] - (g : (Fin n →₀ ℕ) → R → CMvPolynomial k R) - (a : CMvPolynomial n R) : +lemma fromCMvPolynomial_finsupp_sum {σ τ : Type*} [FinEnum σ] [FinEnum τ] + [CommSemiring R] [BEq R] [LawfulBEq R] + (g : (σ →₀ ℕ) → R → CMvPolynomial τ R) + (a : CMvPolynomial σ R) : fromCMvPolynomial (Finsupp.sum (fromCMvPolynomial a) g) = Finsupp.sum (fromCMvPolynomial a) (fun μ c => fromCMvPolynomial (g μ c)) := by @@ -420,8 +445,8 @@ lemma fromCMvPolynomial_finsupp_sum {n k : ℕ} [CommSemiring R] [BEq R] [Lawful /-! ## API lemmas for `sumToIter` -/ -lemma sumToIter_eq {n : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] - (p : CMvPolynomial n R) : sumToIter p = p := by +lemma sumToIter_eq {σ : Type*} [FinEnum σ] {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] + (p : CMvPolynomial σ R) : sumToIter p = p := by rw [eq_iff_fromCMvPolynomial] unfold sumToIter rw [foldl_add_comm (g := fun m c => monomial m c) (t := p.1)] @@ -431,22 +456,24 @@ lemma sumToIter_eq {n : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] rw [Finsupp.sum] exact MvPolynomial.support_sum_monomial_coeff (fromCMvPolynomial p) -lemma coeff_sumToIter {n : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] - (m : CMvMonomial n) (p : CMvPolynomial n R) : +lemma coeff_sumToIter {σ : Type*} [FinEnum σ] {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] + (m : CMvMonomial σ) (p : CMvPolynomial σ R) : coeff m (sumToIter p) = coeff m p := by simp [sumToIter_eq (p := p)] -@[simp] lemma sumToIter_zero {n : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] : - sumToIter (0 : CMvPolynomial n R) = 0 := by - simpa using sumToIter_eq (p := (0 : CMvPolynomial n R)) +@[simp] lemma sumToIter_zero {σ : Type*} [FinEnum σ] {R : Type*} + [CommSemiring R] [BEq R] [LawfulBEq R] : + sumToIter (0 : CMvPolynomial σ R) = 0 := by + simpa using sumToIter_eq (p := (0 : CMvPolynomial σ R)) -lemma sumToIter_add {n : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] - (p q : CMvPolynomial n R) : +lemma sumToIter_add {σ : Type*} [FinEnum σ] {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] + (p q : CMvPolynomial σ R) : sumToIter (p + q) = sumToIter p + sumToIter q := by simp [sumToIter_eq] -@[simp] lemma sumToIter_idempotent {n : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] - (p : CMvPolynomial n R) : +@[simp] lemma sumToIter_idempotent {σ : Type*} [FinEnum σ] {R : Type*} + [CommSemiring R] [BEq R] [LawfulBEq R] + (p : CMvPolynomial σ R) : sumToIter (sumToIter p) = sumToIter p := by simp [sumToIter_eq] @@ -466,13 +493,13 @@ implementation. We prove pointwise equality here so that the `NatPow` instance can be safely routed through the fast version. The proofs need `mul_assoc` / `mul_one` / `mul_comm`, which are only available -once the `CommSemiring (CMvPolynomial n R)` instance has been built — that is +once the `CommSemiring (CMvPolynomial σ R)` instance has been built — that is why these lemmas live in `Operations.lean` rather than in `Lawful.lean`. -/ -variable {n : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] +variable {σ : Type*} [FinEnum σ] {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] /-- Additive law for the naive `npow`: $p^{a+b} = p^a \cdot p^b$. -/ -lemma npow_add (p : Lawful n R) (a b : ℕ) : +lemma npow_add (p : Lawful σ R) (a b : ℕ) : npow (a + b) p = npow a p * npow b p := by induction b with | zero => simp [npow, mul_one] @@ -482,9 +509,9 @@ lemma npow_add (p : Lawful n R) (a b : ℕ) : rw [ih, mul_assoc] /-- The fast repeated-squaring `npowBySq` agrees pointwise with the naive -`npow`. This is the equivalence that lets the `NatPow (Lawful n R)` instance +`npow`. This is the equivalence that lets the `NatPow (Lawful σ R)` instance be routed through `npowBySq` without changing observable behavior. -/ -theorem npowBySq_eq_npow (p : Lawful n R) : ∀ k : ℕ, npowBySq p k = npow k p +theorem npowBySq_eq_npow (p : Lawful σ R) : ∀ k : ℕ, npowBySq p k = npow k p | 0 => by unfold npowBySq; rfl | k + 1 => by unfold npowBySq diff --git a/CompPoly/Multivariate/Rename.lean b/CompPoly/Multivariate/Rename.lean index 2ceb3975..97c9e413 100644 --- a/CompPoly/Multivariate/Rename.lean +++ b/CompPoly/Multivariate/Rename.lean @@ -11,7 +11,7 @@ import Mathlib.Algebra.MvPolynomial.Rename This file proves properties of the `rename` function defined in `CMvPolynomial.lean`, by transferring results from Mathlib's `MvPolynomial.rename` through the -`polyRingEquiv : CMvPolynomial n R ≃+* MvPolynomial (Fin n) R` equivalence. +`polyRingEquiv : CMvPolynomial σ R ≃+* MvPolynomial σ R` equivalence. ## Main results @@ -27,7 +27,7 @@ namespace CPoly open Std CMvPolynomial -variable {n m : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] +variable {σ τ : Type*} [FinEnum σ] [FinEnum τ] {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] /-! ### Helper lemmas for `fromCMvPolynomial_rename` -/ @@ -45,28 +45,29 @@ lemma list_foldl_add_comm {β K V : Type*} [AddCommMonoid β] exact ih _ /-- Swapping addition order in `ExtTreeMap.foldl` does not change the result. -/ -lemma foldl_add_comm' {β : Type*} [AddCommMonoid β] {k : ℕ} - {R' : Type*} (g : CMvMonomial k → R' → β) - (t : Std.ExtTreeMap (CMvMonomial k) R') : +lemma foldl_add_comm' {β : Type*} [AddCommMonoid β] {υ : Type*} [FinEnum υ] + {R' : Type*} (g : CMvMonomial υ → R' → β) + (t : Std.ExtTreeMap (CMvMonomial υ) R') : Std.ExtTreeMap.foldl (fun acc m c => acc + g m c) (0 : β) t = Std.ExtTreeMap.foldl (fun acc m c => g m c + acc) (0 : β) t := by simp only [Std.ExtTreeMap.foldl_eq_foldl_toList] exact list_foldl_add_comm g t.toList 0 -/-- Applying `CMvMonomial.toFinsupp` at index `i` equals `Vector.get`. -/ -lemma toFinsupp_apply (mono : CMvMonomial n) (i : Fin n) : - (CMvMonomial.toFinsupp mono) i = mono.get i := rfl +/-- Applying `CMvMonomial.toFinsupp` at index `i` equals `Vector.get` through +the enumeration. -/ +lemma toFinsupp_apply (mono : CMvMonomial σ) (i : σ) : + (CMvMonomial.toFinsupp mono) i = mono.get (FinEnum.equiv i) := rfl /-- Monomial renaming via `Vector.ofFn` corresponds to `Finsupp.mapDomain` on the `Finsupp` side. -/ -lemma renameMonomial_eq (f : Fin n → Fin m) (mono : CMvMonomial n) : - (Vector.ofFn (fun j => (Finset.univ.filter (fun i => f i = j)).sum - (fun i => mono.get i)) : CMvMonomial m) = +lemma renameMonomial_eq (f : σ → τ) (mono : CMvMonomial σ) : + (Vector.ofFn (fun k => (Finset.univ.filter (fun i => FinEnum.equiv (f i) = k)).sum + (fun i => mono.get (FinEnum.equiv i))) : CMvMonomial τ) = CMvMonomial.ofFinsupp (Finsupp.mapDomain f (CMvMonomial.toFinsupp mono)) := by unfold CMvMonomial.ofFinsupp - congr 1; funext j - simp only [Finsupp.mapDomain, Finsupp.sum_apply, Finsupp.single_apply] + congr 1; funext k + simp only [Finsupp.mapDomain, Finsupp.sum_apply, Finsupp.single_apply, Equiv.eq_symm_apply] rw [Finset.sum_filter] rw [Finsupp.sum] -- Extend the sum from `support` to `Finset.univ` @@ -78,7 +79,7 @@ lemma renameMonomial_eq (f : Fin n → Fin m) (mono : CMvMonomial n) : /-- `fromCMvPolynomial` maps `CMvPolynomial.monomial` to `MvPolynomial.monomial`. -/ -lemma fromCMvPolynomial_monomial {k : ℕ} (mono : CMvMonomial k) (c : R) : +lemma fromCMvPolynomial_monomial {υ : Type*} [FinEnum υ] (mono : CMvMonomial υ) (c : R) : fromCMvPolynomial (CMvPolynomial.monomial mono c) = MvPolynomial.monomial (CMvMonomial.toFinsupp mono) c := by by_cases hc : c = 0 @@ -105,9 +106,9 @@ lemma fromCMvPolynomial_monomial {k : ℕ} (mono : CMvMonomial k) (c : R) : rfl /-- `fromCMvPolynomial` distributes over `Finsupp.sum`. -/ -lemma fromCMvPolynomial_finsupp_sum {k : ℕ} - (g : (Fin n →₀ ℕ) → R → CMvPolynomial k R) - (a : CMvPolynomial n R) : +lemma fromCMvPolynomial_finsupp_sum {υ : Type*} [FinEnum υ] + (g : (σ →₀ ℕ) → R → CMvPolynomial υ R) + (a : CMvPolynomial σ R) : fromCMvPolynomial (Finsupp.sum (fromCMvPolynomial a) g) = Finsupp.sum (fromCMvPolynomial a) (fun μ c => fromCMvPolynomial (g μ c)) := by @@ -118,8 +119,8 @@ lemma fromCMvPolynomial_finsupp_sum {k : ℕ} /-- `CMvPolynomial.rename` agrees with `MvPolynomial.rename` under the `fromCMvPolynomial` equivalence. -/ -lemma fromCMvPolynomial_rename (f : Fin n → Fin m) - (p : CMvPolynomial n R) : +lemma fromCMvPolynomial_rename (f : σ → τ) + (p : CMvPolynomial σ R) : fromCMvPolynomial (CMvPolynomial.rename f p) = MvPolynomial.rename f (fromCMvPolynomial p) := by -- Express rename as a `Finsupp.sum` via `foldl_eq_sum` @@ -129,9 +130,9 @@ lemma fromCMvPolynomial_rename (f : Fin n → Fin m) (CMvMonomial.ofFinsupp (Finsupp.mapDomain f μ)) c) := by show Std.ExtTreeMap.foldl (fun acc mono c => acc + CMvPolynomial.monomial - (Vector.ofFn fun j => - (Finset.univ.filter fun i => f i = j).sum - fun i => mono.get i) c) + (Vector.ofFn fun k => + (Finset.univ.filter fun i => FinEnum.equiv (f i) = k).sum + fun i => mono.get (FinEnum.equiv i)) c) 0 p.1 = _ simp_rw [renameMonomial_eq f] rw [foldl_add_comm' (fun mono c => @@ -155,8 +156,8 @@ lemma fromCMvPolynomial_rename (f : Fin n → Fin m) /-! ### Bridging lemmas for `C` and `X` -/ /-- `CMvPolynomial.C c` equals `CMvPolynomial.monomial 0 c`. -/ -lemma C_eq_monomial {k : ℕ} (c : R) : - CMvPolynomial.C (n := k) c = CMvPolynomial.monomial 0 c := by +lemma C_eq_monomial {υ : Type*} [FinEnum υ] (c : R) : + CMvPolynomial.C (σ := υ) c = CMvPolynomial.monomial 0 c := by by_cases hc : c = 0 · subst hc; ext m unfold CMvPolynomial.coeff CMvPolynomial.C CMvPolynomial.monomial @@ -164,7 +165,7 @@ lemma C_eq_monomial {k : ℕ} (c : R) : grind · ext m show (CMvPolynomial.C c).coeff m = - (CMvPolynomial.monomial (0 : CMvMonomial k) c).coeff m + (CMvPolynomial.monomial (0 : CMvMonomial υ) c).coeff m unfold CMvPolynomial.coeff CMvPolynomial.C Lawful.C CMvPolynomial.monomial Unlawful.C simp only [show (c == (0 : R)) = false from by simp [hc], @@ -176,15 +177,16 @@ lemma C_eq_monomial {k : ℕ} (c : R) : erw [Unlawful.filter_get] /-- The `Finsupp` of the zero monomial is zero. -/ -lemma toFinsupp_zero {k : ℕ} : - CMvMonomial.toFinsupp (0 : CMvMonomial k) = 0 := by +lemma toFinsupp_zero {υ : Type*} [FinEnum υ] : + CMvMonomial.toFinsupp (0 : CMvMonomial υ) = 0 := by ext i - simp [CMvMonomial.toFinsupp, Vector.get] - exact Vector.getElem_zero i.val i.isLt + simp only [CMvMonomial.toFinsupp, Finsupp.coe_mk, Finsupp.coe_zero, Pi.zero_apply] + simp only [show (0 : CMvMonomial υ) = Vector.replicate (FinEnum.card υ) 0 from rfl, + Vector.get_replicate] /-- `fromCMvPolynomial` maps `CMvPolynomial.C` to `MvPolynomial.C`. -/ -lemma fromCMvPolynomial_C {k : ℕ} (c : R) : - fromCMvPolynomial (CMvPolynomial.C (n := k) c) = +lemma fromCMvPolynomial_C {υ : Type*} [FinEnum υ] (c : R) : + fromCMvPolynomial (CMvPolynomial.C (σ := υ) c) = MvPolynomial.C c := by rw [C_eq_monomial, fromCMvPolynomial_monomial, toFinsupp_zero, ← MvPolynomial.C_apply] @@ -193,9 +195,9 @@ lemma fromCMvPolynomial_C {k : ℕ} (c : R) : /-- Constants are unchanged under renaming. -/ @[simp] -lemma rename_C (f : Fin n → Fin m) (c : R) : +lemma rename_C (f : σ → τ) (c : R) : CMvPolynomial.rename f (CMvPolynomial.C c) = - CMvPolynomial.C (n := m) c := by + CMvPolynomial.C (σ := τ) c := by apply fromCMvPolynomial_injective rw [fromCMvPolynomial_rename, fromCMvPolynomial_C, fromCMvPolynomial_C] @@ -203,9 +205,9 @@ lemma rename_C (f : Fin n → Fin m) (c : R) : /-- `CMvPolynomial.X i` equals `CMvPolynomial.monomial eᵢ 1` where `eᵢ` is the `i`-th standard basis vector. -/ -lemma X_eq_monomial {k : ℕ} (i : Fin k) : +lemma X_eq_monomial {υ : Type*} [FinEnum υ] (i : υ) : CMvPolynomial.X (R := R) i = CMvPolynomial.monomial - (Vector.ofFn (fun j => if j = i then 1 else 0)) + (Vector.ofFn (fun j => if j = FinEnum.equiv i then 1 else 0)) (1 : R) := by unfold CMvPolynomial.X CMvPolynomial.monomial by_cases h : (1 : R) = 0 @@ -216,18 +218,19 @@ lemma X_eq_monomial {k : ℕ} (i : Fin k) : /-- The `Finsupp` of the `i`-th standard basis monomial is `Finsupp.single i 1`. -/ -lemma toFinsupp_unitMono {k : ℕ} (i : Fin k) : +lemma toFinsupp_unitMono {υ : Type*} [FinEnum υ] (i : υ) : CMvMonomial.toFinsupp - (Vector.ofFn (fun j : Fin k => - if j = i then 1 else 0)) = + (Vector.ofFn (fun j : Fin (FinEnum.card υ) => + if j = FinEnum.equiv i then 1 else 0)) = Finsupp.single i 1 := by ext j - simp [CMvMonomial.toFinsupp, Vector.get, - Finsupp.single_apply, eq_comm] + simp only [CMvMonomial.toFinsupp, Finsupp.coe_mk, Finsupp.single_apply] + rw [Vector.get_ofFn] + simp only [EmbeddingLike.apply_eq_iff_eq, eq_comm] /-- `fromCMvPolynomial` maps `CMvPolynomial.X i` to `MvPolynomial.X i`. -/ -lemma fromCMvPolynomial_X {k : ℕ} (i : Fin k) : +lemma fromCMvPolynomial_X {υ : Type*} [FinEnum υ] (i : υ) : fromCMvPolynomial (CMvPolynomial.X (R := R) i) = MvPolynomial.X i := by rw [X_eq_monomial, fromCMvPolynomial_monomial, @@ -236,7 +239,7 @@ lemma fromCMvPolynomial_X {k : ℕ} (i : Fin k) : /-- Renaming maps variable `X i` to `X (f i)`. -/ @[simp] -lemma rename_X (f : Fin n → Fin m) (i : Fin n) : +lemma rename_X (f : σ → τ) (i : σ) : CMvPolynomial.rename f (CMvPolynomial.X (R := R) i) = CMvPolynomial.X (f i) := by apply fromCMvPolynomial_injective @@ -246,8 +249,8 @@ lemma rename_X (f : Fin n → Fin m) (i : Fin n) : /-- Renaming preserves addition. -/ @[simp] -lemma rename_add (f : Fin n → Fin m) - (p q : CMvPolynomial n R) : +lemma rename_add (f : σ → τ) + (p q : CMvPolynomial σ R) : CMvPolynomial.rename f (p + q) = CMvPolynomial.rename f p + CMvPolynomial.rename f q := by @@ -258,8 +261,8 @@ lemma rename_add (f : Fin n → Fin m) /-- Renaming preserves multiplication. -/ @[simp] -lemma rename_mul (f : Fin n → Fin m) - (p q : CMvPolynomial n R) : +lemma rename_mul (f : σ → τ) + (p q : CMvPolynomial σ R) : CMvPolynomial.rename f (p * q) = CMvPolynomial.rename f p * CMvPolynomial.rename f q := by @@ -270,7 +273,7 @@ lemma rename_mul (f : Fin n → Fin m) /-- Renaming by the identity function is the identity. -/ @[simp] -lemma rename_id (p : CMvPolynomial n R) : +lemma rename_id (p : CMvPolynomial σ R) : CMvPolynomial.rename id p = p := by apply fromCMvPolynomial_injective rw [fromCMvPolynomial_rename] @@ -278,8 +281,8 @@ lemma rename_id (p : CMvPolynomial n R) : /-- Composing two renamings equals renaming by the composition. -/ @[simp] -lemma rename_rename {k : ℕ} (f : Fin n → Fin m) - (g : Fin m → Fin k) (p : CMvPolynomial n R) : +lemma rename_rename {υ : Type*} [FinEnum υ] (f : σ → τ) + (g : τ → υ) (p : CMvPolynomial σ R) : CMvPolynomial.rename g (CMvPolynomial.rename f p) = CMvPolynomial.rename (g ∘ f) p := by apply fromCMvPolynomial_injective @@ -293,13 +296,13 @@ namespace CMvPolynomial open CPoly -variable {n m : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] +variable {σ τ : Type*} [FinEnum σ] [FinEnum τ] {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] /-- Ring equivalence for variable renaming when the function is a bijection. -/ noncomputable def renameEquiv - (f : Fin n ≃ Fin m) : - CMvPolynomial n R ≃+* CMvPolynomial m R where + (f : σ ≃ τ) : + CMvPolynomial σ R ≃+* CMvPolynomial τ R where toFun := CMvPolynomial.rename f invFun := CMvPolynomial.rename f.symm left_inv p := by diff --git a/CompPoly/Multivariate/Restrict.lean b/CompPoly/Multivariate/Restrict.lean index 18c6a13a..7c6b2a05 100644 --- a/CompPoly/Multivariate/Restrict.lean +++ b/CompPoly/Multivariate/Restrict.lean @@ -20,11 +20,11 @@ namespace CPoly open CMvPolynomial -variable {n : ℕ} {R : Type*} [Zero R] [BEq R] [LawfulBEq R] +variable {σ : Type*} [FinEnum σ] {R : Type*} [Zero R] [BEq R] [LawfulBEq R] /-- Coefficient of `restrictBy keep p` at `m`: `p.coeff m` if `keep m`, else `0`. -/ -lemma coeff_restrictBy (keep : CMvMonomial n → Prop) [DecidablePred keep] - (m : CMvMonomial n) (p : CMvPolynomial n R) : +lemma coeff_restrictBy (keep : CMvMonomial σ → Prop) [DecidablePred keep] + (m : CMvMonomial σ) (p : CMvPolynomial σ R) : (CMvPolynomial.restrictBy keep p).coeff m = if keep m then p.coeff m else 0 := by unfold CMvPolynomial.coeff CMvPolynomial.restrictBy unfold Lawful.fromUnlawful @@ -32,7 +32,7 @@ lemma coeff_restrictBy (keep : CMvMonomial n → Prop) [DecidablePred keep] ((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 - let t : Unlawful n R := Std.ExtTreeMap.filter (fun m' _ => decide (keep m')) p.1 + let t : Unlawful σ R := Std.ExtTreeMap.filter (fun m' _ => decide (keep m')) p.1 have h0 : (Std.ExtTreeMap.filter (fun _ c => c != (0 : R)) t)[m]?.getD 0 = t[m]?.getD 0 := by exact (Unlawful.filter_get (v := (0 : R)) (m := m) (a := t)) @@ -51,7 +51,7 @@ lemma coeff_restrictBy (keep : CMvMonomial n → Prop) [DecidablePred keep] /-- Coeff at `m`: `p.coeff m` if `m.totalDegree ≤ d`, else `0`. -/ @[simp] -lemma coeff_restrictTotalDegree (d : ℕ) (m : CMvMonomial n) (p : CMvPolynomial n R) : +lemma coeff_restrictTotalDegree (d : ℕ) (m : CMvMonomial σ) (p : CMvPolynomial σ R) : (CMvPolynomial.restrictTotalDegree d p).coeff m = if m.totalDegree ≤ d then p.coeff m else 0 := by simpa [CMvPolynomial.restrictTotalDegree] using @@ -59,39 +59,39 @@ lemma coeff_restrictTotalDegree (d : ℕ) (m : CMvMonomial n) (p : CMvPolynomial /-- Coefficient of `restrictDegree d p` at `m`: `p.coeff m` if `∀ i, m.degreeOf i ≤ d`, else `0`. -/ @[simp] -lemma coeff_restrictDegree (d : ℕ) (m : CMvMonomial n) (p : CMvPolynomial n R) : +lemma coeff_restrictDegree (d : ℕ) (m : CMvMonomial σ) (p : CMvPolynomial σ R) : (CMvPolynomial.restrictDegree d p).coeff m = - if ∀ i : Fin n, m.degreeOf i ≤ d then p.coeff m else 0 := by + if ∀ i : σ, m.degreeOf i ≤ d then p.coeff m else 0 := by simpa [CMvPolynomial.restrictDegree] using - (coeff_restrictBy (keep := fun m => ∀ i : Fin n, m.degreeOf i ≤ d) m p) + (coeff_restrictBy (keep := fun m => ∀ i : σ, m.degreeOf i ≤ d) m p) /-- When `m.totalDegree ≤ d`, coeff at `m` is unchanged by `restrictTotalDegree d`. -/ -lemma coeff_restrictTotalDegree_eq_self_of_le {d : ℕ} {m : CMvMonomial n} - {p : CMvPolynomial n R} (h : m.totalDegree ≤ d) : +lemma coeff_restrictTotalDegree_eq_self_of_le {d : ℕ} {m : CMvMonomial σ} + {p : CMvPolynomial σ R} (h : m.totalDegree ≤ d) : (CMvPolynomial.restrictTotalDegree d p).coeff m = p.coeff m := by simp [coeff_restrictTotalDegree, h] /-- When `d < m.totalDegree`, coeff at `m` is `0` in `restrictTotalDegree d p`. -/ -lemma coeff_restrictTotalDegree_eq_zero_of_lt {d : ℕ} {m : CMvMonomial n} - {p : CMvPolynomial n R} (h : d < m.totalDegree) : +lemma coeff_restrictTotalDegree_eq_zero_of_lt {d : ℕ} {m : CMvMonomial σ} + {p : CMvPolynomial σ R} (h : d < m.totalDegree) : (CMvPolynomial.restrictTotalDegree d p).coeff m = 0 := by simp [coeff_restrictTotalDegree, Nat.not_le_of_lt h] /-- When `∀ i, m.degreeOf i ≤ d`, coeff at `m` is unchanged by `restrictDegree d`. -/ -lemma coeff_restrictDegree_eq_self_of_le {d : ℕ} {m : CMvMonomial n} - {p : CMvPolynomial n R} (h : ∀ i : Fin n, m.degreeOf i ≤ d) : +lemma coeff_restrictDegree_eq_self_of_le {d : ℕ} {m : CMvMonomial σ} + {p : CMvPolynomial σ R} (h : ∀ i : σ, m.degreeOf i ≤ d) : (CMvPolynomial.restrictDegree d p).coeff m = p.coeff m := by simp [coeff_restrictDegree, h] /-- When `¬(∀ i, m.degreeOf i ≤ d)`, coeff at `m` is `0` in `restrictDegree d p`. -/ -lemma coeff_restrictDegree_eq_zero_of_not_le {d : ℕ} {m : CMvMonomial n} - {p : CMvPolynomial n R} (h : ¬ (∀ i : Fin n, m.degreeOf i ≤ d)) : +lemma coeff_restrictDegree_eq_zero_of_not_le {d : ℕ} {m : CMvMonomial σ} + {p : CMvPolynomial σ R} (h : ¬ (∀ i : σ, m.degreeOf i ≤ d)) : (CMvPolynomial.restrictDegree d p).coeff m = 0 := by simp [coeff_restrictDegree, h] /-- Monomials in `restrictTotalDegree d p` have `totalDegree ≤ d`. -/ -lemma totalDegree_le_of_mem_monomials_restrictTotalDegree {d : ℕ} {m : CMvMonomial n} - {p : CMvPolynomial n R} +lemma totalDegree_le_of_mem_monomials_restrictTotalDegree {d : ℕ} {m : CMvMonomial σ} + {p : CMvPolynomial σ R} (hm : m ∈ Lawful.monomials (CMvPolynomial.restrictTotalDegree d p)) : m.totalDegree ≤ d := by have hm' : m ∈ CMvPolynomial.restrictTotalDegree d p := (Lawful.mem_monomials_iff).1 hm @@ -106,16 +106,16 @@ lemma totalDegree_le_of_mem_monomials_restrictTotalDegree {d : ℕ} {m : CMvMono exact False.elim (hcoeff_ne_zero hcoeff_zero) /-- Monomials in `restrictDegree d p` have `degreeOf i ≤ d` for each variable `i`. -/ -lemma degreeOf_le_of_mem_monomials_restrictDegree {d : ℕ} {m : CMvMonomial n} - {p : CMvPolynomial n R} +lemma degreeOf_le_of_mem_monomials_restrictDegree {d : ℕ} {m : CMvMonomial σ} + {p : CMvPolynomial σ R} (hm : m ∈ Lawful.monomials (CMvPolynomial.restrictDegree d p)) : - ∀ i : Fin n, m.degreeOf i ≤ d := by + ∀ i : σ, m.degreeOf i ≤ d := by have hm' : m ∈ CMvPolynomial.restrictDegree d p := (Lawful.mem_monomials_iff).1 hm have hcoeff_ne_zero : (CMvPolynomial.restrictDegree d p).coeff m ≠ 0 := by simpa [CMvPolynomial.coeff] using (Lawful.getD_getElem?_ne_zero_of_mem (p := CMvPolynomial.restrictDegree d p) (m := m) hm') - by_cases hdeg : ∀ i : Fin n, m.degreeOf i ≤ d + by_cases hdeg : ∀ i : σ, m.degreeOf i ≤ d · exact hdeg · have hcoeff_zero : (CMvPolynomial.restrictDegree d p).coeff m = 0 := by simp [coeff_restrictDegree, hdeg] @@ -158,13 +158,14 @@ private lemma vector_ofFn_sum_eq_finSum {n : ℕ} (s : Fin n → ℕ) : _ = ∑ i : Fin n, s i := list_ofFn_sum_eq_finSum s /-- Monomial `totalDegree` equals `Finsupp.sum` of its exponents. -/ -private lemma totalDegree_eq_finsupp_sum {n : ℕ} (m : CMvMonomial n) : +private lemma totalDegree_eq_finsupp_sum (m : CMvMonomial σ) : m.totalDegree = Finsupp.sum m.toFinsupp (fun _ e => e) := by have hof : (CMvMonomial.ofFinsupp m.toFinsupp).totalDegree = Finsupp.sum m.toFinsupp (fun _ e => e) := by unfold CMvMonomial.totalDegree CMvMonomial.ofFinsupp rw [Finsupp.sum_fintype] - · simpa using (vector_ofFn_sum_eq_finSum (s := (m.toFinsupp : Fin n →₀ ℕ))) + · rw [vector_ofFn_sum_eq_finSum (s := fun k => m.toFinsupp (FinEnum.equiv.symm k))] + exact Equiv.sum_comp FinEnum.equiv.symm (fun i => m.toFinsupp i) · intro i simp simpa [CMvMonomial.ofFinsupp_toFinsupp] using hof @@ -172,7 +173,7 @@ private lemma totalDegree_eq_finsupp_sum {n : ℕ} (m : CMvMonomial n) : /-- `restrictTotalDegree d p` has `totalDegree ≤ d`. -/ lemma totalDegree_restrictTotalDegree_le {R' : Type*} [CommSemiring R'] [BEq R'] [LawfulBEq R'] - (d : ℕ) (p : CMvPolynomial n R') : + (d : ℕ) (p : CMvPolynomial σ R') : (CMvPolynomial.restrictTotalDegree d p).totalDegree ≤ d := by classical unfold CMvPolynomial.totalDegree @@ -189,22 +190,22 @@ lemma totalDegree_restrictTotalDegree_le /-- `restrictTotalDegree d 0 = 0`. -/ @[simp] lemma restrictTotalDegree_zero (d : ℕ) : - CMvPolynomial.restrictTotalDegree d (0 : CMvPolynomial n R) = 0 := by + CMvPolynomial.restrictTotalDegree d (0 : CMvPolynomial σ R) = 0 := by ext m simpa [CMvPolynomial.coeff] using - (coeff_restrictTotalDegree (d := d) (m := m) (p := (0 : CMvPolynomial n R))) + (coeff_restrictTotalDegree (d := d) (m := m) (p := (0 : CMvPolynomial σ R))) /-- `restrictDegree d 0 = 0`. -/ @[simp] lemma restrictDegree_zero (d : ℕ) : - CMvPolynomial.restrictDegree d (0 : CMvPolynomial n R) = 0 := by + CMvPolynomial.restrictDegree d (0 : CMvPolynomial σ R) = 0 := by ext m simpa [CMvPolynomial.coeff] using - (coeff_restrictDegree (d := d) (m := m) (p := (0 : CMvPolynomial n R))) + (coeff_restrictDegree (d := d) (m := m) (p := (0 : CMvPolynomial σ R))) /-- Double `restrictTotalDegree` equals `restrictTotalDegree (min d d')`. -/ @[simp] -lemma restrictTotalDegree_restrictTotalDegree (d d' : ℕ) (p : CMvPolynomial n R) : +lemma restrictTotalDegree_restrictTotalDegree (d d' : ℕ) (p : CMvPolynomial σ R) : CMvPolynomial.restrictTotalDegree d (CMvPolynomial.restrictTotalDegree d' p) = CMvPolynomial.restrictTotalDegree (min d d') p := by ext m @@ -213,35 +214,35 @@ lemma restrictTotalDegree_restrictTotalDegree (d d' : ℕ) (p : CMvPolynomial n /-- Double `restrictDegree` equals `restrictDegree (min d d')`. -/ @[simp] -lemma restrictDegree_restrictDegree (d d' : ℕ) (p : CMvPolynomial n R) : +lemma restrictDegree_restrictDegree (d d' : ℕ) (p : CMvPolynomial σ R) : CMvPolynomial.restrictDegree d (CMvPolynomial.restrictDegree d' p) = CMvPolynomial.restrictDegree (min d d') p := by ext m - by_cases h₁ : ∀ i : Fin n, m.degreeOf i ≤ d - · by_cases h₂ : ∀ i : Fin n, m.degreeOf i ≤ d' - · have hmin : ∀ i : Fin n, m.degreeOf i ≤ min d d' := by + by_cases h₁ : ∀ i : σ, m.degreeOf i ≤ d + · by_cases h₂ : ∀ i : σ, m.degreeOf i ≤ d' + · have hmin : ∀ i : σ, m.degreeOf i ≤ min d d' := by intro i exact (le_min_iff.mpr ⟨h₁ i, h₂ i⟩) simp [coeff_restrictDegree, h₁, h₂, hmin] - · have hmin : ¬ (∀ i : Fin n, m.degreeOf i ≤ min d d') := by + · have hmin : ¬ (∀ i : σ, m.degreeOf i ≤ min d d') := by intro h exact h₂ (fun i => (le_min_iff.mp (h i)).2) simp [coeff_restrictDegree, h₁, h₂] - · have hmin : ¬ (∀ i : Fin n, m.degreeOf i ≤ min d d') := by + · have hmin : ¬ (∀ i : σ, m.degreeOf i ≤ min d d') := by intro h exact h₁ (fun i => (le_min_iff.mp (h i)).1) - have hpair : ¬ (∀ i : Fin n, m.degreeOf i ≤ d ∧ m.degreeOf i ≤ d') := by + have hpair : ¬ (∀ i : σ, m.degreeOf i ≤ d ∧ m.degreeOf i ≤ d') := by intro h exact h₁ (fun i => (h i).1) simp [coeff_restrictDegree, h₁, hpair] /-- `restrictTotalDegree d` and `restrictDegree d'` commute. -/ @[simp] -lemma restrictTotalDegree_restrictDegree_comm (d d' : ℕ) (p : CMvPolynomial n R) : +lemma restrictTotalDegree_restrictDegree_comm (d d' : ℕ) (p : CMvPolynomial σ R) : CMvPolynomial.restrictTotalDegree d (CMvPolynomial.restrictDegree d' p) = CMvPolynomial.restrictDegree d' (CMvPolynomial.restrictTotalDegree d p) := by ext m - by_cases h₁ : m.totalDegree ≤ d <;> by_cases h₂ : ∀ i : Fin n, m.degreeOf i ≤ d' <;> + by_cases h₁ : m.totalDegree ≤ d <;> by_cases h₂ : ∀ i : σ, m.degreeOf i ≤ d' <;> simp [coeff_restrictTotalDegree, coeff_restrictDegree, h₁, h₂] end CPoly diff --git a/CompPoly/Multivariate/Unlawful.lean b/CompPoly/Multivariate/Unlawful.lean index 2c439215..252c509b 100644 --- a/CompPoly/Multivariate/Unlawful.lean +++ b/CompPoly/Multivariate/Unlawful.lean @@ -17,7 +17,7 @@ the absence of zero coefficients. ## Main definitions -* `CPoly.Unlawful n R`: A map from `CMvMonomial n` to `R`, implemented using `Std.ExtTreeMap`. +* `CPoly.Unlawful σ R`: A map from `CMvMonomial σ` to `R`, implemented using `Std.ExtTreeMap`. -/ set_option allowUnsafeReducibility true in attribute [local reducible] instDecidableEqOfLawfulBEq @@ -28,42 +28,42 @@ namespace CPoly open Std /-- - Polynomial in `n` variables with coefficients in `R`. + Polynomial in variables `σ` with coefficients in `R`. Internally represented as a tree map from monomials to coefficients. -/ -abbrev Unlawful (n : ℕ) (R : Type*) : Type _ := - Std.ExtTreeMap (CMvMonomial n) R (Ord.compare (α := CMvMonomial n)) +abbrev Unlawful (σ : Type*) [FinEnum σ] (R : Type*) : Type _ := + Std.ExtTreeMap (CMvMonomial σ) R (Ord.compare (α := CMvMonomial σ)) section Instances -variable {n : ℕ} {R : Type*} +variable {σ : Type*} [FinEnum σ] {R : Type*} -instance : EmptyCollection (Unlawful n R) := ⟨(∅ : Std.ExtTreeMap (CMvMonomial n) R compare)⟩ +instance : EmptyCollection (Unlawful σ R) := ⟨(∅ : Std.ExtTreeMap (CMvMonomial σ) R compare)⟩ -instance : Singleton (MonoR n R) (Unlawful n R) := - inferInstanceAs (Singleton (MonoR n R) (Std.ExtTreeMap (CMvMonomial n) R compare)) +instance : Singleton (MonoR σ R) (Unlawful σ R) := + inferInstanceAs (Singleton (MonoR σ R) (Std.ExtTreeMap (CMvMonomial σ) R compare)) -instance : Insert (MonoR n R) (Unlawful n R) := - inferInstanceAs (Insert (MonoR n R) (Std.ExtTreeMap (CMvMonomial n) R compare)) +instance : Insert (MonoR σ R) (Unlawful σ R) := + inferInstanceAs (Insert (MonoR σ R) (Std.ExtTreeMap (CMvMonomial σ) R compare)) -instance : LawfulSingleton (MonoR n R) (Unlawful n R) := - inferInstanceAs (LawfulSingleton (MonoR n R) (Std.ExtTreeMap (CMvMonomial n) R compare)) +instance : LawfulSingleton (MonoR σ R) (Unlawful σ R) := + inferInstanceAs (LawfulSingleton (MonoR σ R) (Std.ExtTreeMap (CMvMonomial σ) R compare)) -instance : Membership (CMvMonomial n) (Unlawful n R) := - inferInstanceAs (Membership (CMvMonomial n) (Std.ExtTreeMap (CMvMonomial n) R compare)) +instance : Membership (CMvMonomial σ) (Unlawful σ R) := + inferInstanceAs (Membership (CMvMonomial σ) (Std.ExtTreeMap (CMvMonomial σ) R compare)) @[default_instance] -instance (priority := high) : GetElem (Unlawful n R) (CMvMonomial n) R (fun lp m ↦ m ∈ lp) := +instance (priority := high) : GetElem (Unlawful σ R) (CMvMonomial σ) R (fun lp m ↦ m ∈ lp) := inferInstanceAs - (GetElem (Std.ExtTreeMap (CMvMonomial n) R compare) (CMvMonomial n) R (fun lp m ↦ m ∈ lp)) + (GetElem (Std.ExtTreeMap (CMvMonomial σ) R compare) (CMvMonomial σ) R (fun lp m ↦ m ∈ lp)) -instance : GetElem? (Unlawful n R) (CMvMonomial n) R (fun lp m ↦ m ∈ lp) := +instance : GetElem? (Unlawful σ R) (CMvMonomial σ) R (fun lp m ↦ m ∈ lp) := inferInstanceAs - (GetElem? (Std.ExtTreeMap (CMvMonomial n) R compare) (CMvMonomial n) R (fun lp m ↦ m ∈ lp)) + (GetElem? (Std.ExtTreeMap (CMvMonomial σ) R compare) (CMvMonomial σ) R (fun lp m ↦ m ∈ lp)) -instance : LawfulGetElem (Unlawful n R) (CMvMonomial n) R (fun lp m ↦ m ∈ lp) := +instance : LawfulGetElem (Unlawful σ R) (CMvMonomial σ) R (fun lp m ↦ m ∈ lp) := inferInstanceAs - (LawfulGetElem (Std.ExtTreeMap (CMvMonomial n) R compare) (CMvMonomial n) R (fun lp m ↦ m ∈ lp)) + (LawfulGetElem (Std.ExtTreeMap (CMvMonomial σ) R compare) (CMvMonomial σ) R (fun lp m ↦ m ∈ lp)) end Instances @@ -72,70 +72,66 @@ namespace Unlawful attribute [grind ext] Std.ExtTreeMap.ext_getElem? @[ext, grind ext] -lemma ext_getElem? {n R} {t₁ t₂ : Unlawful n R} - (h : ∀ (k : CMvMonomial n), t₁[k]? = t₂[k]?) : t₁ = t₂ := +lemma ext_getElem? {σ : Type*} [FinEnum σ] {R} {t₁ t₂ : Unlawful σ R} + (h : ∀ (k : CMvMonomial σ), t₁[k]? = t₂[k]?) : t₁ = t₂ := Std.ExtTreeMap.ext_getElem? h -variable {n : ℕ} {R : Type*} +variable {σ : Type*} [FinEnum σ] {R : Type*} /-- Construct an `Unlawful` polynomial from a list of monomial-coefficient pairs. -/ @[simp, grind =] -def ofList (l : List (CMvMonomial n × R)) : Unlawful n R := ExtTreeMap.ofList l compare - -/-- Extend the number of variables by padding monomials with zeros. -/ -def extend (n' : ℕ) (p : Unlawful n R) : Unlawful (n ⊔ n') R := - .ofList (p.keys.map (CMvMonomial.extend n') |>.zip p.values) +def ofList (l : List (CMvMonomial σ × R)) : Unlawful σ R := ExtTreeMap.ofList l compare /-- Check if the polynomial has no zero coefficients. -/ -abbrev isNoZeroCoef [Zero R] (p : Unlawful n R) : Prop := ∀ (m : CMvMonomial n), p[m]? ≠ some 0 +abbrev isNoZeroCoef [Zero R] (p : Unlawful σ R) : Prop := ∀ (m : CMvMonomial σ), p[m]? ≠ some 0 -def toFinset [DecidableEq R] (p : Unlawful n R) : Finset (CMvMonomial n × R) := +def toFinset [DecidableEq R] (p : Unlawful σ R) : Finset (CMvMonomial σ × R) := p.toList.toFinset /-- The list of monomials present in the polynomial. -/ -abbrev monomials (p : Unlawful n R) : List (CMvMonomial n) := +abbrev monomials (p : Unlawful σ R) : List (CMvMonomial σ) := p.keys @[simp] -lemma mem_monomials {m : CMvMonomial n} {up : Unlawful n R} : +lemma mem_monomials {m : CMvMonomial σ} {up : Unlawful σ R} : m ∈ up.monomials ↔ m ∈ up := ExtTreeMap.mem_keys -instance [Repr R] : Repr (Unlawful n R) where +instance [Repr R] : Repr (Unlawful σ R) where reprPrec p _ := if p.isEmpty then "0" else - let toFormat : Std.ToFormat (CMvMonomial n × R) := + let toFormat : Std.ToFormat (CMvMonomial σ × R) := ⟨fun (m, c) => repr c ++ " * " ++ repr m⟩ @Std.Format.joinSep _ toFormat p.toList " + " /-- Constant polynomial. -/ @[grind =] -def C [BEq R] [LawfulBEq R] [Zero R] (c : R) : Unlawful n R := +def C [BEq R] [LawfulBEq R] [Zero R] (c : R) : Unlawful σ R := if c = 0 then ∅ else .ofList [MonoR.C c] section -variable {m : ℕ} [Zero R] {x : CMvMonomial n} +variable {m : ℕ} [Zero R] {x : CMvMonomial σ} section variable [BEq R] [LawfulBEq R] -instance : OfNat (Unlawful n R) 0 := ⟨C 0⟩ +instance : OfNat (Unlawful σ R) 0 := ⟨C 0⟩ -instance [NatCast R] [NeZero m] : OfNat (Unlawful n R) m := ⟨C m⟩ +instance [NatCast R] [NeZero m] : OfNat (Unlawful σ R) m := ⟨C m⟩ @[simp, grind =] -lemma C_zero : C (n := n) (0 : R) = 0 := rfl +lemma C_zero : C (σ := σ) (0 : R) = 0 := rfl end @[simp, grind =] -lemma C_zero' : C (n := n) (0 : ℕ) = 0 := rfl +lemma C_zero' : C (σ := σ) (0 : ℕ) = 0 := rfl @[simp, grind =] lemma zero_eq_zero : (Zero.zero : R) = 0 := rfl -lemma zero_eq_empty [BEq R] [LawfulBEq R] : (0 : Unlawful n R) = ∅ := by +lemma zero_eq_empty [BEq R] [LawfulBEq R] : (0 : Unlawful σ R) = ∅ := by unfold_projs simp [C] @@ -147,88 +143,88 @@ section variable [BEq R] [LawfulBEq R] @[simp, grind .] -lemma not_mem_zero : x ∉ (0 : Unlawful n R) := by rw [← C_zero]; grind +lemma not_mem_zero : x ∉ (0 : Unlawful σ R) := by rw [← C_zero]; grind @[simp, grind .] -lemma isNoZeroCoef_zero : isNoZeroCoef (n := n) (R := R) 0 := by rw [← C_zero]; grind +lemma isNoZeroCoef_zero : isNoZeroCoef (σ := σ) (R := R) 0 := by rw [← C_zero]; grind end end /-- Pointwise addition of coefficients. -/ -def add [Add R] (p₁ p₂ : Unlawful n R) : Unlawful n R := +def add [Add R] (p₁ p₂ : Unlawful σ R) : Unlawful σ R := p₁.mergeWith (fun _ c₁ c₂ ↦ c₁ + c₂) p₂ -instance [Add R] : Add (Unlawful n R) := ⟨add⟩ +instance [Add R] : Add (Unlawful σ R) := ⟨add⟩ @[grind =] -protected lemma grind_add_skip [Add R] {p₁ p₂ : Unlawful n R} : +protected lemma grind_add_skip [Add R] {p₁ p₂ : Unlawful σ R} : p₁ + p₂ = p₁.mergeWith (fun _ c₁ c₂ ↦ c₁ + c₂) p₂ := rfl /-- Add a single monomial-coefficient term to a polynomial. -/ -def addMonoR [Add R] (p : Unlawful n R) (term : MonoR n R) : Unlawful n R := +def addMonoR [Add R] (p : Unlawful σ R) (term : MonoR σ R) : Unlawful σ R := p + .ofList [term] /-- Multiply a polynomial by a single monomial term. -/ -def mul₀ [Mul R] (t : MonoR n R) (p : Unlawful n R) : Unlawful n R := +def mul₀ [Mul R] (t : MonoR σ R) (p : Unlawful σ R) : Unlawful σ R := .ofList (p.toList.map fun (k, v) => (t.1 + k, t.2 * v)) attribute [grind =] ExtTreeMap.ofList_eq_empty_iff List.map_eq_nil_iff ExtTreeMap.toList_eq_nil_iff @[simp, grind =] -lemma mul₀_zero [Zero R] [BEq R] [LawfulBEq R] [Mul R] {t : MonoR n R} : mul₀ t 0 = 0 := by +lemma mul₀_zero [Zero R] [BEq R] [LawfulBEq R] [Mul R] {t : MonoR σ R} : mul₀ t 0 = 0 := by unfold mul₀ grind /-- Polynomial multiplication using a nested fold (distributive law). -/ -def mul [Mul R] [Add R] [Zero R] [BEq R] [LawfulBEq R] (p₁ p₂ : Unlawful n R) : Unlawful n R := +def mul [Mul R] [Add R] [Zero R] [BEq R] [LawfulBEq R] (p₁ p₂ : Unlawful σ R) : Unlawful σ R := p₁.foldl (init := 0) fun p m₁ c₁ ↦ (p₂.foldl (init := 0) fun p' m₂ c₂ ↦ {(m₁ + m₂, c₁ * c₂)} + p') + p -instance [BEq R] [LawfulBEq R] [Mul R] [Add R] [Zero R] : Mul (Unlawful n R) := ⟨mul⟩ +instance [BEq R] [LawfulBEq R] [Mul R] [Add R] [Zero R] : Mul (Unlawful σ R) := ⟨mul⟩ section Neg variable [Neg R] /-- Negation (negates all coefficients). -/ -def neg (p : Unlawful n R) : Unlawful n R := +def neg (p : Unlawful σ R) : Unlawful σ R := p.map fun _ v ↦ -v -instance : Neg (Unlawful n R) := ⟨neg⟩ +instance : Neg (Unlawful σ R) := ⟨neg⟩ /-- Subtraction. -/ -def sub [Add R] (p₁ p₂ : Unlawful n R) : Unlawful n R := +def sub [Add R] (p₁ p₂ : Unlawful σ R) : Unlawful σ R := Unlawful.add p₁ (-p₂) -instance [Add R] : Sub (Unlawful n R) := ⟨sub⟩ +instance [Add R] : Sub (Unlawful σ R) := ⟨sub⟩ end Neg /-- Return the term with the lexicographically largest monomial. -/ -def leadingTerm? : Unlawful n R → Option (MonoR n R) := +def leadingTerm? : Unlawful σ R → Option (MonoR σ R) := ExtTreeMap.maxEntry? /-- Return the lexicographically largest monomial. -/ -def leadingMonomial? : Unlawful n R → Option (CMvMonomial n) := +def leadingMonomial? : Unlawful σ R → Option (CMvMonomial σ) := .map Prod.fst ∘ Unlawful.leadingTerm? -instance instDecidableEq [DecidableEq R] : DecidableEq (Unlawful n R) := fun x y ↦ +instance instDecidableEq [DecidableEq R] : DecidableEq (Unlawful σ R) := fun x y ↦ if h : x.toList = y.toList then Decidable.isTrue (ExtTreeMap.ext_toList (h ▸ List.perm_rfl)) else Decidable.isFalse (by grind) -def coeff {R : Type*} {n : ℕ} [Zero R] (m : CMvMonomial n) (p : Unlawful n R) : R := +def coeff {R : Type*} {σ : Type*} [FinEnum σ] [Zero R] (m : CMvMonomial σ) (p : Unlawful σ R) : R := p[m]?.getD 0 @[simp, grind =] -lemma filter_get {R : Type*} [BEq R] [LawfulBEq R] {v : R} {m : CMvMonomial n} (a : Unlawful n R) : +lemma filter_get {R : Type*} [BEq R] [LawfulBEq R] {v : R} {m : CMvMonomial σ} (a : Unlawful σ R) : (ExtTreeMap.filter (fun _ c => c != v) a)[m]?.getD v = a[m]?.getD v := by grind -lemma add_getD? [AddZeroClass R] {m : CMvMonomial n} {p q : Unlawful n R} : +lemma add_getD? [AddZeroClass R] {m : CMvMonomial σ} {p q : Unlawful σ R} : (p.add q)[m]?.getD 0 = p[m]?.getD 0 + q[m]?.getD 0 := by unfold Unlawful.add by_cases m ∈ p <;> by_cases m ∈ q <;> grind [add_zero, zero_add] diff --git a/CompPoly/Multivariate/VarsDegrees.lean b/CompPoly/Multivariate/VarsDegrees.lean index 985d1e40..d7461dae 100644 --- a/CompPoly/Multivariate/VarsDegrees.lean +++ b/CompPoly/Multivariate/VarsDegrees.lean @@ -18,18 +18,18 @@ namespace CPoly open CMvPolynomial -variable {n : ℕ} {R : Type*} +variable {σ : Type*} [FinEnum σ] {R : Type*} /-- `i ∈ p.vars` iff `0 < p.degreeOf i`. -/ @[simp] lemma mem_vars_iff_degreeOf_pos [Zero R] - (i : Fin n) (p : CMvPolynomial n R) : + (i : σ) (p : CMvPolynomial σ R) : i ∈ p.vars ↔ 0 < p.degreeOf i := by simp [CMvPolynomial.vars] /-- `degrees` agrees with `MvPolynomial.degrees` via `fromCMvPolynomial`. -/ lemma degrees_equiv [CommSemiring R] [BEq R] [LawfulBEq R] - (p : CMvPolynomial n R) : + (p : CMvPolynomial σ R) : p.degrees = (fromCMvPolynomial p).degrees := by ext i have hdeg : p.degreeOf i = (fromCMvPolynomial p).degreeOf i := @@ -38,7 +38,7 @@ lemma degrees_equiv [CommSemiring R] [BEq R] [LawfulBEq R] /-- `vars` agrees with `MvPolynomial.vars` via `fromCMvPolynomial`. -/ lemma vars_equiv [CommSemiring R] [BEq R] [LawfulBEq R] - (p : CMvPolynomial n R) : + (p : CMvPolynomial σ R) : p.vars = (fromCMvPolynomial p).vars := by ext i rw [mem_vars_iff_degreeOf_pos] @@ -48,38 +48,38 @@ lemma vars_equiv [CommSemiring R] [BEq R] [LawfulBEq R] simpa [Multiset.mem_toFinset] using (Multiset.count_pos (a := i) (s := (fromCMvPolynomial p).degrees)) -/-- `(0 : CMvPolynomial n R).degreeOf i = 0`. -/ +/-- `(0 : CMvPolynomial σ R).degreeOf i = 0`. -/ @[simp] lemma degreeOf_zero [Zero R] [BEq R] [LawfulBEq R] - (i : Fin n) : - (0 : CMvPolynomial n R).degreeOf i = 0 := by - have hmonomials_zero : Lawful.monomials (0 : CMvPolynomial n R) = [] := by + (i : σ) : + (0 : CMvPolynomial σ R).degreeOf i = 0 := by + have hmonomials_zero : Lawful.monomials (0 : CMvPolynomial σ R) = [] := by apply List.eq_nil_iff_forall_not_mem.mpr intro m hm exact Lawful.not_mem_zero (x := m) ((Lawful.mem_monomials_iff).1 hm) simp [CMvPolynomial.degreeOf, hmonomials_zero] -/-- `(0 : CMvPolynomial n R).degrees = 0`. -/ +/-- `(0 : CMvPolynomial σ R).degrees = 0`. -/ @[simp] lemma degrees_zero [Zero R] [BEq R] [LawfulBEq R] : - (0 : CMvPolynomial n R).degrees = 0 := by + (0 : CMvPolynomial σ R).degrees = 0 := by simp [CMvPolynomial.degrees, degreeOf_zero] -/-- `(0 : CMvPolynomial n R).vars = ∅`. -/ +/-- `(0 : CMvPolynomial σ R).vars = ∅`. -/ @[simp] lemma vars_zero [Zero R] [BEq R] [LawfulBEq R] : - (0 : CMvPolynomial n R).vars = ∅ := by + (0 : CMvPolynomial σ R).vars = ∅ := by simp [CMvPolynomial.vars, degreeOf_zero] -/-- `(1 : CMvPolynomial n R).degrees = 0`. -/ +/-- `(1 : CMvPolynomial σ R).degrees = 0`. -/ @[simp] lemma degrees_one [CommSemiring R] [BEq R] [LawfulBEq R] : - (1 : CMvPolynomial n R).degrees = 0 := by + (1 : CMvPolynomial σ R).degrees = 0 := by simp [degrees_equiv, map_one] /-- `(p + q).vars ⊆ p.vars ∪ q.vars`. -/ lemma vars_add_subset [CommSemiring R] [BEq R] [LawfulBEq R] - (p q : CMvPolynomial n R) : + (p q : CMvPolynomial σ R) : (p + q).vars ⊆ p.vars ∪ q.vars := by rw [vars_equiv (p := p + q), vars_equiv (p := p), vars_equiv (p := q)] simpa [map_add] using diff --git a/CompPoly/Univariate/CMvEquiv.lean b/CompPoly/Univariate/CMvEquiv.lean index 175857e0..b436bb30 100644 --- a/CompPoly/Univariate/CMvEquiv.lean +++ b/CompPoly/Univariate/CMvEquiv.lean @@ -14,10 +14,10 @@ import Mathlib.Algebra.Polynomial.Degree.Lemmas # Equivalence between `CPolynomial` and `CMvPolynomial 1` This file establishes the ring equivalence -`CPolynomial.cmvEquiv : CPolynomial R ≃+* CMvPolynomial 1 R`. +`CPolynomial.cmvEquiv : CPolynomial R ≃+* CMvPolynomial (Fin 1) R`. The equivalence chain is: - `CPolynomial R ≃ R[X] ≃ (CMvPolynomial 0 R)[X] ≃ CMvPolynomial 1 R` + `CPolynomial R ≃ R[X] ≃ (CMvPolynomial 0 R)[X] ≃ CMvPolynomial (Fin 1) R` The bridge lemmas expose how the inverse equivalence interacts with evaluation and degree, so one-variable results proved for `CPolynomial` can be transported @@ -35,7 +35,7 @@ variable {R : Type*} single-variable computable multivariate polynomials. -/ noncomputable def cmvEquiv [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] : - CPolynomial R ≃+* CMvPolynomial 1 R := + CPolynomial R ≃+* CMvPolynomial (Fin 1) R := (ringEquiv (R := R)).trans <| (Polynomial.mapEquiv (CMvPolynomial.isEmptyRingEquiv (R := R))).symm.trans (CMvPolynomial.finSuccEquiv (n := 0) (R := R)).symm @@ -106,7 +106,7 @@ private lemma eval_mvToUnivariate [CommSemiring R] private theorem cmvEquiv_symm_toPoly [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] - (p : CMvPolynomial 1 R) : + (p : CMvPolynomial (Fin 1) R) : ((cmvEquiv (R := R)).symm p).toPoly = mvToUnivariate (fromCMvPolynomial p) := by rw [mvToUnivariate_eq_map_finSuccEquiv] @@ -130,14 +130,14 @@ private theorem cmvEquiv_symm_toPoly `CPolynomial` agrees with multivariate evaluation at the constant assignment. -/ theorem eval_cmvEquiv_symm [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] - (p : CMvPolynomial 1 R) (x : R) : + (p : CMvPolynomial (Fin 1) R) (x : R) : ((cmvEquiv (R := R)).symm p).eval x = p.eval (fun _ ↦ x) := by rw [eval_toPoly, cmvEquiv_symm_toPoly, eval_mvToUnivariate, ← eval_equiv] /-- Degree transport for differences through the inverse of `cmvEquiv`. -/ theorem natDegree_cmvEquiv_symm_sub [CommRing R] [BEq R] [LawfulBEq R] [Nontrivial R] - (p q : CMvPolynomial 1 R) : + (p q : CMvPolynomial (Fin 1) R) : (((cmvEquiv (R := R)).symm p - (cmvEquiv (R := R)).symm q).natDegree) = (fromCMvPolynomial p - fromCMvPolynomial q).degreeOf 0 := by rw [natDegree_toPoly, toPoly_sub, cmvEquiv_symm_toPoly, cmvEquiv_symm_toPoly, diff --git a/bench/CompPolyBench/Multivariate/CMvPolynomial.lean b/bench/CompPolyBench/Multivariate/CMvPolynomial.lean index 1c02db98..1ca65fff 100644 --- a/bench/CompPolyBench/Multivariate/CMvPolynomial.lean +++ b/bench/CompPolyBench/Multivariate/CMvPolynomial.lean @@ -47,11 +47,11 @@ private def multivariateSparseShape : String := /-- Build a computable multivariate polynomial from generated coefficients. -/ private def buildCMvPolynomial {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] - (terms : Array R) : CPoly.CMvPolynomial multivariateVars R := + (terms : Array R) : CPoly.CMvPolynomial (Fin multivariateVars) R := Id.run do - let mut p : CPoly.CMvPolynomial multivariateVars R := 0 + let mut p : CPoly.CMvPolynomial (Fin multivariateVars) R := 0 for i in [0:terms.size] do - let monomial : CPoly.CMvMonomial multivariateVars := Vector.ofFn fun j ↦ + let monomial : CPoly.CMvMonomial (Fin multivariateVars) := Vector.ofFn fun j ↦ (i / (j.val + 1)) % multivariateExponentMod p := p + CPoly.CMvPolynomial.monomial monomial (terms.getD i 0) pure p diff --git a/tests/CompPolyTests/Multivariate/CMvMonomial.lean b/tests/CompPolyTests/Multivariate/CMvMonomial.lean index 6febabdb..acd23c71 100644 --- a/tests/CompPolyTests/Multivariate/CMvMonomial.lean +++ b/tests/CompPolyTests/Multivariate/CMvMonomial.lean @@ -16,19 +16,21 @@ namespace CMvMonomial -- TODO: add more arithmetic compatibility checks with `MonoR.evalMonomial`. -example {n : ℕ} (m : CMvMonomial n) : ofFinsupp m.toFinsupp = m := by +example {σ : Type*} [FinEnum σ] (m : CMvMonomial σ) : ofFinsupp m.toFinsupp = m := by simp -example {n : ℕ} (m : Fin n →₀ ℕ) : (ofFinsupp m).toFinsupp = m := by +example {σ : Type*} [FinEnum σ] (m : σ →₀ ℕ) : (ofFinsupp m).toFinsupp = m := by simp -example {n : ℕ} (m : CMvMonomial n) : m + 0 = m := by +example {σ : Type*} [FinEnum σ] (m : CMvMonomial σ) : m + 0 = m := by simp [add_zero] -example : CMvMonomial.totalDegree (#m[1, 2] : CMvMonomial 2) = 3 := by +example : let v : Vector ℕ 2 := #m[1, 2]; CMvMonomial.totalDegree (σ := Fin 2) v = 3 := by decide -example : CMvMonomial.degreeOf (#m[3, 4] : CMvMonomial 2) ⟨1, by decide⟩ = 4 := by +example : + let v : Vector ℕ 2 := #m[3, 4] + CMvMonomial.degreeOf (σ := Fin 2) v ⟨1, by decide⟩ = 4 := by decide end CMvMonomial diff --git a/tests/CompPolyTests/Multivariate/Restrict.lean b/tests/CompPolyTests/Multivariate/Restrict.lean index f884969f..d8bffd18 100644 --- a/tests/CompPolyTests/Multivariate/Restrict.lean +++ b/tests/CompPolyTests/Multivariate/Restrict.lean @@ -17,21 +17,22 @@ open CMvPolynomial -- TODO: add concrete finite-support examples exercising mixed degree bounds. -example (d : ℕ) : restrictTotalDegree (n := 2) (R := ℚ) d (0 : CMvPolynomial 2 ℚ) = 0 := by +example (d : ℕ) : + restrictTotalDegree (σ := Fin 2) (R := ℚ) d (0 : CMvPolynomial (Fin 2) ℚ) = 0 := by simp [restrictTotalDegree_zero] -example (d : ℕ) : restrictDegree (n := 2) (R := ℚ) d (0 : CMvPolynomial 2 ℚ) = 0 := by +example (d : ℕ) : restrictDegree (σ := Fin 2) (R := ℚ) d (0 : CMvPolynomial (Fin 2) ℚ) = 0 := by simp [restrictDegree_zero] -example (d d' : ℕ) (p : CMvPolynomial 2 ℚ) : +example (d d' : ℕ) (p : CMvPolynomial (Fin 2) ℚ) : restrictTotalDegree d (restrictTotalDegree d' p) = restrictTotalDegree (min d d') p := by simp [restrictTotalDegree_restrictTotalDegree] -example (d d' : ℕ) (p : CMvPolynomial 2 ℚ) : +example (d d' : ℕ) (p : CMvPolynomial (Fin 2) ℚ) : restrictDegree d (restrictDegree d' p) = restrictDegree (min d d') p := by simp [restrictDegree_restrictDegree] -example (d d' : ℕ) (p : CMvPolynomial 2 ℚ) : +example (d d' : ℕ) (p : CMvPolynomial (Fin 2) ℚ) : restrictTotalDegree d (restrictDegree d' p) = restrictDegree d' (restrictTotalDegree d p) := by simp [restrictTotalDegree_restrictDegree_comm] diff --git a/tests/CompPolyTests/Multivariate/TypeclassMinimization.lean b/tests/CompPolyTests/Multivariate/TypeclassMinimization.lean index 7c716150..6cce6ae9 100644 --- a/tests/CompPolyTests/Multivariate/TypeclassMinimization.lean +++ b/tests/CompPolyTests/Multivariate/TypeclassMinimization.lean @@ -65,37 +65,32 @@ private def x1 : Fin 2 := ⟨1, by decide⟩ private def collapse : Fin 2 → Fin 1 := fun _ => ⟨0, by decide⟩ -example : CMvPolynomial 2 MinimalCoeff := +example : CMvPolynomial (Fin 2) MinimalCoeff := X (R := MinimalCoeff) x0 example : ℕ := totalDegree <| X (R := MinimalCoeff) x0 -example : CMvPolynomial 1 MinimalCoeff := +example : CMvPolynomial (Fin 1) MinimalCoeff := rename (R := MinimalCoeff) collapse (X (R := MinimalCoeff) x0) -example : CMvPolynomial 2 MinimalCoeff := +example : CMvPolynomial (Fin 2) MinimalCoeff := sumToIter <| X (R := MinimalCoeff) x0 + X (R := MinimalCoeff) x1 -example (p : CMvPolynomial 2 MinimalCoeff) : CMvPolynomial 2 MinimalCoeff := +example (p : CMvPolynomial (Fin 2) MinimalCoeff) : CMvPolynomial (Fin 2) MinimalCoeff := -p -example (p q : CMvPolynomial 2 MinimalCoeff) : CMvPolynomial 2 MinimalCoeff := +example (p q : CMvPolynomial (Fin 2) MinimalCoeff) : CMvPolynomial (Fin 2) MinimalCoeff := p - q -example (p : CMvPolynomial 1 MinimalCoeff) (q : CMvPolynomial 2 MinimalCoeff) : - CMvPolynomial 2 MinimalCoeff := - p + q - -example (p : CMvPolynomial 1 MinimalCoeff) (q : CMvPolynomial 2 MinimalCoeff) : - CMvPolynomial 2 MinimalCoeff := - p - q - -example (p : CMvPolynomial 1 MinimalCoeff) (q : CMvPolynomial 2 MinimalCoeff) : - CMvPolynomial 2 MinimalCoeff := - p * q +-- Combining polynomials over different variable types is done explicitly via +-- `embedDomain`/`rename` (the caller chooses the embedding); there are intentionally no +-- mixed-arity `+`/`*`/`-` instances. `embedDomain` holds under the weakened assumptions. +example (p : CMvPolynomial (Fin 1) MinimalCoeff) : + CMvPolynomial (Fin 1 ⊕ Fin 2) MinimalCoeff := + embedDomain ⟨Sum.inl, Sum.inl_injective⟩ p end CMvPolynomial diff --git a/tests/CompPolyTests/Multivariate/VarsDegrees.lean b/tests/CompPolyTests/Multivariate/VarsDegrees.lean index 205c4d01..2a258978 100644 --- a/tests/CompPolyTests/Multivariate/VarsDegrees.lean +++ b/tests/CompPolyTests/Multivariate/VarsDegrees.lean @@ -17,19 +17,19 @@ open CMvPolynomial -- TODO: add nontrivial examples relating `vars`/`degrees` to explicit monomials. -example (i : Fin 3) : (0 : CMvPolynomial 3 ℚ).degreeOf i = 0 := by +example (i : Fin 3) : (0 : CMvPolynomial (Fin 3) ℚ).degreeOf i = 0 := by simp [degreeOf_zero] -example : (0 : CMvPolynomial 3 ℚ).degrees = 0 := by +example : (0 : CMvPolynomial (Fin 3) ℚ).degrees = 0 := by simp [degrees_zero] -example : (0 : CMvPolynomial 3 ℚ).vars = ∅ := by +example : (0 : CMvPolynomial (Fin 3) ℚ).vars = ∅ := by simp [vars_zero] -example : (1 : CMvPolynomial 3 ℚ).degrees = 0 := by +example : (1 : CMvPolynomial (Fin 3) ℚ).degrees = 0 := by simp [degrees_one] -example (p : CMvPolynomial 3 ℚ) (i : Fin 3) : +example (p : CMvPolynomial (Fin 3) ℚ) (i : Fin 3) : i ∈ p.vars ↔ 0 < p.degreeOf i := by simp [mem_vars_iff_degreeOf_pos]