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)

theories/Init/Notations.v theories/Init/Datatypes.v theories/Init/Logic.v theories/Init/Logic_Type.v theories/Init/Nat.v theories/Init/Peano.v theories/Init/Specif.v theories/Init/Tactics.v theories/Init/Wf.v (theories/Init/Prelude.v)

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

theories/Logic/SetIsType.v theories/Logic/Classical_Pred_Type.v theories/Logic/Classical_Prop.v (theories/Logic/Classical.v) theories/Logic/ClassicalFacts.v theories/Logic/Decidable.v theories/Logic/Eqdep_dec.v theories/Logic/EqdepFacts.v theories/Logic/Eqdep.v theories/Logic/JMeq.v theories/Logic/ChoiceFacts.v theories/Logic/RelationalChoice.v theories/Logic/ClassicalChoice.v theories/Logic/ClassicalDescription.v theories/Logic/ClassicalEpsilon.v theories/Logic/ClassicalUniqueChoice.v theories/Logic/Berardi.v theories/Logic/Diaconescu.v theories/Logic/Hurkens.v theories/Logic/ProofIrrelevance.v theories/Logic/ProofIrrelevanceFacts.v theories/Logic/ConstructiveEpsilon.v theories/Logic/Description.v theories/Logic/Epsilon.v theories/Logic/IndefiniteDescription.v theories/Logic/FunctionalExtensionality.v theories/Logic/ExtensionalityFacts.v theories/Logic/WeakFan.v theories/Logic/WKL.v theories/Logic/FinFun.v

Structures: Algebraic structures (types with equality, with order, ...). DecidableType* and OrderedType* are there only for compatibility.

theories/Structures/Equalities.v theories/Structures/EqualitiesFacts.v theories/Structures/Orders.v theories/Structures/OrdersTac.v theories/Structures/OrdersAlt.v theories/Structures/OrdersEx.v theories/Structures/OrdersFacts.v theories/Structures/OrdersLists.v theories/Structures/GenericMinMax.v theories/Structures/DecidableType.v theories/Structures/DecidableTypeEx.v theories/Structures/OrderedType.v theories/Structures/OrderedTypeAlt.v theories/Structures/OrderedTypeEx.v

Bool: Booleans (basic functions and results)

theories/Bool/Bool.v theories/Bool/BoolEq.v theories/Bool/DecBool.v theories/Bool/IfProp.v theories/Bool/Sumbool.v theories/Bool/Zerob.v theories/Bool/Bvector.v

Arith: Basic Peano arithmetic

theories/Arith/PeanoNat.v theories/Arith/Le.v theories/Arith/Lt.v theories/Arith/Plus.v theories/Arith/Minus.v theories/Arith/Mult.v theories/Arith/Gt.v theories/Arith/Between.v theories/Arith/Peano_dec.v theories/Arith/Compare_dec.v (theories/Arith/Arith_base.v) (theories/Arith/Arith.v) theories/Arith/Min.v theories/Arith/Max.v theories/Arith/Compare.v theories/Arith/Div2.v theories/Arith/EqNat.v theories/Arith/Euclid.v theories/Arith/Even.v theories/Arith/Bool_nat.v theories/Arith/Factorial.v theories/Arith/Wf_nat.v

PArith: Binary positive integers

theories/PArith/BinPosDef.v theories/PArith/BinPos.v theories/PArith/Pnat.v theories/PArith/POrderedType.v (theories/PArith/PArith.v)

NArith: Binary natural numbers

theories/NArith/BinNatDef.v theories/NArith/BinNat.v theories/NArith/Nnat.v theories/NArith/Ndigits.v theories/NArith/Ndist.v theories/NArith/Ndec.v theories/NArith/Ndiv_def.v theories/NArith/Ngcd_def.v theories/NArith/Nsqrt_def.v (theories/NArith/NArith.v)

ZArith: Binary integers

theories/ZArith/BinIntDef.v theories/ZArith/BinInt.v theories/ZArith/Zorder.v theories/ZArith/Zcompare.v theories/ZArith/Znat.v theories/ZArith/Zmin.v theories/ZArith/Zmax.v theories/ZArith/Zminmax.v theories/ZArith/Zabs.v theories/ZArith/Zeven.v theories/ZArith/auxiliary.v theories/ZArith/ZArith_dec.v theories/ZArith/Zbool.v theories/ZArith/Zmisc.v theories/ZArith/Wf_Z.v theories/ZArith/Zhints.v (theories/ZArith/ZArith_base.v) theories/ZArith/Zcomplements.v theories/ZArith/Zsqrt_compat.v theories/ZArith/Zpow_def.v theories/ZArith/Zpow_alt.v theories/ZArith/Zpower.v theories/ZArith/Zdiv.v theories/ZArith/Zquot.v theories/ZArith/Zeuclid.v theories/ZArith/Zlogarithm.v (theories/ZArith/ZArith.v) theories/ZArith/Zgcd_alt.v theories/ZArith/Zwf.v theories/ZArith/Znumtheory.v theories/ZArith/Int.v theories/ZArith/Zpow_facts.v theories/ZArith/Zdigits.v

QArith: Rational numbers

theories/QArith/QArith_base.v theories/QArith/Qabs.v theories/QArith/Qpower.v theories/QArith/Qreduction.v theories/QArith/Qring.v theories/QArith/Qfield.v (theories/QArith/QArith.v) theories/QArith/Qreals.v theories/QArith/Qcanon.v theories/QArith/Qround.v theories/QArith/QOrderedType.v theories/QArith/Qminmax.v

Numbers: An experimental modular architecture for arithmetic

  Prelude:

theories/Numbers/BinNums.v theories/Numbers/NumPrelude.v theories/Numbers/BigNumPrelude.v theories/Numbers/NaryFunctions.v

  NatInt: Abstract mixed natural/integer/cyclic arithmetic

theories/Numbers/NatInt/NZAdd.v theories/Numbers/NatInt/NZAddOrder.v theories/Numbers/NatInt/NZAxioms.v theories/Numbers/NatInt/NZBase.v theories/Numbers/NatInt/NZMul.v theories/Numbers/NatInt/NZDiv.v theories/Numbers/NatInt/NZMulOrder.v theories/Numbers/NatInt/NZOrder.v theories/Numbers/NatInt/NZDomain.v theories/Numbers/NatInt/NZProperties.v theories/Numbers/NatInt/NZParity.v theories/Numbers/NatInt/NZPow.v theories/Numbers/NatInt/NZSqrt.v theories/Numbers/NatInt/NZLog.v theories/Numbers/NatInt/NZGcd.v theories/Numbers/NatInt/NZBits.v

  Cyclic: Abstract and 31-bits-based cyclic arithmetic

theories/Numbers/Cyclic/Abstract/CyclicAxioms.v theories/Numbers/Cyclic/Abstract/NZCyclic.v theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v theories/Numbers/Cyclic/Int31/Cyclic31.v theories/Numbers/Cyclic/Int31/Ring31.v theories/Numbers/Cyclic/Int31/Int31.v theories/Numbers/Cyclic/ZModulo/ZModulo.v

  Natural: Abstract and 31-bits-words-based natural arithmetic

theories/Numbers/Natural/Abstract/NAdd.v theories/Numbers/Natural/Abstract/NAddOrder.v theories/Numbers/Natural/Abstract/NAxioms.v theories/Numbers/Natural/Abstract/NBase.v theories/Numbers/Natural/Abstract/NDefOps.v theories/Numbers/Natural/Abstract/NIso.v theories/Numbers/Natural/Abstract/NMulOrder.v theories/Numbers/Natural/Abstract/NOrder.v theories/Numbers/Natural/Abstract/NStrongRec.v theories/Numbers/Natural/Abstract/NSub.v theories/Numbers/Natural/Abstract/NDiv.v theories/Numbers/Natural/Abstract/NMaxMin.v theories/Numbers/Natural/Abstract/NParity.v theories/Numbers/Natural/Abstract/NPow.v theories/Numbers/Natural/Abstract/NSqrt.v theories/Numbers/Natural/Abstract/NLog.v theories/Numbers/Natural/Abstract/NGcd.v theories/Numbers/Natural/Abstract/NLcm.v theories/Numbers/Natural/Abstract/NBits.v theories/Numbers/Natural/Abstract/NProperties.v theories/Numbers/Natural/Binary/NBinary.v theories/Numbers/Natural/Peano/NPeano.v theories/Numbers/Natural/SpecViaZ/NSig.v theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v theories/Numbers/Natural/BigN/BigN.v theories/Numbers/Natural/BigN/Nbasic.v theories/Numbers/Natural/BigN/NMake.v theories/Numbers/Natural/BigN/NMake_gen.v

  Integer: Abstract and concrete (especially 31-bits-words-based) integer arithmetic

theories/Numbers/Integer/Abstract/ZAdd.v theories/Numbers/Integer/Abstract/ZAddOrder.v theories/Numbers/Integer/Abstract/ZAxioms.v theories/Numbers/Integer/Abstract/ZBase.v theories/Numbers/Integer/Abstract/ZLt.v theories/Numbers/Integer/Abstract/ZMul.v theories/Numbers/Integer/Abstract/ZMulOrder.v theories/Numbers/Integer/Abstract/ZSgnAbs.v theories/Numbers/Integer/Abstract/ZMaxMin.v theories/Numbers/Integer/Abstract/ZParity.v theories/Numbers/Integer/Abstract/ZPow.v theories/Numbers/Integer/Abstract/ZGcd.v theories/Numbers/Integer/Abstract/ZLcm.v theories/Numbers/Integer/Abstract/ZBits.v theories/Numbers/Integer/Abstract/ZProperties.v theories/Numbers/Integer/Abstract/ZDivEucl.v theories/Numbers/Integer/Abstract/ZDivFloor.v theories/Numbers/Integer/Abstract/ZDivTrunc.v theories/Numbers/Integer/Binary/ZBinary.v theories/Numbers/Integer/NatPairs/ZNatPairs.v theories/Numbers/Integer/SpecViaZ/ZSig.v theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v theories/Numbers/Integer/BigZ/BigZ.v theories/Numbers/Integer/BigZ/ZMake.v

  Rational: Abstract and 31-bits-words-based rational arithmetic

theories/Numbers/Rational/SpecViaQ/QSig.v theories/Numbers/Rational/BigQ/BigQ.v theories/Numbers/Rational/BigQ/QMake.v

Relations: Relations (definitions and basic results)

theories/Relations/Relation_Definitions.v theories/Relations/Relation_Operators.v theories/Relations/Relations.v theories/Relations/Operators_Properties.v

Sets: Sets (classical, constructive, finite, infinite, powerset, etc.)

theories/Sets/Classical_sets.v theories/Sets/Constructive_sets.v theories/Sets/Cpo.v theories/Sets/Ensembles.v theories/Sets/Finite_sets_facts.v theories/Sets/Finite_sets.v theories/Sets/Image.v theories/Sets/Infinite_sets.v theories/Sets/Integers.v theories/Sets/Multiset.v theories/Sets/Partial_Order.v theories/Sets/Permut.v theories/Sets/Powerset_Classical_facts.v theories/Sets/Powerset_facts.v theories/Sets/Powerset.v theories/Sets/Relations_1_facts.v theories/Sets/Relations_1.v theories/Sets/Relations_2_facts.v theories/Sets/Relations_2.v theories/Sets/Relations_3_facts.v theories/Sets/Relations_3.v theories/Sets/Uniset.v

Classes:

theories/Classes/Init.v theories/Classes/RelationClasses.v theories/Classes/Morphisms.v theories/Classes/Morphisms_Prop.v theories/Classes/Morphisms_Relations.v theories/Classes/Equivalence.v theories/Classes/CRelationClasses.v theories/Classes/CMorphisms.v theories/Classes/CEquivalence.v theories/Classes/EquivDec.v theories/Classes/SetoidTactics.v theories/Classes/SetoidClass.v theories/Classes/SetoidDec.v theories/Classes/RelationPairs.v theories/Classes/DecidableClass.v

Setoids:

theories/Setoids/Setoid.v

Lists: Polymorphic lists, Streams (infinite sequences)

theories/Lists/List.v theories/Lists/ListDec.v theories/Lists/ListSet.v theories/Lists/SetoidList.v theories/Lists/SetoidPermutation.v theories/Lists/Streams.v theories/Lists/StreamMemo.v theories/Lists/ListTactics.v

Vectors: Dependent datastructures storing their length

theories/Vectors/Fin.v theories/Vectors/VectorDef.v theories/Vectors/VectorSpec.v theories/Vectors/VectorEq.v (theories/Vectors/Vector.v)

Sorting: Axiomatizations of sorts

theories/Sorting/Heap.v theories/Sorting/Permutation.v theories/Sorting/Sorting.v theories/Sorting/PermutEq.v theories/Sorting/PermutSetoid.v theories/Sorting/Mergesort.v theories/Sorting/Sorted.v

Wellfounded: Well-founded Relations

theories/Wellfounded/Disjoint_Union.v theories/Wellfounded/Inclusion.v theories/Wellfounded/Inverse_Image.v theories/Wellfounded/Lexicographic_Exponentiation.v theories/Wellfounded/Lexicographic_Product.v theories/Wellfounded/Transitive_Closure.v theories/Wellfounded/Union.v theories/Wellfounded/Wellfounded.v theories/Wellfounded/Well_Ordering.v

MSets: Modular implementation of finite sets using lists or efficient trees. This is a modernization of FSets.

theories/MSets/MSetInterface.v theories/MSets/MSetFacts.v theories/MSets/MSetDecide.v theories/MSets/MSetProperties.v theories/MSets/MSetEqProperties.v theories/MSets/MSetWeakList.v theories/MSets/MSetList.v theories/MSets/MSetGenTree.v theories/MSets/MSetAVL.v theories/MSets/MSetRBT.v theories/MSets/MSetPositive.v theories/MSets/MSetToFiniteSet.v (theories/MSets/MSets.v)

FSets: Modular implementation of finite sets/maps using lists or efficient trees. For sets, please consider the more modern MSets.

theories/FSets/FSetInterface.v theories/FSets/FSetBridge.v theories/FSets/FSetFacts.v theories/FSets/FSetDecide.v theories/FSets/FSetProperties.v theories/FSets/FSetEqProperties.v theories/FSets/FSetList.v theories/FSets/FSetWeakList.v theories/FSets/FSetCompat.v theories/FSets/FSetAVL.v theories/FSets/FSetPositive.v (theories/FSets/FSets.v) theories/FSets/FSetToFiniteSet.v theories/FSets/FMapInterface.v theories/FSets/FMapWeakList.v theories/FSets/FMapList.v theories/FSets/FMapPositive.v theories/FSets/FMapFacts.v (theories/FSets/FMaps.v) theories/FSets/FMapAVL.v theories/FSets/FMapFullAVL.v

Strings Implementation of string as list of ascii characters

theories/Strings/Ascii.v theories/Strings/String.v

Reals: Formalization of real numbers

theories/Reals/Rdefinitions.v theories/Reals/Raxioms.v theories/Reals/RIneq.v theories/Reals/DiscrR.v theories/Reals/ROrderedType.v theories/Reals/Rminmax.v (theories/Reals/Rbase.v) theories/Reals/RList.v theories/Reals/Ranalysis.v theories/Reals/Rbasic_fun.v theories/Reals/Rderiv.v theories/Reals/Rfunctions.v theories/Reals/Rgeom.v theories/Reals/R_Ifp.v theories/Reals/Rlimit.v theories/Reals/Rseries.v theories/Reals/Rsigma.v theories/Reals/R_sqr.v theories/Reals/Rtrigo_fun.v theories/Reals/Rtrigo1.v theories/Reals/Rtrigo.v theories/Reals/Ratan.v theories/Reals/Machin.v theories/Reals/SplitAbsolu.v theories/Reals/SplitRmult.v theories/Reals/Alembert.v theories/Reals/AltSeries.v theories/Reals/ArithProp.v theories/Reals/Binomial.v theories/Reals/Cauchy_prod.v theories/Reals/Cos_plus.v theories/Reals/Cos_rel.v theories/Reals/Exp_prop.v theories/Reals/Integration.v theories/Reals/MVT.v theories/Reals/NewtonInt.v theories/Reals/PSeries_reg.v theories/Reals/PartSum.v theories/Reals/R_sqrt.v theories/Reals/Ranalysis1.v theories/Reals/Ranalysis2.v theories/Reals/Ranalysis3.v theories/Reals/Ranalysis4.v theories/Reals/Ranalysis5.v theories/Reals/Ranalysis_reg.v theories/Reals/Rcomplete.v theories/Reals/RiemannInt.v theories/Reals/RiemannInt_SF.v theories/Reals/Rpow_def.v theories/Reals/Rpower.v theories/Reals/Rprod.v theories/Reals/Rsqrt_def.v theories/Reals/Rtopology.v theories/Reals/Rtrigo_alt.v theories/Reals/Rtrigo_calc.v theories/Reals/Rtrigo_def.v theories/Reals/Rtrigo_reg.v theories/Reals/SeqProp.v theories/Reals/SeqSeries.v theories/Reals/Sqrt_reg.v theories/Reals/Rlogic.v (theories/Reals/Reals.v)

Program: Support for dependently-typed programming.

theories/Program/Basics.v theories/Program/Wf.v theories/Program/Subset.v theories/Program/Equality.v theories/Program/Tactics.v theories/Program/Utils.v theories/Program/Syntax.v theories/Program/Program.v theories/Program/Combinators.v

Unicode: Unicode-based notations

theories/Unicode/Utf8_core.v theories/Unicode/Utf8.v