Structures:
Basic "algebraic" structures: types with decidable equality and with order.
Common instances can be found in orders-ex.
More developped algebra can be found in the
mathematical components
library.
Arith-base:
Basic Peano Arithmetic.
Everything can be loaded with From Stdlib Require Import Arith_base.
To enjoy the ring and lia automatic tactic, you additionally need to load
arith below, using From Stdlib Require Import Arith Lia.
PArith:
Binary representation of positive integers for effective computation.
You may also want narith and zarith below for N and Z
built on top of positive.
NArith-base:
Binary natural numbers.
Everything can be loaded with From Stdlib Require Import NArith_base.
To enjoy the ring automatic tactic, you need to load
narith below, using From Stdlib Require Import NArith.
ZArith:
Binary encoding of integers.
This binary encoding was initially developped to enable effective
computations, compared to the unary encoding of nat. Proofs were then added
making the types usable for mathematical proofs, although this was not
the initial intent. If even-more efficient computations are needed, look
at the primitive-int package below for 63 bits machine arithmetic
or the coq-bignums package for arbitrary precision machine arithmetic.
Everything can be imported with From Stdlib Require Import ZArith.
Also contains the migromega tactic that can be loaded with
From Stdlib Require Import Lia.
Zmod and Zstar:
Modular arithmetic -- integers modulo another integer -- including machine
words (bitvectors) and the multiplicative group of integers modulo another
integer.
Primitive Integers:
Interface for hardware integers (63 rather than 64 bits due to OCaml
garbage collector). This enables very efficient arithmetic, for developing
tactics for proofs by reflection for instance.
Floats:
Efficient machine floating-point arithmetic
Interface to hardware floating-point arithmetic for efficient computations.
This offers a basic model of floating-point arithmetic but is not very
usable alone. Look at the coq-flocq package for an actual model of
floating-point arithmetic, including links to Stdlib reals and the current
Floats.
Vectors:
Dependent datastructures storing their length.
This is known to be technically difficult to use. It is often much better
to use a dependent pair with a list and a proof about its length,
as provided by the tuple type in package coq-mathcomp-ssreflect,
allowing almost transparent mixing with lists.
Sets:
Classical sets. This is known to be outdated. More modern alternatives
can be found in coq-mathcomp-ssreflect (for finite sets)
and coq-mathcomp-classical (for classical sets) or coq-stdpp.
QArith:
Binary rational numbers, made on top of zarith.
Those enable effective computations in arbitrary precision exact rational
arithmetic. Those rationals are known to be difficult to use for
mathematical proofs because there is no canonical representation
(2/3 and 4/6 are not equal for instance). For even more efficient
computation, look at the coq-bignums package which uses machine integers.
For mathematical proofs, the rat type of the coq-mathcomp-algebra package
are much more comfortable, although they don't enjoy efficient computation
(coq-coqeal offers a refinement with coq-bignums that enables to enjoy
both aspects).
Reals:
Formalization of real numbers.
Most of it can be loaded with From Stdlib Require Import Reals.
Also contains the micromega tactics, loadable with
From Stdlib Require Import Lra. and From Stdlib Require Import Psatz.
Classical Reals:
Real numbers with excluded middle, total order and least upper bounds