3.2 The standard library
3.2.1 Survey
The rest of the standard library is structured into the following subdirectories:| LOGIC | Classical logic and dependent equality |
| ARITH | Basic Peano arithmetic |
| ZARITH | Basic 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, powerset, etc.) |
| RELATIONS | Relations (definitions and basic results). There is a subdirectory about well-founded relations (WELLFOUNDED) |
| SORTING | Axiomatizations of sorts |
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 5). 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
(http://pauillac.inria.fr/coq).
3.2.2 Notations for integer arithmetics
On figure 3.2.2 is described the syntax of expressions for integer arithmetics. It is provided by requiring the module ZArith.The + and - binary operators bind less than the * operator which binds less than the | ... | and - unary operators which bind less than the others constructions. All the binary operators are left associative. The [ ... ] allows to escape the zarith grammar.
form ::= ` zarith_formula ` term ::= ` zarith ` zarith_formula ::= zarith = zarith | zarith <= zarith | zarith < zarith | zarith >= zarith | zarith > zarith | zarith = zarith = zarith | zarith <= zarith <= zarith | zarith <= zarith < zarith | zarith < zarith <= zarith | zarith < zarith < zarith | zarith <> zarith | zarith ? = zarith zarith ::= zarith + zarith | zarith - zarith | zarith * zarith | | zarith | | - zarith | ident | [ term ] | ( zarith ... zarith ) | ( zarith , ... , zarith ) | integer
Figure 3.4:Syntax of expressions in integer arithmetics
3.2.3 Notations for Peano's arithmetic (nat)
After having required the module Arith, the user can type the naturals using decimal notation. That is he can write (3) for (S (S (S O))). The number must be between parentheses. This works also in the left hand side of a Cases expression (see for example section 8.1).