Buchberger

A verified implementation of Buchberger's algorithm in Coq, which computes the Gröbner basis associated with a polynomial ideal. Also includes a constructive proof of Dickson's lemma.

Meta

• Author(s):
  • Laurent Théry (initial)
  • Henrik Persson (initial)
• Coq-community maintainer(s):
  • Karl Palmskog (@palmskog)
• License: GNU Lesser General Public License v2.1 or later
• Compatible Coq versions: 8.17 or later
• Additional dependencies: none
• Coq namespace: Buchberger
• Related publication(s):
  • A machine checked implementation of Buchberger's algorithm doi:10.1023/A:1026518331905
  • An Integrated Development of Buchberger's Algorithm in Coq
  • Gröbner Bases in Type Theory doi:10.1007/3-540-48167-2_3

Building and installation instructions

The easiest way to install the latest released version of Buchberger is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-buchberger

To instead build and install manually, do:

git clone https://github.com/coq-community/buchberger.git
cd buchberger
make   # or make -j <number-of-cores-on-your-machine> 
make install

Documentation

This project contains a Coq formalization of Buchberger's algorithm. It is composed of:

• A proof of correctness of the algorithm as described in A machine checked implementation of Buchberger's algorithm, Journal of Automated Reasoning, January 2001.
• An implementation of the algorithm. With respect to the paper, terms are not abstracted but built directly from coef and monomials.
• A constructive proof of Dickson's lemma due to Henrik Persson.

In the file Extract.v, it is explained how the extracted code found in sin_num.ml can be used to compute Gröbner bases.

Related work

An alternative formalization of Gröbner bases in Coq using the SSReflect proof language and the Mathematical Components library is available elsewhere.