Merge pull request #54 from coq-community/add-matrix-normal-forms

Add matrix normal forms

README.md

@@ -25,7 +25,8 @@ 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 and optimized algorithms on mathcomp data structures.
+- 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.
 
 ## Meta
@@ -48,14 +49,16 @@ of the ForMath EU FP7 project (2009-2013). It has two parts:
   - [Bignums](https://github.com/coq/bignums) same version as Coq
   - [Paramcoq](https://github.com/coq-community/paramcoq) 1.1.3 or later
   - [MathComp Multinomials](https://github.com/math-comp/multinomials) >= 1.5.1 and < 1.7
-  - [MathComp](https://math-comp.github.io) 1.12.0 or newer
+  - [MathComp algebra](https://math-comp.github.io) 1.12.0 or later
+  - [MathComp real-closed](https://math-comp.github.io) 1.1.2 or later
 - Coq namespace: `CoqEAL`
 - Related publication(s):
   - [A refinement-based approach to computational algebra in Coq](https://hal.inria.fr/hal-00734505/document) doi:[10.1007/978-3-642-32347-8_7](https://doi.org/10.1007/978-3-642-32347-8_7)
   - [Refinements for free!](https://hal.inria.fr/hal-01113453/document) doi:[10.1007/978-3-319-03545-1_10](https://doi.org/10.1007/978-3-319-03545-1_10)
   - [A Coq Formalization of Finitely Presented Modules](https://hal.inria.fr/hal-01378905/document) doi:[10.1007/978-3-319-08970-6_13](https://doi.org/10.1007/978-3-319-08970-6_13)
   - [Formalized Linear Algebra over Elementary Divisor Rings in Coq](https://hal.inria.fr/hal-01081908/document) doi:[10.2168/LMCS-12(2:7)2016](https://doi.org/10.2168/LMCS-12(2:7)2016)
   - [A refinement-based approach to large scale reflection for algebra](https://hal.inria.fr/hal-01414881/document) 
+  - [Interaction entre algèbre linéaire et analyse en formalisation des mathématiques](https://tel.archives-ouvertes.fr/tel-00986283/) 
 
 ## Building and installation instructions
 
@@ -94,6 +97,11 @@ The theory directory has the following content:
 - `kaplansky`: For providing elementary divisor rings from the
   Kaplansky condition.
 
+- `closed_poly`: Polynomials with coefficients in a closed field.
+
+- `companion`, `frobenius_form`, `jordan`, `perm_eq_image`,
+  `smith_complements`: Results on normal forms of matrices.
+
 - `bareiss_dvdring`, `bareiss`, `gauss`, `karatsuba`, `rank`
   `strassen` `toomcook`, `smithpid`, `smith`: Various efficient
   algorithms for computing operations on polynomials or matrices.

_CoqProject

@@ -15,20 +15,26 @@ theory/atomic_operations.v
 theory/bareiss_dvdring.v
 theory/bareiss.v
 theory/binetcauchy.v
+theory/closed_poly.v
 theory/coherent.v
+theory/companion.v
 theory/dvdring.v
 theory/edr.v
 theory/fpmod.v
+theory/frobenius_form.v
 theory/gauss.v
+theory/jordan.v
 theory/kaplansky.v
 theory/karatsuba.v
 theory/minor.v
 theory/mxstructure.v
+theory/perm_eq_image.v
 theory/polydvd.v
 theory/rank.v
 theory/similar.v
 theory/smithpid.v
 theory/smith.v
+theory/smith_complements.v
 theory/ssralg_ring_tac.v
 theory/ssrcomplements.v
 theory/strassen.v

coq-coqeal.opam

@@ -14,7 +14,8 @@ 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 and optimized algorithms on mathcomp data structures.
+- 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."""
 
 build: [make "-j%{jobs}%"]
@@ -25,6 +26,7 @@ depends: [
   "coq-paramcoq" {>= "1.1.3"}
   "coq-mathcomp-multinomials" {((>= "1.5.1" & < "1.7~") | = "dev")}
   "coq-mathcomp-algebra" {((>= "1.12.0" & < "1.14~") | = "dev")}
+  "coq-mathcomp-real-closed" {(>= "1.1.2" & < "1.2~") | (= "dev")}
 ]
 
 tags: [

meta.yml

@@ -13,7 +13,8 @@ synopsis: >-
 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 and optimized algorithms on mathcomp data structures.
+  - 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.
 
 publications:
@@ -31,6 +32,8 @@ publications:
   pub_doi: 10.2168/LMCS-12(2:7)2016
 - pub_url: https://hal.inria.fr/hal-01414881/document
   pub_title: A refinement-based approach to large scale reflection for algebra
+- pub_url: https://tel.archives-ouvertes.fr/tel-00986283/
+  pub_title: Interaction entre algèbre linéaire et analyse en formalisation des mathématiques
 
 authors:
 - name: Guillaume Cano
@@ -87,7 +90,12 @@ dependencies:
     name: coq-mathcomp-algebra
     version: '{((>= "1.12.0" & < "1.14~") | = "dev")}'
   description: |-
-    [MathComp](https://math-comp.github.io) 1.12.0 or newer
+    [MathComp algebra](https://math-comp.github.io) 1.12.0 or later
+- opam:
+    name: coq-mathcomp-real-closed
+    version: '{(>= "1.1.2" & < "1.2~") | (= "dev")}'
+  description: |-
+    [MathComp real-closed](https://math-comp.github.io) 1.1.2 or later
 
 tested_coq_opam_versions:
 - version: '1.13.0-coq-8.14'
@@ -151,6 +159,11 @@ documentation: |-
   - `kaplansky`: For providing elementary divisor rings from the
     Kaplansky condition.
 
+  - `closed_poly`: Polynomials with coefficients in a closed field.
+
+  - `companion`, `frobenius_form`, `jordan`, `perm_eq_image`,
+    `smith_complements`: Results on normal forms of matrices.
+
   - `bareiss_dvdring`, `bareiss`, `gauss`, `karatsuba`, `rank`
     `strassen` `toomcook`, `smithpid`, `smith`: Various efficient
     algorithms for computing operations on polynomials or matrices.