A fornalisation of Grobner basis in ssreflect
Coq Shell
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
Make
README.md
configure.sh
grobner.v

README.md

grobner

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

grobner.v

It defines

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

(* p belongs to the ideal generated by L *)

Check 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)