The Coq library¶
The Coq library has two parts:
The prelude: definitions and theorems for the most commonly used elementary logical notions and data types. Coq normally loads these files automatically when it starts.
The standard library: generalpurpose libraries with definitions and theorems for sets, lists, sorting, arithmetic, etc. To use these files, users must load them explicitly with the
Require
command (see Compiled files)
There are also many libraries provided by Coq users' community. These libraries and developments are available for download at https://coq.inria.fr/ (see Users’ contributions).
This chapter briefly reviews the Coq libraries whose contents can also be browsed at https://coq.inria.fr/stdlib/.
The prelude¶
This section lists the basic notions and results which are directly
available in the standard Coq system. Most of these constructions
are defined in the Prelude
module in directory theories/Init
in the Coq root directory; this includes the modules
Notations
,
Logic
,
Datatypes
,
Specif
,
Peano
,
Wf
and
Tactics
.
Module Logic_Type
also makes it in the initial state.
Notations¶
This module defines the parsing and prettyprinting of many symbols (infixes, prefixes, etc.). However, it does not assign a meaning to these notations. The purpose of this is to define and fix once for all the precedence and associativity of very common notations. The main notations fixed in the initial state are :
Notation 
Precedence 
Associativity 


99 
right 

95 
no 

85 
right 

80 
right 

75 
right 

70 
no 

70 
no 

70 
no 

70 
no 

70 
no 

70 
no 

70 
no 

70 
no 

70 
no 

70 
no 

70 
no 

70 
no 

70 
no 

50 
left 

50 
left 

50 
left 

40 
left 

40 
left 

40 
left 

35 
right 

35 
right 

30 
right 
Logic¶
Logic.v
in the basic library of Coq has the definitions of standard
(intuitionistic) logical connectives defined as inductive
constructions. They are equipped with an appealing syntax enriching the
subclass form
of the syntactic class term
. The constructs
for form
are:
True 
True 
False 
False 

not 
and 

or 

primitive implication 

iff 

primitive for all 

ex 

ex2 

eq 

eq 
Note
Implication is not defined but primitive (it is a nondependent product of a proposition over another proposition). There is also a primitive universal quantification (it is a dependent product over a proposition). The primitive universal quantification allows both firstorder and higherorder quantification.
Propositional Connectives¶
First, we find propositional calculus connectives. At times, it's helpful to know exactly what these notations represent.
Quantifiers¶
Then we find firstorder quantifiers:
 Definition all (A:Set) (P:A > Prop) := forall x:A, P x.
 all is defined
 Inductive ex (A: Set) (P:A > Prop) : Prop := ex_intro (x:A) (_:P x).
 ex is defined ex_ind is defined ex_sind is defined
 Inductive ex2 (A:Set) (P Q:A > Prop) : Prop := ex_intro2 (x:A) (_:P x) (_:Q x).
 ex2 is defined ex2_ind is defined ex2_sind is defined
The following abbreviations are allowed:








The type annotation :A
can be omitted when A
can be
synthesized by the system.
Equality¶
Then, we find equality, defined as an inductive relation. That is,
given a type A
and an x
of type A
, the
predicate (eq A x)
is the smallest one which contains x
.
This definition, due to Christine PaulinMohring, is equivalent to
define eq
as the smallest reflexive relation, and it is also
equivalent to Leibniz' equality.
 Inductive eq (A:Type) (x:A) : A > Prop := eq_refl : eq A x x.
 eq is defined eq_rect is defined eq_ind is defined eq_rec is defined eq_sind is defined
Lemmas¶
Finally, a few easy lemmas are provided.
The theorem f_equal
is extended to functions with two to five
arguments. The theorem are names f_equal2
, f_equal3
,
f_equal4
and f_equal5
.
For instance f_equal3
is defined the following way.
 Theorem f_equal3 : forall (A1 A2 A3 B:Type) (f:A1 > A2 > A3 > B) (x1 y1:A1) (x2 y2:A2) (x3 y3:A3), x1 = y1 > x2 = y2 > x3 = y3 > f x1 x2 x3 = f y1 y2 y3.
 1 goal ============================ forall (A1 A2 A3 B : Type) (f : A1 > A2 > A3 > B) (x1 y1 : A1) (x2 y2 : A2) (x3 y3 : A3), x1 = y1 > x2 = y2 > x3 = y3 > f x1 x2 x3 = f y1 y2 y3
Datatypes¶
In the basic library, we find in Datatypes.v
the definition
of the basic datatypes of programming,
defined as inductive constructions over the sort Set
. Some of
them come with a special syntax shown below (this syntax table is common with
the next section Specification). The constructs for specif
are:
prod 

sum 

sumor 

sumbool 

sig 

sig2 

sigT 

sigT2 
The notation for pairs (elements of type prod) is: (term, term)
Programming¶
 Inductive unit : Set := tt.
 unit is defined unit_rect is defined unit_ind is defined unit_rec is defined unit_sind is defined
 Inductive bool : Set := true  false.
 bool is defined bool_rect is defined bool_ind is defined bool_rec is defined bool_sind is defined
 Inductive nat : Set := O  S (n:nat).
 nat is defined nat_rect is defined nat_ind is defined nat_rec is defined nat_sind is defined
 Inductive option (A:Set) : Set := Some (_:A)  None.
 option is defined option_rect is defined option_ind is defined option_rec is defined option_sind is defined
 Inductive identity (A:Type) (a:A) : A > Type := refl_identity : identity A a a.
 identity is defined identity_rect is defined identity_ind is defined identity_rec is defined identity_sind is defined
Note that zero is the letter O
, and not the numeral 0
.
The predicate identity
is logically
equivalent to equality but it lives in sort Type
.
It is mainly maintained for compatibility.
We then define the disjoint sum of A+B
of two sets A
and
B
, and their product A*B
.
 Inductive sum (A B:Set) : Set := inl (_:A)  inr (_:B).
 sum is defined sum_rect is defined sum_ind is defined sum_rec is defined sum_sind is defined
 Inductive prod (A B:Set) : Set := pair (_:A) (_:B).
 prod is defined prod_rect is defined prod_ind is defined prod_rec is defined prod_sind is defined
 Section projections.
 Variables A B : Set.
 A is declared B is declared
 Definition fst (H: prod A B) := match H with  pair _ _ x y => x end.
 fst is defined
 Definition snd (H: prod A B) := match H with  pair _ _ x y => y end.
 snd is defined
 End projections.
Some operations on bool
are also provided: andb
(with
infix notation &&
), orb
(with
infix notation 
), xorb
, implb
and negb
.
Specification¶
The following notions defined in module Specif.v
allow to build new datatypes and specifications.
They are available with the syntax shown in the previous section Datatypes.
For instance, given A:Type
and P:A>Prop
, the construct
{x:A  P x}
(in abstract syntax (sig A P)
) is a
Type
. We may build elements of this set as (exist x p)
whenever we have a witness x:A
with its justification
p:P x
.
From such a (exist x p)
we may in turn extract its witness
x:A
(using an elimination construct such as match
) but
not its justification, which stays hidden, like in an abstract
datatype. In technical terms, one says that sig
is a weak
(dependent) sum. A variant sig2
with two predicates is also
provided.
 Inductive sig (A:Set) (P:A > Prop) : Set := exist (x:A) (_:P x).
 sig is defined sig_rect is defined sig_ind is defined sig_rec is defined sig_sind is defined
 Inductive sig2 (A:Set) (P Q:A > Prop) : Set := exist2 (x:A) (_:P x) (_:Q x).
 sig2 is defined sig2_rect is defined sig2_ind is defined sig2_rec is defined sig2_sind is defined
A strong (dependent) sum {x:A & P x}
may be also defined,
when the predicate P
is now defined as a
constructor of types in Type
.
 Inductive sigT (A:Type) (P:A > Type) : Type := existT (x:A) (_:P x).
 sigT is defined sigT_rect is defined sigT_ind is defined sigT_rec is defined sigT_sind is defined
 Section Projections2.
 Variable A : Type.
 A is declared
 Variable P : A > Type.
 P is declared
 Definition projT1 (H:sigT A P) := let (x, h) := H in x.
 projT1 is defined
 Definition projT2 (H:sigT A P) := match H return P (projT1 H) with existT _ _ x h => h end.
 projT2 is defined
 End Projections2.
 Inductive sigT2 (A: Type) (P Q:A > Type) : Type := existT2 (x:A) (_:P x) (_:Q x).
 sigT2 is defined sigT2_rect is defined sigT2_ind is defined sigT2_rec is defined sigT2_sind is defined
A related nondependent construct is the constructive sum
{A}+{B}
of two propositions A
and B
.
 Inductive sumbool (A B:Prop) : Set := left (_:A)  right (_:B).
 sumbool is defined sumbool_rect is defined sumbool_ind is defined sumbool_rec is defined sumbool_sind is defined
This sumbool
construct may be used as a kind of indexed boolean
datatype. An intermediate between sumbool
and sum
is
the mixed sumor
which combines A:Set
and B:Prop
in the construction A+{B}
in Set
.
 Inductive sumor (A:Set) (B:Prop) : Set :=  inleft (_:A)  inright (_:B).
 sumor is defined sumor_rect is defined sumor_ind is defined sumor_rec is defined sumor_sind is defined
We may define variants of the axiom of choice, like in MartinLöf's Intuitionistic Type Theory.
The next construct builds a sum between a datatype A:Type
and
an exceptional value encoding errors:
 Definition Exc := option.
 Exc is defined
 Definition value := Some.
 value is defined
 Definition error := None.
 error is defined
This module ends with theorems, relating the sorts Set
or
Type
and Prop
in a way which is consistent with the
realizability interpretation.
Basic Arithmetic¶
The basic library includes a few elementary properties of natural
numbers, together with the definitions of predecessor, addition and
multiplication, in module Peano.v
. It also
provides a scope nat_scope
gathering standard notations for
common operations (+
, *
) and a decimal notation for
numbers, allowing, for instance, writing 3
for S (S (S O))
.
This also works on
the left hand side of a match
expression (see for example
section refine
). This scope is opened by default.
Example
The following example is not part of the standard library, but it shows the usage of the notations:
 Fixpoint even (n:nat) : bool := match n with  0 => true  1 => false  S (S n) => even n end.
 even is defined even is recursively defined (guarded on 1st argument)
Now comes the content of module Peano
:
Finally, it gives the definition of the usual orderings le
,
lt
, ge
and gt
.
 Inductive le (n:nat) : nat > Prop :=  le_n : le n n  le_S : forall m:nat, n <= m > n <= (S m) where "n <= m" := (le n m) : nat_scope.
 Toplevel input, characters 0137: > Inductive le (n:nat) : nat > Prop :=  le_n : le n n  le_S : forall m:nat, n <= m > n <= (S m) where "n <= m" := (le n m) : nat_scope. > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning: Notation "_ <= _" was already used in scope nat_scope. [notationoverridden,parsing,default] le is defined le_ind is defined le_sind is defined Toplevel input, characters 0137: > Inductive le (n:nat) : nat > Prop :=  le_n : le n n  le_S : forall m:nat, n <= m > n <= (S m) where "n <= m" := (le n m) : nat_scope. > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning: Notation "_ <= _" was already used in scope nat_scope. [notationoverridden,parsing,default]
 Definition lt (n m:nat) := S n <= m.
 lt is defined
 Definition ge (n m:nat) := m <= n.
 ge is defined
 Definition gt (n m:nat) := m < n.
 gt is defined
Properties of these relations are not initially known, but may be
required by the user from modules Le
and Lt
. Finally,
Peano
gives some lemmas allowing pattern matching, and a double
induction principle.
Wellfounded recursion¶
The basic library contains the basics of wellfounded recursion and
wellfounded induction, in module Wf.v
.
The automatically generated scheme Acc_rect
can be used to define functions by fixpoints using
wellfounded relations to justify termination. Assuming
extensionality of the functional used for the recursive call, the
fixpoint equation can be proved.
Accessing the Type level¶
The standard library includes Type
level definitions of counterparts of some
logic concepts and basic lemmas about them.
The module Datatypes
defines identity
, which is the Type
level counterpart
of equality:
 Inductive identity (A:Type) (a:A) : A > Type := identity_refl : identity A a a.
 identity is defined identity_rect is defined identity_ind is defined identity_rec is defined identity_sind is defined
Some properties of identity
are proved in the module Logic_Type
, which also
provides the definition of Type
level negation:
 Definition notT (A:Type) := A > False.
 notT is defined
Tactics¶
A few tactics defined at the user level are provided in the initial
state, in module Tactics.v
. They are listed at
https://coq.inria.fr/stdlib/, in paragraph Init
, link Tactics
.
The standard library¶
Survey¶
The rest of the standard library is structured into the following subdirectories:
Logic : Classical logic and dependent equality
Arith : Basic Peano arithmetic
PArith : Basic positive integer arithmetic
NArith : Basic binary natural number arithmetic
ZArith : Basic relative integer arithmetic
Numbers : Various approaches to natural, integer and cyclic numbers (currently axiomatically and on top of 2^31 binary words)
Bool : Booleans (basic functions and results)
Lists : Monomorphic and polymorphic lists (basic functions and results), Streams (infinite sequences defined with coinductive types)
Sets : Sets (classical, constructive, finite, infinite, power set, etc.)
FSets : Specification and implementations of finite sets and finite maps (by lists and by AVL trees)
Reals : Axiomatization of real numbers (classical, basic functions, integer part, fractional part, limit, derivative, Cauchy series, power series and results,...)
Floats : Machine implementation of floatingpoint arithmetic (for the binary64 format)
Relations : Relations (definitions and basic results)
Sorting : Sorted list (basic definitions and heapsort correctness)
Strings : 8bits characters and strings
Wellfounded : Wellfounded relations (basic results)
These directories belong to the initial load path of the system, and
the modules they provide are compiled at installation time. So they
are directly accessible with the command Require
(see
Section Compiled files).
The different modules of the Coq standard library are documented online at https://coq.inria.fr/stdlib/.
Peano’s arithmetic (nat)¶
While in the initial state, many operations and predicates of Peano's
arithmetic are defined, further operations and results belong to other
modules. For instance, the decidability of the basic predicates are
defined here. This is provided by requiring the module Arith
.
The following table describes the notations available in scope
nat_scope
:
Notation 
Interpretation 























Notations for integer arithmetic¶
The following table describes the syntax of expressions
for integer arithmetic. It is provided by requiring and opening the module ZArith
and opening scope Z_scope
.
It specifies how notations are interpreted and, when not
already reserved, the precedence and associativity.
Notation 
Interpretation 
Precedence 
Associativity 



























70 
no 














40 
no 





Example
 Require Import ZArith.
 [Loading ML file ring_plugin.cmxs (using legacy method) ... done] [Loading ML file zify_plugin.cmxs (using legacy method) ... done] [Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done] [Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
 Check (2 + 3)%Z.
 (2 + 3)%Z : Z
 Open Scope Z_scope.
 Check 2 + 3.
 2 + 3 : Z
Real numbers library¶
Notations for real numbers¶
This is provided by requiring and opening the module Reals
and
opening scope R_scope
. This set of notations is very similar to
the notation for integer arithmetic. The inverse function was added.
Notation 
Interpretation 































Example
 Require Import Reals.
 Check (2 + 3)%R.
 (2 + 3)%R : R
 Open Scope R_scope.
 Check 2 + 3.
 2 + 3 : R
Some tactics for real numbers¶
In addition to the powerful ring
, field
and lra
tactics (see Chapter Tactics), there are also:
 Tactic discrR¶
Proves that two real integer constants are different.
Example
 Require Import DiscrR.
 Open Scope R_scope.
 Goal 5 <> 0.
 1 goal ============================ 5 <> 0
 discrR.
 Tactic split_Rabs¶
Allows unfolding the
Rabs
constant and splits corresponding conjunctions.
Example
 Require Import Reals.
 Open Scope R_scope.
 Goal forall x:R, x <= Rabs x.
 1 goal ============================ forall x : R, x <= Rabs x
 intro; split_Rabs.
 2 goals x : R Hlt : x < 0 ============================ x <=  x goal 2 is: x <= x
 Tactic split_Rmult¶
Splits a condition that a product is nonnull into subgoals corresponding to the condition on each operand of the product.
Example
 Require Import Reals.
 Open Scope R_scope.
 Goal forall x y z:R, x * y * z <> 0.
 1 goal ============================ forall x y z : R, x * y * z <> 0
 intros; split_Rmult.
 3 goals x, y, z : R ============================ x <> 0 goal 2 is: y <> 0 goal 3 is: z <> 0
List library¶
Some elementary operations on polymorphic lists are defined here.
They can be accessed by requiring module List
.
It defines the following notions:
length
head
: first element (with default)
tail
: all but first element
app
: concatenation
rev
: reverse
nth
: accessing nth element (with default)
map
: applying a function
flat_map
: applying a function returning lists
fold_left
: iterator (from head to tail)
fold_right
: iterator (from tail to head)
The following table shows notations available when opening scope list_scope
.
Notation 
Interpretation 
Precedence 
Associativity 



60 
right 


60 
right 
Floats library¶
The standard library has a small Floats
module for accessing
processor floatingpoint operations through the Coq kernel.
However, while this module supports computation and has a bitlevel
specification, it doesn't include elaborate theorems, such as a link
to real arithmetic or various error bounds. To do proofs by
reflection, use Floats
in conjunction with the complementary
Flocq library, which provides
many such theorems.
The library of primitive floatingpoint arithmetic can be loaded by
requiring module Floats
:
 Require Import Floats.
It exports the module PrimFloat
that provides a primitive type
named float
, defined in the kernel (see section Primitive Floats),
as well as two variant types float_comparison
and float_class
:
 Print float.
 *** [ float : Set ]
 Print float_comparison.
 Variant float_comparison : Set := FEq : float_comparison  FLt : float_comparison  FGt : float_comparison  FNotComparable : float_comparison.
 Print float_class.
 Variant float_class : Set := PNormal : float_class  NNormal : float_class  PSubn : float_class  NSubn : float_class  PZero : float_class  NZero : float_class  PInf : float_class  NInf : float_class  NaN : float_class.
It then defines the primitive operators below, using the processor floatingpoint operators for binary64 in roundingtonearest even:
abs
opp
sub
add
mul
div
sqrt
compare
: compare two floats and return afloat_comparison
classify
: analyze a float and return afloat_class
of_int63
: round a primitive integer and convert it into a floatnormfr_mantissa
: take a float in[0.5; 1.0)
and return its mantissafrshiftexp
: convert a float to fractional part in[0.5; 1.0)
and integer partldshiftexp
: multiply a float by an integral power of2
next_up
: return the next float towards positive infinitynext_down
: return the next float towards negative infinity
For special floatingpoint values, the following constants are also defined:
zero
neg_zero
one
two
infinity
neg_infinity
nan
: Not a Number (assumed to be unique: the "payload" of NaNs is ignored)
The following table shows the notations available when opening scope
float_scope
.
Notation 
Interpretation 



















Floatingpoint constants are parsed and prettyprinted as (17digit) decimal constants. This ensures that the composition \(\text{parse} \circ \text{print}\) amounts to the identity.
 Warning The constant number is not a binary64 floatingpoint value. A closest value number will be used and unambiguously printed number. [inexactfloat,parsing]¶
Not all decimal constants are floatingpoint values. This warning is generated when parsing such a constant (for instance
0.1
).
 Flag Printing Float¶
Turn this flag off (it is on by default) to deactivate decimal printing of floatingpoint constants. They will then be printed with an hexadecimal representation.
Example
 Open Scope float_scope.
 Eval compute in 1 + 0.5.
 = 1.5 : float
 Eval compute in 1 / 0.
 = infinity : float
 Eval compute in 1 / 0.
 = neg_infinity : float
 Eval compute in 0 / 0.
 = nan : float
 Eval compute in 0 ?= 0.
 = FEq : float_comparison
 Eval compute in nan ?= nan.
 = FNotComparable : float_comparison
 Eval compute in next_down (1).
 = 1.0000000000000002 : float
The primitive operators are specified with respect to their Gallina
counterpart, using the variant type spec_float
, and the injection
Prim2SF
:
 Print spec_float.
 Variant spec_float : Set := S754_zero : bool > spec_float  S754_infinity : bool > spec_float  S754_nan : spec_float  S754_finite : bool > positive > Z > spec_float. Arguments S754_zero s%bool_scope Arguments S754_infinity s%bool_scope Arguments S754_finite s%bool_scope m%positive_scope e%Z_scope
 Check Prim2SF.
 Prim2SF : float > spec_float
 Check mul_spec.
 mul_spec : forall x y : float, Prim2SF (x * y) = SF64mul (Prim2SF x) (Prim2SF y)
For more details on the available definitions and lemmas, see the
online documentation of the Floats
library.
Users’ contributions¶
Numerous users' contributions have been collected and are available at URL https://coq.inria.fr/opam/www/. On this web page, you have a list of all contributions with informations (author, institution, quick description, etc.) and the possibility to download them one by one. You will also find informations on how to submit a new contribution.