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 Nat Peano Specif Tactics Wf (Prelude)

Logic: Classical logic, dependent equality, extensionality, choice axioms

SetIsType Classical_Pred_Type Classical_Prop (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 WeakFan WKL FinFun

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

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 Zsqrt_compat Zpow_def Zpow_alt Zpower 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 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

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 (Reals)

Program: Support for dependently-typed programming

Basics Wf Subset Equality Tactics Utils Syntax Program Combinators

Unicode: Unicode-based notations

Utf8_core Utf8

Compat: Compatibility wrappers for previous versions of Coq

AdmitAxiom Coq84 Coq85