MonomialOrderedPolynomial

This library provides a formally verified data structure for efficient polynomial identity testing via kernel reduction in Lean 4. By leveraging strictly ordered data structures, it ensures reliable in-kernel computation and verification of polynomial operations. Although primarily optimized for polynomial identity testing, the library also supports or plans to support a wide range of fundamental operations, including computing degrees, extracting coefficients, performing evaluations, and handling expansions of both univariate and multivariate polynomials across diverse contexts.

One of the project's goals is to develop tools that support both formal verification and the computation of Gröbner bases for polynomial ideals. Additionally, it may support other fundamental polynomial operations in the future, including the calculation of greatest common divisors, factorization, and solving polynomial systems. For our Gröbner basis formalization, see: WuProver/groebner_proj. This work is still in progress and under active development.

Both the library and its documents are still WIP.

Introduction

Main Contents

This library focuses on a structure based on a list where elements are sorted in order.

• List.lean: General operations and properties of the list structure.
• DSortedListMap.lean: Maps based on sorted list.
• DSortedFinsupp.lean: A sorted implementation of finitely-supported dependent functions DFinsupp within the Mathlib. It is built upon the DSortedListMap data structure.
• SortedFinsupp.lean: A sorted implementation of finitely-supported functions Finsupp within the Mathlib.
• SortedAddMonoidAlgebra.lean: A sorted implementation of AddMonoidAlgebra within the Mathlib.
• TreeRepr.lean: instances that extract a computable tree structure from concrete Polynomial expressions
• Polynomial.lean: equivalence of algebras from SortedAddMonoidAlgebra (where monomials are represented as sorted elements of a list) to Polynomial.
• MonomialOrder.lean: Order on SortedFinsupp.
• MvPolynomial.Lean: equivalence of algebras from SortedAddMonoidAlgebra to MvPolynomial.

How It Works

At its core, this library enables computation through a technique known as proof by reflection. We establish a formal isomorphism, defining a two-way translation between incomputable mathematical objects from Mathlib and our computable data structures. This allows the kernel to efficiently reduce concrete expressions about structures we defined, and prove propositions about the corresponding objects from Mathlib by the result, while guaranteeing mathematically sound and consistent with the original theory.

Build

If you don't already have Lean 4 set up, please follow the official Lean 4 installation instructions.

Once Lean is installed, you can clone this repository and build the project:

git clone https://github.com/WuProver/MonomialOrderedPolynomial.git
cd MonomialOrderedPolynomial
lake exe cache get
lake build

Capabilities about MvPolynomial and Polynomial

This library provides support for operations of polynomials (MvPolynomial and Polynomial) on SortedAddMonoidAlgebra:

• const,
• variable,
• addition/subtraction,
• multiplication,
• exponentiation.

One of their applications is PIT (polynomial identity testing).

The corresponding SortedAddMonoidAlgebra of concrete polynomials can be synthesized via an instance. Some examples are in PolynomialExamples.lean.

Polynomial-specific Operations

• Degree Computation (WIP, still not sorry-free): Calculation of polynomial degrees
• Coefficient Extraction (WIP, still not sorry-free): Retrieval of specific coefficients from polynomial expressions

open Polynomial

example : ((X ^ 3 + C 1) ^ 3 - X ^ 9: Int[X]).degree = 6 := by
  rw [Polynomial.PolyRepr.degree_eq]
  decide +kernel

example : ((X ^ 3 + C 1) ^ 3 - X ^ 9: Int[X]).degree ^ 2 = 36 := by
  rw [Polynomial.PolyRepr.degree_eq]
  decide +kernel

example : (((X + C (1 / 2 : ℚ)) ^ 3 : ℚ[X]) - X ^ 3).leadingCoeff = (3 / 2 : ℚ) := by
  rw [Polynomial.PolyRepr.leadingCoeff]
  decide +kernel

example : (((X + C (1 / 2 : ℚ)) ^ 3 : ℚ[X]) - X ^ 3).coeff 1 = (3 / 4 : ℚ) := by
  rw [Polynomial.PolyRepr.coeff]
  decide +kernel

MvPolynomial-specific Operations

• Degree Computation (TODO): Calculation of polynomial degrees w.r.t. a specific monomial order (such as lexicographic order);
• Coefficient Extraction (TODO): Retrieval of specific coefficients from polynomial expressions w.r.t. a specific monomial order.

Comparison on PIT

Our comparison is confined solely to polynomial operations within polynomial rings. Moreover, we only consider the case of processing a single goal or a single hypothesis.

Comparison Table

Some Examples

Polynomial

grind doesn't solve the polynomial identity test below, since the coefficients are rational numbers and it doesn't know Polynomial.C:

open Polynomial in
example : ((X + C (1 / 2 : ℚ)) ^ 2 : ℚ[X]) = ((X ^ 2 + X + C (1 / 4 : ℚ))) := by
  fail_if_success grind  -- `grind` failed
  sorry

Our approach is capable of establishing the following polynomial identity:

open Polynomial in
example : ((X + C (1 / 2 : ℚ)) ^ 2 : ℚ[X]) = ((X ^ 2 + X + C (1 / 4 : ℚ))) := by
  rw [Polynomial.PolyRepr.eq_iff']
  decide +kernel

grind cannot determine if two polynomials are not equal

open Polynomial in
example : ((X + 1) ^ 20 : Nat[X]) ≠ ((X ^ 2 + 2 * X +1) ^ 10: Nat[X]) + 1 := by
  fail_if_success grind  --`grind` failed
  sorry

We establish the following polynomial inequality using our method:

open Polynomial in
example : ((X + 1) ^ 20 : Nat[X]) ≠ ((X ^ 2 + 2 * X +1) ^ 10: Nat[X]) + 1 := by
  simp +decide [Polynomial.PolyRepr.eq_iff']

grind can prove some goals dependent on hypotheses, including but not limited to abstract algebra structures, unknown polynomials, and equations.

open Polynomial in
example {R : Type*} [CommRing R] (p : Polynomial R) : p + 1 + X = 1 + p + X := by
  grind

open Polynomial in
example {R : Type*} [CommRing R] (p q : Polynomial R) (h : p + 1 = q) :
    p ^ 2 - 1 + Polynomial.X = q ^ 2 - 2 * q + Polynomial.X := by
  grind

We simply note that our method is not yet able to handle the above examples.

MvPolynomial

Equality:

open MvPolynomial in
example : ((X 0 + X 1) ^ 10 : MvPolynomial Nat Nat) = ((X 1 ^ 2 + 2 * X 0 * X 1 + X 0 ^ 2) ^ 5) := by
  rw [MvPolynomial.PolyRepr.eq_iff'] -- this line is optional
  decide +kernel

Disequality:

open MvPolynomial in
example : ((X 0 + X 1 + 1) ^ 10 : MvPolynomial Nat Nat) ≠ ((X 1 ^ 2 + 2 * X 1 +1) ^ 5) := by
  rw [ne_eq, MvPolynomial.PolyRepr.eq_iff'] -- this line is optional
  decide +kernel

WIP

1. clean up code;
2. support more monomial orders;
3. refactor SortedFinsupp to replace dependent sum type Sigma (used as key-value pair) with independent Prod, to make it much faster;
4. faster algorithm;
5. a user-friendly way to interact with exponents and monomial order of MvPolynomial;
6. prove equalities via homomorphism from computable structures (such as ℕ, ℤ, ℚ, and ZMod n) to incomputable ones, and prove disequalities via embedding into them.

Thanks

This project, especially the approach of synthesizing computable structure from incomputable expressions, is inspired by Junyan Xu's work on polynomial computations via reflection. Addition inspiration comes from the implementation of computable sturctures of the algebraic solver of Grind.