Merge PR #6997: Sphinx doc chapter 3

5 files changed, 989 insertions, 1114 deletions

diff --git a/Makefile.doc b/Makefile.doc
index a6d4584d8..7c68e5d8e 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -58,7 +58,6 @@ DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex
 
 REFMANCOQTEXFILES:=$(addprefix doc/refman/, \
   RefMan-gal.v.tex \
-  RefMan-lib.v.tex \
   RefMan-oth.v.tex RefMan-ltac.v.tex \
   RefMan-pro.v.tex \
   Cases.v.tex Coercion.v.tex CanonicalStructures.v.tex Extraction.v.tex \
diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex
deleted file mode 100644
index 89f5be843..000000000
--- a/doc/refman/RefMan-lib.tex
+++ /dev/null
@@ -1,1112 +0,0 @@
-\chapter[The {\Coq} library]{The {\Coq} library\index{Theories}\label{Theories}}
-%HEVEA\cutname{stdlib.html}
-
-The \Coq\ library is structured into two parts:
-
-\begin{description}
-\item[The initial library:] it contains
-  elementary logical notions and data-types. It constitutes the
-  basic state of the system directly available when running
-  \Coq;
-
-\item[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 \verb!Require! command
-  (see Section~\ref{Require});
-\end{description}
-
-In addition, user-provided libraries or developments are provided by
-\Coq\ users' community. These libraries and developments are available
-for download at \url{http://coq.inria.fr} (see
-Section~\ref{Contributions}).
-
-The chapter briefly reviews the \Coq\ libraries whose contents can
-also be browsed at \url{http://coq.inria.fr/stdlib}.
-
-\section[The basic library]{The basic library\label{Prelude}}
-
-This section lists the basic notions and results which are directly
-available in the standard \Coq\ system\footnote{Most 
-of these constructions are defined in the
-{\tt Prelude} module in directory {\tt theories/Init} at the {\Coq}
-root directory; this includes the modules
-{\tt Notations},
-{\tt Logic},
-{\tt Datatypes},
-{\tt Specif},
-{\tt Peano},
-{\tt Wf} and 
-{\tt Tactics}.
-Module {\tt Logic\_Type} also makes it in the initial state}.
-
-\subsection[Notations]{Notations\label{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~\ref{init-notations}.
-
-\begin{figure}
-\begin{center}
-\begin{tabular}{|cll|}
-\hline
-Notation & Precedence & Associativity \\
-\hline
-\verb!_ -> _! & 99 & right \\
-\verb!_ <-> _! & 95 & no \\
-\verb!_ \/ _!  & 85 & right \\
-\verb!_ /\ _!  & 80 & right \\
-\verb!~ _!   & 75 & right \\
-\verb!_ = _!   & 70 & no \\
-\verb!_ = _ = _!   & 70 & no \\
-\verb!_ = _ :> _!   & 70 & no \\
-\verb!_ <> _!  & 70 & no \\
-\verb!_ <> _ :> _!  & 70 & no \\
-\verb!_ < _!   & 70 & no \\
-\verb!_ > _!   & 70 & no \\
-\verb!_ <= _!  & 70 & no \\
-\verb!_ >= _!  & 70 & no \\
-\verb!_ < _ < _! & 70 & no \\
-\verb!_ < _ <= _! & 70 & no \\
-\verb!_ <= _ < _! & 70 & no \\
-\verb!_ <= _ <= _! & 70 & no \\
-\verb!_ + _!   & 50 & left \\
-\verb!_ || _!  & 50 & left \\
-\verb!_ - _!   & 50 & left \\
-\verb!_ * _!   & 40 & left \\
-\verb!_ && _!  & 40 & left \\
-\verb!_ / _!   & 40 & left \\
-\verb!- _!  & 35 & right \\
-\verb!/ _!  & 35 & right \\
-\verb!_ ^ _!   & 30 & right \\
-\hline
-\end{tabular}
-\end{center}
-\caption{Notations in the initial state}
-\label{init-notations}
-\end{figure}
-
-\subsection[Logic]{Logic\label{Logic}}
-
-\begin{figure}
-\begin{centerframe}
-\begin{tabular}{lclr}
-{\form} & ::= & {\tt True} & ({\tt True})\\
-  & $|$ & {\tt False} & ({\tt False})\\
-  & $|$ & {\tt\char'176} {\form} & ({\tt not})\\
-  & $|$ & {\form} {\tt /$\backslash$} {\form} & ({\tt and})\\
-  & $|$ & {\form} {\tt $\backslash$/} {\form} & ({\tt or})\\
-  & $|$ & {\form} {\tt ->} {\form} & (\em{primitive implication})\\
-  & $|$ & {\form} {\tt <->} {\form} & ({\tt iff})\\
-  & $|$ & {\tt forall} {\ident} {\tt :} {\type} {\tt ,}
-  {\form} & (\em{primitive for all})\\
-  & $|$ & {\tt exists} {\ident} \zeroone{{\tt :} {\specif}} {\tt
-  ,} {\form}  & ({\tt ex})\\
-  & $|$ & {\tt exists2} {\ident} \zeroone{{\tt :} {\specif}} {\tt
-  ,} {\form}  {\tt \&} {\form} & ({\tt ex2})\\
-  & $|$ & {\term} {\tt =} {\term} & ({\tt eq})\\
-  & $|$ & {\term} {\tt =} {\term} {\tt :>} {\specif} & ({\tt eq})
-\end{tabular}
-\end{centerframe}
-\caption{Syntax of formulas}
-\label{formulas-syntax}
-\end{figure}
-
-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~\ref{formulas-syntax}.
-
-% 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 \footnote{This syntax is defined in module {\tt
-%     LogicSyntax}} is shown on Figure~\ref{formulas-syntax}.
- 
-\Rem 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.
-
-\subsubsection[Propositional Connectives]{Propositional Connectives\label{Connectives}
-\index{Connectives}}
-
-First, we find propositional calculus connectives:
-\ttindex{True}
-\ttindex{I}
-\ttindex{False}
-\ttindex{not}
-\ttindex{and}
-\ttindex{conj}
-\ttindex{proj1}
-\ttindex{proj2}
-
-\begin{coq_eval}
-Set Printing Depth 50.
-\end{coq_eval}
-\begin{coq_example*}
-Inductive True : Prop := I.
-Inductive False :  Prop := .
-Definition not (A: Prop) := A -> False.
-Inductive and (A B:Prop) : Prop := conj (_:A) (_:B).
-Section Projections.
-Variables A B : Prop.
-Theorem proj1 : A /\ B -> A.
-Theorem proj2 : A /\ B -> B.
-\end{coq_example*}
-\begin{coq_eval}
-Abort All.
-\end{coq_eval}
-\begin{coq_example*}
-End Projections.
-\end{coq_example*}
-\ttindex{or}
-\ttindex{or\_introl}
-\ttindex{or\_intror}
-\ttindex{iff}
-\ttindex{IF\_then\_else}
-\begin{coq_example*}
-Inductive or (A B:Prop) : Prop :=
-  | or_introl (_:A)
-  | or_intror (_:B).
-Definition iff (P Q:Prop) := (P -> Q) /\ (Q -> P).
-Definition IF_then_else (P Q R:Prop) := P /\ Q \/ ~ P /\ R.
-\end{coq_example*}
-
-\subsubsection[Quantifiers]{Quantifiers\label{Quantifiers}
-\index{Quantifiers}}
-
-Then we find first-order quantifiers:
-\ttindex{all}
-\ttindex{ex}
-\ttindex{exists}
-\ttindex{ex\_intro}
-\ttindex{ex2}
-\ttindex{exists2}
-\ttindex{ex\_intro2}
-
-\begin{coq_example*}
-Definition all (A:Set) (P:A -> Prop) := forall x:A, P x.
-Inductive ex (A: Set) (P:A -> Prop) : Prop :=
-    ex_intro (x:A) (_:P x).
-Inductive ex2 (A:Set) (P Q:A -> Prop) : Prop :=
-    ex_intro2 (x:A) (_:P x) (_:Q x).
-\end{coq_example*}
-
-The following abbreviations are allowed:
-\begin{center}
-  \begin{tabular}[h]{|l|l|}
-    \hline
-    \verb+exists x:A, P+     & \verb+ex A (fun x:A => P)+ \\
-    \verb+exists x, P+       & \verb+ex _ (fun x => P)+ \\
-    \verb+exists2 x:A, P & Q+ & \verb+ex2 A (fun x:A => P) (fun x:A => Q)+ \\
-    \verb+exists2 x, P & Q+   & \verb+ex2 _ (fun x => P) (fun x => Q)+ \\
-    \hline
-  \end{tabular}
-\end{center}
-
-The type annotation ``\texttt{:A}'' can be omitted when \texttt{A} can be
-synthesized by the system.
-
-\subsubsection[Equality]{Equality\label{Equality}
-\index{Equality}}
-
-Then, we find equality, defined as an inductive relation. That is,
-given a type \verb:A: and an \verb:x: of type \verb:A:, the
-predicate \verb:(eq A x): is the smallest one which contains \verb:x:.
-This definition, due to Christine Paulin-Mohring, is equivalent to
-define \verb:eq: as the smallest reflexive relation, and it is also
-equivalent to Leibniz' equality.
-
-\ttindex{eq}
-\ttindex{eq\_refl}
-
-\begin{coq_example*}
-Inductive eq (A:Type) (x:A) : A -> Prop :=
-    eq_refl : eq A x x.
-\end{coq_example*}
-
-\subsubsection[Lemmas]{Lemmas\label{PreludeLemmas}}
-
-Finally, a few easy lemmas are provided.
-
-\ttindex{absurd}
-
-\begin{coq_example*}
-Theorem absurd : forall A C:Prop, A -> ~ A -> C.
-\end{coq_example*}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-\ttindex{eq\_sym}
-\ttindex{eq\_trans}
-\ttindex{f\_equal}
-\ttindex{sym\_not\_eq}
-\begin{coq_example*}
-Section equality.
-Variables A B : Type.
-Variable f : A -> B.
-Variables x y z : A.
-Theorem eq_sym : x = y -> y = x.
-Theorem eq_trans : x = y -> y = z -> x = z.
-Theorem f_equal : x = y -> f x = f y.
-Theorem not_eq_sym : x <> y -> y <> x.
-\end{coq_example*}
-\begin{coq_eval}
-Abort.
-Abort.
-Abort.
-Abort.
-\end{coq_eval}
-\ttindex{eq\_ind\_r}
-\ttindex{eq\_rec\_r}
-\ttindex{eq\_rect}
-\ttindex{eq\_rect\_r}
-%Definition eq_rect: (A:Set)(x:A)(P:A->Type)(P x)->(y:A)(x=y)->(P y).
-\begin{coq_example*}
-End equality.
-Definition eq_ind_r :
-  forall (A:Type) (x:A) (P:A->Prop), P x -> forall y:A, y = x -> P y.
-Definition eq_rec_r :
-  forall (A:Type) (x:A) (P:A->Set), P x -> forall y:A, y = x -> P y.
-Definition eq_rect_r :
-  forall (A:Type) (x:A) (P:A->Type), P x -> forall y:A, y = x -> P y.
-\end{coq_example*}
-\begin{coq_eval}
-Abort.
-Abort.
-Abort.
-\end{coq_eval}
-%Abort (for now predefined eq_rect)
-\begin{coq_example*}
-Hint Immediate eq_sym not_eq_sym : core.
-\end{coq_example*}
-\ttindex{f\_equal$i$}
-
-The theorem {\tt f\_equal} is extended to functions with two to five
-arguments. The theorem are names {\tt f\_equal2}, {\tt f\_equal3}, 
-{\tt f\_equal4} and {\tt f\_equal5}.
-For instance {\tt f\_equal3} is defined the following way.
-\begin{coq_example*}
-Theorem f_equal3 :
- forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B)
-   (x1 y1:A1) (x2 y2:A2) (x3 y3:A3),
-   x1 = y1 -> x2 = y2 -> x3 = y3 -> f x1 x2 x3 = f y1 y2 y3.
-\end{coq_example*}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-\subsection[Datatypes]{Datatypes\label{Datatypes}
-\index{Datatypes}}
-
-\begin{figure}
-\begin{centerframe}
-\begin{tabular}{rclr}
-{\specif} & ::= & {\specif} {\tt *} {\specif} & ({\tt prod})\\
-  & $|$ & {\specif} {\tt +} {\specif} & ({\tt sum})\\
-  & $|$ & {\specif} {\tt + \{} {\specif} {\tt \}} & ({\tt sumor})\\
-  & $|$ & {\tt \{} {\specif} {\tt \} + \{} {\specif} {\tt \}} &
-  ({\tt sumbool})\\  
-  & $|$ & {\tt \{} {\ident} {\tt :} {\specif} {\tt |} {\form} {\tt \}}
-  & ({\tt sig})\\
-  & $|$ & {\tt \{} {\ident} {\tt :} {\specif} {\tt |} {\form}  {\tt \&}
-  {\form} {\tt \}} & ({\tt sig2})\\
-  & $|$ & {\tt \{} {\ident} {\tt :} {\specif} {\tt \&} {\specif} {\tt
-    \}} & ({\tt sigT})\\
-  & $|$ & {\tt \{} {\ident} {\tt :} {\specif} {\tt \&} {\specif} {\tt
-    \&} {\specif} {\tt \}} & ({\tt sigT2})\\
-  &  & & \\
-{\term} & ::= & {\tt (} {\term} {\tt ,} {\term} {\tt )} & ({\tt pair})
-\end{tabular}
-\end{centerframe}
-\caption{Syntax of data-types and specifications}
-\label{specif-syntax}
-\end{figure}
-
-
-In the basic library, we find the definition\footnote{They are in {\tt
-    Datatypes.v}} of the basic data-types of programming, again
-defined as inductive constructions over the sort \verb:Set:. Some of
-them come with a special syntax shown on Figure~\ref{specif-syntax}.
-
-\subsubsection[Programming]{Programming\label{Programming}
-\index{Programming}
-\label{libnats}
-\ttindex{unit}
-\ttindex{tt}
-\ttindex{bool}
-\ttindex{true}
-\ttindex{false}
-\ttindex{nat}
-\ttindex{O}
-\ttindex{S}
-\ttindex{option}
-\ttindex{Some}
-\ttindex{None}
-\ttindex{identity}
-\ttindex{refl\_identity}}
-
-\begin{coq_example*}
-Inductive unit : Set := tt.
-Inductive bool : Set := true | false.
-Inductive nat : Set := O | S (n:nat).
-Inductive option (A:Set) : Set := Some (_:A) | None.
-Inductive identity (A:Type) (a:A) : A -> Type :=
-    refl_identity : identity A a a.
-\end{coq_example*}
-
-Note that zero is the letter \verb:O:, and {\sl not} the numeral
-\verb:0:.
-
-The predicate {\tt identity} is logically 
-equivalent to equality but it lives in sort {\tt
-  Type}. It is mainly maintained for compatibility.
-
-We then define the disjoint sum of \verb:A+B: of two sets \verb:A: and
-\verb:B:, and their product \verb:A*B:.
-\ttindex{sum}
-\ttindex{A+B}
-\ttindex{+}
-\ttindex{inl}
-\ttindex{inr}
-\ttindex{prod}
-\ttindex{A*B}
-\ttindex{*}
-\ttindex{pair}
-\ttindex{fst}
-\ttindex{snd}
-
-\begin{coq_example*}
-Inductive sum (A B:Set) : Set := inl (_:A) | inr (_:B).
-Inductive prod (A B:Set) : Set := pair (_:A) (_:B).
-Section projections.
-Variables A B : Set.
-Definition fst (H: prod A B) := match H with
-                                | pair _ _ x y => x
-                                end.
-Definition snd (H: prod A B) := match H with
-                                | pair _ _ x y => y
-                                end.
-End projections.
-\end{coq_example*}
-
-Some operations on {\tt bool} are also provided: {\tt andb} (with
-infix notation {\tt \&\&}), {\tt orb} (with
-infix notation {\tt ||}), {\tt xorb}, {\tt implb} and {\tt negb}.
-
-\subsection{Specification}
-
-The following notions\footnote{They are defined in module {\tt
-Specif.v}} allow to build new data-types and specifications. 
-They are available with the syntax shown on
-Figure~\ref{specif-syntax}.
-
-For instance, given \verb|A:Type| and \verb|P:A->Prop|, the construct
-\verb+{x:A | P x}+ (in abstract syntax \verb+(sig A P)+) is a
-\verb:Type:. We may build elements of this set as \verb:(exist x p):
-whenever we have a witness \verb|x:A| with its justification
-\verb|p:P x|.
-
-From such a \verb:(exist x p): we may in turn extract its witness
-\verb|x:A| (using an elimination construct such as \verb:match:) but
-{\sl not} its justification, which stays hidden, like in an abstract
-data-type. In technical terms, one says that \verb:sig: is a ``weak
-(dependent) sum''.  A variant \verb:sig2: with two predicates is also
-provided.
-
-\ttindex{\{x:A $\mid$ (P x)\}}
-\ttindex{sig}
-\ttindex{exist}
-\ttindex{sig2}
-\ttindex{exist2}
-
-\begin{coq_example*}
-Inductive sig (A:Set) (P:A -> Prop) : Set := exist (x:A) (_:P x).
-Inductive sig2 (A:Set) (P Q:A -> Prop) : Set := 
-  exist2 (x:A) (_:P x) (_:Q x).
-\end{coq_example*}
-
-A ``strong (dependent) sum'' \verb+{x:A & P x}+ may be also defined,
-when the predicate \verb:P: is now defined as a 
-constructor of types in \verb:Type:.
-
-\ttindex{\{x:A \& (P x)\}}
-\ttindex{\&}
-\ttindex{sigT}
-\ttindex{existT}
-\ttindex{projT1}
-\ttindex{projT2}
-\ttindex{sigT2}
-\ttindex{existT2}
-
-\begin{coq_example*}
-Inductive sigT (A:Type) (P:A -> Type) : Type := existT (x:A) (_:P x).
-Section Projections2.
-Variable A : Type.
-Variable P : A -> Type.
-Definition projT1 (H:sigT A P) := let (x, h) := H in x.
-Definition projT2 (H:sigT A P) :=
-  match H return P (projT1 H) with
-    existT _ _ x h => h
-  end.
-End Projections2.
-Inductive sigT2 (A: Type) (P Q:A -> Type) : Type :=
-    existT2 (x:A) (_:P x) (_:Q x).
-\end{coq_example*}
-
-A related non-dependent construct is the constructive sum
-\verb"{A}+{B}" of two propositions \verb:A: and \verb:B:.
-\label{sumbool}
-\ttindex{sumbool}
-\ttindex{left}
-\ttindex{right}
-\ttindex{\{A\}+\{B\}}
-
-\begin{coq_example*}
-Inductive sumbool (A B:Prop) : Set := left (_:A) | right (_:B).
-\end{coq_example*}
-
-This \verb"sumbool" construct may be used as a kind of indexed boolean
-data-type. An intermediate between \verb"sumbool" and \verb"sum" is
-the mixed \verb"sumor" which combines \verb"A:Set" and \verb"B:Prop"
-in the \verb"Set" \verb"A+{B}".
-\ttindex{sumor}
-\ttindex{inleft}
-\ttindex{inright}
-\ttindex{A+\{B\}}
-
-\begin{coq_example*}
-Inductive sumor (A:Set) (B:Prop) : Set :=
-| inleft (_:A)
-| inright (_:B).
-\end{coq_example*}
-
-We may define variants of the axiom of choice, like in Martin-Löf's
-Intuitionistic Type Theory.
-\ttindex{Choice}
-\ttindex{Choice2}
-\ttindex{bool\_choice}
-
-\begin{coq_example*}
-Lemma Choice :
- forall (S S':Set) (R:S -> S' -> Prop),
-   (forall x:S, {y : S' | R x y}) ->
-   {f : S -> S' | forall z:S, R z (f z)}.
-Lemma Choice2 :
- forall (S S':Set) (R:S -> S' -> Set),
-   (forall x:S, {y : S' &  R x y}) ->
-   {f : S -> S' &  forall z:S, R z (f z)}.
-Lemma bool_choice :
- forall (S:Set) (R1 R2:S -> Prop),
-   (forall x:S, {R1 x} + {R2 x}) ->
-   {f : S -> bool |
-   forall x:S, f x = true /\ R1 x \/ f x = false /\ R2 x}.
-\end{coq_example*}
-\begin{coq_eval}
-Abort.
-Abort.
-Abort.
-\end{coq_eval}
-
-The next construct builds a sum between a data-type \verb|A:Type| and
-an exceptional value encoding errors:
-
-\ttindex{Exc}
-\ttindex{value}
-\ttindex{error}
-
-\begin{coq_example*}
-Definition Exc := option.
-Definition value := Some.
-Definition error := None.
-\end{coq_example*}
-
-
-This module ends with theorems, 
-relating the sorts \verb:Set: or \verb:Type: and
-\verb:Prop: in a way which is consistent with the realizability
-interpretation.
-\ttindex{False\_rect}
-\ttindex{False\_rec}
-\ttindex{eq\_rect}
-\ttindex{absurd\_set}
-\ttindex{and\_rect}
-
-\begin{coq_example*}
-Definition except := False_rec.
-Theorem absurd_set : forall (A:Prop) (C:Set), A -> ~ A -> C.
-Theorem and_rect2 :
- forall (A B:Prop) (P:Type), (A -> B -> P) -> A /\ B -> P.
-\end{coq_example*}
-%\begin{coq_eval}
-%Abort.
-%Abort.
-%\end{coq_eval}
-
-\subsection{Basic Arithmetics}
-
-The basic library includes a few elementary properties of natural
-numbers, together with the definitions of predecessor, addition and
-multiplication\footnote{This is in module {\tt Peano.v}}. It also
-provides a scope {\tt nat\_scope} gathering standard notations for
-common operations (+, *) and a decimal notation for numbers. That is he
-can write \texttt{3} for \texttt{(S (S (S O)))}. This also works on
-the left hand side of a \texttt{match} expression (see for example
-section~\ref{refine-example}). This scope is opened by default.
-
-%Remove the redefinition of nat
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-
-The following example is not part of the standard library, but it
-shows the usage of the notations:
-
-\begin{coq_example*}
-Fixpoint even (n:nat) : bool :=
-  match n with
-  | 0 => true
-  | 1 => false
-  | S (S n) => even n
-  end.
-\end{coq_example*}
-
-
-\ttindex{eq\_S}
-\ttindex{pred}
-\ttindex{pred\_Sn}
-\ttindex{eq\_add\_S}
-\ttindex{not\_eq\_S}
-\ttindex{IsSucc}
-\ttindex{O\_S}
-\ttindex{n\_Sn}
-\ttindex{plus}
-\ttindex{plus\_n\_O}
-\ttindex{plus\_n\_Sm}
-\ttindex{mult}
-\ttindex{mult\_n\_O}
-\ttindex{mult\_n\_Sm}
-
-\begin{coq_example*}
-Theorem eq_S : forall x y:nat, x = y -> S x = S y.
-\end{coq_example*}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-\begin{coq_example*}
-Definition pred (n:nat) : nat :=
-  match n with
-  | 0 => 0
-  | S u => u
-  end.
-Theorem pred_Sn : forall m:nat, m = pred (S m).
-Theorem eq_add_S : forall n m:nat, S n = S m -> n = m.
-Hint Immediate eq_add_S : core.
-Theorem not_eq_S : forall n m:nat, n <> m -> S n <> S m.
-\end{coq_example*}
-\begin{coq_eval}
-Abort All.
-\end{coq_eval}
-\begin{coq_example*}
-Definition IsSucc (n:nat) : Prop :=
-  match n with
-  | 0 => False
-  | S p => True
-  end.
-Theorem O_S : forall n:nat, 0 <> S n.
-Theorem n_Sn : forall n:nat, n <> S n.
-\end{coq_example*}
-\begin{coq_eval}
-Abort All.
-\end{coq_eval}
-\begin{coq_example*}
-Fixpoint plus (n m:nat) {struct n} : nat :=
-  match n with
-  | 0 => m
-  | S p => S (p + m)
-  end
-where "n + m" := (plus n m) : nat_scope.
-Lemma plus_n_O : forall n:nat, n = n + 0.
-Lemma plus_n_Sm : forall n m:nat, S (n + m) = n + S m.
-\end{coq_example*}
-\begin{coq_eval}
-Abort All.
-\end{coq_eval}
-\begin{coq_example*}
-Fixpoint mult (n m:nat) {struct n} : nat :=
-  match n with
-  | 0 => 0
-  | S p => m + p * m
-  end
-where "n * m" := (mult n m) : nat_scope.
-Lemma mult_n_O : forall n:nat, 0 = n * 0.
-Lemma mult_n_Sm : forall n m:nat, n * m + n = n * (S m).
-\end{coq_example*}
-\begin{coq_eval}
-Abort All.
-\end{coq_eval}
-
-Finally, it gives the definition of the usual orderings \verb:le:,
-\verb:lt:, \verb:ge:, and \verb:gt:.
-\ttindex{le}
-\ttindex{le\_n}
-\ttindex{le\_S}
-\ttindex{lt}
-\ttindex{ge}
-\ttindex{gt}
-
-\begin{coq_example*}
-Inductive le (n:nat) : nat -> Prop :=
-  | le_n : le n n
-  | le_S : forall m:nat, n <= m -> n <= (S m)
-where "n <= m" := (le n m) : nat_scope.
-Definition lt (n m:nat) := S n <= m.
-Definition ge (n m:nat) := m <= n.
-Definition gt (n m:nat) := m < n.
-\end{coq_example*}
-
-Properties of these relations are not initially known, but may be
-required by the user from modules \verb:Le: and \verb:Lt:.  Finally,
-\verb:Peano: gives some lemmas allowing pattern-matching, and a double
-induction principle.
-
-\ttindex{nat\_case}
-\ttindex{nat\_double\_ind}
-
-\begin{coq_example*}
-Theorem nat_case :
- forall (n:nat) (P:nat -> Prop), 
- P 0 -> (forall m:nat, P (S m)) -> P n.
-\end{coq_example*}
-\begin{coq_eval}
-Abort All.
-\end{coq_eval}
-\begin{coq_example*}
-Theorem nat_double_ind :
- forall R:nat -> nat -> Prop,
-   (forall n:nat, R 0 n) ->
-   (forall n:nat, R (S n) 0) ->
-   (forall n m:nat, R n m -> R (S n) (S m)) -> forall n m:nat, R n m.
-\end{coq_example*}
-\begin{coq_eval}
-Abort All.
-\end{coq_eval}
-
-\subsection{Well-founded recursion}
-
-The basic library contains the basics of well-founded recursion and 
-well-founded induction\footnote{This is defined in module {\tt Wf.v}}.
-\index{Well foundedness}
-\index{Recursion}
-\index{Well founded induction}
-\ttindex{Acc}
-\ttindex{Acc\_inv}
-\ttindex{Acc\_rect}
-\ttindex{well\_founded}
-
-\begin{coq_example*}
-Section Well_founded.
-Variable A : Type.
-Variable R : A -> A -> Prop.
-Inductive Acc (x:A) : Prop :=
-    Acc_intro : (forall y:A, R y x -> Acc y) -> Acc x.
-Lemma Acc_inv x : Acc x -> forall y:A, R y x -> Acc y.
-\end{coq_example*}
-\begin{coq_eval}
-destruct 1; trivial.
-Defined.
-\end{coq_eval}
-%% Acc_rect now primitively defined
-%% Section AccRec.
-%% Variable P : A -> Set.
-%% Variable F :
-%%     forall x:A,
-%%       (forall y:A, R y x -> Acc y) -> (forall y:A, R y x -> P y) -> P x.
-%% Fixpoint Acc_rec (x:A) (a:Acc x) {struct a} : P x :=
-%%   F x (Acc_inv x a)
-%%     (fun (y:A) (h:R y x) => Acc_rec y (Acc_inv x a y h)).
-%% End AccRec.
-\begin{coq_example*}
-Definition well_founded := forall a:A, Acc a.
-Hypothesis Rwf : well_founded.
-Theorem well_founded_induction :
- forall P:A -> Set,
-   (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a.
-Theorem well_founded_ind :
- forall P:A -> Prop,
-   (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a.
-\end{coq_example*}
-\begin{coq_eval}
-Abort All.
-\end{coq_eval}
-The automatically generated scheme {\tt 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.
-\ttindex{Fix\_F}
-\ttindex{fix\_eq}
-\ttindex{Fix\_F\_inv}
-\ttindex{Fix\_F\_eq}
-\begin{coq_example*}
-Section FixPoint.
-Variable P : A -> Type.
-Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x.
-Fixpoint Fix_F (x:A) (r:Acc x) {struct r} : P x :=
-  F x (fun (y:A) (p:R y x) => Fix_F y (Acc_inv x r y p)).
-Definition Fix (x:A) := Fix_F x (Rwf x).
-Hypothesis F_ext :
-    forall (x:A) (f g:forall y:A, R y x -> P y),
-      (forall (y:A) (p:R y x), f y p = g y p) -> F x f = F x g.
-Lemma Fix_F_eq :
- forall (x:A) (r:Acc x),
-   F x (fun (y:A) (p:R y x) => Fix_F y (Acc_inv x r y p)) = Fix_F x r.
-Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F x r = Fix_F x s.
-Lemma fix_eq : forall x:A, Fix x = F x (fun (y:A) (p:R y x) => Fix y).
-\end{coq_example*}
-\begin{coq_eval}
-Abort All.
-\end{coq_eval}
-\begin{coq_example*}
-End FixPoint.
-End Well_founded.
-\end{coq_example*}
-
-\subsection{Accessing the {\Type} level}
-
-The basic library includes the definitions\footnote{This is in module
-{\tt Logic\_Type.v}} of the counterparts of some data-types and logical
-quantifiers at the \verb:Type: level: negation, pair, and properties
-of {\tt identity}.
-
-\ttindex{notT}
-\ttindex{prodT}
-\ttindex{pairT}
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-\begin{coq_example*}
-Definition notT (A:Type) := A -> False.
-Inductive prodT (A B:Type) : Type := pairT (_:A) (_:B).
-\end{coq_example*}
-
-At the end, it defines data-types at the {\Type} level.
-
-\subsection{Tactics}
-
-A few tactics defined at the user level are provided in the initial
-state\footnote{This is in module {\tt Tactics.v}}. They are listed at
-\url{http://coq.inria.fr/stdlib} (paragraph {\tt Init}, link {\tt
-  Tactics}).
-
-\section{The standard library}
-
-\subsection{Survey}
-
-The rest of the standard library is structured into the following 
-subdirectories:
-
-\begin{tabular}{lp{12cm}}
-  {\bf Logic}   & Classical logic and dependent equality \\
-  {\bf Arith}   & Basic Peano arithmetic \\
-  {\bf PArith}  & Basic positive integer arithmetic \\
-  {\bf NArith}  & Basic binary natural number arithmetic \\
-  {\bf ZArith}  & Basic relative integer arithmetic \\
-  {\bf Numbers} & Various approaches to natural, integer and cyclic numbers (currently axiomatically and on top of 2$^{31}$ binary words) \\
-  {\bf Bool}    & Booleans (basic functions and results) \\
-  {\bf Lists}   & Monomorphic and polymorphic lists (basic functions and
-            results), Streams (infinite sequences defined with co-inductive
-            types) \\
-  {\bf Sets}    & Sets (classical, constructive, finite, infinite, power set,
-            etc.) \\
-  {\bf FSets}   & Specification and implementations of finite sets and finite
-                  maps (by lists and by AVL trees)\\
- {\bf Reals}    & Axiomatization of real numbers (classical, basic functions, 
-                  integer part, fractional part, limit, derivative, Cauchy 
-                  series, power series and results,...)\\
- {\bf Relations} & Relations (definitions and basic results) \\
- {\bf Sorting}  & Sorted list (basic definitions and heapsort correctness) \\
- {\bf Strings}  & 8-bits characters and strings\\
- {\bf Wellfounded} & Well-founded relations (basic results) \\
-
-\end{tabular}
-\medskip
-
-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 \verb!Require! (see
-Chapter~\ref{Other-commands}). 
-
-The different modules of the \Coq\ standard library are described in the
-additional document \verb!Library.dvi!. They are also accessible on the WWW
-through the \Coq\ homepage
-\footnote{\url{http://coq.inria.fr}}.
-
-\subsection[Notations for integer arithmetics]{Notations for integer arithmetics\index{Arithmetical notations}}
-
-On Figure~\ref{zarith-syntax} is described the syntax of expressions
-for integer arithmetics. It is provided by requiring and opening the
-module {\tt ZArith} and opening scope {\tt Z\_scope}.
-
-\ttindex{+}
-\ttindex{*}
-\ttindex{-}
-\ttindex{/}
-\ttindex{<=}
-\ttindex{>=}
-\ttindex{<}
-\ttindex{>}
-\ttindex{?=}
-\ttindex{mod}
-
-\begin{figure}
-\begin{center}
-\begin{tabular}{l|l|l|l}
-Notation & Interpretation & Precedence & Associativity\\
-\hline
-\verb!_ < _! & {\tt Z.lt} &&\\
-\verb!x <= y! & {\tt Z.le} &&\\
-\verb!_ > _! & {\tt Z.gt} &&\\
-\verb!x >= y! & {\tt Z.ge} &&\\
-\verb!x < y < z! & {\tt x < y \verb!/\! y < z} &&\\
-\verb!x < y <= z! & {\tt x < y \verb!/\! y <= z} &&\\
-\verb!x <= y < z! & {\tt x <= y \verb!/\! y < z} &&\\
-\verb!x <= y <= z! & {\tt x <= y \verb!/\! y <= z} &&\\
-\verb!_ ?= _! & {\tt Z.compare} & 70 & no\\
-\verb!_ + _! & {\tt Z.add} &&\\
-\verb!_ - _! & {\tt Z.sub} &&\\
-\verb!_ * _! & {\tt Z.mul} &&\\
-\verb!_ / _! & {\tt Z.div} &&\\
-\verb!_ mod _! & {\tt Z.modulo} & 40 & no \\
-\verb!- _!  & {\tt Z.opp} &&\\
-\verb!_ ^ _! & {\tt Z.pow} &&\\
-\end{tabular}
-\end{center}
-\caption{Definition of the scope for integer arithmetics ({\tt Z\_scope})}
-\label{zarith-syntax}
-\end{figure}
-
-Figure~\ref{zarith-syntax} shows the notations provided by {\tt
-Z\_scope}. It specifies how notations are interpreted and, when not
-already reserved, the precedence and associativity.
-
-\begin{coq_example*}
-Require Import ZArith.
-\end{coq_example*}
-\begin{coq_example}
-Check  (2 + 3)%Z.
-Open Scope Z_scope.
-Check 2 + 3.
-\end{coq_example}
-
-\subsection[Peano's arithmetic (\texttt{nat})]{Peano's arithmetic (\texttt{nat})\index{Peano's arithmetic}
-\ttindex{nat\_scope}}
-
-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 {\tt Arith}.
-
-Figure~\ref{nat-syntax} describes notation available in scope {\tt
-nat\_scope}.
-
-\begin{figure}
-\begin{center}
-\begin{tabular}{l|l}
-Notation & Interpretation \\
-\hline
-\verb!_ < _! & {\tt lt} \\
-\verb!x <= y! & {\tt le} \\
-\verb!_ > _! & {\tt gt} \\
-\verb!x >= y! & {\tt ge} \\
-\verb!x < y < z! & {\tt x < y \verb!/\! y < z} \\
-\verb!x < y <= z! & {\tt x < y \verb!/\! y <= z} \\
-\verb!x <= y < z! & {\tt x <= y \verb!/\! y < z} \\
-\verb!x <= y <= z! & {\tt x <= y \verb!/\! y <= z} \\
-\verb!_ + _! & {\tt plus} \\
-\verb!_ - _! & {\tt minus} \\
-\verb!_ * _! & {\tt mult} \\
-\end{tabular}
-\end{center}
-\caption{Definition of the scope for natural numbers ({\tt nat\_scope})}
-\label{nat-syntax}
-\end{figure}
-
-\subsection{Real numbers library}
-
-\subsubsection[Notations for real numbers]{Notations for real numbers\index{Notations for real numbers}}
-
-This is provided by requiring and opening the module {\tt Reals} and
-opening scope {\tt R\_scope}. This set of notations is very similar to
-the notation for integer arithmetics. The inverse function was added.
-\begin{figure}
-\begin{center}
-\begin{tabular}{l|l}
-Notation & Interpretation \\
-\hline
-\verb!_ < _! & {\tt Rlt} \\
-\verb!x <= y! & {\tt Rle} \\
-\verb!_ > _! & {\tt Rgt} \\
-\verb!x >= y! & {\tt Rge} \\
-\verb!x < y < z! & {\tt x < y \verb!/\! y < z} \\
-\verb!x < y <= z! & {\tt x < y \verb!/\! y <= z} \\
-\verb!x <= y < z! & {\tt x <= y \verb!/\! y < z} \\
-\verb!x <= y <= z! & {\tt x <= y \verb!/\! y <= z} \\
-\verb!_ + _! & {\tt Rplus} \\
-\verb!_ - _! & {\tt Rminus} \\
-\verb!_ * _! & {\tt Rmult} \\
-\verb!_ / _! & {\tt Rdiv} \\
-\verb!- _!  & {\tt Ropp} \\
-\verb!/ _!  & {\tt Rinv} \\
-\verb!_ ^ _! & {\tt pow} \\
-\end{tabular}
-\end{center}
-\label{reals-syntax}
-\caption{Definition of the scope for real arithmetics ({\tt R\_scope})}
-\end{figure}
-
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-\begin{coq_example*}
-Require Import Reals.
-\end{coq_example*}
-\begin{coq_example}
-Check  (2 + 3)%R.
-Open Scope R_scope.
-Check 2 + 3.
-\end{coq_example}
-
-\subsubsection{Some tactics}
-
-In addition to the \verb|ring|, \verb|field| and \verb|fourier|
-tactics (see Chapter~\ref{Tactics}) there are:
-\begin{itemize}
-\item {\tt discrR} \tacindex{discrR}
-  
-  Proves that a real integer constant $c_1$ is different from another
-  real integer constant $c_2$.  
-
-\begin{coq_example*}
-Require Import DiscrR.
-Goal 5 <> 0.
-\end{coq_example*}
-
-\begin{coq_example}
-discrR.
-\end{coq_example}
-
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-\item {\tt split\_Rabs} allows unfolding the {\tt Rabs} constant and splits 
-corresponding conjunctions.
-\tacindex{split\_Rabs}
-
-\begin{coq_example*}
-Require Import SplitAbsolu.
-Goal forall x:R, x <= Rabs x.
-\end{coq_example*}
-
-\begin{coq_example}
-intro; split_Rabs.
-\end{coq_example}
-
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-\item {\tt split\_Rmult} splits a condition that a product is
-  non null into subgoals corresponding to the condition on each
-  operand of the product. 
-\tacindex{split\_Rmult}
-
-\begin{coq_example*}
-Require Import SplitRmult.
-Goal forall x y z:R, x * y * z <> 0.
-\end{coq_example*}
-
-\begin{coq_example}
-intros; split_Rmult.
-\end{coq_example}
-
-\end{itemize}
-
-These tactics has been written with the tactic language Ltac
-described in Chapter~\ref{TacticLanguage}.
-
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-
-\subsection[List library]{List library\index{Notations for lists}
-\ttindex{length}
-\ttindex{head}
-\ttindex{tail}
-\ttindex{app}
-\ttindex{rev}
-\ttindex{nth}
-\ttindex{map}
-\ttindex{flat\_map}
-\ttindex{fold\_left}
-\ttindex{fold\_right}}
-
-Some elementary operations on polymorphic lists are defined here. They
-can be accessed by requiring module {\tt List}.
-
-It defines the following notions:
-\begin{center}
-\begin{tabular}{l|l}
-\hline
-{\tt length} & length \\
-{\tt head} & first element (with default) \\
-{\tt tail} & all but first element \\
-{\tt app} & concatenation \\
-{\tt rev} & reverse \\
-{\tt nth} & accessing $n$-th element (with default) \\
-{\tt map} & applying a function \\
-{\tt flat\_map} & applying a function returning lists \\
-{\tt fold\_left} & iterator (from head to tail) \\
-{\tt fold\_right} & iterator (from tail to head) \\
-\hline
-\end{tabular}
-\end{center}
-
-Table show notations available when opening scope {\tt list\_scope}.
-
-\begin{figure}
-\begin{center}
-\begin{tabular}{l|l|l|l}
-Notation & Interpretation & Precedence & Associativity\\
-\hline
-\verb!_ ++ _! & {\tt app} & 60 & right \\
-\verb!_ :: _! & {\tt cons} & 60 & right \\
-\end{tabular}
-\end{center}
-\label{list-syntax}
-\caption{Definition of the scope for lists ({\tt list\_scope})}
-\end{figure}
-
-
-\section[Users' contributions]{Users' contributions\index{Contributions}
-\label{Contributions}}
-
-Numerous users' contributions have been collected and are available at
-URL \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.
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "Reference-Manual"
-%%% End: 
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index a6a3670bd..5122b2a36 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -95,7 +95,6 @@ Options A and B of the licence are {\em not} elected.}
 \defaultheaders
 %END LATEX
 \include{RefMan-gal.v}% Gallina
-\include{RefMan-lib.v}% The coq library
 
 
 \part{The proof engine}
diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst
index 84c670175..b3f160df1 100644
--- a/doc/sphinx/index.rst
+++ b/doc/sphinx/index.rst
@@ -17,6 +17,7 @@ Table of contents
    :caption: The language
 
    language/gallina-extensions
+   language/coq-library
    language/cic
    language/module-system
 
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
new file mode 100644
index 000000000..29053d6a5
--- /dev/null
+++ b/doc/sphinx/language/coq-library.rst
@@ -0,0 +1,988 @@
+.. include:: ../replaces.rst
+
+.. _thecoqlibrary:
+
+The |Coq| library
+=================
+
+:Source: https://coq.inria.fr/distrib/current/refman/stdlib.html
+:Converted by: Pierre Letouzey
+
+.. index::
+   single: Theories
+
+
+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 :ref:`TODO-6.5.1-Require`);
+
+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 :ref:`userscontributions`).
+
+This chapter briefly reviews the |Coq| libraries whose contents can
+also be browsed at http://coq.inria.fr/stdlib.
+
+
+
+
+The basic library
+-----------------
+
+This section lists the basic notions and results which are directly
+available in the standard |Coq| system. 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.
+
+
+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 :
+
+================  ============  ===============
+Notation          Precedence    Associativity
+================  ============  ===============
+``_ -> _``        99            right
+``_ <-> _``       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
+================  ============  ===============
+
+Logic
+~~~~~
+
+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 of `form`
+is shown below:
+
+.. /!\ Please keep the blanks in the lines below, experimentally they produce
+   a nice last column. Or even better, find a proper way to do this!
+
+.. productionlist::
+   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)
+
+.. note::
+
+  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
++++++++++++++++++++++++++
+
+.. index::
+  single: Connectives
+  single: True (term)
+  single: I (term)
+  single: False (term)
+  single: not (term)
+  single: and (term)
+  single: conj (term)
+  single: proj1 (term)
+  single: proj2 (term)
+  single: or (term)
+  single: or_introl (term)
+  single: or_intror (term)
+  single: iff (term)
+  single: IF_then_else (term)
+
+First, we find propositional calculus connectives:
+
+.. coqtop:: in
+
+  Inductive True : Prop := I.
+  Inductive False :  Prop := .
+  Definition not (A: Prop) := A -> False.
+  Inductive and (A B:Prop) : Prop := conj (_:A) (_:B).
+  Section Projections.
+   Variables A B : Prop.
+   Theorem proj1 : A /\ B -> A.
+   Theorem proj2 : A /\ B -> B.
+  End Projections.
+  Inductive or (A B:Prop) : Prop :=
+  | or_introl (_:A)
+  | or_intror (_:B).
+  Definition iff (P Q:Prop) := (P -> Q) /\ (Q -> P).
+  Definition IF_then_else (P Q R:Prop) := P /\ Q \/ ~ P /\ R.
+
+Quantifiers
++++++++++++
+
+.. index::
+  single: Quantifiers
+  single: all (term)
+  single: ex (term)
+  single: exists (term)
+  single: ex_intro (term)
+  single: ex2 (term)
+  single: exists2 (term)
+  single: ex_intro2 (term)
+
+Then we find first-order quantifiers:
+
+.. coqtop:: in
+  
+   Definition all (A:Set) (P:A -> Prop) := forall x:A, P x.
+   Inductive ex (A: Set) (P:A -> Prop) : Prop :=
+    ex_intro (x:A) (_:P x).
+   Inductive ex2 (A:Set) (P Q:A -> Prop) : Prop :=
+    ex_intro2 (x:A) (_:P x) (_:Q x).
+
+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.
+
+Equality
+++++++++
+
+.. index::
+  single: Equality
+  single: eq (term)
+  single: eq_refl (term)
+
+Then, we find equality, defined as an inductive relation. That is,
+given a type ``A`` and an ``x`` of type ``A``, the
+predicate :g:`(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.
+
+.. coqtop:: in
+
+  Inductive eq (A:Type) (x:A) : A -> Prop :=
+    eq_refl : eq A x x.
+
+Lemmas
+++++++
+
+Finally, a few easy lemmas are provided.
+
+.. index::
+  single: absurd (term)
+  single: eq_sym (term)
+  single: eq_trans (term)
+  single: f_equal (term)
+  single: sym_not_eq (term)
+  single: eq_ind_r (term)
+  single: eq_rec_r (term)
+  single: eq_rect (term)
+  single: eq_rect_r (term)
+
+.. coqtop:: in
+
+  Theorem absurd : forall A C:Prop, A -> ~ A -> C.
+  Section equality.
+  Variables A B : Type.
+  Variable f : A -> B.
+  Variables x y z : A.
+  Theorem eq_sym : x = y -> y = x.
+  Theorem eq_trans : x = y -> y = z -> x = z.
+  Theorem f_equal : x = y -> f x = f y.
+  Theorem not_eq_sym : x <> y -> y <> x.
+  End equality.
+  Definition eq_ind_r :
+   forall (A:Type) (x:A) (P:A->Prop), P x -> forall y:A, y = x -> P y.
+  Definition eq_rec_r :
+   forall (A:Type) (x:A) (P:A->Set), P x -> forall y:A, y = x -> P y.
+  Definition eq_rect_r :
+   forall (A:Type) (x:A) (P:A->Type), P x -> forall y:A, y = x -> P y.
+  Hint Immediate eq_sym not_eq_sym : core.
+
+.. index::
+  single: f_equal2 ... f_equal5 (term)
+
+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.
+
+.. coqtop:: in
+  
+  Theorem f_equal3 :
+   forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B)
+     (x1 y1:A1) (x2 y2:A2) (x3 y3:A3),
+     x1 = y1 -> x2 = y2 -> x3 = y3 -> f x1 x2 x3 = f y1 y2 y3.
+
+.. _datatypes:
+
+Datatypes
+~~~~~~~~~
+
+.. index::
+   single: Datatypes
+
+In the basic library, we find in ``Datatypes.v`` the definition
+of the basic data-types of programming,
+defined as inductive constructions over the sort ``Set``. Some of
+them come with a special syntax shown below (this syntax table is common with
+the next section :ref:`specification`):
+
+.. productionlist::
+   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)
+
+
+Programming
++++++++++++
+
+.. index::
+  single: Programming
+  single: unit (term)
+  single: tt (term)
+  single: bool (term)
+  single: true (term)
+  single: false (term)
+  single: nat (term)
+  single: O (term)
+  single: S (term)
+  single: option (term)
+  single: Some (term)
+  single: None (term)
+  single: identity (term)
+  single: refl_identity (term)
+
+.. coqtop:: in
+
+  Inductive unit : Set := tt.
+  Inductive bool : Set := true | false.
+  Inductive nat : Set := O | S (n:nat).
+  Inductive option (A:Set) : Set := Some (_:A) | None.
+  Inductive identity (A:Type) (a:A) : A -> Type :=
+    refl_identity : identity A a a.
+
+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``.
+
+.. index::
+  single: sum (term)
+  single: A+B (term)
+  single: + (term)
+  single: inl (term)
+  single: inr (term)
+  single: prod (term)
+  single: A*B (term)
+  single: * (term)
+  single: pair (term)
+  single: fst (term)
+  single: snd (term)
+
+.. coqtop:: in
+
+  Inductive sum (A B:Set) : Set := inl (_:A) | inr (_:B).
+  Inductive prod (A B:Set) : Set := pair (_:A) (_:B).
+  Section projections.
+  Variables A B : Set.
+  Definition fst (H: prod A B) := match H with
+                                | pair _ _ x y => x
+                                end.
+  Definition snd (H: prod A B) := match H with
+                                | pair _ _ x y => y
+                                end.
+  End projections.
+
+Some operations on ``bool`` are also provided: ``andb`` (with
+infix notation ``&&``), ``orb`` (with
+infix notation ``||``), ``xorb``, ``implb`` and ``negb``.
+
+.. _specification:
+
+Specification
+~~~~~~~~~~~~~
+
+The following notions defined in module ``Specif.v`` allow to build new data-types and specifications. 
+They are available with the syntax shown in the previous section :ref:`datatypes`.
+
+For instance, given :g:`A:Type` and :g:`P:A->Prop`, the construct
+:g:`{x:A | P x}` (in abstract syntax :g:`(sig A P)`) is a
+``Type``. We may build elements of this set as :g:`(exist x p)`
+whenever we have a witness :g:`x:A` with its justification
+:g:`p:P x`.
+
+From such a :g:`(exist x p)` we may in turn extract its witness
+:g:`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.
+
+.. index::
+   single: {x:A | P x} (term)
+   single: sig (term)
+   single: exist (term)
+   single: sig2 (term)
+   single: exist2 (term)
+
+.. coqtop:: in
+
+  Inductive sig (A:Set) (P:A -> Prop) : Set := exist (x:A) (_:P x).
+  Inductive sig2 (A:Set) (P Q:A -> Prop) : Set := 
+    exist2 (x:A) (_:P x) (_:Q x).
+
+A *strong (dependent) sum* :g:`{x:A & P x}` may be also defined,
+when the predicate ``P`` is now defined as a 
+constructor of types in ``Type``.
+
+.. index::
+   single: {x:A & P x} (term)
+   single: sigT (term)
+   single: existT (term)
+   single: sigT2 (term)
+   single: existT2 (term)
+   single: projT1 (term)
+   single: projT2 (term)
+
+.. coqtop:: in
+
+  Inductive sigT (A:Type) (P:A -> Type) : Type := existT (x:A) (_:P x).
+  Section Projections2.
+  Variable A : Type.
+  Variable P : A -> Type.
+  Definition projT1 (H:sigT A P) := let (x, h) := H in x.
+  Definition projT2 (H:sigT A P) :=
+   match H return P (projT1 H) with
+    existT _ _ x h => h
+   end.
+  End Projections2.
+  Inductive sigT2 (A: Type) (P Q:A -> Type) : Type :=
+    existT2 (x:A) (_:P x) (_:Q x).
+
+A related non-dependent construct is the constructive sum
+:g:`{A}+{B}` of two propositions ``A`` and ``B``.
+
+.. index::
+  single: sumbool (term)
+  single: left (term)
+  single: right (term)
+  single: {A}+{B} (term)
+
+.. coqtop:: in
+
+  Inductive sumbool (A B:Prop) : Set := left (_:A) | right (_: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 :g:`A:Set` and :g:`B:Prop`
+in the construction :g:`A+{B}` in ``Set``.
+
+.. index::
+  single: sumor (term)
+  single: inleft (term)
+  single: inright (term)
+  single: A+{B} (term)
+
+.. coqtop:: in
+
+  Inductive sumor (A:Set) (B:Prop) : Set :=
+  | inleft (_:A)
+  | inright (_:B).
+
+We may define variants of the axiom of choice, like in Martin-Löf's
+Intuitionistic Type Theory.
+
+.. index::
+  single: Choice (term)
+  single: Choice2 (term)
+  single: bool_choice (term)
+
+.. coqtop:: in
+
+  Lemma Choice :
+   forall (S S':Set) (R:S -> S' -> Prop),
+    (forall x:S, {y : S' | R x y}) ->
+    {f : S -> S' | forall z:S, R z (f z)}.
+  Lemma Choice2 :
+   forall (S S':Set) (R:S -> S' -> Set),
+    (forall x:S, {y : S' &  R x y}) ->
+     {f : S -> S' &  forall z:S, R z (f z)}.
+  Lemma bool_choice :
+   forall (S:Set) (R1 R2:S -> Prop),
+    (forall x:S, {R1 x} + {R2 x}) ->
+    {f : S -> bool |
+     forall x:S, f x = true /\ R1 x \/ f x = false /\ R2 x}.
+
+The next construct builds a sum between a data-type :g:`A:Type` and
+an exceptional value encoding errors:
+
+.. index::
+  single: Exc (term)
+  single: value (term)
+  single: error (term)
+
+.. coqtop:: in
+
+  Definition Exc := option.
+  Definition value := Some.
+  Definition error := None.
+
+This module ends with theorems, relating the sorts ``Set`` or
+``Type`` and ``Prop`` in a way which is consistent with the
+realizability interpretation.
+
+.. index::
+  single: False_rect (term)
+  single: False_rec (term)
+  single: eq_rect (term)
+  single: absurd_set (term)
+  single: and_rect (term)
+
+.. coqtop:: in
+
+  Definition except := False_rec.
+  Theorem absurd_set : forall (A:Prop) (C:Set), A -> ~ A -> C.
+  Theorem and_rect2 :
+   forall (A B:Prop) (P:Type), (A -> B -> P) -> A /\ B -> P.
+
+
+Basic Arithmetics
+~~~~~~~~~~~~~~~~~
+
+The basic library includes a few elementary properties of natural
+numbers, together with the definitions of predecessor, addition and
+multiplication, in module ``Peano.v``. It also
+provides a scope ``nat_scope`` gathering standard notations for
+common operations (``+``, ``*``) and a decimal notation for
+numbers, allowing for instance to write ``3`` for :g:`S (S (S O)))`. This also works on
+the left hand side of a ``match`` expression (see for example
+section :ref:`TODO-refine-example`). This scope is opened by default.
+
+.. example::
+
+  The following example is not part of the standard library, but it
+  shows the usage of the notations:
+
+  .. coqtop:: in
+
+    Fixpoint even (n:nat) : bool :=
+     match n with
+     | 0 => true
+     | 1 => false
+     | S (S n) => even n
+     end.
+
+.. index::
+  single: eq_S (term)
+  single: pred (term)
+  single: pred_Sn (term)
+  single: eq_add_S (term)
+  single: not_eq_S (term)
+  single: IsSucc (term)
+  single: O_S (term)
+  single: n_Sn (term)
+  single: plus (term)
+  single: plus_n_O (term)
+  single: plus_n_Sm (term)
+  single: mult (term)
+  single: mult_n_O (term)
+  single: mult_n_Sm (term)
+
+Now comes the content of module ``Peano``:
+
+.. coqtop:: in
+  
+  Theorem eq_S : forall x y:nat, x = y -> S x = S y.
+  Definition pred (n:nat) : nat :=
+   match n with
+   | 0 => 0
+   | S u => u
+   end.
+  Theorem pred_Sn : forall m:nat, m = pred (S m).
+  Theorem eq_add_S : forall n m:nat, S n = S m -> n = m.
+  Hint Immediate eq_add_S : core.
+  Theorem not_eq_S : forall n m:nat, n <> m -> S n <> S m.
+  Definition IsSucc (n:nat) : Prop :=
+   match n with
+   | 0 => False
+   | S p => True
+   end.
+  Theorem O_S : forall n:nat, 0 <> S n.
+  Theorem n_Sn : forall n:nat, n <> S n.
+  Fixpoint plus (n m:nat) {struct n} : nat :=
+   match n with
+   | 0 => m
+   | S p => S (p + m)
+   end
+  where "n + m" := (plus n m) : nat_scope.
+  Lemma plus_n_O : forall n:nat, n = n + 0.
+  Lemma plus_n_Sm : forall n m:nat, S (n + m) = n + S m.
+  Fixpoint mult (n m:nat) {struct n} : nat :=
+   match n with
+   | 0 => 0
+   | S p => m + p * m
+   end
+  where "n * m" := (mult n m) : nat_scope.
+  Lemma mult_n_O : forall n:nat, 0 = n * 0.
+  Lemma mult_n_Sm : forall n m:nat, n * m + n = n * (S m).
+
+
+Finally, it gives the definition of the usual orderings ``le``,
+``lt``, ``ge`` and ``gt``.
+
+.. index::
+  single: le (term)
+  single: le_n (term)
+  single: le_S (term)
+  single: lt (term)
+  single: ge (term)
+  single: gt (term)
+
+.. coqtop:: in
+
+  Inductive le (n:nat) : nat -> Prop :=
+  | le_n : le n n
+  | le_S : forall m:nat, n <= m -> n <= (S m).
+  where "n <= m" := (le n m) : nat_scope.
+  Definition lt (n m:nat) := S n <= m.
+  Definition ge (n m:nat) := m <= n.
+  Definition gt (n m:nat) := m < n.
+
+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.
+
+.. index::
+  single: nat_case (term)
+  single: nat_double_ind (term)
+
+.. coqtop:: in
+
+  Theorem nat_case :
+   forall (n:nat) (P:nat -> Prop), 
+   P 0 -> (forall m:nat, P (S m)) -> P n.
+  Theorem nat_double_ind :
+   forall R:nat -> nat -> Prop,
+    (forall n:nat, R 0 n) ->
+    (forall n:nat, R (S n) 0) ->
+    (forall n m:nat, R n m -> R (S n) (S m)) -> forall n m:nat, R n m.
+
+
+Well-founded recursion
+~~~~~~~~~~~~~~~~~~~~~~
+
+The basic library contains the basics of well-founded recursion and 
+well-founded induction, in module ``Wf.v``.
+
+.. index::
+   single: Well foundedness
+   single: Recursion
+   single: Well founded induction
+   single: Acc (term)
+   single: Acc_inv (term)
+   single: Acc_rect (term)
+   single: well_founded (term)
+
+.. coqtop:: in
+
+  Section Well_founded.
+  Variable A : Type.
+  Variable R : A -> A -> Prop.
+  Inductive Acc (x:A) : Prop :=
+    Acc_intro : (forall y:A, R y x -> Acc y) -> Acc x.
+  Lemma Acc_inv x : Acc x -> forall y:A, R y x -> Acc y.
+  Definition well_founded := forall a:A, Acc a.
+  Hypothesis Rwf : well_founded.
+  Theorem well_founded_induction :
+   forall P:A -> Set,
+    (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a.
+  Theorem well_founded_ind :
+   forall P:A -> Prop,
+    (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a.
+
+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.
+
+.. index::
+  single: Fix_F (term)
+  single: fix_eq (term)
+  single: Fix_F_inv (term)
+  single: Fix_F_eq (term)
+
+.. coqtop:: in
+
+  Section FixPoint.
+  Variable P : A -> Type.
+  Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x.
+  Fixpoint Fix_F (x:A) (r:Acc x) {struct r} : P x :=
+    F x (fun (y:A) (p:R y x) => Fix_F y (Acc_inv x r y p)).
+  Definition Fix (x:A) := Fix_F x (Rwf x).
+  Hypothesis F_ext :
+    forall (x:A) (f g:forall y:A, R y x -> P y),
+      (forall (y:A) (p:R y x), f y p = g y p) -> F x f = F x g.
+  Lemma Fix_F_eq :
+   forall (x:A) (r:Acc x),
+     F x (fun (y:A) (p:R y x) => Fix_F y (Acc_inv x r y p)) = Fix_F x r.
+  Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F x r = Fix_F x s.
+  Lemma fix_eq : forall x:A, Fix x = F x (fun (y:A) (p:R y x) => Fix y).
+  End FixPoint.
+  End Well_founded.
+
+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``. This is the module ``Logic_Type.v``.
+
+.. index::
+  single: notT (term)
+  single: prodT (term)
+  single: pairT (term)
+
+.. coqtop:: in
+
+  Definition notT (A:Type) := A -> False.
+  Inductive prodT (A B:Type) : Type := pairT (_:A) (_:B).
+
+At the end, it defines data-types at the ``Type`` level.
+
+Tactics
+~~~~~~~
+
+A few tactics defined at the user level are provided in the initial
+state, in module ``Tactics.v``. They are listed at
+http://coq.inria.fr/stdlib, in paragraph ``Init``, link ``Tactics``.
+
+
+The standard library
+--------------------
+
+Survey
+~~~~~~
+
+The rest of the standard library is structured into the following 
+subdirectories:
+
+  * **Logic** : Classical logic and dependent equality
+  * **Arith** : Basic Peano arithmetic
+  * **PArith** : Basic positive integer arithmetic
+  * **NArith** : Basic binary natural number arithmetic
+  * **ZArith** : Basic relative integer arithmetic
+  * **Numbers** : Various approaches to natural, integer and cyclic numbers (currently axiomatically and on top of 2^31 binary words)
+  * **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)
+  * **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
+Section :ref:`TODO-6.5.1-Require`).
+
+The different modules of the |Coq| standard library are documented
+online at http://coq.inria.fr/stdlib.
+
+Peano’s arithmetic (nat)
+~~~~~~~~~~~~~~~~~~~~~~~~
+
+.. index::
+   single: Peano's arithmetic
+   single: nat_scope
+
+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``.
+
+The following table describes the notations available in scope
+``nat_scope`` :
+
+===============   ===================
+Notation          Interpretation
+===============   ===================
+``_ < _``         ``lt``
+``_ <= _``        ``le``
+``_ > _``         ``gt``
+``_ >= _``        ``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``
+===============   ===================
+
+
+Notations for integer arithmetics
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+.. index::
+  single: Arithmetical notations
+  single: + (term)
+  single: * (term)
+  single: - (term)
+  singel: / (term)
+  single: <= (term)
+  single: >= (term)
+  single: < (term)
+  single: > (term)
+  single: ?= (term)
+  single: mod (term)
+
+
+The following table describes the syntax of expressions
+for integer arithmetics. It is provided by requiring and opening the module ``ZArith`` and opening scope ``Z_scope``.
+It specifies how notations are interpreted and, when not
+already reserved, the precedence and associativity.
+
+===============   ====================  ==========  =============
+Notation          Interpretation        Precedence  Associativity
+===============   ====================  ==========  =============
+``_ < _``         ``Z.lt``
+``_ <= _``        ``Z.le``
+``_ > _``         ``Z.gt``
+``_ >= _``        ``Z.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``
+``_ ?= _``        ``Z.compare``         70          no
+``_ + _``         ``Z.add``
+``_ - _``         ``Z.sub``
+``_ * _``         ``Z.mul``
+``_ / _``         ``Z.div``
+``_ mod _``       ``Z.modulo``          40          no
+``- _``           ``Z.opp``
+``_ ^ _``         ``Z.pow``
+===============   ====================  ==========  =============
+
+
+.. example::
+  .. coqtop:: all reset
+
+    Require Import ZArith.
+    Check (2 + 3)%Z.
+    Open Scope Z_scope.
+    Check 2 + 3.
+
+
+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``
+``_ <= _``        ``Rle``
+``_ > _``         ``Rgt``
+``_ >= _``        ``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``
+===============   ===================
+
+.. example::
+  .. coqtop:: all reset
+
+    Require Import Reals.
+    Check  (2 + 3)%R.
+    Open Scope R_scope.
+    Check 2 + 3.
+
+Some tactics for real numbers
++++++++++++++++++++++++++++++
+
+In addition to the powerful ``ring``, ``field`` and ``fourier``
+tactics (see Chapter :ref:`tactics`), there are also:
+
+.. tacn:: discrR
+  :name: discrR
+  
+  Proves that two real integer constants are different.
+
+.. example::
+  .. coqtop:: all reset
+
+    Require Import DiscrR.
+    Open Scope R_scope.
+    Goal 5 <> 0.
+    discrR.
+
+.. tacn:: split_Rabs
+  :name: split_Rabs
+
+  Allows unfolding the ``Rabs`` constant and splits corresponding conjunctions.
+
+.. example::
+  .. coqtop:: all reset
+
+    Require Import Reals.
+    Open Scope R_scope.
+    Goal forall x:R, x <= Rabs x.
+    intro; split_Rabs.
+
+.. tacn:: split_Rmult
+  :name: split_Rmult
+ 
+  Splits a condition that a product is non null into subgoals
+  corresponding to the condition on each operand of the product.
+
+.. example::
+  .. coqtop:: all reset
+
+    Require Import Reals.
+    Open Scope R_scope.
+    Goal forall x y z:R, x * y * z <> 0.
+    intros; split_Rmult.
+
+These tactics has been written with the tactic language Ltac
+described in Chapter :ref:`thetacticlanguage`.
+
+
+List library
+~~~~~~~~~~~~
+
+.. index::
+  single: Notations for lists
+  single: length (term)
+  single: head (term)
+  single: tail (term)
+  single: app (term)
+  single: rev (term)
+  single: nth (term)
+  single: map (term)
+  single: flat_map (term)
+  single: fold_left (term)
+  single: fold_right (term)
+
+Some elementary operations on polymorphic lists are defined here. 
+They can be accessed by requiring module ``List``.
+
+It defines the following notions:
+
+  * ``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)
+
+The following table shows notations available when opening scope ``list_scope``.
+
+==========  ==============  ==========  =============
+Notation    Interpretation  Precedence  Associativity
+==========  ==============  ==========  =============
+``_ ++ _``  ``app``         60          right
+``_ :: _``  ``cons``        60          right
+==========  ==============  ==========  =============
+
+.. _userscontributions:
+
+Users’ contributions
+--------------------
+
+Numerous users' contributions have been collected and are available at
+URL http://coq.inria.fr/opam/www/.  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.