Chapter 3  The Coq library

• 3.1  The basic library
• 3.2  The standard library
• 3.3  Users’ contributions

The Coq library is structured into two parts:

The initial library:

it contains elementary logical notions and data-types. It constitutes the basic state of the system directly available when running Coq;

The standard library:

general-purpose libraries containing various developments of Coq axiomatizations about sets, lists, sorting, arithmetic, etc. This library comes with the system and its modules are directly accessible through the Require command (see Section 6.5.1);

In addition, user-provided libraries or developments are provided by Coq users’ community. These libraries and developments are available for download at http://coq.inria.fr (see Section 3.3).

The chapter briefly reviews the Coq libraries.

3.1  The basic library

This section lists the basic notions and results which are directly available in the standard Coq system¹.

3.1.1  Notations

This module defines the parsing and pretty-printing 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 listed on Figure 3.1.

---

Notation	Precedence	Associativity
_ <-> _	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

Figure 3.1: Notations in the initial state

---

3.1.2  Logic

---

form	::=	True	(True)
	|	False	(False)
	|	~ form	(not)
	|	form /\ form	(and)
	|	form \/ form	(or)
	|	form -> form	(primitive implication)
	|	form <-> form	(iff)
	|	forall ident : type , form	(primitive for all)
	|	exists ident [: specif] , form	(ex)
	|	exists2 ident [: specif] , form & form	(ex2)
	|	term = term	(eq)
	|	term = term :> specif	(eq)

Figure 3.2: Syntax of formulas

---

The basic library of Coq comes with the definitions of standard (intuitionistic) logical connectives (they are defined as inductive constructions). They are equipped with an appealing syntax enriching the (subclass form) of the syntactic class term. The syntax extension is shown on Figure 3.2.

Remark: Implication is not defined but primitive (it is a non-dependent 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 first-order and higher-order quantification.

Propositional Connectives

First, we find propositional calculus connectives:

Quantifiers

Then we find first-order quantifiers:

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 Paulin-Mohring, is equivalent to define eq as the smallest reflexive relation, and it is also equivalent to Leibniz’ equality.

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.

3.1.3  Datatypes

---

specif	::=	specif * specif	(prod)
	|	specif + specif	(sum)
	|	specif + { specif }	(sumor)
	|	{ specif } + { specif }	(sumbool)
	|	{ ident : specif | form }	(sig)
	|	{ ident : specif | form & form }	(sig2)
	|	{ ident : specif & specif }	(sigT)
	|	{ ident : specif & specif & specif }	(sigT2)
term	::=	( term , term )	(pair)

Figure 3.3: Syntax of data-types and specifications

---

In the basic library, we find the definition² of the basic data-types of programming, again defined as inductive constructions over the sort Set. Some of them come with a special syntax shown on Figure 3.3.

Programming

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.

Some operations on bool are also provided: andb (with infix notation &&), orb (with infix notation ||), xorb, implb and negb.

3.1.4  Specification

The following notions³ allow to build new data-types and specifications. They are available with the syntax shown on Figure 3.3.

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 data-type. In technical terms, one says that sig is a “weak (dependent) sum”. A variant sig2 with two predicates is also provided.

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.

A related non-dependent construct is the constructive sum {A}+{B} of two propositions A and B.

This sumbool construct may be used as a kind of indexed boolean data-type. An intermediate between sumbool and sum is the mixed sumor which combines A:Set and B:Prop in the Set A+{B}.

We may define variants of the axiom of choice, like in Martin-Löf’s Intuitionistic Type Theory.

The next construct builds a sum between a data-type A:Type and an exceptional value encoding errors:

This module ends with theorems, relating the sorts Set or Type and Prop in a way which is consistent with the realizability interpretation.

3.1.5  Basic Arithmetics

The basic library includes a few elementary properties of natural numbers, together with the definitions of predecessor, addition and multiplication⁴. It also provides a scope nat_scope gathering standard notations for common operations (+, *) and a decimal notation for numbers. That is he can write 3 for (S (S (S O))). This also works on the left hand side of a match expression (see for example section 10.1). This scope is opened by default.

The following example is not part of the standard library, but it shows the usage of the notations:

Finally, it gives the definition of the usual orderings le, lt, ge, and gt.

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.

3.1.6  Well-founded recursion

The basic library contains the basics of well-founded recursion and well-founded induction⁵.

The automatically generated scheme Acc_rect can be used to define functions by fixpoints using well-founded relations to justify termination. Assuming extensionality of the functional used for the recursive call, the fixpoint equation can be proved.

3.1.7  Accessing the Type level

The basic library includes the definitions⁶ of the counterparts of some data-types and logical quantifiers at the Type level: negation, pair, and properties of identity.

At the end, it defines data-types at the Type level.

3.1.8  Tactics

A few tactics defined at the user level are provided in the initial state⁷.

3.2  The standard library

3.2.1  Survey

The rest of the standard library is structured into the following subdirectories:

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 Chapter 6).

The different modules of the Coq standard library are described in the additional document Library.dvi. They are also accessible on the WWW through the Coq homepage ⁸.

3.2.2  Notations for integer arithmetics

On Figure 3.4 is described the syntax of expressions for integer arithmetics. It is provided by requiring and opening the module ZArith and opening scope Z_scope.

---

Notation	Interpretation	Precedence	Associativity
_ < _	Zlt
x <= y	Zle
_ > _	Zgt
x >= y	Zge
x < y < z	x < y /\ y < z
x < y <= z	x < y /\ y <= z
x <= y < z	x <= y /\ y < z
x <= y <= z	x <= y /\ y <= z
_ ?= _	Zcompare	70	no
_ + _	Zplus
_ - _	Zminus
_ * _	Zmult
_ / _	Zdiv
_ mod _	Zmod	40	no
- _	Zopp
_ ^ _	Zpower

Figure 3.4: Definition of the scope for integer arithmetics (Z_scope)

---

Figure 3.4 shows the notations provided by Z_scope. It specifies how notations are interpreted and, when not already reserved, the precedence and associativity.

3.2.3  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.

Figure 3.5 describes notation available in scope nat_scope.

---

Notation	Interpretation
_ < _	lt
x <= y	le
_ > _	gt
x >= y	ge
x < y < z	x < y /\ y < z
x < y <= z	x < y /\ y <= z
x <= y < z	x <= y /\ y < z
x <= y <= z	x <= y /\ y <= z
_ + _	plus
_ - _	minus
_ * _	mult

Figure 3.5: Definition of the scope for natural numbers (nat_scope)

---

3.2.4  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 arithmetics. The inverse function was added.

---

Notation	Interpretation
_ < _	Rlt
x <= y	Rle
_ > _	Rgt
x >= y	Rge
x < y < z	x < y /\ y < z
x < y <= z	x < y /\ y <= z
x <= y < z	x <= y /\ y < z
x <= y <= z	x <= y /\ y <= z
_ + _	Rplus
_ - _	Rminus
_ * _	Rmult
_ / _	Rdiv
- _	Ropp
/ _	Rinv
_ ^ _	pow

Figure 3.6: Definition of the scope for real arithmetics (R_scope)

---

Some tactics

In addition to the ring, field and fourier tactics (see Chapter 8) there are:

• discrR

  Proves that a real integer constant c₁ is different from another real integer constant c₂.

  Coq < Require Import DiscrR.
  
  Coq < Goal 5 <> 0.
  
  Coq < discrR.
  Proof completed.
  
• split_Rabs allows to unfold Rabs constant and splits corresponding conjonctions.
  Coq < Require Import SplitAbsolu.
  
  Coq < Goal forall x:R, x <= Rabs x.
  
  Coq < intro; split_Rabs.
  2 subgoals
    
    x : R
    r : x < 0
    ============================
     x <= - x
  subgoal 2 is:
   x <= x
  
• split_Rmult allows to split a condition that a product is non null into subgoals corresponding to the condition on each operand of the product.
  Coq < Require Import SplitRmult.
  
  Coq < Goal forall x y z:R, x * y * z <> 0.
  
  Coq < intros; split_Rmult.
  3 subgoals
    
    x : R
    y : R
    z : R
    ============================
     x <> 0
  subgoal 2 is:
   y <> 0
  subgoal 3 is:
   z <> 0
  

All this tactics has been written with the tactic language Ltac described in Chapter 9.

3.2.5  List library

Some elementary operations on polymorphic lists are defined here. They can be accessed by requiring module List.

It defines the following notions:

Table show notations available when opening scope list_scope.

---

Notation	Interpretation	Precedence	Associativity
_ ++ _	app	60	right
_ :: _	cons	60	right

Figure 3.7: Definition of the scope for lists (list_scope)

---

3.3  Users’ contributions

Numerous users’ contributions have been collected and are available at URL http://coq.inria.fr/contribs/. 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.

1

Most of these constructions are defined in the Prelude module in directory theories/Init at 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

2

They are in Datatypes.v

3

They are defined in module Specif.v

4

This is in module Peano.v

5

This is defined in module Wf.v

6

This is in module Logic_Type.v

7

This is in module Tactics.v

8

http://coq.inria.fr