From efa40a333461c95699f05cc99c57b57ac0e37694 Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Wed, 18 Feb 2026 10:24:37 +0000 Subject: [PATCH 01/18] first commit --- CompPoly.lean | 1 + CompPoly/Bivariate/Basic.lean | 0 2 files changed, 1 insertion(+) create mode 100644 CompPoly/Bivariate/Basic.lean diff --git a/CompPoly.lean b/CompPoly.lean index 9ef5636..2f05478 100644 --- a/CompPoly.lean +++ b/CompPoly.lean @@ -20,3 +20,4 @@ import CompPoly.Univariate.Basic import CompPoly.Univariate.Quotient import CompPoly.Univariate.ToPoly import CompPoly.Univariate.Lagrange +import CompPoly.Bivariate.Basic diff --git a/CompPoly/Bivariate/Basic.lean b/CompPoly/Bivariate/Basic.lean new file mode 100644 index 0000000..e69de29 From 8318b5ff366520493bd46fb6c974f7159a21ab55 Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Wed, 18 Feb 2026 11:17:23 +0000 Subject: [PATCH 02/18] feat: basic skeleton for bivariate polynomials --- CompPoly.lean | 1 + CompPoly/Bivariate/Basic.lean | 131 +++++++++++++++++++++++++++++++++ CompPoly/Bivariate/README.md | 20 +++++ CompPoly/Bivariate/ToPoly.lean | 54 ++++++++++++++ 4 files changed, 206 insertions(+) create mode 100644 CompPoly/Bivariate/README.md create mode 100644 CompPoly/Bivariate/ToPoly.lean diff --git a/CompPoly.lean b/CompPoly.lean index 2f05478..16a8c68 100644 --- a/CompPoly.lean +++ b/CompPoly.lean @@ -21,3 +21,4 @@ import CompPoly.Univariate.Quotient import CompPoly.Univariate.ToPoly import CompPoly.Univariate.Lagrange import CompPoly.Bivariate.Basic +import CompPoly.Bivariate.ToPoly diff --git a/CompPoly/Bivariate/Basic.lean b/CompPoly/Bivariate/Basic.lean index e69de29..47fa259 100644 --- a/CompPoly/Bivariate/Basic.lean +++ b/CompPoly/Bivariate/Basic.lean @@ -0,0 +1,131 @@ +/- +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.Basic + +/-! +# Computable Bivariate Polynomials + +This file defines `CBivariate R`, the computable representation of bivariate polynomials with +coefficients in `R`. The type is `CPolynomial (CPolynomial R)`, i.e. polynomials in `Y` with +coefficients that are polynomials in `X`, matching Mathlib's `R[X][Y]` +(i.e. `Polynomial (Polynomial R)`). + +The design is intended to be compatible with: +- Mathlib's `Polynomial.Bivariate` (see `CompPoly/Bivariate/ToPoly.lean`) +- ArkLib's `Polynomial.Bivariate` interface (see ArkLib/Data/Polynomial/Bivariate.lean and + ArkLib/Data/CodingTheory/PolishchukSpielman/Degrees.lean, BCIKS20.lean, etc.) +-/ + +namespace CompPoly + +/-- Computable bivariate polynomials: `F[X][Y]` as `CPolynomial (CPolynomial R)`. + + 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] + [BEq (CPolynomial R)] := CPolynomial (CPolynomial R) + +namespace CBivariate + +-- TODO prove that BEq R => BEq (CPolynomial R) +variable {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [BEq (CPolynomial R)] + +/-- Extensionality: two bivariate polynomials are equal iff their underlying values are. -/ +@[ext] theorem ext {p q : CBivariate R} (h : p.val = q.val) : p = q := + CPolynomial.ext h + +/-- Coerce to the underlying univariate polynomial (in Y) with polynomial coefficients. -/ +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))) + +-- --------------------------------------------------------------------------- +-- Operation stubs (for ArkLib compatibility; proofs deferred) +-- --------------------------------------------------------------------------- +-- ArkLib's Polynomial.Bivariate uses: coeff, natDegreeY, degreeX, totalDegree, +-- evalX, evalY, leadingCoeffY, swap. These will be implemented and proven +-- equivalent to Mathlib/ArkLib via ToPoly.lean. +-- --------------------------------------------------------------------------- + +section Operations + +-- TODO simplify these variables so only assumptions on R are needed if possible +variable (R : Type*) [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] [Semiring R] + [BEq (CPolynomial R)] [LawfulBEq (CPolynomial R)] [DecidableEq (CPolynomial R)] + +/-- Constant as a bivariate polynomial. Mathlib: `Polynomial.Bivariate.CC`. -/ +def CC (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 C_X [Nontrivial R] : CBivariate R := CPolynomial.C CPolynomial.X + +/-- The variable Y (outer variable). Monomial `Y^1` with coefficient 1. -/ +def Y : CBivariate R := CPolynomial.monomial 1 (CPolynomial.C 1) + +/-- Monomial `c * X^n * Y^m`. ArkLib: `Polynomial.Bivariate.monomialXY`. -/ +def monomialXY (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 := + (f.val.coeff j).coeff i + +/-- The Y-support: indices j such that the coefficient of Y^j is nonzero. -/ +def support (f : CBivariate R) : Finset ℕ := CPolynomial.support f + +/-- The `Y`-degree (degree when viewed as a polynomial in `Y`). + ArkLib: `Polynomial.Bivariate.natDegreeY`. -/ +def natDegreeY (f : CBivariate R) : ℕ := + f.val.natDegree + +/-- The `X`-degree: maximum over all Y-coefficients of their degree in X. + ArkLib: `Polynomial.Bivariate.degreeX`. -/ +def degreeX (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) : ℕ := + (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`. + TODO: implement via mapping each Y-coefficient through `eval a`. -/ +def evalX (a : R) (f : CBivariate R) : CPolynomial R := sorry + +/-- 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 := + f.val.eval (CPolynomial.C a) + +/-- Full evaluation at `(x, y)`: `p(x, y)`. Equivalently `(evalY y f).eval x`. + Mathlib: `Polynomial.evalEval`. -/ +def evalEval (x y : R) (f : CBivariate R) : R := + CPolynomial.eval x (f.val.eval (CPolynomial.C y)) + +/-- Leading coefficient when viewed as a polynomial in Y. + ArkLib: `Polynomial.Bivariate.leadingCoeffY`. -/ +def leadingCoeffY (f : CBivariate R) : CPolynomial R := + f.val.coeff (f.val.natDegree) + +/-- Swap the roles of X and Y. + ArkLib/Mathlib: `Polynomial.Bivariate.swap`. -/ +def swap (f : CBivariate R) : CBivariate R := sorry + +/-- Leading coefficient when viewed as a polynomial in X. + The coefficient of X^(degreeX f): a polynomial in Y. Equivalently, `leadingCoeffY (swap f)`. + TODO: implement as `leadingCoeffY (swap f)` once `swap` has a computable definition. -/ +def leadingCoeffX (f : CBivariate R) : CPolynomial R := sorry -- leadingCoeffY (swap f) + +end Operations + +end CBivariate + +end CompPoly diff --git a/CompPoly/Bivariate/README.md b/CompPoly/Bivariate/README.md new file mode 100644 index 0000000..5e306c0 --- /dev/null +++ b/CompPoly/Bivariate/README.md @@ -0,0 +1,20 @@ +# Bivariate Polynomials + +Formally verified computable bivariate polynomials for [CompPoly](../README.md), represented as `CPolynomial (CPolynomial R)` — polynomials in Y whose coefficients are univariate polynomials in X. Matches Mathlib's `R[X][Y]` and is compatible with [ArkLib](https://github.com/Verified-zkEVM/ArkLib)'s `Polynomial.Bivariate` interface. + +## Type + +| Type | Description | +|------|-------------| +| `CBivariate R` | `CPolynomial (CPolynomial R)` — canonical polynomials in Y with polynomial-in-X coefficients. Same structure as Mathlib's `Polynomial (Polynomial R)`. | + +## Modules + +- **Basic.lean** — Type definition, constructors (`CC`, `C_X`, `Y`, `monomialXY`), operations (`coeff`, `evalX`, `evalY`, `evalEval`, `degreeX`, `natDegreeY`, `totalDegree`, `leadingCoeffY`, `leadingCoeffX`, `swap`, `support`). +- **ToPoly.lean** — Conversion to/from Mathlib's `R[X][Y]` via `toPoly` and `ofPoly` (stubs; proofs to follow). + +## Indexing + +- `coeff f i j` = coefficient of `X^i Y^j` (X is inner variable, Y is outer). +- Outer structure: indexed by powers of Y. +- Inner structure: each Y-coefficient is a `CPolynomial R` (polynomial in X). diff --git a/CompPoly/Bivariate/ToPoly.lean b/CompPoly/Bivariate/ToPoly.lean new file mode 100644 index 0000000..84f457e --- /dev/null +++ b/CompPoly/Bivariate/ToPoly.lean @@ -0,0 +1,54 @@ +/- +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.Basic +import CompPoly.Univariate.ToPoly +import Mathlib.Algebra.Polynomial.Bivariate + +/-! +# Equivalence with Mathlib Bivariate Polynomials + +This file establishes the conversion from `CBivariate R` to Mathlib's `R[X][Y]` +(`Polynomial (Polynomial R)`). + +The main definition is: +- `toPoly`: converts `CBivariate R` to `R[X][Y]` + +Proofs that `toPoly` preserves evaluation, coefficients, degrees, etc. (and that it +forms an isomorphism with an inverse `ofPoly`) will be added as the implementation +is completed. The target interface matches ArkLib's `Polynomial.Bivariate` and +Mathlib's `Polynomial.Bivariate`. +-/ + +open Polynomial +open scoped Polynomial.Bivariate + +namespace CompPoly + +namespace CBivariate + +/-- Convert `CBivariate R` to Mathlib's bivariate polynomial `R[X][Y]`. + + Intended implementation: map each Y-coefficient (a `CPolynomial R`) through + `CPolynomial.toPoly` to obtain `Polynomial R`, then build `Polynomial (Polynomial R)` + via `eval₂` (analogous to univariate `Raw.toPoly`). + -/ +noncomputable def toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] + [BEq (CPolynomial R)] (p : CBivariate R) : R[X][Y] := sorry + +/-- Convert Mathlib's `R[X][Y]` to `CBivariate R` (inverse of `toPoly`). + + Intended implementation: extract each Y-coefficient via `p.coeff`, convert to + `CPolynomial R` via `Polynomial.toImpl`, then build canonical bivariate. + TODO: implement and prove round-trip lemmas. -/ +noncomputable def ofPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] + [BEq (CPolynomial R)] (p : R[X][Y]) : CBivariate R := sorry + +-- TODO: toPoly_ofPoly, ofPoly_toPoly (round-trips), ring equiv, evalEval/toPoly compatibility + +end CBivariate + +end CompPoly From fd0c59febc2bcd652df174cb8e2a7964bc19ba65 Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Wed, 18 Feb 2026 15:41:40 +0000 Subject: [PATCH 03/18] feat: adjusting the namespace to be within CPolynomial .. experimentally --- CompPoly/Bivariate/Basic.lean | 46 +++++++++++++++++----------------- CompPoly/Bivariate/ToPoly.lean | 16 ++++++------ 2 files changed, 31 insertions(+), 31 deletions(-) diff --git a/CompPoly/Bivariate/Basic.lean b/CompPoly/Bivariate/Basic.lean index 47fa259..fd2c10b 100644 --- a/CompPoly/Bivariate/Basic.lean +++ b/CompPoly/Bivariate/Basic.lean @@ -9,7 +9,7 @@ import CompPoly.Univariate.Basic /-! # Computable Bivariate Polynomials -This file defines `CBivariate R`, the computable representation of bivariate polynomials with +This file defines `Bivariate R`, the computable representation of bivariate polynomials with coefficients in `R`. The type is `CPolynomial (CPolynomial R)`, i.e. polynomials in `Y` with coefficients that are polynomials in `X`, matching Mathlib's `R[X][Y]` (i.e. `Polynomial (Polynomial R)`). @@ -24,26 +24,26 @@ namespace CompPoly /-- Computable bivariate polynomials: `F[X][Y]` as `CPolynomial (CPolynomial R)`. - Each `p : CBivariate R` is a polynomial in `Y` whose coefficients are univariate polynomials + Each `p : Bivariate 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 CPolynomial.Bivariate (R : Type*) [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [BEq (CPolynomial R)] := CPolynomial (CPolynomial R) -namespace CBivariate +namespace CPolynomial.Bivariate -- TODO prove that BEq R => BEq (CPolynomial R) variable {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [BEq (CPolynomial R)] /-- Extensionality: two bivariate polynomials are equal iff their underlying values are. -/ -@[ext] theorem ext {p q : CBivariate R} (h : p.val = q.val) : p = q := +@[ext] theorem ext {p q : Bivariate R} (h : p.val = q.val) : p = q := CPolynomial.ext h /-- Coerce to the underlying univariate polynomial (in Y) with polynomial coefficients. -/ -instance : Coe (CBivariate R) (CPolynomial (CPolynomial R)) where coe := id +instance : Coe (Bivariate R) (CPolynomial (CPolynomial R)) where coe := id /-- The zero bivariate polynomial is canonical. -/ -instance : Inhabited (CBivariate R) := inferInstanceAs (Inhabited (CPolynomial (CPolynomial R))) +instance : Inhabited (Bivariate R) := inferInstanceAs (Inhabited (CPolynomial (CPolynomial R))) -- --------------------------------------------------------------------------- -- Operation stubs (for ArkLib compatibility; proofs deferred) @@ -60,72 +60,72 @@ variable (R : Type*) [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] [Semir [BEq (CPolynomial R)] [LawfulBEq (CPolynomial R)] [DecidableEq (CPolynomial R)] /-- Constant as a bivariate polynomial. Mathlib: `Polynomial.Bivariate.CC`. -/ -def CC (r : R) : CBivariate R := CPolynomial.C (CPolynomial.C r) +def CC (r : R) : Bivariate R := CPolynomial.C (CPolynomial.C r) /-- The variable X (inner variable). As bivariate: polynomial in Y with single coeff `X` at Y^0. -/ -def C_X [Nontrivial R] : CBivariate R := CPolynomial.C CPolynomial.X +def C_X [Nontrivial R] : Bivariate R := CPolynomial.C CPolynomial.X /-- The variable Y (outer variable). Monomial `Y^1` with coefficient 1. -/ -def Y : CBivariate R := CPolynomial.monomial 1 (CPolynomial.C 1) +def Y : Bivariate R := CPolynomial.monomial 1 (CPolynomial.C 1) /-- Monomial `c * X^n * Y^m`. ArkLib: `Polynomial.Bivariate.monomialXY`. -/ -def monomialXY (n m : ℕ) (c : R) : CBivariate R := +def monomialXY (n m : ℕ) (c : R) : Bivariate 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 (f : Bivariate 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 support (f : CBivariate R) : Finset ℕ := CPolynomial.support f +def support (f : Bivariate R) : Finset ℕ := CPolynomial.support f /-- The `Y`-degree (degree when viewed as a polynomial in `Y`). ArkLib: `Polynomial.Bivariate.natDegreeY`. -/ -def natDegreeY (f : CBivariate R) : ℕ := +def natDegreeY (f : Bivariate R) : ℕ := f.val.natDegree /-- The `X`-degree: maximum over all Y-coefficients of their degree in X. ArkLib: `Polynomial.Bivariate.degreeX`. -/ -def degreeX (f : CBivariate R) : ℕ := +def degreeX (f : Bivariate 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 (f : Bivariate 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`. TODO: implement via mapping each Y-coefficient through `eval a`. -/ -def evalX (a : R) (f : CBivariate R) : CPolynomial R := sorry +def evalX (a : R) (f : Bivariate R) : CPolynomial R := sorry /-- 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 (a : R) (f : Bivariate R) : CPolynomial R := f.val.eval (CPolynomial.C a) /-- Full evaluation at `(x, y)`: `p(x, y)`. Equivalently `(evalY y f).eval x`. Mathlib: `Polynomial.evalEval`. -/ -def evalEval (x y : R) (f : CBivariate R) : R := +def evalEval (x y : R) (f : Bivariate R) : R := CPolynomial.eval x (f.val.eval (CPolynomial.C y)) /-- Leading coefficient when viewed as a polynomial in Y. ArkLib: `Polynomial.Bivariate.leadingCoeffY`. -/ -def leadingCoeffY (f : CBivariate R) : CPolynomial R := +def leadingCoeffY (f : Bivariate R) : CPolynomial R := f.val.coeff (f.val.natDegree) /-- Swap the roles of X and Y. ArkLib/Mathlib: `Polynomial.Bivariate.swap`. -/ -def swap (f : CBivariate R) : CBivariate R := sorry +def swap (f : Bivariate R) : Bivariate R := sorry /-- Leading coefficient when viewed as a polynomial in X. The coefficient of X^(degreeX f): a polynomial in Y. Equivalently, `leadingCoeffY (swap f)`. TODO: implement as `leadingCoeffY (swap f)` once `swap` has a computable definition. -/ -def leadingCoeffX (f : CBivariate R) : CPolynomial R := sorry -- leadingCoeffY (swap f) +def leadingCoeffX (f : Bivariate R) : CPolynomial R := sorry -- leadingCoeffY (swap f) end Operations -end CBivariate +end CPolynomial.Bivariate end CompPoly diff --git a/CompPoly/Bivariate/ToPoly.lean b/CompPoly/Bivariate/ToPoly.lean index 84f457e..51a81e8 100644 --- a/CompPoly/Bivariate/ToPoly.lean +++ b/CompPoly/Bivariate/ToPoly.lean @@ -11,11 +11,11 @@ import Mathlib.Algebra.Polynomial.Bivariate /-! # Equivalence with Mathlib Bivariate Polynomials -This file establishes the conversion from `CBivariate R` to Mathlib's `R[X][Y]` +This file establishes the conversion from `Bivariate R` to Mathlib's `R[X][Y]` (`Polynomial (Polynomial R)`). The main definition is: -- `toPoly`: converts `CBivariate R` to `R[X][Y]` +- `toPoly`: converts `Bivariate R` to `R[X][Y]` Proofs that `toPoly` preserves evaluation, coefficients, degrees, etc. (and that it forms an isomorphism with an inverse `ofPoly`) will be added as the implementation @@ -28,27 +28,27 @@ open scoped Polynomial.Bivariate namespace CompPoly -namespace CBivariate +namespace CPolynomial.Bivariate -/-- Convert `CBivariate R` to Mathlib's bivariate polynomial `R[X][Y]`. +/-- Convert `Bivariate R` to Mathlib's bivariate polynomial `R[X][Y]`. Intended implementation: map each Y-coefficient (a `CPolynomial R`) through `CPolynomial.toPoly` to obtain `Polynomial R`, then build `Polynomial (Polynomial R)` via `eval₂` (analogous to univariate `Raw.toPoly`). -/ noncomputable def toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] - [BEq (CPolynomial R)] (p : CBivariate R) : R[X][Y] := sorry + [BEq (CPolynomial R)] (p : Bivariate R) : R[X][Y] := sorry -/-- Convert Mathlib's `R[X][Y]` to `CBivariate R` (inverse of `toPoly`). +/-- Convert Mathlib's `R[X][Y]` to `Bivariate R` (inverse of `toPoly`). Intended implementation: extract each Y-coefficient via `p.coeff`, convert to `CPolynomial R` via `Polynomial.toImpl`, then build canonical bivariate. TODO: implement and prove round-trip lemmas. -/ noncomputable def ofPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] - [BEq (CPolynomial R)] (p : R[X][Y]) : CBivariate R := sorry + [BEq (CPolynomial R)] (p : R[X][Y]) : Bivariate R := sorry -- TODO: toPoly_ofPoly, ofPoly_toPoly (round-trips), ring equiv, evalEval/toPoly compatibility -end CBivariate +end CPolynomial.Bivariate end CompPoly From 69b697f87a4997837d5c64089f501ff0371978b6 Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Wed, 18 Feb 2026 16:39:03 +0000 Subject: [PATCH 04/18] feat: simplify typeclass instances --- CompPoly/Bivariate/Basic.lean | 17 +++++++---------- CompPoly/Bivariate/ToPoly.lean | 4 ++-- CompPoly/Univariate/Basic.lean | 19 +++++++++++++++++++ 3 files changed, 28 insertions(+), 12 deletions(-) diff --git a/CompPoly/Bivariate/Basic.lean b/CompPoly/Bivariate/Basic.lean index fd2c10b..66a2bcc 100644 --- a/CompPoly/Bivariate/Basic.lean +++ b/CompPoly/Bivariate/Basic.lean @@ -27,13 +27,12 @@ namespace CompPoly Each `p : Bivariate 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 CPolynomial.Bivariate (R : Type*) [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] - [BEq (CPolynomial R)] := CPolynomial (CPolynomial R) +def CPolynomial.Bivariate (R : Type*) [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] := + CPolynomial (CPolynomial R) namespace CPolynomial.Bivariate --- TODO prove that BEq R => BEq (CPolynomial R) -variable {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [BEq (CPolynomial R)] +variable {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] /-- Extensionality: two bivariate polynomials are equal iff their underlying values are. -/ @[ext] theorem ext {p q : Bivariate R} (h : p.val = q.val) : p = q := @@ -55,21 +54,19 @@ instance : Inhabited (Bivariate R) := inferInstanceAs (Inhabited (CPolynomial (C section Operations --- TODO simplify these variables so only assumptions on R are needed if possible -variable (R : Type*) [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] [Semiring R] - [BEq (CPolynomial R)] [LawfulBEq (CPolynomial R)] [DecidableEq (CPolynomial R)] +variable (R : Type*) [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] /-- Constant as a bivariate polynomial. Mathlib: `Polynomial.Bivariate.CC`. -/ def CC (r : R) : Bivariate R := CPolynomial.C (CPolynomial.C r) /-- The variable X (inner variable). As bivariate: polynomial in Y with single coeff `X` at Y^0. -/ -def C_X [Nontrivial R] : Bivariate R := CPolynomial.C CPolynomial.X +def C_X : Bivariate R := CPolynomial.C CPolynomial.X /-- The variable Y (outer variable). Monomial `Y^1` with coefficient 1. -/ -def Y : Bivariate R := CPolynomial.monomial 1 (CPolynomial.C 1) +def Y [DecidableEq R] : Bivariate R := CPolynomial.monomial 1 (CPolynomial.C 1) /-- Monomial `c * X^n * Y^m`. ArkLib: `Polynomial.Bivariate.monomialXY`. -/ -def monomialXY (n m : ℕ) (c : R) : Bivariate R := +def monomialXY [DecidableEq R] (n m : ℕ) (c : R) : Bivariate 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) diff --git a/CompPoly/Bivariate/ToPoly.lean b/CompPoly/Bivariate/ToPoly.lean index 51a81e8..3f70d7f 100644 --- a/CompPoly/Bivariate/ToPoly.lean +++ b/CompPoly/Bivariate/ToPoly.lean @@ -37,7 +37,7 @@ namespace CPolynomial.Bivariate via `eval₂` (analogous to univariate `Raw.toPoly`). -/ noncomputable def toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] - [BEq (CPolynomial R)] (p : Bivariate R) : R[X][Y] := sorry + (p : Bivariate R) : R[X][Y] := sorry /-- Convert Mathlib's `R[X][Y]` to `Bivariate R` (inverse of `toPoly`). @@ -45,7 +45,7 @@ noncomputable def toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semir `CPolynomial R` via `Polynomial.toImpl`, then build canonical bivariate. TODO: implement and prove round-trip lemmas. -/ noncomputable def ofPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] - [BEq (CPolynomial R)] (p : R[X][Y]) : Bivariate R := sorry + (p : R[X][Y]) : Bivariate R := sorry -- TODO: toPoly_ofPoly, ofPoly_toPoly (round-trips), ring equiv, evalEval/toPoly compatibility diff --git a/CompPoly/Univariate/Basic.lean b/CompPoly/Univariate/Basic.lean index be5a63a..638c743 100644 --- a/CompPoly/Univariate/Basic.lean +++ b/CompPoly/Univariate/Basic.lean @@ -44,6 +44,25 @@ instance [Semiring R] : Coe (CPolynomial R) (CPolynomial.Raw R) where coe := Sub /-- The zero polynomial is canonical. -/ instance [Semiring R] : Inhabited (CPolynomial R) := ⟨#[], Trim.canonical_empty⟩ +/-- `CPolynomial R` has `BEq` when `R` does, comparing the underlying coefficient arrays. -/ +instance (R : Type*) [BEq R] [Semiring 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 + rfl := by + have h_raw : ∀ (a : CPolynomial.Raw R), a == a ↔ a = a := by + aesop + convert h_raw _ + swap + exact #[] + simp +decide [ BEq.beq ] + 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 + section Operations variable [Semiring R] [LawfulBEq R] From 7fb729db60dac9c55ddec9393477be43189f0d37 Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Wed, 18 Feb 2026 16:47:21 +0000 Subject: [PATCH 05/18] fix: namespace simplification --- CompPoly/Bivariate/Basic.lean | 46 +++++++++++++++++----------------- CompPoly/Bivariate/ToPoly.lean | 16 ++++++------ 2 files changed, 31 insertions(+), 31 deletions(-) diff --git a/CompPoly/Bivariate/Basic.lean b/CompPoly/Bivariate/Basic.lean index 66a2bcc..a804be3 100644 --- a/CompPoly/Bivariate/Basic.lean +++ b/CompPoly/Bivariate/Basic.lean @@ -9,7 +9,7 @@ import CompPoly.Univariate.Basic /-! # Computable Bivariate Polynomials -This file defines `Bivariate R`, the computable representation of bivariate polynomials with +This file defines `CBivariate R`, the computable representation of bivariate polynomials with coefficients in `R`. The type is `CPolynomial (CPolynomial R)`, i.e. polynomials in `Y` with coefficients that are polynomials in `X`, matching Mathlib's `R[X][Y]` (i.e. `Polynomial (Polynomial R)`). @@ -24,25 +24,25 @@ namespace CompPoly /-- Computable bivariate polynomials: `F[X][Y]` as `CPolynomial (CPolynomial R)`. - Each `p : Bivariate R` is a polynomial in `Y` whose coefficients are univariate polynomials + 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 CPolynomial.Bivariate (R : Type*) [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] := +def CBivariate (R : Type*) [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] := CPolynomial (CPolynomial R) -namespace CPolynomial.Bivariate +namespace CBivariate variable {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] /-- Extensionality: two bivariate polynomials are equal iff their underlying values are. -/ -@[ext] theorem ext {p q : Bivariate R} (h : p.val = q.val) : p = q := +@[ext] theorem ext {p q : CBivariate R} (h : p.val = q.val) : p = q := CPolynomial.ext h /-- Coerce to the underlying univariate polynomial (in Y) with polynomial coefficients. -/ -instance : Coe (Bivariate R) (CPolynomial (CPolynomial R)) where coe := id +instance : Coe (CBivariate R) (CPolynomial (CPolynomial R)) where coe := id /-- The zero bivariate polynomial is canonical. -/ -instance : Inhabited (Bivariate R) := inferInstanceAs (Inhabited (CPolynomial (CPolynomial R))) +instance : Inhabited (CBivariate R) := inferInstanceAs (Inhabited (CPolynomial (CPolynomial R))) -- --------------------------------------------------------------------------- -- Operation stubs (for ArkLib compatibility; proofs deferred) @@ -57,72 +57,72 @@ 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) : Bivariate R := CPolynomial.C (CPolynomial.C r) +def CC (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 C_X : Bivariate R := CPolynomial.C CPolynomial.X +def C_X : CBivariate R := CPolynomial.C CPolynomial.X /-- The variable Y (outer variable). Monomial `Y^1` with coefficient 1. -/ -def Y [DecidableEq R] : Bivariate R := CPolynomial.monomial 1 (CPolynomial.C 1) +def Y [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) : Bivariate R := +def monomialXY [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 : Bivariate R) (i j : ℕ) : R := +def coeff (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 support (f : Bivariate R) : Finset ℕ := CPolynomial.support f +def support (f : CBivariate R) : Finset ℕ := CPolynomial.support f /-- The `Y`-degree (degree when viewed as a polynomial in `Y`). ArkLib: `Polynomial.Bivariate.natDegreeY`. -/ -def natDegreeY (f : Bivariate R) : ℕ := +def natDegreeY (f : CBivariate R) : ℕ := f.val.natDegree /-- The `X`-degree: maximum over all Y-coefficients of their degree in X. ArkLib: `Polynomial.Bivariate.degreeX`. -/ -def degreeX (f : Bivariate R) : ℕ := +def degreeX (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 : Bivariate R) : ℕ := +def totalDegree (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`. TODO: implement via mapping each Y-coefficient through `eval a`. -/ -def evalX (a : R) (f : Bivariate R) : CPolynomial R := sorry +def evalX (a : R) (f : CBivariate R) : CPolynomial R := sorry /-- Evaluate in the second variable (Y) at `a`, yielding a univariate polynomial in X. ArkLib: `Polynomial.Bivariate.evalY`. -/ -def evalY (a : R) (f : Bivariate R) : CPolynomial R := +def evalY (a : R) (f : CBivariate R) : CPolynomial R := f.val.eval (CPolynomial.C a) /-- Full evaluation at `(x, y)`: `p(x, y)`. Equivalently `(evalY y f).eval x`. Mathlib: `Polynomial.evalEval`. -/ -def evalEval (x y : R) (f : Bivariate R) : R := +def evalEval (x y : R) (f : CBivariate R) : R := CPolynomial.eval x (f.val.eval (CPolynomial.C y)) /-- Leading coefficient when viewed as a polynomial in Y. ArkLib: `Polynomial.Bivariate.leadingCoeffY`. -/ -def leadingCoeffY (f : Bivariate R) : CPolynomial R := +def leadingCoeffY (f : CBivariate R) : CPolynomial R := f.val.coeff (f.val.natDegree) /-- Swap the roles of X and Y. ArkLib/Mathlib: `Polynomial.Bivariate.swap`. -/ -def swap (f : Bivariate R) : Bivariate R := sorry +def swap (f : CBivariate R) : CBivariate R := sorry /-- Leading coefficient when viewed as a polynomial in X. The coefficient of X^(degreeX f): a polynomial in Y. Equivalently, `leadingCoeffY (swap f)`. TODO: implement as `leadingCoeffY (swap f)` once `swap` has a computable definition. -/ -def leadingCoeffX (f : Bivariate R) : CPolynomial R := sorry -- leadingCoeffY (swap f) +def leadingCoeffX (f : CBivariate R) : CPolynomial R := sorry -- leadingCoeffY (swap f) end Operations -end CPolynomial.Bivariate +end CBivariate end CompPoly diff --git a/CompPoly/Bivariate/ToPoly.lean b/CompPoly/Bivariate/ToPoly.lean index 3f70d7f..7f2b20b 100644 --- a/CompPoly/Bivariate/ToPoly.lean +++ b/CompPoly/Bivariate/ToPoly.lean @@ -11,11 +11,11 @@ import Mathlib.Algebra.Polynomial.Bivariate /-! # Equivalence with Mathlib Bivariate Polynomials -This file establishes the conversion from `Bivariate R` to Mathlib's `R[X][Y]` +This file establishes the conversion from `CBivariate R` to Mathlib's `R[X][Y]` (`Polynomial (Polynomial R)`). The main definition is: -- `toPoly`: converts `Bivariate R` to `R[X][Y]` +- `toPoly`: converts `CBivariate R` to `R[X][Y]` Proofs that `toPoly` preserves evaluation, coefficients, degrees, etc. (and that it forms an isomorphism with an inverse `ofPoly`) will be added as the implementation @@ -28,27 +28,27 @@ open scoped Polynomial.Bivariate namespace CompPoly -namespace CPolynomial.Bivariate +namespace CBivariate -/-- Convert `Bivariate R` to Mathlib's bivariate polynomial `R[X][Y]`. +/-- Convert `CBivariate R` to Mathlib's bivariate polynomial `R[X][Y]`. Intended implementation: map each Y-coefficient (a `CPolynomial R`) through `CPolynomial.toPoly` to obtain `Polynomial R`, then build `Polynomial (Polynomial R)` via `eval₂` (analogous to univariate `Raw.toPoly`). -/ noncomputable def toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] - (p : Bivariate R) : R[X][Y] := sorry + (p : CBivariate R) : R[X][Y] := sorry -/-- Convert Mathlib's `R[X][Y]` to `Bivariate R` (inverse of `toPoly`). +/-- Convert Mathlib's `R[X][Y]` to `CBivariate R` (inverse of `toPoly`). Intended implementation: extract each Y-coefficient via `p.coeff`, convert to `CPolynomial R` via `Polynomial.toImpl`, then build canonical bivariate. TODO: implement and prove round-trip lemmas. -/ noncomputable def ofPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] - (p : R[X][Y]) : Bivariate R := sorry + (p : R[X][Y]) : CBivariate R := sorry -- TODO: toPoly_ofPoly, ofPoly_toPoly (round-trips), ring equiv, evalEval/toPoly compatibility -end CPolynomial.Bivariate +end CBivariate end CompPoly From 529355ba5799c3a06065553cdca6b0f05de3082e Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Fri, 20 Feb 2026 16:12:52 +0000 Subject: [PATCH 06/18] feat: fix initial sorry's, complete definitions --- CompPoly/Bivariate/Basic.lean | 36 +++++++++++++++++++++++----------- CompPoly/Bivariate/ToPoly.lean | 24 +++++++++++++---------- CompPoly/Univariate/Basic.lean | 7 +++++++ 3 files changed, 46 insertions(+), 21 deletions(-) diff --git a/CompPoly/Bivariate/Basic.lean b/CompPoly/Bivariate/Basic.lean index a804be3..cb39294 100644 --- a/CompPoly/Bivariate/Basic.lean +++ b/CompPoly/Bivariate/Basic.lean @@ -44,6 +44,10 @@ 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))) +/-- Additive structure on CBivariate R -/ +instance : AddCommMonoid (CBivariate R) := + inferInstanceAs (AddCommMonoid (CPolynomial (CPolynomial R))) + -- --------------------------------------------------------------------------- -- Operation stubs (for ArkLib compatibility; proofs deferred) -- --------------------------------------------------------------------------- @@ -60,7 +64,7 @@ variable (R : Type*) [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] def CC (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 C_X : CBivariate R := CPolynomial.C CPolynomial.X +def X : 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) @@ -75,7 +79,12 @@ def coeff (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 support (f : CBivariate R) : Finset ℕ := CPolynomial.support f +def supportY (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 ℕ := + (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`. -/ @@ -93,17 +102,17 @@ def totalDegree (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`. - TODO: implement via mapping each Y-coefficient through `eval a`. -/ -def evalX (a : R) (f : CBivariate R) : CPolynomial R := sorry + ArkLib: `Polynomial.Bivariate.evalX`. -/ +def evalX [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 := f.val.eval (CPolynomial.C a) -/-- Full evaluation at `(x, y)`: `p(x, y)`. Equivalently `(evalY y f).eval x`. - Mathlib: `Polynomial.evalEval`. -/ +/-- 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 := CPolynomial.eval x (f.val.eval (CPolynomial.C y)) @@ -114,12 +123,17 @@ def leadingCoeffY (f : CBivariate R) : CPolynomial R := /-- Swap the roles of X and Y. ArkLib/Mathlib: `Polynomial.Bivariate.swap`. -/ -def swap (f : CBivariate R) : CBivariate R := sorry +def swap [DecidableEq R] (f : CBivariate R) : CBivariate R := + (f.supportY).sum (fun j => + let coeffJ : CPolynomial R := + (CPolynomial.support (f.val.coeff j)).sum (fun i => + CPolynomial.monomial i ((f.val.coeff j).coeff i)) + CPolynomial.monomial j coeffJ) /-- Leading coefficient when viewed as a polynomial in X. - The coefficient of X^(degreeX f): a polynomial in Y. Equivalently, `leadingCoeffY (swap f)`. - TODO: implement as `leadingCoeffY (swap f)` once `swap` has a computable definition. -/ -def leadingCoeffX (f : CBivariate R) : CPolynomial R := sorry -- leadingCoeffY (swap f) + The coefficient of X^(degreeX f): a polynomial in Y. -/ +def leadingCoeffX [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 7f2b20b..c35ac77 100644 --- a/CompPoly/Bivariate/ToPoly.lean +++ b/CompPoly/Bivariate/ToPoly.lean @@ -32,20 +32,24 @@ namespace CBivariate /-- Convert `CBivariate R` to Mathlib's bivariate polynomial `R[X][Y]`. - Intended implementation: map each Y-coefficient (a `CPolynomial R`) through - `CPolynomial.toPoly` to obtain `Polynomial R`, then build `Polynomial (Polynomial R)` - via `eval₂` (analogous to univariate `Raw.toPoly`). + 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] [Semiring R] - (p : CBivariate R) : R[X][Y] := sorry +noncomputable def toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] + (p : CBivariate R) : R[X][Y] := + (CPolynomial.support p).sum (fun j => + monomial j (CPolynomial.toPoly (p.val.coeff j))) /-- Convert Mathlib's `R[X][Y]` to `CBivariate R` (inverse of `toPoly`). - Intended implementation: extract each Y-coefficient via `p.coeff`, convert to - `CPolynomial R` via `Polynomial.toImpl`, then build canonical bivariate. - TODO: implement and prove round-trip lemmas. -/ -noncomputable def ofPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] - (p : R[X][Y]) : CBivariate R := sorry + 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] + [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⟩) -- TODO: toPoly_ofPoly, ofPoly_toPoly (round-trips), ring equiv, evalEval/toPoly compatibility diff --git a/CompPoly/Univariate/Basic.lean b/CompPoly/Univariate/Basic.lean index 638c743..326155b 100644 --- a/CompPoly/Univariate/Basic.lean +++ b/CompPoly/Univariate/Basic.lean @@ -123,6 +123,13 @@ lemma one_is_trimmed [Nontrivial R] : (1 : CPolynomial.Raw R).trim = 1 := instance [Nontrivial R] : One (CPolynomial R) where one := ⟨Raw.C 1, by exact one_is_trimmed⟩ +instance [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 + simp at this + exact Nat.zero_ne_one this⟩ + /-- 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 From f72eb43dd4c1057ed941115d9b4df4a7d59f74a8 Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Fri, 20 Feb 2026 16:23:26 +0000 Subject: [PATCH 07/18] feat: add isomorphism theorem statements --- CompPoly/Bivariate/Basic.lean | 4 ++++ CompPoly/Bivariate/ToPoly.lean | 40 +++++++++++++++++++++++++++++++++- 2 files changed, 43 insertions(+), 1 deletion(-) diff --git a/CompPoly/Bivariate/Basic.lean b/CompPoly/Bivariate/Basic.lean index cb39294..fbec93f 100644 --- a/CompPoly/Bivariate/Basic.lean +++ b/CompPoly/Bivariate/Basic.lean @@ -48,6 +48,10 @@ instance : Inhabited (CBivariate R) := inferInstanceAs (Inhabited (CPolynomial ( instance : AddCommMonoid (CBivariate R) := inferInstanceAs (AddCommMonoid (CPolynomial (CPolynomial R))) +/-- Ring structure on CBivariate R (for ring equiv with Mathlib in ToPoly). -/ +instance : Semiring (CBivariate R) := + inferInstanceAs (Semiring (CPolynomial (CPolynomial R))) + -- --------------------------------------------------------------------------- -- Operation stubs (for ArkLib compatibility; proofs deferred) -- --------------------------------------------------------------------------- diff --git a/CompPoly/Bivariate/ToPoly.lean b/CompPoly/Bivariate/ToPoly.lean index c35ac77..ff9d69f 100644 --- a/CompPoly/Bivariate/ToPoly.lean +++ b/CompPoly/Bivariate/ToPoly.lean @@ -51,8 +51,46 @@ def ofPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] let cj := p.coeff j CPolynomial.monomial j ⟨cj.toImpl, CPolynomial.Raw.trim_toImpl cj⟩) --- TODO: toPoly_ofPoly, ofPoly_toPoly (round-trips), ring equiv, evalEval/toPoly compatibility +/-- 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] + (p : R[X][Y]) : toPoly (ofPoly p) = p := sorry + +/-- 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] + (p : CBivariate R) : ofPoly (toPoly p) = p := sorry + +/-- 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] : + CBivariate R ≃+* R[X][Y] where + toFun := toPoly + invFun := ofPoly + left_inv := toPoly_ofPoly + right_inv := ofPoly_toPoly + map_mul' := sorry + map_add' := sorry + +/-- `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] + (x y : R) (f : CBivariate R) : + @CompPoly.CBivariate.evalEval R _ _ _ _ x y f = (toPoly f).evalEval x y := sorry + +/-- `toPoly` preserves coefficients: coefficient of `X^i Y^j` matches. -/ +theorem coeff_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] + (f : CBivariate R) (i j : ℕ) : + ((toPoly f).coeff j).coeff i = @CompPoly.CBivariate.coeff R _ _ _ _ f i j := sorry + +/-- `toPoly` preserves Y-degree. -/ +theorem natDegreeY_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] + (f : CBivariate R) : (toPoly f).natDegree = f.natDegreeY := sorry + +/-- `toPoly` preserves X-degree (max over Y-coefficients of their degree in X). -/ +theorem degreeX_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] + (f : CBivariate R) : + (toPoly f).support.sup (fun j => ((toPoly f).coeff j).natDegree) = f.degreeX := sorry end CBivariate +-- TODO correctness lemmas for operations and API functions + end CompPoly From 939a77a0edf1acf5f8958236201990c6119646c6 Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Mon, 23 Feb 2026 13:42:03 +0000 Subject: [PATCH 08/18] feat: build out toPoly with proofs of all the key theorems, to be able to prove API correct --- CompPoly/Bivariate/ToPoly.lean | 499 ++++++++++++++++++++++++++++++++- 1 file changed, 491 insertions(+), 8 deletions(-) diff --git a/CompPoly/Bivariate/ToPoly.lean b/CompPoly/Bivariate/ToPoly.lean index ff9d69f..bb7cac2 100644 --- a/CompPoly/Bivariate/ToPoly.lean +++ b/CompPoly/Bivariate/ToPoly.lean @@ -51,13 +51,283 @@ def ofPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] let cj := p.coeff j CPolynomial.monomial j ⟨cj.toImpl, CPolynomial.Raw.trim_toImpl cj⟩) +/- +Helper lemma: `toPoly` maps zero to zero. +-/ +lemma toPoly_zero {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] : + toPoly (0 : CBivariate R) = 0 := by + -- The sum over the empty set is zero. + simp [CompPoly.CBivariate.toPoly] + rw [ Finset.sum_eq_zero ] + aesop + +/- +Helper lemma: `toPoly` preserves addition. +Proof idea: +1. `toPoly` is a sum of monomials. +2. `coeff (p + q) j = coeff p j + coeff q j`. +3. `CPolynomial.toPoly` is additive. +4. `monomial` is additive. +5. Use `Finset.sum_add_distrib` and `Finset.sum_subset` to handle supports. +-/ +lemma toPoly_add {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring 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 + exact (by + apply CPolynomial.Raw.toPoly_add) + -- Apply the linearity of toPoly to the coefficients of p and q. + have h_coeff : ∀ (j : ℕ), (p + q).val.coeff j = p.val.coeff j + q.val.coeff j := by + apply CPolynomial.coeff_add + unfold CBivariate.toPoly + rw [ Finset.sum_subset + ( show CompPoly.CPolynomial.support (p + q) ⊆ + CompPoly.CPolynomial.support p ∪ CompPoly.CPolynomial.support q from ?_ ) ] + · simp +decide [ Finset.sum_add_distrib, h_coeff, h_linear ] + rw [ ← Finset.sum_subset (Finset.subset_union_left), + ← Finset.sum_subset (Finset.subset_union_right) ] + · simp +contextual [ CPolynomial.support ] + intro x hx hq + cases hx <;> simp_all +decide + · by_cases hx : x < Array.size q.val <;> simp_all +decide + · exact toFinsupp_eq_zero.mp rfl + · exact toFinsupp_eq_zero.mp rfl + · grind + · simp +contextual [ CPolynomial.mem_support_iff ] + aesop + · simp +contextual [ h_coeff ] + intro j hj₁ hj₂ + contrapose! hj₂ + simp_all +decide + -- Since $j$ is in the support of $p$ or $q$, the coefficient of $j$ in $p + q$ is non-zero. + have h_coeff_nonzero : (p + q).val.coeff j ≠ 0 := by + intro h + simp_all +decide [ Polynomial.ext_iff ] + obtain ⟨ x, hx ⟩ := hj₂ + specialize h_coeff j + simp_all +decide + exact hx ( by rw [ ← h_linear ]; aesop ) + exact (CPolynomial.mem_support_iff (p + q) j).mpr h_coeff_nonzero + · intro j hj + simp_all +decide [ CompPoly.CPolynomial.support ] + grind + +/- +Helper lemma: `toPoly` maps a monomial `c * Y^n` to `c.toPoly * Y^n`. +-/ +lemma toPoly_monomial {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] [DecidableEq R] + (n : ℕ) (c : CPolynomial R) : + toPoly (CPolynomial.monomial n c) = monomial n (c.toPoly) := by + unfold CPolynomial.monomial + unfold CBivariate.toPoly + unfold CPolynomial.support + rw [ Finset.sum_eq_single n ] <;> + simp +decide [ CompPoly.CPolynomial.Raw.monomial ] + · split_ifs <;> simp_all +decide [ Array.push ] + · grind + · split_ifs <;> simp_all +decide [ Array.push ] + exact toFinsupp_eq_zero.mp rfl + +/- +Helper lemma: `ofPoly` maps zero to zero. +-/ +lemma ofPoly_zero {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] [DecidableEq R] : + ofPoly (0 : R[X][Y]) = 0 := by + unfold CompPoly.CBivariate.ofPoly + simp +decide [ Polynomial.support ] + +/- +Helper lemma: `ofPoly` maps a monomial `c * Y^n` to `CPolynomial.monomial n ⟨c.toImpl, ...⟩`. +-/ +lemma ofPoly_monomial {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] [DecidableEq R] + (n : ℕ) (c : R[X]) : + ofPoly (monomial n c) = + CPolynomial.monomial n ⟨c.toImpl, CPolynomial.Raw.trim_toImpl c⟩ := by + unfold CompPoly.CBivariate.ofPoly + simp +decide + rw [ Finset.sum_eq_single n ] <;> simp +decide [ Polynomial.coeff_monomial ] + aesop + +/- +Helper lemma: `toImpl` preserves addition (where addition on `Raw` includes trimming). +Note: `CPolynomial.Raw.add p q` is defined as `(p.addRaw q).trim`. +`toImpl` produces a trimmed array representing the polynomial. +So this states that adding the array representations and trimming yields the array +representation of the sum. +-/ +lemma toImpl_add {R : Type*} [BEq R] [LawfulBEq R] [Ring 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 + convert CPolynomial.Raw.toPoly_add p.toImpl q.toImpl using 1 + convert h_add using 1 + rw [ CPolynomial.Raw.toPoly_toImpl, CPolynomial.Raw.toPoly_toImpl, + CPolynomial.Raw.toPoly_toImpl ] + have h_add_trim : ∀ p q : CPolynomial.Raw R, + p.toPoly = q.toPoly → p.trim = q.trim := by + intros p q h_eq + have h_coeff : ∀ n, p.coeff n = q.coeff n := by + intro n; exact (by + convert congr_arg (fun f => f.coeff n) h_eq using 1 <;> + simp +decide [ CPolynomial.Raw.coeff_toPoly ]) + exact CPolynomial.Raw.Trim.eq_of_equiv h_coeff + convert h_add_trim _ _ h_add using 1 + · have h_add_trim : ∀ p q : CPolynomial.Raw R, + (p + q).toPoly = p.toPoly + q.toPoly → (p + q).trim = p.trim + q.trim := by + intros p q h_add + apply ‹∀ (p q : CompPoly.CPolynomial.Raw R), + p.toPoly = q.toPoly → p.trim = q.trim› + grind + grind + · exact Eq.symm (CPolynomial.Raw.trim_toImpl (p + q)) + +/- +Helper lemma: `CPolynomial.monomial` is additive. +Proof: Use extensionality of `CPolynomial` and that coefficients are additive. +-/ +lemma CPolynomial_monomial_add {S : Type*} [Ring S] [BEq S] [LawfulBEq S] [DecidableEq S] + (n : ℕ) (a b : S) : + CPolynomial.monomial n (a + b) = CPolynomial.monomial n a + CPolynomial.monomial n b := by + -- By definition of monomial, we know that `coeff (monomial n c) i = if i = n then c else 0`. + have h_monomial_coeff : ∀ n : ℕ, ∀ c : S, ∀ i, + CPolynomial.Raw.coeff (CPolynomial.Raw.monomial n c) i = if i = n then c else 0 := by + unfold CompPoly.CPolynomial.Raw.monomial + intro n c i + split_ifs <;> simp_all +decide [ CompPoly.CPolynomial.Raw.coeff ] + · simp +decide [ Array.push ] + · grind + -- So we can apply this to both sides of the equation. + have h_monomial_coeff_eq : ∀ i, + CPolynomial.Raw.coeff (CPolynomial.Raw.monomial n (a + b)) i = + CPolynomial.Raw.coeff (CPolynomial.Raw.monomial n a + CPolynomial.Raw.monomial n b) i := by + -- Coefficient of the sum is the sum of the coefficients. + have h_coeff_add : ∀ (p q : CPolynomial.Raw S) (i : ℕ), + (p + q).coeff i = p.coeff i + q.coeff i := by + exact fun p q i => CPolynomial.Raw.add_coeff_trimmed p q i + aesop + exact CPolynomial.eq_iff_coeff.mpr h_monomial_coeff_eq + +lemma ofPoly_add {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring 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)), + ofPoly (p + q) = ofPoly p + ofPoly q := by + unfold CompPoly.CBivariate.ofPoly + intro p q + rw [ Finset.sum_subset + ( show (p + q |> Polynomial.support) ⊆ p.support ∪ q.support from fun x hx => ?_ ) ] + · simp +zetaDelta at * + rw [ Finset.sum_subset + (show p.support ⊆ p.support ∪ q.support from Finset.subset_union_left), + Finset.sum_subset + (show q.support ⊆ p.support ∪ q.support from Finset.subset_union_right) ] + · rw [ ← Finset.sum_add_distrib ] + refine' Finset.sum_congr rfl fun x hx => _ + rw [ ← CPolynomial_monomial_add ] + congr + exact Eq.symm (toImpl_add (p.coeff x) (q.coeff x)) + · aesop + · aesop + · aesop + · contrapose! hx + aesop + exact h_ofPoly_add_p p q + +theorem ofPoly_coeff {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] [DecidableEq R] + (p : R[X][Y]) (n : ℕ) : (CompPoly.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 : CompPoly.CPolynomial.coeff (CompPoly.CBivariate.ofPoly p) n = + Finset.sum (Polynomial.support p) (fun j => + CompPoly.CPolynomial.coeff + (CompPoly.CPolynomial.monomial j + ⟨Polynomial.toImpl (Polynomial.coeff p j), + CompPoly.CPolynomial.Raw.trim_toImpl (Polynomial.coeff p j)⟩) n) := by + unfold CompPoly.CBivariate.ofPoly + induction' p.support using Finset.induction with j s hj ih + · exact CPolynomial.eq_iff_coeff.mpr (congrFun rfl) + · rw [ Finset.sum_insert hj, CompPoly.CPolynomial.coeff_add, ih, Finset.sum_insert hj ] + rw [ h_coeff_sum, Finset.sum_eq_single n ] + · rw [ CompPoly.CPolynomial.coeff_monomial ] + simp +decide [ CompPoly.CPolynomial.toPoly ] + exact CPolynomial.Raw.toPoly_toImpl + · simp +decide [ CompPoly.CPolynomial.coeff, CompPoly.CPolynomial.monomial ] + unfold CompPoly.CPolynomial.Raw.monomial + grind + · aesop + +theorem toPoly_coeff {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] + (p : CBivariate R) (n : ℕ) : (toPoly p).coeff n = (CompPoly.CPolynomial.coeff p n).toPoly := by + rw [ CBivariate.toPoly, Polynomial.finset_sum_coeff ] + rw [ Finset.sum_eq_single n ] <;> simp +contextual [ Polynomial.coeff_monomial ] + simp_all +decide [ CompPoly.CPolynomial.mem_support_iff ] + aesop + /-- 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] - (p : R[X][Y]) : toPoly (ofPoly p) = p := sorry + (p : R[X][Y]) : toPoly (ofPoly p) = p := by + induction p using Polynomial.induction_on' + · rw [ ofPoly_add, toPoly_add, + ‹(CompPoly.CBivariate.ofPoly _).toPoly = _›, ‹(CompPoly.CBivariate.ofPoly _).toPoly = _› ] + · rename_i n c + simp +decide [ ofPoly_monomial, toPoly_monomial ] + exact congr_arg _ ( CompPoly.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] - (p : CBivariate R) : ofPoly (toPoly p) = p := sorry + (p : CBivariate R) : ofPoly (toPoly p) = p := by + apply CompPoly.CPolynomial.eq_iff_coeff.mpr + intro i + -- Since `toPoly` is injective on canonical polynomials, coefficients equal ⇒ poly equal. + have h_inj : Function.Injective (fun p : CompPoly.CPolynomial R => p.toPoly) := by + intro p q h_eq + have := CompPoly.CPolynomial.toImpl_toPoly_of_canonical p + have := CompPoly.CPolynomial.toImpl_toPoly_of_canonical q + aesop + apply h_inj + convert ofPoly_coeff p.toPoly i using 1 + exact Eq.symm (toPoly_coeff p i) + +/- +`toPoly` is equivalent to converting the outer polynomial to a `Polynomial` and then +mapping the inner coefficients using `CPolynomial.toPoly`. +-/ +theorem toPoly_eq_map {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] + (p : CBivariate R) : + toPoly p = (CPolynomial.toPoly p).map (CPolynomial.ringEquiv (R := R)) := by + convert Polynomial.ext _ + unfold CBivariate.toPoly + simp +decide [ Polynomial.coeff_monomial ] + intro n + split_ifs <;> simp_all +decide [ CompPoly.CPolynomial.toPoly ] + · erw [ CompPoly.CPolynomial.Raw.coeff_toPoly ] + unfold CompPoly.CPolynomial.ringEquiv + aesop + · rw [ CPolynomial.Raw.coeff_toPoly ] + simp +decide [ CPolynomial.support, * ] at * + by_cases h : n < Array.size p.val <;> aesop + +/- +`toPoly` preserves addition. +-/ +theorem toPoly_add₂ {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] + (p q : CBivariate R) : + toPoly (p + q) = toPoly p + toPoly q := by + rw [ CBivariate.toPoly_eq_map, CBivariate.toPoly_eq_map, CBivariate.toPoly_eq_map ] + rw [ ← Polynomial.map_add ] + congr + exact CPolynomial.Raw.toPoly_add _ _ + +/- +`toPoly` preserves multiplication. +-/ +theorem toPoly_mul {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] + (p q : CBivariate R) : + toPoly (p * q) = toPoly p * toPoly q := by + have h_mul : (p * q).toPoly = + (CPolynomial.toPoly (p * q)).map (CPolynomial.ringEquiv (R := R)) := by + exact toPoly_eq_map (p * q) + rw [ h_mul, CPolynomial.toPoly_mul ] + rw [ Polynomial.map_mul, ← toPoly_eq_map, ← toPoly_eq_map ] /-- Ring equivalence between `CBivariate R` and Mathlib's `R[X][Y]`. -/ noncomputable def ringEquiv @@ -67,27 +337,240 @@ noncomputable def ringEquiv invFun := ofPoly left_inv := toPoly_ofPoly right_inv := ofPoly_toPoly - map_mul' := sorry - map_add' := sorry + map_mul' := by apply toPoly_mul + map_add' := by exact fun x y => toPoly_add₂ x y + +/- +Evaluation of a canonical polynomial is equal to the sum over its support of +coefficients multiplied by powers of the variable. +-/ +theorem CompPoly.CPolynomial.eval_eq_sum_support + {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] (p : CompPoly.CPolynomial R) (x : R) : + p.eval x = p.support.sum (fun i => p.coeff i * x ^ i) := by + -- By definition of polynomial evaluation, we can expand both sides. + have h_eval_def : p.val.eval x = + (p.val.zipIdx.toList.map (fun ⟨a, i⟩ => a * x ^ i)).sum := by + unfold CompPoly.CPolynomial.Raw.eval + unfold CompPoly.CPolynomial.Raw.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⟩ => a * x ^ i)).sum = + (Finset.range p.val.size).sum (fun i => p.val.coeff i * x ^ i) := by + convert CompPoly.CPolynomial.Raw.sum_zipIdx_eq_sum_range p.val (fun a i => 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 + +/- +Evaluation (via a ring hom) of a canonical polynomial is the sum over its support +of mapped coefficients multiplied by powers of the variable. +-/ +theorem CompPoly.CPolynomial.eval₂_eq_sum_support + {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] {S : Type*} [Semiring S] + (f : R →+* S) (p : CompPoly.CPolynomial R) (x : S) : + p.eval₂ f x = p.support.sum (fun i => f (p.coeff i) * x ^ i) := by + unfold CompPoly.CPolynomial.support + convert CompPoly.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 CompPoly.CPolynomial.eval₂ + unfold CompPoly.CPolynomial.Raw.eval₂ + induction' ( Array.zipIdx p.val ) with a ha ih + simp +decide [ * ] + induction a using List.reverseRecOn <;> aesop + · rw [ Finset.sum_filter ] /-- `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] (x y : R) (f : CBivariate R) : - @CompPoly.CBivariate.evalEval R _ _ _ _ x y f = (toPoly f).evalEval x y := sorry + @CompPoly.CBivariate.evalEval R _ _ _ _ x y f = (toPoly f).evalEval x y := by + unfold CompPoly.CBivariate.evalEval Polynomial.evalEval + -- `toPoly f` has coefficients `f.val.coeff i`. + have h_toPoly : (toPoly f).eval (Polynomial.C y) = (f.val.eval (CPolynomial.C y)).toPoly := by + unfold CompPoly.CBivariate.toPoly + simp +decide [ Polynomial.eval_finset_sum, CompPoly.CPolynomial.Raw.eval ] + unfold CompPoly.CPolynomial.Raw.eval₂ + simp +decide [ Polynomial.eval₂_finset_sum ] + -- Rewrite the right-hand side to match the left-hand side. + have h_foldl : ∀ (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 + intro arr y + induction' arr using Array.recOn with arr ih + induction' arr using List.reverseRecOn with arr ih + · rfl + · simp_all +decide [ Finset.sum_range_succ, Array.zipIdx ] + rw [ Finset.sum_congr rfl fun i hi => by rw [ List.getElem?_append ] ] + rw [ Finset.sum_congr rfl fun i hi => by rw [ if_pos (Finset.mem_range.mp hi) ] ] + convert congr_arg₂ ( · + · ) ‹_› rfl using 1 + convert CPolynomial.Raw.toPoly_add _ _ using 1 + · congr! 1 + -- `toPoly (ih * C y ^ arr.length) = toPoly ih * toPoly (C y ^ arr.length)`. + have h_toPoly_mul : ∀ (p q : CPolynomial R), + (p * q).toPoly = p.toPoly * q.toPoly := by grind + convert h_toPoly_mul ih (CPolynomial.C y ^ arr.length) |> Eq.symm using 1 + congr! 1 + induction' arr.length with n ih <;> simp_all +decide [ pow_succ ] + · exact Eq.symm ( CPolynomial.Raw.toPoly_one ) + · congr! 1 + exact Eq.symm (CPolynomial.C_toPoly y) + · infer_instance + rw [ h_foldl, Finset.sum_subset ] + · exact fun i hi => Finset.mem_range.mpr + (Nat.lt_of_lt_of_le (Finset.mem_range.mp (Finset.mem_filter.mp hi |>.1)) (by simp)) + · simp +contextual [ CompPoly.CPolynomial.support ] + simp +decide [ CompPoly.CPolynomial.toPoly, CompPoly.CPolynomial.Raw.toPoly ] + unfold CompPoly.CPolynomial.Raw.eval₂ + erw [ Array.foldl_empty ] + simp + -- `toPoly (f.val.eval (C y))` equals the polynomial with coefficients `f.val.coeff i`. + rw [h_toPoly] + 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] (f : CBivariate R) (i j : ℕ) : - ((toPoly f).coeff j).coeff i = @CompPoly.CBivariate.coeff R _ _ _ _ f i j := sorry + ((toPoly f).coeff j).coeff i = @CompPoly.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 + +/- +The coefficient of `Y^j` in `toPoly f` is the converted coefficient of `Y^j` in `f`. +-/ +theorem coeff_toPoly_outer {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] + (f : CBivariate R) (j : ℕ) : + (toPoly f).coeff j = CPolynomial.toPoly (f.val.coeff j) := by + simp [CompPoly.CBivariate.toPoly] + rw [ Finset.sum_eq_single j ] <;> simp +decide [ Polynomial.coeff_monomial ] + · aesop + · intro hj + rw [ CompPoly.CPolynomial.support ] at hj + by_cases hj' : j < f.val.size <;> aesop + +/- +`toPoly` maps a canonical polynomial to 0 iff the polynomial is 0. +-/ +theorem CompPoly.CPolynomial.toPoly_eq_zero_iff + {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] (p : CPolynomial R) : + p.toPoly = 0 ↔ p = 0 := by + constructor + · intro hp + have h_trivial : p.toPoly.toImpl = p := by + exact CPolynomial.toImpl_toPoly_of_canonical p + rw [ eq_comm ] at h_trivial + aesop + · aesop + +/- +The support of `toPoly f` is the same as the Y-support of `f`. +-/ +theorem support_toPoly_outer {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] + (f : CBivariate R) : (toPoly f).support = f.supportY := by + ext x + simp +decide [ CompPoly.CPolynomial.mem_support_iff, CompPoly.CBivariate.supportY ] + rw [ CompPoly.CBivariate.toPoly ] + simp +decide [ Polynomial.coeff_monomial ] + rw [ CPolynomial.mem_support_iff, CompPoly.CPolynomial.toPoly_eq_zero_iff ] + aesop + +/- +The natural degree of a canonical polynomial is the maximum element of its support. +-/ +theorem CompPoly.CPolynomial.natDegree_eq_support_sup + {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring 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 ] + · -- If the size of the array is zero, then the polynomial is zero. + 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 /-- `toPoly` preserves Y-degree. -/ theorem natDegreeY_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] - (f : CBivariate R) : (toPoly f).natDegree = f.natDegreeY := sorry + (f : CBivariate R) : (toPoly f).natDegree = f.natDegreeY := by + unfold CompPoly.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 + by_cases hp : p = 0; + · simp +decide [ hp ]; + · refine' le_antisymm _ _; + · exact Finset.le_sup ( f := id ) ( Polynomial.natDegree_mem_support_of_nonzero hp ); + · exact Finset.sup_le fun i hi => Polynomial.le_natDegree_of_mem_supp _ hi; + 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 (CompPoly.CPolynomial.natDegree_eq_support_sup f) + +/- `toPoly` preserves X-degree (max over Y-coefficients of their degree in X). -/ +theorem CompPoly.CBivariate.coeff_toPoly_Y {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] + (f : CompPoly.CBivariate R) (j : ℕ) : + (CompPoly.CBivariate.toPoly f).coeff j = CompPoly.CPolynomial.toPoly (f.val.coeff j) := by + erw [ Polynomial.finset_sum_coeff ]; + rw [ Finset.sum_eq_single j ] <;> simp +contextual [ Polynomial.coeff_monomial ] + intro hj; + rw [ CompPoly.CPolynomial.support ] at hj; + by_cases hj' : j < f.val.size <;> simp_all +decide + · exact (CPolynomial.toPoly_eq_zero_iff 0).mpr rfl + · exact (CPolynomial.toPoly_eq_zero_iff 0).mpr rfl /-- `toPoly` preserves X-degree (max over Y-coefficients of their degree in X). -/ theorem degreeX_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] (f : CBivariate R) : - (toPoly f).support.sup (fun j => ((toPoly f).coeff j).natDegree) = f.degreeX := sorry + (toPoly f).support.sup (fun j => ((toPoly f).coeff j).natDegree) = f.degreeX := by + convert ( Finset.sup_congr ?_ ?_ ); + · ext; simp +decide [ CompPoly.CBivariate.coeff_toPoly_Y ]; + rw [ CompPoly.CPolynomial.support ]; + by_cases h : ‹_› < f.val.size <;> simp_all +decide [ Finset.mem_filter, Finset.mem_range ]; + · -- Since `toPoly` is injective, if `toPoly (f.coeff j) = 0`, then `f.coeff j = 0`. + have h_inj : ∀ (p : CompPoly.CPolynomial R), p.toPoly = 0 ↔ p = 0 := by + intro p; exact ⟨fun hp => by + apply Subtype.ext; + apply_fun (fun p => p.toImpl) at hp; + convert hp using 1; + exact Eq.symm (CPolynomial.toImpl_toPoly_of_canonical p), + fun hp => by aesop⟩ + aesop + · exact (CompPoly.CPolynomial.toPoly_eq_zero_iff 0).mpr rfl + · intro j hj + rw [ CompPoly.CBivariate.coeff_toPoly_Y ] + exact Eq.symm (CPolynomial.natDegree_toPoly (f.val.coeff j)) end CBivariate From 1cfed60807036e09baf7d0174023a0f46830139c Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Mon, 23 Feb 2026 14:07:57 +0000 Subject: [PATCH 09/18] feat: refactor some of the theorem statements throughout the repository, improve quality and documentation --- CompPoly/Bivariate/ToPoly.lean | 400 +++++++++++--------------------- CompPoly/Univariate/Basic.lean | 81 +++++++ CompPoly/Univariate/ToPoly.lean | 10 + 3 files changed, 221 insertions(+), 270 deletions(-) diff --git a/CompPoly/Bivariate/ToPoly.lean b/CompPoly/Bivariate/ToPoly.lean index bb7cac2..8de2e64 100644 --- a/CompPoly/Bivariate/ToPoly.lean +++ b/CompPoly/Bivariate/ToPoly.lean @@ -14,13 +14,14 @@ import Mathlib.Algebra.Polynomial.Bivariate This file establishes the conversion from `CBivariate R` to Mathlib's `R[X][Y]` (`Polynomial (Polynomial R)`). -The main definition is: +Main definitions: - `toPoly`: converts `CBivariate R` to `R[X][Y]` +- `ofPoly`: converts `R[X][Y]` back to `CBivariate R` -Proofs that `toPoly` preserves evaluation, coefficients, degrees, etc. (and that it -forms an isomorphism with an inverse `ofPoly`) will be added as the implementation -is completed. The target interface matches ArkLib's `Polynomial.Bivariate` and -Mathlib's `Polynomial.Bivariate`. +Main results: +- round-trip identities: `ofPoly_toPoly`, `toPoly_ofPoly` +- ring equivalence: `ringEquiv` +- API correctness lemmas for evaluation, coefficients, support, and degrees -/ open Polynomial @@ -30,6 +31,9 @@ namespace CompPoly namespace CBivariate +/-! Core conversion lemmas between `CBivariate R` and `R[X][Y]`. -/ +section ToPolyCore + /-- Convert `CBivariate R` to Mathlib's bivariate polynomial `R[X][Y]`. Maps each Y-coefficient through `CPolynomial.toPoly`, then builds @@ -51,25 +55,15 @@ def ofPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] let cj := p.coeff j CPolynomial.monomial j ⟨cj.toImpl, CPolynomial.Raw.trim_toImpl cj⟩) -/- -Helper lemma: `toPoly` maps zero to zero. --/ +/-- `toPoly` maps the zero bivariate polynomial to `0`. -/ lemma toPoly_zero {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] : toPoly (0 : CBivariate R) = 0 := by -- The sum over the empty set is zero. - simp [CompPoly.CBivariate.toPoly] + simp [CBivariate.toPoly] rw [ Finset.sum_eq_zero ] aesop -/- -Helper lemma: `toPoly` preserves addition. -Proof idea: -1. `toPoly` is a sum of monomials. -2. `coeff (p + q) j = coeff p j + coeff q j`. -3. `CPolynomial.toPoly` is additive. -4. `monomial` is additive. -5. Use `Finset.sum_add_distrib` and `Finset.sum_subset` to handle supports. --/ +/-- `toPoly` preserves addition. -/ lemma toPoly_add {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring 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 @@ -81,8 +75,8 @@ lemma toPoly_add {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] apply CPolynomial.coeff_add unfold CBivariate.toPoly rw [ Finset.sum_subset - ( show CompPoly.CPolynomial.support (p + q) ⊆ - CompPoly.CPolynomial.support p ∪ CompPoly.CPolynomial.support q from ?_ ) ] + ( show CPolynomial.support (p + q) ⊆ + CPolynomial.support p ∪ CPolynomial.support q from ?_ ) ] · simp +decide [ Finset.sum_add_distrib, h_coeff, h_linear ] rw [ ← Finset.sum_subset (Finset.subset_union_left), ← Finset.sum_subset (Finset.subset_union_right) ] @@ -109,12 +103,10 @@ lemma toPoly_add {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] exact hx ( by rw [ ← h_linear ]; aesop ) exact (CPolynomial.mem_support_iff (p + q) j).mpr h_coeff_nonzero · intro j hj - simp_all +decide [ CompPoly.CPolynomial.support ] + simp_all +decide [ CPolynomial.support ] grind -/- -Helper lemma: `toPoly` maps a monomial `c * Y^n` to `c.toPoly * Y^n`. --/ +/-- `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] (n : ℕ) (c : CPolynomial R) : toPoly (CPolynomial.monomial n c) = monomial n (c.toPoly) := by @@ -122,38 +114,30 @@ lemma toPoly_monomial {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] unfold CBivariate.toPoly unfold CPolynomial.support rw [ Finset.sum_eq_single n ] <;> - simp +decide [ CompPoly.CPolynomial.Raw.monomial ] + simp +decide [ CPolynomial.Raw.monomial ] · split_ifs <;> simp_all +decide [ Array.push ] · grind · split_ifs <;> simp_all +decide [ Array.push ] exact toFinsupp_eq_zero.mp rfl -/- -Helper lemma: `ofPoly` maps zero to zero. --/ +/-- `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] : ofPoly (0 : R[X][Y]) = 0 := by - unfold CompPoly.CBivariate.ofPoly + unfold CBivariate.ofPoly simp +decide [ Polynomial.support ] -/- -Helper lemma: `ofPoly` maps a monomial `c * Y^n` to `CPolynomial.monomial n ⟨c.toImpl, ...⟩`. --/ +/-- `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] (n : ℕ) (c : R[X]) : ofPoly (monomial n c) = CPolynomial.monomial n ⟨c.toImpl, CPolynomial.Raw.trim_toImpl c⟩ := by - unfold CompPoly.CBivariate.ofPoly + unfold CBivariate.ofPoly simp +decide rw [ Finset.sum_eq_single n ] <;> simp +decide [ Polynomial.coeff_monomial ] aesop -/- -Helper lemma: `toImpl` preserves addition (where addition on `Raw` includes trimming). -Note: `CPolynomial.Raw.add p q` is defined as `(p.addRaw q).trim`. -`toImpl` produces a trimmed array representing the polynomial. -So this states that adding the array representations and trimming yields the array -representation of the sum. +/-- +`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]) : p.toImpl + q.toImpl = (p + q).toImpl := by @@ -175,44 +159,19 @@ lemma toImpl_add {R : Type*} [BEq R] [LawfulBEq R] [Ring R] (p q : R[X]) : · have h_add_trim : ∀ p q : CPolynomial.Raw R, (p + q).toPoly = p.toPoly + q.toPoly → (p + q).trim = p.trim + q.trim := by intros p q h_add - apply ‹∀ (p q : CompPoly.CPolynomial.Raw R), + apply ‹∀ (p q : CPolynomial.Raw R), p.toPoly = q.toPoly → p.trim = q.trim› grind grind · exact Eq.symm (CPolynomial.Raw.trim_toImpl (p + q)) -/- -Helper lemma: `CPolynomial.monomial` is additive. -Proof: Use extensionality of `CPolynomial` and that coefficients are additive. --/ -lemma CPolynomial_monomial_add {S : Type*} [Ring S] [BEq S] [LawfulBEq S] [DecidableEq S] - (n : ℕ) (a b : S) : - CPolynomial.monomial n (a + b) = CPolynomial.monomial n a + CPolynomial.monomial n b := by - -- By definition of monomial, we know that `coeff (monomial n c) i = if i = n then c else 0`. - have h_monomial_coeff : ∀ n : ℕ, ∀ c : S, ∀ i, - CPolynomial.Raw.coeff (CPolynomial.Raw.monomial n c) i = if i = n then c else 0 := by - unfold CompPoly.CPolynomial.Raw.monomial - intro n c i - split_ifs <;> simp_all +decide [ CompPoly.CPolynomial.Raw.coeff ] - · simp +decide [ Array.push ] - · grind - -- So we can apply this to both sides of the equation. - have h_monomial_coeff_eq : ∀ i, - CPolynomial.Raw.coeff (CPolynomial.Raw.monomial n (a + b)) i = - CPolynomial.Raw.coeff (CPolynomial.Raw.monomial n a + CPolynomial.Raw.monomial n b) i := by - -- Coefficient of the sum is the sum of the coefficients. - have h_coeff_add : ∀ (p q : CPolynomial.Raw S) (i : ℕ), - (p + q).coeff i = p.coeff i + q.coeff i := by - exact fun p q i => CPolynomial.Raw.add_coeff_trimmed p q i - aesop - exact CPolynomial.eq_iff_coeff.mpr h_monomial_coeff_eq - +/-- `ofPoly` preserves addition in `R[X][Y]`. -/ lemma ofPoly_add {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring 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)), ofPoly (p + q) = ofPoly p + ofPoly q := by - unfold CompPoly.CBivariate.ofPoly + unfold CBivariate.ofPoly intro p q rw [ Finset.sum_subset ( show (p + q |> Polynomial.support) ⊆ p.support ∪ q.support from fun x hx => ?_ ) ] @@ -223,7 +182,7 @@ lemma ofPoly_add {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] [Deci (show q.support ⊆ p.support ∪ q.support from Finset.subset_union_right) ] · rw [ ← Finset.sum_add_distrib ] refine' Finset.sum_congr rfl fun x hx => _ - rw [ ← CPolynomial_monomial_add ] + rw [ ← CPolynomial.monomial_add ] congr exact Eq.symm (toImpl_add (p.coeff x) (q.coeff x)) · aesop @@ -233,63 +192,39 @@ lemma ofPoly_add {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] [Deci aesop 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] - (p : R[X][Y]) (n : ℕ) : (CompPoly.CPolynomial.coeff (ofPoly p) n).toPoly = p.coeff n := by + (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 : CompPoly.CPolynomial.coeff (CompPoly.CBivariate.ofPoly p) n = + have h_coeff_sum : CPolynomial.coeff (ofPoly p) n = Finset.sum (Polynomial.support p) (fun j => - CompPoly.CPolynomial.coeff - (CompPoly.CPolynomial.monomial j + CPolynomial.coeff + (CPolynomial.monomial j ⟨Polynomial.toImpl (Polynomial.coeff p j), - CompPoly.CPolynomial.Raw.trim_toImpl (Polynomial.coeff p j)⟩) n) := by - unfold CompPoly.CBivariate.ofPoly + CPolynomial.Raw.trim_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) - · rw [ Finset.sum_insert hj, CompPoly.CPolynomial.coeff_add, ih, Finset.sum_insert hj ] + · rw [ Finset.sum_insert hj, CPolynomial.coeff_add, ih, Finset.sum_insert hj ] rw [ h_coeff_sum, Finset.sum_eq_single n ] - · rw [ CompPoly.CPolynomial.coeff_monomial ] - simp +decide [ CompPoly.CPolynomial.toPoly ] + · rw [ CPolynomial.coeff_monomial ] + simp +decide [ CPolynomial.toPoly ] exact CPolynomial.Raw.toPoly_toImpl - · simp +decide [ CompPoly.CPolynomial.coeff, CompPoly.CPolynomial.monomial ] - unfold CompPoly.CPolynomial.Raw.monomial + · simp +decide [ CPolynomial.coeff, CPolynomial.monomial ] + unfold CPolynomial.Raw.monomial grind · 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] - (p : CBivariate R) (n : ℕ) : (toPoly p).coeff n = (CompPoly.CPolynomial.coeff p n).toPoly := by + (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 ] - simp_all +decide [ CompPoly.CPolynomial.mem_support_iff ] + simp_all +decide [ CPolynomial.mem_support_iff ] aesop -/-- 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] - (p : R[X][Y]) : toPoly (ofPoly p) = p := by - induction p using Polynomial.induction_on' - · rw [ ofPoly_add, toPoly_add, - ‹(CompPoly.CBivariate.ofPoly _).toPoly = _›, ‹(CompPoly.CBivariate.ofPoly _).toPoly = _› ] - · rename_i n c - simp +decide [ ofPoly_monomial, toPoly_monomial ] - exact congr_arg _ ( CompPoly.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] - (p : CBivariate R) : ofPoly (toPoly p) = p := by - apply CompPoly.CPolynomial.eq_iff_coeff.mpr - intro i - -- Since `toPoly` is injective on canonical polynomials, coefficients equal ⇒ poly equal. - have h_inj : Function.Injective (fun p : CompPoly.CPolynomial R => p.toPoly) := by - intro p q h_eq - have := CompPoly.CPolynomial.toImpl_toPoly_of_canonical p - have := CompPoly.CPolynomial.toImpl_toPoly_of_canonical q - aesop - apply h_inj - convert ofPoly_coeff p.toPoly i using 1 - exact Eq.symm (toPoly_coeff p i) - -/- -`toPoly` is equivalent to converting the outer polynomial to a `Polynomial` and then -mapping the inner coefficients using `CPolynomial.toPoly`. +/-- +`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] (p : CBivariate R) : @@ -298,28 +233,15 @@ theorem toPoly_eq_map {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] unfold CBivariate.toPoly simp +decide [ Polynomial.coeff_monomial ] intro n - split_ifs <;> simp_all +decide [ CompPoly.CPolynomial.toPoly ] - · erw [ CompPoly.CPolynomial.Raw.coeff_toPoly ] - unfold CompPoly.CPolynomial.ringEquiv + split_ifs <;> simp_all +decide [ CPolynomial.toPoly ] + · erw [ CPolynomial.Raw.coeff_toPoly ] + unfold CPolynomial.ringEquiv aesop · rw [ CPolynomial.Raw.coeff_toPoly ] simp +decide [ CPolynomial.support, * ] at * by_cases h : n < Array.size p.val <;> aesop -/- -`toPoly` preserves addition. --/ -theorem toPoly_add₂ {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] - (p q : CBivariate R) : - toPoly (p + q) = toPoly p + toPoly q := by - rw [ CBivariate.toPoly_eq_map, CBivariate.toPoly_eq_map, CBivariate.toPoly_eq_map ] - rw [ ← Polynomial.map_add ] - congr - exact CPolynomial.Raw.toPoly_add _ _ - -/- -`toPoly` preserves multiplication. --/ +/-- `toPoly` preserves multiplication. -/ theorem toPoly_mul {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] (p q : CBivariate R) : toPoly (p * q) = toPoly p * toPoly q := by @@ -329,6 +251,36 @@ theorem toPoly_mul {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] rw [ h_mul, CPolynomial.toPoly_mul ] rw [ Polynomial.map_mul, ← toPoly_eq_map, ← toPoly_eq_map ] +end ToPolyCore + +/-! Ring equivalence between bivariate representations. -/ +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] + (p : R[X][Y]) : toPoly (ofPoly p) = p := by + induction p using Polynomial.induction_on' + · rw [ ofPoly_add, toPoly_add, + ‹(ofPoly _).toPoly = _›, ‹(ofPoly _).toPoly = _› ] + · rename_i n c + simp +decide [ ofPoly_monomial, toPoly_monomial ] + 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] + (p : CBivariate R) : ofPoly (toPoly p) = p := by + apply CPolynomial.eq_iff_coeff.mpr + intro i + -- Since `toPoly` is injective on canonical polynomials, coefficients equal ⇒ poly equal. + have h_inj : Function.Injective (fun p : CPolynomial R => p.toPoly) := by + intro p q h_eq + have := CPolynomial.toImpl_toPoly_of_canonical p + have := CPolynomial.toImpl_toPoly_of_canonical q + aesop + apply h_inj + convert ofPoly_coeff p.toPoly i using 1 + exact Eq.symm (toPoly_coeff p i) + /-- 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] : @@ -338,67 +290,24 @@ noncomputable def ringEquiv left_inv := toPoly_ofPoly right_inv := ofPoly_toPoly map_mul' := by apply toPoly_mul - map_add' := by exact fun x y => toPoly_add₂ x y + map_add' := by exact fun x y => toPoly_add x y -/- -Evaluation of a canonical polynomial is equal to the sum over its support of -coefficients multiplied by powers of the variable. --/ -theorem CompPoly.CPolynomial.eval_eq_sum_support - {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] (p : CompPoly.CPolynomial R) (x : R) : - p.eval x = p.support.sum (fun i => p.coeff i * x ^ i) := by - -- By definition of polynomial evaluation, we can expand both sides. - have h_eval_def : p.val.eval x = - (p.val.zipIdx.toList.map (fun ⟨a, i⟩ => a * x ^ i)).sum := by - unfold CompPoly.CPolynomial.Raw.eval - unfold CompPoly.CPolynomial.Raw.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⟩ => a * x ^ i)).sum = - (Finset.range p.val.size).sum (fun i => p.val.coeff i * x ^ i) := by - convert CompPoly.CPolynomial.Raw.sum_zipIdx_eq_sum_range p.val (fun a i => 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 +end RingEquiv -/- -Evaluation (via a ring hom) of a canonical polynomial is the sum over its support -of mapped coefficients multiplied by powers of the variable. --/ -theorem CompPoly.CPolynomial.eval₂_eq_sum_support - {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] {S : Type*} [Semiring S] - (f : R →+* S) (p : CompPoly.CPolynomial R) (x : S) : - p.eval₂ f x = p.support.sum (fun i => f (p.coeff i) * x ^ i) := by - unfold CompPoly.CPolynomial.support - convert CompPoly.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 CompPoly.CPolynomial.eval₂ - unfold CompPoly.CPolynomial.Raw.eval₂ - induction' ( Array.zipIdx p.val ) with a ha ih - simp +decide [ * ] - induction a using List.reverseRecOn <;> aesop - · rw [ Finset.sum_filter ] +/-! Correctness lemmas for evaluation, coefficients, support, and degrees. -/ +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] (x y : R) (f : CBivariate R) : - @CompPoly.CBivariate.evalEval R _ _ _ _ x y f = (toPoly f).evalEval x y := by - unfold CompPoly.CBivariate.evalEval Polynomial.evalEval + @CBivariate.evalEval R _ _ _ _ x y f = (toPoly f).evalEval x y := by + unfold CBivariate.evalEval Polynomial.evalEval -- `toPoly f` has coefficients `f.val.coeff i`. have h_toPoly : (toPoly f).eval (Polynomial.C y) = (f.val.eval (CPolynomial.C y)).toPoly := by - unfold CompPoly.CBivariate.toPoly - simp +decide [ Polynomial.eval_finset_sum, CompPoly.CPolynomial.Raw.eval ] - unfold CompPoly.CPolynomial.Raw.eval₂ - simp +decide [ Polynomial.eval₂_finset_sum ] + unfold CBivariate.toPoly + simp +decide [ Polynomial.eval_finset_sum, CPolynomial.Raw.eval ] + unfold CPolynomial.Raw.eval₂ + simp +decide -- Rewrite the right-hand side to match the left-hand side. have h_foldl : ∀ (arr : Array (CPolynomial R)) (y : R), (Array.foldl (fun (acc : CPolynomial R) (x : CPolynomial R × ℕ) => @@ -427,9 +336,9 @@ theorem evalEval_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R rw [ h_foldl, Finset.sum_subset ] · exact fun i hi => Finset.mem_range.mpr (Nat.lt_of_lt_of_le (Finset.mem_range.mp (Finset.mem_filter.mp hi |>.1)) (by simp)) - · simp +contextual [ CompPoly.CPolynomial.support ] - simp +decide [ CompPoly.CPolynomial.toPoly, CompPoly.CPolynomial.Raw.toPoly ] - unfold CompPoly.CPolynomial.Raw.eval₂ + · simp +contextual [ CPolynomial.support ] + simp +decide [ CPolynomial.toPoly, CPolynomial.Raw.toPoly ] + unfold CPolynomial.Raw.eval₂ erw [ Array.foldl_empty ] simp -- `toPoly (f.val.eval (C y))` equals the polynomial with coefficients `f.val.coeff i`. @@ -439,7 +348,7 @@ theorem evalEval_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R /-- `toPoly` preserves coefficients: coefficient of `X^i Y^j` matches. -/ theorem coeff_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] (f : CBivariate R) (i j : ℕ) : - ((toPoly f).coeff j).coeff i = @CompPoly.CBivariate.coeff R _ _ _ _ f i j := by + ((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 ] @@ -447,105 +356,52 @@ theorem coeff_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] · congr · by_cases h : j < ( f.val.size : ℕ ) <;> aesop -/- -The coefficient of `Y^j` in `toPoly f` is the converted coefficient of `Y^j` in `f`. --/ +/-- The outer `Y`-coefficient of `toPoly f` is `CPolynomial.toPoly (f.val.coeff j)`. -/ theorem coeff_toPoly_outer {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] (f : CBivariate R) (j : ℕ) : (toPoly f).coeff j = CPolynomial.toPoly (f.val.coeff j) := by - simp [CompPoly.CBivariate.toPoly] + simp [CBivariate.toPoly] rw [ Finset.sum_eq_single j ] <;> simp +decide [ Polynomial.coeff_monomial ] · aesop · intro hj - rw [ CompPoly.CPolynomial.support ] at hj + rw [ CPolynomial.support ] at hj by_cases hj' : j < f.val.size <;> aesop -/- -`toPoly` maps a canonical polynomial to 0 iff the polynomial is 0. --/ -theorem CompPoly.CPolynomial.toPoly_eq_zero_iff - {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] (p : CPolynomial R) : - p.toPoly = 0 ↔ p = 0 := by - constructor - · intro hp - have h_trivial : p.toPoly.toImpl = p := by - exact CPolynomial.toImpl_toPoly_of_canonical p - rw [ eq_comm ] at h_trivial - aesop - · aesop - -/- -The support of `toPoly f` is the same as the Y-support of `f`. --/ +/-- 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] (f : CBivariate R) : (toPoly f).support = f.supportY := by ext x - simp +decide [ CompPoly.CPolynomial.mem_support_iff, CompPoly.CBivariate.supportY ] - rw [ CompPoly.CBivariate.toPoly ] + simp +decide [ CPolynomial.mem_support_iff, CBivariate.supportY ] + rw [ CBivariate.toPoly ] simp +decide [ Polynomial.coeff_monomial ] - rw [ CPolynomial.mem_support_iff, CompPoly.CPolynomial.toPoly_eq_zero_iff ] + rw [ CPolynomial.mem_support_iff, CPolynomial.toPoly_eq_zero_iff ] aesop -/- -The natural degree of a canonical polynomial is the maximum element of its support. --/ -theorem CompPoly.CPolynomial.natDegree_eq_support_sup - {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring 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 ] - · -- If the size of the array is zero, then the polynomial is zero. - 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 - /-- `toPoly` preserves Y-degree. -/ theorem natDegreeY_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] (f : CBivariate R) : (toPoly f).natDegree = f.natDegreeY := by - unfold CompPoly.CBivariate.natDegreeY; + 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 - by_cases hp : p = 0; - · simp +decide [ hp ]; - · refine' le_antisymm _ _; - · exact Finset.le_sup ( f := id ) ( Polynomial.natDegree_mem_support_of_nonzero hp ); - · exact Finset.sup_le fun i hi => Polynomial.le_natDegree_of_mem_supp _ hi; - rw [ h_deg, support_toPoly_outer ]; + by_cases hp : p = 0 + · simp +decide [ hp ] + · refine' le_antisymm _ _ + · exact Finset.le_sup (f := id) (Polynomial.natDegree_mem_support_of_nonzero hp) + · exact Finset.sup_le fun i hi => Polynomial.le_natDegree_of_mem_supp _ hi + 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 (CompPoly.CPolynomial.natDegree_eq_support_sup f) + apply Eq.symm + exact CPolynomial.natDegree_eq_support_sup f -/- `toPoly` preserves X-degree (max over Y-coefficients of their degree in X). -/ -theorem CompPoly.CBivariate.coeff_toPoly_Y {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] - (f : CompPoly.CBivariate R) (j : ℕ) : - (CompPoly.CBivariate.toPoly f).coeff j = CompPoly.CPolynomial.toPoly (f.val.coeff j) := by - erw [ Polynomial.finset_sum_coeff ]; +/-- The outer `Y`-coefficient formula used for X-degree transport. -/ +theorem coeff_toPoly_Y {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] + (f : CBivariate R) (j : ℕ) : + (toPoly f).coeff j = CPolynomial.toPoly (f.val.coeff j) := by + erw [ Polynomial.finset_sum_coeff ] rw [ Finset.sum_eq_single j ] <;> simp +contextual [ Polynomial.coeff_monomial ] - intro hj; - rw [ CompPoly.CPolynomial.support ] at hj; + intro hj + rw [ CPolynomial.support ] at hj by_cases hj' : j < f.val.size <;> simp_all +decide · exact (CPolynomial.toPoly_eq_zero_iff 0).mpr rfl · exact (CPolynomial.toPoly_eq_zero_iff 0).mpr rfl @@ -554,24 +410,28 @@ theorem CompPoly.CBivariate.coeff_toPoly_Y {R : Type*} [BEq R] [LawfulBEq R] [No theorem degreeX_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] (f : CBivariate R) : (toPoly f).support.sup (fun j => ((toPoly f).coeff j).natDegree) = f.degreeX := by - convert ( Finset.sup_congr ?_ ?_ ); - · ext; simp +decide [ CompPoly.CBivariate.coeff_toPoly_Y ]; - rw [ CompPoly.CPolynomial.support ]; - by_cases h : ‹_› < f.val.size <;> simp_all +decide [ Finset.mem_filter, Finset.mem_range ]; + convert (Finset.sup_congr ?_ ?_) + · ext + simp +decide [ coeff_toPoly_Y ] + rw [ CPolynomial.support ] + by_cases h : ‹_› < f.val.size <;> simp_all +decide [ Finset.mem_filter, Finset.mem_range ] · -- Since `toPoly` is injective, if `toPoly (f.coeff j) = 0`, then `f.coeff j = 0`. - have h_inj : ∀ (p : CompPoly.CPolynomial R), p.toPoly = 0 ↔ p = 0 := by - intro p; exact ⟨fun hp => by - apply Subtype.ext; - apply_fun (fun p => p.toImpl) at hp; - convert hp using 1; + have h_inj : ∀ (p : CPolynomial R), p.toPoly = 0 ↔ p = 0 := by + intro p + exact ⟨fun hp => by + apply Subtype.ext + apply_fun (fun p => p.toImpl) at hp + convert hp using 1 exact Eq.symm (CPolynomial.toImpl_toPoly_of_canonical p), fun hp => by aesop⟩ aesop - · exact (CompPoly.CPolynomial.toPoly_eq_zero_iff 0).mpr rfl + · exact (CPolynomial.toPoly_eq_zero_iff 0).mpr rfl · intro j hj - rw [ CompPoly.CBivariate.coeff_toPoly_Y ] + rw [ coeff_toPoly_Y ] exact Eq.symm (CPolynomial.natDegree_toPoly (f.val.coeff j)) +end ImplementationCorrectness + end CBivariate -- TODO correctness lemmas for operations and API functions diff --git a/CompPoly/Univariate/Basic.lean b/CompPoly/Univariate/Basic.lean index 7217744..79c2438 100644 --- a/CompPoly/Univariate/Basic.lean +++ b/CompPoly/Univariate/Basic.lean @@ -236,6 +236,14 @@ theorem eq_iff_coeff {p q : CPolynomial R} : · intro h i; rw [h] · intro h; apply ext; exact Trim.canonical_ext p.prop q.prop (fun i => h i) +/-- Monomials are additive in their coefficient. -/ +theorem monomial_add [DecidableEq R] (n : ℕ) (a b : R) : + monomial n (a + b) = monomial n a + monomial n b := by + apply (eq_iff_coeff).2 + intro i + rw [coeff_monomial, coeff_add, coeff_monomial, coeff_monomial] + 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 rw [eq_iff_coeff]; simp only [coeff_zero] @@ -261,6 +269,47 @@ theorem support_empty_iff (p : CPolynomial R) : p.support = ∅ ↔ p = 0 := by · 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) : + p.eval x = p.support.sum (fun i => p.coeff i * x ^ i) := by + have h_eval_def : p.val.eval x = + (p.val.zipIdx.toList.map (fun ⟨a, i⟩ => a * x ^ i)).sum := by + unfold CPolynomial.Raw.eval + unfold CPolynomial.Raw.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⟩ => a * x ^ i)).sum = + (Finset.range p.val.size).sum (fun i => p.val.coeff i * x ^ i) := by + convert CPolynomial.Raw.sum_zipIdx_eq_sum_range p.val (fun a i => 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 + +/-- +Evaluation via a ring hom equals the sum over support of mapped coefficients times powers. +-/ +theorem eval₂_eq_sum_support {S : Type*} [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 ] + /-- Lemmas on coefficients and multiplication by `X`. -/ lemma coeff_X_mul_succ [Nontrivial R] (p : CPolynomial R) (n : ℕ) : coeff (X * p) (n + 1) = coeff p n := by @@ -497,6 +546,38 @@ theorem degree_eq_natDegree (p : CPolynomial R) (hp : p ≠ 0) : unfold natDegree Raw.natDegree rw [hk] +/-- The natural degree is the maximum element of the support. -/ +theorem natDegree_eq_support_sup [Nontrivial 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 + end Operations section Semiring diff --git a/CompPoly/Univariate/ToPoly.lean b/CompPoly/Univariate/ToPoly.lean index f670fc8..b17d6a9 100644 --- a/CompPoly/Univariate/ToPoly.lean +++ b/CompPoly/Univariate/ToPoly.lean @@ -209,6 +209,16 @@ theorem Raw.toImpl_toPoly [LawfulBEq R] (p : CPolynomial.Raw R) : p.toPoly.toImp rw [← toPoly_trim] exact toImpl_toPoly_of_canonical ⟨ p.trim, Trim.trim_twice p⟩ +/-- `toPoly` maps a canonical polynomial to `0` iff the polynomial is `0`. -/ +theorem toPoly_eq_zero_iff [Nontrivial R] [LawfulBEq R] (p : CPolynomial R) : + p.toPoly = 0 ↔ p = 0 := by + constructor + · intro hp + have hround : p.toPoly.toImpl = p := toImpl_toPoly_of_canonical p + rw [eq_comm] at hround + aesop + · aesop + /-- Evaluation is preserved by `toImpl`. -/ @[simp, grind =] theorem eval_toImpl_eq_eval [LawfulBEq R] (x : R) (p : R[X]) : p.toImpl.eval x = p.eval x := by From 2c42d71507747bb37a7a633e40fa43405327c772 Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Mon, 23 Feb 2026 14:40:49 +0000 Subject: [PATCH 10/18] feat: progress on correctness lemmas, fixing some bugs in API and cleaning up --- CompPoly/Bivariate/Basic.lean | 8 +- CompPoly/Bivariate/ToPoly.lean | 155 ++++++++++++++++++++++++++++++++- 2 files changed, 156 insertions(+), 7 deletions(-) diff --git a/CompPoly/Bivariate/Basic.lean b/CompPoly/Bivariate/Basic.lean index fbec93f..859aeb5 100644 --- a/CompPoly/Bivariate/Basic.lean +++ b/CompPoly/Bivariate/Basic.lean @@ -123,16 +123,14 @@ def evalEval (x y : R) (f : CBivariate R) : R := /-- Leading coefficient when viewed as a polynomial in Y. ArkLib: `Polynomial.Bivariate.leadingCoeffY`. -/ def leadingCoeffY (f : CBivariate R) : CPolynomial R := - f.val.coeff (f.val.natDegree) + f.val.leadingCoeff /-- Swap the roles of X and Y. ArkLib/Mathlib: `Polynomial.Bivariate.swap`. -/ def swap [DecidableEq R] (f : CBivariate R) : CBivariate R := (f.supportY).sum (fun j => - let coeffJ : CPolynomial R := - (CPolynomial.support (f.val.coeff j)).sum (fun i => - CPolynomial.monomial i ((f.val.coeff j).coeff i)) - CPolynomial.monomial j coeffJ) + (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 X. The coefficient of X^(degreeX f): a polynomial in Y. -/ diff --git a/CompPoly/Bivariate/ToPoly.lean b/CompPoly/Bivariate/ToPoly.lean index 8de2e64..9e1d00e 100644 --- a/CompPoly/Bivariate/ToPoly.lean +++ b/CompPoly/Bivariate/ToPoly.lean @@ -430,10 +430,161 @@ theorem degreeX_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] rw [ coeff_toPoly_Y ] exact Eq.symm (CPolynomial.natDegree_toPoly (f.val.coeff j)) +/-- +`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) : + toPoly (CC (R := R) r) = Polynomial.C (Polynomial.C r) := by + rw [ toPoly_eq_map ] + unfold CBivariate.CC + simp [ CPolynomial.C_toPoly ] + change (CPolynomial.C r).toPoly = Polynomial.C r + exact CPolynomial.C_toPoly 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] : + toPoly (X (R := R)) = Polynomial.C Polynomial.X := by + rw [ toPoly_eq_map ] + simp [ CBivariate.X, CPolynomial.C_toPoly ] + change (CPolynomial.X : CPolynomial R).toPoly = Polynomial.X + exact CPolynomial.X_toPoly + +/-- +`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] : + 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)) + +/-- +`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] + [DecidableEq R] (n m : ℕ) (c : R) : + toPoly (monomialXY (R := R) n m c) = Polynomial.monomial m (Polynomial.monomial n c) := by + unfold CBivariate.monomialXY + rw [ toPoly_monomial ] + congr + simpa using CPolynomial.monomial_toPoly (R := R) n c + +/-- +`supportX` corresponds to the union of inner supports of outer coefficients. +-/ +theorem supportX_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] + (f : CBivariate R) : + CBivariate.supportX (R := R) f = + (toPoly f).support.biUnion (fun j => ((toPoly f).coeff j).support) := by + unfold CBivariate.supportX + rw [ support_toPoly_outer ] + refine Finset.biUnion_congr rfl ?_ + intro j hj + simpa [ coeff_toPoly_outer ] using (CPolynomial.support_toPoly (f.val.coeff j)) + +/-- +`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] + (f : CBivariate R) : + CBivariate.totalDegree (R := R) f = + (toPoly f).support.sup (fun j => ((toPoly f).coeff j).natDegree + j) := by + unfold CBivariate.totalDegree + rw [ support_toPoly_outer ] + refine Finset.sup_congr rfl ?_ + intro j hj + rw [ coeff_toPoly_outer ] + simpa using congrArg (fun n => n + j) (CPolynomial.natDegree_toPoly (f.val.coeff j)) + +/-- +`evalX a` evaluates each inner coefficient at `a`. +-/ +theorem evalX_toPoly_coeff {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] + [DecidableEq R] (a : R) (f : CBivariate R) (j : ℕ) : + ((evalX (R := R) a f).toPoly).coeff j = ((toPoly f).coeff j).eval a := by + sorry + +/-- +`evalX` is compatible with full bivariate evaluation. +-/ +theorem evalX_toPoly_eval {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] + [DecidableEq R] (a y : R) (f : CBivariate R) : + (evalX (R := R) a f).eval y = (toPoly f).evalEval a y := by + sorry + +/-- +`evalY a` corresponds to outer evaluation at `Polynomial.C a`. +-/ +theorem evalY_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] + (a : R) (f : CBivariate R) : + (evalY (R := R) a f).toPoly = (toPoly f).eval (Polynomial.C a) := by + unfold CBivariate.evalY + have h_toPoly : (toPoly f).eval (Polynomial.C a) = (f.val.eval (CPolynomial.C a)).toPoly := by + unfold CBivariate.toPoly + simp +decide [ Polynomial.eval_finset_sum, CPolynomial.Raw.eval ] + unfold CPolynomial.Raw.eval₂ + simp +decide + have h_foldl : ∀ (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 + intro arr y + induction' arr using Array.recOn with arr ih + induction' arr using List.reverseRecOn with arr ih + · rfl + · simp_all +decide [ Finset.sum_range_succ, Array.zipIdx ] + rw [ Finset.sum_congr rfl fun i hi => by rw [ List.getElem?_append ] ] + rw [ Finset.sum_congr rfl fun i hi => by rw [ if_pos (Finset.mem_range.mp hi) ] ] + convert congr_arg₂ ( · + · ) ‹_› rfl using 1 + convert CPolynomial.Raw.toPoly_add _ _ using 1 + · congr! 1 + have h_toPoly_mul : ∀ (p q : CPolynomial R), + (p * q).toPoly = p.toPoly * q.toPoly := by grind + convert h_toPoly_mul ih (CPolynomial.C y ^ arr.length) |> Eq.symm using 1 + congr! 1 + induction' arr.length with n ih <;> simp_all +decide [ pow_succ ] + · exact Eq.symm ( CPolynomial.Raw.toPoly_one ) + · congr! 1 + exact Eq.symm (CPolynomial.C_toPoly y) + · infer_instance + rw [ h_foldl, Finset.sum_subset ] + · exact fun i hi => Finset.mem_range.mpr + (Nat.lt_of_lt_of_le (Finset.mem_range.mp (Finset.mem_filter.mp hi |>.1)) (by simp)) + · simp +contextual [ CPolynomial.support ] + simp +decide [ CPolynomial.toPoly, CPolynomial.Raw.toPoly ] + unfold CPolynomial.Raw.eval₂ + erw [ Array.foldl_empty ] + simp + exact h_toPoly.symm + +/-- +`leadingCoeffY` corresponds to the leading coefficient in the outer variable. +-/ +theorem leadingCoeffY_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] + (f : CBivariate R) : + (leadingCoeffY (R := R) f).toPoly = (toPoly f).leadingCoeff := by + sorry + +/-- +`swap` exchanges X- and Y-exponents. +-/ +theorem swap_toPoly_coeff {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] + [DecidableEq R] (f : CBivariate R) (i j : ℕ) : + ((toPoly (swap (R := R) f)).coeff j).coeff i = ((toPoly f).coeff i).coeff j := by + sorry + +/-- +`leadingCoeffX` is the Y-leading coefficient of the swapped polynomial. +-/ +theorem leadingCoeffX_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] + [DecidableEq R] (f : CBivariate R) : + (leadingCoeffX (R := R) f).toPoly = (toPoly (swap (R := R) f)).leadingCoeff := by + simpa [ CBivariate.leadingCoeffX ] using + (leadingCoeffY_toPoly (R := R) (f := CBivariate.swap (R := R) f)) + end ImplementationCorrectness end CBivariate --- TODO correctness lemmas for operations and API functions - end CompPoly From 99beed8d743c8d3bdb4a61c4725d0cd37f5b1ec1 Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Tue, 24 Feb 2026 10:31:04 +0000 Subject: [PATCH 11/18] feat: proof of leadingCoeffY_toPoly --- CompPoly/Bivariate/ToPoly.lean | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/CompPoly/Bivariate/ToPoly.lean b/CompPoly/Bivariate/ToPoly.lean index 9e1d00e..9545679 100644 --- a/CompPoly/Bivariate/ToPoly.lean +++ b/CompPoly/Bivariate/ToPoly.lean @@ -564,7 +564,16 @@ theorem evalY_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] theorem leadingCoeffY_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] (f : CBivariate R) : (leadingCoeffY (R := R) f).toPoly = (toPoly f).leadingCoeff := by - sorry + 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 /-- `swap` exchanges X- and Y-exponents. From ffc7743e3817d25054b08a232a91a96f55355d26 Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Tue, 24 Feb 2026 10:45:03 +0000 Subject: [PATCH 12/18] fix: remove unnecessary [Nontrivial R] --- CompPoly/Univariate/Basic.lean | 2 +- CompPoly/Univariate/ToPoly.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/CompPoly/Univariate/Basic.lean b/CompPoly/Univariate/Basic.lean index 79c2438..510c067 100644 --- a/CompPoly/Univariate/Basic.lean +++ b/CompPoly/Univariate/Basic.lean @@ -547,7 +547,7 @@ theorem degree_eq_natDegree (p : CPolynomial R) (hp : p ≠ 0) : rw [hk] /-- The natural degree is the maximum element of the support. -/ -theorem natDegree_eq_support_sup [Nontrivial R] (p : CPolynomial R) : +theorem natDegree_eq_support_sup (p : CPolynomial R) : p.natDegree = p.support.sup (fun n => n) := by have := p.2 unfold CPolynomial.Raw.trim at this diff --git a/CompPoly/Univariate/ToPoly.lean b/CompPoly/Univariate/ToPoly.lean index b17d6a9..75f6426 100644 --- a/CompPoly/Univariate/ToPoly.lean +++ b/CompPoly/Univariate/ToPoly.lean @@ -210,7 +210,7 @@ theorem Raw.toImpl_toPoly [LawfulBEq R] (p : CPolynomial.Raw R) : p.toPoly.toImp exact toImpl_toPoly_of_canonical ⟨ p.trim, Trim.trim_twice p⟩ /-- `toPoly` maps a canonical polynomial to `0` iff the polynomial is `0`. -/ -theorem toPoly_eq_zero_iff [Nontrivial R] [LawfulBEq R] (p : CPolynomial R) : +theorem toPoly_eq_zero_iff [LawfulBEq R] (p : CPolynomial R) : p.toPoly = 0 ↔ p = 0 := by constructor · intro hp From 73b401156ed3c811ca1adb337c7553cad357ec7e Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Tue, 24 Feb 2026 10:53:00 +0000 Subject: [PATCH 13/18] fix: remove redundant lemma --- CompPoly/Bivariate/ToPoly.lean | 15 ++------------- 1 file changed, 2 insertions(+), 13 deletions(-) diff --git a/CompPoly/Bivariate/ToPoly.lean b/CompPoly/Bivariate/ToPoly.lean index 9545679..191e8ad 100644 --- a/CompPoly/Bivariate/ToPoly.lean +++ b/CompPoly/Bivariate/ToPoly.lean @@ -356,17 +356,6 @@ theorem coeff_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] · congr · by_cases h : j < ( f.val.size : ℕ ) <;> aesop -/-- The outer `Y`-coefficient of `toPoly f` is `CPolynomial.toPoly (f.val.coeff j)`. -/ -theorem coeff_toPoly_outer {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] - (f : CBivariate R) (j : ℕ) : - (toPoly f).coeff j = CPolynomial.toPoly (f.val.coeff j) := by - simp [CBivariate.toPoly] - rw [ Finset.sum_eq_single j ] <;> simp +decide [ Polynomial.coeff_monomial ] - · aesop - · intro hj - rw [ CPolynomial.support ] at hj - by_cases hj' : j < f.val.size <;> aesop - /-- 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] (f : CBivariate R) : (toPoly f).support = f.supportY := by @@ -481,7 +470,7 @@ theorem supportX_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R rw [ support_toPoly_outer ] refine Finset.biUnion_congr rfl ?_ intro j hj - simpa [ coeff_toPoly_outer ] using (CPolynomial.support_toPoly (f.val.coeff j)) + simpa [ toPoly_coeff ] using (CPolynomial.support_toPoly (f.val.coeff j)) /-- `totalDegree` corresponds to the supremum over `j` of `natDegree ((toPoly f).coeff j) + j`. @@ -494,7 +483,7 @@ theorem totalDegree_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Rin rw [ support_toPoly_outer ] refine Finset.sup_congr rfl ?_ intro j hj - rw [ coeff_toPoly_outer ] + rw [ toPoly_coeff ] simpa using congrArg (fun n => n + j) (CPolynomial.natDegree_toPoly (f.val.coeff j)) /-- From f1355bd35e6320cfeef9010ae95737c23d506347 Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Wed, 25 Feb 2026 07:23:24 +0000 Subject: [PATCH 14/18] fix: style guide, respond to katy's comments --- CompPoly/Bivariate/Basic.lean | 16 ++++++++-------- CompPoly/Bivariate/ToPoly.lean | 4 ++-- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/CompPoly/Bivariate/Basic.lean b/CompPoly/Bivariate/Basic.lean index 859aeb5..3b5c5e3 100644 --- a/CompPoly/Bivariate/Basic.lean +++ b/CompPoly/Bivariate/Basic.lean @@ -34,7 +34,7 @@ namespace CBivariate variable {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] -/-- Extensionality: two bivariate polynomials are equal iff their underlying values are. -/ +/-- 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 := CPolynomial.ext h @@ -96,8 +96,8 @@ def natDegreeY (f : CBivariate R) : ℕ := f.val.natDegree /-- The `X`-degree: maximum over all Y-coefficients of their degree in X. - ArkLib: `Polynomial.Bivariate.degreeX`. -/ -def degreeX (f : CBivariate R) : ℕ := + ArkLib: `Polynomial.Bivariate.natDegreeX`. -/ +def natDegreeX (f : CBivariate R) : ℕ := (CPolynomial.support f).sup (fun n => (f.val.coeff n).natDegree) /-- Total degree: max over monomials of (deg_X + deg_Y). @@ -120,11 +120,6 @@ def evalY (a : R) (f : CBivariate R) : CPolynomial R := def evalEval (x y : R) (f : CBivariate R) : R := CPolynomial.eval x (f.val.eval (CPolynomial.C y)) -/-- Leading coefficient when viewed as a polynomial in Y. - ArkLib: `Polynomial.Bivariate.leadingCoeffY`. -/ -def leadingCoeffY (f : CBivariate R) : CPolynomial R := - f.val.leadingCoeff - /-- Swap the roles of X and Y. ArkLib/Mathlib: `Polynomial.Bivariate.swap`. -/ def swap [DecidableEq R] (f : CBivariate R) : CBivariate R := @@ -132,6 +127,11 @@ def swap [DecidableEq R] (f : CBivariate R) : CBivariate R := (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 + /-- 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 := diff --git a/CompPoly/Bivariate/ToPoly.lean b/CompPoly/Bivariate/ToPoly.lean index 191e8ad..9aea699 100644 --- a/CompPoly/Bivariate/ToPoly.lean +++ b/CompPoly/Bivariate/ToPoly.lean @@ -396,9 +396,9 @@ 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 degreeX_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] +theorem natDegreeX_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] (f : CBivariate R) : - (toPoly f).support.sup (fun j => ((toPoly f).coeff j).natDegree) = f.degreeX := by + (toPoly f).support.sup (fun j => ((toPoly f).coeff j).natDegree) = f.natDegreeX := by convert (Finset.sup_congr ?_ ?_) · ext simp +decide [ coeff_toPoly_Y ] From ecc7e981ac066e83b1802dd4e7f9507cb78524f8 Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Wed, 25 Feb 2026 13:36:20 +0000 Subject: [PATCH 15/18] feat: add toPoly_one, ofPoly_one, and toPolyRingHom, ofPolyRingHom, etc --- CompPoly/Bivariate/ToPoly.lean | 63 ++++++++++++++++++++++++++-------- 1 file changed, 49 insertions(+), 14 deletions(-) diff --git a/CompPoly/Bivariate/ToPoly.lean b/CompPoly/Bivariate/ToPoly.lean index 9aea699..5eea7e3 100644 --- a/CompPoly/Bivariate/ToPoly.lean +++ b/CompPoly/Bivariate/ToPoly.lean @@ -55,14 +55,6 @@ def ofPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] let cj := p.coeff j CPolynomial.monomial j ⟨cj.toImpl, CPolynomial.Raw.trim_toImpl cj⟩) -/-- `toPoly` maps the zero bivariate polynomial to `0`. -/ -lemma toPoly_zero {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] : - toPoly (0 : CBivariate R) = 0 := by - -- The sum over the empty set is zero. - simp [CBivariate.toPoly] - rw [ Finset.sum_eq_zero ] - aesop - /-- `toPoly` preserves addition. -/ lemma toPoly_add {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] (p q : CBivariate R) : toPoly (p + q) = toPoly p + toPoly q := by @@ -120,12 +112,6 @@ lemma toPoly_monomial {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] · split_ifs <;> simp_all +decide [ Array.push ] exact toFinsupp_eq_zero.mp rfl -/-- `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] : - ofPoly (0 : R[X][Y]) = 0 := by - unfold CBivariate.ofPoly - simp +decide [ Polynomial.support ] - /-- `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] (n : ℕ) (c : R[X]) : @@ -292,6 +278,55 @@ noncomputable def ringEquiv map_mul' := by apply toPoly_mul map_add' := by exact fun x y => toPoly_add x y +/-- `toPoly` preserves `1`. -/ +theorem toPoly_one + {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring 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] : + 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] : + toPoly (0 : CBivariate R) = 0 := by + -- The sum over the empty set is zero. + simp [CBivariate.toPoly] + rw [ Finset.sum_eq_zero ] + 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] : + 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] : + 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[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] + (p q : R[X][Y]) : + ofPoly (p * q) = ofPoly p * ofPoly q := by + apply (ringEquiv (R := R)).injective + change toPoly (ofPoly (p * q)) = toPoly (ofPoly p * ofPoly q) + rw [ofPoly_toPoly, toPoly_mul, ofPoly_toPoly, ofPoly_toPoly] + end RingEquiv /-! Correctness lemmas for evaluation, coefficients, support, and degrees. -/ From 4bb2a569d02980878521c9be251624fe29d477fb Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Wed, 25 Feb 2026 23:27:24 +0000 Subject: [PATCH 16/18] feat: add more typeclasses and one TODO --- CompPoly/Bivariate/Basic.lean | 44 +++++++++++++++++++++++++++++++++-- 1 file changed, 42 insertions(+), 2 deletions(-) diff --git a/CompPoly/Bivariate/Basic.lean b/CompPoly/Bivariate/Basic.lean index 3b5c5e3..e94e463 100644 --- a/CompPoly/Bivariate/Basic.lean +++ b/CompPoly/Bivariate/Basic.lean @@ -32,7 +32,11 @@ def CBivariate (R : Type*) [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] := namespace CBivariate -variable {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] +variable {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] + +section Semiring + +variable [Semiring 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 := @@ -52,6 +56,40 @@ instance : AddCommMonoid (CBivariate R) := instance : Semiring (CBivariate R) := inferInstanceAs (Semiring (CPolynomial (CPolynomial R))) +end Semiring + +section CommSemiring + +variable [CommSemiring R] + +instance : CommSemiring (CBivariate R) := by + letI : CommSemiring (CPolynomial R) := inferInstance + simpa [CBivariate] using (inferInstance : CommSemiring (CPolynomial (CPolynomial R))) + +end CommSemiring + +section Ring + +variable [Ring R] + +instance : Ring (CBivariate R) := by + letI : Ring (CPolynomial R) := inferInstance + simpa [CBivariate] using (inferInstance : Ring (CPolynomial (CPolynomial R))) + +end Ring + +section CommRing + +variable [CommRing R] + +instance : CommRing (CBivariate R) := by + letI : CommRing (CPolynomial R) := inferInstance + simpa [CBivariate] using (inferInstance : CommRing (CPolynomial (CPolynomial R))) + +end CommRing + +-- TODO any remaining typeclasses? + -- --------------------------------------------------------------------------- -- Operation stubs (for ArkLib compatibility; proofs deferred) -- --------------------------------------------------------------------------- @@ -121,7 +159,9 @@ def evalEval (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`. -/ + ArkLib/Mathlib: `Polynomial.Bivariate.swap`. + TODO a more efficient implementation + -/ def swap [DecidableEq R] (f : CBivariate R) : CBivariate R := (f.supportY).sum (fun j => (CPolynomial.support (f.val.coeff j)).sum (fun i => From b2b76013744354daa76dd3abf4846589e7c41abe Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Wed, 25 Feb 2026 23:39:39 +0000 Subject: [PATCH 17/18] feat: add some TODOs for future PRs --- CompPoly/Bivariate/Basic.lean | 2 ++ CompPoly/Univariate/Basic.lean | 1 + 2 files changed, 3 insertions(+) diff --git a/CompPoly/Bivariate/Basic.lean b/CompPoly/Bivariate/Basic.lean index e94e463..70914b3 100644 --- a/CompPoly/Bivariate/Basic.lean +++ b/CompPoly/Bivariate/Basic.lean @@ -96,6 +96,8 @@ end CommRing -- ArkLib's Polynomial.Bivariate uses: coeff, natDegreeY, degreeX, totalDegree, -- evalX, evalY, leadingCoeffY, swap. These will be implemented and proven -- equivalent to Mathlib/ArkLib via ToPoly.lean. +-- TODO: Add bridge lemmas/equivalences between `CBivariate R` and +-- `CMvPolynomial 2 R` for interoperability with the multivariate API. -- --------------------------------------------------------------------------- section Operations diff --git a/CompPoly/Univariate/Basic.lean b/CompPoly/Univariate/Basic.lean index 2f2fea5..98c4ba8 100644 --- a/CompPoly/Univariate/Basic.lean +++ b/CompPoly/Univariate/Basic.lean @@ -29,6 +29,7 @@ variable {R : Type*} [BEq R] is non-zero (or the polynomial is empty). This provides a unique representative for each polynomial equivalence class. + 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 } From dd34ce37c5c8e79a3f781dec33e2672a4ad4645c Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Wed, 25 Feb 2026 23:43:02 +0000 Subject: [PATCH 18/18] fix: style guide --- CompPoly/Bivariate/Basic.lean | 12 ++++----- CompPoly/Bivariate/ToPoly.lean | 48 +++++++++++++++++----------------- 2 files changed, 30 insertions(+), 30 deletions(-) diff --git a/CompPoly/Bivariate/Basic.lean b/CompPoly/Bivariate/Basic.lean index 70914b3..f47104b 100644 --- a/CompPoly/Bivariate/Basic.lean +++ b/CompPoly/Bivariate/Basic.lean @@ -128,7 +128,7 @@ def supportY (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 ℕ := - (CPolynomial.support f).biUnion (fun j => CPolynomial.support (f.val.coeff j)) + (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`. -/ @@ -138,17 +138,17 @@ def natDegreeY (f : CBivariate R) : ℕ := /-- The `X`-degree: maximum over all Y-coefficients of their degree in X. ArkLib: `Polynomial.Bivariate.natDegreeX`. -/ def natDegreeX (f : CBivariate R) : ℕ := - (CPolynomial.support f).sup (fun n => (f.val.coeff n).natDegree) + (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) : ℕ := - (CPolynomial.support f).sup (fun m => (f.val.coeff m).natDegree + m) + (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 := - (CPolynomial.support f).sum (fun j => CPolynomial.monomial j (CPolynomial.eval a (f.val.coeff j))) + (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`. -/ @@ -165,8 +165,8 @@ def evalEval (x y : R) (f : CBivariate R) : R := TODO a more efficient implementation -/ def swap [DecidableEq R] (f : CBivariate R) : CBivariate R := - (f.supportY).sum (fun j => - (CPolynomial.support (f.val.coeff j)).sum (fun i => + (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. diff --git a/CompPoly/Bivariate/ToPoly.lean b/CompPoly/Bivariate/ToPoly.lean index 5eea7e3..340a432 100644 --- a/CompPoly/Bivariate/ToPoly.lean +++ b/CompPoly/Bivariate/ToPoly.lean @@ -41,7 +41,7 @@ section ToPolyCore -/ noncomputable def toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] (p : CBivariate R) : R[X][Y] := - (CPolynomial.support p).sum (fun j => + (CPolynomial.support p).sum (fun j ↦ monomial j (CPolynomial.toPoly (p.val.coeff j))) /-- Convert Mathlib's `R[X][Y]` to `CBivariate R` (inverse of `toPoly`). @@ -51,7 +51,7 @@ noncomputable def toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring -/ def ofPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] [DecidableEq R] (p : R[X][Y]) : CBivariate R := - (p.support).sum (fun j => + (p.support).sum (fun j ↦ let cj := p.coeff j CPolynomial.monomial j ⟨cj.toImpl, CPolynomial.Raw.trim_toImpl cj⟩) @@ -138,7 +138,7 @@ lemma toImpl_add {R : Type*} [BEq R] [LawfulBEq R] [Ring R] (p q : R[X]) : intros p q h_eq have h_coeff : ∀ n, p.coeff n = q.coeff n := by intro n; exact (by - convert congr_arg (fun f => f.coeff n) h_eq using 1 <;> + convert congr_arg (fun f ↦ f.coeff n) h_eq using 1 <;> simp +decide [ CPolynomial.Raw.coeff_toPoly ]) exact CPolynomial.Raw.Trim.eq_of_equiv h_coeff convert h_add_trim _ _ h_add using 1 @@ -160,14 +160,14 @@ lemma ofPoly_add {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] [Deci unfold CBivariate.ofPoly intro p q rw [ Finset.sum_subset - ( show (p + q |> Polynomial.support) ⊆ p.support ∪ q.support from fun x hx => ?_ ) ] + ( show (p + q |> Polynomial.support) ⊆ p.support ∪ q.support from fun x hx ↦ ?_ ) ] · simp +zetaDelta at * rw [ Finset.sum_subset (show p.support ⊆ p.support ∪ q.support from Finset.subset_union_left), Finset.sum_subset (show q.support ⊆ p.support ∪ q.support from Finset.subset_union_right) ] · rw [ ← Finset.sum_add_distrib ] - refine' Finset.sum_congr rfl fun x hx => _ + refine' Finset.sum_congr rfl fun x hx ↦ _ rw [ ← CPolynomial.monomial_add ] congr exact Eq.symm (toImpl_add (p.coeff x) (q.coeff x)) @@ -183,7 +183,7 @@ theorem ofPoly_coeff {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring 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 = - Finset.sum (Polynomial.support p) (fun j => + Finset.sum (Polynomial.support p) (fun j ↦ CPolynomial.coeff (CPolynomial.monomial j ⟨Polynomial.toImpl (Polynomial.coeff p j), @@ -258,7 +258,7 @@ theorem toPoly_ofPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] apply CPolynomial.eq_iff_coeff.mpr intro i -- Since `toPoly` is injective on canonical polynomials, coefficients equal ⇒ poly equal. - have h_inj : Function.Injective (fun p : CPolynomial R => p.toPoly) := by + have h_inj : Function.Injective (fun p : CPolynomial R ↦ p.toPoly) := by intro p q h_eq have := CPolynomial.toImpl_toPoly_of_canonical p have := CPolynomial.toImpl_toPoly_of_canonical q @@ -276,7 +276,7 @@ noncomputable def ringEquiv left_inv := toPoly_ofPoly right_inv := ofPoly_toPoly map_mul' := by apply toPoly_mul - map_add' := by exact fun x y => toPoly_add x y + map_add' := by exact fun x y ↦ toPoly_add x y /-- `toPoly` preserves `1`. -/ theorem toPoly_one @@ -345,7 +345,7 @@ theorem evalEval_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R simp +decide -- Rewrite the right-hand side to match the left-hand side. have h_foldl : ∀ (arr : Array (CPolynomial R)) (y : R), - (Array.foldl (fun (acc : CPolynomial R) (x : CPolynomial 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 intro arr y @@ -353,8 +353,8 @@ theorem evalEval_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R induction' arr using List.reverseRecOn with arr ih · rfl · simp_all +decide [ Finset.sum_range_succ, Array.zipIdx ] - rw [ Finset.sum_congr rfl fun i hi => by rw [ List.getElem?_append ] ] - rw [ Finset.sum_congr rfl fun i hi => by rw [ if_pos (Finset.mem_range.mp hi) ] ] + rw [ Finset.sum_congr rfl fun i hi ↦ by rw [ List.getElem?_append ] ] + rw [ Finset.sum_congr rfl fun i hi ↦ by rw [ if_pos (Finset.mem_range.mp hi) ] ] convert congr_arg₂ ( · + · ) ‹_› rfl using 1 convert CPolynomial.Raw.toPoly_add _ _ using 1 · congr! 1 @@ -369,7 +369,7 @@ theorem evalEval_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R exact Eq.symm (CPolynomial.C_toPoly y) · infer_instance rw [ h_foldl, Finset.sum_subset ] - · exact fun i hi => Finset.mem_range.mpr + · exact fun i hi ↦ Finset.mem_range.mpr (Nat.lt_of_lt_of_le (Finset.mem_range.mp (Finset.mem_filter.mp hi |>.1)) (by simp)) · simp +contextual [ CPolynomial.support ] simp +decide [ CPolynomial.toPoly, CPolynomial.Raw.toPoly ] @@ -412,7 +412,7 @@ theorem natDegreeY_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring · simp +decide [ hp ] · refine' le_antisymm _ _ · exact Finset.le_sup (f := id) (Polynomial.natDegree_mem_support_of_nonzero hp) - · exact Finset.sup_le fun i hi => Polynomial.le_natDegree_of_mem_supp _ hi + · exact Finset.sup_le fun i hi ↦ Polynomial.le_natDegree_of_mem_supp _ hi 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 @@ -433,7 +433,7 @@ theorem coeff_toPoly_Y {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] /-- `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] (f : CBivariate R) : - (toPoly f).support.sup (fun j => ((toPoly f).coeff j).natDegree) = f.natDegreeX := by + (toPoly f).support.sup (fun j ↦ ((toPoly f).coeff j).natDegree) = f.natDegreeX := by convert (Finset.sup_congr ?_ ?_) · ext simp +decide [ coeff_toPoly_Y ] @@ -442,12 +442,12 @@ theorem natDegreeX_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring · -- Since `toPoly` is injective, if `toPoly (f.coeff j) = 0`, then `f.coeff j = 0`. have h_inj : ∀ (p : CPolynomial R), p.toPoly = 0 ↔ p = 0 := by intro p - exact ⟨fun hp => by + exact ⟨fun hp ↦ by apply Subtype.ext - apply_fun (fun p => p.toImpl) at hp + apply_fun (fun p ↦ p.toImpl) at hp convert hp using 1 exact Eq.symm (CPolynomial.toImpl_toPoly_of_canonical p), - fun hp => by aesop⟩ + fun hp ↦ by aesop⟩ aesop · exact (CPolynomial.toPoly_eq_zero_iff 0).mpr rfl · intro j hj @@ -500,7 +500,7 @@ theorem monomialXY_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring theorem supportX_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] (f : CBivariate R) : CBivariate.supportX (R := R) f = - (toPoly f).support.biUnion (fun j => ((toPoly f).coeff j).support) := by + (toPoly f).support.biUnion (fun j ↦ ((toPoly f).coeff j).support) := by unfold CBivariate.supportX rw [ support_toPoly_outer ] refine Finset.biUnion_congr rfl ?_ @@ -513,13 +513,13 @@ theorem supportX_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R theorem totalDegree_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] (f : CBivariate R) : CBivariate.totalDegree (R := R) f = - (toPoly f).support.sup (fun j => ((toPoly f).coeff j).natDegree + j) := by + (toPoly f).support.sup (fun j ↦ ((toPoly f).coeff j).natDegree + j) := by unfold CBivariate.totalDegree rw [ support_toPoly_outer ] refine Finset.sup_congr rfl ?_ intro j hj rw [ toPoly_coeff ] - simpa using congrArg (fun n => n + j) (CPolynomial.natDegree_toPoly (f.val.coeff j)) + simpa using congrArg (fun n ↦ n + j) (CPolynomial.natDegree_toPoly (f.val.coeff j)) /-- `evalX a` evaluates each inner coefficient at `a`. @@ -550,7 +550,7 @@ theorem evalY_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] unfold CPolynomial.Raw.eval₂ simp +decide have h_foldl : ∀ (arr : Array (CPolynomial R)) (y : R), - (Array.foldl (fun (acc : CPolynomial R) (x : CPolynomial 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 intro arr y @@ -558,8 +558,8 @@ theorem evalY_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] induction' arr using List.reverseRecOn with arr ih · rfl · simp_all +decide [ Finset.sum_range_succ, Array.zipIdx ] - rw [ Finset.sum_congr rfl fun i hi => by rw [ List.getElem?_append ] ] - rw [ Finset.sum_congr rfl fun i hi => by rw [ if_pos (Finset.mem_range.mp hi) ] ] + rw [ Finset.sum_congr rfl fun i hi ↦ by rw [ List.getElem?_append ] ] + rw [ Finset.sum_congr rfl fun i hi ↦ by rw [ if_pos (Finset.mem_range.mp hi) ] ] convert congr_arg₂ ( · + · ) ‹_› rfl using 1 convert CPolynomial.Raw.toPoly_add _ _ using 1 · congr! 1 @@ -573,7 +573,7 @@ theorem evalY_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] exact Eq.symm (CPolynomial.C_toPoly y) · infer_instance rw [ h_foldl, Finset.sum_subset ] - · exact fun i hi => Finset.mem_range.mpr + · exact fun i hi ↦ Finset.mem_range.mpr (Nat.lt_of_lt_of_le (Finset.mem_range.mp (Finset.mem_filter.mp hi |>.1)) (by simp)) · simp +contextual [ CPolynomial.support ] simp +decide [ CPolynomial.toPoly, CPolynomial.Raw.toPoly ]