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
Logic_Type
Byte
Nat
Decimal
Hexadecimal
Numeral
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
- 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
Le
Lt
Plus
Minus
Mult
Gt
Between
Peano_dec
Compare_dec
(Arith_base)
(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
Zpow_def
Zpow_alt
Zpower
Zdiv
Zquot
Zeuclid
(ZArith)
Zgcd_alt
Zwf
Znumtheory
Int
Zpow_facts
Zdigits
- 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
DecimalString
HexadecimalFacts
HexadecimalNat
HexadecimalPos
HexadecimalN
HexadecimalZ
HexadecimalQ
HexadecimalString
- 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 63-bits-based cyclic arithmetic
-
CyclicAxioms
NZCyclic
DoubleType
Cyclic31
Ring31
Int31
Cyclic63
Int63
Ring63
ZModulo
- Natural:
Abstract and 63-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
- 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
ZDivEucl
ZDivFloor
ZDivTrunc
ZBinary
ZNatPairs
- 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
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
ByteVector
- 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
Constr
Control
Env
Fresh
Ident
Init
Int
List
Ltac1
Message
Notations
Option
Pattern
Std
String
- Unicode:
Unicode-based notations
-
Utf8_core
Utf8
- Compat:
Compatibility wrappers for previous versions of Coq
-
AdmitAxiom
Coq810
Coq811
Coq812