Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

documentation changes, adding grobner #71

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

documentation changes, adding grobner #71

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
32 changes: 21 additions & 11 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -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))
Expand Down Expand Up @@ -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,
Expand All @@ -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.
Expand All @@ -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
Expand All @@ -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.
Expand Down
16 changes: 10 additions & 6 deletions coq-coqeal.opam
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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")}
Expand All @@ -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: [
Expand All @@ -49,4 +52,5 @@ authors: [
"Damien Rouhling"
"Pierre Roux"
"Vincent Siles"
"Laurent Théry"
]
38 changes: 26 additions & 12 deletions meta.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -60,6 +60,8 @@ authors:
initial: false
- name: Vincent Siles
initial: true
- name: Laurent Théry
initial: false

maintainers:
- name: Cyril Cohen
Expand All @@ -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:
Expand Down Expand Up @@ -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,
Expand All @@ -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.
Expand All @@ -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
Expand All @@ -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.
Expand Down