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)
Notations Datatypes Logic Logic_Type Peano Specif Tactics Wf (Prelude)
Logic: Classical logic and dependent equality
SetIsType Classical_Pred_Set Classical_Pred_Type Classical_Prop Classical_Type (Classical) ClassicalFacts Decidable Eqdep_dec EqdepFacts Eqdep JMeq ChoiceFacts RelationalChoice ClassicalChoice ClassicalDescription ClassicalEpsilon ClassicalUniqueChoice Berardi Diaconescu Hurkens ProofIrrelevance ProofIrrelevanceFacts ConstructiveEpsilon Description Epsilon IndefiniteDescription FunctionalExtensionality
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 DecBool IfProp Sumbool Zerob Bvector
Arith: Basic Peano arithmetic
Arith_base Le Lt Plus Minus Mult Gt Between Peano_dec Compare_dec (Arith) Min Max MinMax Compare Div2 EqNat Euclid Even Bool_nat Factorial Wf_nat NatOrderedType
NArith: Binary positive integers
BinPos BinNat (NArith) Pnat Nnat Ndigits Ndist Ndec NOrderedType Nminmax POrderedType Pminmax
ZArith: Binary integers
BinInt Zorder Zcompare Znat Zmin Zmax Zminmax Zabs Zeven auxiliary ZArith_dec Zbool Zmisc Wf_Z Zhints (ZArith_base) Zcomplements Zsqrt Zpow_def Zpower Zdiv Zlogarithm (ZArith) Zgcd_alt Zwf Znumtheory Int ZOdiv_def ZOdiv Zpow_facts ZOrderedType Zdigits
QArith: Rational numbers
QArith_base Qabs Qpower Qreduction Qring Qfield (QArith) Qreals Qcanon Qround QOrderedType Qminmax
Numbers: An experimental modular architecture for arithmetic
  Prelude:
NumPrelude BigNumPrelude NaryFunctions
  NatInt: Abstract mixed natural/integer/cyclic arithmetic
NZAdd NZAddOrder NZAxioms NZBase NZMul NZDiv NZMulOrder NZOrder NZDomain NZProperties
  Cyclic: Abstract and 31-bits-based cyclic arithmetic
CyclicAxioms NZCyclic DoubleAdd DoubleBase DoubleCyclic DoubleDiv DoubleDivn1 DoubleLift DoubleMul DoubleSqrt DoubleSub DoubleType Cyclic31 Ring31 Int31 ZModulo
  Natural: Abstract and 31-bits-words-based natural arithmetic
NAdd NAddOrder NAxioms NBase NDefOps NIso NMulOrder NOrder NStrongRec NSub NDiv NProperties NBinary NPeano NSig NSigNAxioms BigN Nbasic NMake NMake_gen
  Integer: Abstract and concrete (especially 31-bits-words-based) integer arithmetic
ZAdd ZAddOrder ZAxioms ZBase ZLt ZMul ZMulOrder ZDivEucl ZDivFloor ZDivTrunc ZProperties ZSgnAbs ZBinary ZNatPairs ZSig ZSigZAxioms BigZ ZMake
  Rational: Abstract and 31-bits-words-based rational arithmetic
QSig BigQ QMake
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 EquivDec SetoidTactics SetoidClass SetoidDec RelationPairs
Setoids:
Setoid
Lists: Polymorphic lists, Streams (infinite sequences)
List ListSet SetoidList Streams StreamMemo TheoryList ListTactics
Sorting: Axiomatizations of sorts
Heap Permutation Sorting PermutEq PermutSetoid Mergesort Sorted
Wellfounded: Well-founded Relations
Disjoint_Union Inclusion Inverse_Image Lexicographic_Exponentiation Lexicographic_Product 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 MSetAVL 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
Ascii String
Reals: Formalization of real numbers
Rdefinitions Raxioms RIneq DiscrR ROrderedType Rminmax (Rbase) RList Ranalysis Rbasic_fun Rderiv Rfunctions Rgeom R_Ifp Rlimit Rseries Rsigma R_sqr Rtrigo_fun Rtrigo 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 Rcomplete RiemannInt RiemannInt_SF Rpow_def Rpower Rprod Rsqrt_def Rtopology Rtrigo_alt Rtrigo_calc Rtrigo_def Rtrigo_reg SeqProp SeqSeries Sqrt_reg Rlogic LegacyRfield (Reals)
Program: Support for dependently-typed programming.
Basics Wf Subset Equality Tactics Utils Syntax Program Combinators