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
ExtensionalityFacts
- 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
Compare
Div2
EqNat
Euclid
Even
Bool_nat
Factorial
Wf_nat
- PArith:
Binary positive integers
-
BinPosDef
BinPos
Pnat
POrderedType
(PArith)
- NArith:
Binary natural numbers
-
BinNatDef
BinNat
Nnat
Ndigits
Ndist
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
Zsqrt_compat
Zpow_def
Zpow_alt
Zpower
ZOdiv_def
ZOdiv
Zdiv
Zquot
Zeuclid
Zlogarithm
(ZArith)
Zgcd_alt
Zwf
Znumtheory
Int
Zpow_facts
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:
-
BinNums
NumPrelude
BigNumPrelude
NaryFunctions
- NatInt:
Abstract mixed natural/integer/cyclic arithmetic
-
NZAdd
NZAddOrder
NZAxioms
NZBase
NZMul
NZDiv
NZMulOrder
NZOrder
NZDomain
NZProperties
NZParity
NZPow
NZSqrt
NZLog
NZGcd
NZBits
- 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
NMaxMin
NParity
NPow
NSqrt
NLog
NGcd
NLcm
NBits
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
ZSgnAbs
ZMaxMin
ZParity
ZPow
ZGcd
ZLcm
ZBits
ZProperties
ZDivEucl
ZDivFloor
ZDivTrunc
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
SetoidPermutation
Streams
StreamMemo
ListTactics
- Vectors:
Dependent datastructures storing their length
-
Fin
VectorDef
VectorSpec
(Vector)
- 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
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
-
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
Rtrigo1
Rtrigo
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
LegacyRfield
(Reals)
- Program:
Support for dependently-typed programming.
-
Basics
Wf
Subset
Equality
Tactics
Utils
Syntax
Program
Combinators
- Unicode:
Unicode-based notations
-
Utf8_core
Utf8