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:
CoqEAL
The easiest way to install the latest released version of CoqEAL is via OPAM:
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-coqeal
To instead build and install manually, do:
git clone https://github.com/coq-community/coqeal.git
cd coqeal
make # or make -j <number-of-cores-on-your-machine>
make install
The theory directory has the following content:
ssrcomplements
, minor
mxstructure
, polydvd
, similar
,
binetcauchy
, ssralg_ring_tac
: Various extensions of the
Mathematical Components library.
dvdring
, coherent
, stronglydiscrete
, edr
: Hierarchy of
structures with divisibility (from rings with divisibility, PIDs,
elementary divisor rings, etc.).
fpmod
: Formalization of finitely presented modules.
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.
The refinements directory has the following content:
refinements
: Classes for refinements and refines together with
operational typeclasses for common operations.
binnat
: Proof that the binary naturals of Coq (N
) are a refinement
of the MathComp unary naturals (nat
) together with basic operations.
binord
: Proof that the binary natural numbers of Coq (N
) are a refinement
of the MathComp ordinals.
binint
: MathComp integers (ssrint
) are refined to a new type
parameterized by positive numbers (represented by a sigma type) and
natural numbers. This means that proofs can be done using only
lemmas from the MathComp library which leads to simpler proofs than
previous versions of binint
(e.g., N
).
binrat
: Arbitrary precision rational numbers (bigQ
) from the
Bignums library are refined to
MathComp's rationals (rat
).
rational
: The rational numbers of MathComp (rat
) are refined to
pairs of elements refining integers using parametricity of
refinements.
seqmatrix
and seqmx_complements
: Refinement of MathComp
matrices (M[R]_(m,n)
) to lists of lists (seq (seq R)
).
seqpoly
: Refinement of MathComp polynomials ({poly R}
) to lists (seq R
).
multipoly
: Refinement of
MathComp multinomials
and multivariate polynomials to Coq
finite maps.
Files should use the following conventions (w.r.t. Local
and Global
instances):
(** Part 1: Generic operations *)
Section generic_operations.
Global Instance generic_operation := ...
(** Part 2: Correctness proof for proof-oriented types and programs *)
Section theory.
Local Instance param_correctness : param ...
(** Part 3: Parametricity *)
Section parametricity.
Global Instance param_parametricity : param ...
Proof. exact: param_trans. Qed.
End parametricity.
End theory.