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.