The Coq Standard Library

The standard library is composed of the following subdirectories:

Init: The core library

Datatypes Logic_Type Logic Notations Peano Prelude Specif Wf

Logic: Classical logic and dependent equality

Berardi ChoiceFacts ClassicalChoice ClassicalDescription ClassicalFacts Classical_Pred_Set Classical_Pred_Type Classical_Prop Classical_Type Classical Decidable Diaconescu Eqdep_dec Eqdep Hurkens JMeq ProofIrrelevance RelationalChoice

Arith: Basic Peano arithmetic

Arith Between Bool_nat Compare_dec Compare Div2 Div EqNat Euclid Even Factorial Gt Le Lt Max Minus Min Mult Peano_dec Plus Wf_nat

NArith: Binary positive integers

BinNat BinPos NArith Pnat

ZArith: Binary integers

auxiliary BinInt Wf_Z Zabs ZArith_base ZArith_dec ZArith Zbinary Zbool Zcompare Zcomplements Zdiv Zeven Zhints Zlogarithm Zmin Zmisc Znat Znumtheory Zorder Zpower Zsqrt Zwf

Reals: Formalization of real numbers

Alembert AltSeries ArithProp Binomial Cauchy_prod Cos_plus Cos_rel DiscrR Exp_prop Integration MVT NewtonInt PartSum PSeries_reg Ranalysis1 Ranalysis2 Ranalysis3 Ranalysis4 Ranalysis Raxioms Rbase Rbasic_fun Rcomplete Rdefinitions Rderiv Reals Rfunctions Rgeom RiemannInt_SF RiemannInt R_Ifp RIneq Rlimit RList Rpower Rprod Rseries Rsigma Rsqrt_def R_sqrt R_sqr Rtopology Rtrigo_alt Rtrigo_calc Rtrigo_def Rtrigo_fun Rtrigo_reg Rtrigo SeqProp SeqSeries SplitAbsolu SplitRmult Sqrt_reg

Bool: Booleans (basic functions and results)

BoolEq Bool Bvector DecBool IfProp Sumbool Zerob

Lists : Monomorphic and polymorphic lists, Streams (infinite sequences)

ListSet List MonoList Streams TheoryList

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)

Newman Operators_Properties Relation_Definitions Relation_Operators Relations Rstar

Wellfounded: Well-founded Relations

Disjoint_Union Inclusion Inverse_Image Lexicographic_Exponentiation Lexicographic_Product Transitive_Closure Union Wellfounded Well_Ordering

Sorting: Axiomatizations of sorts

Heap Permutation Sorting

Setoids:

Setoid

IntMap: Finite sets/maps as trees indexed by addresses

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