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

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

Arith: Basic Peano arithmetic

Le Lt Plus Minus Mult Gt Between Peano_dec Compare_dec (Arith) Min Max Compare Div2 Div 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 Zpower Zdiv Zlogarithm (ZArith) Zwf Zbinary Znumtheory Int

QArith: Rational numbers

QArith_base Qreduction Qring (QArith) Qreals Qcanon

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 Rpower Rprod Rsqrt_def Rtopology Rtrigo_alt Rtrigo_calc Rtrigo_def Rtrigo_reg SeqProp SeqSeries Sqrt_reg LegacyRfield Rpow_def (Reals)

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

Relations: Relations (definitions and basic results)

Relation_Definitions Relation_Operators Relations Operators_Properties Rstar Newman

Wellfounded: Well-founded Relations

Disjoint_Union Inclusion Inverse_Image Lexicographic_Exponentiation Lexicographic_Product Transitive_Closure Union Wellfounded Well_Ordering

Setoids:

Setoid

Bool: Booleans (basic functions and results)

Bool BoolEq DecBool IfProp Sumbool Zerob Bvector

Lists: Polymorphic lists, Streams (infinite sequences)

List ListSet MonoList SetoidList Streams TheoryList ListTactics

FSets: Modular implementation of finite sets/maps using lists

OrderedType OrderedTypeAlt OrderedTypeEx FSetInterface FSetBridge FSetProperties FSetEqProperties FSetList (FSets) FSetFacts FSetAVL FSetToFiniteSet FSetWeakProperties FSetWeakInterface FSetWeakFacts FSetWeakList FSetWeak FMapInterface FMapList FMapPositive FMapIntMap FMapFacts (FMaps) FMapAVL FMapWeakInterface FMapWeakList FMapWeak FMapWeakFacts

IntMap: An implementation of finite sets/maps as trees indexed by addresses

Adalloc Map Fset Mapaxioms Mapiter Mapcanon Mapsubset Lsort Mapfold Mapcard Mapc Maplists Allmaps

Strings Implementation of string as list of ascii characters

Ascii String

Sorting: Axiomatizations of sorts

Heap Permutation Sorting PermutEq PermutSetoid