From 4dcb7bde084d062f62af5f64dc132be2d22f1026 Mon Sep 17 00:00:00 2001
From: thery <thery@sophia.inria.fr>
Date: Fri, 19 Feb 2016 13:02:53 +0100
Subject: [PATCH] configure

---
 Make         |  4 ++++
 README.md    | 32 +++++++++++++++++++++++++++++++-
 configure.sh |  4 ++++
 grobner.v    | 14 ++++++--------
 4 files changed, 45 insertions(+), 9 deletions(-)
 create mode 100644 Make
 create mode 100755 configure.sh

diff --git a/Make b/Make
new file mode 100644
index 0000000..1e7a89f
--- /dev/null
+++ b/Make
@@ -0,0 +1,4 @@
+grobner.v
+
+-I .
+-R . mathcomp.contrib.grobner
diff --git a/README.md b/README.md
index 541a05f..11f4c46 100644
--- a/README.md
+++ b/README.md
@@ -1,2 +1,32 @@
 # grobner
-A fornalisation of Grobner basis in ssreflect
+A fornalisation of Grobner basis in ssreflect.
+It contains one file
+
+grobner.v
+
+It define 
+
+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)
+
diff --git a/configure.sh b/configure.sh
new file mode 100755
index 0000000..58f22d4
--- /dev/null
+++ b/configure.sh
@@ -0,0 +1,4 @@
+#!/bin/sh
+
+coq_makefile -f Make -o Makefile
+
diff --git a/grobner.v b/grobner.v
index d4a83f0..d8de105 100644
--- a/grobner.v
+++ b/grobner.v
@@ -1,8 +1,6 @@
 Require Import Inverse_Image.
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype.
-Require Import tuple bigop ssralg poly.
-Require Import ssrcomplements poset freeg mpoly.
-
+From mathcomp Require Import all_ssreflect all_algebra.
+From SsrMultinomials Require Import ssrcomplements poset freeg mpoly.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -1499,18 +1497,18 @@ elim: n => [|n IH].
   apply: bar_1 => a; apply: bar_1 => b; apply: bar_0 => /=.
   by rewrite !orbF; apply/forallP => /= [[]].
 pose f (a : nat * 'X_{1..n}) := [multinom of a.1 :: a.2].
-pose R1 := [rel a b | (~~ (b.1 < a.1)) && (lem a.2 b.2)].
+pose R1 := [rel a b | ((~~ (b.1 < a.1)) && (lem a.2 b.2))%N].
 rewrite [bar_r _ _]/(bar_r (@lem _)[seq f i | i <- [::]]).
 have HR1R a b : R1 _ a b -> @lem _ (f a) (f b).
   case/andP=> aLb /forallP Ht.
   apply/mnm_lepP=> /= [[[|i] Hi]] /=.
     by rewrite /fun_of_multinom /= !(tnth_nth 0%N) /= leqNgt.
-  have := Ht (Ordinal (Hi : i < n)).
+  have := Ht (Ordinal (Hi : (i < n)%N)).
   by rewrite /fun_of_multinom !(tnth_nth 0%N) /=.
 apply: bar_r_map HR1R _ _ _ => [a|].
   case: a => t; exists (tnth t ord0, [multinom [tuple of behead t]]).
   by apply/val_eqP=> /=; apply/eqP/val_eqP; case: t => /= [[]].
-have Hlt a b : (a < b) -> (a < b)%coq_nat by move/ltP.
+have Hlt a b : (a < b)%N -> (a < b)%coq_nat by move/ltP.
 exact: bar_r_prod_nil (Wf_nat.well_founded_lt_compat _ _ _ Hlt) IH.
 Qed.
 
@@ -1554,7 +1552,7 @@ Implicit Types m : 'X_{1..n}.
 (* Order on pairs of polynomials *)
 Definition psplt (psp1 psp2 : seq {mpoly R[n]} * seq {mpoly R[n]}) :=
   (splt psp1.1 psp2.1) || 
-  ((psp1.1 == psp2.1) && (size psp1.2 < size psp2.2)).
+  ((psp1.1 == psp2.1) && (size psp1.2 < size psp2.2)%N).
 
 Lemma wf_ltn : well_founded (ltn : nat -> nat -> bool).
 Proof.