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 DecidableType DecidableTypeEx Eqdep_dec EqdepFacts Eqdep JMeq ChoiceFacts RelationalChoice ClassicalChoice ClassicalDescription ClassicalEpsilon ClassicalUniqueChoice Berardi Diaconescu Hurkens ProofIrrelevance ProofIrrelevanceFacts ConstructiveEpsilon Description Epsilon IndefiniteDescription FunctionalExtensionality
- 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
- NArith: Binary positive integers
- BinPos BinNat (NArith) Pnat Nnat Ndigits Ndist Ndec
- ZArith: Binary integers
- BinInt Zorder Zcompare Znat Zmin Zmax Zminmax Zabs Zeven auxiliary ZArith_dec Zbool Zmisc Wf_Z Zhints (ZArith_base) Zcomplements Zsqrt Zpow_def Zpower Zdiv Zlogarithm (ZArith) Zgcd_alt Zwf Zbinary Znumtheory Int ZOdiv_def ZOdiv Zpow_facts
- QArith: Rational numbers
- QArith_base Qabs Qpower Qreduction Qring Qfield (QArith) Qreals Qcanon Qround
- Numbers: A modular axiomatic construction for numbers
- NumPrelude BigNumPrelude NaryFunctions
- CyclicAxioms NZCyclic DoubleAdd DoubleBase DoubleCyclic DoubleDiv DoubleDivn1 DoubleLift DoubleMul DoubleSqrt DoubleSub DoubleType Cyclic31 Int31 ZModulo
- ZAdd ZAddOrder ZAxioms ZBase ZDomain ZLt ZMul ZMulOrder BigZ ZMake ZBinary ZNatPairs ZSig ZSigZAxioms
- NZAdd NZAddOrder NZAxioms NZBase NZMul NZMulOrder NZOrder
- NAdd NAddOrder NAxioms NBase NDefOps NIso NMul NMulOrder NOrder NStrongRec NSub BigN Nbasic NMake NBinary NBinDefs NPeano NSig NSigNAxioms
- BigQ QMake QSig
- 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 Functions SetoidTactics SetoidClass SetoidDec SetoidAxioms
- Setoids:
- Setoid
- Lists: Polymorphic lists, Streams (infinite sequences)
- List ListSet MonoList SetoidList Streams StreamMemo TheoryList ListTactics
- Sorting: Axiomatizations of sorts
- Heap Permutation Sorting PermutEq PermutSetoid
- Wellfounded: Well-founded Relations
- Disjoint_Union Inclusion Inverse_Image Lexicographic_Exponentiation Lexicographic_Product Transitive_Closure Union Wellfounded Well_Ordering
- FSets: Modular implementation of finite sets/maps using lists or efficient trees
- OrderedType OrderedTypeAlt OrderedTypeEx FSetInterface FSetBridge FSetFacts FSetDecide FSetProperties FSetEqProperties FSetList FSetWeakList (FSets) FSetAVL FSetToFiniteSet FMapInterface FMapWeakList FMapList FMapPositive FMapFacts (FMaps) FMapAVL FSetFullAVL FMapFullAVL
- Reals: Formalization of real numbers
- Rdefinitions Raxioms RIneq DiscrR (Rbase) RList Ranalysis Rbasic_fun Rderiv Rfunctions Rgeom R_Ifp Rlimit Rseries Rsigma R_sqr Rtrigo_fun Rtrigo 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 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