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.
- Author(s):
- Laurent Théry (initial)
- Henrik Persson (initial)
- Rocq-community maintainer(s):
- Karl Palmskog (@palmskog)
- License: GNU Lesser General Public License v2.1 or later
- Compatible Rocq/Coq versions: 8.18 or later
- Additional dependencies: none
- Rocq/Coq namespace:
Buchberger - Related publication(s):
The easiest way to install the latest released version of Buchberger is via OPAM:
opam repo add rocq-released https://rocq-prover.org/opam/released
opam install coq-buchbergerTo instead build and install manually, you need to make sure that all the libraries this development depends on are installed. The easiest way to do that is still to rely on opam:
git clone https://github.com/coq-community/buchberger.git
cd buchberger
opam repo add rocq-released https://rocq-prover.org/opam/released
opam install --deps-only .
make # or make -j <number-of-cores-on-your-machine>
make installThis 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.
An alternative formalization of Gröbner bases in Coq using the SSReflect proof language and the Mathematical Components library is available elsewhere.