documentation changes, adding grobner

Author: palmskog

README.md

@@ -23,11 +23,11 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 
 
 
-This Coq library contains a subset of the work that was developed in the context
-of the ForMath EU FP7 project (2009-2013). It has two parts:
-- theory, which contains developments in algebra including normal forms of matrices,
-  and optimized algorithms on MathComp data structures.
-- refinements, which is a framework to ease change of data representations during a proof.
+This Coq library is based on Mathematical Components and has two parts:
+- theory, which contains developments in algebra, including normal forms of matrices
+  and optimized algorithms for matrix operations and on structures such as polynomials.
+- refinements, which is a framework to ease change of data representations during a proof
+  with the help of parametricity.
 
 ## Meta
 
@@ -40,6 +40,7 @@ of the ForMath EU FP7 project (2009-2013). It has two parts:
   - Damien Rouhling
   - Pierre Roux
   - Vincent Siles (initial)
+  - Laurent Théry
 - Coq-community maintainer(s):
   - Cyril Cohen ([**@CohenCyril**](https://github.com/CohenCyril))
   - Pierre Roux ([**@proux01**](https://github.com/proux01))
@@ -83,13 +84,20 @@ make install
 ```
 
 
+## Background
+
+The library hosts a subset of the work that was developed in the context of
+the ForMath EU FP7 project (2009-2013). More information about
+the project and its deliverables is available on its
+[website](http://wiki.portal.chalmers.se/cse/pmwiki.php/ForMath).
+
 ## Theory
 
-The theory directory has the following content:
+The `theory` directory has the following content:
 
 - `ssrcomplements`, `minor` `mxstructure`, `polydvd`, `similar`,
   `binetcauchy`, `ssralg_ring_tac`: Various extensions of the
-  Mathematical Components library.
+  Mathematical Components (MathComp) library.
 
 - `dvdring`, `coherent`, `stronglydiscrete`, `edr`: Hierarchy of
   structures with divisibility (from rings with divisibility, PIDs,
@@ -109,9 +117,12 @@ The theory directory has the following content:
   `strassen`, `toomcook`, `smithpid`, `smith`: Various efficient
   algorithms for computing operations on polynomials or matrices.
 
+- `grobner`: Formalization of Gröbner bases associated with polynomial
+   ideals, and Buchberger's algorithm for computing such bases.
+
 ## Refinements
 
-The refinements directory has the following content:
+The `refinements` directory has the following content:
 
 - `refinements`: Classes for refinements and refines together with
   operational typeclasses for common operations.
@@ -129,7 +140,7 @@ The refinements directory has the following content:
   previous versions of `binint` (e.g., `N`).
 
 - `binrat`: Arbitrary precision rational numbers (`bigQ`) from the
-  [Bignums](https://github.com/coq/bignums) library are refined to
+  [Bignums](https://github.com/coq-community/bignums) library are refined to
   MathComp's rationals (`rat`).
 
 - `rational`: The rational numbers of MathComp (`rat`) are refined to
@@ -143,11 +154,10 @@ The refinements directory has the following content:
 
 - `multipoly`: Refinement of
   [MathComp multinomials](https://github.com/math-comp/multinomials)
-  and multivariate polynomials to Coq
+  and multivariate polynomials to the Coq Stdlib's
   [finite maps](https://github.com/coq/coq/blob/master/theories/FSets/FMapAVL.v).
 
 Files should use the following conventions (w.r.t. `Local` and `Global` instances):
-
 ```coq
 (** Part 1: Generic operations *)
 Section generic_operations.

coq-coqeal.opam

@@ -12,16 +12,16 @@ license: "MIT"
 
 synopsis: "CoqEAL - The Coq Effective Algebra Library"
 description: """
-This Coq library contains a subset of the work that was developed in the context
-of the ForMath EU FP7 project (2009-2013). It has two parts:
-- theory, which contains developments in algebra including normal forms of matrices,
-  and optimized algorithms on MathComp data structures.
-- refinements, which is a framework to ease change of data representations during a proof."""
+This Coq library is based on Mathematical Components and has two parts:
+- theory, which contains developments in algebra, including normal forms of matrices
+  and optimized algorithms for matrix operations and on structures such as polynomials.
+- refinements, which is a framework to ease change of data representations during a proof
+  with the help of parametricity."""
 
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.13" & < "8.17~") | (= "dev")}
+  "coq" {(>= "8.13" & < "8.18~") | (= "dev")}
   "coq-bignums" 
   "coq-paramcoq" {>= "1.1.3"}
   "coq-mathcomp-multinomials" {((>= "1.5.1" & < "1.7~") | = "dev")}
@@ -38,6 +38,9 @@ tags: [
   "keyword:Bareiss"
   "keyword:Karatsuba multiplication"
   "keyword:refinements"
+  "keyword:Buchberger's algorithm"
+  "keyword:Gröbner basis"
+  "keyword:polynomials"
   "logpath:CoqEAL"
 ]
 authors: [
@@ -49,4 +52,5 @@ authors: [
   "Damien Rouhling"
   "Pierre Roux"
   "Vincent Siles"
+  "Laurent Théry"
 ]

meta.yml

@@ -11,11 +11,11 @@ synopsis: >-
   CoqEAL - The Coq Effective Algebra Library
 
 description: |-
-  This Coq library contains a subset of the work that was developed in the context
-  of the ForMath EU FP7 project (2009-2013). It has two parts:
-  - theory, which contains developments in algebra including normal forms of matrices,
-    and optimized algorithms on MathComp data structures.
-  - refinements, which is a framework to ease change of data representations during a proof.
+  This Coq library is based on Mathematical Components and has two parts:
+  - theory, which contains developments in algebra, including normal forms of matrices
+    and optimized algorithms for matrix operations and on structures such as polynomials.
+  - refinements, which is a framework to ease change of data representations during a proof
+    with the help of parametricity.
 
 publications:
 - pub_url: https://hal.inria.fr/hal-00734505/document
@@ -60,6 +60,8 @@ authors:
   initial: false
 - name: Vincent Siles
   initial: true
+- name: Laurent Théry
+  initial: false
 
 maintainers:
 - name: Cyril Cohen
@@ -77,7 +79,7 @@ license:
 
 supported_coq_versions:
   text: 8.13 or later (use releases for other Coq versions)
-  opam: '{(>= "8.13" & < "8.17~") | (= "dev")}'
+  opam: '{(>= "8.13" & < "8.18~") | (= "dev")}'
 
 dependencies:
 - opam:
@@ -141,18 +143,28 @@ keywords:
 - name: Bareiss
 - name: Karatsuba multiplication
 - name: refinements
+- name: Buchberger's algorithm
+- name: Gröbner basis
+- name: polynomials
 
 categories:
 - name: Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms
 
 documentation: |-
+  ## Background
+
+  The library hosts a subset of the work that was developed in the context of
+  the ForMath EU FP7 project (2009-2013). More information about
+  the project and its deliverables is available on its
+  [website](http://wiki.portal.chalmers.se/cse/pmwiki.php/ForMath).
+
   ## Theory
 
-  The theory directory has the following content:
+  The `theory` directory has the following content:
 
   - `ssrcomplements`, `minor` `mxstructure`, `polydvd`, `similar`,
     `binetcauchy`, `ssralg_ring_tac`: Various extensions of the
-    Mathematical Components library.
+    Mathematical Components (MathComp) library.
 
   - `dvdring`, `coherent`, `stronglydiscrete`, `edr`: Hierarchy of
     structures with divisibility (from rings with divisibility, PIDs,
@@ -172,9 +184,12 @@ documentation: |-
     `strassen`, `toomcook`, `smithpid`, `smith`: Various efficient
     algorithms for computing operations on polynomials or matrices.
 
+  - `grobner`: Formalization of Gröbner bases associated with polynomial
+     ideals, and Buchberger's algorithm for computing such bases.
+
   ## Refinements
 
-  The refinements directory has the following content:
+  The `refinements` directory has the following content:
 
   - `refinements`: Classes for refinements and refines together with
     operational typeclasses for common operations.
@@ -192,7 +207,7 @@ documentation: |-
     previous versions of `binint` (e.g., `N`).
 
   - `binrat`: Arbitrary precision rational numbers (`bigQ`) from the
-    [Bignums](https://github.com/coq/bignums) library are refined to
+    [Bignums](https://github.com/coq-community/bignums) library are refined to
     MathComp's rationals (`rat`).
 
   - `rational`: The rational numbers of MathComp (`rat`) are refined to
@@ -206,11 +221,10 @@ documentation: |-
 
   - `multipoly`: Refinement of
     [MathComp multinomials](https://github.com/math-comp/multinomials)
-    and multivariate polynomials to Coq
+    and multivariate polynomials to the Coq Stdlib's
     [finite maps](https://github.com/coq/coq/blob/master/theories/FSets/FMapAVL.v).
 
   Files should use the following conventions (w.r.t. `Local` and `Global` instances):
-
   ```coq
   (** Part 1: Generic operations *)
   Section generic_operations.