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 DecidableType DecidableTypeEx Eqdep_dec EqdepFacts Eqdep JMeq ChoiceFacts RelationalChoice ClassicalChoice ClassicalDescription ClassicalEpsilon ClassicalUniqueChoice Berardi Diaconescu Hurkens ProofIrrelevance ProofIrrelevanceFacts ConstructiveEpsilon Description Epsilon IndefiniteDescription FunctionalExtensionality
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 Compare Div2 EqNat Euclid Even Bool_nat Factorial Wf_nat
NArith: Binary positive integers
BinPos BinNat (NArith) Pnat Nnat Ndigits Ndist Ndec
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 Zbinary Znumtheory Int ZOdiv_def ZOdiv Zpow_facts
QArith: Rational numbers
QArith_base Qabs Qpower Qreduction Qring Qfield (QArith) Qreals Qcanon Qround
Numbers: A modular axiomatic construction for numbers
NumPrelude BigNumPrelude NaryFunctions
CyclicAxioms NZCyclic DoubleAdd DoubleBase DoubleCyclic DoubleDiv DoubleDivn1 DoubleLift DoubleMul DoubleSqrt DoubleSub DoubleType Cyclic31 Int31 ZModulo
ZAdd ZAddOrder ZAxioms ZBase ZDomain ZLt ZMul ZMulOrder BigZ ZMake ZBinary ZNatPairs ZSig ZSigZAxioms
NZAdd NZAddOrder NZAxioms NZBase NZMul NZMulOrder NZOrder
NAdd NAddOrder NAxioms NBase NDefOps NIso NMul NMulOrder NOrder NStrongRec NSub BigN Nbasic NMake NBinary NBinDefs NPeano NSig NSigNAxioms
BigQ QMake QSig
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 Functions SetoidTactics SetoidClass SetoidDec SetoidAxioms
Setoids:
Setoid theories/Setoids/Setoid_tac.v theories/Setoids/Setoid_Prop.v
Lists: Polymorphic lists, Streams (infinite sequences)
List ListSet MonoList SetoidList Streams StreamMemo TheoryList ListTactics
Sorting: Axiomatizations of sorts
Heap Permutation Sorting PermutEq PermutSetoid
Wellfounded: Well-founded Relations
Disjoint_Union Inclusion Inverse_Image Lexicographic_Exponentiation Lexicographic_Product Transitive_Closure Union Wellfounded Well_Ordering
FSets: Modular implementation of finite sets/maps using lists or efficient trees
OrderedType OrderedTypeAlt OrderedTypeEx FSetInterface FSetBridge FSetFacts FSetDecide FSetProperties FSetEqProperties FSetList FSetWeakList (FSets) FSetAVL FSetToFiniteSet FMapInterface FMapWeakList FMapList FMapPositive FMapFacts (FMaps) FMapAVL FSetFullAVL FMapFullAVL
Reals: Formalization of real numbers
Rdefinitions Raxioms RIneq DiscrR (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
Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (13562 entries)
Instance Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (96 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (210 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (71 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (6947 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (306 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (351 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (182 entries)
Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (295 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (2870 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (286 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (433 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (1189 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (326 entries)