The Coq Standard Library

# 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
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