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)
-
theories/Init/Notations.v
theories/Init/Datatypes.v
theories/Init/Logic.v
theories/Init/Logic_Type.v
theories/Init/Peano.v
theories/Init/Specif.v
theories/Init/Tactics.v
theories/Init/Wf.v
(theories/Init/Prelude.v)
- Logic:
Classical logic and dependent equality
-
theories/Logic/Classical_Pred_Set.v
theories/Logic/Classical_Pred_Type.v
theories/Logic/Classical_Prop.v
theories/Logic/Classical_Type.v
(theories/Logic/Classical.v)
theories/Logic/ClassicalFacts.v
theories/Logic/Decidable.v
theories/Logic/DecidableType.v
theories/Logic/DecidableTypeEx.v
theories/Logic/Eqdep_dec.v
theories/Logic/EqdepFacts.v
theories/Logic/Eqdep.v
theories/Logic/JMeq.v
theories/Logic/ChoiceFacts.v
theories/Logic/RelationalChoice.v
theories/Logic/ClassicalChoice.v
theories/Logic/ClassicalDescription.v
theories/Logic/ClassicalEpsilon.v
theories/Logic/ClassicalUniqueChoice.v
theories/Logic/Berardi.v
theories/Logic/Diaconescu.v
theories/Logic/Hurkens.v
theories/Logic/ProofIrrelevance.v
theories/Logic/ProofIrrelevanceFacts.v
theories/Logic/ConstructiveEpsilon.v
- Arith:
Basic Peano arithmetic
-
theories/Arith/Le.v
theories/Arith/Lt.v
theories/Arith/Plus.v
theories/Arith/Minus.v
theories/Arith/Mult.v
theories/Arith/Gt.v
theories/Arith/Between.v
theories/Arith/Peano_dec.v
theories/Arith/Compare_dec.v
(theories/Arith/Arith.v)
theories/Arith/Min.v
theories/Arith/Max.v
theories/Arith/Compare.v
theories/Arith/Div2.v
theories/Arith/Div.v
theories/Arith/EqNat.v
theories/Arith/Euclid.v
theories/Arith/Even.v
theories/Arith/Bool_nat.v
theories/Arith/Factorial.v
theories/Arith/Wf_nat.v
- NArith:
Binary positive integers
-
theories/NArith/BinPos.v
theories/NArith/BinNat.v
(theories/NArith/NArith.v)
theories/NArith/Pnat.v
theories/NArith/Nnat.v
theories/NArith/Ndigits.v
theories/NArith/Ndist.v
theories/NArith/Ndec.v
.
- ZArith:
Binary integers
-
theories/ZArith/BinInt.v
theories/ZArith/Zorder.v
theories/ZArith/Zcompare.v
theories/ZArith/Znat.v
theories/ZArith/Zmin.v
theories/ZArith/Zmax.v
theories/ZArith/Zminmax.v
theories/ZArith/Zabs.v
theories/ZArith/Zeven.v
theories/ZArith/auxiliary.v
theories/ZArith/ZArith_dec.v
theories/ZArith/Zbool.v
theories/ZArith/Zmisc.v
theories/ZArith/Wf_Z.v
theories/ZArith/Zhints.v
(theories/ZArith/ZArith_base.v)
theories/ZArith/Zcomplements.v
theories/ZArith/Zsqrt.v
theories/ZArith/Zpower.v
theories/ZArith/Zdiv.v
theories/ZArith/Zlogarithm.v
(theories/ZArith/ZArith.v)
theories/ZArith/Zwf.v
theories/ZArith/Zbinary.v
theories/ZArith/Znumtheory.v
theories/ZArith/Int.v
- QArith:
Rational numbers
-
theories/QArith/QArith_base.v
theories/QArith/Qreduction.v
theories/QArith/Qring.v
(theories/QArith/QArith.v)
theories/QArith/Qreals.v
theories/QArith/Qcanon.v
- Reals:
Formalization of real numbers
-
theories/Reals/Rdefinitions.v
theories/Reals/Raxioms.v
theories/Reals/RIneq.v
theories/Reals/DiscrR.v
(theories/Reals/Rbase.v)
theories/Reals/RList.v
theories/Reals/Ranalysis.v
theories/Reals/Rbasic_fun.v
theories/Reals/Rderiv.v
theories/Reals/Rfunctions.v
theories/Reals/Rgeom.v
theories/Reals/R_Ifp.v
theories/Reals/Rlimit.v
theories/Reals/Rseries.v
theories/Reals/Rsigma.v
theories/Reals/R_sqr.v
theories/Reals/Rtrigo_fun.v
theories/Reals/Rtrigo.v
theories/Reals/SplitAbsolu.v
theories/Reals/SplitRmult.v
theories/Reals/Alembert.v
theories/Reals/AltSeries.v
theories/Reals/ArithProp.v
theories/Reals/Binomial.v
theories/Reals/Cauchy_prod.v
theories/Reals/Cos_plus.v
theories/Reals/Cos_rel.v
theories/Reals/Exp_prop.v
theories/Reals/Integration.v
theories/Reals/MVT.v
theories/Reals/NewtonInt.v
theories/Reals/PSeries_reg.v
theories/Reals/PartSum.v
theories/Reals/R_sqrt.v
theories/Reals/Ranalysis1.v
theories/Reals/Ranalysis2.v
theories/Reals/Ranalysis3.v
theories/Reals/Ranalysis4.v
theories/Reals/Rcomplete.v
theories/Reals/RiemannInt.v
theories/Reals/RiemannInt_SF.v
theories/Reals/Rpower.v
theories/Reals/Rprod.v
theories/Reals/Rsqrt_def.v
theories/Reals/Rtopology.v
theories/Reals/Rtrigo_alt.v
theories/Reals/Rtrigo_calc.v
theories/Reals/Rtrigo_def.v
theories/Reals/Rtrigo_reg.v
theories/Reals/SeqProp.v
theories/Reals/SeqSeries.v
theories/Reals/Sqrt_reg.v
theories/Reals/LegacyRfield.v
theories/Reals/Rpow_def.v
(theories/Reals/Reals.v)
- Sets:
Sets (classical, constructive, finite, infinite, powerset, etc.)
-
theories/Sets/Classical_sets.v
theories/Sets/Constructive_sets.v
theories/Sets/Cpo.v
theories/Sets/Ensembles.v
theories/Sets/Finite_sets_facts.v
theories/Sets/Finite_sets.v
theories/Sets/Image.v
theories/Sets/Infinite_sets.v
theories/Sets/Integers.v
theories/Sets/Multiset.v
theories/Sets/Partial_Order.v
theories/Sets/Permut.v
theories/Sets/Powerset_Classical_facts.v
theories/Sets/Powerset_facts.v
theories/Sets/Powerset.v
theories/Sets/Relations_1_facts.v
theories/Sets/Relations_1.v
theories/Sets/Relations_2_facts.v
theories/Sets/Relations_2.v
theories/Sets/Relations_3_facts.v
theories/Sets/Relations_3.v
theories/Sets/Uniset.v
- Relations:
Relations (definitions and basic results)
-
theories/Relations/Relation_Definitions.v
theories/Relations/Relation_Operators.v
theories/Relations/Relations.v
theories/Relations/Operators_Properties.v
theories/Relations/Rstar.v
theories/Relations/Newman.v
- Wellfounded:
Well-founded Relations
-
theories/Wellfounded/Disjoint_Union.v
theories/Wellfounded/Inclusion.v
theories/Wellfounded/Inverse_Image.v
theories/Wellfounded/Lexicographic_Exponentiation.v
theories/Wellfounded/Lexicographic_Product.v
theories/Wellfounded/Transitive_Closure.v
theories/Wellfounded/Union.v
theories/Wellfounded/Wellfounded.v
theories/Wellfounded/Well_Ordering.v
- Setoids:
-
theories/Setoids/Setoid.v
- Bool:
Booleans (basic functions and results)
-
theories/Bool/Bool.v
theories/Bool/BoolEq.v
theories/Bool/DecBool.v
theories/Bool/IfProp.v
theories/Bool/Sumbool.v
theories/Bool/Zerob.v
theories/Bool/Bvector.v
- Lists:
Polymorphic lists, Streams (infinite sequences)
-
theories/Lists/List.v
theories/Lists/ListSet.v
theories/Lists/MonoList.v
theories/Lists/SetoidList.v
theories/Lists/Streams.v
theories/Lists/TheoryList.v
theories/Lists/ListTactics.v
- FSets:
Modular implementation of finite sets/maps using lists
-
theories/FSets/OrderedType.v
theories/FSets/OrderedTypeAlt.v
theories/FSets/OrderedTypeEx.v
theories/FSets/FSetInterface.v
theories/FSets/FSetBridge.v
theories/FSets/FSetProperties.v
theories/FSets/FSetEqProperties.v
theories/FSets/FSetList.v
(theories/FSets/FSets.v)
theories/FSets/FSetFacts.v
theories/FSets/FSetAVL.v
theories/FSets/FSetToFiniteSet.v
theories/FSets/FSetWeakProperties.v
theories/FSets/FSetWeakInterface.v
theories/FSets/FSetWeakFacts.v
theories/FSets/FSetWeakList.v
theories/FSets/FSetWeak.v
theories/FSets/FMapInterface.v
theories/FSets/FMapList.v
theories/FSets/FMapPositive.v
theories/FSets/FMapIntMap.v
theories/FSets/FMapFacts.v
(theories/FSets/FMaps.v)
theories/FSets/FMapAVL.v
theories/FSets/FMapWeakInterface.v
theories/FSets/FMapWeakList.v
theories/FSets/FMapWeak.v
theories/FSets/FMapWeakFacts.v
- IntMap:
An implementation of finite sets/maps as trees indexed by addresses
-
theories/IntMap/Adalloc.v
theories/IntMap/Map.v
theories/IntMap/Fset.v
theories/IntMap/Mapaxioms.v
theories/IntMap/Mapiter.v
theories/IntMap/Mapcanon.v
theories/IntMap/Mapsubset.v
theories/IntMap/Lsort.v
theories/IntMap/Mapfold.v
theories/IntMap/Mapcard.v
theories/IntMap/Mapc.v
theories/IntMap/Maplists.v
theories/IntMap/Allmaps.v
- Strings
Implementation of string as list of ascii characters
-
theories/Strings/Ascii.v
theories/Strings/String.v
- Sorting:
Axiomatizations of sorts
-
theories/Sorting/Heap.v
theories/Sorting/Permutation.v
theories/Sorting/Sorting.v
theories/Sorting/PermutEq.v
theories/Sorting/PermutSetoid.v