The Rocq Standard Library

This is the index of the Rocq standard library. It provides a set of modules directly available through the From Stdlib Require Import command.

stdlib_deps bool bool classes classes bool->classes program program classes->program relations relations classes->relations corelib-wrapper corelib-wrapper program->corelib-wrapper logic logic program->logic relations->corelib-wrapper strings strings arith arith strings->arith ring ring arith->ring reals reals qarith qarith reals->qarith vectors vectors reals->vectors lqa lqa reals->lqa classical-logic classical-logic reals->classical-logic nsatz nsatz reals->nsatz field field qarith->field lists lists vectors->lists lqa->field classical-logic->arith zarith zarith nsatz->zarith qarith-base qarith-base nsatz->qarith-base arith-base arith-base structures structures arith-base->structures structures->bool lia lia zarith->lia lia->arith field->zarith field->qarith-base positive positive positive->arith-base narith narith narith->positive ring->lists zarith-base zarith-base ring->zarith-base lists->arith-base zarith-base->narith primitive-int primitive-int primitive-int->zarith unicode unicode primitive-int->unicode fmaps-fsets-msets fmaps-fsets-msets fmaps-fsets-msets->zarith orders-ex orders-ex fmaps-fsets-msets->orders-ex orders-ex->strings sorting sorting orders-ex->sorting sorting->vectors sorting->lia sets sets sorting->sets sets->classical-logic primitive-floats primitive-floats primitive-floats->primitive-int wellfounded wellfounded wellfounded->lists primitive-string primitive-string primitive-string->primitive-int primitive-string->orders-ex qarith-base->ring extraction extraction extraction->primitive-floats extraction->primitive-string primitive-array primitive-array extraction->primitive-array primitive-array->primitive-int streams streams streams->logic funind funind funind->arith-base rtauto rtauto rtauto->positive rtauto->lists compat compat compat->reals compat->fmaps-fsets-msets compat->wellfounded compat->primitive-string compat->extraction compat->streams compat->funind compat->rtauto all all all->compat

The standard library is composed of the following subdirectories:

Logic: Logic, dependent equality, extensionality, choice axioms. Look at classical-logic for more elaborate results.
SetIsType StrictProp Decidable Eqdep_dec EqdepFacts Eqdep JMeq RelationalChoice Berardi Hurkens ProofIrrelevance ProofIrrelevanceFacts ConstructiveEpsilon PropExtensionalityFacts FunctionalExtensionality ExtensionalFunctionRepresentative ExtensionalityFacts WeakFan PropFacts HLevels Adjointification
Program: Support for dependently-typed programming Beware that there are also Tactics.v and Wf.v files in Init.
Subset Equality Syntax WfExtensionality Program Combinators
Relations: Relations (definitions and basic results)
Relation_Operators Relations Operators_Properties
Classes:
Morphisms_Relations CEquivalence SetoidClass RelationPairs DecidableClass
Bool: Booleans (basic functions and results)
Bool BoolEq DecBool IfProp
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.
Equalities Orders OrdersTac OrdersFacts GenericMinMax
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.
PeanoNat Between Peano_dec Compare_dec (Arith_base) Compare EqNat Euclid Factorial Wf_nat Cantor Zerob NumPrelude NZAdd NZAddOrder NZAxioms NZBase NZMul NZDiv NZMulOrder NZOrder NZParity NZPow NZSqrt NZLog NZGcd NZBits NAdd NAddOrder NAxioms NBase NMulOrder NOrder NStrongRec NSub NDiv NDiv0 NMaxMin NParity NPow NSqrt NLog NGcd NLcm NLcm0 NBits NProperties SetoidDec
Lists: Polymorphic lists
List ListDec ListSet ListTactics NaryFunctions WKL EquivDec
Streams: Streams (infinite sequences)
Streams StreamMemo
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.
AltBinNotations BinPosDef BinPos Pnat POrderedType (PArith)
NArith: Binary natural numbers
BinNatDef BinNat Nnat Ndec Ndiv_def Ngcd_def Nsqrt_def (NArith)
ZArith-base: Basic binary integers
ZAdd ZAddOrder ZAxioms ZBase ZLt ZMul ZMulOrder ZSgnAbs ZMaxMin ZParity ZPow ZGcd ZLcm ZBits ZProperties ZDivFloor ZDivTrunc BinIntDef BinInt Zorder Zcompare Znat Zmin Zmax Zminmax Zabs Zeven auxiliary ZArith_dec Zbool Zmisc Wf_Z Zhints (ZArith_base) Zpow_alt Int
Ring: Ring tactic.
Zcomplements Zpow_def Zdiv Znumtheory
Arith: Basic Peano arithmetic
(Arith)
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.
Zpower Zquot (ZArith) Zgcd_alt Zwf Zpow_facts Zdiv_facts Zbitwise DecimalFacts DecimalNat DecimalPos DecimalN DecimalZ HexadecimalFacts HexadecimalNat HexadecimalPos HexadecimalN HexadecimalZ
Unicode: Unicode-based alternative notations
Utf8_core Utf8
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.
CyclicAxioms NZCyclic DoubleType Cyclic63 Uint63 Sint63 Ring63
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.
FloatLemmas (Floats)
Primitive Arrays: Persistent native arrays, enabling efficient computations with arrays.
PArray
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.
Fin VectorDef VectorSpec VectorEq (Vector) FinFun Bvector
Strings Implementation of string as list of ASCII characters Beware that there is also a Byte.v file in Init.
Byte Ascii String BinaryString HexString OctalString DecimalString HexadecimalString
Classical Logic: Classical logic, dependent equality, extensionality, choice axioms
Classical_Pred_Type Classical_Prop (Classical) ClassicalFacts ChoiceFacts ClassicalChoice ClassicalDescription ClassicalEpsilon ClassicalUniqueChoice SetoidChoice Diaconescu Description Epsilon IndefiniteDescription PropExtensionality
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.
Classical_sets Constructive_sets Cpo Ensembles Finite_sets_facts Finite_sets Image Infinite_sets Integers Multiset Partial_Order Permut Powerset_Classical_facts Powerset_facts Powerset Relations_1_facts Relations_1 Relations_2_facts Relations_2 Relations_3_facts Relations_3 Uniset
Sorting: Axiomatizations of sorts
SetoidList SetoidPermutation Heap Permutation Sorting PermutEq PermutSetoid Mergesort Sorted CPermutation
Structure Instances: Instances of order structures from Structures above. DecidableType* and OrderedType* are there only for compatibility.
EqualitiesFacts OrdersAlt OrdersEx OrdersLists DecidableType DecidableTypeEx OrderedType OrderedTypeAlt OrderedTypeEx BoolOrder
Primitive Strings Native string type
PString
QArith-base: Basic binary rational numbers. Look at qarith below for more functionalities with the field and Lqa tactics.
QArith_base Qreduction QOrderedType Qminmax
Field: Field tactic.
Qpower Qring Qfield Qcanon Qround
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).
Qabs (QArith) Qcabs DecimalQ HexadecimalQ
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
Rdefinitions ClassicalDedekindReals ClassicalConstructiveReals Raxioms RIneq DiscrR ROrderedType Rminmax (Rbase) RList Ranalysis Rbasic_fun Rderiv Rfunctions Zfloor Rgeom R_Ifp Rlimit Rseries Rsigma R_sqr Rtrigo_fun Rtrigo1 Rtrigo Rtrigo_facts Ratan Machin SplitAbsolu SplitRmult Alembert AltSeries ArithProp Binomial Cauchy_prod Cos_plus Cos_rel Exp_prop Integration MVT NewtonInt PSeries_reg PartSum R_sqrt Ranalysis1 Ranalysis2 Ranalysis3 Ranalysis4 Ranalysis5 Ranalysis_reg Rcomplete RiemannInt RiemannInt_SF Rpow_def Rpower Rprod Rsqrt_def Rtopology Rtrigo_alt Rtrigo_calc Rtrigo_def Rtrigo_reg SeqProp SeqSeries Sqrt_reg Rlogic Rregisternames (Reals) Runcountable
Abstract Constructive Reals: Interface of constructive reals, proof of equivalence of all implementations. EXPERIMENTAL
ConstructiveReals ConstructiveRealsMorphisms ConstructiveLUB ConstructiveAbs ConstructiveLimits ConstructiveMinMax ConstructivePower ConstructiveSum
Constructive Cauchy Reals: Cauchy sequences of rational numbers, implementation of the interface. EXPERIMENTAL
ConstructiveRcomplete ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveCauchyAbs Qreals DecimalR HexadecimalR
MSets: Modular implementation of finite sets using lists or efficient trees. This is a modernization of FSets.
MSetInterface MSetFacts MSetDecide MSetProperties MSetEqProperties MSetWeakList MSetList MSetGenTree MSetAVL MSetRBT MSetPositive MSetToFiniteSet (MSets)
FSets: Modular implementation of finite sets/maps using lists or efficient trees. For sets, please consider the more modern MSets.
FSetInterface FSetBridge FSetFacts FSetDecide FSetProperties FSetEqProperties FSetList FSetWeakList FSetCompat FSetAVL FSetPositive (FSets) FSetToFiniteSet FMapInterface FMapWeakList FMapList FMapPositive FMapFacts (FMaps) FMapAVL FMapFullAVL
Wellfounded: Well-founded Relations
Disjoint_Union Inclusion Inverse_Image Lexicographic_Exponentiation Lexicographic_Product List_Extension Transitive_Closure Union Wellfounded Well_Ordering
Compat: Compatibility wrappers for previous versions of Stdlib
AdmitAxiom Stdlib818