Awesome

Grobner

A fornalisation of Grobner basis in ssreflect. It contains one file

grobner.v

It defines

From mathcomp Require Import all_ssreflect all_algebra.
From SsrMultinomials Require Import ssrcomplements freeg mpoly.
From mathcomp.contrib.grobner Require Import grobner.

Print ideal.

(*
ideal =
fun (R : ringType) (n : nat) (L : seq {mpoly R[n]}) (p : {mpoly R[n]})
  =>
  exists t, p = sum_(i < size L) t`_i * L`_i
*)

(* it is decidable *)

Check idealfP.
(*
idealfP
     : forall (R : fieldType)  (n : nat) (p : {mpoly R[n]})
              (l : seq {mpoly R[n]}),
       reflect (ideal l p) (idealf l p)
*)

Meta

• Author(s):
  • Laurent Théry
• License: MIT License
• Compatible Coq versions: 8.17 or later
• Additional dependencies:
  • MathComp ssreflect 2.1 or later
  • MathComp algebra 2.1 or later
  • MathComp Multinomials 2.1.0 or later
• Coq namespace: grobner
• Related publication(s): none

Building and installation instructions

To build and install manually, do:

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