path: root/doc/RefMan-lib.tex

\chapter{The {\Coq} library}
\index{Theories}\label{Theories}

The \Coq\ library is structured into three parts:

\begin{description}
\item[The initial library:] it contains
  elementary logical notions and datatypes. 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});

\item[User contributions:] Other specification and proof developments
  coming from the \Coq\ users' community. These libraries are no
  longer distributed with the system.  They are available by anonymous
  FTP (see section~\ref{Contributions}).
\end{description}

This chapter briefly reviews these libraries.

\section{The basic library}
\label{Prelude}

This section lists the basic notions and results which are directly
available in the standard \Coq\ system
\footnote{These constructions are defined in the
{\tt Prelude} module in directory {\tt theories/Init} at the {\Coq}
root directory; this includes the modules
% {\tt Core} l'inexplicable let
{\tt Logic},
{\tt Datatypes},
{\tt Specif},
{\tt Peano},
and {\tt Wf}
plus the module {\tt Logic\_Type}}.

\subsection{Logic} \label{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
extension
\footnote{This syntax is defined in module {\tt LogicSyntax}}
 is shown on figure \ref{formulas-syntax}.

\begin{figure}
\label{formulas-syntax}
\begin{center}
\begin{tabular}{|lclr|}
\hline
{\form} & ::= & {\tt True} & ({\tt True})\\
  & $|$ & {\tt False} & ({\tt False})\\
  & $|$ & {\verb|~|} {\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 (} {\ident} {\tt :} {\type} {\tt )}
  {\form} & (\em{primitive for all})\\
  & $|$ & {\tt ( ALL} {\ident} \zeroone{{\tt :} {\specif}} {\tt |}
  {\form} {\tt )} & ({\tt all})\\
  & $|$ & {\tt ( EX} {\ident} \zeroone{{\tt :} {\specif}} {\tt
  |} {\form} {\tt )}  & ({\tt ex})\\
  & $|$ & {\tt ( EX} {\ident} \zeroone{{\tt :} {\specif}} {\tt
  |} {\form}  {\tt \&} {\form} {\tt )} & ({\tt ex2})\\
  & $|$ & {\term} {\tt =} {\term} & ({\tt eq})\\
\hline
\end{tabular}
\end{center}

\medskip

\Rem The 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. There is true reason to
have the notation {\tt ( ALL} {\ident} \zeroone{{\tt :} {\specif}} {\tt
|} {\form} {\tt )} propositions), except to have a notation dual of
the notation for first-order existential quantification.
\caption{Syntax of formulas}
\end{figure}

\subsubsection{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 :

(********** Next parsing errors for /\ and \/ are harmless ***********)
(******************* since output is not displayed *******************)
(* Just to adjust the prompt: *) Prop :=
    I : True.
Inductive False :  Prop :=.
Definition not (A: Prop) := A -> False.
Inductive and (A B:Prop) : Prop :=
    conj : A -> B -> 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}
\ttindex{or}
\ttindex{or\_introl}
\ttindex{or\_intror}
\ttindex{iff}
\ttindex{IF}
\begin{coq_example*}
End Projections.
Inductive or (A B:Prop) : Prop :=
  | or_introl : A -> A \/ B
  | or_intror : B -> A \/ B.
Definition iff (P Q:Prop) := (P -> Q) /\ (Q -> P).
Definition IF (P Q R:Prop) := P /\ Q \/ ~ P /\ R.
\end{coq_example*}

\subsubsection{Quantifiers} \label{Quantifiers}
\index{Quantifiers}

Then we find first-order quantifiers:
\ttindex{all}
\ttindex{All}
\ttindex{ex}
\ttindex{Ex}
\ttindex{EX}
\ttindex{ex\_intro}
\ttindex{ex2}
\ttindex{Ex2}
\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 : forall x:A, P x -> ex A P.
Inductive ex2 (A:Set) (P Q:A -> Prop) : Prop :=
    ex_intro2 : forall x:A, P x -> Q x -> ex2 A P Q.
\end{coq_example*}

The following abbreviations are allowed:
\begin{center}
  \begin{tabular}[h]{|l|r|}
    \hline
    \verb+(ALL x:A | P)+    & \verb+(all A [x:A]P)+ \\
    \verb+(ALL x | P)+      & \verb+(all A [x:A]P)+ \\
    \verb+(EX x:A | P)+     & \verb+(ex A [x:A]P)+ \\
    \verb+(EX x | P)+       & \verb+(ex A [x:A]P)+ \\
    \verb+(EX x:A | P & Q)+ & \verb+(ex2 A [x:A]P [x:A]Q)+ \\
    \verb+(EX x | P & Q)+   & \verb+(ex2 A [x:A]P [x:A]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} \label{Equality}
\index{Equality}

Then, we find equality, defined as an inductive relation. That is,
given a \verb:Set: \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{refl\_equal}

\begin{coq_example*}
Inductive eq (A:Set) (x:A) : A -> Prop :=
    refl_equal : eq A x x.
\end{coq_example*}

\subsubsection{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{sym\_eq}
\ttindex{trans\_eq}
\ttindex{f\_equal}
\ttindex{sym\_not\_eq}
\begin{coq_example*}
Section equality.
Variables A B : 
             Set.
Variable f : 
            A -> B.
Variables x y z : 
             A.
Theorem sym_eq : 
  x = y -> y = x.
Theorem trans_eq : 
  x = y -> y = z -> x = z.
Theorem f_equal : 
  x = y -> f x = f y.
Theorem sym_not_eq : 
  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:Set) (x:A) (P:A -> Prop), P x -> forall y:A, y = x -> P y.
Definition eq_rec_r :
  forall (A:Set) (x:A) (P:A -> Set), P x -> forall y:A, y = x -> P y.
Definition eq_rect_r :
  forall (A:Set) (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*}
Hints Immediate sym_eq sym_not_eq : 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:Set) (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} \label{Datatypes}

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} \label{Programming}
\index{Programming}
\index{Datatypes}

\ttindex{unit}
\ttindex{tt}
\ttindex{bool}
\ttindex{true}
\ttindex{false}
\ttindex{nat}
\ttindex{O}
\ttindex{S}
\ttindex{option}
\ttindex{Some}
\ttindex{None}

\begin{coq_example*}
Inductive unit : Set :=
    tt : unit.
Inductive bool : Set :=
  | true : bool
  | false : bool.
Inductive option (A:Set) : Set :=
  | Some : A -> option A
  | None : option A.
Inductive nat : Set :=
  | O : nat
  | S : nat -> nat.
\end{coq_example*}

Note that zero is the letter \verb:O:, and {\sl not} the numeral
\verb:0:.

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}
\ttindex{Fst}
\ttindex{Snd}

\begin{coq_example*}
Inductive sum (A B:Set) : Set :=
  | inl : A -> sum A B
  | inr : B -> sum A B.
Inductive prod (A B:Set) : Set :=
    pair : A -> B -> prod 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.
Notation Fst := (fst _ _).
Notation Snd := (snd _ _).
\end{coq_example*}

\subsection{Specification}

The following notions\footnote{They are defined in module {\tt
Specif.v}} allows to build new datatypes and specifications. 
They are available with the syntax shown on
figure \ref{specif-syntax}\footnote{This syntax can be found in the module
{\tt SpecifSyntax.v}}.

For instance, given \verb|A:Set| and \verb|P:A->Prop|, the construct
\verb+{x:A | (P x)}+ (in abstract syntax \verb+(sig A P)+) is a
\verb:Set:. 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:Cases:) 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.

\index{\{x:A "| (P x)\}}
\index{"|}
\ttindex{sig}
\ttindex{exist}
\ttindex{sig2}
\ttindex{exist2}

\begin{coq_example*}
Inductive sig (A:Set) (P:A -> Prop) : Set :=
    exist : forall x:A, P x -> sig A P.
Inductive sig2 (A:Set) (P Q:A -> Prop) : Set :=
    exist2 : forall x:A, P x -> Q x -> sig2 A P Q.
\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 \verb:Set:
constructor.

\ttindex{\{x:A \& (P x)\}}
\ttindex{\&}
\ttindex{sigS}
\ttindex{existS}
\ttindex{projS1}
\ttindex{projS2}
\ttindex{sigS2}
\ttindex{existS2}

\begin{coq_example*}
Inductive sigS (A:Set) (P:A -> Set) : Set :=
    existS : forall x:A, P x -> sigS A P.
Section sigSprojections.
Variable A : 
              Set.
Variable P : 
              A -> Set.
Definition projS1 (H:
                      sigS A P) := let (x, h) := H in x.
Definition projS2 (H:
                      sigS A P) :=
  let (x, h) as H return P (projS1 H) := H in h.
End sigSprojections.
Inductive sigS2 (A: Set) (P Q:A -> Set) : Set :=
    existS2 : forall x:A, P x -> Q x -> sigS2 A P Q.
\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 -> sumbool A B
  | right : B -> sumbool A 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 -> sumor A B
  | inright : B -> sumor A B.
\end{coq_example*}

\begin{figure}
\label{specif-syntax}
\begin{center}
\begin{tabular}{|lclr|}
\hline
{\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 sigS})\\
  & $|$ & {\tt \{} {\ident} {\tt :} {\specif} {\tt \&} {\specif} {\tt
    \&} {\specif} {\tt \}} & ({\tt sigS2})\\
  &  & & \\
{\term} & ::= & {\tt (} {\term} {\tt ,} {\term} {\tt )} & ({\tt pair})\\
\hline
\end{tabular}
\caption{Syntax of datatypes and specifications}
\end{center}
\end{figure}

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 constructs builds a sum between a data type \verb|A:Set| 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: and
\verb:Prop: in a way which is consistent with the realizability
interpretation.
\ttindex{False\_rec}
\ttindex{eq\_rec}
\ttindex{Except}
\ttindex{absurd\_set}
\ttindex{and\_rec}

%Lemma False_rec : (P:Set)False->P.
%Lemma False_rect : (P:Type)False->P.
\begin{coq_example*}
Definition except := False_rec.
Notation Except := (except _).
Theorem absurd_set : forall (A:Prop) (C:Set), A -> ~ A -> C.
Theorem and_rec :
 forall (A B:Prop) (C:Set), (A -> B -> C) -> A /\ B -> C.
\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}}.
\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 n m:nat, n = m -> S n = S m.
\end{coq_example*}
\begin{coq_eval}
Abort.
\end{coq_eval}
\begin{coq_example*}
Definition pred (n:nat) : nat :=
  match n return nat with
  | O => O
  | 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.
Hints 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
  | O => False
  | S p => True
  end.
Theorem O_S : forall n:nat, O <> 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
  | O => m
  | S p => S (plus p m)
  end.
Lemma plus_n_O : forall n:nat, n = plus n O.
Lemma plus_n_Sm : forall n m:nat, S (plus n m) = plus 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
  | O => O
  | S p => plus m (mult p m)
  end.
Lemma mult_n_O : forall n:nat, O = mult n O.
Lemma mult_n_Sm : forall n m:nat, plus (mult n m) n = mult 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, le n m -> le n (S m).
Definition lt (n m:nat) := le (S n) m.
Definition ge (n m:nat) := le m n.
Definition gt (n m:nat) := lt 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 O -> (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 O n) ->
   (forall n:nat, R (S n) O) ->
   (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\_rec}
\ttindex{well\_founded}

\begin{coq_example*}
Section Well_founded.
Variable A : Set.
Variable R : A -> A -> Prop.
Inductive Acc : A -> Prop :=
    Acc_intro : forall x:A, (forall y:A, R y x -> Acc y) -> Acc x.
Lemma Acc_inv : forall x:A, Acc x -> forall y:A, R y x -> Acc y.
\end{coq_example*}
\begin{coq_eval}
olddestruct 1; trivial.
Defined.
\end{coq_eval}
\begin{coq_example*}
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.
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}
{\tt 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.
\ttindex{Fix\_F}
\ttindex{fix\_eq}
\ttindex{Fix\_F\_inv}
\ttindex{Fix\_F\_eq}
\begin{coq_example*}
Section FixPoint.
Variable P : A -> Set.
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 logical quantifiers axiomatized at the
\verb:Type: level. 

\ttindex{allT}
\ttindex{AllT}
\ttindex{inst}
\ttindex{gen}
\ttindex{exT}
\ttindex{ExT}
\ttindex{EXT}
\ttindex{exT\_intro}
\ttindex{ExT2}
\ttindex{exT2}
\ttindex{EmptyT}
\ttindex{UnitT}
\ttindex{notT}

\begin{coq_example*}
Definition allT (A: Type) (P:A -> Prop) := forall x:A, P x.
Section universal_quantification.
Variable A :  Type.
Variable P : A -> Prop.
Theorem inst : forall x:A, ( ALL x : _ | P x) -> P x.
Theorem gen : forall (B:Prop) (f:forall y:A, B -> P y), B -> allT _ P.
\end{coq_example*}
\begin{coq_eval}
Abort All.
\end{coq_eval}
\begin{coq_example*}
End universal_quantification.
Inductive exT (A:Type) (P:A -> Prop) : Prop :=
    exT_intro : forall x:A, P x -> exT A P.
Inductive exT2 (A:Type) (P Q:A -> Prop) : Prop :=
    exT_intro2 : forall x:A, P x -> Q x -> exT2 A P Q.
\end{coq_example*}

It defines also Leibniz equality \verb:x==y: when \verb:x: and
\verb:y: belong to \verb+A:Type+.
\ttindex{eqT}
\ttindex{refl\_eqT}
\ttindex{sum\_eqT}
\ttindex{sym\_not\_eqT}
\ttindex{trans\_eqT}
\ttindex{congr\_eqT}
\ttindex{eqT\_ind\_r}
\ttindex{eqT\_rec\_r}

\begin{coq_example*}
Inductive eqT (A:Type) (x:A) : A -> Prop :=
    refl_eqT : eqT A x x.
Section Equality_is_a_congruence.
Variables A B : Type.
Variable f : A -> B.
Variables x y z : A.
Lemma sym_eqT : x = y -> y = x.
Lemma trans_eqT : x = y -> y = z -> x = z.
Lemma congr_eqT : x = y -> f x = f y.
\end{coq_example*}
\begin{coq_eval}
Abort All.
\end{coq_eval}
\begin{coq_example*}
End Equality_is_a_congruence.
Hints Immediate sym_eq sym_not_eqT : core.
Definition eqT_ind_r :
  forall (A:Type) (x:A) (P:A -> Prop), P x -> forall y:A, y = x -> P y.
\end{coq_example*}
\begin{coq_eval}
Abort.
\end{coq_eval}

The figure \ref{formulas-syntax-type} presents the syntactic notations 
corresponding to the main definitions
\footnote{This syntax is defined in module {\tt Logic\_TypeSyntax}}

\begin{figure}
\label{formulas-syntax-type}
\begin{center}
\begin{tabular}{|lclr|}
\hline
{\form} & ::= & {\tt ( ALLT} {\ident} \zeroone{{\tt :} {\specif}} {\tt |}
  {\form} {\tt )} & ({\tt allT})\\
  & $|$ & {\tt ( EXT} {\ident} \zeroone{{\tt :} {\specif}} {\tt
  |} {\form} {\tt )}  & ({\tt exT})\\
  & $|$ & {\tt ( EXT} {\ident} \zeroone{{\tt :} {\specif}} {\tt
  |} {\form}  {\tt \&} {\form} {\tt )} & ({\tt exT2})\\
  & $|$ & {\term} {\tt ==} {\term} & ({\tt eqT})\\
\hline
\end{tabular}
\end{center}
\caption{Syntax of first-order formulas in the type universe}
\end{figure}

At the end, it defines datatypes at the {\Type} level.

\begin{coq_example*}
Inductive EmptyT : Type :=.
Inductive UnitT : Type :=
    IT : UnitT.
Definition notT (A:Type) := A -> EmptyT.
Inductive identityT (A:
                     Type) (a:A) : A -> Type :=
    refl_identityT : identityT A a a.
\end{coq_example*}

\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 ZArith}  & Basic integer arithmetic \\
  {\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 IntMap}    & Representation of finite sets by an efficient
  structure of map (trees indexed by binary integers).\\
 {\bf Reals}   & Axiomatization of Real Numbers (classical, basic functions, 
                 integer part, fractional part, limit, derivative, Cauchy 
                 series, power series and results,... Requires the 
                 \textbf{ZArith} library).\\
 {\bf Relations} & Relations (definitions and basic results). \\
 {\bf Sorting} & Sorted list (basic definitions and heapsort correctness). \\
 {\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{\texttt{http://coq.inria.fr}}.

\subsection{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 the module {\tt ZArith}.

\ttindex{+}
\ttindex{*}
\ttindex{-}

The {\tt +} and {\tt -} binary operators bind less than the {\tt *} operator
which binds less than the {\tt |}~...~{\tt |} and {\tt -} unary
operators which bind less than the others constructions.
All the binary operators are left associative. The {\tt [}~...~{\tt ]}
allows to escape the {\zarith} grammar.

\begin{figure}
\begin{center}
\begin{tabular}{|lcl|}
\hline
{\form} & ::= & {\tt `} {\zarithformula} {\tt `}\\
  & & \\
{\term} & ::= & {\tt `} {\zarith} {\tt `}\\
  & & \\
{\zarithformula} & ::= & {\zarith} {\tt =} {\zarith} \\
   & $|$ & {\zarith} {\tt <=} {\zarith} \\
   & $|$ & {\zarith} {\tt <} {\zarith} \\
   & $|$ & {\zarith} {\tt >=} {\zarith} \\
   & $|$ & {\zarith} {\tt >} {\zarith}  \\
   & $|$ & {\zarith} {\tt =} {\zarith} {\tt =} {\zarith} \\
   & $|$ & {\zarith} {\tt <=} {\zarith} {\tt <=} {\zarith} \\
   & $|$ & {\zarith} {\tt <=} {\zarith} {\tt <} {\zarith} \\
   & $|$ & {\zarith} {\tt <} {\zarith} {\tt <=} {\zarith} \\
   & $|$ & {\zarith} {\tt <} {\zarith} {\tt <} {\zarith} \\
   & $|$ & {\zarith} {\tt <>} {\zarith} \\
   & $|$ & {\zarith} {\tt ?} {\tt =} {\zarith} \\
  & & \\
{\zarith}  & ::= & {\zarith} {\tt +} {\zarith} \\
   & $|$ & {\zarith} {\tt -} {\zarith} \\
   & $|$ & {\zarith} {\tt *} {\zarith} \\
   & $|$ & {\tt |} {\zarith} {\tt |} \\
   & $|$ & {\tt -} {\zarith} \\
   & $|$ & {\ident} \\
   & $|$ & {\tt [} {\term} {\tt ]} \\
   & $|$ & {\tt (} \nelist{\zarith}{} {\tt )} \\
   & $|$ & {\tt (} \nelist{\zarith}{,} {\tt )} \\
   & $|$ & {\integer} \\
\hline
\end{tabular}
\end{center}
\label{zarith-syntax}
\caption{Syntax of expressions in integer arithmetics}
\end{figure}

\subsection{Notations for Peano's arithmetic (\texttt{nat})}
\index{Peano's arithmetic notations}

After having required the module \texttt{Arith}, the user can type the
naturals using decimal notation. That is he can write \texttt{(3)}
for \texttt{(S (S (S O)))}. The number must be between parentheses.
This works also in the left hand side of a \texttt{Cases} expression
(see for example section \ref{Refine-example}).

%Remove the redefinition of nat
\begin{coq_eval}
Reset Initial.
\end{coq_eval}

\begin{coq_example*}
Require Import Arith.
Fixpoint even (n:nat) : bool :=
  match n with
  | O => true
  | S O => false
  | S (S n) => even n
  end.
\end{coq_example*}

\begin{coq_eval}
Reset Initial.
\end{coq_eval}

\subsection{Real numbers library}

\subsubsection{Notations for real numbers}
\index{Notations for real numbers}

This is provided by requiring the module {\tt Reals}. This notation is very
similar to the notation for integer arithmetics (see figure 
\ref{zarith-syntax}) where Inverse (/x) and division (x/y) have been added. 
This syntax is used parenthesizing by a double back-quote (\verb:``:).

\begin{coq_example}
Require Import Reals.
Check  (2 + 3)%R.
\end{coq_example}

\subsubsection{Some tactics}

In addition to the Ring, Field and Fourier tactics (see chapter \ref{Tactics})
there are:

{\tt DiscrR} prove that a real integer constante c1 is non equal to
another real integer constante c2.
\tacindex{DiscrR}

\begin{coq_example*}
Require Import DiscrR.
Goal 5%R <> 0%R.
\end{coq_example*}

\begin{coq_example}
discrR.
\end{coq_example}

\begin{coq_eval}
Abort.
\end{coq_eval}

{\tt SplitAbsolu} allows us to unfold {\tt Rabsolu} contants and split 
corresponding conjonctions.
\tacindex{SplitAbsolu}

\begin{coq_example*}
Require Import SplitAbsolu.
Goal forall x:R, (x <= Rabs x)%R.
\end{coq_example*}

\begin{coq_example}
intro; split_Rabs.
\end{coq_example}

\begin{coq_eval}
Abort.
\end{coq_eval}

{\tt 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.
\tacindex{SplitRmult}

\begin{coq_example*}
Require Import SplitRmult.
Goal forall x y z:R, (x * y * z)%R <> 0%R.
\end{coq_example*}

\begin{coq_example}
intros; split_Rmult.
\end{coq_example}

All this tactics has been written with the new tactic language.\\

More details are available in this document: {\tt http://coq.inria.fr/$\sim$desmettr/Reals.ps}.\\

\begin{coq_eval}
Reset Initial.
\end{coq_eval}

\section{Users' contributions}
\index{Contributions}
\label{Contributions}

Numerous users' contributions have been collected and are available on
the WWW at the following address: \verb!pauillac.inria.fr/coq/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
\verb:ftp.inria.fr:, in directory \verb:INRIA/coq/: and
searchable on-line at 

\begin{quotation}
  \texttt{http://coq.inria.fr/contribs-eng.html}
\end{quotation}

% $Id$ 


%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: