The Rocq Standard Library

These modules are available through the From Stdlib Require Import command.

This table of components covers top-level modules intended for direct use. For an exhaustive listing of standard-library modules (public and internal) as well as the internal dependencies between them, see the subcomponent index. There is also an alphabetical index of all modules and objects.

To find specific lemmas and defintions in the standard library, do From Stdlib Require All. (no Import!) and use the Search command, for example Search (_ * (_ + _)).

Concrete Computable Objects

Bool: Booleans bool (true and false), boolean operators, and their properties.
Byte: A variant type with 256 cases.
PeanoNat: Unary natural numbers nat. The first-principles construction in this module is intended for learning, use for structural recursion, and for type indices in advanced dependently typed programming. For code that treats natural numbers opaquely, consider NArith.
List: Lists of any element type (e.g. list nat).
NArith: Natural numbers N. For Peano induction, use N.peano_ind.
ZArith: Integers Z. Induction: Z.peano_ind, Z.order_induction_0 or, for non-negative, Wf_Z.natlike_ind.
Zmod: Integers modulo another integer (Zmod m).
Bits: Machine integers, machine words, or bitvectors (bits n).
Zstar: Multiplicative group of coprime integers modulo another integer (Zstar m).
QArith: Rational numbers with canonical and non-canonical representations (Qc and Q). Also consider rat from math-comp or bigQ from coq-bignums.
SpecFloat: Floating-point numbers spec_float, defined following the fully specified subset of IEEE-754 (without NaN payloads). Continued in flocq.

Programming Aides

Utf8: notations for quantifiers and operators.
Wf: well-founded recursion (Fix) for non-structural recursion based on a termination proof.
Wellfounded: Relations without infinite descending chains for termination proofs.
Program: More intensive elaboration; documented in the Rocq Prover manual: Program. Also consider rocq-equations.

Decision Procedures

Documented in the Rocq Prover manual: Automatic Solvers.

Real Numbers

Reals: Classical real numbers R with excluded middle, total order and least upper bounds.
Reals: Axiomatization and uniqeness of constructive real numbers.
Cauchy.ConstructiveRcomplete: Construction and completeness of Cauchy real numbers.

Advanced Dependendly Typed Programming

EqDep_dec: Uniqueness of proofs of decidable equalities.
Vector: Lists with length-dependent type, constructed as an inductive type indexed by a nat (the length). This construction is uniquely suitable for nesting with other inductive types, but direct proofs about it require skilled use of dependent pattern matching with an in clause. Indirect reasoning about vectors converted to lists is often preferred. If nesting is not needed, consider using list, potentially paired with a proof about its length.
Fin: Bounded natural numbers, constructed as an inductive type indexed by a nat (the strict upper bound). This construction matches the index space of Vector, but again direct proofs about it require skilled use of dependent pattern matching with an in clause. Further, Fin.t n is inhabited only if n is nonzero, so a natural number cannot be a always converted to Fin.t (unlike Zmod 0, which is isomorphic to Z).

Study of Rocq's Logic

The standard library contains substantial study of near-paradoxes and edge cases in Rocq's logic. See the logic and classical-logic subcomponents. However, if looking at the included sets library, also consider math-comp/analysis/classical.

Axiomatized OCaml Primitives

Rocq Prover documentation: Primitive Objects.

Uint63: OCaml 63-bit unsigned integers and axioms relating them to Z.
Sint63: OCaml 63-bit signed integers and axioms relating them to Z.
Floats: Hardware floating-point arithmetic and axioms relating them to SpecFloat.
PArray: Persistent arrays implemented in OCaml using internal mutability.
PString