diff --git a/AGENTS.md b/AGENTS.md index c5b1ac11..751ebb5c 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -54,6 +54,8 @@ Human contributors should usually start with [`README.md`](README.md), rules for generated or derived outputs. - [`docs/wiki/representations-and-bridges.md`](docs/wiki/representations-and-bridges.md) - main polynomial representations and Mathlib bridge layers. +- [`docs/wiki/typeclass-minimization.md`](docs/wiki/typeclass-minimization.md) - + minimal typeclass assumptions and no-blanket-scope guidance. - [`docs/wiki/binary-fields-and-ntt.md`](docs/wiki/binary-fields-and-ntt.md) - binary-field stack, GHASH, and additive NTT. @@ -88,6 +90,10 @@ trusting the compiler. that cause `simp` to unfold typeclass internals and balloon unification work. - Prefer explicit instance constructions such as `Field.isDomain` over `inferInstance` when the synthesis path is long or ambiguous. +- State the minimal typeclass assumptions for each new `def`, `instance`, + `lemma`, and `theorem`. Avoid blanket section-level `variable [...]` + declarations unless every declaration in scope genuinely needs them; see + [`docs/wiki/typeclass-minimization.md`](docs/wiki/typeclass-minimization.md). ### Tactics diff --git a/CompPoly/Bivariate/Basic.lean b/CompPoly/Bivariate/Basic.lean index f47104b3..4d3da5c8 100644 --- a/CompPoly/Bivariate/Basic.lean +++ b/CompPoly/Bivariate/Basic.lean @@ -27,16 +27,14 @@ namespace CompPoly Each `p : CBivariate R` is a polynomial in `Y` whose coefficients are univariate polynomials in `X`. The outer structure is indexed by powers of `Y`, the inner by powers of `X`. -/ -def CBivariate (R : Type*) [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] := +def CBivariate (R : Type*) [Zero R] := CPolynomial (CPolynomial R) namespace CBivariate -variable {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] +section ZeroOnly -section Semiring - -variable [Semiring R] +variable {R : Type*} [Zero R] /-- Extensionality: two bivariate polynomials are equal if their underlying values are. -/ @[ext] theorem ext {p q : CBivariate R} (h : p.val = q.val) : p = q := @@ -48,6 +46,22 @@ instance : Coe (CBivariate R) (CPolynomial (CPolynomial R)) where coe := id /-- The zero bivariate polynomial is canonical. -/ instance : Inhabited (CBivariate R) := inferInstanceAs (Inhabited (CPolynomial (CPolynomial R))) +instance [BEq R] : BEq (CBivariate R) := + inferInstanceAs (BEq (CPolynomial (CPolynomial R))) + +instance [BEq R] [LawfulBEq R] : LawfulBEq (CBivariate R) := + inferInstanceAs (LawfulBEq (CPolynomial (CPolynomial R))) + +instance [DecidableEq R] : DecidableEq (CBivariate R) := + inferInstanceAs (DecidableEq (CPolynomial (CPolynomial R))) + +end ZeroOnly + +section Semiring + +variable {R : Type*} +variable [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] + /-- Additive structure on CBivariate R -/ instance : AddCommMonoid (CBivariate R) := inferInstanceAs (AddCommMonoid (CPolynomial (CPolynomial R))) @@ -60,36 +74,34 @@ end Semiring section CommSemiring -variable [CommSemiring R] +variable {R : Type*} +variable [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] -instance : CommSemiring (CBivariate R) := by - letI : CommSemiring (CPolynomial R) := inferInstance - simpa [CBivariate] using (inferInstance : CommSemiring (CPolynomial (CPolynomial R))) +instance : CommSemiring (CBivariate R) := + inferInstanceAs (CommSemiring (CPolynomial (CPolynomial R))) end CommSemiring section Ring -variable [Ring R] +variable {R : Type*} +variable [Ring R] [BEq R] [LawfulBEq R] [Nontrivial R] -instance : Ring (CBivariate R) := by - letI : Ring (CPolynomial R) := inferInstance - simpa [CBivariate] using (inferInstance : Ring (CPolynomial (CPolynomial R))) +instance : Ring (CBivariate R) := + inferInstanceAs (Ring (CPolynomial (CPolynomial R))) end Ring section CommRing -variable [CommRing R] +variable {R : Type*} +variable [CommRing R] [BEq R] [LawfulBEq R] [Nontrivial R] -instance : CommRing (CBivariate R) := by - letI : CommRing (CPolynomial R) := inferInstance - simpa [CBivariate] using (inferInstance : CommRing (CPolynomial (CPolynomial R))) +instance : CommRing (CBivariate R) := + inferInstanceAs (CommRing (CPolynomial (CPolynomial R))) end CommRing --- TODO any remaining typeclasses? - -- --------------------------------------------------------------------------- -- Operation stubs (for ArkLib compatibility; proofs deferred) -- --------------------------------------------------------------------------- @@ -102,81 +114,89 @@ end CommRing section Operations -variable (R : Type*) [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] - /-- Constant as a bivariate polynomial. Mathlib: `Polynomial.Bivariate.CC`. -/ -def CC (r : R) : CBivariate R := CPolynomial.C (CPolynomial.C r) +def CC {R : Type*} [Zero R] [BEq R] [LawfulBEq R] (r : R) : CBivariate R := + CPolynomial.C (CPolynomial.C r) /-- The variable X (inner variable). As bivariate: polynomial in Y with single coeff `X` at Y^0. -/ -def X : CBivariate R := CPolynomial.C CPolynomial.X +def X {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] : CBivariate R := + CPolynomial.C CPolynomial.X /-- The variable Y (outer variable). Monomial `Y^1` with coefficient 1. -/ -def Y [DecidableEq R] : CBivariate R := CPolynomial.monomial 1 (CPolynomial.C 1) +def Y {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] : + CBivariate R := + CPolynomial.monomial 1 (CPolynomial.C 1) /-- Monomial `c * X^n * Y^m`. ArkLib: `Polynomial.Bivariate.monomialXY`. -/ -def monomialXY [DecidableEq R] (n m : ℕ) (c : R) : CBivariate R := +def monomialXY {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] + (n m : ℕ) (c : R) : CBivariate R := CPolynomial.monomial m (CPolynomial.monomial n c) /-- Coefficient of `X^i Y^j` in the bivariate polynomial. Here `i` is the X-exponent (inner) and `j` is the Y-exponent (outer). ArkLib: `Polynomial.Bivariate.coeff f i j`. -/ -def coeff (f : CBivariate R) (i j : ℕ) : R := +def coeff {R : Type*} [Zero R] (f : CBivariate R) (i j : ℕ) : R := (f.val.coeff j).coeff i /-- The Y-support: indices j such that the coefficient of Y^j is nonzero. -/ -def supportY (f : CBivariate R) : Finset ℕ := CPolynomial.support f +def supportY {R : Type*} [Zero R] [BEq R] (f : CBivariate R) : Finset ℕ := CPolynomial.support f /-- The X-support: indices i such that the coefficient of X^i is nonzero (i.e. some monomial X^i Y^j has nonzero coefficient). -/ -def supportX (f : CBivariate R) : Finset ℕ := +def supportX {R : Type*} [Zero R] [BEq R] (f : CBivariate R) : Finset ℕ := (CPolynomial.support f).biUnion (fun j ↦ CPolynomial.support (f.val.coeff j)) /-- The `Y`-degree (degree when viewed as a polynomial in `Y`). ArkLib: `Polynomial.Bivariate.natDegreeY`. -/ -def natDegreeY (f : CBivariate R) : ℕ := - f.val.natDegree +def natDegreeY {R : Type*} [Zero R] (f : CBivariate R) : ℕ := + f.natDegree /-- The `X`-degree: maximum over all Y-coefficients of their degree in X. ArkLib: `Polynomial.Bivariate.natDegreeX`. -/ -def natDegreeX (f : CBivariate R) : ℕ := +def natDegreeX {R : Type*} [Zero R] [BEq R] (f : CBivariate R) : ℕ := (CPolynomial.support f).sup (fun n ↦ (f.val.coeff n).natDegree) /-- Total degree: max over monomials of (deg_X + deg_Y). ArkLib: `Polynomial.Bivariate.totalDegree`. -/ -def totalDegree (f : CBivariate R) : ℕ := +def totalDegree {R : Type*} [Zero R] [BEq R] (f : CBivariate R) : ℕ := (CPolynomial.support f).sup (fun m ↦ (f.val.coeff m).natDegree + m) /-- Evaluate in the first variable (X) at `a`, yielding a univariate polynomial in Y. ArkLib: `Polynomial.Bivariate.evalX`. -/ -def evalX [DecidableEq R] (a : R) (f : CBivariate R) : CPolynomial R := +def evalX {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] [DecidableEq R] + (a : R) (f : CBivariate R) : CPolynomial R := (CPolynomial.support f).sum (fun j ↦ CPolynomial.monomial j (CPolynomial.eval a (f.val.coeff j))) /-- Evaluate in the second variable (Y) at `a`, yielding a univariate polynomial in X. ArkLib: `Polynomial.Bivariate.evalY`. -/ -def evalY (a : R) (f : CBivariate R) : CPolynomial R := +def evalY {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] + (a : R) (f : CBivariate R) : CPolynomial R := f.val.eval (CPolynomial.C a) /-- Full evaluation at `(x, y)`: `p(x, y)`. Inner variable X at `x`, outer variable Y at `y`. Equivalently `(evalY y f).eval x`. Mathlib: `Polynomial.evalEval`. -/ -def evalEval (x y : R) (f : CBivariate R) : R := +def evalEval {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] + (x y : R) (f : CBivariate R) : R := CPolynomial.eval x (f.val.eval (CPolynomial.C y)) /-- Swap the roles of X and Y. ArkLib/Mathlib: `Polynomial.Bivariate.swap`. TODO a more efficient implementation -/ -def swap [DecidableEq R] (f : CBivariate R) : CBivariate R := +def swap {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] + (f : CBivariate R) : CBivariate R := (f.supportY).sum (fun j ↦ (CPolynomial.support (f.val.coeff j)).sum (fun i ↦ CPolynomial.monomial i (CPolynomial.monomial j ((f.val.coeff j).coeff i)))) /-- Leading coefficient when viewed as a polynomial in Y. ArkLib: `Polynomial.Bivariate.leadingCoeffY`. -/ -def leadingCoeffY (f : CBivariate R) : CPolynomial R := - f.val.leadingCoeff +def leadingCoeffY {R : Type*} [Zero R] (f : CBivariate R) : CPolynomial R := + f.leadingCoeff /-- Leading coefficient when viewed as a polynomial in X. The coefficient of X^(degreeX f): a polynomial in Y. -/ -def leadingCoeffX [DecidableEq R] (f : CBivariate R) : CPolynomial R := +def leadingCoeffX {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] + (f : CBivariate R) : CPolynomial R := (f.swap).leadingCoeffY end Operations diff --git a/CompPoly/Bivariate/ToPoly.lean b/CompPoly/Bivariate/ToPoly.lean index 4ba7579b..3f7ea03a 100644 --- a/CompPoly/Bivariate/ToPoly.lean +++ b/CompPoly/Bivariate/ToPoly.lean @@ -39,7 +39,7 @@ section ToPolyCore Maps each Y-coefficient through `CPolynomial.toPoly`, then builds `Polynomial (Polynomial R)` as the sum of monomials. -/ -noncomputable def toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] +noncomputable def toPoly {R : Type*} [BEq R] [LawfulBEq R] [Semiring R] (p : CBivariate R) : R[X][Y] := (CPolynomial.support p).sum (fun j ↦ monomial j (CPolynomial.toPoly (p.val.coeff j))) @@ -49,14 +49,14 @@ noncomputable def toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring Extracts each Y-coefficient via `p.coeff`, converts to `CPolynomial R` via `toImpl` and trimming, then builds the canonical bivariate sum. -/ -def ofPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] +def ofPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] (p : R[X][Y]) : CBivariate R := (p.support).sum (fun j ↦ let cj := p.coeff j - CPolynomial.monomial j ⟨cj.toImpl, CPolynomial.Raw.trim_toImpl cj⟩) + CPolynomial.monomial j ⟨cj.toImpl, CPolynomial.Raw.isCanonical_toImpl cj⟩) /-- `toPoly` preserves addition. -/ -lemma toPoly_add {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] +lemma toPoly_add {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (p q : CBivariate R) : toPoly (p + q) = toPoly p + toPoly q := by have h_linear : ∀ (p q : CPolynomial R), (p + q).toPoly = p.toPoly + q.toPoly := by intros p q @@ -99,7 +99,8 @@ lemma toPoly_add {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] grind /-- `toPoly` sends a Y-monomial to the corresponding monomial in `R[X][Y]`. -/ -lemma toPoly_monomial {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] [DecidableEq R] +lemma toPoly_monomial {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] + [DecidableEq R] (n : ℕ) (c : CPolynomial R) : toPoly (CPolynomial.monomial n c) = monomial n (c.toPoly) := by unfold CPolynomial.monomial @@ -113,10 +114,11 @@ lemma toPoly_monomial {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] exact toFinsupp_eq_zero.mp rfl /-- `ofPoly` sends a Y-monomial in `R[X][Y]` to a bivariate monomial. -/ -lemma ofPoly_monomial {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] [DecidableEq R] +lemma ofPoly_monomial {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] + [DecidableEq R] (n : ℕ) (c : R[X]) : ofPoly (monomial n c) = - CPolynomial.monomial n ⟨c.toImpl, CPolynomial.Raw.trim_toImpl c⟩ := by + CPolynomial.monomial n ⟨c.toImpl, CPolynomial.Raw.isCanonical_toImpl c⟩ := by unfold CBivariate.ofPoly simp +decide rw [ Finset.sum_eq_single n ] <;> simp +decide [ Polynomial.coeff_monomial ] @@ -125,7 +127,7 @@ lemma ofPoly_monomial {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] /-- `Polynomial.toImpl` preserves addition, accounting for trimming in the raw representation. -/ -lemma toImpl_add {R : Type*} [BEq R] [LawfulBEq R] [Ring R] (p q : R[X]) : +lemma toImpl_add {R : Type*} [BEq R] [LawfulBEq R] [Semiring R] (p q : R[X]) : p.toImpl + q.toImpl = (p + q).toImpl := by have h_add : (p.toImpl + q.toImpl).toPoly = (p + q).toImpl.toPoly := by have h_add : (p.toImpl + q.toImpl).toPoly = p.toImpl.toPoly + q.toImpl.toPoly := by @@ -152,7 +154,8 @@ lemma toImpl_add {R : Type*} [BEq R] [LawfulBEq R] [Ring R] (p q : R[X]) : · exact Eq.symm (CPolynomial.Raw.trim_toImpl (p + q)) /-- `ofPoly` preserves addition in `R[X][Y]`. -/ -lemma ofPoly_add {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] [DecidableEq R] +lemma ofPoly_add {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] + [DecidableEq R] (p q : R[X][Y]) : ofPoly (p + q) = ofPoly p + ofPoly q := by -- Sum of two polynomials is sum of their coefficients; convert back using `ofPoly`. have h_ofPoly_add_p : ∀ (p q : Polynomial (Polynomial R)), @@ -179,7 +182,8 @@ lemma ofPoly_add {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] [Deci exact h_ofPoly_add_p p q /-- The outer coefficient of `ofPoly p` converts back to the corresponding `R[X]` coefficient. -/ -theorem ofPoly_coeff {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] [DecidableEq R] +theorem ofPoly_coeff {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] + [DecidableEq R] (p : R[X][Y]) (n : ℕ) : (CPolynomial.coeff (ofPoly p) n).toPoly = p.coeff n := by -- By definition of `coeff`, we can express it as a sum over the support of `p`. have h_coeff_sum : CPolynomial.coeff (ofPoly p) n = @@ -187,7 +191,7 @@ theorem ofPoly_coeff {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] [ CPolynomial.coeff (CPolynomial.monomial j ⟨Polynomial.toImpl (Polynomial.coeff p j), - CPolynomial.Raw.trim_toImpl (Polynomial.coeff p j)⟩) n) := by + CPolynomial.Raw.isCanonical_toImpl (Polynomial.coeff p j)⟩) n) := by unfold CBivariate.ofPoly induction' p.support using Finset.induction with j s hj ih · exact CPolynomial.eq_iff_coeff.mpr (congrFun rfl) @@ -202,7 +206,7 @@ theorem ofPoly_coeff {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] [ · aesop /-- The outer coefficient of `toPoly p` is `CPolynomial.coeff p n` converted to `R[X]`. -/ -theorem toPoly_coeff {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] +theorem toPoly_coeff {R : Type*} [BEq R] [LawfulBEq R] [Semiring R] (p : CBivariate R) (n : ℕ) : (toPoly p).coeff n = (CPolynomial.coeff p n).toPoly := by rw [ CBivariate.toPoly, Polynomial.finset_sum_coeff ] rw [ Finset.sum_eq_single n ] <;> simp +contextual [ Polynomial.coeff_monomial ] @@ -212,7 +216,7 @@ theorem toPoly_coeff {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] /-- `toPoly` is the map of the outer polynomial via `CPolynomial.ringEquiv`. -/ -theorem toPoly_eq_map {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] +theorem toPoly_eq_map {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (p : CBivariate R) : toPoly p = (CPolynomial.toPoly p).map (CPolynomial.ringEquiv (R := R)) := by convert Polynomial.ext _ @@ -228,7 +232,7 @@ theorem toPoly_eq_map {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] by_cases h : n < Array.size p.val <;> aesop /-- `toPoly` preserves multiplication. -/ -theorem toPoly_mul {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] +theorem toPoly_mul {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (p q : CBivariate R) : toPoly (p * q) = toPoly p * toPoly q := by have h_mul : (p * q).toPoly = @@ -242,7 +246,8 @@ end ToPolyCore section RingEquiv /-- Round-trip from Mathlib: converting a polynomial to `CBivariate` and back is the identity. -/ -theorem ofPoly_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] [DecidableEq R] +theorem ofPoly_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] + [DecidableEq R] (p : R[X][Y]) : toPoly (ofPoly p) = p := by induction p using Polynomial.induction_on' · rw [ ofPoly_add, toPoly_add, @@ -252,7 +257,8 @@ theorem ofPoly_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] exact congr_arg _ ( CPolynomial.Raw.toPoly_toImpl ) /-- Round-trip from `CBivariate`: converting to Mathlib and back is the identity. -/ -theorem toPoly_ofPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] [DecidableEq R] +theorem toPoly_ofPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] + [DecidableEq R] (p : CBivariate R) : ofPoly (toPoly p) = p := by apply CPolynomial.eq_iff_coeff.mpr intro i @@ -268,7 +274,7 @@ theorem toPoly_ofPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] /-- Ring equivalence between `CBivariate R` and Mathlib's `R[X][Y]`. -/ noncomputable def ringEquiv - {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] [DecidableEq R] : + {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] : CBivariate R ≃+* R[X][Y] where toFun := toPoly invFun := ofPoly @@ -279,20 +285,20 @@ noncomputable def ringEquiv /-- `toPoly` preserves `1`. -/ theorem toPoly_one - {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] [DecidableEq R] : + {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] : toPoly (1 : CBivariate R) = 1 := by simpa [ringEquiv] using (ringEquiv (R := R)).map_one /-- `ofPoly` preserves `1`. -/ theorem ofPoly_one - {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] [DecidableEq R] : + {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] : ofPoly (1 : R[X][Y]) = 1 := by apply (ringEquiv (R := R)).injective change toPoly (ofPoly (1 : R[X][Y])) = toPoly (1 : CBivariate R) rw [ofPoly_toPoly, toPoly_one] /-- `toPoly` maps the zero bivariate polynomial to `0`. -/ -lemma toPoly_zero {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] : +lemma toPoly_zero {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] : toPoly (0 : CBivariate R) = 0 := by -- The sum over the empty set is zero. simp [CBivariate.toPoly] @@ -300,26 +306,26 @@ lemma toPoly_zero {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] : aesop /-- `ofPoly` maps `0` in `R[X][Y]` to the zero bivariate polynomial. -/ -lemma ofPoly_zero {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] [DecidableEq R] : +lemma ofPoly_zero {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] : ofPoly (0 : R[X][Y]) = 0 := by unfold CBivariate.ofPoly simp +decide [ Polynomial.support ] /-- Ring hom from computable bivariates to Mathlib bivariates. -/ noncomputable def toPolyRingHom - {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] [DecidableEq R] : + {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] : CBivariate R →+* R[X][Y] := (ringEquiv (R := R)).toRingHom /-- Ring hom from Mathlib bivariates to computable bivariates. -/ noncomputable def ofPolyRingHom - {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] [DecidableEq R] : + {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] : R[X][Y] →+* CBivariate R := (ringEquiv (R := R)).symm.toRingHom /-- `ofPoly` preserves multiplication. -/ theorem ofPoly_mul - {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] [DecidableEq R] + {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] (p q : R[X][Y]) : ofPoly (p * q) = ofPoly p * ofPoly q := by apply (ringEquiv (R := R)).injective @@ -333,7 +339,7 @@ end RingEquiv /-- Converting a `foldl` over `Array.zipIdx` of `CPolynomial` coefficients to a `Finset.sum` of their `toPoly` images commutes with the `toPoly` map. -/ private theorem toPoly_foldl_zipIdx_eq_sum {R : Type*} [BEq R] [LawfulBEq R] - [Nontrivial R] [Ring R] (arr : Array (CPolynomial R)) (y : R) : + [Nontrivial R] [Semiring R] (arr : Array (CPolynomial R)) (y : R) : (Array.foldl (fun (acc : CPolynomial R) (x : CPolynomial R × ℕ) ↦ acc + x.1 * CPolynomial.C y ^ x.2) 0 (Array.zipIdx arr) 0 arr.size).toPoly = ∑ i ∈ Finset.range arr.size, (arr[i]?.getD 0).toPoly * (Polynomial.C y) ^ i := by @@ -361,7 +367,7 @@ private theorem toPoly_foldl_zipIdx_eq_sum {R : Type*} [BEq R] [LawfulBEq R] section ImplementationCorrectness /-- `toPoly` preserves full evaluation: `evalEval x y f = (toPoly f).evalEval x y`. -/ -theorem evalEval_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] +theorem evalEval_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (x y : R) (f : CBivariate R) : @CBivariate.evalEval R _ _ _ _ x y f = (toPoly f).evalEval x y := by unfold CBivariate.evalEval Polynomial.evalEval @@ -384,18 +390,15 @@ theorem evalEval_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R exact CPolynomial.eval_toPoly x (CPolynomial.Raw.eval (CPolynomial.C y) ↑f) /-- `toPoly` preserves coefficients: coefficient of `X^i Y^j` matches. -/ -theorem coeff_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] +theorem coeff_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (f : CBivariate R) (i j : ℕ) : - ((toPoly f).coeff j).coeff i = @CBivariate.coeff R _ _ _ _ f i j := by - convert CPolynomial.Raw.coeff_toPoly using 1 - rw [ CBivariate.toPoly ] - simp +decide [ Polynomial.coeff_monomial ] - split_ifs <;> simp_all +decide [ CPolynomial.support ] - · congr - · by_cases h : j < ( f.val.size : ℕ ) <;> aesop + ((toPoly f).coeff j).coeff i = CBivariate.coeff (R := R) f i j := by + rw [toPoly_coeff] + simpa [CBivariate.coeff] using + (CPolynomial.coeff_toPoly (p := CPolynomial.coeff f j) (i := i)).symm /-- The outer support of `toPoly f` equals the Y-support of `f`. -/ -theorem support_toPoly_outer {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] +theorem support_toPoly_outer {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (f : CBivariate R) : (toPoly f).support = f.supportY := by ext x simp +decide [ CPolynomial.mem_support_iff, CBivariate.supportY ] @@ -405,9 +408,8 @@ theorem support_toPoly_outer {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [R aesop /-- `toPoly` preserves Y-degree. -/ -theorem natDegreeY_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] +theorem natDegreeY_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (f : CBivariate R) : (toPoly f).natDegree = f.natDegreeY := by - unfold CBivariate.natDegreeY -- The degree of the polynomial is the supremum of the exponents in its support. have h_deg : ∀ p : Polynomial (Polynomial R), p.natDegree = p.support.sup id := by intro p @@ -419,10 +421,11 @@ theorem natDegreeY_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring rw [ h_deg, support_toPoly_outer ] -- Apply the fact that the degree of a polynomial is equal to the supremum of its support. apply Eq.symm - exact CPolynomial.natDegree_eq_support_sup f + simpa [CBivariate.natDegreeY, CBivariate.supportY, id] using + (CPolynomial.natDegree_eq_support_sup (p := f)) /-- The outer `Y`-coefficient formula used for X-degree transport. -/ -theorem coeff_toPoly_Y {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] +theorem coeff_toPoly_Y {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (f : CBivariate R) (j : ℕ) : (toPoly f).coeff j = CPolynomial.toPoly (f.val.coeff j) := by erw [ Polynomial.finset_sum_coeff ] @@ -434,7 +437,7 @@ theorem coeff_toPoly_Y {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] · exact (CPolynomial.toPoly_eq_zero_iff 0).mpr rfl /-- `toPoly` preserves X-degree (max over Y-coefficients of their degree in X). -/ -theorem natDegreeX_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] +theorem natDegreeX_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (f : CBivariate R) : (toPoly f).support.sup (fun j ↦ ((toPoly f).coeff j).natDegree) = f.natDegreeX := by convert (Finset.sup_congr ?_ ?_) @@ -460,7 +463,7 @@ theorem natDegreeX_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring /-- `CC` corresponds to the nested constant polynomial in `R[X][Y]`. -/ -theorem CC_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] (r : R) : +theorem CC_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (r : R) : toPoly (CC (R := R) r) = Polynomial.C (Polynomial.C r) := by rw [ toPoly_eq_map ] unfold CBivariate.CC @@ -471,7 +474,7 @@ theorem CC_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] (r : /-- `X` (inner variable) corresponds to `Polynomial.C Polynomial.X` in `R[X][Y]`. -/ -theorem X_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] : +theorem X_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] : toPoly (X (R := R)) = Polynomial.C Polynomial.X := by rw [ toPoly_eq_map ] simp [ CBivariate.X, CPolynomial.C_toPoly ] @@ -481,7 +484,7 @@ theorem X_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] : /-- `Y` (outer variable) corresponds to `Polynomial.X` in `R[X][Y]`. -/ -theorem Y_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] [DecidableEq R] : +theorem Y_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] : toPoly (CBivariate.Y (R := R)) = (Polynomial.X : Polynomial (Polynomial R)) := by simpa [CBivariate.Y, CPolynomial.C_toPoly] using (toPoly_monomial (R := R) 1 (CPolynomial.C 1)) @@ -489,7 +492,7 @@ theorem Y_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] [Deci /-- `monomialXY n m c` corresponds to `Y^m` with inner coefficient `X^n * c`. -/ -theorem monomialXY_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] +theorem monomialXY_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] (n m : ℕ) (c : R) : toPoly (monomialXY (R := R) n m c) = Polynomial.monomial m (Polynomial.monomial n c) := by unfold CBivariate.monomialXY @@ -500,7 +503,7 @@ theorem monomialXY_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring /-- `supportX` corresponds to the union of inner supports of outer coefficients. -/ -theorem supportX_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] +theorem supportX_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (f : CBivariate R) : CBivariate.supportX (R := R) f = (toPoly f).support.biUnion (fun j ↦ ((toPoly f).coeff j).support) := by @@ -513,7 +516,7 @@ theorem supportX_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R /-- `totalDegree` corresponds to the supremum over `j` of `natDegree ((toPoly f).coeff j) + j`. -/ -theorem totalDegree_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] +theorem totalDegree_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (f : CBivariate R) : CBivariate.totalDegree (R := R) f = (toPoly f).support.sup (fun j ↦ ((toPoly f).coeff j).natDegree + j) := by @@ -527,7 +530,7 @@ theorem totalDegree_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Rin /-- `evalX a` evaluates each inner coefficient at `a`. -/ -theorem evalX_toPoly_coeff {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] +theorem evalX_toPoly_coeff {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] (a : R) (f : CBivariate R) (j : ℕ) : ((evalX (R := R) a f).toPoly).coeff j = ((toPoly f).coeff j).eval a := by have h₁ : @@ -552,7 +555,7 @@ theorem evalX_toPoly_coeff {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Rin /-- `evalX` is compatible with full bivariate evaluation when `a` and `y` commute. -/ -theorem evalX_toPoly_eval_commute {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] +theorem evalX_toPoly_eval_commute {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] (a y : R) (hc : Commute a y) (f : CBivariate R) : (evalX (R := R) a f).eval y = (toPoly f).evalEval a y := by have h_lhs : @@ -592,7 +595,7 @@ theorem evalX_toPoly_eval_commute {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial /-- `evalX_toPoly_eval_commute` specialized to commutative rings. -/ -theorem evalX_toPoly_eval {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [CommRing R] +theorem evalX_toPoly_eval {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [CommSemiring R] [DecidableEq R] (a y : R) (f : CBivariate R) : (evalX (R := R) a f).eval y = (toPoly f).evalEval a y := by simpa using @@ -603,7 +606,7 @@ The `Commute` hypothesis in `evalX_toPoly_eval_commute` is necessary: if the identity holds for every bivariate polynomial then `a` and `y` commute. -/ theorem evalX_toPoly_eval_commute_converse - {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] [DecidableEq R] + {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] (a y : R) (h : ∀ f : CBivariate R, (evalX (R := R) a f).eval y = (toPoly f).evalEval a y) : @@ -629,7 +632,7 @@ theorem evalX_toPoly_eval_commute_converse /-- `evalY a` corresponds to outer evaluation at `Polynomial.C a`. -/ -theorem evalY_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] +theorem evalY_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (a : R) (f : CBivariate R) : (evalY (R := R) a f).toPoly = (toPoly f).eval (Polynomial.C a) := by unfold CBivariate.evalY @@ -651,24 +654,22 @@ theorem evalY_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] /-- `leadingCoeffY` corresponds to the leading coefficient in the outer variable. -/ -theorem leadingCoeffY_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] +theorem leadingCoeffY_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (f : CBivariate R) : (leadingCoeffY (R := R) f).toPoly = (toPoly f).leadingCoeff := by - have h_leadingCoeffY : (f.val.leadingCoeff).toPoly = (toPoly f).coeff (f.val.natDegree) := by - rw [ CBivariate.toPoly_coeff ] - congr - convert CompPoly.CPolynomial.leadingCoeff_eq_coeff_natDegree f - exact instDecidableEqOfLawfulBEq - convert h_leadingCoeffY - rw [ Polynomial.leadingCoeff, Polynomial.natDegree ] - by_cases h : f.toPoly = 0 <;> simp_all +decide [ Polynomial.degree_eq_natDegree ] - rw [ CompPoly.CBivariate.natDegreeY_toPoly ] - rfl + classical + have h_leadingCoeffY : f.leadingCoeff.toPoly = (toPoly f).coeff f.natDegree := by + rw [CBivariate.toPoly_coeff] + exact + congrArg CPolynomial.toPoly + (CompPoly.CPolynomial.leadingCoeff_eq_coeff_natDegree (p := f)) + rw [← Polynomial.coeff_natDegree, CompPoly.CBivariate.natDegreeY_toPoly] + simpa [CBivariate.leadingCoeffY, CBivariate.natDegreeY] using h_leadingCoeffY /-- `swap` exchanges X- and Y-exponents. -/ -theorem swap_toPoly_coeff {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] +theorem swap_toPoly_coeff {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] (f : CBivariate R) (i j : ℕ) : ((toPoly (swap (R := R) f)).coeff j).coeff i = ((toPoly f).coeff i).coeff j := by rw [coeff_toPoly, coeff_toPoly] @@ -775,7 +776,7 @@ theorem swap_toPoly_coeff {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring /-- `leadingCoeffX` is the Y-leading coefficient of the swapped polynomial. -/ -theorem leadingCoeffX_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] +theorem leadingCoeffX_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] (f : CBivariate R) : (leadingCoeffX (R := R) f).toPoly = (toPoly (swap (R := R) f)).leadingCoeff := by simpa [ CBivariate.leadingCoeffX ] using diff --git a/CompPoly/Multilinear/Basic.lean b/CompPoly/Multilinear/Basic.lean index 33fc2a88..b605874a 100644 --- a/CompPoly/Multilinear/Basic.lean +++ b/CompPoly/Multilinear/Basic.lean @@ -141,8 +141,8 @@ end CMlPolynomialInstances section CMlPolynomialMonomialBasisAndEvaluations -variable [CommRing R] -variable {S : Type*} [CommRing S] +variable [CommSemiring R] +variable {S : Type*} [CommSemiring S] /- Monomial-basis evaluations at point `w`. @@ -167,10 +167,9 @@ theorem monomialBasis_getElem {w : Vector R n} (i : Fin (2 ^ n)) : rw [monomialBasis] simp only [BitVec.getLsb_eq_getElem, Fin.getElem_fin, BitVec.getElem_ofFin, Vector.getElem_ofFn] -variable {S : Type*} [CommRing S] - -def map (f : R →+* S) (p : CMlPolynomial R n) : CMlPolynomial S n := - Vector.map (fun a => f a) p +def map {R S : Type*} [Semiring R] [Semiring S] (f : R →+* S) + (p : CMlPolynomial R n) : CMlPolynomial S n := + Vector.map f p /-- Evaluate a `CMlPolynomial` at a point -/ def eval (p : CMlPolynomial R n) (x : Vector R n) : R := @@ -304,10 +303,9 @@ theorem lagrangeBasis_getElem {w : Vector R n} (i : Fin (2 ^ n)) : rw [lagrangeBasis] simp only [BitVec.getLsb_eq_getElem, Fin.getElem_fin, BitVec.getElem_ofFin, Vector.getElem_ofFn] -variable {S : Type*} [CommRing S] - /-- Map a ring homomorphism over a `CMlPolynomialEval` -/ -def map (f : R →+* S) (p : CMlPolynomialEval R n) : CMlPolynomialEval S n := +def map {R S : Type*} [Semiring R] [Semiring S] + (f : R →+* S) (p : CMlPolynomialEval R n) : CMlPolynomialEval S n := Vector.map (fun a => f a) p /-- Evaluate a `CMlPolynomialEval` at a point -/ diff --git a/CompPoly/Multilinear/Equiv.lean b/CompPoly/Multilinear/Equiv.lean index 5697d235..8921472f 100644 --- a/CompPoly/Multilinear/Equiv.lean +++ b/CompPoly/Multilinear/Equiv.lean @@ -16,7 +16,7 @@ import CompPoly.Multilinear.Basic -/ open MvPolynomial -variable {R : Type*} [CommRing R] {n : ℕ} +variable {R : Type*} [CommSemiring R] {n : ℕ} noncomputable section diff --git a/CompPoly/Multivariate/CMvPolynomial.lean b/CompPoly/Multivariate/CMvPolynomial.lean index 4f3fae3f..a412497e 100644 --- a/CompPoly/Multivariate/CMvPolynomial.lean +++ b/CompPoly/Multivariate/CMvPolynomial.lean @@ -50,7 +50,8 @@ def C {n : ℕ} {R : Type} [BEq R] [LawfulBEq R] [Zero R] (c : R) : CMvPolynomia Lawful.C (n := n) (R := R) c /-- Construct the polynomial $X_i$. -/ -def X {n : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] (i : Fin n) : CMvPolynomial n R := +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) Lawful.fromUnlawful <| .ofList [(monomial, (1 : R))] @@ -138,7 +139,7 @@ def support {R : Type} {n : ℕ} [Zero R] (p : CMvPolynomial n R) : Finset (Fin (Lawful.monomials p).map CMvMonomial.toFinsupp |>.toFinset /-- The total degree of a polynomial (maximum total degree of its monomials). -/ -def totalDegree {R : Type} {n : ℕ} [inst : CommSemiring R] : CMvPolynomial n R → ℕ := +def totalDegree {R : Type} {n : ℕ} [Zero R] : CMvPolynomial n R → ℕ := fun p => Finset.sup (List.toFinset (List.map CMvMonomial.toFinsupp (Lawful.monomials p))) (fun s => Finsupp.sum s (fun _ e => e)) diff --git a/CompPoly/Multivariate/Lawful.lean b/CompPoly/Multivariate/Lawful.lean index 65def2ee..0b42ba7d 100644 --- a/CompPoly/Multivariate/Lawful.lean +++ b/CompPoly/Multivariate/Lawful.lean @@ -191,19 +191,19 @@ lemma fromUnlawful_cast {p : Lawful n R} : fromUnlawful p.1 = p := by section -variable [BEq R] [LawfulBEq R] [CommRing R] +variable [BEq R] [LawfulBEq R] /-- Negation of a polynomial. -/ -def neg (p : Lawful n R) : Lawful n R := +def neg [Neg R] (p : Lawful n R) : Lawful n R := fromUnlawful p.1.neg -instance : Neg (Lawful n R) := ⟨neg⟩ +instance [Neg R] : Neg (Lawful n R) := ⟨neg⟩ /-- Subtraction of polynomials. -/ -def sub (p₁ p₂ : Lawful n R) : Lawful n R := +def sub [Add R] [Neg R] (p₁ p₂ : Lawful n R) : Lawful n R := p₁ + (-p₂) -instance : Sub (Lawful n R) := ⟨sub⟩ +instance [Add R] [Neg R] : Sub (Lawful n R) := ⟨sub⟩ instance instDecidableEq [DecidableEq R] : DecidableEq (Lawful n R) := fun x y ↦ if h : x.1.toList = y.1.toList @@ -238,26 +238,31 @@ def liftPoly Lawful (n₁ ⊔ n₂) R) (p₁ : Lawful n₁ R) (p₂ : Lawful n₂ R) : Lawful (n₁ ⊔ n₂) R := Function.uncurry f (align p₁ p₂) -section -variable [CommRing R] +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⟩ -instance : HAdd (Lawful n₁ R) (Lawful n₂ R) (Lawful (n₁ ⊔ n₂) R) := +section + +-- Mixed-arity fallbacks: keep these low-priority so same-arity `Add`/`Sub`/`Mul`/`NatPow` +-- instances win when both operands already live in `Lawful n R`. +instance (priority := low) [Add R] : + HAdd (Lawful n₁ R) (Lawful n₂ R) (Lawful (n₁ ⊔ n₂) R) := ⟨fun p₁ p₂ ↦ liftPoly (·+·) p₁ p₂⟩ -instance : HSub (Lawful n₁ R) (Lawful n₂ R) (Lawful (n₁ ⊔ n₂) R) := +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 : HMul (Lawful n₁ R) (Lawful n₂ R) (Lawful (n₁ ⊔ n₂) R) := +instance (priority := low) [Add R] [Mul R] : + HMul (Lawful n₁ R) (Lawful n₂ R) (Lawful (n₁ ⊔ n₂) R) := ⟨fun p₁ p₂ ↦ liftPoly (·*·) p₁ p₂⟩ -instance : HPow (Lawful n R) ℕ (Lawful n R) := +instance (priority := low) [NatCast R] [Add R] [Mul R] : + HPow (Lawful n R) ℕ (Lawful n R) := ⟨fun p₁ exp ↦ exp.iterate p₁.mul 1⟩ -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⟩ - end end diff --git a/CompPoly/Multivariate/MvPolyEquiv/Instances.lean b/CompPoly/Multivariate/MvPolyEquiv/Instances.lean index 88eb9fa5..3c234441 100644 --- a/CompPoly/Multivariate/MvPolyEquiv/Instances.lean +++ b/CompPoly/Multivariate/MvPolyEquiv/Instances.lean @@ -334,7 +334,8 @@ lemma map_neg (a : CMvPolynomial n R) : lemma map_sub (a b : CMvPolynomial n R) : fromCMvPolynomial (Sub.sub a b) = fromCMvPolynomial a - fromCMvPolynomial b := by - unfold Sub.sub Lawful.instSub Lawful.sub + 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 diff --git a/CompPoly/Multivariate/Operations.lean b/CompPoly/Multivariate/Operations.lean index a5676252..e3c0b5a5 100644 --- a/CompPoly/Multivariate/Operations.lean +++ b/CompPoly/Multivariate/Operations.lean @@ -204,7 +204,7 @@ lemma bind₁_eq_aeval {n m : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBE Given `f : Fin n → Fin m`, renames variable `X i` to `X (f i)`. -/ -def rename {n m : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] +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)) @@ -213,7 +213,7 @@ def rename {n m : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] -- `renameEquiv` is defined in `CompPoly.Multivariate.Rename` /-- Iterative reconstruction of a polynomial by folding over terms. -/ -def sumToIter {n : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] +def sumToIter {n : ℕ} {R : Type} [Zero R] [Add R] [BEq R] [LawfulBEq R] (p : CMvPolynomial n R) : CMvPolynomial n R := ExtTreeMap.foldl (fun acc m c => acc + monomial m c) 0 p.1 diff --git a/CompPoly/Univariate/Basic.lean b/CompPoly/Univariate/Basic.lean index a5937310..440ecb6a 100644 --- a/CompPoly/Univariate/Basic.lean +++ b/CompPoly/Univariate/Basic.lean @@ -12,8 +12,9 @@ import CompPoly.Univariate.Raw.Division /-! # Computable Univariate Polynomials - This file defines `CPolynomial R`, the type of canonical (trimmed) univariate polynomials. - A polynomial is canonical if it has no trailing zeros, i.e., `p.trim = p`. + This file defines `CPolynomial R`, the type of canonical univariate polynomials. + Canonicality is tracked semantically by requiring the last stored coefficient, when present, + to be nonzero. This provides a unique representation for each polynomial, enabling stronger extensionality properties compared to the raw `CPolynomial.Raw` type. @@ -22,36 +23,41 @@ namespace CompPoly open CPolynomial.Raw -variable {R : Type*} [BEq R] +variable {R : Type*} /-- Computable univariate polynomials are represented canonically with no trailing zeros. - A polynomial `p : CPolynomial.Raw R` is canonical if `p.trim = p`, meaning the last coefficient - is non-zero (or the polynomial is empty). This provides a unique representative for each - polynomial equivalence class. + A polynomial `p : CPolynomial.Raw R` is canonical if its last stored coefficient is nonzero + whenever the underlying array is nonempty. This gives an instance-stable carrier while keeping + the raw normalization algorithms available separately. TODO optimizations may be had by trimming only at the end of iterative operations -/ -def CPolynomial (R : Type*) [BEq R] [Semiring R] := { p : CPolynomial.Raw R // p.trim = p } +def CPolynomial (R : Type*) [Zero R] := { p : CPolynomial.Raw R // CPolynomial.Raw.IsCanonical p } namespace CPolynomial +section ZeroOnly + /-- Extensionality for canonical polynomials. -/ -@[ext] theorem ext [Semiring R] {p q : CPolynomial R} (h : p.val = q.val) : p = q := by +@[ext] theorem ext [Zero R] {p q : CPolynomial R} (h : p.val = q.val) : p = q := by exact Subtype.ext h /-- Canonical polynomials coerce to raw polynomials. -/ -instance [Semiring R] : Coe (CPolynomial R) (CPolynomial.Raw R) where coe := Subtype.val +instance [Zero R] : Coe (CPolynomial R) (CPolynomial.Raw R) where coe := Subtype.val + +/-- The zero polynomial is canonical without any normalization assumptions. -/ +instance [Zero R] : Zero (CPolynomial R) := ⟨⟨#[], Trim.isCanonical_empty⟩⟩ -/-- The zero polynomial is canonical. -/ -instance [Semiring R] : Inhabited (CPolynomial R) := ⟨#[], Trim.canonical_empty⟩ +/-- The zero polynomial provides the inhabited instance. -/ +instance [Zero R] : Inhabited (CPolynomial R) := ⟨0⟩ /-- `CPolynomial R` has `BEq` when `R` does, comparing the underlying coefficient arrays. -/ -instance (R : Type*) [BEq R] [Semiring R] : BEq (CPolynomial R) where +instance (R : Type*) [Zero R] [BEq R] : BEq (CPolynomial R) where beq p q := p.val == q.val /-- `CPolynomial R` has `LawfulBEq` when `R` does: `p == q` iff `p = q`. -/ -instance (R : Type*) [BEq R] [LawfulBEq R] [Semiring R] : LawfulBEq (CPolynomial R) where +instance (R : Type*) [Zero R] [BEq R] [LawfulBEq R] : LawfulBEq (CPolynomial R) where rfl := by have h_raw : ∀ (a : CPolynomial.Raw R), a == a ↔ a = a := by aesop @@ -62,45 +68,59 @@ instance (R : Type*) [BEq R] [LawfulBEq R] [Semiring R] : LawfulBEq (CPolynomial eq_of_beq h := Subtype.ext (LawfulBEq.eq_of_beq h) /-- `CPolynomial R` has `DecidableEq` when `R` does, via the underlying `Array R` representation. -/ -instance (R : Type*) [BEq R] [DecidableEq R] [Semiring R] : DecidableEq (CPolynomial R) := - @Subtype.instDecidableEq (CPolynomial.Raw R) (fun p => p.trim = p) inferInstance +instance (R : Type*) [Zero R] [DecidableEq R] : DecidableEq (CPolynomial R) := + @Subtype.instDecidableEq + (CPolynomial.Raw R) + (fun p => CPolynomial.Raw.IsCanonical p) + inferInstance + +end ZeroOnly section Operations -variable [Semiring R] [LawfulBEq R] -variable (p q r : CPolynomial R) +/-- Canonical computable polynomials are trim-stable. -/ +@[simp] theorem trim_eq [Zero R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : p.val.trim = p.val := + Trim.trim_eq_of_isCanonical p.property /-- Addition of canonical polynomials (result is canonical). -/ -instance : Add (CPolynomial R) where - add p q := ⟨p.val + q.val, by apply Trim.trim_twice⟩ - -theorem add_comm : p + q = q + p := by - apply CPolynomial.ext; apply Raw.add_comm +instance [Semiring R] [BEq R] [LawfulBEq R] : Add (CPolynomial R) where + add p q := ⟨p.val + q.val, + Trim.isCanonical_of_trim_eq (by + simpa [Raw.add] using Trim.trim_twice (Raw.addRaw p.val q.val))⟩ -theorem add_assoc : p + q + r = p + (q + r) := by - apply CPolynomial.ext; apply Raw.add_assoc +theorem add_comm [Semiring R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) : p + q = q + p := by + apply CPolynomial.ext + simpa using (Raw.add_comm p.val q.val) -instance : Zero (CPolynomial R) := ⟨0, zero_canonical⟩ +theorem add_assoc [Semiring R] [BEq R] [LawfulBEq R] + (p q r : CPolynomial R) : p + q + r = p + (q + r) := by + apply CPolynomial.ext + simpa using (Raw.add_assoc p.val q.val r.val) -theorem zero_add : 0 + p = p := by +theorem zero_add [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : 0 + p = p := by apply CPolynomial.ext - apply Raw.zero_add p.val p.prop + simpa using (Raw.zero_add p.val (trim_eq p)) -theorem add_zero : p + 0 = p := by +theorem add_zero [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : p + 0 = p := by apply CPolynomial.ext - apply Raw.add_zero p.val p.prop + simpa using (Raw.add_zero p.val (trim_eq p)) /-- Scalar multiplication by a natural number (result is canonical). -/ -def nsmul (n : ℕ) (p : CPolynomial R) : CPolynomial R := - ⟨Raw.nsmul n p.val, by apply Trim.trim_twice⟩ +def nsmul [Semiring R] [BEq R] [LawfulBEq R] (n : ℕ) (p : CPolynomial R) : CPolynomial R := + ⟨Raw.nsmul n p.val, + Trim.isCanonical_of_trim_eq (by + simpa [Raw.nsmul] using Trim.trim_twice (Raw.nsmulRaw n p.val))⟩ -theorem nsmul_zero : nsmul 0 p = 0 := by - apply CPolynomial.ext; apply Raw.nsmul_zero +theorem nsmul_zero [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : nsmul 0 p = 0 := by + apply CPolynomial.ext + simpa using (Raw.nsmul_zero p.val) -theorem nsmul_succ (n : ℕ) (p : CPolynomial R) : nsmul (n + 1) p = nsmul n p + p := by - apply CPolynomial.ext; apply Raw.nsmul_succ +theorem nsmul_succ [Semiring R] [BEq R] [LawfulBEq R] + (n : ℕ) (p : CPolynomial R) : nsmul (n + 1) p = nsmul n p + p := by + apply CPolynomial.ext + simpa using (Raw.nsmul_succ n (p := p.val)) -instance [LawfulBEq R] : AddCommSemigroup (CPolynomial R) where +instance [Semiring R] [BEq R] [LawfulBEq R] : AddCommSemigroup (CPolynomial R) where add_assoc := add_assoc add_comm := add_comm @@ -109,11 +129,12 @@ instance [LawfulBEq R] : AddCommSemigroup (CPolynomial R) where The product of two canonical polynomials is canonical because multiplication preserves the "no trailing zeros" property. -/ -instance : Mul (CPolynomial R) where +instance [Semiring R] [BEq R] [LawfulBEq R] : Mul (CPolynomial R) where mul p q := - ⟨p.val * q.val, by exact mul_is_trimmed p.val q.val⟩ + ⟨p.val * q.val, Trim.isCanonical_of_trim_eq (mul_is_trimmed p.val q.val)⟩ -lemma one_is_trimmed [Nontrivial R] : (1 : CPolynomial.Raw R).trim = 1 := +lemma one_is_trimmed [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] : + (1 : CPolynomial.Raw R).trim = 1 := Trim.push_trim #[] 1 one_ne_zero /-- The constant polynomial 1 is canonical, and is the Unit for multiplication. @@ -122,10 +143,10 @@ lemma one_is_trimmed [Nontrivial R] : (1 : CPolynomial.Raw R).trim = 1 := This proof does not work without the assumption that R is non-trivial. -/ -instance [Nontrivial R] : One (CPolynomial R) where - one := ⟨Raw.C 1, by exact one_is_trimmed⟩ +instance [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] : One (CPolynomial R) where + one := ⟨Raw.C 1, Trim.isCanonical_of_trim_eq one_is_trimmed⟩ -instance [Nontrivial R] : Nontrivial (CPolynomial R) where +instance [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] : Nontrivial (CPolynomial R) where exists_pair_ne := ⟨0, 1, by intro h have := congr_arg (fun p : CPolynomial R => p.val.size) h @@ -134,13 +155,15 @@ instance [Nontrivial R] : Nontrivial (CPolynomial R) where /-- The coefficient of `X^i` in the polynomial. Returns `0` if `i` is out of bounds. -/ @[reducible] -def coeff (p : CPolynomial R) (i : ℕ) : R := p.val.coeff i +def coeff [Zero R] (p : CPolynomial R) (i : ℕ) : R := p.val.coeff i /-- The constant polynomial `C r`. -/ -def C (r : R) : CPolynomial R := ⟨(Raw.C r).trim, by rw [Trim.trim_twice]⟩ +def C [Zero R] [BEq R] [LawfulBEq R] (r : R) : CPolynomial R := + ⟨(Raw.C r).trim, Trim.isCanonical_trim (Raw.C r)⟩ /-- The variable `X`. -/ -def X [Nontrivial R] : CPolynomial R := ⟨Raw.X, X_canonical⟩ +def X [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] : CPolynomial R := + ⟨Raw.X, Trim.isCanonical_of_trim_eq X_canonical⟩ /-- Construct a canonical monomial `c * X^n` as a `CPolynomial R`. @@ -149,97 +172,113 @@ def X [Nontrivial R] : CPolynomial R := ⟨Raw.X, X_canonical⟩ Note: If `c = 0`, this returns `0` (the zero polynomial). -/ -def monomial [DecidableEq R] (n : ℕ) (c : R) : CPolynomial R := - ⟨Raw.monomial n c, Raw.monomial_canonical n c⟩ +def monomial [Semiring R] [BEq R] [LawfulBEq R] [DecidableEq R] + (n : ℕ) (c : R) : CPolynomial R := + ⟨Raw.monomial n c, Trim.isCanonical_of_trim_eq (Raw.monomial_canonical n c)⟩ /-- Return the degree of a `CPolynomial`. -/ -def degree (p : CPolynomial R) : WithBot ℕ := p.val.degree +def degree [Zero R] (p : CPolynomial R) : WithBot ℕ := + match p.val.size with + | 0 => ⊥ + | .succ n => n /-- Natural number degree of a canonical polynomial. Returns the degree as a natural number. For the zero polynomial, returns `0`. This matches Mathlib's `Polynomial.natDegree` API. -/ -def natDegree (p : CPolynomial R) : ℕ := p.val.natDegree +def natDegree [Zero R] (p : CPolynomial R) : ℕ := + match p.val.size with + | 0 => 0 + | .succ n => n /-- Return the leading coefficient of a `CPolynomial` as the last coefficient of the trimmed array, or `0` if the trimmed array is empty. -/ -def leadingCoeff (p : CPolynomial R) : R := p.val.leadingCoeff +def leadingCoeff [Zero R] (p : CPolynomial R) : R := p.val.getLastD 0 /-- Evaluate a polynomial at a point. -/ -def eval (x : R) (p : CPolynomial R) : R := p.val.eval x +def eval [Semiring R] (x : R) (p : CPolynomial R) : R := + p.val.zipIdx.foldl (fun acc ⟨a, i⟩ => acc + a * x ^ i) 0 /-- Evaluate at `x : S` via a ring hom `f : R →+* S`; `eval₂ f x p = f(a₀) + f(a₁)*x + f(a₂)*x² + ...`. -/ -def eval₂ {S : Type*} [Semiring S] (f : R →+* S) (x : S) (p : CPolynomial R) : S := p.val.eval₂ f x +def eval₂ {S : Type*} [Semiring R] [Semiring S] + (f : R →+* S) (x : S) (p : CPolynomial R) : S := + p.val.zipIdx.foldl (fun acc ⟨a, i⟩ => acc + f a * x ^ i) 0 /-- The support of a polynomial: indices with nonzero coefficients. -/ -def support (p : CPolynomial R) : Finset ℕ := +def support [Zero R] [BEq R] (p : CPolynomial R) : Finset ℕ := (Finset.range p.val.size).filter (fun i => p.val.coeff i != 0) /-- Number of coefficients (length of the underlying array). -/ -def size (p : CPolynomial R) : ℕ := p.val.size +def size [Zero R] (p : CPolynomial R) : ℕ := p.val.size /-- Upper bound on degree: `size - 1` if non-empty, `⊥` if empty. -/ -def degreeBound (p : CPolynomial R) : WithBot Nat := p.val.degreeBound +def degreeBound [Zero R] (p : CPolynomial R) : WithBot Nat := p.degree /-- Convert `degreeBound` to a natural number by sending `⊥` to `0`. -/ -def natDegreeBound (p : CPolynomial R) : Nat := p.val.natDegreeBound +def natDegreeBound [Zero R] (p : CPolynomial R) : Nat := p.natDegree /-- Check if a `CPolynomial` is monic, i.e. its leading coefficient is 1. -/ -def monic (p : CPolynomial R) : Bool := p.val.monic +def monic [Zero R] [One R] [BEq R] (p : CPolynomial R) : Bool := p.leadingCoeff == 1 /-- The polynomial with the constant term removed; `coeff (divX p) i = coeff p (i + 1)`. -/ -def divX (p : CPolynomial R) : CPolynomial R := - ⟨(Raw.divX p.val).trim, by - simpa using (Trim.trim_twice (p.val.extract 1 p.val.size))⟩ +def divX [Zero R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : CPolynomial R := + let q : CPolynomial.Raw R := p.val.extract 1 p.val.size + ⟨q.trim, Trim.isCanonical_trim q⟩ /-- Coefficient of the constant polynomial `C r`. -/ -lemma coeff_C (r : R) (i : ℕ) : coeff (C r) i = if i = 0 then r else 0 := by - unfold C; simp only [coeff] - rw [Trim.coeff_eq_coeff, Raw.coeff_C] +lemma coeff_C [Zero R] [BEq R] [LawfulBEq R] (r : R) (i : ℕ) : + coeff (C r) i = if i = 0 then r else 0 := by + unfold coeff C + rw [Trim.coeff_eq_coeff] + unfold Raw.C Raw.coeff + split_ifs with h <;> simp [h] -omit [BEq R] [Semiring R] [LawfulBEq R] in /-- Coefficient of the variable `X`. -/ -lemma coeff_X [Nontrivial R] (i : ℕ) : coeff X i = if i = 1 then 1 else 0 := by - simp only [X, coeff]; rw [Raw.coeff_X] +lemma coeff_X [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (i : ℕ) : + coeff X i = if i = 1 then 1 else 0 := by + unfold coeff X Raw.X Raw.coeff + rcases i with (_ | _ | i) <;> rfl -omit [LawfulBEq R] in /-- Coefficient of the zero polynomial. -/ @[simp] -lemma coeff_zero (i : ℕ) : coeff (0 : CPolynomial R) i = 0 := by - simp; rfl +lemma coeff_zero [Zero R] (i : ℕ) : coeff (0 : CPolynomial R) i = 0 := by + change (#[].getD i 0) = 0 + simp /-- Coefficient of the constant polynomial `1`. -/ -lemma coeff_one [Nontrivial R] (i : ℕ) : +lemma coeff_one [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (i : ℕ) : coeff (1 : CPolynomial R) i = if i = 0 then 1 else 0 := by - simp only [coeff] - change Raw.coeff 1 i = if i = 0 then 1 else 0 - rw [Raw.coeff_one] + simpa [coeff] using (Raw.coeff_one (R := R) i) /-- Coefficient of a sum. -/ -lemma coeff_add (p q : CPolynomial R) (i : ℕ) : coeff (p + q) i = coeff p i + coeff q i := by +lemma coeff_add [Semiring R] [BEq R] [LawfulBEq R] + (p q : CPolynomial R) (i : ℕ) : coeff (p + q) i = coeff p i + coeff q i := by unfold coeff; exact Raw.add_coeff_trimmed p.val q.val i /-- Coefficient of a monomial. -/ -lemma coeff_monomial [DecidableEq R] (n i : ℕ) (c : R) : +lemma coeff_monomial [Semiring R] [BEq R] [LawfulBEq R] [DecidableEq R] + (n i : ℕ) (c : R) : coeff (monomial n c) i = if i = n then c else 0 := by unfold coeff monomial; rw [Raw.coeff_monomial]; simp only [eq_comm] /-- Coefficient of a product (convolution sum). -/ -lemma coeff_mul (p q : CPolynomial R) (k : ℕ) : +lemma coeff_mul [Semiring R] [BEq R] [LawfulBEq R] + (p q : CPolynomial R) (k : ℕ) : coeff (p * q) k = (Finset.range (k + 1)).sum (fun i => coeff p i * coeff q (k - i)) := by unfold coeff; exact Raw.mul_coeff p.val q.val k /-- Two polynomials are equal iff they have the same coefficients. -/ -theorem eq_iff_coeff {p q : CPolynomial R} : +theorem eq_iff_coeff [Zero R] [BEq R] [LawfulBEq R] {p q : CPolynomial R} : p = q ↔ ∀ i, coeff p i = coeff q i := by constructor · intro h i; rw [h] - · intro h; apply ext; exact Trim.canonical_ext p.prop q.prop (fun i => h i) + · intro h; apply ext; exact Trim.isCanonical_ext p.property q.property (fun i => h i) /-- Monomials are additive in their coefficient. -/ -theorem monomial_add [DecidableEq R] (n : ℕ) (a b : R) : +theorem monomial_add [Semiring R] [BEq R] [LawfulBEq R] [DecidableEq R] + (n : ℕ) (a b : R) : monomial n (a + b) = monomial n a + monomial n b := by apply (eq_iff_coeff).2 intro i @@ -247,11 +286,13 @@ theorem monomial_add [DecidableEq R] (n : ℕ) (a b : R) : split_ifs <;> simp_all /-- Zero characterization: `p = 0` iff all coefficients are zero. -/ -theorem eq_zero_iff_coeff_zero {p : CPolynomial R} : p = 0 ↔ ∀ i, coeff p i = 0 := by +theorem eq_zero_iff_coeff_zero [Zero R] [BEq R] [LawfulBEq R] {p : CPolynomial R} : + p = 0 ↔ ∀ i, coeff p i = 0 := by rw [eq_iff_coeff]; simp only [coeff_zero] /-- An index is in the support iff the coefficient there is nonzero. -/ -lemma mem_support_iff (p : CPolynomial R) (i : ℕ) : i ∈ p.support ↔ coeff p i ≠ 0 := by +lemma mem_support_iff [Zero R] [BEq R] [LawfulBEq R] (p : CPolynomial R) (i : ℕ) : + i ∈ p.support ↔ coeff p i ≠ 0 := by unfold support coeff rw [Finset.mem_filter] constructor @@ -265,19 +306,19 @@ lemma mem_support_iff (p : CPolynomial R) (i : ℕ) : i ∈ p.support ↔ coeff · exact bne_iff_ne.mpr h /-- The support is empty iff the polynomial is zero. -/ -theorem support_empty_iff (p : CPolynomial R) : p.support = ∅ ↔ p = 0 := by +theorem support_empty_iff [Zero R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : + p.support = ∅ ↔ p = 0 := by rw [eq_zero_iff_coeff_zero, Finset.eq_empty_iff_forall_notMem] constructor · intro h i; by_contra hne; exact h i ((mem_support_iff p i).mpr hne) · intro h i; rw [mem_support_iff, h]; simp /-- Evaluation equals the sum over support of coefficients times powers. -/ -theorem eval_eq_sum_support (p : CPolynomial R) (x : R) : +theorem eval_eq_sum_support [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) (x : R) : p.eval x = p.support.sum (fun i => p.coeff i * x ^ i) := by - have h_eval_def : p.val.eval x = + have h_eval_def : p.eval x = (p.val.zipIdx.toList.map (fun ⟨a, i⟩ => a * x ^ i)).sum := by - unfold CPolynomial.Raw.eval - unfold CPolynomial.Raw.eval₂ + unfold CPolynomial.eval simp +decide induction p.val simp +decide [ * ] @@ -297,22 +338,30 @@ theorem eval_eq_sum_support (p : CPolynomial R) (x : R) : /-- Evaluation via a ring hom equals the sum over support of mapped coefficients times powers. -/ -theorem eval₂_eq_sum_support {S : Type*} [Semiring S] +theorem eval₂_eq_sum_support {S : Type*} [Semiring R] [BEq R] [LawfulBEq R] [Semiring S] (f : R →+* S) (p : CPolynomial R) (x : S) : p.eval₂ f x = p.support.sum (fun i => f (p.coeff i) * x ^ i) := by - unfold CPolynomial.support - convert CPolynomial.Raw.sum_zipIdx_eq_sum_range p.val _ using 1 - rotate_right - use fun a i => if a != 0 then f a * x ^ i else 0 - all_goals try infer_instance - · unfold CPolynomial.eval₂ - unfold CPolynomial.Raw.eval₂ - induction' (Array.zipIdx p.val) with a ha ih - simp +decide [ * ] - induction a using List.reverseRecOn <;> aesop - · rw [ Finset.sum_filter ] + have h_eval_def : p.eval₂ f x = + (p.val.zipIdx.toList.map (fun ⟨a, i⟩ => f a * x ^ i)).sum := by + unfold CPolynomial.eval₂ + simp +decide + induction p.val + simp +decide [*] + induction' ‹List R› using List.reverseRecOn with a l ih <;> + simp +decide [*, List.zipIdx_append] + have h_sum_range : (p.val.zipIdx.toList.map (fun ⟨a, i⟩ => f a * x ^ i)).sum = + (Finset.range p.val.size).sum (fun i => f (p.val.coeff i) * x ^ i) := by + convert CPolynomial.Raw.sum_zipIdx_eq_sum_range p.val (fun a i => f a * x ^ i) + using 1 + convert h_eval_def.trans h_sum_range using 1 + refine' Finset.sum_subset _ _ <;> intro i hi <;> + simp_all +decide [CPolynomial.Raw.coeff] + · exact Finset.mem_range.mp (Finset.mem_filter.mp hi |>.1) + · unfold CPolynomial.support + aesop -lemma coeff_C_mul [Nontrivial R] (p : CPolynomial R) (c : R) : +lemma coeff_C_mul [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] + (p : CPolynomial R) (c : R) : ∀ i, coeff ((C c) * p) i = c * (coeff p i) := by intros i rw [coeff_mul, Finset.sum_eq_single 0] @@ -322,7 +371,8 @@ lemma coeff_C_mul [Nontrivial R] (p : CPolynomial R) (c : R) : · simp /-- Lemmas on coefficients and multiplication by `X`. -/ -lemma coeff_X_mul_succ [Nontrivial R] (p : CPolynomial R) (n : ℕ) : +lemma coeff_X_mul_succ [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] + (p : CPolynomial R) (n : ℕ) : coeff (X * p) (n + 1) = coeff p n := by unfold coeff change ((X.val * p.val).coeff (n + 1) = p.val.coeff n) @@ -341,14 +391,16 @@ lemma coeff_X_mul_succ [Nontrivial R] (p : CPolynomial R) (n : ℕ) : rw [hn, Raw.coeff_X (R := R) 1] simp -lemma coeff_X_mul_zero [Nontrivial R] (p : CPolynomial R) : coeff (X * p) 0 = 0 := by +lemma coeff_X_mul_zero [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] + (p : CPolynomial R) : coeff (X * p) 0 = 0 := by unfold coeff change ((Raw.X * p.val) : Raw R).coeff 0 = 0 rw [Raw.mul_coeff] -- (Finset.range 1).sum ... reduces to the single term at 0 simp [Raw.X] -theorem coeff_mul_X_succ [Nontrivial R] (p : CPolynomial R) (n : ℕ) : +theorem coeff_mul_X_succ [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] + (p : CPolynomial R) (n : ℕ) : coeff (p * X) (n + 1) = coeff p n := by unfold coeff change ((p.val * X.val).coeff (n + 1) = p.val.coeff n) @@ -374,12 +426,12 @@ theorem coeff_mul_X_succ [Nontrivial R] (p : CPolynomial R) (n : ℕ) : rw [hn, Raw.coeff_X (R := R) 1] simp -theorem coeff_mul_X_zero [Nontrivial R] (p : CPolynomial R) : coeff (p * X) 0 = 0 := by +theorem coeff_mul_X_zero [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] + (p : CPolynomial R) : coeff (p * X) 0 = 0 := by rw [coeff_mul] simp [X, Raw.X] -omit [BEq R] [LawfulBEq R] in -lemma coeff_extract_succ (a : CPolynomial.Raw R) (i : ℕ) : +lemma coeff_extract_succ [Zero R] (a : CPolynomial.Raw R) (i : ℕ) : Raw.coeff (a.extract 1 a.size) i = Raw.coeff a (i + 1) := by simp [Raw.coeff, Array.getElem?_extract] by_cases h : i < a.size - 1 @@ -388,7 +440,8 @@ lemma coeff_extract_succ (a : CPolynomial.Raw R) (i : ℕ) : · have hge : a.size ≤ i + 1 := by omega simp [h, Array.getElem?_eq_none (xs := a) (i := i + 1) hge] -lemma coeff_divX (p : CPolynomial R) (i : ℕ) : coeff (divX p) i = coeff p (i + 1) := by +lemma coeff_divX [Zero R] [BEq R] [LawfulBEq R] (p : CPolynomial R) (i : ℕ) : + coeff (divX p) i = coeff p (i + 1) := by -- LHS: coeff of divX = coeff of trimmed extract unfold divX -- turn coefficients of CPolynomial into raw coefficients @@ -400,10 +453,11 @@ lemma coeff_divX (p : CPolynomial R) (i : ℕ) : coeff (divX p) i = coeff p (i + -- shift the extract exact htrim.trans (coeff_extract_succ (a := (↑p : CPolynomial.Raw R)) (i := i)) -lemma X_mul_divX_add [Nontrivial R] (p : CPolynomial R) : p = X * divX p + C (coeff p 0) := by +lemma X_mul_divX_add [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] + (p : CPolynomial R) : p = X * divX p + C (coeff p 0) := by apply CPolynomial.ext rw [add_comm] - refine Trim.canonical_ext (p := p.val) + refine Trim.isCanonical_ext (p := p.val) (q := (C (coeff p 0) + X * divX p).val) ?_ ?_ ?_ · exact p.property · exact (C (coeff p 0) + X * divX p).property @@ -417,7 +471,7 @@ lemma X_mul_divX_add [Nontrivial R] (p : CPolynomial R) : p = X * divX p + C (co have hX0 : coeff (X * divX p) 0 = 0 := by simpa using (coeff_X_mul_zero (R := R) (p := divX p)) rw [hC0, hX0] - simp only [_root_.add_zero] + rw [_root_.add_zero] | succ n => rw [coeff_add (p := C (coeff p 0)) (q := X * divX p) (i := n + 1)] have hCsucc : coeff (C (coeff p 0)) (n + 1) = 0 := by @@ -428,9 +482,10 @@ lemma X_mul_divX_add [Nontrivial R] (p : CPolynomial R) : p = X * divX p + C (co have hdivX : coeff (divX p) n = coeff p (n + 1) := by simpa using (coeff_divX (p := p) (i := n)) rw [hCsucc, hXsucc, hdivX] - simp only [_root_.zero_add] + rw [_root_.zero_add] -theorem divX_mul_X_add [Nontrivial R] (p : CPolynomial R) : divX p * X + C (p.coeff 0) = p := by +theorem divX_mul_X_add [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] + (p : CPolynomial R) : divX p * X + C (p.coeff 0) = p := by classical rw [eq_iff_coeff] intro k @@ -447,10 +502,11 @@ theorem divX_mul_X_add [Nontrivial R] (p : CPolynomial R) : divX p * X + C (p.co have hne : n + 1 ≠ 0 := by exact Nat.succ_ne_zero n simp only [Array.getD_eq_getD_getElem?, Nat.add_eq_zero_iff, one_ne_zero, - and_false, ↓reduceIte, _root_.add_zero] + and_false, ↓reduceIte] + rw [_root_.add_zero] simpa using (coeff_divX (p := p) (i := n)) -lemma divX_size_lt (p : CPolynomial R) (hp : p.val.size > 0) : +lemma divX_size_lt [Zero R] [BEq R] [LawfulBEq R] (p : CPolynomial R) (hp : p.val.size > 0) : (divX p).val.size < p.val.size := by unfold divX have hle : (Raw.trim (p.val.extract 1 p.val.size)).size @@ -463,7 +519,8 @@ lemma divX_size_lt (p : CPolynomial R) (hp : p.val.size > 0) : exact lt_of_le_of_lt hle' (Nat.pred_lt_self hp) /-- Induction principle for polynomials (mirrors mathlib's `Polynomial.induction_on`). -/ -theorem induction_on [Nontrivial R] {P : CPolynomial R → Prop} (p : CPolynomial R) +theorem induction_on [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] + {P : CPolynomial R → Prop} (p : CPolynomial R) (h0 : P 0) (hC : ∀ a, P (C a)) (hadd : ∀ p q, P p → P q → P (p + q)) (hX : ∀ p, P p → P (X * p)) : P p := by -- Strong induction on the size of the underlying coefficient array @@ -494,17 +551,26 @@ theorem induction_on [Nontrivial R] {P : CPolynomial R → Prop} (p : CPolynomia rw [X_mul_divX_add (p := p), add_comm] exact hsum -omit [LawfulBEq R] in /- Auxiliary lemmas for `degree_eq_support_max`: relating `degree`, `support`, and `lastNonzero`. -/ /-- Lemma for `degree_eq_support_max`: degree in terms of `lastNonzero`. -/ -lemma degree_eq_support_max_aux_degree (p : CPolynomial R) {k : Fin p.val.size} +lemma degree_eq_support_max_aux_degree [Zero R] [BEq R] [LawfulBEq R] + (p : CPolynomial R) {k : Fin p.val.size} (hk : p.val.lastNonzero = some k) : p.degree = k.val := by - unfold CPolynomial.degree - unfold Raw.degree - simp [hk] - -omit [LawfulBEq R] in -lemma degree_eq_support_max_aux_lastNonzero (p : CPolynomial R) (hp : p ≠ 0) : + have hp : p.val.size > 0 := by + exact lt_of_lt_of_le (Nat.succ_pos _) (Nat.succ_le_of_lt k.is_lt) + have hlast : + p.val.lastNonzero = some ⟨p.val.size - 1, Nat.pred_lt_self hp⟩ := by + exact (Trim.canonical_nonempty_iff (p := p.val) hp).mp (trim_eq p) + have hkEq : k = ⟨p.val.size - 1, Nat.pred_lt_self hp⟩ := by + apply Option.some.inj + exact hk.symm.trans hlast + have hkVal : k.val = p.val.size - 1 := by + simpa using congrArg Fin.val hkEq + have hs : p.val.size = k.val + 1 := by omega + simp [CPolynomial.degree, hs] + +lemma degree_eq_support_max_aux_lastNonzero [Zero R] [BEq R] [LawfulBEq R] + (p : CPolynomial R) (hp : p ≠ 0) : ∃ k : Fin p.val.size, p.val.lastNonzero = some k := by cases hln : p.val.lastNonzero with | some k => @@ -514,22 +580,23 @@ lemma degree_eq_support_max_aux_lastNonzero (p : CPolynomial R) (hp : p ≠ 0) : simp [Raw.trim, hln] have hval : p.val = (#[] : CPolynomial.Raw R) := by have htrim' := htrim - rw [p.prop] at htrim' + rw [trim_eq p] at htrim' exact htrim' have hp0 : p = 0 := by apply Subtype.ext simpa using hval exact (hp hp0).elim -lemma degree_eq_support_max_aux_mem_support (p : CPolynomial R) {k : Fin p.val.size} +lemma degree_eq_support_max_aux_mem_support [Zero R] [BEq R] [LawfulBEq R] + (p : CPolynomial R) {k : Fin p.val.size} (hk : p.val.lastNonzero = some k) : k.val ∈ p.support := by unfold CPolynomial.support rcases k with ⟨k, hklt⟩ refine (Finset.mem_filter).2 ?_ refine ⟨?_, ?_⟩ · exact Finset.mem_range.2 hklt - · have hnonzeroFin : p.val[(⟨k, hklt⟩ : Fin p.val.size)] ≠ (0 : R) := - (Trim.lastNonzero_spec (p := p.val) (k := ⟨k, hklt⟩) hk).1 + · have hnonzeroFin : p.val[(⟨k, hklt⟩ : Fin p.val.size)] ≠ (0 : R) := by + simpa using (Trim.lastNonzero_spec (p := p.val) (k := ⟨k, hklt⟩) hk).1 have hnonzero : p.val[k]'hklt ≠ (0 : R) := by simpa using hnonzeroFin have hcoeff_ne : p.val.coeff k ≠ (0 : R) := by @@ -540,7 +607,8 @@ lemma degree_eq_support_max_aux_mem_support (p : CPolynomial R) {k : Fin p.val.s /-- Degree equals the maximum of the support when the polynomial is non-zero. Here `p.degree = some n` where `n` is the maximum index in `p.support`. -/ -theorem degree_eq_support_max (p : CPolynomial R) (hp : p ≠ 0) : +theorem degree_eq_support_max [Zero R] [BEq R] [LawfulBEq R] + (p : CPolynomial R) (hp : p ≠ 0) : ∃ n, n ∈ p.support ∧ p.degree = n := by obtain ⟨k, hk⟩ := degree_eq_support_max_aux_lastNonzero (p := p) hp refine ⟨k.val, ?_⟩ @@ -548,98 +616,102 @@ theorem degree_eq_support_max (p : CPolynomial R) (hp : p ≠ 0) : · exact degree_eq_support_max_aux_mem_support (p := p) hk · exact degree_eq_support_max_aux_degree (p := p) hk -omit [LawfulBEq R] in /-- When `p ≠ 0`, `degree p` equals `natDegree p` (as `WithBot ℕ`). -/ -theorem degree_eq_natDegree (p : CPolynomial R) (hp : p ≠ 0) : +theorem degree_eq_natDegree [Zero R] (p : CPolynomial R) (hp : p ≠ 0) : p.degree = p.natDegree := by - obtain ⟨k, hk⟩ := degree_eq_support_max_aux_lastNonzero (p := p) hp - rw [degree_eq_support_max_aux_degree (p := p) hk] - unfold natDegree Raw.natDegree - rw [hk] + cases hs : p.val.size with + | zero => + have hval : p.val = (#[] : CPolynomial.Raw R) := Array.eq_empty_of_size_eq_zero hs + apply (hp ?_).elim + apply CPolynomial.ext + simpa using hval + | succ n => + have hdeg : p.degree = n := by simp [CPolynomial.degree, hs] + have hnat : p.natDegree = n := by simp [CPolynomial.natDegree, hs] + rw [hdeg, hnat] -omit [LawfulBEq R] in /-- Lemma for computing the degree of 0 in proofs. -/ -lemma degree_zero : degree (0 : CPolynomial R) = ⊥ := by - unfold degree Raw.degree - have : (0 : CPolynomial.Raw R).lastNonzero = none := by - simp [Raw.lastNonzero] - apply Array.findIdxRev?_empty_none - rfl - show Raw.degree (0 : CPolynomial.Raw R) = ⊥ - rw [Raw.degree, this] +lemma degree_zero [Zero R] : degree (0 : CPolynomial R) = ⊥ := by + rfl /-- The natural degree is the maximum element of the support. -/ -theorem natDegree_eq_support_sup (p : CPolynomial R) : +theorem natDegree_eq_support_sup [Zero R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : p.natDegree = p.support.sup (fun n => n) := by - have := p.2 - unfold CPolynomial.Raw.trim at this - cases h' : (p : CPolynomial.Raw R).lastNonzero <;> - simp_all +decide [ Array.ext_iff ] - · have h_zero : p.val = #[] := by - exact Array.eq_empty_of_size_eq_zero this.symm - cases p - simp_all +decide [ CPolynomial.natDegree ] - unfold CPolynomial.Raw.natDegree CPolynomial.support - simp +decide - grind - · rename_i k - have h_deg : ∀ n, n ∈ p.support → n ≤ k := by - intro n hn - have h_coeff : p.val.coeff n ≠ 0 := by - exact (CPolynomial.mem_support_iff p n).mp hn - have h_last : ∀ j, (hj : j < p.val.size) → j > k → p.val[j] = 0 := by - exact fun j hj₁ hj₂ => by linarith - have h_le : n ≤ k := by - grind - exact h_le - have h_deg : k.val ∈ p.support := by - exact CPolynomial.degree_eq_support_max_aux_mem_support p h' - rw [ show p.natDegree = k from ?_ ] - · exact le_antisymm (Finset.le_sup (f := fun n => n) h_deg) (Finset.sup_le ‹_›) - · rw [ CPolynomial.natDegree ] - unfold CPolynomial.Raw.natDegree - aesop + cases hs : p.val.size with + | zero => + have hval : p.val = (#[] : CPolynomial.Raw R) := Array.eq_empty_of_size_eq_zero hs + rw [CPolynomial.natDegree, CPolynomial.support, hval] + rfl + | succ n => + have hp : p.val.size > 0 := by simp [hs] + have hp' : n < p.val.size := by + simp [hs] + have hnat : p.natDegree = n := by + simp [CPolynomial.natDegree, hs] + have hlast : + p.val.lastNonzero = some ⟨n, hp'⟩ := by + simpa [hs] using (Trim.canonical_nonempty_iff (p := p.val) hp).mp (trim_eq p) + have hspec := Trim.lastNonzero_spec (p := p.val) (k := ⟨n, hp'⟩) hlast + have hn_mem : n ∈ p.support := by + exact degree_eq_support_max_aux_mem_support (p := p) hlast + have hle : ∀ m, m ∈ p.support → m ≤ n := by + intro m hm + have hm_lt : m < p.val.size := (Finset.mem_filter.mp hm).1 |> Finset.mem_range.mp + by_cases hmn : m ≤ n + · exact hmn + · have hm_gt : m > n := Nat.lt_of_not_ge hmn + have hm_zero : p.val[m] = 0 := hspec.2 m hm_lt hm_gt + have hm_nonzero : p.val.coeff m ≠ 0 := (CPolynomial.mem_support_iff p m).mp hm + have hcoeff : p.val.coeff m = p.val[m] := by + simpa using (Trim.coeff_eq_getElem (p := p.val) (i := m) hm_lt) + exact (hm_nonzero (hcoeff.trans hm_zero)).elim + rw [hnat] + apply le_antisymm + · simpa using (Finset.le_sup (f := fun m => m) hn_mem) + · exact Finset.sup_le fun m hm => hle m hm end Operations section Semiring -variable [Semiring R] [LawfulBEq R] -variable (p q r : CPolynomial R) - -lemma one_mul [Nontrivial R] (p : CPolynomial R) : 1 * p = p := by +lemma one_mul [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] + (p : CPolynomial R) : 1 * p = p := by apply Subtype.ext have : (1 * p : CPolynomial R) = (1: CPolynomial.Raw R) * p.val := rfl rw[this, one_mul_trim] - exact p.prop + exact trim_eq p -lemma mul_one [Nontrivial R] (p : CPolynomial R) : p * 1 = p := by +lemma mul_one [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] + (p : CPolynomial R) : p * 1 = p := by apply Subtype.ext have : (p * 1 : CPolynomial R) = p.val * (1: CPolynomial.Raw R) := rfl rw[this, mul_one_trim] - exact p.prop + exact trim_eq p -lemma mul_assoc (p q r : CPolynomial R) : (p * q) * r = p * (q * r) := by +lemma mul_assoc [Semiring R] [BEq R] [LawfulBEq R] + (p q r : CPolynomial R) : (p * q) * r = p * (q * r) := by apply Subtype.ext exact Raw.mul_assoc p.val q.val r.val -lemma zero_mul (p : CPolynomial R) : 0 * p = 0 := by +lemma zero_mul [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : 0 * p = 0 := by apply Subtype.ext exact Raw.zero_mul p.val -lemma mul_zero (p : CPolynomial R) : p * 0 = 0 := by +lemma mul_zero [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : p * 0 = 0 := by apply Subtype.ext exact Raw.mul_zero p.val -lemma mul_add (p q r : CPolynomial R) : p * (q + r) = p * q + p * r := by +lemma mul_add [Semiring R] [BEq R] [LawfulBEq R] + (p q r : CPolynomial R) : p * (q + r) = p * q + p * r := by apply Subtype.ext exact Raw.mul_add p.val q.val r.val -lemma add_mul (p q r : CPolynomial R) : (p + q) * r = p * r + q * r := by +lemma add_mul [Semiring R] [BEq R] [LawfulBEq R] + (p q r : CPolynomial R) : (p + q) * r = p * r + q * r := by apply Subtype.ext exact Raw.add_mul p.val q.val r.val -lemma pow_is_trimmed [Nontrivial R] +lemma pow_is_trimmed [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : CPolynomial.Raw R) (n : ℕ) : (p ^ n).trim = p ^ n := by induction' n with n ih generalizing p; · convert one_is_trimmed @@ -650,7 +722,7 @@ lemma pow_is_trimmed [Nontrivial R] rw [h_exp] convert mul_is_trimmed p ( p ^ n ) using 1 -lemma pow_succ_right [Nontrivial R] +lemma pow_succ_right [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : CPolynomial.Raw R) (n : ℕ) : p ^ (n + 1) = p ^ n * p := by convert pow_succ p n using 1; induction' n with n ih; @@ -664,34 +736,42 @@ lemma pow_succ_right [Nontrivial R] /-- `CPolynomial R` forms a commutative monoid when `R` is a semiring. -/ -instance : AddCommMonoid (CPolynomial R) where - zero_add := zero_add - add_zero := by intro p; exact add_zero p - nsmul := nsmul - nsmul_zero := nsmul_zero - nsmul_succ := nsmul_succ +instance [Semiring R] [BEq R] [LawfulBEq R] : AddCommMonoid (CPolynomial R) where + zero := 0 + add := (· + ·) + add_assoc := CPolynomial.add_assoc + add_comm := CPolynomial.add_comm + zero_add := CPolynomial.zero_add + add_zero := by intro p; exact CPolynomial.add_zero p + nsmul := CPolynomial.nsmul + nsmul_zero := CPolynomial.nsmul_zero + nsmul_succ := CPolynomial.nsmul_succ /-- `CPolynomial R` forms a semiring when `R` is a semiring. The semiring structure extends the `AddCommGroup` structure with multiplication. All operations preserve the canonical property (no trailing zeros). -/ -instance [LawfulBEq R] [Nontrivial R] : Semiring (CPolynomial R) where - add_assoc := add_assoc - zero_add := zero_add - add_zero := by intro p; exact add_zero p - add_comm := add_comm - zero_mul := by intro p; exact zero_mul p - mul_zero := by intro p; exact mul_zero p - mul_assoc := by intro p q r; exact mul_assoc p q r - one_mul := by intro p; exact one_mul p - mul_one := by intro p; exact mul_one p - left_distrib := by intro p q r; exact mul_add p q r - right_distrib := by intro p q r; exact add_mul p q r - nsmul := nsmul - nsmul_zero := nsmul_zero - nsmul_succ := nsmul_succ - npow n p := ⟨p.val ^ n, by apply CPolynomial.pow_is_trimmed⟩ +instance [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] : Semiring (CPolynomial R) where + zero := 0 + one := 1 + add := (· + ·) + mul := (· * ·) + add_assoc := CPolynomial.add_assoc + zero_add := CPolynomial.zero_add + add_zero := by intro p; exact CPolynomial.add_zero p + add_comm := CPolynomial.add_comm + zero_mul := by intro p; exact CPolynomial.zero_mul p + mul_zero := by intro p; exact CPolynomial.mul_zero p + mul_assoc := by intro p q r; exact CPolynomial.mul_assoc p q r + one_mul := by intro p; exact CPolynomial.one_mul p + mul_one := by intro p; exact CPolynomial.mul_one p + left_distrib := by intro p q r; exact CPolynomial.mul_add p q r + right_distrib := by intro p q r; exact CPolynomial.add_mul p q r + nsmul := CPolynomial.nsmul + nsmul_zero := CPolynomial.nsmul_zero + nsmul_succ := CPolynomial.nsmul_succ + npow n p := ⟨p.val ^ n, Trim.isCanonical_of_trim_eq (CPolynomial.pow_is_trimmed p.val n)⟩ npow_zero := by intro x; apply Subtype.ext; rfl npow_succ := by intro n p; apply Subtype.ext; exact (CPolynomial.pow_succ_right p.val n) @@ -699,7 +779,8 @@ instance [LawfulBEq R] [Nontrivial R] : Semiring (CPolynomial R) where natCast_succ := by intro n; rfl /-- `C r * X^n = monomial n r` as canonical polynomials. -/ -lemma C_mul_X_pow_eq_monomial [LawfulBEq R] [DecidableEq R] [Nontrivial R] (r : R) (n : ℕ) : +lemma C_mul_X_pow_eq_monomial [Semiring R] [BEq R] [LawfulBEq R] [DecidableEq R] [Nontrivial R] + (r : R) (n : ℕ) : (C r : CPolynomial R) * (X ^ n) = monomial n r := by by_cases hr : r = 0 · convert Subtype.ext ?_ @@ -731,10 +812,7 @@ end Semiring section CommSemiring -variable [CommSemiring R] [LawfulBEq R] -variable (p q : CPolynomial R) - -lemma mul_comm (p q : CPolynomial R) : p * q = q * p := by +lemma mul_comm [CommSemiring R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) : p * q = q * p := by apply Subtype.ext have dist_lhs : (p * q : CPolynomial R) = (p.val * q.val : CPolynomial.Raw R) := rfl have dist_rhs : (q * p : CPolynomial R) = (q.val * p.val : CPolynomial.Raw R) := rfl @@ -745,34 +823,35 @@ lemma mul_comm (p q : CPolynomial R) : p * q = q * p := by Commutativity follows from the commutativity of multiplication in the base ring. -/ -instance [CommSemiring R] [Nontrivial R] : CommSemiring (CPolynomial R) where +instance [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] : CommSemiring (CPolynomial R) where + __ := (inferInstance : Semiring (CPolynomial R)) mul_comm := by intro p q; exact mul_comm p q end CommSemiring section Ring -variable [Ring R] [LawfulBEq R] -variable (p q : CPolynomial R) - -instance : Neg (CPolynomial R) where - neg p := ⟨-p.val, neg_trim p.val p.prop⟩ +instance [Ring R] [BEq R] [LawfulBEq R] : Neg (CPolynomial R) where + neg p := ⟨-p.val, Trim.isCanonical_of_trim_eq (neg_trim p.val (trim_eq p))⟩ -instance : Sub (CPolynomial R) where +instance [Ring R] [BEq R] [LawfulBEq R] : Sub (CPolynomial R) where sub p q := p + -q -lemma erase_canonical [DecidableEq R] (n : ℕ) (p : CPolynomial R) : +lemma erase_canonical [Ring R] [BEq R] [LawfulBEq R] [DecidableEq R] + (n : ℕ) (p : CPolynomial R) : let e := p.val - Raw.monomial n (p.val.coeff n) e.trim = e := by simp; apply Trim.trim_twice /-- Erase the coefficient at index `n` (same as `p` except `coeff n = 0`, then trimmed). -/ -def erase [DecidableEq R] (n : ℕ) (p : CPolynomial R) : CPolynomial R := +def erase [Ring R] [BEq R] [LawfulBEq R] [DecidableEq R] + (n : ℕ) (p : CPolynomial R) : CPolynomial R := let e := p.val - Raw.monomial n (p.val.coeff n) - ⟨e, by rw [erase_canonical]⟩ + ⟨e, Trim.isCanonical_of_trim_eq (by rw [erase_canonical])⟩ /-- Coefficient of `erase n p`: zero at `n`, otherwise `coeff p i`. -/ -lemma coeff_erase [DecidableEq R] (n i : ℕ) (p : CPolynomial R) : +lemma coeff_erase [Ring R] [BEq R] [LawfulBEq R] [DecidableEq R] + (n i : ℕ) (p : CPolynomial R) : coeff (erase n p) i = if i = n then 0 else coeff p i := by unfold erase coeff rw [Raw.sub_coeff, Raw.coeff_monomial] @@ -781,138 +860,113 @@ lemma coeff_erase [DecidableEq R] (n i : ℕ) (p : CPolynomial R) : contradiction /-- Leading coefficient equals the coefficient at `natDegree`. -/ -lemma leadingCoeff_eq_coeff_natDegree [Semiring R] [DecidableEq R] (p : CPolynomial R) : +lemma leadingCoeff_eq_coeff_natDegree [Zero R] (p : CPolynomial R) : p.leadingCoeff = p.coeff p.natDegree := by - -- If empty, both leadingCoeff and coeff at natDegree are zero. - by_cases h_empty : p.val.size = 0; - · simp +decide [h_empty, CPolynomial.leadingCoeff, CPolynomial.coeff, - CPolynomial.natDegree] - unfold Raw.leadingCoeff - unfold Raw.trim; aesop - · -- Since `p` is canonical, `p.val.getLastD 0` is the last element of `p.val`. - have h_last : p.val.getLastD 0 = p.val.coeff (p.val.size - 1) := by - simp +decide [Array.getLastD, Raw.coeff] - cases h : (p : CPolynomial.Raw R)[(p : CPolynomial.Raw R).size - 1]? <;> - aesop - have h_natDegree : p.val.lastNonzero = - some ⟨p.val.size - 1, Nat.pred_lt_self (Nat.pos_of_ne_zero h_empty)⟩ := by - convert Trim.lastNonzero_last_iff (show p.val.size > 0 from Nat.pos_of_ne_zero h_empty) - |>.2 _ - convert Trim.canonical_iff.mp p.prop using 1 - generalize_proofs at * - exact ⟨fun h hp => h, fun h => h ‹_›⟩ - -- natDegree is the index of the last non-zero coefficient: p.natDegree = p.val.size - 1. - have h_natDegree_eq : p.natDegree = p.val.size - 1 := by - have h_natDegree_eq : p.natDegree = p.val.natDegree := by rfl - unfold Raw.natDegree at *; aesop - convert h_last using 1 - · rw [leadingCoeff, Raw.leadingCoeff, p.prop] - exact id (Eq.symm h_last) - · exact h_natDegree_eq ▸ rfl + cases hs : p.val.size with + | zero => + have hval : p.val = (#[] : CPolynomial.Raw R) := Array.eq_empty_of_size_eq_zero hs + have hp0 : p = 0 := by + apply CPolynomial.ext + simpa using hval + cases hp0 + rfl + | succ n => + have hnat : p.natDegree = n := by simp [CPolynomial.natDegree, hs] + rw [hnat] + simp [CPolynomial.leadingCoeff, CPolynomial.coeff, Raw.coeff, Array.getLastD, hs] /-- A polynomial equals its leading monomial plus the rest (`erase` at `natDegree`). -/ -lemma monomial_add_erase [DecidableEq R] (p : CPolynomial R) : +lemma monomial_add_erase [Ring R] [BEq R] [LawfulBEq R] [DecidableEq R] + (p : CPolynomial R) : p = monomial p.natDegree p.leadingCoeff + erase p.natDegree p := by - apply CPolynomial.ext - refine' Eq.symm ( Trim.canonical_ext _ _ _ ) - · exact Trim.trim_twice _ - · exact p.2 - · intro i; simp - convert Raw.add_coeff_trimmed _ _ i using 1 - rotate_left - rotate_left - (expose_names; exact inst_1.toSemiring) - (expose_names; exact inst) - (expose_names; exact inst_2) - exact Raw.monomial p.natDegree p.leadingCoeff - exact p.val - Raw.monomial p.natDegree ( p.val.coeff p.natDegree ) - · exact Eq.symm Array.getD_eq_getD_getElem? - · convert Eq.symm ( add_sub_cancel _ _ ) using 1 - congr! 1 - convert Raw.sub_coeff _ _ _ using 1 - · congr! 1 - · exact Eq.symm Array.getD_eq_getD_getElem? - · congr! 1 - congr! 1 - exact leadingCoeff_eq_coeff_natDegree p - · grind - -lemma coeff_neg (p : CPolynomial R) (i : ℕ) : coeff (-p) i = -coeff p i := by + apply (eq_iff_coeff).2 + intro i + rw [coeff_add, coeff_monomial, coeff_erase] + by_cases hi : i = p.natDegree + · subst hi + rw [if_pos rfl, if_pos rfl, leadingCoeff_eq_coeff_natDegree] + simp + · rw [if_neg hi, if_neg hi] + simp + +lemma coeff_neg [Ring R] [BEq R] [LawfulBEq R] + (p : CPolynomial R) (i : ℕ) : coeff (-p) i = -coeff p i := by unfold coeff; exact Raw.neg_coeff p.val i -lemma coeff_sub (p q : CPolynomial R) (i : ℕ) : coeff (p - q) i = coeff p i - coeff q i := by +lemma coeff_sub [Ring R] [BEq R] [LawfulBEq R] + (p q : CPolynomial R) (i : ℕ) : coeff (p - q) i = coeff p i - coeff q i := by unfold coeff; exact Raw.sub_coeff p.val q.val i -theorem neg_add_cancel : -p + p = 0 := by +theorem neg_add_cancel [Ring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : -p + p = 0 := by apply Subtype.ext have dist_lhs : (-p + p).val = ((-p).val + p.val) := rfl rw [dist_lhs] exact Raw.neg_add_cancel p.val -instance : AddCommGroup (CPolynomial R) where - add_assoc := add_assoc - zero_add := zero_add - add_zero := add_zero - add_comm := add_comm - neg_add_cancel := by intro a; exact neg_add_cancel a - nsmul := nsmul -- TODO do we actually need this custom implementation? - nsmul_zero := nsmul_zero - nsmul_succ := nsmul_succ - zsmul := zsmulRec -- TODO do we want a custom efficient implementation? +instance [Ring R] [BEq R] [LawfulBEq R] : AddCommGroup (CPolynomial R) where + zero := 0 + add := (· + ·) + neg := Neg.neg + sub := HSub.hSub + add_assoc := CPolynomial.add_assoc + zero_add := CPolynomial.zero_add + add_zero := CPolynomial.add_zero + add_comm := CPolynomial.add_comm + neg_add_cancel := by intro a; exact CPolynomial.neg_add_cancel (p := a) + nsmul := CPolynomial.nsmul + nsmul_zero := CPolynomial.nsmul_zero + nsmul_succ := CPolynomial.nsmul_succ + sub_eq_add_neg := by intro a b; rfl + zsmul := zsmulRec + zsmul_zero' := by intro p; apply Subtype.ext; rfl + zsmul_succ' := by intro n p; apply Subtype.ext; rfl + zsmul_neg' := by intro n p; apply Subtype.ext; rfl /-- `CPolynomial R` forms a ring when `R` is a ring. The ring structure extends the semiring structure with negation and subtraction. Most of the structure is already provided by the `Semiring` instance. -/ -instance [LawfulBEq R] [Nontrivial R] : Ring (CPolynomial R) where - sub_eq_add_neg := by intro a b; rfl - zsmul := zsmulRec - zsmul_zero' := by intro p; apply Subtype.ext; rfl - zsmul_succ' := by intro n p; apply Subtype.ext; rfl - zsmul_neg' := by intro n p; apply Subtype.ext; rfl +instance [Ring R] [BEq R] [LawfulBEq R] [Nontrivial R] : Ring (CPolynomial R) where + __ := (inferInstance : Semiring (CPolynomial R)) + __ := (inferInstance : AddCommGroup (CPolynomial R)) intCast_ofNat := by intro n; apply Subtype.ext; rfl intCast_negSucc := by intro n; apply Subtype.ext; rfl - neg_add_cancel := by intro p; exact neg_add_cancel p end Ring section CommRing -variable [CommRing R] [LawfulBEq R] - /-- `CPolynomial R` forms a commutative ring when `R` is a commutative ring. This combines the `CommSemiring` and `Ring` structures. -/ -instance [Nontrivial R] : CommRing (CPolynomial R) where - -- All structure inherited from `CommSemiring` and `Ring` instances +instance [CommRing R] [BEq R] [LawfulBEq R] [Nontrivial R] : CommRing (CPolynomial R) where + __ := (inferInstance : Ring (CPolynomial R)) + __ := (inferInstance : CommSemiring (CPolynomial R)) end CommRing section Division -variable [Field R] [LawfulBEq R] -variable (p q : CPolynomial R) - /-- Quotient of `p` by a monic polynomial `q`. Matches Mathlib's `Polynomial.divByMonic`. -/ -def divByMonic (p q : CPolynomial R) : CPolynomial R := - ⟨(Raw.divByMonic p.val q.val).trim, by simpa using Trim.trim_twice (Raw.divByMonic p.val q.val)⟩ +def divByMonic [Field R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) : CPolynomial R := + ⟨(Raw.divByMonic p.val q.val).trim, Trim.isCanonical_trim (Raw.divByMonic p.val q.val)⟩ /-- Remainder of `p` modulo a monic polynomial `q`. Matches Mathlib's `Polynomial.modByMonic`. -/ -def modByMonic (p q : CPolynomial R) : CPolynomial R := - ⟨(Raw.modByMonic p.val q.val).trim, by simpa using Trim.trim_twice (Raw.modByMonic p.val q.val)⟩ +def modByMonic [Field R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) : CPolynomial R := + ⟨(Raw.modByMonic p.val q.val).trim, Trim.isCanonical_trim (Raw.modByMonic p.val q.val)⟩ /-- Quotient of `p` by `q` (when `R` is a field). -/ -def div (p q : CPolynomial R) : CPolynomial R := - ⟨(Raw.div p.val q.val).trim, by simpa using Trim.trim_twice (Raw.div p.val q.val)⟩ +def div [Field R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) : CPolynomial R := + ⟨(Raw.div p.val q.val).trim, Trim.isCanonical_trim (Raw.div p.val q.val)⟩ /-- Remainder of `p` modulo `q` (when `R` is a field). -/ -def mod (p q : CPolynomial R) : CPolynomial R := - ⟨(Raw.mod p.val q.val).trim, by simpa using Trim.trim_twice (Raw.mod p.val q.val)⟩ +def mod [Field R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) : CPolynomial R := + ⟨(Raw.mod p.val q.val).trim, Trim.isCanonical_trim (Raw.mod p.val q.val)⟩ -instance : Div (CPolynomial R) := ⟨div⟩ -instance : Mod (CPolynomial R) := ⟨mod⟩ +instance [Field R] [BEq R] [LawfulBEq R] : Div (CPolynomial R) := ⟨div⟩ +instance [Field R] [BEq R] [LawfulBEq R] : Mod (CPolynomial R) := ⟨mod⟩ end Division @@ -920,33 +974,33 @@ section ModuleTheory -- The assumptions are required for `CPolynomial R` to be a module and are necessary downstream. -variable [Semiring R] [LawfulBEq R] - /-- Scalar multiplication for canonical polynomials: multiply each coefficient by `r`, then trim to restore canonicity. -/ -instance smul : SMul R (CPolynomial R) where - smul r p := ⟨(Raw.smul r p.val).trim, Trim.trim_twice _⟩ +instance smul [Semiring R] [BEq R] [LawfulBEq R] : SMul R (CPolynomial R) where + smul r p := ⟨(Raw.smul r p.val).trim, Trim.isCanonical_trim (Raw.smul r p.val)⟩ /-- Coefficient of a scalar multiple. -/ -lemma coeff_smul (r : R) (p : CPolynomial R) (i : ℕ) : +lemma coeff_smul [Semiring R] [BEq R] [LawfulBEq R] + (r : R) (p : CPolynomial R) (i : ℕ) : coeff (r • p) i = r * coeff p i := by show (Raw.smul r p.val).trim.coeff i = r * p.val.coeff i rw [Trim.coeff_eq_coeff, Raw.smul_equiv] /-- Scalar multiplication on 0 gives 0. -/ -lemma smul_zero (r : R) : r • (0 : CPolynomial R) = 0 := by +lemma smul_zero [Semiring R] [BEq R] [LawfulBEq R] (r : R) : r • (0 : CPolynomial R) = 0 := by rw [eq_iff_coeff]; intro i rw [coeff_smul, coeff_zero]; simp /-- Helper lemma: Two CPolynomials are equal if the underlying Raw CPolynomials are trim equivalent. -/ -lemma smul_eq_of_coeff_eq {p q : CPolynomial R} +lemma smul_eq_of_coeff_eq [Zero R] [BEq R] [LawfulBEq R] {p q : CPolynomial R} (h : Trim.equiv p.val q.val) : p = q := by apply CPolynomial.ext - exact Trim.canonical_ext p.prop q.prop h + exact Trim.isCanonical_ext p.property q.property h /-- Scalar multiplication distributes. -/ -lemma smul_add (r : R) (p q : CPolynomial R) : +lemma smul_add [Semiring R] [BEq R] [LawfulBEq R] + (r : R) (p q : CPolynomial R) : r • (p + q) = r • p + r • q := by apply smul_eq_of_coeff_eq; intro i show (Raw.smul r (p.val + q.val)).trim.coeff i = @@ -957,31 +1011,33 @@ lemma smul_add (r : R) (p q : CPolynomial R) : exact Distrib.left_distrib r (p.val.coeff i) (q.val.coeff i) /-- Scalar multiplication distributes across scalar addition. -/ -lemma add_smul (r s : R) (p : CPolynomial R) : +lemma add_smul [Semiring R] [BEq R] [LawfulBEq R] + (r s : R) (p : CPolynomial R) : (r + s) • p = r • p + s • p := by rw [eq_iff_coeff]; intro i rw [coeff_smul, coeff_add, coeff_smul, coeff_smul]; grind /-- Scalar multiplication by 0 gives 0. -/ -lemma zero_smul (p : CPolynomial R) : (0 : R) • p = 0 := by +lemma zero_smul [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : (0 : R) • p = 0 := by apply smul_eq_of_coeff_eq; intro i show (Raw.smul 0 p.val).trim.coeff i = (0 : Raw R).coeff i rw [Trim.coeff_eq_coeff, smul_equiv] exact MulZeroClass.zero_mul (p.val.coeff i) /-- Scalar multiplication on p by 1 gives p. -/ -lemma one_smul (p : CPolynomial R) : (1 : R) • p = p := by +lemma one_smul [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : (1 : R) • p = p := by rw [eq_iff_coeff]; intro i rw [coeff_smul, _root_.one_mul] /-- Scalar multiplication is associative. -/ -lemma mul_smul (r s : R) (p : CPolynomial R) : +lemma mul_smul [Semiring R] [BEq R] [LawfulBEq R] + (r s : R) (p : CPolynomial R) : (r * s) • p = r • (s • p) := by rw [eq_iff_coeff]; intro i rw [coeff_smul, coeff_smul, coeff_smul, _root_.mul_assoc] /-- `CPolynomial` forms a module when R is a semiring. -/ -instance : Module R (CPolynomial R) where +instance [Semiring R] [BEq R] [LawfulBEq R] : Module R (CPolynomial R) where smul:= SMul.smul mul_smul := mul_smul one_smul := one_smul diff --git a/CompPoly/Univariate/Linear.lean b/CompPoly/Univariate/Linear.lean index 21672d55..ffa08c15 100644 --- a/CompPoly/Univariate/Linear.lean +++ b/CompPoly/Univariate/Linear.lean @@ -8,64 +8,171 @@ import CompPoly.Univariate.Basic /-! # Linear Algebra API for Computable Univariate Polynomials -This file contains linear-map and bounded-degree submodule constructions for `CPolynomial`. +This file contains linear maps and instance-stable bounded-degree predicates for `CPolynomial`. -/ namespace CompPoly namespace CPolynomial -variable {R : Type*} [BEq R] +variable {R : Type*} -section LinearTheory +section LinearMaps -variable [Semiring R] [LawfulBEq R] +variable [Semiring R] [BEq R] [LawfulBEq R] /-- This is an R-linear function that returns the coefficient of X^n. -/ -def lcoeff (S : Type*) [BEq S] [Semiring S] [LawfulBEq S] (n : ℕ) : (CPolynomial S) →ₗ[S] S where +def lcoeff (n : ℕ) : (CPolynomial R) →ₗ[R] R where toFun p := coeff p n map_add' p q := coeff_add p q n map_smul' r p := coeff_smul r p n -/-- The `R`-submodule of `CPolynomial R` consisting of polynomials of degree ≤ `n`. -/ -def degreeLE (S : Type*) [BEq S] [Semiring S] [LawfulBEq S] (n : WithBot ℕ) : - Submodule S (CPolynomial S) := - ⨅ k : ℕ, ⨅ _ : ↑k > n, LinearMap.ker (lcoeff S k) - -/-- The `R`-submodule of `CPolynomial R` consisting of polynomials of degree < `n`. -/ -def degreeLT (S : Type*) [BEq S] [Semiring S] [LawfulBEq S] (n : ℕ) : - Submodule S (CPolynomial S) := - ⨅ k : ℕ, ⨅ (_ : k ≥ n), LinearMap.ker (lcoeff S k) - -/-- The forward map of `degreeLTEquiv` preserves addition: - extracting coefficients commutes with polynomial addition. -/ -lemma degreeLTEquiv_map_add (n : ℕ) - (p q : ↥(degreeLT R n)) : - (fun i : Fin n => coeff (↑(p + q) : CPolynomial R) (↑i)) = - (fun i : Fin n => coeff (↑p : CPolynomial R) (↑i) + coeff (↑q : CPolynomial R) (↑i)) := by - exact funext fun i => coeff_add _ _ _ - -/-- The forward map of `degreeLTEquiv` preserves scalar multiplication: - extracting coefficients commutes with scalar multiplication. -/ -lemma degreeLTEquiv_map_smul (n : ℕ) - (r : R) (p : ↥(degreeLT R n)) : - (fun i : Fin n => coeff (↑(r • p) : CPolynomial R) (↑i)) = - (fun i : Fin n => r * coeff (↑p : CPolynomial R) (↑i)) := by - exact funext fun i => coeff_smul r ↑p i - -/-- The first `n` coefficients on `degreeLT n` define a linear map to `Fin n → R`. - - This is the computable polynomial analogue of `Polynomial.degreeLTEquiv`. - - The map sends a polynomial `p` with `degree p < n` to the function - `i ↦ coeff p i` for `i : Fin n`. -/ -def degreeLTEquiv (S : Type*) [BEq S] [Semiring S] [LawfulBEq S] [DecidableEq S] (n : ℕ) : - degreeLT S n →ₗ[S] (Fin n → S) where - toFun p i := coeff p.1 i - map_add' := fun p q => degreeLTEquiv_map_add n p q - map_smul' := fun r p => degreeLTEquiv_map_smul n r p - -end LinearTheory +end LinearMaps + +section DegreeBounds + +variable [Zero R] + +/-- The set of `CPolynomial R` consisting of polynomials of degree ≤ `n`. -/ +def degreeLE (n : WithBot ℕ) : Set (CPolynomial R) := + { p | p.val.degreeBound ≤ n } + +/-- The set of `CPolynomial R` consisting of polynomials of degree < `n`. -/ +def degreeLT (n : ℕ) : Set (CPolynomial R) := + { p | p.val.degreeBound < n } + +/-- `degreeLT n` is exactly the bounded-size carrier storing at most `n` coefficients. -/ +theorem mem_degreeLT_iff_size_le {n : ℕ} {p : CPolynomial R} : + p ∈ degreeLT (R := R) n ↔ p.val.size ≤ n := by + cases hs : p.val.size with + | zero => + simp [degreeLT, Raw.degreeBound, hs] + | succ m => + simp [degreeLT, Raw.degreeBound, hs] + +/-- The zero polynomial has bounded degree for every cutoff. -/ +theorem zero_mem_degreeLT (n : ℕ) : (0 : CPolynomial R) ∈ degreeLT (R := R) n := by + rw [mem_degreeLT_iff_size_le] + exact Nat.zero_le n + +end DegreeBounds + +section DegreeLTSubtype + +variable [Semiring R] [BEq R] [LawfulBEq R] + +/-- `degreeLT n` is closed under addition. -/ +theorem add_mem_degreeLT {n : ℕ} {p q : CPolynomial R} + (hp : p ∈ degreeLT (R := R) n) (hq : q ∈ degreeLT (R := R) n) : + p + q ∈ degreeLT (R := R) n := by + rw [mem_degreeLT_iff_size_le] at hp hq ⊢ + calc + (p + q).val.size = (Raw.addRaw p.val q.val).trim.size := by rfl + _ ≤ (Raw.addRaw p.val q.val).size := Raw.Trim.size_le_size _ + _ = max p.val.size q.val.size := Raw.add_size + _ ≤ n := max_le hp hq + +/-- `degreeLT n` is closed under additive scalar multiplication. -/ +theorem nsmul_mem_degreeLT {n m : ℕ} {p : CPolynomial R} + (hp : p ∈ degreeLT (R := R) n) : + m • p ∈ degreeLT (R := R) n := by + rw [mem_degreeLT_iff_size_le] at hp ⊢ + calc + (m • p).val.size = (Raw.nsmulRaw m p.val).trim.size := by rfl + _ ≤ (Raw.nsmulRaw m p.val).size := Raw.Trim.size_le_size _ + _ = p.val.size := by simp [Raw.nsmulRaw] + _ ≤ n := hp + +/-- `degreeLT n` is closed under semiring scalar multiplication. -/ +theorem smul_mem_degreeLT {n : ℕ} (r : R) {p : CPolynomial R} + (hp : p ∈ degreeLT (R := R) n) : + r • p ∈ degreeLT (R := R) n := by + rw [mem_degreeLT_iff_size_le] at hp ⊢ + calc + (r • p).val.size = (Raw.smul r p.val).trim.size := by rfl + _ ≤ (Raw.smul r p.val).size := Raw.Trim.size_le_size _ + _ = p.val.size := by simp [Raw.smul] + _ ≤ n := hp + +instance (n : ℕ) : Zero ↥(degreeLT (R := R) n) where + zero := ⟨0, zero_mem_degreeLT (R := R) n⟩ + +instance (n : ℕ) : Add ↥(degreeLT (R := R) n) where + add p q := ⟨p.1 + q.1, add_mem_degreeLT p.2 q.2⟩ + +instance (n : ℕ) : SMul ℕ ↥(degreeLT (R := R) n) where + smul m p := ⟨m • p.1, nsmul_mem_degreeLT (R := R) (n := n) (m := m) p.2⟩ + +instance (n : ℕ) : SMul R ↥(degreeLT (R := R) n) where + smul r p := ⟨r • p.1, smul_mem_degreeLT (R := R) (n := n) r p.2⟩ + +instance (n : ℕ) : AddCommMonoid ↥(degreeLT (R := R) n) where + add_assoc := by + intro a b c + apply Subtype.ext + simpa using (CPolynomial.add_assoc a.1 b.1 c.1) + add_comm := by + intro a b + apply Subtype.ext + simpa using (CPolynomial.add_comm a.1 b.1) + zero_add := by + intro a + apply Subtype.ext + exact CPolynomial.zero_add a.1 + add_zero := by + intro a + apply Subtype.ext + exact CPolynomial.add_zero a.1 + nsmul := (· • ·) + nsmul_zero := by + intro p + apply Subtype.ext + exact CPolynomial.nsmul_zero p.1 + nsmul_succ := by + intro m p + apply Subtype.ext + simpa using (CPolynomial.nsmul_succ m p.1) + +instance (n : ℕ) : Module R ↥(degreeLT (R := R) n) where + smul := (· • ·) + one_smul := by + intro p + apply Subtype.ext + exact CPolynomial.one_smul p.1 + mul_smul := by + intro r s p + apply Subtype.ext + simpa using (CPolynomial.mul_smul r s p.1) + smul_zero := by + intro r + apply Subtype.ext + exact CPolynomial.smul_zero (R := R) r + smul_add := by + intro r p q + apply Subtype.ext + exact CPolynomial.smul_add r p.1 q.1 + add_smul := by + intro r s p + apply Subtype.ext + simpa using (CPolynomial.add_smul r s p.1) + zero_smul := by + intro p + apply Subtype.ext + exact CPolynomial.zero_smul p.1 + +/-- The first `n` coefficients on `degreeLT n` form a computable linear map to `Fin n → R`. -/ +def degreeLTCoeffs (n : ℕ) : ↥(degreeLT (R := R) n) →ₗ[R] (Fin n → R) where + toFun p i := coeff p.1 ↑i + map_add' := by + intro p q + funext i + exact coeff_add p.1 q.1 i + map_smul' := by + intro r p + funext i + exact coeff_smul r p.1 i + +end DegreeLTSubtype end CPolynomial diff --git a/CompPoly/Univariate/Quotient.lean b/CompPoly/Univariate/Quotient.lean index 26e62fa6..03fb4c8d 100644 --- a/CompPoly/Univariate/Quotient.lean +++ b/CompPoly/Univariate/Quotient.lean @@ -24,33 +24,33 @@ namespace CPolynomial open Raw Trim -variable {R : Type*} [Ring R] [BEq R] -variable {Q : Type*} [Ring Q] +variable {R : Type*} +variable {Q : Type*} /-- Reflexivity of the equivalence relation. -/ -@[simp] theorem equiv_refl (p : CPolynomial.Raw Q) : equiv p p := +@[simp] theorem equiv_refl [Zero Q] (p : CPolynomial.Raw Q) : equiv p p := by simp [equiv] /-- Symmetry of the equivalence relation. -/ -@[simp] theorem equiv_symm {p q : CPolynomial.Raw Q} : equiv p q → equiv q p := by +@[simp] theorem equiv_symm [Zero Q] {p q : CPolynomial.Raw Q} : equiv p q → equiv q p := by simp [equiv] intro h i exact Eq.symm (h i) /-- Transitivity of the equivalence relation. -/ -@[simp] theorem equiv_trans {p q r : CPolynomial.Raw Q} : +@[simp] theorem equiv_trans [Zero Q] {p q r : CPolynomial.Raw Q} : Trim.equiv p q → equiv q r → equiv p r := by simp_all [Trim.equiv] /-- The `CPolynomial.Raw.equiv` is indeed an equivalence relation. -/ -instance instEquivalenceEquiv : Equivalence (equiv (R := R)) where +instance instEquivalenceEquiv [Zero R] : Equivalence (equiv (R := R)) where refl := equiv_refl symm := equiv_symm trans := equiv_trans /-- The `Setoid` instance for `CPolynomial.Raw R` induced by `CPolynomial.Raw.equiv`. -/ -instance Raw.instSetoidCPolynomial : Setoid (CPolynomial.Raw R) where +instance Raw.instSetoidCPolynomial [Zero R] : Setoid (CPolynomial.Raw R) where r := equiv iseqv := instEquivalenceEquiv @@ -58,19 +58,20 @@ instance Raw.instSetoidCPolynomial : Setoid (CPolynomial.Raw R) where This quotient identifies polynomials that differ only by trailing zeros, and is intended to be equivalent to mathlib's `Polynomial R`. -/ -def QuotientCPolynomial (R : Type*) [Ring R] [BEq R] := Quotient (@Raw.instSetoidCPolynomial R _) +def QuotientCPolynomial (R : Type*) [Zero R] := Quotient (@Raw.instSetoidCPolynomial R _) namespace QuotientCPolynomial -- The operations on `CPolynomial.Raw` descend to `QuotientCPolynomial` section EquivalenceLemmas -omit [BEq R] in /-- Convert propositional equality to equivalence. -/ -lemma eq_to_equiv (p q : CPolynomial.Raw R) : p = q → p ≈ q := by intro h; rw [h] +lemma eq_to_equiv [Zero R] (p q : CPolynomial.Raw R) : p = q → p ≈ q := by + intro h + rw [h] /-- Scalar multiplication by 0 is equivalent to the zero polynomial. -/ -lemma smul_zero_equiv {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (p : CPolynomial.Raw R) : +lemma smul_zero_equiv {R : Type*} [Semiring R] (p : CPolynomial.Raw R) : (smul 0 p) ≈ 0 := by have h_smul_zero : ∀ (p : CPolynomial.Raw R), (smul 0 p).coeff = 0 := by intro p; ext i; simp [smul] @@ -78,7 +79,7 @@ lemma smul_zero_equiv {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (p : CPolynomia exact fun i => by simpa using congr_fun (h_smul_zero p) i /-- Addition respects the equivalence relation. -/ -lemma add_equiv {R : Type*} [Ring R] [BEq R] [LawfulBEq R] +lemma add_equiv {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] (p1 p2 q1 q2 : CPolynomial.Raw R) (hp : equiv p1 p2) (hq : equiv q1 q2) : equiv (p1.add q1) (p2.add q2) := by @@ -90,7 +91,7 @@ lemma add_equiv {R : Type*} [Ring R] [BEq R] [LawfulBEq R] simp_all [ equiv ] /-- Multiplication by `X^i` respects the equivalence relation. -/ -lemma mulPowX_equiv {R : Type*} [Ring R] [BEq R] [LawfulBEq R] +lemma mulPowX_equiv {R : Type*} [Zero R] (i : ℕ) (p q : CPolynomial.Raw R) (h : equiv p q) : equiv (mulPowX i p) (mulPowX i q) := by unfold equiv at * @@ -102,7 +103,7 @@ lemma mulPowX_equiv {R : Type*} [Ring R] [BEq R] [LawfulBEq R] · rw [ if_neg ( not_lt_of_ge hj ) ] /-- Adding a polynomial equivalent to zero acts as the identity. -/ -lemma add_zero_equiv {R : Type*} [Ring R] [BEq R] [LawfulBEq R] +lemma add_zero_equiv {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] (p q : CPolynomial.Raw R) (hq : equiv q 0) : equiv (add p q) p := by intro x @@ -113,7 +114,7 @@ lemma add_zero_equiv {R : Type*} [Ring R] [BEq R] [LawfulBEq R] aesop /-- Multiplying the zero polynomial by `X^i` results in a polynomial equivalent to zero. -/ -lemma mulPowX_zero_equiv {R : Type*} [Ring R] [BEq R] [LawfulBEq R] +lemma mulPowX_zero_equiv {R : Type*} [Zero R] (i : ℕ) : equiv (mulPowX i (0 : CPolynomial.Raw R)) 0 := by unfold equiv simp [coeff] @@ -121,19 +122,19 @@ lemma mulPowX_zero_equiv {R : Type*} [Ring R] [BEq R] [LawfulBEq R] grind /-- A single step in polynomial multiplication: add `(coefficient * q) * X^power` to accumulator. -/ -def mulStep {R : Type*} [Ring R] [BEq R] [LawfulBEq R] +def mulStep {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] (q : CPolynomial.Raw R) (acc : CPolynomial.Raw R) (x : R × ℕ) : CPolynomial.Raw R := acc.add ((smul x.1 q).mulPowX x.2) /-- The multiplication step respects equivalence of the accumulator. -/ -lemma mulStep_equiv {R : Type*} [Ring R] [BEq R] [LawfulBEq R] +lemma mulStep_equiv {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] (q : CPolynomial.Raw R) (acc1 acc2 : CPolynomial.Raw R) (x : R × ℕ) (h : equiv acc1 acc2) : equiv (mulStep q acc1 x) (mulStep q acc2 x) := by apply_rules [ add_equiv, mulPowX_equiv, smul_equiv ] /-- The multiplication step with a zero coefficient acts as the identity modulo equivalence. -/ -lemma mulStep_zero {R : Type*} [Ring R] [BEq R] [LawfulBEq R] +lemma mulStep_zero {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] (q : CPolynomial.Raw R) (acc : CPolynomial.Raw R) (i : ℕ) : equiv (mulStep q acc (0, i)) acc := by have h_mulStep : mulStep q acc (0, i) = acc.add ((smul 0 q).mulPowX i) := by exact rfl @@ -142,7 +143,7 @@ lemma mulStep_zero {R : Type*} [Ring R] [BEq R] [LawfulBEq R] exact add_zero_equiv _ _ ( smul_zero_equiv _ ) /-- Folding `mulStep` over a list of zero coefficients preserves equivalence. -/ -lemma foldl_mulStep_zeros {R : Type*} [Ring R] [BEq R] [LawfulBEq R] +lemma foldl_mulStep_zeros {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] (q : CPolynomial.Raw R) (acc : CPolynomial.Raw R) (l : List (R × ℕ)) (hl : ∀ x ∈ l, x.1 = 0) : equiv (l.foldl (mulStep q) acc) acc := by @@ -158,7 +159,7 @@ lemma foldl_mulStep_zeros {R : Type*} [Ring R] [BEq R] [LawfulBEq R] exact equiv_trans h_mulStep (ih acc) /-- The `zipIdx` of a polynomial is the `zipIdx` of its trim followed by zero coefficients. -/ -lemma zipIdx_trim_append {R : Type*} [Ring R] [BEq R] [LawfulBEq R] +lemma zipIdx_trim_append {R : Type*} [Zero R] [BEq R] [LawfulBEq R] (p : CPolynomial.Raw R) : ∃ l, p.zipIdx.toList = p.trim.zipIdx.toList ++ l ∧ ∀ x ∈ l, x.1 = 0 := by have h_zipIdx : (p.zipIdx.toList.take p.trim.size) = (p.trim.zipIdx.toList) := by @@ -189,7 +190,7 @@ lemma zipIdx_trim_append {R : Type*} [Ring R] [BEq R] [LawfulBEq R] aesop /-- Multiplication by a trimmed polynomial is equivalent to multiplication by the original. -/ -lemma mul_trim_equiv [LawfulBEq R] (a b : CPolynomial.Raw R) : +lemma mul_trim_equiv [Semiring R] [BEq R] [LawfulBEq R] (a b : CPolynomial.Raw R) : a.mul b ≈ a.trim.mul b := by have h_zipIdx_split : ∃ l, a.zipIdx.toList = a.trim.zipIdx.toList ++ l ∧ ∀ x ∈ l, x.1 = 0 := by exact zipIdx_trim_append a @@ -207,7 +208,7 @@ lemma mul_trim_equiv [LawfulBEq R] (a b : CPolynomial.Raw R) : exact h₁.symm ▸ h₂.symm ▸ foldl_mulStep_zeros b acc l hl.2 /-- Multiplication is well-defined on the left with respect to equivalence. -/ -lemma mul_equiv [LawfulBEq R] (a₁ a₂ b : CPolynomial.Raw R) : +lemma mul_equiv [Semiring R] [BEq R] [LawfulBEq R] (a₁ a₂ b : CPolynomial.Raw R) : a₁ ≈ a₂ → a₁.mul b ≈ a₂.mul b := by intro h calc @@ -216,7 +217,7 @@ lemma mul_equiv [LawfulBEq R] (a₁ a₂ b : CPolynomial.Raw R) : _ ≈ a₂.mul b := equiv_symm (mul_trim_equiv a₂ b) /-- Multiplication is well-defined on the right with respect to equivalence. -/ -lemma mul_equiv₂ [LawfulBEq R] (a b₁ b₂ : CPolynomial.Raw R) : +lemma mul_equiv₂ [Semiring R] [BEq R] [LawfulBEq R] (a b₁ b₂ : CPolynomial.Raw R) : b₁ ≈ b₂ → a.mul b₁ ≈ a.mul b₂ := by -- By definition of multiplication, we can express `a.mul b₁` and `a.mul b₂` in terms of -- their sums of products of coefficients. @@ -241,10 +242,11 @@ lemma mul_equiv₂ [LawfulBEq R] (a b₁ b₂ : CPolynomial.Raw R) : end EquivalenceLemmas /-- Helper function showing addition descends to the quotient. -/ -def addDescending (p q : CPolynomial.Raw R) : QuotientCPolynomial R := +def addDescending [Semiring R] [BEq R] [LawfulBEq R] + (p q : CPolynomial.Raw R) : QuotientCPolynomial R := Quotient.mk _ (add p q) -lemma add_descends [LawfulBEq R] (a₁ b₁ a₂ b₂ : CPolynomial.Raw R) : +lemma add_descends [Semiring R] [BEq R] [LawfulBEq R] (a₁ b₁ a₂ b₂ : CPolynomial.Raw R) : equiv a₁ a₂ → equiv b₁ b₂ → addDescending a₁ b₁ = addDescending a₂ b₂ := by intros heq_a heq_b unfold addDescending @@ -259,15 +261,15 @@ lemma add_descends [LawfulBEq R] (a₁ b₁ a₂ b₂ : CPolynomial.Raw R) : /-- Addition on the quotient. -/ @[inline, specialize] -def add {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (p q : QuotientCPolynomial R) : +def add {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] (p q : QuotientCPolynomial R) : QuotientCPolynomial R := Quotient.lift₂ addDescending add_descends p q /-- Helper function showing scalar multiplication descends to the quotient. -/ -def smulDescending (r : R) (p : CPolynomial.Raw R) : QuotientCPolynomial R := +def smulDescending [Semiring R] (r : R) (p : CPolynomial.Raw R) : QuotientCPolynomial R := Quotient.mk _ (smul r p) -lemma smul_descends [LawfulBEq R] (r : R) (p₁ p₂ : CPolynomial.Raw R) : +lemma smul_descends [Semiring R] (r : R) (p₁ p₂ : CPolynomial.Raw R) : equiv p₁ p₂ → smulDescending r p₁ = smulDescending r p₂ := by unfold equiv smulDescending intro heq @@ -278,15 +280,16 @@ lemma smul_descends [LawfulBEq R] (r : R) (p₁ p₂ : CPolynomial.Raw R) : /-- Scalar multiplication on the quotient. -/ @[inline, specialize] -def smul {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (r : R) (p : QuotientCPolynomial R) : +def smul {R : Type*} [Semiring R] (r : R) (p : QuotientCPolynomial R) : QuotientCPolynomial R := Quotient.lift (smulDescending r) (smul_descends r) p /-- Helper function showing natural number scalar multiplication descends to the quotient. -/ -def nsmulDescending (n : ℕ) (p : CPolynomial.Raw R) : QuotientCPolynomial R := +def nsmulDescending [Semiring R] [BEq R] (n : ℕ) (p : CPolynomial.Raw R) : QuotientCPolynomial R := Quotient.mk _ (nsmul n p) -lemma nsmul_descends [LawfulBEq R] (n : ℕ) (p₁ p₂ : CPolynomial.Raw R) : +lemma nsmul_descends [Semiring R] [BEq R] [LawfulBEq R] (n : ℕ) + (p₁ p₂ : CPolynomial.Raw R) : equiv p₁ p₂ → nsmulDescending n p₁ = nsmulDescending n p₂ := by unfold equiv intro heq @@ -300,15 +303,17 @@ lemma nsmul_descends [LawfulBEq R] (n : ℕ) (p₁ p₂ : CPolynomial.Raw R) : /-- Natural number scalar multiplication on the quotient. -/ @[inline, specialize] -def nsmul {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (n : ℕ) (p : QuotientCPolynomial R) : +def nsmul {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] (n : ℕ) + (p : QuotientCPolynomial R) : QuotientCPolynomial R := Quotient.lift (nsmulDescending n) (nsmul_descends n) p /-- Helper function showing negation descends to the quotient. -/ -def negDescending (p : CPolynomial.Raw R) : QuotientCPolynomial R := +def negDescending [Zero R] [Neg R] (p : CPolynomial.Raw R) : QuotientCPolynomial R := Quotient.mk _ (neg p) -lemma neg_descends (a b : CPolynomial.Raw R) : equiv a b → negDescending a = negDescending b := by +lemma neg_descends [NegZeroClass R] (a b : CPolynomial.Raw R) : + equiv a b → negDescending a = negDescending b := by unfold equiv negDescending intros heq rw [Quotient.eq] @@ -319,14 +324,15 @@ lemma neg_descends (a b : CPolynomial.Raw R) : equiv a b → negDescending a = n /-- Negation on the quotient. -/ @[inline, specialize] -def neg {R : Type*} [Ring R] [BEq R] (p : QuotientCPolynomial R) : QuotientCPolynomial R := +def neg {R : Type*} [NegZeroClass R] (p : QuotientCPolynomial R) : QuotientCPolynomial R := Quotient.lift negDescending neg_descends p /-- Helper function showing subtraction descends to the quotient. -/ -def subDescending (p q : CPolynomial.Raw R) : QuotientCPolynomial R := +def subDescending [Ring R] [BEq R] [LawfulBEq R] + (p q : CPolynomial.Raw R) : QuotientCPolynomial R := Quotient.mk _ (sub p q) -lemma sub_descends [LawfulBEq R] (a₁ b₁ a₂ b₂ : CPolynomial.Raw R) : +lemma sub_descends [Ring R] [BEq R] [LawfulBEq R] (a₁ b₁ a₂ b₂ : CPolynomial.Raw R) : equiv a₁ a₂ → equiv b₁ b₂ → subDescending a₁ b₁ = subDescending a₂ b₂ := by unfold equiv subDescending intros heq_a heq_b @@ -348,10 +354,10 @@ def sub {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (p q : QuotientCPolynomial R) Quotient.lift₂ subDescending sub_descends p q /-- Helper function showing multiplication by `X^i` descends to the quotient. -/ -def mulPowXDescending (i : ℕ) (p : CPolynomial.Raw R) : QuotientCPolynomial R := +def mulPowXDescending [Zero R] (i : ℕ) (p : CPolynomial.Raw R) : QuotientCPolynomial R := Quotient.mk _ (mulPowX i p) -lemma mulPowX_descends [LawfulBEq R] (i : ℕ) (p₁ p₂ : CPolynomial.Raw R) : +lemma mulPowX_descends [Zero R] (i : ℕ) (p₁ p₂ : CPolynomial.Raw R) : equiv p₁ p₂ → mulPowXDescending i p₁ = mulPowXDescending i p₂ := by unfold mulPowXDescending intro heq @@ -361,19 +367,20 @@ lemma mulPowX_descends [LawfulBEq R] (i : ℕ) (p₁ p₂ : CPolynomial.Raw R) : /-- Multiplication by `X^i` on the quotient. -/ @[inline, specialize] -def mulPowX {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (i : ℕ) (p : QuotientCPolynomial R) : +def mulPowX {R : Type*} [Zero R] (i : ℕ) (p : QuotientCPolynomial R) : QuotientCPolynomial R := Quotient.lift (mulPowXDescending i) (mulPowX_descends i) p /-- Multiplication by `X` on the quotient (equivalent to `mulPowX 1`). -/ @[inline, specialize] -def mulX [LawfulBEq R] (p : QuotientCPolynomial R) : QuotientCPolynomial R := p.mulPowX 1 +def mulX [Zero R] (p : QuotientCPolynomial R) : QuotientCPolynomial R := p.mulPowX 1 /-- Helper function showing multiplication descends to the quotient. -/ -def mulDescending (p q : CPolynomial.Raw R) : QuotientCPolynomial R := +def mulDescending [Semiring R] [BEq R] [LawfulBEq R] + (p q : CPolynomial.Raw R) : QuotientCPolynomial R := Quotient.mk _ (mul p q) -lemma mul_descends [LawfulBEq R] (a₁ b₁ a₂ b₂ : CPolynomial.Raw R) : +lemma mul_descends [Semiring R] [BEq R] [LawfulBEq R] (a₁ b₁ a₂ b₂ : CPolynomial.Raw R) : equiv a₁ a₂ → equiv b₁ b₂ → mulDescending a₁ b₁ = mulDescending a₂ b₂ := by unfold mulDescending intros heq_a heq_b @@ -385,15 +392,16 @@ lemma mul_descends [LawfulBEq R] (a₁ b₁ a₂ b₂ : CPolynomial.Raw R) : /-- Multiplication on the quotient. -/ @[inline, specialize] -def mul {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (p q : QuotientCPolynomial R) : +def mul {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] (p q : QuotientCPolynomial R) : QuotientCPolynomial R := Quotient.lift₂ mulDescending mul_descends p q /-- Helper function showing exponentiation descends to the quotient. -/ -def powDescending (p : CPolynomial.Raw R) (n : ℕ) : QuotientCPolynomial R := +def powDescending [Semiring R] [BEq R] (p : CPolynomial.Raw R) (n : ℕ) : + QuotientCPolynomial R := Quotient.mk _ (pow p n) -lemma pow_descends [LawfulBEq R] (n : ℕ) (p₁ p₂ : CPolynomial.Raw R) : +lemma pow_descends [Semiring R] [BEq R] [LawfulBEq R] (n : ℕ) (p₁ p₂ : CPolynomial.Raw R) : equiv p₁ p₂ → powDescending p₁ n = powDescending p₂ n := by intro heq unfold powDescending @@ -414,30 +422,36 @@ lemma pow_descends [LawfulBEq R] (n : ℕ) (p₁ p₂ : CPolynomial.Raw R) : /-- Exponentiation on the quotient. -/ @[inline, specialize] -def pow {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (p : QuotientCPolynomial R) (n : ℕ) : +def pow {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] + (p : QuotientCPolynomial R) (n : ℕ) : QuotientCPolynomial R := Quotient.lift (fun p => powDescending p n) (pow_descends n) p -- TODO: div/field operations? -instance : Zero (QuotientCPolynomial R) := ⟨Quotient.mk _ #[]⟩ -instance : One (QuotientCPolynomial R) := ⟨Quotient.mk _ (CPolynomial.Raw.C 1)⟩ -instance [LawfulBEq R] : Add (QuotientCPolynomial R) := ⟨QuotientCPolynomial.add⟩ -instance [LawfulBEq R] : SMul R (QuotientCPolynomial R) := ⟨smul⟩ -instance [LawfulBEq R] : SMul ℕ (QuotientCPolynomial R) := ⟨nsmul⟩ -instance : Neg (QuotientCPolynomial R) := ⟨neg⟩ -instance [LawfulBEq R] : Sub (QuotientCPolynomial R) := ⟨sub⟩ -instance [LawfulBEq R] : Mul (QuotientCPolynomial R) := ⟨mul⟩ -instance [LawfulBEq R] : Pow (QuotientCPolynomial R) Nat := ⟨pow⟩ -instance : NatCast (QuotientCPolynomial R) := ⟨fun n => Quotient.mk _ (CPolynomial.Raw.C (n : R))⟩ -instance : IntCast (QuotientCPolynomial R) := ⟨fun n => Quotient.mk _ (CPolynomial.Raw.C (n : R))⟩ +instance [Zero R] : Zero (QuotientCPolynomial R) := ⟨Quotient.mk _ #[]⟩ +instance [Zero R] [One R] : One (QuotientCPolynomial R) := ⟨Quotient.mk _ (CPolynomial.Raw.C 1)⟩ +instance [Semiring R] [BEq R] [LawfulBEq R] : Add (QuotientCPolynomial R) := + ⟨QuotientCPolynomial.add⟩ +instance [Semiring R] : SMul R (QuotientCPolynomial R) := ⟨smul⟩ +instance [Semiring R] [BEq R] [LawfulBEq R] : SMul ℕ (QuotientCPolynomial R) := ⟨nsmul⟩ +instance [NegZeroClass R] : Neg (QuotientCPolynomial R) := ⟨neg⟩ +instance [Ring R] [BEq R] [LawfulBEq R] : Sub (QuotientCPolynomial R) := ⟨sub⟩ +instance [Semiring R] [BEq R] [LawfulBEq R] : Mul (QuotientCPolynomial R) := ⟨mul⟩ +instance [Semiring R] [BEq R] [LawfulBEq R] : Pow (QuotientCPolynomial R) Nat := ⟨pow⟩ +instance [Zero R] [NatCast R] : NatCast (QuotientCPolynomial R) := + ⟨fun n => Quotient.mk _ (CPolynomial.Raw.C (n : R))⟩ +instance [Zero R] [IntCast R] : IntCast (QuotientCPolynomial R) := + ⟨fun n => Quotient.mk _ (CPolynomial.Raw.C (n : R))⟩ -- instance [Field R] : Div (QuotientCPolynomial R) := ⟨div⟩ -- instance [Field R] : Mod (QuotientCPolynomial R) := ⟨mod⟩ -section AddCommGroup +section AddCommMonoid + +variable [Semiring R] [BEq R] [LawfulBEq R] @[grind =_] -lemma add_assoc [LawfulBEq R] : ∀ (a b c : QuotientCPolynomial R), a + b + c = a + (b + c) := by +lemma add_assoc : ∀ (a b c : QuotientCPolynomial R), a + b + c = a + (b + c) := by intro a b c refine Quotient.inductionOn₃ a b c ?_ intro p q r; clear a b c @@ -446,7 +460,7 @@ lemma add_assoc [LawfulBEq R] : ∀ (a b c : QuotientCPolynomial R), a + b + c = apply CPolynomial.Raw.add_assoc @[simp] -lemma zero_add_equiv [LawfulBEq R] (p : CPolynomial.Raw R) : 0 + p ≈ p := by +lemma zero_add_equiv (p : CPolynomial.Raw R) : 0 + p ≈ p := by intro i change ((0 : CPolynomial.Raw R).add p).coeff i = p.coeff i unfold CPolynomial.Raw.add @@ -455,7 +469,7 @@ lemma zero_add_equiv [LawfulBEq R] (p : CPolynomial.Raw R) : 0 + p ≈ p := by simp @[simp] -lemma zero_add [LawfulBEq R] : ∀ (a : QuotientCPolynomial R), 0 + a = a := by +lemma zero_add : ∀ (a : QuotientCPolynomial R), 0 + a = a := by intros a refine Quotient.inductionOn a ?_ intro p; clear a @@ -463,7 +477,7 @@ lemma zero_add [LawfulBEq R] : ∀ (a : QuotientCPolynomial R), 0 + a = a := by apply zero_add_equiv @[simp] -lemma add_zero [LawfulBEq R] : ∀ (a : QuotientCPolynomial R), a + 0 = a := by +lemma add_zero : ∀ (a : QuotientCPolynomial R), a + 0 = a := by intros a refine Quotient.inductionOn a ?_ intro p; clear a @@ -475,7 +489,7 @@ lemma add_zero [LawfulBEq R] : ∀ (a : QuotientCPolynomial R), a + 0 = a := by simp @[grind =>] -lemma add_comm [LawfulBEq R] : ∀ (a b : QuotientCPolynomial R), a + b = b + a := by +lemma add_comm : ∀ (a b : QuotientCPolynomial R), a + b = b + a := by intro a b refine Quotient.inductionOn₂ a b ?_ intros p q; clear a b @@ -484,16 +498,7 @@ lemma add_comm [LawfulBEq R] : ∀ (a b : QuotientCPolynomial R), a + b = b + a apply CPolynomial.Raw.add_comm @[simp] -lemma neg_add_cancel [LawfulBEq R] : ∀ (a : QuotientCPolynomial R), -a + a = 0 := by - intros a - refine Quotient.inductionOn a ?_ - intro p; clear a - apply Quotient.sound - apply eq_to_equiv - apply CPolynomial.Raw.neg_add_cancel - -@[simp] -lemma nsmul_zero [LawfulBEq R] : ∀ (x : QuotientCPolynomial R), +lemma nsmul_zero : ∀ (x : QuotientCPolynomial R), QuotientCPolynomial.nsmul 0 x = 0 := by intros x refine Quotient.inductionOn x ?_ @@ -503,7 +508,7 @@ lemma nsmul_zero [LawfulBEq R] : ∀ (x : QuotientCPolynomial R), apply CPolynomial.Raw.nsmul_zero @[grind =>] -lemma nsmul_succ [LawfulBEq R] : ∀ (n : ℕ) (x : QuotientCPolynomial R), +lemma nsmul_succ : ∀ (n : ℕ) (x : QuotientCPolynomial R), QuotientCPolynomial.nsmul (n + 1) x = QuotientCPolynomial.nsmul n x + x := by intro n x refine Quotient.inductionOn x ?_ @@ -512,8 +517,32 @@ lemma nsmul_succ [LawfulBEq R] : ∀ (n : ℕ) (x : QuotientCPolynomial R), apply eq_to_equiv apply CPolynomial.Raw.nsmul_succ +instance : AddCommMonoid (QuotientCPolynomial R) where + add_assoc := add_assoc + zero_add := zero_add + add_zero := add_zero + add_comm := add_comm + nsmul := nsmul + nsmul_zero := nsmul_zero + nsmul_succ := nsmul_succ + +end AddCommMonoid + +section AddCommGroup + +variable [Ring R] [BEq R] [LawfulBEq R] + +@[simp] +lemma neg_add_cancel : ∀ (a : QuotientCPolynomial R), -a + a = 0 := by + intros a + refine Quotient.inductionOn a ?_ + intro p; clear a + apply Quotient.sound + apply eq_to_equiv + apply CPolynomial.Raw.neg_add_cancel + @[grind =] -lemma sub_eq_add_neg [LawfulBEq R] : ∀ (a b : QuotientCPolynomial R), a - b = a + -b := by +lemma sub_eq_add_neg : ∀ (a b : QuotientCPolynomial R), a - b = a + -b := by intro a b refine Quotient.inductionOn₂ a b ?_ intros p q; clear a b @@ -521,25 +550,18 @@ lemma sub_eq_add_neg [LawfulBEq R] : ∀ (a b : QuotientCPolynomial R), a - b = apply eq_to_equiv rfl -instance [LawfulBEq R] : AddCommGroup (QuotientCPolynomial R) where - add_assoc := add_assoc - zero_add := zero_add - add_zero := add_zero - add_comm := add_comm +instance : AddCommGroup (QuotientCPolynomial R) where neg_add_cancel := neg_add_cancel - nsmul := nsmul - nsmul_zero := nsmul_zero - nsmul_succ := nsmul_succ zsmul := zsmulRec sub_eq_add_neg := sub_eq_add_neg end AddCommGroup section Semiring -variable [LawfulBEq R] -lemma mul_assoc {R : Type*} [Ring R] [BEq R] [LawfulBEq R] - (a b c : QuotientCPolynomial R) : +variable [Semiring R] [BEq R] [LawfulBEq R] + +lemma mul_assoc (a b c : QuotientCPolynomial R) : a * b * c = a * (b * c) := by refine Quotient.inductionOn₃ a b c ?_ intro p q r @@ -614,8 +636,7 @@ lemma const_sum (r s : R) : (C r).add (C s) ≈ C (r + s) := by /- x^(n+1) = x * x^n for QuotientCPolynomial -/ -lemma pow_succ_left {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (n : ℕ) - (x : QuotientCPolynomial R) : +lemma pow_succ_left (n : ℕ) (x : QuotientCPolynomial R) : x.pow (n + 1) = x * x.pow n := by refine Quotient.inductionOn x ?_ intro p @@ -629,8 +650,7 @@ lemma pow_succ_left {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (n : ℕ) /- x commutes with x^n -/ -lemma commute_pow_self {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (n : ℕ) - (x : QuotientCPolynomial R) : +lemma commute_pow_self (n : ℕ) (x : QuotientCPolynomial R) : x * x.pow n = x.pow n * x := by induction' n with n ih generalizing x all_goals generalize_proofs at * @@ -656,7 +676,7 @@ lemma npow_succ : ∀ (n : ℕ) (x : QuotientCPolynomial R), x.pow (n + 1) = x.p The semiring structure is inherited from the coefficient-wise operations on arrays, with addition and multiplication defined via the standard polynomial operations. -/ -instance [Semiring R] [LawfulBEq R] : Semiring (QuotientCPolynomial R) where +instance : Semiring (QuotientCPolynomial R) where mul_assoc := mul_assoc one_mul := one_mul mul_one := mul_one @@ -679,9 +699,9 @@ end Semiring section CommSemiring -variable {R : Type*} [CommRing R] [BEq R] +variable [CommSemiring R] [BEq R] [LawfulBEq R] -lemma mul_comm [LawfulBEq R]: ∀ (a b : QuotientCPolynomial R), a * b = b * a := by +lemma mul_comm : ∀ (a b : QuotientCPolynomial R), a * b = b * a := by intro a b refine Quotient.inductionOn₂ a b ?_ intros p q; clear a b @@ -693,14 +713,16 @@ lemma mul_comm [LawfulBEq R]: ∀ (a b : QuotientCPolynomial R), a * b = b * a : Commutativity follows from the commutativity of multiplication in the base ring. -/ -instance [CommRing R] [LawfulBEq R] : CommSemiring (QuotientCPolynomial R) where +instance : CommSemiring (QuotientCPolynomial R) where mul_comm := mul_comm end CommSemiring section Ring -lemma zsmul_zero' [LawfulBEq R] : ∀ (a : QuotientCPolynomial R), zsmulRec nsmulRec 0 a = 0 := by +variable [Ring R] [BEq R] [LawfulBEq R] + +lemma zsmul_zero' : ∀ (a : QuotientCPolynomial R), zsmulRec nsmulRec 0 a = 0 := by intro a; simp [zsmulRec]; simp [nsmulRec] /-- `QuotientCPolynomial R` forms a ring when `R` is a ring. @@ -708,7 +730,7 @@ lemma zsmul_zero' [LawfulBEq R] : ∀ (a : QuotientCPolynomial R), zsmulRec nsmu The ring structure extends the semiring structure with negation and subtraction. Most of the structure is already provided by the `Semiring` instance. -/ -instance [LawfulBEq R] : Ring (QuotientCPolynomial R) where +instance : Ring (QuotientCPolynomial R) where sub_eq_add_neg := by intro a b; (grind) zsmul := zsmulRec zsmul_zero' := zsmul_zero' @@ -729,13 +751,13 @@ end Ring section CommRing -variable {R : Type*} [CommRing R] [BEq R] +variable [CommRing R] [BEq R] [LawfulBEq R] /-- `QuotientCPolynomial R` forms a commutative ring when `R` is a commutative ring. This combines the `CommSemiring` and `Ring` structures. -/ -instance [CommRing R] [BEq R] [LawfulBEq R] : CommRing (QuotientCPolynomial R) where +instance : CommRing (QuotientCPolynomial R) where -- All structure inherited from `CommSemiring` and `Ring` instances end CommRing diff --git a/CompPoly/Univariate/QuotientEquiv.lean b/CompPoly/Univariate/QuotientEquiv.lean index d8bca4f2..ef6dfa08 100644 --- a/CompPoly/Univariate/QuotientEquiv.lean +++ b/CompPoly/Univariate/QuotientEquiv.lean @@ -30,9 +30,8 @@ namespace QuotientCPolynomial open Raw Trim -variable {R : Type*} [Ring R] [BEq R] [LawfulBEq R] +variable {R : Type*} [Semiring R] -omit [BEq R] [LawfulBEq R] in /-- Well-definedness: equivalent raw polynomials map to the same `Polynomial`. -/ private theorem toPoly_resp (p q : CPolynomial.Raw R) (h : p ≈ q) : p.toPoly = q.toPoly := by @@ -54,7 +53,6 @@ noncomputable def toPoly (p : QuotientCPolynomial R) : Polynomial R := def ofPoly (p : Polynomial R) : QuotientCPolynomial R := Quotient.mk _ (Polynomial.toImpl p) -omit [LawfulBEq R] in /-- Round-trip identity: `toPoly ∘ ofPoly = id`. -/ @[simp] theorem toPoly_ofPoly (p : Polynomial R) : toPoly (ofPoly p) = p := by @@ -62,7 +60,8 @@ theorem toPoly_ofPoly (p : Polynomial R) : toPoly (ofPoly p) = p := by /-- Round-trip identity: `ofPoly ∘ toPoly = id`. -/ @[simp] -theorem ofPoly_toPoly (q : QuotientCPolynomial R) : ofPoly (toPoly q) = q := by +theorem ofPoly_toPoly [BEq R] [LawfulBEq R] (q : QuotientCPolynomial R) : + ofPoly (toPoly q) = q := by refine Quotient.inductionOn q ?_ intro p simp only [toPoly, ofPoly, Quotient.lift_mk] @@ -77,7 +76,7 @@ theorem ofPoly_toPoly (q : QuotientCPolynomial R) : ofPoly (toPoly q) = q := by The forward map is `toPoly` (quotient-lift of `Raw.toPoly`); the inverse is `ofPoly` (coefficient extraction via `Polynomial.toImpl`). Preserves both addition and multiplication. -/ -noncomputable def ringEquiv : QuotientCPolynomial R ≃+* Polynomial R where +noncomputable def ringEquiv [BEq R] [LawfulBEq R] : QuotientCPolynomial R ≃+* Polynomial R where toFun := toPoly invFun := ofPoly left_inv := ofPoly_toPoly diff --git a/CompPoly/Univariate/Raw/Core.lean b/CompPoly/Univariate/Raw/Core.lean index 599bea71..633e74d0 100644 --- a/CompPoly/Univariate/Raw/Core.lean +++ b/CompPoly/Univariate/Raw/Core.lean @@ -42,18 +42,15 @@ variable {Q : Type*} section Foundations -variable [Semiring R] [BEq R] -variable [Semiring Q] - /-- The coefficient of `X^i` in the polynomial. Returns `0` if `i` is out of bounds. -/ @[reducible] -def coeff (p : CPolynomial.Raw R) (i : ℕ) : R := p.getD i 0 +def coeff [Zero R] (p : CPolynomial.Raw R) (i : ℕ) : R := p.getD i 0 /-- The constant polynomial `C r`. -/ def C (r : R) : CPolynomial.Raw R := #[r] /-- The variable `X`. -/ -def X : CPolynomial.Raw R := #[0, 1] +def X [Zero R] [One R] : CPolynomial.Raw R := #[0, 1] /-- Construct a monomial `c * X^n` as a `CPolynomial.Raw R`. @@ -62,22 +59,22 @@ def X : CPolynomial.Raw R := #[0, 1] Note: If `c = 0`, this returns `#[]` (the zero polynomial). -/ -def monomial [DecidableEq R] (n : ℕ) (c : R) : CPolynomial.Raw R := +def monomial [Zero R] [DecidableEq R] (n : ℕ) (c : R) : CPolynomial.Raw R := if c = 0 then #[] else .mk (Array.replicate n 0 ++ #[c]) /-- Return the index of the last non-zero coefficient of a `CPolynomial.Raw` -/ -def lastNonzero (p : CPolynomial.Raw R) : Option (Fin p.size) := +def lastNonzero [Zero R] [BEq R] (p : CPolynomial.Raw R) : Option (Fin p.size) := p.findIdxRev? (· != 0) /-- Remove trailing zeroes from a `CPolynomial.Raw`. Requires `BEq` to check if the coefficients are zero. -/ -def trim (p : CPolynomial.Raw R) : CPolynomial.Raw R := +def trim [Zero R] [BEq R] (p : CPolynomial.Raw R) : CPolynomial.Raw R := match p.lastNonzero with | none => #[] | some i => p.extract 0 (i.val + 1) /-- Return the degree of a `CPolynomial.Raw`. -/ -def degree (p : CPolynomial.Raw R) : WithBot ℕ := +def degree [Zero R] [BEq R] (p : CPolynomial.Raw R) : WithBot ℕ := match p.lastNonzero with | none => ⊥ | some i => i.val @@ -87,24 +84,30 @@ def degree (p : CPolynomial.Raw R) : WithBot ℕ := Returns the degree as a natural number. For the zero polynomial, returns `0`. This matches Mathlib's `Polynomial.natDegree` API. -/ -def natDegree (p : CPolynomial.Raw R) : ℕ := +def natDegree [Zero R] [BEq R] (p : CPolynomial.Raw R) : ℕ := match p.lastNonzero with | none => 0 | some i => i.val /-- Return the leading coefficient of a `CPolynomial.Raw` as the last coefficient of the trimmed array, or `0` if the trimmed array is empty. -/ -def leadingCoeff (p : CPolynomial.Raw R) : R := p.trim.getLastD 0 +def leadingCoeff [Zero R] [BEq R] (p : CPolynomial.Raw R) : R := p.trim.getLastD 0 + +/-- Semantic canonicality for raw coefficient arrays: a polynomial is canonical iff its +last stored coefficient, when present, is nonzero. This invariant is independent of any +particular `BEq` instance. -/ +def IsCanonical [Zero R] (p : CPolynomial.Raw R) : Prop := + ∀ hp : p.size > 0, p.getLast hp ≠ 0 /-- A polynomial is canonical if it has no trailing zeros, i.e. `p.trim = p`. -/ -def canonical (p : CPolynomial.Raw R) : Prop := p.trim = p +def canonical [Zero R] [BEq R] (p : CPolynomial.Raw R) : Prop := p.trim = p /- Lemmas about trimming and canonical forms. Central results: `trim_twice`, `canonical_iff`, `eq_of_equiv`, `canonical_ext`. -/ namespace Trim /-- If all coefficients are zero, `lastNonzero` is `none`. -/ -theorem lastNonzero_none [LawfulBEq R] {p : CPolynomial.Raw R} : +theorem lastNonzero_none [Zero R] [BEq R] [LawfulBEq R] {p : CPolynomial.Raw R} : (∀ i, (hi : i < p.size) → p[i] = 0) → p.lastNonzero = none := by intro h apply Array.findIdxRev?_eq_none @@ -113,12 +116,13 @@ theorem lastNonzero_none [LawfulBEq R] {p : CPolynomial.Raw R} : apply_assumption /-- If there is a non-zero coefficient, `lastNonzero` is `some`. -/ -theorem lastNonzero_some [LawfulBEq R] {p : CPolynomial.Raw R} {i} (hi : i < p.size) +theorem lastNonzero_some [Zero R] [BEq R] [LawfulBEq R] + {p : CPolynomial.Raw R} {i} (hi : i < p.size) (h : p[i] ≠ 0) : ∃ k, p.lastNonzero = some k := Array.findIdxRev?_eq_some ⟨i, hi, bne_iff_ne.mpr h⟩ /-- `lastNonzero` returns the largest index with a non-zero coefficient. -/ -theorem lastNonzero_spec [LawfulBEq R] {p : CPolynomial.Raw R} {k} : +theorem lastNonzero_spec [Zero R] [BEq R] [LawfulBEq R] {p : CPolynomial.Raw R} {k} : p.lastNonzero = some k → p[k] ≠ 0 ∧ (∀ j, (hj : j < p.size) → j > k → p[j] = 0) := by intro (h : p.lastNonzero = some k) @@ -131,11 +135,11 @@ theorem lastNonzero_spec [LawfulBEq R] {p : CPolynomial.Raw R} {k} : rwa [bne_iff_ne, ne_eq, not_not] at h /-- The property that an index is the last non-zero coefficient. -/ -def lastNonzeroProp {p : CPolynomial.Raw R} (k : Fin p.size) : Prop := +def lastNonzeroProp [Zero R] {p : CPolynomial.Raw R} (k : Fin p.size) : Prop := p[k] ≠ 0 ∧ (∀ j, (hj : j < p.size) → j > k → p[j] = 0) /-- The last non-zero index is unique. -/ -lemma lastNonzero_unique {p : CPolynomial.Raw Q} {k k' : Fin p.size} : +lemma lastNonzero_unique [Zero Q] {p : CPolynomial.Raw Q} {k k' : Fin p.size} : lastNonzeroProp k → lastNonzeroProp k' → k = k' := by suffices weaker : ∀ k k', lastNonzeroProp k → lastNonzeroProp k' → k ≤ k' by intro h h' @@ -146,7 +150,7 @@ lemma lastNonzero_unique {p : CPolynomial.Raw Q} {k k' : Fin p.size} : contradiction /-- Characterization of `lastNonzero` via `lastNonzeroProp`. -/ -theorem lastNonzero_some_iff [LawfulBEq R] {p : CPolynomial.Raw R} {k} : +theorem lastNonzero_some_iff [Zero R] [BEq R] [LawfulBEq R] {p : CPolynomial.Raw R} {k} : p.lastNonzero = some k ↔ (p[k] ≠ 0 ∧ (∀ j, (hj : j < p.size) → j > k → p[j] = 0)) := by constructor · apply lastNonzero_spec @@ -162,7 +166,7 @@ theorem lastNonzero_some_iff [LawfulBEq R] {p : CPolynomial.Raw R} {k} : | case2 p k h_some h_nonzero h_max => ... ``` -/ -theorem lastNonzero_induct [LawfulBEq R] {motive : CPolynomial.Raw R → Prop} +theorem lastNonzero_induct [Zero R] [BEq R] [LawfulBEq R] {motive : CPolynomial.Raw R → Prop} (case1 : ∀ p, p.lastNonzero = none → (∀ i, (hi : i < p.size) → p[i] = 0) → motive p) (case2 : ∀ p : CPolynomial.Raw R, ∀ k : Fin p.size, p.lastNonzero = some k → p[k] ≠ 0 → (∀ j : ℕ, (hj : j < p.size) → j > k → p[j] = 0) → motive p) @@ -181,7 +185,7 @@ theorem lastNonzero_induct [LawfulBEq R] {motive : CPolynomial.Raw R → Prop} | case2 p k h_extract h_nonzero h_max => ... ``` -/ -theorem induct [LawfulBEq R] {motive : CPolynomial.Raw R → Prop} +theorem induct [Zero R] [BEq R] [LawfulBEq R] {motive : CPolynomial.Raw R → Prop} (case1 : ∀ p, p.trim = #[] → (∀ i, (hi : i < p.size) → p[i] = 0) → motive p) (case2 : ∀ p : CPolynomial.Raw R, ∀ k : Fin p.size, p.trim = p.extract 0 (k + 1) → p[k] ≠ 0 → (∀ j : ℕ, (hj : j < p.size) → j > k → p[j] = 0) → motive p) @@ -198,7 +202,7 @@ theorem induct [LawfulBEq R] {motive : CPolynomial.Raw R → Prop} rcases (Trim.elim p) with ⟨ h_empty, h_all_zero ⟩ | ⟨ k, h_extract, h_nonzero, h_max ⟩ ``` -/ -theorem elim [LawfulBEq R] (p : CPolynomial.Raw R) : +theorem elim [Zero R] [BEq R] [LawfulBEq R] (p : CPolynomial.Raw R) : (p.trim = #[] ∧ (∀ i, (hi : i < p.size) → p[i] = 0)) ∨ (∃ k : Fin p.size, p.trim = p.extract 0 (k + 1) @@ -207,21 +211,24 @@ theorem elim [LawfulBEq R] (p : CPolynomial.Raw R) : | case1 p h_empty h_all_zero => left; exact ⟨h_empty, h_all_zero⟩ | case2 p k h_extract h_nonzero h_max => right; exact ⟨k, h_extract, h_nonzero, h_max⟩ -theorem size_eq_degree_plus_one (p : CPolynomial.Raw R) (h_trim: p.trim ≠ (mk #[])) : +theorem size_eq_degree_plus_one [Zero R] [BEq R] + (p : CPolynomial.Raw R) (h_trim : p.trim ≠ (mk #[])) : p.trim.size = p.degree + 1 := by unfold trim degree match h : p.lastNonzero with | none => exfalso; unfold trim at h_trim; rw [h] at h_trim; contradiction | some i => simp [Fin.is_lt] -theorem size_eq_natDegree_plus_one (p : CPolynomial.Raw R) (h_trim: p.trim ≠ (mk #[])) : +theorem size_eq_natDegree_plus_one [Zero R] [BEq R] + (p : CPolynomial.Raw R) (h_trim : p.trim ≠ (mk #[])) : p.trim.size = p.natDegree + 1 := by unfold trim natDegree match h : p.lastNonzero with | none => exfalso; unfold trim at h_trim; rw [h] at h_trim; contradiction | some i => simp [Fin.is_lt] -theorem size_eq_natDegree_of_zero (p : CPolynomial.Raw R) (h_trim: p.trim = (mk #[])) : +theorem size_eq_natDegree_of_zero [Zero R] [BEq R] + (p : CPolynomial.Raw R) (h_trim : p.trim = (mk #[])) : p.trim.size = p.natDegree := by unfold trim natDegree match h : p.lastNonzero with @@ -231,7 +238,7 @@ theorem size_eq_natDegree_of_zero (p : CPolynomial.Raw R) (h_trim: p.trim = (mk rw [h] at h_trim; have h_size := congrArg Array.size h_trim simp [Array.size_extract, Nat.succ_le_of_lt i.is_lt] at h_size -theorem size_le_size (p : CPolynomial.Raw R) : p.trim.size ≤ p.size := by +theorem size_le_size [Zero R] [BEq R] (p : CPolynomial.Raw R) : p.trim.size ≤ p.size := by unfold trim match h : p.lastNonzero with | none => simp @@ -239,7 +246,8 @@ theorem size_le_size (p : CPolynomial.Raw R) : p.trim.size ≤ p.size := by attribute [simp] Array.getElem?_eq_none -theorem coeff_eq_getElem_of_lt [LawfulBEq R] {p : CPolynomial.Raw R} {i} (hi : i < p.size) : +theorem coeff_eq_getElem_of_lt [Zero R] [BEq R] [LawfulBEq R] + {p : CPolynomial.Raw R} {i} (hi : i < p.size) : p.trim.coeff i = p[i] := by induction p using induct with | case1 p h_empty h_all_zero => @@ -257,7 +265,8 @@ theorem coeff_eq_getElem_of_lt [LawfulBEq R] {p : CPolynomial.Raw R} {i} (hi : i rw [Array.getElem?_eq_getElem hik', Option.getD_some, Array.getElem_extract] simp only [zero_add] -theorem coeff_eq_coeff [LawfulBEq R] (p : CPolynomial.Raw R) (i : ℕ) : +theorem coeff_eq_coeff [Zero R] [BEq R] [LawfulBEq R] + (p : CPolynomial.Raw R) (i : ℕ) : p.trim.coeff i = p.coeff i := by rcases (Nat.lt_or_ge i p.size) with hi | hi · rw [coeff_eq_getElem_of_lt hi] @@ -265,21 +274,21 @@ theorem coeff_eq_coeff [LawfulBEq R] (p : CPolynomial.Raw R) (i : ℕ) : · have hi' : i ≥ p.trim.size := by linarith [size_le_size p] simp [hi, hi'] -lemma coeff_eq_getElem {p : CPolynomial.Raw Q} {i} (hp : i < p.size) : +lemma coeff_eq_getElem [Zero Q] {p : CPolynomial.Raw Q} {i} (hp : i < p.size) : p.coeff i = p[i] := by simp [hp] /-- Equivalence relation: two polynomials are equivalent if all coefficients agree. -/ -def equiv (p q : CPolynomial.Raw R) : Prop := +def equiv [Zero R] (p q : CPolynomial.Raw R) : Prop := ∀ i, p.coeff i = q.coeff i -lemma coeff_eq_zero {p : CPolynomial.Raw Q} : +lemma coeff_eq_zero [Zero Q] {p : CPolynomial.Raw Q} : (∀ i, (hi : i < p.size) → p[i] = 0) ↔ ∀ i, p.coeff i = 0 := by constructor <;> intro h i · cases Nat.lt_or_ge i p.size <;> simp [*] · intro hi; specialize h i; simp [hi] at h; assumption -lemma eq_degree_of_equiv [LawfulBEq R] {p q : CPolynomial.Raw R} : +lemma eq_degree_of_equiv [Zero R] [BEq R] [LawfulBEq R] {p q : CPolynomial.Raw R} : equiv p q → p.degree = q.degree := by unfold equiv degree intro h_equiv @@ -310,7 +319,8 @@ lemma eq_degree_of_equiv [LawfulBEq R] {p q : CPolynomial.Raw R} : lastNonzero_some_iff.mpr ⟨ h_nonzero_q, h_max_q ⟩ rw [h_some_p, h_some_q] -theorem eq_of_equiv [LawfulBEq R] {p q : CPolynomial.Raw R} : equiv p q → p.trim = q.trim := by +theorem eq_of_equiv [Zero R] [BEq R] [LawfulBEq R] {p q : CPolynomial.Raw R} : + equiv p q → p.trim = q.trim := by unfold equiv intro h ext @@ -332,26 +342,30 @@ theorem eq_of_equiv [LawfulBEq R] {p q : CPolynomial.Raw R} : equiv p q → p.tr · rw [← coeff_eq_getElem, ← coeff_eq_getElem] rw [coeff_eq_coeff, coeff_eq_coeff, h _] -theorem trim_equiv [LawfulBEq R] (p : CPolynomial.Raw R) : equiv p.trim p := by +theorem trim_equiv [Zero R] [BEq R] [LawfulBEq R] (p : CPolynomial.Raw R) : + equiv p.trim p := by apply coeff_eq_coeff -theorem trim_twice [LawfulBEq R] (p : CPolynomial.Raw R) : p.trim.trim = p.trim := by +theorem trim_twice [Zero R] [BEq R] [LawfulBEq R] (p : CPolynomial.Raw R) : + p.trim.trim = p.trim := by apply eq_of_equiv apply trim_equiv -theorem canonical_empty : (mk (R:=R) #[]).trim = #[] := by +theorem canonical_empty [Zero R] [BEq R] : (mk (R := R) #[]).trim = #[] := by have : (mk (R:=R) #[]).lastNonzero = none := by simp [lastNonzero] apply Array.findIdxRev?_empty_none rfl rw [trim, this] -theorem canonical_of_size_zero {p : CPolynomial.Raw R} : p.size = 0 → p.trim = p := by +theorem canonical_of_size_zero [Zero R] [BEq R] {p : CPolynomial.Raw R} : + p.size = 0 → p.trim = p := by intro h suffices h_empty : p = #[] by rw [h_empty]; exact canonical_empty exact Array.eq_empty_of_size_eq_zero h -theorem canonical_nonempty_iff [LawfulBEq R] {p : CPolynomial.Raw R} (hp : p.size > 0) : +theorem canonical_nonempty_iff [Zero R] [BEq R] [LawfulBEq R] + {p : CPolynomial.Raw R} (hp : p.size > 0) : p.trim = p ↔ p.lastNonzero = some ⟨ p.size - 1, Nat.pred_lt_self hp ⟩ := by unfold trim induction p using lastNonzero_induct with @@ -376,7 +390,8 @@ theorem canonical_nonempty_iff [LawfulBEq R] {p : CPolynomial.Raw R} (hp : p.siz right exact le_refl _ -theorem lastNonzero_last_iff [LawfulBEq R] {p : CPolynomial.Raw R} (hp : p.size > 0) : +theorem lastNonzero_last_iff [Zero R] [BEq R] [LawfulBEq R] + {p : CPolynomial.Raw R} (hp : p.size > 0) : p.lastNonzero = some ⟨ p.size - 1, Nat.pred_lt_self hp ⟩ ↔ p.getLast hp ≠ 0 := by induction p using lastNonzero_induct with | case1 => simp [Array.getLast, *] @@ -396,8 +411,8 @@ theorem lastNonzero_last_iff [LawfulBEq R] {p : CPolynomial.Raw R} (hp : p.size have : k ≥ p.size := Nat.le_of_pred_lt h_gt linarith -theorem canonical_iff [LawfulBEq R] {p : CPolynomial.Raw R} : - p.trim = p ↔ ∀ hp : p.size > 0, p.getLast hp ≠ 0 := by +theorem canonical_iff [Zero R] [BEq R] [LawfulBEq R] {p : CPolynomial.Raw R} : + p.trim = p ↔ IsCanonical p := by constructor · intro h hp rwa [← lastNonzero_last_iff hp, ← canonical_nonempty_iff hp] @@ -407,15 +422,39 @@ theorem canonical_iff [LawfulBEq R] {p : CPolynomial.Raw R} : · rw [canonical_nonempty_iff hp, lastNonzero_last_iff hp] exact h hp +theorem isCanonical_empty [Zero R] : IsCanonical (mk (R := R) #[]) := by + intro hp + simp at hp + +theorem isCanonical_of_size_zero [Zero R] {p : CPolynomial.Raw R} (hp : p.size = 0) : + IsCanonical p := by + intro hPos + simp [hp] at hPos + +theorem trim_eq_of_isCanonical [Zero R] [BEq R] [LawfulBEq R] + {p : CPolynomial.Raw R} (hp : IsCanonical p) : + p.trim = p := + canonical_iff.mpr hp + +theorem isCanonical_of_trim_eq [Zero R] [BEq R] [LawfulBEq R] + {p : CPolynomial.Raw R} (hp : p.trim = p) : + IsCanonical p := + canonical_iff.mp hp + +theorem isCanonical_trim [Zero R] [BEq R] [LawfulBEq R] + (p : CPolynomial.Raw R) : IsCanonical p.trim := + isCanonical_of_trim_eq (trim_twice p) + @[grind =] -lemma push_trim [LawfulBEq R] (arr : Array R) (c : R) : +lemma push_trim [Zero R] [BEq R] [LawfulBEq R] (arr : Array R) (c : R) : ¬c = 0 → trim (arr.push c) = arr.push c := by rw [Trim.canonical_iff] intros h_c hp simp [Array.getLast] exact h_c -theorem non_zero_map [LawfulBEq R] (f : R → R) (hf : ∀ r, f r = 0 → r = 0) (p : CPolynomial.Raw R) : +theorem non_zero_map [Zero R] [BEq R] [LawfulBEq R] + (f : R → R) (hf : ∀ r, f r = 0 → r = 0) (p : CPolynomial.Raw R) : let fp := mk (p.map f); p.trim = p → fp.trim = fp := by intro fp p_canon @@ -435,12 +474,18 @@ theorem non_zero_map [LawfulBEq R] (f : R → R) (hf : ∀ r, f r = 0 → r = 0) /-- Canonical polynomials enjoy a stronger extensionality theorem: they just need to agree at all coefficients (without assuming equal sizes) -/ -theorem canonical_ext [LawfulBEq R] {p q : CPolynomial.Raw R} (hp : p.trim = p) (hq : q.trim = q) : +theorem canonical_ext [Zero R] [BEq R] [LawfulBEq R] + {p q : CPolynomial.Raw R} (hp : p.trim = p) (hq : q.trim = q) : equiv p q → p = q := by intro h_equiv rw [← hp, ← hq] exact eq_of_equiv h_equiv +theorem isCanonical_ext [Zero R] [BEq R] [LawfulBEq R] {p q : CPolynomial.Raw R} + (hp : IsCanonical p) (hq : IsCanonical q) : + equiv p q → p = q := by + exact canonical_ext (trim_eq_of_isCanonical hp) (trim_eq_of_isCanonical hq) + end Trim end Foundations diff --git a/CompPoly/Univariate/Raw/Division.lean b/CompPoly/Univariate/Raw/Division.lean index 88ef363f..167be1cc 100644 --- a/CompPoly/Univariate/Raw/Division.lean +++ b/CompPoly/Univariate/Raw/Division.lean @@ -19,7 +19,7 @@ variable {R : Type*} section Division -variable [Ring R] [BEq R] +variable [BEq R] /-- Division with remainder by a monic polynomial using polynomial long division. -/ def divModByMonicAux [Field R] (p : CPolynomial.Raw R) (q : CPolynomial.Raw R) : diff --git a/CompPoly/Univariate/Raw/Ops.lean b/CompPoly/Univariate/Raw/Ops.lean index 7192d0c9..a28f7719 100644 --- a/CompPoly/Univariate/Raw/Ops.lean +++ b/CompPoly/Univariate/Raw/Ops.lean @@ -22,9 +22,6 @@ section Operations section Semiring -variable [Semiring R] [BEq R] -variable [Semiring Q] - variable {S : Type*} /-- Evaluates a `CPolynomial.Raw` at `x : S` using a ring homomorphism `f : R →+* S`. @@ -32,42 +29,42 @@ variable {S : Type*} Computes `f(a₀) + f(a₁) * x + f(a₂) * x² + ...` where `aᵢ` are the coefficients. TODO: define an efficient version of this with caching -/ -def eval₂ [Semiring S] (f : R →+* S) (x : S) (p : CPolynomial.Raw R) : S := +def eval₂ [Semiring R] [Semiring S] (f : R →+* S) (x : S) (p : CPolynomial.Raw R) : S := p.zipIdx.foldl (fun acc ⟨a, i⟩ => acc + f a * x ^ i) 0 /-- Evaluates a `CPolynomial.Raw` at a given value -/ @[inline, specialize] -def eval (x : R) (p : CPolynomial.Raw R) : R := +def eval [Semiring R] (x : R) (p : CPolynomial.Raw R) : R := p.eval₂ (RingHom.id R) x /-- Raw addition: pointwise sum of coefficient arrays (padded to equal length). The result may have trailing zeros and should be trimmed for canonical form. -/ @[inline, specialize] -def addRaw (p q : CPolynomial.Raw R) : CPolynomial.Raw R := +def addRaw [Zero R] [Add R] (p q : CPolynomial.Raw R) : CPolynomial.Raw R := let ⟨p', q'⟩ := Array.matchSize p q 0 .mk (Array.zipWith (· + ·) p' q' ) /-- Addition of two `CPolynomial.Raw`s, with result trimmed. -/ @[inline, specialize] -def add (p q : CPolynomial.Raw R) : CPolynomial.Raw R := +def add [Zero R] [Add R] [BEq R] (p q : CPolynomial.Raw R) : CPolynomial.Raw R := addRaw p q |> trim section SMulDefs /-- Scalar multiplication: multiplies each coefficient by `r`. -/ @[inline, specialize] -def smul (r : R) (p : CPolynomial.Raw R) : CPolynomial.Raw R := +def smul [Mul R] (r : R) (p : CPolynomial.Raw R) : CPolynomial.Raw R := .mk (Array.map (fun a => r * a) p) /-- Raw scalar multiplication by a natural number (may have trailing zeros). -/ @[inline, specialize] -def nsmulRaw (n : ℕ) (p : CPolynomial.Raw R) : CPolynomial.Raw R := +def nsmulRaw [Semiring R] (n : ℕ) (p : CPolynomial.Raw R) : CPolynomial.Raw R := .mk (Array.map (fun a => n * a) p) /-- Scalar multiplication of `CPolynomial.Raw` by a natural number, with result trimmed. -/ @[inline, specialize] -def nsmul (n : ℕ) (p : CPolynomial.Raw R) : CPolynomial.Raw R := +def nsmul [Semiring R] [BEq R] (n : ℕ) (p : CPolynomial.Raw R) : CPolynomial.Raw R := nsmulRaw n p |> trim end SMulDefs @@ -76,31 +73,33 @@ section MulPowXDefs /-- Multiplication by `X^i`: shifts coefficients right by `i` positions (prepends `i` zeros). -/ @[inline, specialize] -def mulPowX (i : Nat) (p : CPolynomial.Raw R) : CPolynomial.Raw R := .mk (Array.replicate i 0 ++ p) +def mulPowX [Zero R] (i : Nat) (p : CPolynomial.Raw R) : CPolynomial.Raw R := + .mk (Array.replicate i 0 ++ p) /-- Multiplication of a `CPolynomial.Raw` by `X`, reduces to `mulPowX 1`. -/ @[inline, specialize] -def mulX (p : CPolynomial.Raw R) : CPolynomial.Raw R := p.mulPowX 1 +def mulX [Zero R] (p : CPolynomial.Raw R) : CPolynomial.Raw R := p.mulPowX 1 end MulPowXDefs /-- Multiplication using the naive `O(n²)` algorithm: `Σᵢ (aᵢ * q) * X^i`. -/ @[inline, specialize] -def mul (p q : CPolynomial.Raw R) : CPolynomial.Raw R := +def mul [Semiring R] [BEq R] (p q : CPolynomial.Raw R) : CPolynomial.Raw R := p.zipIdx.foldl (fun acc ⟨a, i⟩ => acc.add <| (smul a q).mulPowX i) (mk #[]) /-- Exponentiation of a `CPolynomial.Raw` by a natural number `n` via repeated multiplication. -/ @[inline, specialize] -def pow (p : CPolynomial.Raw R) (n : Nat) : CPolynomial.Raw R := (mul p)^[n] (C 1) +def pow [Semiring R] [BEq R] (p : CPolynomial.Raw R) (n : Nat) : CPolynomial.Raw R := + (mul p)^[n] (C 1) instance : Zero (CPolynomial.Raw R) := ⟨#[]⟩ -instance : One (CPolynomial.Raw R) := ⟨C 1⟩ -instance : Add (CPolynomial.Raw R) := ⟨add⟩ -instance : SMul R (CPolynomial.Raw R) := ⟨smul⟩ -instance : SMul ℕ (CPolynomial.Raw R) := ⟨nsmul⟩ -instance : Mul (CPolynomial.Raw R) := ⟨mul⟩ -instance : Pow (CPolynomial.Raw R) Nat := ⟨pow⟩ -instance : NatCast (CPolynomial.Raw R) := ⟨fun n => C (n : R)⟩ +instance [One R] : One (CPolynomial.Raw R) := ⟨C 1⟩ +instance [Zero R] [Add R] [BEq R] : Add (CPolynomial.Raw R) := ⟨add⟩ +instance [Mul R] : SMul R (CPolynomial.Raw R) := ⟨smul⟩ +instance [Semiring R] [BEq R] : SMul ℕ (CPolynomial.Raw R) := ⟨nsmul⟩ +instance [Semiring R] [BEq R] : Mul (CPolynomial.Raw R) := ⟨mul⟩ +instance [Semiring R] [BEq R] : Pow (CPolynomial.Raw R) Nat := ⟨pow⟩ +instance [NatCast R] : NatCast (CPolynomial.Raw R) := ⟨fun n => C (n : R)⟩ /-- Upper bound on degree: `size - 1` if non-empty, `⊥` if empty. -/ def degreeBound (p : CPolynomial.Raw R) : WithBot Nat := @@ -113,7 +112,7 @@ def natDegreeBound (p : CPolynomial.Raw R) : Nat := (degreeBound p).getD 0 /-- Check if a `CPolynomial.Raw` is monic, i.e. its leading coefficient is 1. -/ -def monic (p : CPolynomial.Raw R) : Bool := p.leadingCoeff == 1 +def monic [Zero R] [One R] [BEq R] (p : CPolynomial.Raw R) : Bool := p.leadingCoeff == 1 /-- Pseudo-division by `X`: removes the constant term and shifts remaining coefficients left. -/ def divX (p : CPolynomial.Raw R) : CPolynomial.Raw R := p.extract 1 p.size @@ -122,22 +121,23 @@ end Semiring section Ring -variable [Ring R] [BEq R] - /-- Negation of a `CPolynomial.Raw`. -/ @[inline, specialize] -def neg (p : CPolynomial.Raw R) : CPolynomial.Raw R := p.map (fun a => -a) +def neg [Neg R] (p : CPolynomial.Raw R) : CPolynomial.Raw R := p.map (fun a => -a) /-- Subtraction of two `CPolynomial.Raw`s. -/ @[inline, specialize] -def sub (p q : CPolynomial.Raw R) : CPolynomial.Raw R := p.add q.neg +def sub [Zero R] [Add R] [Neg R] [BEq R] + (p q : CPolynomial.Raw R) : CPolynomial.Raw R := + p.add q.neg -instance : Neg (CPolynomial.Raw R) := ⟨neg⟩ -instance : Sub (CPolynomial.Raw R) := ⟨sub⟩ -instance : IntCast (CPolynomial.Raw R) := ⟨fun n => C (n : R)⟩ +instance [Neg R] : Neg (CPolynomial.Raw R) := ⟨neg⟩ +instance [Zero R] [Add R] [Neg R] [BEq R] : Sub (CPolynomial.Raw R) := ⟨sub⟩ +instance [IntCast R] : IntCast (CPolynomial.Raw R) := ⟨fun n => C (n : R)⟩ /-- Erase the coefficient at index `n`: same as `p` except `coeff n = 0`, then trimmed. -/ -def erase [DecidableEq R] (n : ℕ) (p : CPolynomial.Raw R) : CPolynomial.Raw R := +def erase [Zero R] [Add R] [Neg R] [BEq R] [DecidableEq R] + (n : ℕ) (p : CPolynomial.Raw R) : CPolynomial.Raw R := p - monomial n (p.coeff n) end Ring diff --git a/CompPoly/Univariate/Raw/Proofs.lean b/CompPoly/Univariate/Raw/Proofs.lean index 07d40754..c5abdfc8 100644 --- a/CompPoly/Univariate/Raw/Proofs.lean +++ b/CompPoly/Univariate/Raw/Proofs.lean @@ -937,16 +937,15 @@ protected theorem mul_comm [LawfulBEq R] (p q : CPolynomial.Raw R) : p * q = q * end CommutativeSemiring +lemma neg_coeff {R : Type*} [NegZeroClass R] (p : CPolynomial.Raw R) (i : ℕ) : + p.neg.coeff i = - p.coeff i := by + unfold neg coeff + rcases (Nat.lt_or_ge i p.size) with hi | hi <;> simp [hi] + section Ring variable [Ring R] [BEq R] -omit [BEq R] in -lemma neg_coeff : ∀ (p : CPolynomial.Raw R) (i : ℕ), p.neg.coeff i = - p.coeff i := by - intro p i - unfold neg coeff - rcases (Nat.lt_or_ge i p.size) with hi | hi <;> simp [hi] - theorem neg_trim [LawfulBEq R] (p : CPolynomial.Raw R) : p.trim = p → (-p).trim = -p := by apply Trim.non_zero_map simp diff --git a/CompPoly/Univariate/ToPoly/Core.lean b/CompPoly/Univariate/ToPoly/Core.lean index d24dad23..d0292733 100644 --- a/CompPoly/Univariate/ToPoly/Core.lean +++ b/CompPoly/Univariate/ToPoly/Core.lean @@ -32,17 +32,17 @@ namespace CPolynomial open Raw -variable {R : Type*} [Ring R] [BEq R] -variable {Q : Type*} [Ring Q] +variable {R : Type*} +variable {Q : Type*} -section ToPoly +section ToPolyDefs /-- Convert a `CPolynomial.Raw` to a (mathlib) `Polynomial`. -/ -noncomputable def Raw.toPoly (p : CPolynomial.Raw R) : Polynomial R := +noncomputable def Raw.toPoly [Semiring R] (p : CPolynomial.Raw R) : Polynomial R := p.eval₂ Polynomial.C Polynomial.X /-- Alternative definition of `toPoly` using `Finsupp`; currently unused. -/ -noncomputable def Raw.toPoly' (p : CPolynomial.Raw R) : Polynomial R := +noncomputable def Raw.toPoly' [Semiring R] (p : CPolynomial.Raw R) : Polynomial R := Polynomial.ofFinsupp (Finsupp.onFinset (Finset.range p.size) p.coeff (by intro n hn rw [Finset.mem_range] @@ -52,7 +52,14 @@ noncomputable def Raw.toPoly' (p : CPolynomial.Raw R) : Polynomial R := )) /-- Convert a canonical polynomial to a (mathlib) `Polynomial`. -/ -noncomputable def toPoly (p : CPolynomial R) : Polynomial R := p.val.toPoly +noncomputable def toPoly [Zero R] [Semiring R] (p : CPolynomial R) : Polynomial R := p.val.toPoly + +end ToPolyDefs + +section ToPoly + +variable [Semiring R] [BEq R] +variable [Semiring Q] namespace Raw @@ -167,16 +174,22 @@ lemma getLast_toImpl {p : Q[X]} (hp : p ≠ 0) : let h : p.toImpl.size > 0 := to · contradiction simp [h] +omit [BEq R] in +/-- `toImpl` lands in the semantic canonical carrier used by `CPolynomial`. -/ +@[simp] +theorem isCanonical_toImpl (p : R[X]) : CPolynomial.Raw.IsCanonical p.toImpl := by + rcases toImpl_elim p with ⟨rfl, h⟩ | ⟨h_nz, _⟩ + · simpa [h] using (Trim.isCanonical_empty (R := R)) + · intro hp + have hlast : p.toImpl.getLast hp = p.leadingCoeff := by + simpa using (getLast_toImpl (Q := R) (p := p) h_nz) + rw [hlast] + exact Polynomial.leadingCoeff_ne_zero.mpr h_nz + /-- `toImpl` produces canonical polynomials (no trailing zeros). -/ @[simp, grind =] theorem trim_toImpl [LawfulBEq R] (p : R[X]) : p.toImpl.trim = p.toImpl := by - rcases toImpl_elim p with ⟨rfl, h⟩ | ⟨h_nz, _⟩ - · rw [h, Trim.canonical_empty] - rw [Trim.canonical_iff] - unfold Array.getLast - intro - rw [getLast_toImpl h_nz] - exact Polynomial.leadingCoeff_ne_zero.mpr h_nz + exact Trim.trim_eq_of_isCanonical (isCanonical_toImpl p) end Raw @@ -187,10 +200,13 @@ end Raw lemma toImpl_toPoly_of_canonical [LawfulBEq R] (p : CPolynomial R) : p.toPoly.toImpl = p := by suffices h_inj : ∀ q : CPolynomial R, p.toPoly = q.toPoly → p = q by have : p.toPoly = p.toPoly.toImpl.toPoly := by rw [toPoly_toImpl] - exact h_inj ⟨ p.toPoly.toImpl, trim_toImpl p.toPoly ⟩ this |> congrArg Subtype.val |>.symm + exact + h_inj ⟨p.toPoly.toImpl, isCanonical_toImpl p.toPoly⟩ this + |> congrArg Subtype.val + |>.symm intro q hpq apply CPolynomial.ext - apply Trim.canonical_ext p.property q.property + apply Trim.isCanonical_ext p.property q.property intro i rw [← coeff_toPoly, ← coeff_toPoly] exact hpq |> congrArg (fun p => p.coeff i) @@ -199,7 +215,7 @@ lemma toImpl_toPoly_of_canonical [LawfulBEq R] (p : CPolynomial R) : p.toPoly.to @[simp, grind =] theorem Raw.toImpl_toPoly [LawfulBEq R] (p : CPolynomial.Raw R) : p.toPoly.toImpl = p.trim := by rw [← toPoly_trim] - exact toImpl_toPoly_of_canonical ⟨ p.trim, Trim.trim_twice p⟩ + exact toImpl_toPoly_of_canonical ⟨ p.trim, Trim.isCanonical_trim p⟩ /-- `toPoly` maps a canonical polynomial to `0` iff the polynomial is `0`. -/ theorem toPoly_eq_zero_iff [LawfulBEq R] (p : CPolynomial R) : diff --git a/CompPoly/Univariate/ToPoly/Degree.lean b/CompPoly/Univariate/ToPoly/Degree.lean index 43d7766f..90d1b5e5 100644 --- a/CompPoly/Univariate/ToPoly/Degree.lean +++ b/CompPoly/Univariate/ToPoly/Degree.lean @@ -19,68 +19,83 @@ namespace CPolynomial open Raw -variable {R : Type*} [Ring R] [BEq R] +variable {R : Type*} [Semiring R] [BEq R] section ImplementationCorrectness +omit [BEq R] in +private theorem size_toImpl_eq_natDegree_succ {q : R[X]} (hq : q ≠ 0) : + q.toImpl.size = q.natDegree + 1 := by + rcases Raw.toImpl_elim q with ⟨hzero, _⟩ | ⟨_, himpl⟩ + · exact (hq hzero).elim + · simp [himpl] + +private theorem size_eq_toPoly_natDegree_succ [LawfulBEq R] (p : CPolynomial R) (hp : p ≠ 0) : + p.val.size = p.toPoly.natDegree + 1 := by + have htoPoly : p.toPoly ≠ 0 := (toPoly_eq_zero_iff p).not.mpr hp + have hsize : p.toPoly.toImpl.size = p.val.size := by + simpa using congrArg Array.size (toImpl_toPoly_of_canonical p) + rw [← hsize] + exact size_toImpl_eq_natDegree_succ htoPoly + theorem degree_toPoly [LawfulBEq R] (p : CPolynomial R) : p.degree = p.toPoly.degree := by - have h_deg_eq : p.val.toPoly.degree = p.val.degree := by - unfold CPolynomial.Raw.degree at * - rcases h : ( p : CompPoly.CPolynomial.Raw R ).lastNonzero with ( _ | ⟨ k, hk ⟩ ) - <;> simp_all +decide [ Polynomial.degree_eq_bot ] - · have := p.prop - unfold CompPoly.CPolynomial.Raw.trim at this; aesop - · have := CPolynomial.Raw.Trim.lastNonzero_spec h - rw [ Polynomial.degree_eq_of_le_of_coeff_ne_zero ] - · rw [ Polynomial.degree_le_iff_coeff_zero ] - intro m hm; by_cases hm' : m < p.val.size - <;> simp_all +decide [ CPolynomial.Raw.coeff_toPoly ] - · rw [ CompPoly.CPolynomial.Raw.coeff_toPoly ]; aesop - exact h_deg_eq.symm + by_cases hp : p = 0 + · subst hp + rw [toPoly_zero, CPolynomial.degree] + rfl + · have hsize := size_eq_toPoly_natDegree_succ p hp + have htoPoly : p.toPoly ≠ 0 := (toPoly_eq_zero_iff p).not.mpr hp + cases hs : p.val.size with + | zero => + simp [hs] at hsize + | succ n => + have hnat : p.toPoly.natDegree = n := by omega + simp [CPolynomial.degree, hs, hnat, + Polynomial.degree_eq_natDegree htoPoly] theorem natDegree_toPoly [LawfulBEq R] (p : CPolynomial R) : p.natDegree = p.toPoly.natDegree := by - have h_deg_eq : p.degree = p.toPoly.degree := by - exact degree_toPoly p - have h_natDegree_eq : p.natDegree = p.degree.unbotD 0 := by - unfold CPolynomial.natDegree CPolynomial.degree - unfold CPolynomial.Raw.natDegree CPolynomial.Raw.degree - cases p.val.lastNonzero <;> rfl - aesop + by_cases hp : p = 0 + · subst hp + rw [ + toPoly_zero, + CPolynomial.natDegree + ] + rfl + · have hsize := size_eq_toPoly_natDegree_succ p hp + cases hs : p.val.size with + | zero => + simp [hs] at hsize + | succ n => + have hnat : p.toPoly.natDegree = n := by omega + rw [ + hnat, + CPolynomial.natDegree, + hs + ] theorem leadingCoeff_toPoly [LawfulBEq R] (p : CPolynomial R) : p.leadingCoeff = p.toPoly.leadingCoeff := by - by_contra h_contra - apply h_contra - obtain ⟨q, hq⟩ : ∃ q : Polynomial R, p = ⟨q.toImpl, trim_toImpl q⟩ := by - use p.toPoly - generalize_proofs at * - convert Subtype.ext ?_ - exact Eq.symm (toImpl_toPoly_of_canonical p) - have h_leading_coeff_eq : q.toImpl.getLast (by - by_cases hq_zero : q = 0 <;> simp_all +decide [ Polynomial.toImpl ] - · simp [CompPoly.CPolynomial.leadingCoeff, CompPoly.CPolynomial.toPoly] at h_contra - simp +decide [ CompPoly.CPolynomial.Raw.leadingCoeff, CompPoly.CPolynomial.Raw.toPoly ] - at h_contra - exact h_contra (by unfold CompPoly.CPolynomial.Raw.trim; aesop) - · cases h : q.degree <;> simp_all +decide [ Polynomial.degree_eq_natDegree hq_zero ]) - = q.leadingCoeff := by - all_goals generalize_proofs at * - convert Raw.getLast_toImpl _ - rintro rfl; simp_all +decide [ Polynomial.toImpl ] - generalize_proofs at * - convert h_leading_coeff_eq using 1 - · unfold CPolynomial.leadingCoeff - unfold CPolynomial.Raw.leadingCoeff - unfold Array.getLastD; aesop - · rw [ ← h_leading_coeff_eq, hq ] - rw [ show (CompPoly.CPolynomial.toPoly ⟨q.toImpl, by assumption⟩ : Polynomial R) = q - from ?_ ] - · exact h_leading_coeff_eq.symm - · apply Raw.toPoly_toImpl - -theorem erase_toPoly [LawfulBEq R] [DecidableEq R] (n : ℕ) (p : CPolynomial R) : + by_cases hp : p = 0 + · subst hp + rw [toPoly_zero, CPolynomial.leadingCoeff] + rfl + · have htoPoly : p.toPoly ≠ 0 := (toPoly_eq_zero_iff p).not.mpr hp + have hpos : p.val.size > 0 := by + have hsize := size_eq_toPoly_natDegree_succ p hp + omega + have hlastImpl : + p.toPoly.toImpl.getLast (Raw.toImpl_nonzero htoPoly) = p.toPoly.leadingCoeff := by + simpa using Raw.getLast_toImpl htoPoly + have hround : p.toPoly.toImpl = (p : CPolynomial.Raw R) := by + simpa using toImpl_toPoly_of_canonical p + have hlast : p.val.getLast hpos = p.toPoly.leadingCoeff := by + simpa [hround] using hlastImpl + simpa [CPolynomial.leadingCoeff, Array.getLastD, hpos] using hlast + +theorem erase_toPoly {R : Type*} [Ring R] [BEq R] [LawfulBEq R] [DecidableEq R] + (n : ℕ) (p : CPolynomial R) : (erase n p).toPoly = p.toPoly.erase n := by have h_erase_def : (CPolynomial.erase n p).toPoly = p.toPoly - Polynomial.monomial n (p.val.coeff n) := by @@ -117,24 +132,18 @@ theorem C_mul_X_pow_toPoly [LawfulBEq R] [DecidableEq R] [Nontrivial R] (r : R) · convert monomial_toPoly n r theorem lcoeff_toPoly [LawfulBEq R] (n : ℕ) (p : CPolynomial R) : - lcoeff R n p = Polynomial.lcoeff R n (toPoly p) := by + lcoeff (R := R) n p = Polynomial.lcoeff R n (toPoly p) := by simp [lcoeff, Polynomial.lcoeff_apply, ← coeff_toPoly] theorem degreeLE_toPoly {n : WithBot ℕ} [LawfulBEq R] {p : CPolynomial R} : - p ∈ degreeLE R n ↔ p.toPoly ∈ Polynomial.degreeLE R n := by - simp only [degreeLE, Polynomial.degreeLE, Submodule.mem_iInf, LinearMap.mem_ker, - lcoeff_toPoly] + p ∈ degreeLE (R := R) n ↔ p.toPoly ∈ Polynomial.degreeLE R n := by + rw [Polynomial.mem_degreeLE] + convert (show p.degree ≤ n ↔ p.toPoly.degree ≤ n by rw [degree_toPoly]) using 1 theorem degreeLT_toPoly {n : ℕ} [LawfulBEq R] {p : CPolynomial R} : - p ∈ degreeLT R n ↔ p.toPoly ∈ Polynomial.degreeLT R n := by - simp only [degreeLT, Polynomial.degreeLT, Submodule.mem_iInf, LinearMap.mem_ker, - lcoeff_toPoly] - -theorem degreeLTEquiv_toPoly {n : ℕ} [LawfulBEq R] [DecidableEq R] {p : CPolynomial R} - (hp : p ∈ degreeLT R n) (i : Fin n) : - degreeLTEquiv R n ⟨p, hp⟩ i = - Polynomial.degreeLTEquiv R n ⟨p.toPoly, degreeLT_toPoly.mp hp⟩ i := by - simp [degreeLTEquiv, Polynomial.degreeLTEquiv, ← coeff_toPoly] + p ∈ degreeLT (R := R) n ↔ p.toPoly ∈ Polynomial.degreeLT R n := by + rw [Polynomial.mem_degreeLT] + convert (show p.degree < n ↔ p.toPoly.degree < n by rw [degree_toPoly]) using 1 end ImplementationCorrectness @@ -148,28 +157,11 @@ lemma toPoly_smul (r : R) (p : CPolynomial R) : noncomputable def toPolyLinearEquiv : CPolynomial R ≃ₗ[R] R[X] where toFun := toPoly - invFun := fun p => ⟨p.toImpl, trim_toImpl p⟩ + invFun := fun p => ⟨p.toImpl, isCanonical_toImpl p⟩ map_add' := toPoly_add map_smul' := toPoly_smul left_inv := fun p => Subtype.ext (toImpl_toPoly_of_canonical p) right_inv := fun _ => toPoly_toImpl - -theorem degreeLE_map_toPolyLinearEquiv {n : WithBot ℕ} : - (degreeLE R n).map toPolyLinearEquiv.toLinearMap = Polynomial.degreeLE R n := - le_antisymm (fun _ ⟨p, hp, h⟩ => h ▸ degreeLE_toPoly.mp hp) - (fun q hq => ⟨toPolyLinearEquiv.symm q, degreeLE_toPoly.mpr (by - show (toPolyLinearEquiv.symm q).toPoly ∈ _ - rw [show (toPolyLinearEquiv.symm q).toPoly = q from toPolyLinearEquiv.apply_symm_apply q] - exact hq), toPolyLinearEquiv.apply_symm_apply q⟩) - -theorem degreeLT_map_toPolyLinearEquiv {n : ℕ} : - (degreeLT R n).map toPolyLinearEquiv.toLinearMap = Polynomial.degreeLT R n := - le_antisymm (fun _ ⟨p, hp, h⟩ => h ▸ degreeLT_toPoly.mp hp) - (fun q hq => ⟨toPolyLinearEquiv.symm q, degreeLT_toPoly.mpr (by - show (toPolyLinearEquiv.symm q).toPoly ∈ _ - rw [show (toPolyLinearEquiv.symm q).toPoly = q from toPolyLinearEquiv.apply_symm_apply q] - exact hq), toPolyLinearEquiv.apply_symm_apply q⟩) - theorem degree_le_iff_coeff_zero (p : CPolynomial R) (n : WithBot ℕ) : p.degree ≤ n ↔ ∀ k : ℕ, n < k → p.coeff k = 0 := by rw [degree_toPoly, Polynomial.degree_le_iff_coeff_zero] @@ -180,114 +172,135 @@ theorem degree_lt_iff_coeff_zero (p : CPolynomial R) (n : ℕ) : rw [degree_toPoly, Polynomial.degree_lt_iff_coeff_zero] simp only [coeff_toPoly] +omit [BEq R] [LawfulBEq R] in theorem mem_degreeLE {n : WithBot ℕ} {p : (CPolynomial R)} : - p ∈ degreeLE R n ↔ degree p ≤ n := by - simp [degreeLE] - exact Iff.symm (degree_le_iff_coeff_zero p n) + p ∈ degreeLE (R := R) n ↔ degree p ≤ n := by + rfl +omit [BEq R] [LawfulBEq R] in theorem degreeLE_mono (m n : WithBot ℕ) (h_lessThan : m ≤ n) : - degreeLE R m ≤ degreeLE R n := - fun _ hf => mem_degreeLE.2 (le_trans (mem_degreeLE.1 hf) h_lessThan) + degreeLE (R := R) m ≤ degreeLE (R := R) n := + fun _ hf => mem_degreeLE.2 (le_trans (mem_degreeLE.1 hf) h_lessThan) -theorem mem_degreeLT {n : ℕ} {p : CPolynomial R} : p ∈ degreeLT R n ↔ degree p < n := by - simp [degreeLT] - rw[degree_lt_iff_coeff_zero] - exact Lex.forall +omit [BEq R] [LawfulBEq R] in +theorem mem_degreeLT {n : ℕ} {p : CPolynomial R} : p ∈ degreeLT (R := R) n ↔ degree p < n := by + rfl -theorem degreeLT_mono {m n : ℕ} (h : m ≤ n) : degreeLT R m ≤ degreeLT R n := fun _ hf => +omit [BEq R] [LawfulBEq R] in +theorem degreeLT_mono {m n : ℕ} (h : m ≤ n) : + degreeLT (R := R) m ≤ degreeLT (R := R) n := fun _ hf => mem_degreeLT.2 (lt_of_lt_of_le (mem_degreeLT.1 hf) <| WithBot.coe_le_coe.2 h) -theorem degreeLT_succ_eq_degreeLE {n : ℕ} : degreeLT R (n + 1) = degreeLE R ↑n := by - simp +decide [ degreeLT, degreeLE ] - -section bases - -lemma toPolyLinearEquiv_X_pow [Nontrivial R] (k : ℕ) : - toPolyLinearEquiv (R := R) (X ^ k) = Polynomial.X ^ k := by - show toPoly (X ^ k) = Polynomial.X ^ k - rw [toPoly_pow, X_toPoly] - -theorem degreeLE_eq_span_X_pow [DecidableEq R] [Nontrivial R] {n : ℕ} : - degreeLE R ↑n = - Submodule.span R ↑((Finset.range (n + 1)).image fun n => (X : CPolynomial R) ^ n) := by - set e := toPolyLinearEquiv (R := R) - apply Submodule.map_injective_of_injective e.injective - rw [degreeLE_map_toPolyLinearEquiv, Submodule.map_span, Polynomial.degreeLE_eq_span_X_pow] - congr 1 - simp only [Finset.coe_image, Set.image_image, LinearEquiv.coe_toLinearMap] - congr 1; funext k; exact (toPolyLinearEquiv_X_pow (R := R) k).symm - -theorem degreeLT_eq_span_X_pow [DecidableEq R] [Nontrivial R] {n : ℕ} : - degreeLT R n - = Submodule.span R ↑((Finset.range n).image fun n => (X : CPolynomial R) ^ n) := by - set e := toPolyLinearEquiv (R := R) - apply Submodule.map_injective_of_injective e.injective - rw [degreeLT_map_toPolyLinearEquiv, Submodule.map_span, Polynomial.degreeLT_eq_span_X_pow] - congr 1 - simp only [Finset.coe_image, Set.image_image, LinearEquiv.coe_toLinearMap] - congr 1; funext k; exact (toPolyLinearEquiv_X_pow (R := R) k).symm - -end bases +omit [BEq R] [LawfulBEq R] in +theorem degreeLT_succ_eq_degreeLE {n : ℕ} : + degreeLT (R := R) (n + 1) = degreeLE (R := R) ↑n := by + ext p + change p.val.degreeBound < (n + 1 : ℕ) ↔ p.val.degreeBound ≤ (n : WithBot ℕ) + cases hd : p.val.degreeBound with + | bot => + simp + | coe a => + change ((a : WithBot ℕ) < (n + 1 : ℕ)) ↔ ((a : WithBot ℕ) ≤ (n : ℕ)) + exact WithBot.coe_lt_coe.trans (Nat.lt_succ_iff.trans WithBot.coe_le_coe.symm) section degreeLTEquiv +lemma monomial_mem_degreeLT [DecidableEq R] {n : ℕ} (i : Fin n) (c : R) : + monomial (R := R) (i : ℕ) c ∈ degreeLT (R := R) n := by + rw [mem_degreeLT_iff_size_le] + by_cases hc : c = 0 + · simp [monomial, Raw.monomial, hc] + · simp [monomial, Raw.monomial, hc, Nat.succ_le_of_lt i.isLt] + lemma degreeLTEquiv_invFun_mem [DecidableEq R] (n : ℕ) (f : Fin n → R) : - Finset.univ.sum (fun i : Fin n => monomial (↑i) (f i)) ∈ degreeLT R n := by - simp [degreeLT] - intro i hi - simp [lcoeff, monomial] - rw [ Finset.sum_eq_zero ]; intros; simp_all +decide [ CPolynomial.Raw.monomial ]; - grind + Finset.univ.sum (fun i : Fin n => monomial (R := R) (i : ℕ) (f i)) ∈ degreeLT (R := R) n := by + refine Finset.induction_on Finset.univ ?_ ?_ + · exact zero_mem_degreeLT (R := R) n + · intro i s hi hs + rw [Finset.sum_insert hi] + exact add_mem_degreeLT (monomial_mem_degreeLT (R := R) i (f i)) hs lemma degreeLTEquiv_left_inv [DecidableEq R] (n : ℕ) - (p : ↥(degreeLT R n)) : - (⟨Finset.univ.sum (fun i : Fin n => monomial (↑i) (coeff p.1 i)), - degreeLTEquiv_invFun_mem n (fun i => coeff p.1 i)⟩ : ↥(degreeLT R n)) = p := by - apply Subtype.ext - rw [eq_iff_coeff]; intro i - rw [show coeff (∑ j : Fin n, monomial (↑j) (coeff p.1 j)) i = - ∑ j : Fin n, coeff (monomial (↑j) (coeff p.1 j)) i from map_sum (lcoeff R i) _ _] - simp only [coeff_monomial] - by_cases hi : i < n - · rw [Finset.sum_eq_single_of_mem ⟨i, hi⟩ (Finset.mem_univ _) - (fun j _ hji => if_neg fun h => hji (Fin.ext (by aesop)))] - simp - · rw [show coeff p.1 i = 0 from - (degree_lt_iff_coeff_zero p.1 n).mp (mem_degreeLT.mp p.2) i (by omega)] - exact Finset.sum_eq_zero fun j _ => if_neg (by have := j.isLt; omega) + (p : ↥(degreeLT (R := R) n)) : + (⟨ + Finset.univ.sum (fun i : Fin n => monomial (R := R) (↑i) (coeff p.1 i)), + degreeLTEquiv_invFun_mem (R := R) n (fun i => coeff p.1 i) + ⟩ : ↥(degreeLT (R := R) n)) = p := by + apply Subtype.ext + rw [eq_iff_coeff] + intro i + rw [show coeff (∑ j : Fin n, monomial (R := R) (↑j) (coeff p.1 j)) i = + ∑ j : Fin n, coeff (monomial (R := R) (↑j) (coeff p.1 j)) i from + map_sum (lcoeff (R := R) i) _ _] + simp only [coeff_monomial] + by_cases hi : i < n + · rw [Finset.sum_eq_single_of_mem ⟨i, hi⟩ (Finset.mem_univ _) + (fun j _ hji => if_neg fun h => hji (Fin.ext h.symm))] + simp + · rw [show coeff p.1 i = 0 from + (degree_lt_iff_coeff_zero p.1 n).mp (mem_degreeLT.mp p.2) i (by omega)] + exact Finset.sum_eq_zero fun j _ => if_neg (by have := j.isLt; omega) lemma degreeLTEquiv_right_inv [DecidableEq R] (n : ℕ) (f : Fin n → R) : (fun i : Fin n => coeff - (Finset.univ.sum (fun j : Fin n => monomial (↑j) (f j))) i) = f := by - funext i - rw [show coeff (∑ j : Fin n, monomial (↑j) (f j)) ↑i = - ∑ j : Fin n, coeff (monomial (↑j) (f j)) ↑i from map_sum (lcoeff R ↑i) _ _] - simp only [coeff_monomial] - rw [Finset.sum_eq_single_of_mem i (Finset.mem_univ _) - (fun j _ hji => if_neg fun h => hji (Fin.ext (by omega)))] - simp - -noncomputable def degreeLTLinearEquiv [DecidableEq R] (n : ℕ) : degreeLT R n ≃ₗ[R] (Fin n → R) := - LinearEquiv.ofBijective (degreeLTEquiv R n) - ⟨Function.HasLeftInverse.injective ⟨fun f => - ⟨_, degreeLTEquiv_invFun_mem n f⟩, degreeLTEquiv_left_inv n⟩, - fun f => ⟨⟨_, degreeLTEquiv_invFun_mem n f⟩, degreeLTEquiv_right_inv n f⟩⟩ + (Finset.univ.sum (fun j : Fin n => monomial (R := R) (↑j) (f j))) i) = f := by + funext i + rw [show coeff (∑ j : Fin n, monomial (R := R) (↑j) (f j)) ↑i = + ∑ j : Fin n, coeff (monomial (R := R) (↑j) (f j)) ↑i from + map_sum (lcoeff (R := R) ↑i) _ _] + simp only [coeff_monomial] + rw [Finset.sum_eq_single_of_mem i (Finset.mem_univ _) + (fun j _ hji => if_neg fun h => hji (Fin.ext (by omega)))] + simp + +def degreeLTEquiv [DecidableEq R] (n : ℕ) : + ↥(degreeLT (R := R) n) ≃ₗ[R] (Fin n → R) where + toFun := degreeLTCoeffs (R := R) n + invFun := fun f => ⟨Finset.univ.sum (fun i : Fin n => monomial (R := R) (↑i) (f i)), + degreeLTEquiv_invFun_mem (R := R) n f⟩ + left_inv := degreeLTEquiv_left_inv (R := R) n + right_inv := degreeLTEquiv_right_inv (R := R) n + map_add' := by + intro p q + exact (degreeLTCoeffs (R := R) n).map_add p q + map_smul' := by + intro r p + exact (degreeLTCoeffs (R := R) n).map_smul r p + +abbrev degreeLTLinearEquiv [DecidableEq R] (n : ℕ) : + ↥(degreeLT (R := R) n) ≃ₗ[R] (Fin n → R) := + degreeLTEquiv (R := R) n + +theorem degreeLTEquiv_toPoly [DecidableEq R] {n : ℕ} {p : CPolynomial R} + (hp : p ∈ degreeLT (R := R) n) (i : Fin n) : + degreeLTEquiv (R := R) n ⟨p, hp⟩ i = + Polynomial.degreeLTEquiv R n ⟨p.toPoly, degreeLT_toPoly.mp hp⟩ i := by + simp [degreeLTEquiv, degreeLTCoeffs, Polynomial.degreeLTEquiv, ← coeff_toPoly] theorem degreeLTEquiv_eq_zero_iff_eq_zero [DecidableEq R] {n : ℕ} {p : CPolynomial R} - (hp : p ∈ degreeLT R n) : - degreeLTEquiv R n ⟨p, hp⟩ = 0 ↔ p = 0 := by - change (degreeLTLinearEquiv n) ⟨p, hp⟩ = 0 ↔ p = 0 - rw [← map_zero (degreeLTLinearEquiv n), (degreeLTLinearEquiv n).injective.eq_iff, - Subtype.ext_iff, Submodule.coe_zero] + (hp : p ∈ degreeLT (R := R) n) : + degreeLTEquiv (R := R) n ⟨p, hp⟩ = 0 ↔ p = 0 := by + constructor + · intro h + have h_subtype : (⟨p, hp⟩ : ↥(degreeLT (R := R) n)) = 0 := + (degreeLTEquiv (R := R) n).injective (by simpa using h) + exact congrArg Subtype.val h_subtype + · rintro rfl + have h_subtype : (⟨(0 : CPolynomial R), hp⟩ : ↥(degreeLT (R := R) n)) = 0 := by + apply Subtype.ext + rfl + rw [h_subtype] + exact map_zero (degreeLTEquiv (R := R) n) theorem eval_eq_sum_degreeLTEquiv [DecidableEq R] {n : ℕ} {p : CPolynomial R} - (hp : p ∈ degreeLT R n) (x : R) : + (hp : p ∈ degreeLT (R := R) n) (x : R) : eval x p = - Finset.univ.sum (fun i : Fin n => degreeLTEquiv R n ⟨p, hp⟩ i * x ^ (i : ℕ)) := by - rw [eval_toPoly, Polynomial.eval_eq_sum_degreeLTEquiv (degreeLT_toPoly.mp hp)] - congr 1; ext i; congr 1 - rw [degreeLTEquiv_toPoly hp i] + Finset.univ.sum (fun i : Fin n => degreeLTEquiv (R := R) n ⟨p, hp⟩ i * x ^ (i : ℕ)) := by + rw [eval_toPoly, Polynomial.eval_eq_sum_degreeLTEquiv (degreeLT_toPoly.mp hp)] + refine Finset.sum_congr rfl ?_ + intro i _ + rw [degreeLTEquiv_toPoly (R := R) hp i] end degreeLTEquiv diff --git a/CompPoly/Univariate/ToPoly/Equiv.lean b/CompPoly/Univariate/ToPoly/Equiv.lean index 6c28c260..3bb615d2 100644 --- a/CompPoly/Univariate/ToPoly/Equiv.lean +++ b/CompPoly/Univariate/ToPoly/Equiv.lean @@ -19,13 +19,12 @@ namespace CPolynomial open Raw -variable {R : Type*} [Ring R] [BEq R] -variable {Q : Type*} [Ring Q] +variable {R : Type*} [Semiring R] [BEq R] section RingEquiv @[grind =] -lemma toPoly_neg [LawfulBEq R] (p : CPolynomial R) : +lemma toPoly_neg {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : (-p).toPoly = -p.toPoly := by ext i rw [Polynomial.coeff_neg, CPolynomial.toPoly, CPolynomial.toPoly] @@ -38,7 +37,7 @@ lemma toPoly_add [LawfulBEq R] (p q : CPolynomial R) : apply Raw.toPoly_add @[grind =] -lemma toPoly_sub [LawfulBEq R] (p q : CPolynomial R) : +lemma toPoly_sub {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) : (p - q).toPoly = p.toPoly - q.toPoly := by change (p + -q).toPoly = p.toPoly + -q.toPoly rw [toPoly_add, toPoly_neg] @@ -74,7 +73,7 @@ lemma toPoly_mul [LawfulBEq R] (p q : CPolynomial R) : exact toPoly_mul_coeffC p q i @[simp, grind =] -lemma eval₂_C {R : Type*} [Ring R] [BEq R] {S : Type*} [Semiring S] +lemma eval₂_C {R : Type*} [Semiring R] {S : Type*} [Semiring S] (f : R →+* S) (x : S) (r : R) : (Raw.C r).eval₂ f x = f r := by unfold CPolynomial.Raw.eval₂ Raw.C @@ -82,13 +81,13 @@ lemma eval₂_C {R : Type*} [Ring R] [BEq R] {S : Type*} [Semiring S] simp [Array.zipIdx] @[simp, grind =] -lemma Raw.toPoly_C {R : Type*} [Ring R] [BEq R] (r : R) : +lemma Raw.toPoly_C {R : Type*} [Semiring R] (r : R) : (Raw.C r).toPoly = Polynomial.C r := by unfold Raw.toPoly exact eval₂_C Polynomial.C Polynomial.X r @[simp, grind =] -lemma Raw.toPoly_one [LawfulBEq R] : +lemma Raw.toPoly_one {R : Type*} [Semiring R] : (1 : CPolynomial.Raw R).toPoly = 1 := by have : (1 : CPolynomial.Raw R).toPoly = (Raw.C 1).toPoly := by rfl apply this.trans; clear this @@ -97,16 +96,15 @@ lemma Raw.toPoly_one [LawfulBEq R] : lemma toPoly_one [LawfulBEq R] [Nontrivial R] : (1 : CPolynomial R).toPoly = 1 := by apply Raw.toPoly_one -omit [BEq R] in @[simp, grind =] -lemma Raw.toPoly_zero : (0 : CPolynomial.Raw R).toPoly = 0 := by +lemma Raw.toPoly_zero {R : Type*} [Semiring R] : (0 : CPolynomial.Raw R).toPoly = 0 := by simp [Raw.toPoly, Raw.eval₂] -lemma toPoly_zero : (0 : CPolynomial R).toPoly = 0 := by +lemma toPoly_zero {R : Type*} [Semiring R] : (0 : CPolynomial R).toPoly = 0 := by apply Raw.toPoly_zero @[simp, grind =] -lemma Raw.toPoly_X [LawfulBEq R] : +lemma Raw.toPoly_X {R : Type*} [Semiring R] : (Raw.X : CPolynomial.Raw R).toPoly = Polynomial.X := by unfold CPolynomial.Raw.X simp [Raw.toPoly, Raw.eval₂] @@ -127,7 +125,8 @@ lemma toPoly_pow [Nontrivial R] [LawfulBEq R] (p : CPolynomial R) (n : ℕ) : simpa using (_root_.pow_succ (p.toPoly : R[X]) n) rw [hp, toPoly_mul, ih, htp] -lemma toPoly_sum.{u} {R : Type*} [BEq R] [Field R] [LawfulBEq R] {ι : Type u} [DecidableEq ι] +lemma toPoly_sum.{u} {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] {ι : Type u} + [DecidableEq ι] {s : Finset ι} {f : ι → CPolynomial R} : (∑ j ∈ s, f j).toPoly = ∑ j ∈ s, ((f j).toPoly) := by induction s using Finset.induction_on with @@ -136,7 +135,8 @@ lemma toPoly_sum.{u} {R : Type*} [BEq R] [Field R] [LawfulBEq R] {ι : Type u} [ | insert a s ha ih => simp [Finset.sum_insert, ha, toPoly_add, ih] -lemma toPoly_prod.{u} {R : Type*} [BEq R] [Field R] [LawfulBEq R] {ι : Type u} [DecidableEq ι] +lemma toPoly_prod.{u} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] + {ι : Type u} [DecidableEq ι] {s : Finset ι} {f : ι → CPolynomial R} : (∏ j ∈ s, f j).toPoly = ∏ j ∈ s, ((f j).toPoly) := by induction s using Finset.induction_on with @@ -145,10 +145,10 @@ lemma toPoly_prod.{u} {R : Type*} [BEq R] [Field R] [LawfulBEq R] {ι : Type u} | insert a s ha ih => simp [Finset.prod_insert, ha, toPoly_mul, ih] -noncomputable def ringEquiv [LawfulBEq R] : +noncomputable def ringEquiv [LawfulBEq R] [Nontrivial R] : CPolynomial R ≃+* Polynomial R where toFun := CPolynomial.toPoly - invFun := fun p => ⟨p.toImpl, trim_toImpl p⟩ + invFun := fun p => ⟨p.toImpl, isCanonical_toImpl p⟩ left_inv := by unfold Function.LeftInverse; intro x apply Subtype.ext; apply toImpl_toPoly_of_canonical @@ -175,9 +175,8 @@ theorem C_toPoly [LawfulBEq R] (r : R) : (C r).toPoly = Polynomial.C r := by theorem X_toPoly [LawfulBEq R] [Nontrivial R] : (X : CPolynomial R).toPoly = Polynomial.X := by - convert Raw.toPoly_X using 1 - (expose_names; infer_instance) - infer_instance + change (CPolynomial.Raw.X : CPolynomial.Raw R).toPoly = Polynomial.X + exact CPolynomial.Raw.toPoly_X (R := R) theorem eval_toPoly [LawfulBEq R] (x : R) (p : CPolynomial R) : eval x p = p.toPoly.eval x := by @@ -185,8 +184,8 @@ theorem eval_toPoly [LawfulBEq R] (x : R) (p : CPolynomial R) : · rw [ Raw.eval_toPoly_eq_eval ]; rfl · convert Raw.eval_toPoly_eq_eval x p.val -omit [BEq R] in -theorem Raw.eval₂_toPoly {S : Type*} [Semiring S] (f : R →+* S) (x : S) (p : CPolynomial.Raw R) : +theorem Raw.eval₂_toPoly {R : Type*} [Semiring R] {S : Type*} [Semiring S] + (f : R →+* S) (x : S) (p : CPolynomial.Raw R) : p.eval₂ f x = p.toPoly.eval₂ f x := by unfold CompPoly.CPolynomial.Raw.toPoly CompPoly.CPolynomial.Raw.eval₂ rw [← Array.foldl_hom (fun q : R[X] => q.eval₂ f x) @@ -197,9 +196,11 @@ theorem Raw.eval₂_toPoly {S : Type*} [Semiring S] (f : R →+* S) (x : S) (p : rcases t with ⟨a, i⟩ simp [Polynomial.eval₂_add, Polynomial.C_mul_X_pow_eq_monomial] -theorem eval₂_toPoly {S : Type*} [Semiring S] (f : R →+* S) (x : S) (p : CPolynomial R) : +theorem eval₂_toPoly {R : Type*} [Semiring R] {S : Type*} [Semiring S] + (f : R →+* S) (x : S) (p : CPolynomial R) : eval₂ f x p = p.toPoly.eval₂ f x := by - simpa [CompPoly.CPolynomial.eval₂, CompPoly.CPolynomial.toPoly] using + simpa [CompPoly.CPolynomial.eval₂, CompPoly.CPolynomial.toPoly, CompPoly.CPolynomial.Raw.eval₂] + using (Raw.eval₂_toPoly (f := f) (x := x) (p := p.val)) theorem coeff_toPoly [LawfulBEq R] (p : CPolynomial R) (i : ℕ) : diff --git a/docs/wiki/README.md b/docs/wiki/README.md index f7b35ba9..c2e37583 100644 --- a/docs/wiki/README.md +++ b/docs/wiki/README.md @@ -13,6 +13,8 @@ are too specific or too changeable to keep at the repo root. truth. - [`representations-and-bridges.md`](representations-and-bridges.md) - the main polynomial representations and Mathlib bridge layers. +- [`typeclass-minimization.md`](typeclass-minimization.md) - declaration-level + typeclass discipline and minimal-assumption examples. - [`binary-fields-and-ntt.md`](binary-fields-and-ntt.md) - the binary-field stack, GHASH model, and additive-NTT architecture. @@ -25,6 +27,8 @@ are too specific or too changeable to keep at the repo root. - `repo-map.md` for repo structure and work-area routing. - `generated-files.md` for derived outputs and source-of-truth rules. - `representations-and-bridges.md` for representation choice and Mathlib bridges. + - `typeclass-minimization.md` for minimal typeclass assumptions and avoiding + blanket instance scopes. - `binary-fields-and-ntt.md` for the specialized field and NTT stack. - Add new pages when a recurring topic no longer fits cleanly in an existing page. - If a PR changes commands, repo structure, generated-file behavior, or recurring diff --git a/docs/wiki/typeclass-minimization.md b/docs/wiki/typeclass-minimization.md new file mode 100644 index 00000000..b98605d1 --- /dev/null +++ b/docs/wiki/typeclass-minimization.md @@ -0,0 +1,109 @@ +# Typeclass Minimization + +This page records the repo's expectation that new Lean declarations carry the +weakest typeclass assumptions that actually match the code. + +## Core Rule + +- For every new `def`, `instance`, `lemma`, or `theorem`, spell out the minimal + typeclass assumptions needed by that declaration. +- Avoid blanket section-level declarations such as + `variable {R : Type*} [Ring R] [BEq R] [LawfulBEq R]` unless every + declaration in scope genuinely needs all of them. +- Keep definitions as weak as possible even if some later proofs need stronger + assumptions. +- If one theorem in a group needs stronger assumptions than nearby definitions, + strengthen only that theorem instead of the whole section. + +## Preferred Style + +Avoid: + +```lean +variable {R : Type*} [Ring R] [BEq R] [LawfulBEq R] + +def coeff (p : Foo R) : R := ... +def X : Foo R := ... +theorem support_spec (p : Foo R) : ... := ... +``` + +Prefer: + +```lean +def coeff {R : Type*} [Zero R] (p : Foo R) : R := ... + +def X {R : Type*} [Zero R] [One R] : Foo R := ... + +theorem support_spec {R : Type*} [Zero R] [BEq R] (p : Foo R) : ... := ... +``` + +## How To Choose The Weakest Assumptions + +- Use `Zero` for coefficient lookup, support, degree, trimming, and other + zero-sensitive queries. +- Use `Zero` and `One` for constants and variables. +- Use `Add` or `Semiring` only when addition or multiplication is actually used. +- Use `NegZeroClass` for coefficientwise negation facts when the only extra fact + needed is `-0 = 0`. +- Use `Ring` only when the declaration genuinely uses subtraction or additive + inverses in an essential way. +- Add `DecidableEq`, `BEq`, or `LawfulBEq` only when the declaration actually + branches on equality, trims through `BEq`, or uses lemmas that require those + structures. + +## Recent Refactor Examples + +These examples come directly from the recent typeclass-tightening refactor. + +- `CompPoly/Univariate/Quotient.lean` now defines the quotient carrier at + `Zero` level because coefficientwise equivalence only needs zero-padding: + +```lean +def QuotientCPolynomial (R : Type*) [Zero R] := + Quotient (@Raw.instSetoidCPolynomial R _) +``` + +- `CompPoly/Bivariate/ToPoly.lean` now states bridge lemmas like + `evalEval_toPoly` at `Semiring` level because the proof uses only additive and + multiplicative structure: + +```lean +theorem evalEval_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] + (x y : R) (f : CBivariate R) : + @CBivariate.evalEval R _ _ _ _ x y f = (toPoly f).evalEval x y := by + ... +``` + +- `CompPoly/Univariate/Raw/Proofs.lean` now keeps `neg_coeff` at + `NegZeroClass` rather than `Ring` because coefficientwise negation only needs + `-0 = 0`: + +```lean +lemma neg_coeff {R : Type*} [NegZeroClass R] (p : CPolynomial.Raw R) (i : ℕ) : + p.neg.coeff i = - p.coeff i := by + ... +``` + +- `CompPoly/Univariate/Raw/Division.lean` no longer carries a blanket `Ring` + assumption at section scope because every definition already has its own + `[Field R]` requirement: + +```lean +section Division + +variable [BEq R] + +def divModByMonicAux [Field R] ... +``` + +## Review Checklist + +Before finishing a change, check: + +- Could this declaration drop from `Ring` to `Semiring`? +- Could it drop from `Semiring` to `Zero`, `One`, `Add`, or `Mul`? +- Is `NegZeroClass` enough instead of `Ring`? +- Is a section-level `variable [...]` forcing stronger assumptions onto nearby + declarations that do not need them? +- If a stronger theorem is unavoidable, can the stronger assumptions be made + local to that theorem? diff --git a/tests/CompPolyTests.lean b/tests/CompPolyTests.lean index 8f758912..e679534e 100644 --- a/tests/CompPolyTests.lean +++ b/tests/CompPolyTests.lean @@ -1,6 +1,8 @@ import CompPolyTests.Univariate.Raw import CompPolyTests.Univariate.Basic +import CompPolyTests.Univariate.Linear import CompPolyTests.Univariate.ToPoly +import CompPolyTests.Bivariate.Basic import CompPolyTests.BF128GhashPrelude import CompPolyTests.Multivariate.CMvMonomial import CompPolyTests.Multivariate.Restrict diff --git a/tests/CompPolyTests/Bivariate/Basic.lean b/tests/CompPolyTests/Bivariate/Basic.lean new file mode 100644 index 00000000..8acaf2d6 --- /dev/null +++ b/tests/CompPolyTests/Bivariate/Basic.lean @@ -0,0 +1,36 @@ +/- +Copyright (c) 2025 CompPoly. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Derek Sorensen +-/ +import CompPoly.Bivariate.ToPoly + +/-! + # Bivariate Basic Tests + + Lightweight regressions for the canonical Y-facing API and its `toPoly` transport. +-/ + +namespace CompPoly +namespace CBivariate + +example (f : CBivariate ℚ) : (toPoly f).natDegree = f.natDegreeY := by + simpa using natDegreeY_toPoly (R := ℚ) (f := f) + +example (f : CBivariate ℚ) : + (leadingCoeffY (R := ℚ) f).toPoly = (toPoly f).leadingCoeff := by + simpa using leadingCoeffY_toPoly (R := ℚ) (f := f) + +example : coeff (R := ℚ) (monomialXY (R := ℚ) 2 1 5) 2 1 = 5 := by + change ((CPolynomial.monomial 1 (CPolynomial.monomial (R := ℚ) 2 5)).coeff 1).coeff 2 = 5 + have h_outer : + (CPolynomial.monomial 1 (CPolynomial.monomial (R := ℚ) 2 5)).coeff 1 = + CPolynomial.monomial (R := ℚ) 2 5 := by + simpa using + (CPolynomial.coeff_monomial (R := CPolynomial ℚ) 1 1 + (CPolynomial.monomial (R := ℚ) 2 5)) + rw [h_outer] + simpa using (CPolynomial.coeff_monomial (R := ℚ) 2 2 5) + +end CBivariate +end CompPoly diff --git a/tests/CompPolyTests/Univariate/Linear.lean b/tests/CompPolyTests/Univariate/Linear.lean new file mode 100644 index 00000000..98acdc70 --- /dev/null +++ b/tests/CompPolyTests/Univariate/Linear.lean @@ -0,0 +1,88 @@ +/- +Copyright (c) 2025 CompPoly. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Derek Sorensen +-/ +import CompPoly.Univariate.ToPoly.Degree + +/-! + # Univariate Linear Regression Tests + + Compile-time regressions for the instance-stable bounded-degree API. +-/ + +namespace CompPoly +namespace CPolynomial + +private def nat_beq_eq : BEq Nat := ⟨fun a b => decide (a = b)⟩ + +private theorem nat_lawful_beq_eq : @LawfulBEq Nat nat_beq_eq := by + letI : BEq Nat := nat_beq_eq + refine { rfl := ?_, eq_of_beq := ?_ } + · intro a + simp [nat_beq_eq] + · intro a b h + simpa [nat_beq_eq] using h + +private def nat_beq_succ : BEq Nat := ⟨fun a b => decide (a.succ = b.succ)⟩ + +private theorem nat_lawful_beq_succ : @LawfulBEq Nat nat_beq_succ := by + letI : BEq Nat := nat_beq_succ + refine { rfl := ?_, eq_of_beq := ?_ } + · intro a + simp [nat_beq_succ] + · intro a b h + exact Nat.succ.inj <| by simpa [nat_beq_succ] using h + +private def leftPoly : CPolynomial Nat := + @CPolynomial.monomial Nat _ nat_beq_eq nat_lawful_beq_eq _ 1 7 + +private def leftDegreeLT : ↥(CPolynomial.degreeLT (R := Nat) 3) := by + refine ⟨leftPoly, ?_⟩ + rw [CPolynomial.mem_degreeLT_iff_size_le] + simp [leftPoly, CPolynomial.monomial, CPolynomial.Raw.monomial] + +section CrossInstance + +local instance : BEq Nat := nat_beq_succ +local instance : LawfulBEq Nat := nat_lawful_beq_succ + +/-- Reuse a `CPolynomial` built under one lawful `BEq Nat` under another, with no cast. -/ +private def reusedPoly : CPolynomial Nat := leftPoly + +/-- Reuse a nonzero bounded-degree subtype value under a different lawful `BEq Nat`, +with no cast. -/ +private def reusedDegreeLT : ↥(CPolynomial.degreeLT (R := Nat) 3) := leftDegreeLT + +example : reusedPoly.coeff 1 = 7 := by + simpa [reusedPoly, leftPoly] using CPolynomial.coeff_monomial (R := Nat) 1 1 7 + +example : reusedDegreeLT.1 = reusedPoly := rfl + +example : reusedDegreeLT.1 ∈ CPolynomial.degreeLT (R := Nat) 3 := reusedDegreeLT.2 + +example : (reusedDegreeLT + reusedDegreeLT).1.coeff 1 = 14 := by + calc + (reusedDegreeLT + reusedDegreeLT).1.coeff 1 = + reusedDegreeLT.1.coeff 1 + reusedDegreeLT.1.coeff 1 := by + simpa using CPolynomial.coeff_add reusedDegreeLT.1 reusedDegreeLT.1 1 + _ = 7 + 7 := by + congr + _ = 14 := by norm_num + +end CrossInstance + +private def intPoly : CPolynomial Int := + CPolynomial.monomial 1 7 + +private def intDegreeLT : ↥(CPolynomial.degreeLT (R := Int) 3) := by + refine ⟨intPoly, ?_⟩ + rw [CPolynomial.mem_degreeLT_iff_size_le] + simp [intPoly, CPolynomial.monomial, CPolynomial.Raw.monomial] + +example : CPolynomial.degreeLTEquiv (R := Int) 3 intDegreeLT ⟨1, by decide⟩ = 7 := by + simpa [CPolynomial.degreeLTEquiv, CPolynomial.degreeLTCoeffs, intDegreeLT, intPoly] using + CPolynomial.coeff_monomial (R := Int) 1 1 7 + +end CPolynomial +end CompPoly