The Coq Standard Library

Here is a short description of the Coq standard library, which is distributed with the system. It provides a set of modules directly available through the Require Import command.

The standard library is composed of the following subdirectories:

Init: The core library (automatically loaded when starting Coq)
Ltac Notations Datatypes Logic Byte Nat Decimal Hexadecimal Number Peano Specif Tactics Tauto Wf (Prelude)
Logic: Classical logic, dependent equality, extensionality, choice axioms
SetIsType StrictProp Classical_Pred_Type Classical_Prop (Classical) ClassicalFacts Decidable Eqdep_dec EqdepFacts Eqdep JMeq ChoiceFacts RelationalChoice ClassicalChoice ClassicalDescription ClassicalEpsilon ClassicalUniqueChoice SetoidChoice Berardi Diaconescu Hurkens ProofIrrelevance ProofIrrelevanceFacts ConstructiveEpsilon Description Epsilon IndefiniteDescription PropExtensionality PropExtensionalityFacts FunctionalExtensionality ExtensionalFunctionRepresentative ExtensionalityFacts WeakFan WKL FinFun PropFacts HLevels Adjointification
Structures: Algebraic structures (types with equality, with order, ...). DecidableType* and OrderedType* are there only for compatibility.
Equalities EqualitiesFacts Orders OrdersTac OrdersAlt OrdersEx OrdersFacts OrdersLists GenericMinMax DecidableType DecidableTypeEx OrderedType OrderedTypeAlt OrderedTypeEx
Bool: Booleans (basic functions and results)
Bool BoolEq BoolOrder DecBool IfProp Sumbool Zerob Bvector
Arith: Basic Peano arithmetic
PeanoNat Between Peano_dec Compare_dec (Arith_base) (Arith) Compare EqNat Euclid Factorial Wf_nat Cantor
PArith: Binary positive integers
BinPosDef BinPos Pnat POrderedType (PArith)
NArith: Binary natural numbers
BinNatDef BinNat Nnat Ndec Ndiv_def Ngcd_def Nsqrt_def (NArith)
ZArith: Binary integers
BinIntDef BinInt Zorder Zcompare Znat Zmin Zmax Zminmax Zabs Zeven auxiliary ZArith_dec Zbool Zmisc Wf_Z Zhints (ZArith_base) Zcomplements Zpow_def Zpow_alt Zpower Zdiv Zquot (ZArith) Zgcd_alt Zwf Znumtheory Int Zpow_facts Zbitwise
QArith: Rational numbers
QArith_base Qabs Qpower Qreduction Qring Qfield (QArith) Qreals Qcanon Qcabs Qround QOrderedType Qminmax
Numbers: An experimental modular architecture for arithmetic
  Prelude:
BinNums NumPrelude NaryFunctions AltBinNotations DecimalFacts DecimalNat DecimalPos DecimalN DecimalZ DecimalQ DecimalR DecimalString HexadecimalFacts HexadecimalNat HexadecimalPos HexadecimalN HexadecimalZ HexadecimalQ HexadecimalR HexadecimalString
  NatInt: Abstract mixed natural/integer/cyclic arithmetic
NZAdd NZAddOrder NZAxioms NZBase NZMul NZDiv NZMulOrder NZOrder NZParity NZPow NZSqrt NZLog NZGcd NZBits
  Cyclic: Abstract and 63-bits-based cyclic arithmetic
CyclicAxioms NZCyclic CarryType DoubleType Cyclic63 PrimInt63 Uint63 Sint63 Ring63
  Natural: Abstract and 63-bits-words-based natural arithmetic
NAdd NAddOrder NAxioms NBase NMulOrder NOrder NStrongRec NSub NDiv NDiv0 NMaxMin NParity NPow NSqrt NLog NGcd NLcm NLcm0 NBits NProperties
  Integer: Abstract and concrete (especially 63-bits-words-based) integer arithmetic
ZAdd ZAddOrder ZAxioms ZBase ZLt ZMul ZMulOrder ZSgnAbs ZMaxMin ZParity ZPow ZGcd ZLcm ZBits ZProperties ZDivFloor ZDivTrunc
  Floats: Floating-point arithmetic
FloatClass PrimFloat SpecFloat FloatOps FloatAxioms FloatLemmas (Floats)
Relations: Relations (definitions and basic results)
Relation_Definitions Relation_Operators Relations Operators_Properties
Sets: Sets (classical, constructive, finite, infinite, powerset, etc.)
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
Classes:
Init RelationClasses Morphisms Morphisms_Prop Morphisms_Relations Equivalence CRelationClasses CMorphisms CEquivalence EquivDec SetoidTactics SetoidClass SetoidDec RelationPairs DecidableClass
Setoids:
Setoid
Lists: Polymorphic lists, Streams (infinite sequences)
List ListDec ListSet SetoidList SetoidPermutation Streams StreamMemo ListTactics
Vectors: Dependent datastructures storing their length
Fin VectorDef VectorSpec VectorEq (Vector)
Sorting: Axiomatizations of sorts
Heap Permutation Sorting PermutEq PermutSetoid Mergesort Sorted CPermutation
Wellfounded: Well-founded Relations
Disjoint_Union Inclusion Inverse_Image Lexicographic_Exponentiation Lexicographic_Product List_Extension Transitive_Closure Union Wellfounded Well_Ordering
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
Strings Implementation of string as list of ascii characters
Byte Ascii String BinaryString HexString OctalString
Reals: Formalization of real numbers
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 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
Program: Support for dependently-typed programming
Basics Wf Subset Equality Tactics Utils Syntax Program Combinators
SSReflect: Base libraries for the SSReflect proof language and the small scale reflection formalization technique
ssrmatching ssrclasses ssreflect ssrbool ssrfun
Ltac2: The Ltac2 tactic programming language
Ltac2 Array Bool Char Constant Constr Constructor Control Env Evar Float FMap FSet Fresh Ident Ind Init Int Lazy List Ltac1 Message Meta Notations Option Pattern Printf Proj Pstring RedFlags Ref Std String TransparentState Uint63 Unification
Unicode: Unicode-based notations
Utf8_core Utf8
Compat: Compatibility wrappers for previous versions of Coq
AdmitAxiom Coq818 Coq819 Coq820 Coq821 Coq818 Coq819
Array: Persistent native arrays
PArray
Primitive strings Native string type
PrimString PrimStringAxioms PString