Gröbner Tactics

This repository contains Lean 4 tactics for the automated formal verification of Gröbner basis properties and computations.

Our main goal is to create powerful tactics that can automatically prove theorems related to Groebner Basis or the application of Groebner Basis within the Lean 4 theorem prover.

The foundational definitions and core theorems on which this work is built are developed in the companion project groebner_proj. One of the main technical challenges in Lean is that the standard MvPolynomial type is, in general, non-computable from the perspective of proof automation. To overcome this limitation, we introduce a dedicated implementation of computable polynomials that is suitable for execution and computation within Lean's kernel.

Both the library and its accompanying documentation are still under development.

Introduction

Workflow

1. Lean to Externel Solvers: We extract mathematical objects (such as MvPolynomial and generators of Ideals) from the Lean context and employ meta-programming techniques, specifically Qq matching, or manual pattern matching, to deconstruct and analyze Lean expressions.
2. External Computation: Gröbner basis–related computations on multivariate polynomials are delegated to externel solvers. The computed results are serialized into a structured JSON format and returned to Lean, where they are reinterpreted for subsequent verifications.
3. Externel Solver to Lean: Lean parses the incoming JSON data into well-defined intermediate data structures. These structures are then systematically translated back into Expr and ultimately elaborated into Term objects in Lean, allowing the externally computed results to be integrated into the proof environment.
4. Kernel Verification: The verification tasks are reduced to polynomial identity testing （PIT) problems which are discharged entirely within the Lean kernel using its internal computable polynomial representation.

Tactics

1. gb_solve:
   • Certifies that the remainder of a polynomial $f$ upon reduction modulo a set $B$ is $r$.
   • Verifies that a set $B$ is a groebner basis of an ideal $I$.
   • Decides whether a polynomial $f$ belongs to an ideal $I$.
   • Decides whether a polynomial $f$ belongs to the radical ideal $\sqrt{I}$.
2. idealeq: Verifies the equality of two ideals, $I = J$
3. add_gb_hyp: Automatically computes a Gröbner basis $G$ for the ideal generated by $B$ using SageMath and adds the certified $G$ as a hypothesis in Lean.

Modes

Our tactic supports three modes: local SageMath computation (default), external SageMath computation (not recommended), and local SymPy computation.

-- local SageMath computation mode
example :
    lex.IsRemainder (X 0 ^ 2 + X 1 ^ 3 + X 2 ^ 4 + X 3 ^ 5: MvPolynomial (Fin 4) ℚ)
      {X 0, X 1, X 2, X 3} 0 := by
  gb_solve

-- externel SageMath computation (API, not recommended)
set_option gb_tactic.backend 1 in
example :
    lex.IsRemainder (X 0 ^ 2 + X 1 ^ 3 + X 2 ^ 4 + X 3 ^ 5: MvPolynomial (Fin 4) ℚ)
      {X 0, X 1, X 2, X 3} 0 := by
  gb_solve

-- local Sympy computation
set_option gb_tactic.backend 2 in
example :
    lex.IsRemainder (X 0 ^ 2 + X 1 ^ 3 + X 2 ^ 4 + X 3 ^ 5: MvPolynomial (Fin 4) ℚ)
      {X 0, X 1, X 2, X 3} 0 := by
  gb_solve

Some Example

gb_solve

Given a polynomial $f$ and a divisor set $G$, the gb_solve tactic automatically certifies the remainder of $f$ reduced modulo $G$. In this example, it proves that reducing $f = x_0 x_1$ modulo the set $\{2x_0 - x_1\}$ yields the remainder $r = \frac{1}{2} x_1^2$.

-- Certifies that the remainder of a polynomial $f$ upon reduction  modulo a set $B$ is $r$
example :
    lex.IsRemainder (X 0 * X 1 : MvPolynomial (Fin 3) ℚ)
      {2 * X 0 - X 1}
      (C (1/2 : ℚ) * X 1 ^ 2) := by
  gb_solve

The tactic can formally verify if a given set of polynomials constitutes a Gröbner basis for a specific ideal. Here, it proves that $\{1\}$ is indeed the Gröbner basis for the ideal generated by $\{x_0, 1 - x_0\}$.

-- Verifies that a set $B$ is a groebner basis of an ideal $I$
example :
  lex.IsGroebnerBasis
  ({1} : Set <| MvPolynomial (Fin 3) ℚ)
  (Ideal.span ({X 0, 1 - X 0} : Set <| MvPolynomial (Fin 3) ℚ)) := by
  gb_solve

The tactic can automatically decide and prove whether a given polynomial $f$ belongs to an ideal $I$ generated by a set of polynomials. It seamlessly handles both positive ($\in$) and negative ($\notin$) membership cases. Here, it proves that $x_0$ is an element of the ideal generated by $\{x_0, x_1\}$.

-- Decides a polynomial $f$ belongs to an ideal $I$
example :
  X 0 ∈ Ideal.span ({X 0, X 1} : Set (MvPolynomial (Fin 2) ℚ)) := by
  gb_solve

In this example, it proves that $x_2$ does not belong to the ideal generated by $\{x_0 + x_1^2, x_1^2\}$.

-- Decides a polynomial $f$ doesn't belong to an ideal $I$
example :
   X 2 ∉ Ideal.span ({X 0 + X 1^ 2, X 1 ^ 2} : Set (MvPolynomial (Fin 3) ℚ)) := by
  gb_solve

Beyond standard ideals, the tactic can determine if a polynomial $f$ lies within the radical of an ideal, denoted as $\sqrt{I}$. It automatically handles the underlying algebraic transformations to prove both membership and non-membership. For instance, it verifies that the polynomial $x_0 x_1$ is in the radical of the ideal generated by $\{\frac{1}{2}(x_0 + x_1), \frac{1}{2}(x_0 - x_1)\}$.

-- Decides a polynomial $f$ belongs to the radical ideal  $\sqrt{I}$
example :
  X 0 * X 1 ∈ (Ideal.span ({C (1/2 : ℚ) * (X 0 + X 1), C (1/2 : ℚ) * (X 0 - X 1)} :
   Set (MvPolynomial (Fin 2) ℚ))).radical := by
  gb_solve

Conversely, it correctly determines that $x_0$ is not in the radical of the ideal generated by $\{x_0 + x_1\}$.

-- Decides a polynomial $f$ doesn't belong to the radical ideal  $\sqrt{I}$
example :
  X 0 ∉ (Ideal.span ({X 0 + X 1} : Set (MvPolynomial (Fin 3) ℚ))).radical := by
  gb_solve

idealeq

The idealeq tactic automates the proof of equality between two polynomial ideals. It internally computes and compares their Gröbner bases to determine if the ideals generated by two different sets of polynomials are mathematically identical.

In the example below, it automatically verifies that the ideal generated by $\{x_0 + x_1^2, x_1\}$ is equal to the ideal generated by $\{x_0, x_1\}$.

example :
  Ideal.span ({X 0 + X 1^2, X 1 }) =
    Ideal.span ({X 0, X 1 } : Set (MvPolynomial (Fin 3) ℚ)) := by
   idealeq

add_gb_hyp

Instead of directly closing a goal, the add_gb_hyp tactic computes the Gröbner basis for a specified set of polynomials and injects this fact as a new hypothesis into the local proof context. This is particularly useful when the Gröbner basis property is required as an intermediate step for further manual reasoning.

In this example, calling add_gb_hyp h calculates the Gröbner basis for the ideal generated by $\{x_0, x_0 + x_1\}$ and introduces a new hypothesis h stating that this basis is $\{x_0, x_1\}$. After some standard simplification, h exactly matches and closes the goal.

example : lex.IsGroebnerBasis ({X 0, X 1} :
 Set (MvPolynomial (Fin 3) ℚ)) (Ideal.span {X 0, X 0 + X 1}) := by
  add_gb_hyp h ({X 0, X 0 + X 1} : Set (MvPolynomial (Fin 3) ℚ))
  simp only [ne_eq, one_ne_zero, not_false_eq_true, div_self, C_1, Fin.isValue, pow_one, one_mul,
    zero_add] at h
  exact h

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/GroebnerTactic.git
cd GroebnerTactic
lake exe cache get
lake build

If you want to use Sagemath as an external calculation tool, please follow the official SageMath installation instructions.

If you find that SageMath takes up too much storage space, or that installing SageMath on Windows is too cumbersome, you can opt to use SymPy as an external computation tool.

For Linux/MacOS systems, please run the following command:

python -m venv newenv
source newenv/bin/activate
pip install -r requirements.txt

For Windows CMD, please run the following command:

python -m venv newenv
newenv\Scripts\activate.bat
pip install -r requirements.txt

For Windows Powershell, please run the following command:

python -m venv newenv
.\newenv\Scripts\Activate.ps1
pip install -r requirements.txt

Installation

To use our tactics in your Lean 4 project, you need to add this repository as a dependency. Adding he following block to your project's lakefile.toml:

[[require]]
name = "GroebnerTactic"
git = "https://github.com/WuProver/GroebnerTactic.git"
scope  = "WuProver"
rev = "main"

To use the full features, please download Sage as instructed above. Since installing Sage on Windows can be quite cumbersome, you can install Python instead and run the following commands.

python -m venv newenv
source newenv/bin/activate
pip install -r .lake/packages/GroebnerTactic/requirements.txt

If you prefer not to install anything, you can use the API mode, but please use it sparingly.