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 Byte Nat Decimal 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 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 DecimalString
- 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
- 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
- Rdefinitions ConstructiveReals ConstructiveRealsMorphisms ConstructiveCauchyReals ConstructiveCauchyRealsMult ClassicalDedekindReals Raxioms ConstructiveRealsLUB 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 ConstructiveRcomplete 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
- 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 Coq89 Coq810 Coq811