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, power set,
etc.) |
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,... Requires the
ZArith library). |
Relations |
Relations (definitions and basic results). |
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 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
10.
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).
Coq < Require Arith.
Coq < Fixpoint even [n:nat] : bool :=
Coq < Cases n of (0) => true
Coq < | (1) => false
Coq < | (S (S n)) => (even n)
Coq < end.
3.2.4 Real numbers library
Notations for real numbers
This is provided by requiring the module Reals. This notation is very
similar to the notation for integer arithmetics (see figure
3.2.2) where Inverse (/x) and division (x/y) have been added.
This syntax is used parenthesizing by a double back-quote (``
).
Coq < Require Reals.
Coq < Check ``2+3``.
``2+3``
: R
A constant, say ``4``
, is equivalent to ``(1+(1+(1+1)))``
.
Some tactics
In addition to the Ring, Field and Fourier tactics (see chapter 7)
there are:
DiscrR prove that a real integer constante c1 is non equal to
another real integer constante c2.
Coq < Require DiscrR.
Coq < Goal ``5<>0``.
Coq < DiscrR.
Subtree proved!
SplitAbsolu allows us to unfold Rabsolu contants and split
corresponding conjonctions.
Coq < Require SplitAbsolu.
Coq < Goal (x:R) ``x <= (Rabsolu x)``.
Coq < Intro;SplitAbsolu.
2 subgoals
x : R
r : ``x < 0``
============================
``x <= -x``
subgoal 2 is:
``x <= x``
SplitRmult allows us to split a condition that a product is non equal to
zero into subgoals corresponding to the condition on each subterm of the
product.
Coq < Require SplitRmult.
Coq < Goal (x,y,z:R)``x*y*z<>0``.
Coq < Intros;SplitRmult.
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 new tactic language.