The Coq library is structured into three parts:
Require command
(see Section 6.4.1);This chapter briefly reviews these libraries.
This section lists the basic notions and results which are directly available in the standard Coq system1.
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 precedence and associativity of very common notations, and avoid users to use them with other precedence, which may be confusing.
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 _ * _40 left _ / _40 left - _35 right / _35 right _ ^ _30 right
Figure 3.1: Notations in the initial state
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.
First, we find propositional calculus connectives:
Then we find first-order quantifiers:
The following abbreviations are allowed:
exists x:A, P | ex A (fun x:A => P) |
exists x, P | ex _ (fun x => P) |
exists2 x:A, P & Q | ex2 A (fun x:A => P) (fun x:A => Q) |
exists2 x, P & Q | ex2 _ (fun x => P) (fun x => Q) |
The type annotation :A can be omitted when A can be synthesized by the system.
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.
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.
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 } (sigS) | { ident : specif & specif & specif } (sigS2) term ::= ( term , term ) (pair)
Figure 3.3: Syntax of datatypes and specifications
In the basic library, we find the definition2 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.
Note that zero is the letter O, and not the numeral
0.
identity is logically equivalent to equality but it lives in sort Set. Computationaly, it behaves like unit.
We then define the disjoint sum of A+B of two sets A and
B, and their product A*B.
The following notions3 allows to build new datatypes and specifications. They are available with the syntax shown on Figure 3.34.
For instance, given A:Set and P:A->Prop, the construct
{x:A | P x} (in abstract syntax (sig A P)) is a
Set. 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 Set
constructor.
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 constructs builds a sum between a data type A:Set and
an exceptional value encoding errors:
This module ends with theorems,
relating the sorts Set and
Prop in a way which is consistent with the realizability
interpretation.
The basic library includes a few elementary properties of natural numbers, together with the definitions of predecessor, addition and multiplication5. 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.
The basic library contains the basics of well-founded recursion and well-founded induction6.
Acc_rec 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.
The basic library includes the definitions7 of the counterparts of some datatypes and logical
quantifiers at the Type level: negation, pair, and properties
of identity.
At the end, it defines datatypes at the Type level.
The rest of the standard library is structured into the following subdirectories:
| Logic | Classical logic and dependent equality |
| Arith | Basic Peano arithmetic |
| NArith | Basic positive integer arithmetic |
| ZArith | Basic relative integer arithmetic |
| Bool | Booleans (basic functions and results) |
| Lists | Monomorphic and polymorphic lists (basic functions and results), Streams (infinite sequences defined with co-inductive 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) |
| IntMap | Representation of finite sets by an efficient structure of map (trees indexed by binary integers). |
| Reals | Axiomatization of real numbers (classical, basic functions, integer part, fractional part, limit, derivative, Cauchy series, power series and results,...) |
| Relations | Relations (definitions and basic results). |
| Sorting | Sorted list (basic definitions and heapsort correctness). |
| Strings | 8-bits characters and strings |
| Wellfounded | Well-founded 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
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
8.
On Figure 3.2.2 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 <= yZle _ > _Zgt x >= yZge x < y < zx < y /\y < zx < y <= zx < y /\y <= zx <= y < zx <= y /\y < zx <= y <= zx <= 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.2.2 shows the notations provided by Z_scope. It specifies how notations are interpreted and, when not already reserved, the precedence and associativity.
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.2.3 describes notation available in scope nat_scope.
Notation Interpretation _ < _lt x <= yle _ > _gt x >= yge x < y < zx < y /\y < zx < y <= zx < y /\y <= zx <= y < zx <= y /\y < zx <= y <= zx <= y /\y <= z_ + _plus _ - _minus _ * _mult
Figure 3.5: Definition of the scope for natural numbers (nat_scope)
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 <= yRle _ > _Rgt x >= yRge x < y < zx < y /\y < zx < y <= zx < y /\y <= zx <= y < zx <= y /\y < zx <= y <= zx <= y /\y <= z_ + _Rplus _ - _Rminus _ * _Rmult _ / _Rdiv - _Ropp / _Rinv _ ^ _pow
Figure 3.6: Definition of the scope for real arithmetics (R_scope)
In addition to the ring, field and fourier
tactics (see Chapter 8) there are:
Proves that a real integer constant c1 is different from another real integer constant c2.
All this tactics has been written with the tactic language Ltac described in Chapter 9. More details are available in document http://coq.inria.fr/~desmettr/Reals.ps.
Some elementary operations on polymorphic lists are defined here. They can be accessed by requiring module List.
It defines the following notions:
| length | length |
| head | first element (with default) |
| tail | all but first element |
| app | concatenation |
| rev | reverse |
| nth | accessing n-th 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) |
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)
Numerous users’ contributions have been collected and are available at URL 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. There is a small search engine to look for keywords in all contributions. You will also find informations on how to submit a new contribution.
The users’ contributions may also be obtained by anonymous FTP from site
ftp.inria.fr, in directory INRIA/coq/ and
searchable on-line at http://coq.inria.fr/contribs-eng.html