Nettoyage de l'archive doc et restructuration avant intégration à l'archive

principale de Coq et publication des sources (HH)


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8606 85f007b7-540e-0410-9357-904b9bb8a0f7

7 files changed, 5615 insertions, 0 deletions

diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
new file mode 100644
index 000000000..7b8ed6d10
--- /dev/null
+++ b/doc/faq/FAQ.tex
@@ -0,0 +1,2441 @@
+\documentclass[a4paper]{article}
+\pagestyle{plain}
+
+% yay les symboles
+\usepackage{stmaryrd}
+\usepackage{amssymb}
+\usepackage{url}
+%\usepackage{multicol}
+\usepackage{hevea}
+\usepackage{fullpage}
+\usepackage[latin1]{inputenc}
+\usepackage[english]{babel}
+\usepackage{graphics}
+
+%\input{../macros.tex}
+
+% Making hevea happy
+%HEVEA \renewcommand{\textbar}{|}
+%HEVEA \renewcommand{\textunderscore}{\_}
+
+\def\Question#1{\stepcounter{question}\subsubsection{#1}}
+
+% version et date
+\def\faqversion{0.1}
+
+% les macros d'amour
+\def\Coq{\textsc{Coq}}
+\def\Why{\textsc{Why}}
+\def\Caduceus{\textsc{Caduceus}}
+\def\Krakatoa{\textsc{Krakatoa}}
+\def\Ltac{\textsc{Ltac}}
+\def\CoqIde{\textsc{CoqIde}}
+
+\newcommand{\coqtt}[1]{{\tt #1}}
+\newcommand{\coqimp}{{\mbox{\tt ->}}}
+\newcommand{\coqequiv}{{\mbox{\tt <->}}}
+
+
+% macro pour les tactics
+\def\split{{\tt split}}
+\def\assumption{{\tt assumption}}
+\def\auto{{\tt auto}}
+\def\trivial{{\tt trivial}}
+\def\tauto{{\tt tauto}}
+\def\left{{\tt left}}
+\def\right{{\tt right}}
+\def\decompose{{\tt decompose}}
+\def\intro{{\tt intro}}
+\def\intros{{\tt intros}}
+\def\field{{\tt field}}
+\def\ring{{\tt ring}}
+\def\apply{{\tt apply}}
+\def\exact{{\tt exact}}
+\def\cut{{\tt cut}}
+\def\assert{{\tt assert}}
+\def\solve{{\tt solve}}
+\def\idtac{{\tt idtac}}
+\def\fail{{\tt fail}}
+\def\existstac{{\tt exists}}
+\def\firstorder{{\tt firstorder}}
+\def\congruence{{\tt congruence}}
+\def\gb{{\tt gb}}
+\def\generalize{{\tt generalize}}
+\def\abstracttac{{\tt abstract}}
+\def\eapply{{\tt eapply}}
+\def\unfold{{\tt unfold}}
+\def\rewrite{{\tt rewrite}}
+\def\replace{{\tt replace}}
+\def\simpl{{\tt simpl}}
+\def\elim{{\tt elim}}
+\def\set{{\tt set}}
+\def\pose{{\tt pose}}
+\def\case{{\tt case}}
+\def\destruct{{\tt destruct}}
+\def\reflexivity{{\tt reflexivity}}
+\def\transitivity{{\tt transitivity}}
+\def\symmetry{{\tt symmetry}}
+\def\Focus{{\tt Focus}}
+\def\discriminate{{\tt discriminate}}
+\def\contradiction{{\tt contradiction}}
+\def\intuition{{\tt intuition}}
+\def\try{{\tt try}}
+\def\repeat{{\tt repeat}}
+\def\eauto{{\tt eauto}}
+\def\subst{{\tt subst}}
+\def\symmetryin{{\tt symmetryin}}
+\def\instantiate{{\tt instantiate}}
+\def\inversion{{\tt inversion}}
+\def\Defined{{\tt Defined}}
+\def\Qed{{\tt Qed}}
+\def\pattern{{\tt pattern}}
+\def\Type{{\tt Type}}
+\def\Prop{{\tt Prop}}
+\def\Set{{\tt Set}}
+
+
+\newcommand\vfile[2]{\ahref{#1}{\tt {#2}.v}}
+\urldef{\InitWf}{\url}
+  {http://coq.inria.fr/library/Coq.Init.Wf.html}
+\urldef{\LogicBerardi}{\url}
+  {http://coq.inria.fr/library/Coq.Logic.Berardi.html}
+\urldef{\LogicClassical}{\url}
+  {http://coq.inria.fr/library/Coq.Logic.Classical.html}
+\urldef{\LogicClassicalFacts}{\url}
+  {http://coq.inria.fr/library/Coq.Logic.ClassicalFacts.html}
+\urldef{\LogicClassicalDescription}{\url}
+  {http://coq.inria.fr/library/Coq.Logic.ClassicalDescription.html}
+\urldef{\LogicProofIrrelevance}{\url}
+  {http://coq.inria.fr/library/Coq.Logic.ProofIrrelevance.html}
+\urldef{\LogicEqdep}{\url}
+  {http://coq.inria.fr/library/Coq.Logic.Eqdep.html}
+\urldef{\LogicEqdepDec}{\url}
+  {http://coq.inria.fr/library/Coq.Logic.Eqdep_dec.html}
+
+
+
+
+\begin{document}
+\bibliographystyle{plain}
+\newcounter{question}
+\renewcommand{\thesubsubsection}{\arabic{question}}
+
+%%%%%%% Coq pour les nuls %%%%%%%
+
+\title{Coq Version 8.0 for the Clueless\\
+  \large(\protect\ref{lastquestion}
+  \ Hints)
+}
+\author{Pierre Castéran \and Hugo Herbelin \and Florent Kirchner \and Benjamin Monate \and Julien Narboux}
+\maketitle
+
+%%%%%%%
+
+\begin{abstract}
+This note intends to provide an easy way to get acquainted with the
+{\Coq} theorem prover. It tries to formulate appropriate answers
+to some of the questions any newcomers will face, and to give
+pointers to other references when possible.
+\end{abstract}
+
+%%%%%%%
+
+%\begin{multicols}{2}
+\tableofcontents
+%\end{multicols}
+
+%%%%%%%
+
+\newpage
+
+\section{Introduction}
+This FAQ is the sum of the questions that came to mind as we developed
+proofs in \Coq. Since we are singularly short-minded, we wrote the
+answers we found on bits of papers to have them at hand whenever the
+situation occurs again. This is pretty much the result of that: a
+collection of tips one can refer to when proofs become intricate. Yes,
+this means we won't take the blame for the shortcomings of this
+FAQ. But if you want to contribute and send in your own question and
+answers, feel free to write to us\ldots
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section{Presentation}
+
+\Question{What is {\Coq}?}\label{whatiscoq} 
+The {\Coq} tool is a formal proof management system: a proof done with {\Coq} is mechanically checked by the machine. 
+In particular, {\Coq} allows:
+\begin{itemize}
+    \item the definition of functions or predicates,
+    \item to state mathematical theorems and software specifications,
+    \item to develop interactively formal proofs of these theorems,
+    \item to check these proofs by a small certification "kernel".
+\end{itemize}
+{\Coq} is based on a logical framework called "Calculus of Inductive Constructions" extended by a modular development system for theories.
+
+\Question{Did you really need to name it like that?}
+Some French computer scientists have a tradition of naming their
+software as animal species: Caml, Elan, Foc or Phox are examples
+of this tacit convention. In French, ``coq'' means rooster, and it
+sounds like the initials of the Calculus of Constructions CoC on which
+it is based.
+
+\Question{Is {\Coq} a theorem prover?}
+
+{\Coq} comes with a few decision procedures (on propositional
+calculus, Presburger's arithmetic, ring and field simplification,
+resolution, ...) but the main style for proving theorems is
+interactively by using LCF-style tactics.
+
+
+\Question{What are the other theorem provers?} 
+Many other theorem provers are available for use nowadays. 
+Isabelle, HOL, HOL Light, Lego, Nuprl, PVS are examples of provers that are fairly similar
+to {\Coq} by the way they interact with the user. Other relatives of
+{\Coq} are ACL2, Alfa, Elf, Kiv, Mizar, NqThm, 
+\begin{htmlonly}%
+Omega\ldots
+\end{htmlonly}
+\begin{latexonly}%
+{$\Omega$}mega\ldots
+\end{latexonly}
+
+\Question{Who do I have to trust when I see a proof checked by Coq?}
+
+You have to trust:
+
+\begin{description}
+\item[The theory behind Coq] The theory of {\Coq} version 8.0 is
+generally admitted to be consistent wrt Zermelo-Fraenkel set theory +
+inaccessibles cardinals. Proofs of consistency of subsystems of the
+theory of Coq can be found in the literature.
+\item[The Coq kernel implementation] You have to trust that the
+implementation of the {\Coq} kernel mirrors the theory behind {\Coq}. The
+kernel is intentionally small to limit the risk of conceptual or
+accidental implementation bugs.
+\item[The Objective Caml compiler] The {\Coq} kernel is written using the
+Objective Caml language but it uses only the most standard features
+(no object, no label ...), so that it is highly unprobable that an
+Objective Caml bug breaks the consistency of {\Coq} without breaking all
+other kinds of features of {\Coq} or of other software compiled with
+Objective Caml.
+\item[Your hardware] In theory, if your hardware does not work
+properly, it can accidentally be the case that False becomes
+provable. But it is more likely the case that the whole {\Coq} system
+will be unusable. You can check your proof using different computers
+if you feel the need to.
+\item[Your axioms] Your axioms must be consistent with the theory
+behind {\Coq}.
+\end{description}
+
+
+\Question{Where can I find information about the theory behind {\Coq}?}
+\begin{description}
+\item[The Calculus of Inductive Constructions] The
+\ahref{http://coq.inria.fr/doc/Reference-Manual006.html}{corresponding}
+chapter and the chapter on
+\ahref{http://coq.inria.fr/doc/Reference-Manual007.html}{modules} in
+the {\Coq} Reference Manual.
+\item[Type theory] A book~\cite{ProofsTypes} or some lecture
+notes~\cite{Types:Dowek}.
+\item[Inductive types]
+Christine Paulin-Mohring's habilitation thesis~\cite{Pau96b}.
+\item[Co-Inductive types]
+Eduardo Giménez' thesis~\cite{EGThese}.
+\item[Miscellaneous] A
+\ahref{http://coq.inria.fr/doc/biblio.html}{bibliography} about Coq
+\end{description}
+
+
+\Question{How can I use {\Coq} to prove programs?}
+
+You can either extract a program from a proof by using the extraction
+mechanism or use dedicated tools, such as
+\ahref{http://why.lri.fr}{\Why},
+\ahref{http://krakatoa.lri.fr}{\Krakatoa},
+\ahref{http://why.lri.fr/caduceus/index.en.html}{\Caduceus}, to prove
+annotated programs written in other languages.
+
+\Question{How many {\Coq} users are there?}
+
+An estimation is about 100 regular users.
+
+\Question{How old is {\Coq}?}
+
+The first implementation is from 1985 (it was named {\sf CoC} which is
+the acronym of the name of the logic it implemented: the Calculus of
+Constructions).  The first official release of {\Coq} (version 4.10)
+was distributed in 1989.
+
+\Question{What are the \Coq-related tools?}
+
+\begin{description}
+\item[Coqide] A GTK based GUI for \Coq.
+\item[Pcoq] A GUI for {\Coq} with proof by pointing and pretty printing.
+\item[Helm/Mowgli] A rendering, searching and publishing tool.
+\item[Why] A back-end generator of verification conditions.
+\item[Krakatoa] A Java code certification tool that uses both {\Coq} and {\Why} to verify the soundness of implementations with regards to the specifications.
+\item[Caduceus] A C code certification tool that uses both {\Coq} and \Why.
+\item[coqwc] A tool similar to {\tt wc} to count lines in {\Coq} files.
+\item[coq-tex] A tool to insert {\Coq} examples within .tex files. 
+\item[coqdoc] A documentation tool for \Coq.
+\item[Proof General] A emacs mode for {\Coq} and many other proof assistants.
+\item[Foc] The \ahref{http://www-spi.lip6.fr/foc/index-en.html}{Foc} project aims at building an environment to develop certified computer algebra libraries. 
+\end{description}
+
+\Question{What are the high-level tactics of \Coq}
+
+\begin{itemize}
+\item Decision of quantifier-free Presburger's Arithmetic
+\item Simplification of expressions on rings and fields
+\item Decision of closed systems of equations
+\item Semi-decision of first-order logic
+\item Prolog-style proof search, possibly involving equalities
+\end{itemize}
+
+\Question{What are the main libraries available for \Coq}
+
+\begin{itemize}
+\item Basic Peano's arithmetic, binary integer numbers, rational numbers,
+\item Real analysis,
+\item Libraries for lists, boolean, maps, floating-point numbers,
+\item Libraries for relations, sets and constructive algebra,
+\item Geometry
+\end{itemize}
+
+
+\Question{What are the academic applications for {\Coq}?}
+
+{\Coq} is used for formalizing mathematical theories, for teaching,
+and for proving properties of algorithms or programs libraries.
+
+The largest mathematical formalization has been done at the University
+of Nijmegen (see the
+\ahref{http://vacuumcleaner.cs.kun.nl/c-corn}{Constructive Coq
+Repository at Nijmegen}).
+
+
+\Question{What are the industrial applications for {\Coq}?}
+
+{\Coq} is used e.g. to prove properties of the JavaCard system
+(especially by the companies Schlumberger and Trusted Logic). It has
+also been used to formalize the semantics of the Lucid-Synchrone
+data-flow synchronous calculus used by Esterel-Technologies.
+
+\iffalse
+todo christine compilo lustre?
+\fi
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section{Documentation}
+
+\Question{Where can I find documentation about {\Coq}?} 
+All the documentation about \Coq, from the reference manual~\cite{Coq:manual} to
+friendly tutorials~\cite{Coq:Tutorial} and documentation of the standard library, is available 
+\ahref{http://coq.inria.fr/doc-eng.html}{online}.
+All these documents are viewable either in browsable HTML, or as
+downloadable postscripts.
+
+\Question{Where can I find this FAQ on the web?}
+
+This FAQ is available online at \ahref{http://coq.inria.fr/doc/faq.html}{\url{http://coq.inria.fr/doc/faq.html}}.
+
+\Question{How can I submit suggestions / improvements / additions for this FAQ?}
+
+This FAQ is unfinished (in the sense that there are some obvious
+sections that are missing). Please send contributions to \texttt{Florent.Kirchner at lix.polytechnique.fr} and \texttt{Julien.Narboux at inria.fr}.
+
+\Question{Is there any mailing list about {\Coq}?} 
+The main {\Coq} mailing list is \url{coq-club@coq.inria.fr}, which
+broadcasts questions and suggestions about the implementation, the
+logical formalism or proof developments. See
+\ahref{http://coq.inria.fr/mailman/listinfo/coq-club}{\url{http://coq.inria.fr/mailman/listinfo/coq-club}} for
+subscription. For bugs reports see question \ref{coqbug}.
+
+\Question{Where can I find an archive of the list?}
+The archives of the {\Coq} mailing list are available at
+\ahref{http://coq.inria.fr/pipermail/coq-club}{\url{http://coq.inria.fr/pipermail/coq-club}}.
+
+
+\Question{How can I be kept informed of new releases of {\Coq}?}
+
+New versions of {\Coq} are announced on the coq-club mailing list. If you only want to receive information about new releases, you can subscribe to {\Coq} on \ahref{http://freshmeat.net/projects/coq/}{\url{http://freshmeat.net/projects/coq/}}.
+
+
+\Question{Is there any book about {\Coq}?}
+The first book on \Coq, Yves Bertot and Pierre Castéran's Coq'Art has been published by Springer-Verlag in 2004:
+\begin{quote}
+``This book provides a pragmatic introduction to the development of
+proofs and certified programs using \Coq. With its large collection of
+examples and exercises it is an invaluable tool for researchers,
+students, and engineers interested in formal methods and the
+development of zero-default software.''
+\end{quote}
+
+\Question{Where can I find some {\Coq} examples?} 
+
+There are examples in the manual~\cite{Coq:manual} and in the
+Coq'Art~\cite{Coq:coqart} exercises \ahref{\url{http://www.labri.fr/Perso/~casteran/CoqArt/index.html}}{\url{http://www.labri.fr/Perso/~casteran/CoqArt/index.html}}.
+You can also find large developments using
+{\Coq} in the {\Coq} user contributions:
+\ahref{http://coq.inria.fr/contrib-eng.html}{\url{http://coq.inria.fr/contrib-eng.html}}.
+
+\Question{How can I report a bug?}\label{coqbug}
+
+You can use the web interface at \ahref{http://coq.inria.fr/bin/coq-bugs}{\url{http://coq.inria.fr/bin/coq-bugs}}.
+
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section{Installation}
+
+\Question{What is the license of {\Coq}?}
+The main files are distributed under the GNU Lesser General License
+(LGPL). A few contributions are GPL.
+
+\Question{Where can I find the sources of {\Coq}?}
+The sources of {\Coq} can be found online in the tar.gz'ed packages
+(\ahref{http://coq.inria.fr/distrib-eng.html}{\url{http://coq.inria.fr/distrib-eng.html}}). Development sources can
+be accessed via anonymous CVS: \ahref{http://coqcvs.inria.fr/}{\url{http://coqcvs.inria.fr/}}
+
+\Question{On which platform is {\Coq} available?}
+Compiled binaries are available for Linux, MacOS X, Solaris, and
+Windows. The sources can be easily compiled on all platforms supporting Objective Caml.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section{The logic of {\Coq}}
+
+\subsection{General}
+
+\Question{What is the logic of \Coq?}
+
+{\Coq} is based on an axiom-free type theory called
+the Calculus of Inductive Constructions (see Coquand \cite{CoHu86}
+and Coquand--Paulin-Mohring \cite{CoPa89}). It includes higher-order
+functions and predicates, inductive and co-inductive datatypes and
+predicates, and a stratified hierarchy of sets.
+
+\Question{Is \Coq's logic intuitionistic or classical?}
+
+{\Coq} theory is basically intuitionistic
+(i.e. excluded-middle $A\vee\neg A$ is not granted by default) with
+the possibility to reason classically on demand by requiring an
+optional axiom stating $A\vee\neg A$.
+
+\Question{Can I define non-terminating programs in \Coq?}
+
+No, all programs in {\Coq} are terminating. Especially, loops
+must come with an evidence of their termination.
+
+\Question{How is equational reasoning working in {\Coq}?}
+
+ {\Coq} comes with an internal notion of computation called
+{\em conversion} (e.g. $(x+1)+y$ is internally equivalent to
+$(x+y)+1$; similarly applying argument $a$ to a function mapping $x$
+to some expression $t$ converts to the expression $t$ where $x$ is
+replaced by $a$). This notion of conversion (which is decidable
+because {\Coq} programs are terminating) covers a certain part of
+equational reasoning but is limited to sequential evaluation of
+expressions of (not necessarily closed) programs. Besides conversion,
+equations have to be treated by hand or using specialised tactics.
+
+\subsection{Axioms}
+
+\Question{What axioms can be safely added to {\Coq}?}
+
+There are a few typical useful axioms that are independent from the
+Calculus of Inductive Constructions and that can be safely added to
+{\Coq}. These axioms are stated in the directory {\tt Logic} of the
+standard library of {\Coq}. The most interesting ones are
+
+\begin{itemize}
+\item Excluded-middle: $\forall A:Prop, A \vee \neg A$
+\item Proof-irrelevance: $\forall A:Prop, \forall p_1 p_2:A, p_1=p_2$
+\item Unicity of equality proofs (or equivalently Streicher's axiom $K$)
+\item The principle of description: $\forall x, \exists! y, R(x,y) \rightarrow \exists f, \forall x, R(x,f(x))$
+\item The functional axiom of choice: $\forall x, \exists y, R(x,y) \rightarrow \exists f, \forall x, R(x,f(x))$
+\item Extensionality of predicates: $\forall P Q:A\rightarrow Prop, (\forall x, P(x) \leftrightarrow Q(x)) \rightarrow P=Q$
+\item Extensionality of functions: $\forall f g:A\rightarrow B, (\forall x, f(x)=g(x)) \rightarrow f=g$
+\end{itemize}
+
+Here is a summary of the relative strength of these axioms, most
+proofs can be found in directory {\tt Logic} of the standard library.
+
+\includegraphics{axioms}
+
+\Question{What standard axioms are inconsistent with {\Coq}?}
+
+The axiom of description together with classical logic
+(e.g. excluded-middle) are inconsistent in the variant of the Calculus
+of Inductive Constructions where {\Set} is impredicative.
+
+As a consequence, the functional form of the axiom of choice and
+excluded-middle, or any form of the axiom of choice together with
+predicate extensionality are inconsistent in the {\Set}-impredicative
+version of the Calculus of Inductive Constructions.
+
+The main purpose of the \Set-predicative restriction of the Calculus
+of Inductive Constructions is precisely to accommodate these axioms
+which are quite standard in mathematical usage.
+
+The $\Set$-predicative system is commonly considered consistent by
+interpreting it in a standard set-theoretic boolean model, even with
+classical logic, axiom of choice and predicate extensionality added.
+
+\Question{What is Streicher's axiom $K$}
+\label{Streicher}
+
+Streicher's axiom $K$ \cite{HofStr98} asserts dependent
+elimination of reflexive equality proofs.
+
+\begin{coq_example*}
+Axiom Streicher_K :
+  forall (A:Type) (x:A) (P: x=x -> Prop),
+    P (refl_equal x) -> forall p: x=x, P p.
+\end{coq_example*}
+
+In the general case, axiom $K$ is an independent statement of the
+Calculus of Inductive Constructions.  However, it is true on decidable
+domains (see file \vfile{\LogicEqdepDec}{Eqdep\_dec}). It is also
+trivially a consequence of proof-irrelevance (see
+\ref{proof-irrelevance}) hence of classical logic.
+
+Axiom $K$ is equivalent to {\em Uniqueness of Identity Proofs} \cite{HofStr98}
+
+\begin{coq_example*}
+Axiom UIP : forall (A:Set) (x y:A) (p1 p2: x=y), p1 = p2.
+\end{coq_example*}
+
+Axiom $K$ is also equivalent to {\em Uniqueness of Reflexive Identity Proofs} \cite{HofStr98}
+
+\begin{coq_example*}
+Axiom UIP_refl : forall (A:Set) (x:A) (p: x=x), p = refl_equal x.
+\end{coq_example*}
+
+Axiom $K$ is also equivalent to 
+
+\begin{coq_example*}
+Axiom
+  eq_rec_eq :
+    forall (A:Set) (x:A) (P: A->Set) (p:P x) (h: x=x),
+      p = eq_rect x P p x h.
+\end{coq_example*}
+
+It is also equivalent to the injectivity of dependent equality (dependent equality is itself equivalent to equality of dependent pairs).
+
+\begin{coq_example*}
+Inductive eq_dep (U:Set) (P:U -> Set) (p:U) (x:P p) :
+forall q:U, P q -> Prop :=
+    eq_dep_intro : eq_dep U P p x p x.
+Axiom
+  eq_dep_eq :
+    forall (U:Set) (u:U) (P:U -> Set) (p1 p2:P u),
+      eq_dep U P u p1 u p2 -> p1 = p2.
+\end{coq_example*}
+
+\Question{What is proof-irrelevance}
+\label{proof-irrelevance}
+
+A specificity of the Calculus of Inductive Constructions is to permit
+statements about proofs. This leads to the question of comparing two
+proofs of the same proposition. Identifying all proofs of the same
+proposition is called {\em proof-irrelevance}:
+$$
+\forall A:\Prop, \forall p q:A, p=q
+$$ 
+
+Proof-irrelevance (in {\Prop}) can be assumed without contradiction in
+{\Coq}. It corresponds to a model where provability, whatever the
+proof is, is more important than the computational content of the
+proof. This is in harmony with the common purely logical
+interpretation of {\Prop}. Contrastingly, proof-irrelevance is
+inconsistent in {\Set} in harmony with the computational meaning of
+the sort {\Set}.
+
+Proof-irrelevance (in {\Prop}) is a consequence of classical logic
+(see proofs in file \vfile{\LogicClassical}{Classical} and
+\vfile{\LogicBerardi}{Berardi}). Proof-irrelevance is also a
+consequence of propositional extensionality (i.e.  \coqtt{(A {\coqequiv} B)
+{\coqimp} A=B}, see the proof in file
+\vfile{\LogicClassicalFacts}{ClassicalFacts}).
+
+Conversely, proof-irrelevance directly implies Streicher's axiom $K$.
+
+\Question{What about functional extensionality?}
+
+Extensionality of functions is an axiom in, say set theory, but from a
+programing point of view, extensionality cannot be {\em a priori}
+accepted since it would identify, say programs such as mergesort and
+quicksort.
+
+%\begin{coq_example*}
+%  Axiom extensionality : (A,B:Set)(f,g:(A->B))(x:A)(f x)=(g x)->f=g.
+%\end{coq_example*}
+
+Let {\tt A}, {\tt B} be types. To deal with extensionality on 
+\verb=A->B=, the recommended approach is to define one's
+own extensional equality on \verb=A->B=.
+
+\begin{coq_eval}
+Variables A B : Set.
+\end{coq_eval}
+
+\begin{coq_example*}
+Definition ext_eq (f g: A->B) := forall x:A, f x = g x.
+\end{coq_example*}
+
+and to reason on \verb=A->B= as a setoid (see the Chapter on
+Setoids in the Reference Manual).
+
+\Question{Is {\Prop} impredicative?}
+
+Yes, the sort {\Prop} of propositions is {\em
+impredicative}. Otherwise said, a statement of the form $\forall
+A:Prop, P(A)$ can be instantiated by itself: if $\forall A:\Prop, P(A)$
+is provable, then $P(\forall A:\Prop, P(A))$ is.
+
+\Question{Is {\Set} impredicative?}
+
+No, the sort {\Set} lying at the bottom of the hierarchy of
+computational types is {\em predicative} in the basic {\Coq} system.
+This means that a family of types in {\Set}, e.g. $\forall A:\Set, A
+\rightarrow A$, is not a type in {\Set} and it cannot be applied on
+itself.
+
+However, the sort {\Set} was impredicative in the original versions of
+{\Coq}. For backward compatibility, or for experiments by
+knowledgeable users, the logic of {\Coq} can be set impredicative for
+{\Set} by calling {\Coq} with the option {\tt -impredicative-set}.
+
+{\Set} has been made predicative from version 8.0 of {\Coq}. The main
+reason is to interact smoothly with a classical mathematical world
+where both excluded-middle and the axiom of description are valid (see
+file \vfile{\LogicClassicalDescription}{ClassicalDescription} for a
+proof that excluded-middle and description implies the double negation
+of excluded-middle in {\Set} and file {\tt Hurkens\_Set.v} from the
+user contribution {\tt Rocq/PARADOXES} for a proof that
+impredicativity of {\Set} implies the simple negation of
+excluded-middle in {\Set}).
+
+\Question{Is {\Type} impredicative?}
+
+No, {\Type} is stratified. This is hidden for the
+user, but {\Coq} internally maintains a set of constraints ensuring
+stratification.
+
+If {\Type} were impredicative then it would be possible to encode
+Girard's systems $U-$ and $U$ in {\Coq} and it is known from Girard,
+Coquand, Hurkens and Miquel that systems $U-$ and $U$ are inconsistent
+[Girard 1972, Coquand 1991, Hurkens 1993, Miquel 2001]. This encoding
+can be found in file {\tt Logic/Hurkens.v} of {\Coq} standard library.
+
+For instance, when the user see {\tt $\forall$ X:Type, X->X : Type}, each
+occurrence of {\Type} is implicitly bound to a different level, say
+$\alpha$ and $\beta$ and the actual statement is {\tt
+forall X:Type($\alpha$), X->X : Type($\beta$)} with the constraint
+$\alpha<\beta$.
+
+When a statement violates a constraint, the message {\tt Universe
+inconsistency} appears. Example: {\tt fun (x:Type) (y:$\forall$ X:Type, X
+{\coqimp} X) => y x x}.
+
+\Question{I have two proofs of the same proposition. Can I prove they are equal?}
+
+In the base {\Coq} system, the answer is generally no. However, if
+classical logic is set, the answer is yes for propositions in {\Prop}.
+The answer is also yes if proof irrelevance holds (see question
+\ref{proof-irrelevance}).
+
+There are also ``simple enough'' propositions for which you can prove
+the equality without requiring any extra axioms.  This is typically
+the case for propositions defined deterministically as a first-order
+inductive predicate on decidable sets. See for instance in question
+\ref{le-uniqueness} an axiom-free proof of the unicity of the proofs of
+the proposition {\tt le m n} (less or equal on {\tt nat}).
+
+%  It is an ongoing work of research to natively include proof
+%  irrelevance in {\Coq}.
+
+\Question{I have two proofs of an equality statement. Can I prove they are 
+equal?}
+
+ Yes, if equality is decidable on the domain considered (which
+is the case for {\tt nat}, {\tt bool}, etc): see {\Coq} file
+\verb=Eqdep_dec.v=). No otherwise, unless
+assuming Streicher's axiom $K$ (see \cite{HofStr98}) or a more general
+assumption such as proof-irrelevance (see \ref{proof-irrelevance}) or
+classical logic.
+
+All of these statements can be found in file \vfile{\LogicEqdep}{Eqdep}.
+
+\Question{Can I prove that the second components of equal dependent
+pairs are equal?}
+
+ The answer is the same as for proofs of equality
+statements. It is provable if equality on the domain of the first
+component is decidable (look at \verb=inj_right_pair= from file
+\vfile{\LogicEqdepDec}{Eqdep\_dec}), but not provable in the general
+case. However, it is consistent (with the Calculus of Constructions)
+to assume it is true. The file \vfile{\LogicEqdep}{Eqdep} actually
+provides an axiom (equivalent to Streicher's axiom $K$) which entails
+the result (look at \verb=inj_pair2= in \vfile{\LogicEqdep}{Eqdep}).
+
+\subsection{Impredicativity}
+
+\Question{Why {\tt injection} does not work on impredicative {\tt Set}?}
+
+ E.g. in this case (this occurs only in the {\tt Set}-impredicative
+ variant of \Coq):
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+
+\begin{coq_example*}
+Inductive I : Type :=
+  intro : forall k:Set, k -> I.
+Lemma eq_jdef : 
+   forall x y:nat, intro _ x = intro _ y -> x = y.
+Proof.
+   intros x y H; injection H.
+\end{coq_example*}
+
+ Injectivity of constructors is restricted to predicative types. If
+injectivity on large inductive types were not restricted, we would be
+allowed to derive an inconsistency (e.g. following the lines of
+Burali-Forti paradox). The question remains open whether injectivity
+is consistent on some large inductive types not expressive enough to
+encode known paradoxes (such as type I above).
+
+
+\Question{What is a "large inductive definition"?}
+
+ An inductive definition in {\Prop} pr {\Set} is called large
+if its constructors embed sets or propositions. As an example, here is
+a large inductive type:
+
+\begin{coq_example*}
+Inductive sigST (P:Set -> Set) : Type :=
+  existST : forall X:Set, P X -> sigST P.
+\end{coq_example*}
+
+In the {\tt Set} impredicative variant of {\Coq}, large inductive
+definitions in {\tt Set} have restricted elimination schemes to
+prevent inconsistencies. Especially, projecting the set or the
+proposition content of a large inductive definition is forbidden. If
+it were allowed, it would be possible to encode e.g. Burali-Forti
+paradox \cite{Gir70,Coq85}.
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\section{Talkin' with the Rooster}
+
+
+%%%%%%%
+\subsection{My goal is ...,  how can I prove it?}
+
+
+\Question{My goal is a conjunction, how can I prove it?}
+
+Use some theorem or assumption or use the {\split} tactic.
+\begin{coq_example}
+Goal forall A B:Prop, A->B-> A/\B.
+intros.
+split.
+assumption.
+assumption.
+Qed.
+\end{coq_example}
+
+\Question{My goal contains a conjunction as an hypothesis, how can I use it?}
+
+If you want to decompose your hypothesis into other hypothesis you can use the {\decompose} tactic:
+
+\begin{coq_example}
+Goal forall A B:Prop, A/\B-> B.
+intros.
+decompose [and] H.
+assumption.
+Qed.
+\end{coq_example}
+
+
+\Question{My goal is a disjunction, how can I prove it?}
+
+You can prove the left part or the right part of the disjunction using
+{\left} or {\right} tactics. If you want to do a classical
+reasoning step, use the {\tt classic} axiom to prove the right part with the assumption
+that the left part of the disjunction is false.
+
+\begin{coq_example}
+Goal forall A B:Prop, A-> A\/B.
+intros.
+left.
+assumption.
+Qed.
+\end{coq_example}
+
+An example using classical reasoning:
+
+\begin{coq_example}
+Require Import Classical.
+
+Ltac classical_right := 
+match goal with 
+| _:_ |-?X1 \/ _ => (elim (classic X1);intro;[left;trivial|right])
+end.
+
+Ltac classical_left := 
+match goal with 
+| _:_ |- _ \/?X1 => (elim (classic X1);intro;[right;trivial|left])
+end.
+
+
+Goal forall A B:Prop, (~A -> B) -> A\/B.
+intros.
+classical_right.
+auto.
+Qed.
+\end{coq_example}
+
+\Question{My goal is an universally quantified statement, how can I prove it?}
+
+Use some theorem or assumption or introduce the quantified variable in
+the context using the {\intro} tactic. If there are several
+variables you can use the {\intros} tactic. A good habit is to
+provide names for these variables: {\Coq} will do it anyway, but such
+automatic naming decreases legibility and robustness.
+
+
+\Question{My goal is an existential, how can I prove it?}
+
+Use some theorem or assumption or exhibit the witness using the {\existstac} tactic.
+\begin{coq_example}
+Goal exists x:nat, forall y, x+y=y.
+exists 0.
+intros.
+auto.
+Qed.
+\end{coq_example}
+
+
+\Question{My goal is solvable by  some lemma, how can I prove it?}
+
+Just use the {\apply} tactic.
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+
+\begin{coq_example}
+Lemma mylemma : forall x, x+0 = x.
+auto.
+Qed.
+
+Goal 3+0 = 3.
+apply mylemma.
+Qed.
+\end{coq_example}
+
+
+
+\Question{My goal contains False as an hypotheses, how can I prove it?}
+
+You can use the {\contradiction} or {\intuition} tactics.
+
+
+\Question{My goal is an equality of two convertible terms, how can I prove it?}
+
+Just use the {\reflexivity} tactic.
+
+\begin{coq_example}
+Goal forall x, 0+x = x.
+intros.
+reflexivity.
+Qed.
+\end{coq_example}
+
+\Question{My goal is a {\tt let x := a in ...}, how can I prove it?}
+
+Just use the {\intro} tactic.
+
+
+\Question{My goal is a {\tt let (a, ..., b) := c in}, how can I prove it?}
+
+Just use the {\destruct} c as (a,...,b) tactic.
+
+
+\Question{My goal contains some existential hypotheses, how can I use it?}
+
+You can use the tactic {\elim} with you hypotheses as an argument.
+
+\Question{My goal contains some existential hypotheses, how can I use it and decompose my knowledge about this new thing into different hypotheses?}
+
+\begin{verbatim}
+Ltac DecompEx H P := elim H;intro P;intro TO;decompose [and] TO;clear TO;clear H.
+\end{verbatim}
+
+
+\Question{My goal is an equality, how can I swap the left and right hand terms?}
+
+Just use the {\symmetry} tactic.
+\begin{coq_example}
+Goal forall x y : nat, x=y -> y=x.
+intros.
+symmetry.
+assumption.
+Qed.
+\end{coq_example}
+
+\Question{My hypothesis is an equality, how can I swap the left and right hand terms?}
+
+Just use the {\symmetryin} tactic.
+
+\begin{coq_example}
+Goal forall x y : nat, x=y -> y=x.
+intros.
+symmetry in H.
+assumption.
+Qed.
+\end{coq_example}
+
+
+\Question{My goal is an equality, how can I prove it by transitivity?}
+
+Just use the {\transitivity} tactic.
+\begin{coq_example}
+Goal forall x y z : nat, x=y -> y=z -> x=z.
+intros.
+transitivity y.
+assumption.
+assumption.
+Qed.
+\end{coq_example}
+
+
+\Question{My goal would be solvable using {\tt apply;assumption} if it would not create meta-variables, how can I prove it?}
+
+You can use {\tt eapply yourtheorem;eauto} but it won't work in all cases ! (for example if more than one hypothesis match one of the subgoals generated by \eapply) so you should rather use  {\tt try solve [eapply yourtheorem;eauto]}, otherwise some metavariables may be incorrectly instantiated.
+
+\begin{coq_example}
+Lemma trans : forall x y z : nat, x=y -> y=z -> x=z.
+intros.
+transitivity y;assumption.
+Qed.
+
+Goal forall x y z : nat, x=y -> y=z -> x=z.
+intros.
+eapply trans;eauto.
+Qed.
+
+Goal forall x y z t : nat, x=y -> x=t -> y=z -> x=z.
+intros.
+eapply trans;eauto.
+Undo.
+eapply trans.
+apply H.
+auto.
+Qed.
+
+Goal forall x y z t : nat, x=y -> x=t -> y=z -> x=z.
+intros.
+eapply trans;eauto.
+Undo.
+try solve [eapply trans;eauto].
+eapply trans.
+apply H.
+auto.
+Qed.
+
+\end{coq_example}
+
+\Question{My goal is solvable by  some lemma within a set of lemmas and I don't want to remember which one, how can I prove it?}
+
+You can use a what is called a hints' base.
+
+\begin{coq_example}
+Require Import ZArith.
+Require Ring.
+Open Local Scope Z_scope.
+Lemma toto1 : 1+1 = 2.
+ring.
+Qed.
+Lemma toto2 : 2+2 = 4.
+ring.
+Qed.
+Lemma toto3 : 2+1 = 3.
+ring.
+Qed.
+
+Hint Resolve toto1 toto2 toto3 : mybase.
+
+Goal 2+(1+1)=4. 
+auto with mybase.
+Qed.
+\end{coq_example}
+
+
+\Question{My goal is one of the hypotheses, how can I prove it?}
+
+Use the {\assumption} tactic.
+
+\begin{coq_example}
+Goal 1=1 -> 1=1.
+intro.
+assumption.
+Qed.
+\end{coq_example}
+
+
+\Question{My goal appears twice in the hypotheses and I want to choose which one is used, how can I do it?}
+
+Use the {\exact} tactic.
+\begin{coq_example}
+Goal 1=1 -> 1=1 -> 1=1.
+intros.
+exact H0.
+Qed.
+\end{coq_example}
+
+\Question{What can be the difference between applying one hypothesis or another in the context of the last question?}
+
+From a proof point of view it is equivalent but if you want to extract
+a program from your proof, the two hypotheses can lead to different
+programs.
+
+
+\Question{My goal is a propositional tautology, how can I prove it?}
+
+Just use the {\tauto} tactic.
+\begin{coq_example}
+Goal forall A B:Prop, A-> (A\/B) /\ A.
+intros.
+tauto.
+Qed.
+\end{coq_example}
+
+\Question{My goal is a first order formula, how can I prove it?}
+
+Just use the semi-decision tactic: \firstorder.
+
+\iffalse
+todo: demander un exemple à Pierre
+\fi
+
+\Question{My goal is solvable by a sequence of rewrites, how can I prove it?}
+
+Just use the {\congruence} tactic.
+\begin{coq_example}
+Goal forall a b c d e, a=d -> b=e -> c+b=d -> c+e=a.
+intros.
+congruence.
+Qed.
+\end{coq_example}
+
+
+\Question{My goal is a disequality solvable by a sequence of rewrites, how can I prove it?}
+
+Just use the {\congruence} tactic.
+
+\begin{coq_example}
+Goal forall a b c d, a<>d -> b=a -> d=c+b -> b<>c+b.
+intros.
+congruence.
+Qed.
+\end{coq_example}
+
+
+\Question{My goal is an equality on some ring (e.g. natural numbers), how can I prove it?}
+
+Just use the {\ring} tactic.
+
+\begin{coq_example}
+Require Import ZArith.
+Require Ring.
+Open Local Scope Z_scope.
+Goal forall a b : Z, (a+b)*(a+b) = a*a + 2*a*b + b*b. 
+intros.
+ring.
+Qed.
+\end{coq_example}
+
+\Question{My goal is an equality on some field (e.g. real numbers), how can I prove it?}
+
+Just use the {\field} tactic.
+
+\begin{coq_example}
+Require Import Reals.
+Require Ring.
+Open Local Scope R_scope.
+Goal forall a b : R, b*a<>0 -> (a/b) * (b/a) = 1. 
+intros.
+field.
+assumption.
+Qed.
+\end{coq_example}
+
+
+\Question{My goal is an inequality on integers in Presburger's arithmetic (an expression build from +,-,constants and variables), how can I prove it?}
+
+
+\begin{coq_example}
+Require Import ZArith.
+Require Omega.
+Open Local Scope Z_scope.
+Goal forall a : Z, a>0 -> a+a > a. 
+intros.
+omega.
+Qed.
+\end{coq_example}
+
+
+\Question{My goal is an equation solvable using equational hypothesis on some ring (e.g. natural numbers), how can I prove it?}
+
+You need the {\gb} tactic (see Loïc Pottier's homepage).
+
+\subsection{Tactics usage}
+
+\Question{I want to state a fact that I will use later as an hypothesis, how can I do it?}
+
+If you want to use forward reasoning (first proving the fact and then
+using it) you just need to use the {\assert} tactic. If you want to use
+backward reasoning (proving your goal using an assumption and then
+proving the assumption) use the {\cut} tactic.
+
+\begin{coq_example}
+Goal forall A B C D : Prop, (A -> B) -> (B->C) -> A -> C. 
+intros.
+assert (A->C).
+intro;apply H0;apply H;assumption.
+apply H2.
+assumption.
+Qed.
+
+Goal forall A B C D : Prop, (A -> B) -> (B->C) -> A -> C. 
+intros.
+cut (A->C).
+intro.
+apply H2;assumption.
+intro;apply H0;apply H;assumption.
+Qed.
+\end{coq_example}
+
+
+
+
+\Question{I want to state a fact that I will use later as an hypothesis and prove it later, how can I do it?}
+
+You can use {\cut} followed by {\intro} or you can use the following {\Ltac} command:
+\begin{verbatim}
+Ltac assert_later t := cut t;[intro|idtac]. 
+\end{verbatim}
+
+\Question{What is the difference between {\Qed} and {\Defined}?}
+
+These two commands perform type checking, but when {\Defined} is used the new definition is set as transparent, otherwise it is defined as opaque (see \ref{opaque}).
+
+
+\Question{How can I know what a tactic does?}
+
+You can use the {\tt info} command.
+
+
+
+\Question{Why {\auto} does not work? How can I fix it?}
+
+You can increase the depth of the proof search or add some lemmas in the base of hints.
+Perhaps you may need to use \eauto.
+
+\Question{What is {\eauto}?}
+
+This is the same tactic as \auto, but it relies on {\eapply} instead of \apply.
+
+\iffalse
+todo les espaces
+\fi
+
+\Question{How can I speed up {\auto}?}
+
+You can use \texttt{info }\auto to replace {\auto} by the tactics it generates.
+You can split your hint bases into smaller ones.
+
+
+\Question{What is the equivalent of {\tauto} for classical logic?}
+
+Currently there are no equivalent tactic for classical logic. You can use Gödel's ``not not'' translation.
+
+
+\Question{I want to replace some term with another in the goal, how can I do it?}
+
+If one of your hypothesis (say {\tt H}) states that the terms are equal you can use the {\rewrite} tactic. Otherwise you can use the {\replace} {\tt with} tactic. 
+
+\Question{I want to replace some term with another in an hypothesis, how can I do it?}
+
+You can use the {\rewrite} {\tt in} tactic.
+
+\Question{I want to replace some symbol with its definition, how can I do it?}
+
+You can use the {\unfold} tactic.
+
+\Question{How can I reduce some term?}
+
+You can use the {\simpl} tactic.
+
+\Question{How can I declare a shortcut for some term?}
+
+You can use the {\set} or {\pose} tactics.
+
+\Question{How can I perform case analysis?}
+
+You can use the {\case} or {\destruct} tactics.
+
+
+\Question{Why should I name my intros?}
+
+When you use the {\intro} tactic you don't have to give a name to your
+hypothesis. If you do so the name will be generated by {\Coq} but your
+scripts may be less robust. If you add some hypothesis to your theorem
+(or change their order), you will have to change your proof to adapt
+to the new names.
+
+\Question{How can I automatize the naming?}
+
+You can use the {\tt Show Intro.} or  {\tt Show Intros.} commands to generate the names and use your editor to generate a fully named {\intro} tactic. 
+This can be automatized within {\tt xemacs}.
+
+\begin{coq_example}
+Goal forall A B C : Prop, A -> B -> C -> A/\B/\C.
+Show Intros.
+(*
+A B C H H0
+H1
+*)
+intros A B C H H0 H1.
+repeat split;assumption.
+Qed.
+\end{coq_example}
+
+\Question{I want to automatize the use of some tactic, how can I do it?}
+
+You need to use the {\tt proof with T} command and add {\ldots} at the
+end of your sentences.
+
+For instance:
+\begin{coq_example}
+Goal forall A B C : Prop, A -> B/\C -> A/\B/\C.
+Proof with assumption.
+intros.
+split...
+Qed.
+\end{coq_example}
+
+\Question{I want to execute the {\texttt proof with} tactic only if it solves the goal, how can I do it?}
+
+You need to use the {\try} and {\solve} tactics. For instance:
+\begin{coq_example}
+Require Import ZArith.
+Require Ring.
+Open Local Scope Z_scope.
+Goal forall a b c : Z, a+b=b+a.
+Proof with try solve [ring].
+intros...
+Qed.
+\end{coq_example}
+
+\Question{How can I do the opposite of the {\intro} tactic?}
+
+You can use the {\generalize} tactic.
+
+\begin{coq_example}
+Goal forall A B : Prop, A->B-> A/\B.
+intros.
+generalize H.
+intro.
+auto.
+Qed.
+\end{coq_example}
+
+\Question{One of the hypothesis is an equality between a variable and some term, I want to get rid of this variable, how can I do it?}
+
+You can use the {\subst} tactic. This will rewrite the equality everywhere and clear the assumption.
+
+\Question{What can I do if I get ``{\tt generated subgoal term has metavariables in it }''?}
+
+You should use the {\eapply} tactic, this will generate some goals containing metavariables. 
+
+\Question{How can I instantiate some metavariable?}
+
+Just use the {\instantiate} tactic.
+
+
+\Question{What is the use of the {\pattern} tactic?}
+
+The {\pattern} tactic transforms the current goal, performing
+beta-expansion on all the applications featuring this tactic's
+argument. For instance, if the current goal includes a subterm {\tt
+phi(t)}, then {\tt pattern t} transforms the subterm into {\tt (fun
+x:A => phi(x)) t}. This can be useful when {\apply} fails on matching,
+to abstract the appropriate terms.
+
+\Question{What is the difference between assert, cut and generalize?}
+
+PS: Notice for people that are interested in proof rendering that \assert
+and {\pose} (and \cut) are not rendered the same as {\generalize} (see the
+HELM experimental rendering tool at \ahref{http://helm.cs.unibo.it/library.html}{\url{http://helm.cs.unibo.it}}, link
+HELM, link COQ Online). Indeed {\generalize} builds a beta-expanded term
+while \assert, {\pose} and {\cut} uses a let-in.
+
+\begin{verbatim}
+  (* Goal is T *)
+  generalize (H1 H2).
+  (* Goal is A->T *)
+  ... a proof of A->T ...
+\end{verbatim}
+
+is rendered into something like
+\begin{verbatim}
+  (h) ... the proof of A->T ...
+      we proved A->T
+  (h0) by (H1 H2) we proved A
+  by (h h0) we proved T
+\end{verbatim}
+while 
+\begin{verbatim}
+  (* Goal is T *)
+  assert q := (H1 H2).
+  (* Goal is A *)
+  ... a proof of A ...
+  (* Goal is A |- T *)
+  ... a proof of T ...
+\end{verbatim}
+is rendered into something like
+\begin{verbatim}
+  (q) ... the proof of A ...
+      we proved A
+  ... the proof of T ...
+  we proved T
+\end{verbatim}
+Otherwise said, {\generalize} is not rendered in a forward-reasoning way,
+while {\assert} is.
+
+\Question{What can I do if \Coq can not infer some implicit argument ?}
+
+You can state explicitely what this implicit argument is. See \ref{implicit}.
+
+\Question{How can I explicit some implicit argument ?}\label{implicit}
+
+Just use \texttt{A:=term} where \texttt{A} is the argument.
+
+For instance if you want to use the existence of ``nil'' on nat*nat lists:
+\begin{verbatim}
+exists (nil (A:=(nat*nat))).
+\end{verbatim}
+
+\iffalse
+\Question{Is there anyway to do pattern matching with dependent types?}
+
+todo
+\fi
+
+\subsection{Proof management}
+
+
+\Question{How can I change the order of the subgoals?}
+
+You can use the {\Focus} command to concentrate on some goal. When the goal is proved you will see the remaining goals.
+
+\Question{How can I change the order of the hypothesis?}
+
+You can use the {\tt Move ... after} command.
+
+\Question{How can I change the name of an hypothesis?}
+
+You can use the {\tt Rename ... into} command.
+
+\Question{How can I delete some hypothesis?}
+
+You can use the {\tt Clear} command.
+
+\Question{How can use a proof which is not finished?}
+
+You can use the {\tt Admitted} command to state your current proof as an axiom.
+
+\Question{How can I state a conjecture?}
+
+You can use the {\tt Admitted} command to state your current proof as an axiom.
+
+\Question{What is the difference between a lemma, a fact and a theorem?}
+
+From {\Coq} point of view there are no difference. But some tools can
+have a different behavior when you use a lemma rather than a
+theorem. For instance {\tt coqdoc} will not generate documentation for
+the lemmas within your development.
+
+\Question{How can I organize my proofs?}
+
+You can organize your proofs using the section mechanism of \Coq. Have
+a look at the manual for further information.
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\section{Inductive and Co-inductive types}
+
+\subsection{General}
+
+\Question{How can I prove that two constructors are different?}
+
+You can use the {\discriminate} tactic.
+
+\begin{coq_example}
+Inductive toto : Set := | C1 : toto | C2 : toto.
+Goal C1 <> C2.
+discriminate.
+Qed.
+\end{coq_example}
+
+\Question{During an inductive proof, how to get rid of impossible cases of an inductive definition?}
+
+Use the {\inversion} tactic.
+
+
+\Question{How can I prove that 2 terms in an inductive set are equal? Or different?}
+
+Have a look at "decide equality" and "discriminate" in the \ahref{http://coq.inria.fr/doc/main.html}{Reference Manual}.
+
+\Question{Why is the proof of \coqtt{0+n=n} on natural numbers
+trivial but the proof of \coqtt{n+0=n} is not?}
+
+ Since \coqtt{+} (\coqtt{plus}) on natural numbers is defined by analysis on its first argument
+
+\begin{coq_example}
+Print plus.
+\end{coq_example}
+
+{\noindent} The expression \coqtt{0+n} evaluates to \coqtt{n}. As {\Coq} reasons
+modulo evaluation of expressions, \coqtt{0+n} and \coqtt{n} are
+considered equal and the theorem \coqtt{0+n=n} is an instance of the
+reflexivity of equality. On the other side, \coqtt{n+0} does not
+evaluate to \coqtt{n} and a proof by induction on \coqtt{n} is
+necessary to trigger the evaluation of \coqtt{+}.
+
+\Question{Why is dependent elimination in Prop not
+available by default?}
+
+ 
+This is just because most of the time it is not needed. To derive a
+dependent elimination principle in {\tt Prop}, use the command {\tt Scheme} and
+apply the elimination scheme using the \verb=using= option of
+\verb=elim=, \verb=destruct= or \verb=induction=.
+
+
+\Question{Argh! I cannot write expressions like ``~{\tt if n <= p then p else n}~'', as in any programming language}
+\label{minmax}
+
+The short answer : You should use {\texttt le\_lt\_dec n p} instead.\\
+
+That's right, you can't.
+If you type for instance the following ``definition'':
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+\begin{coq_example}
+Definition max (n p : nat) := if n <= p then p else n.
+\end{coq_example}
+
+As \Coq~ says, the term ``~\texttt{n <= p}~'' is a proposition, i.e. a
+statement that belongs to the mathematical world. There are many ways to
+prove such a proposition, either by some computation, or using some already
+proven theoremas. For instance, proving $3-2 \leq 2^{45503}$ is very easy,
+using some theorems on arithmetical operations. If you compute both numbers
+before comparing them, you risk to use a lot of time and space.
+
+
+On the contrary, a function for computing the greatest of two natural numbers
+is an algorithm  which, called on two natural numbers
+$n$ and $p$, determines wether $n\leq p$ or $p < n$.
+Such a function is a \emph{decision  procedure} for the inequality of
+ \texttt{nat}.  The possibility of writing such a procedure comes 
+directly from de decidability of the order $\leq$ on natural numbers.
+
+
+When you write a piece of code like 
+``~\texttt{if n <= p then \dots{} else \dots}~''
+in a
+programming language like \emph{ML} or \emph{Java}, a call to such a 
+decision procedure is generated. The decision procedure is in general
+a primitive function, written in a low-level language, in the correctness
+of which you have to trust.
+
+The standard Library of the system \emph{Coq} contains a  
+(constructive) proof of decidability of the order $\leq$ on
+\texttt{nat} : the function \texttt{le\_lt\_dec} of 
+the module \texttt{Compare\_dec} of library \texttt{Arith}.
+
+The following code shows how to define correctly \texttt{min} and
+\texttt{max}, and prove some properties of these functions.
+
+\begin{coq_example}
+Require Import Compare_dec.
+
+Definition max (n p : nat) := if le_lt_dec n p then p else n.
+
+Definition min (n p : nat) := if le_lt_dec n p then n else p.
+
+Eval compute in (min 4 7).
+
+Theorem min_plus_max : forall n p, min n p + max n p  = n + p.
+Proof.
+ intros n p; 
+ unfold min, max; 
+ case (le_lt_dec n p);
+ simpl; auto with arith.
+Qed.
+
+Theorem max_equiv : forall n p, max n p = p <-> n <= p.
+Proof.
+ unfold max; intros n p; case (le_lt_dec n p);simpl; auto.
+ intuition auto with arith.
+ split. 
+ intro e; rewrite e; auto with arith.
+ intro H; absurd (p < p); eauto with arith.
+Qed.
+\end{coq_example}
+
+\Question{I wrote my own decision procedure for $\leq$, which
+is much  faster than yours, but proving such theorems as
+ \texttt{max\_equiv} seems to be quite difficult}
+
+Your code is probably the following one:
+
+\begin{coq_example}
+Fixpoint my_le_lt_dec (n p :nat) {struct n}: bool  :=
+ match n, p with 0, _ => true
+               | S n', S p' => my_le_lt_dec n' p'
+               | _   , _    => false
+ end.
+
+Definition my_max (n p:nat) := if my_le_lt_dec n p then p else n.
+
+Definition my_min (n p:nat) := if my_le_lt_dec n p then n else p.
+\end{coq_example}
+
+
+For instance, the computation of \texttt{my\_max 567 321} is almost
+immediate, whereas one can't wait for  the result of 
+\texttt{max 56 32}, using \emph{Coq's} \texttt{le\_lt\_dec}.
+
+This is normal. Your definition is a simple recursive function which
+returns a boolean value. Coq's \texttt{le\_lt\_dec} is a \emph{certified
+function}, i.e. a complex object, able not only to tell wether $n\leq p$
+or $p<n$, but also of building a complete proof of the correct inequality.
+What make \texttt{le\_lt\_dec} inefficient for computing \texttt{min}
+and \texttt{max} is the building of a huge proof term.
+
+Nevertheless,  \texttt{le\_lt\_dec} is very useful. Its type 
+is a strong specification, using the
+\texttt{sumbool} type (look at the reference manual or chapter 9 of
+\cite{coqart}). Eliminations of the form
+``~\texttt{case (le\_lt\_dec n p)}~'' provide proofs of
+either $n \leq p$ or $p < n$, allowing to prove easily theorems as in
+question~\ref{minmax}. Unfortunately, this not the case of your
+\texttt{my\_le\_lt\_dec}, which returns a quite non-informative boolean
+value.
+
+
+\begin{coq_example}
+Check le_lt_dec.
+\end{coq_example}
+
+You should keep in mind that \texttt{le\_lt\_dec} is useful to build
+certified programs which need to compare natural numbers, and is not
+designed to compare quickly two numbers.
+
+Nevertheless, the \emph{extraction} of \texttt{le\_lt\_dec} towards 
+\emph{Ocaml} or \emph{Haskell}, is a reasonable program for comparing two
+natural numbers in Peano form in linear time.
+
+It is also possible to keep your boolean function as a decision procedure,
+but you have to establish yourself the relationship between \texttt{my\_le\_lt\_dec} and the propositions $n\leq p$ and $p<n$:
+
+\begin{coq_example*}
+Theorem my_le_lt_dec_true : 
+    forall n p, my_le_lt_dec n p = true <-> n <= p.
+
+Theorem  my_le_lt_dec_false : 
+   forall n p, my_le_lt_dec n p = false <-> p < n.
+\end{coq_example*}
+
+
+\subsection{Recursion}
+
+\Question{Why can't I define a non terminating program?}
+
+ Because otherwise the decidability of the type-checking
+algorithm (which involves evaluation of programs) is not ensured.  On
+another side, if non terminating proofs were allowed, we could get a
+proof of {\tt False}:
+
+\begin{coq_example*}
+(* This is fortunately not allowed! *)
+Fixpoint InfiniteProof (n:nat) : False := InfiniteProof n.
+Theorem Paradox : False.
+Proof (InfiniteProof O).
+\end{coq_example*}
+
+
+\Question{Why only structurally well-founded loops are allowed?}
+
+ The structural order on inductive types is a simple and
+powerful notion of termination. The consistency of the Calculus of
+Inductive Constructions relies on it and another consistency proof
+would have to be made for stronger termination arguments (such
+as the termination of the evaluation of CIC programs themselves!).
+
+In spite of this, all non-pathological termination orders can be mapped
+to a structural order. Tools to do this are provided in the file 
+\vfile{\InitWf}{Wf} of the standard library of {\Coq}.
+
+\Question{How to define loops based on non structurally smaller
+recursive calls?}
+
+ The procedure is as follows (we consider the definition of {\tt
+mergesort} as an example).
+
+\begin{itemize}
+
+\item Define the termination order, say {\tt R} on the type {\tt A} of
+the arguments of the loop.
+
+\begin{coq_eval}
+Open Scope R_scope.
+Require Import List.
+\end{coq_eval}
+
+\begin{coq_example*}
+Definition R (a b:list nat) := length a < length b.
+\end{coq_example*}
+
+\item Prove that this order is well-founded (in fact that all elements in {\tt A} are accessible along {\tt R}).
+
+\begin{coq_example*}
+Lemma Rwf : well_founded (A:=R).
+\end{coq_example*}
+
+\item Define the step function (which needs proofs that recursive
+calls are on smaller arguments).
+
+\begin{coq_example*}
+Definition split (l : list nat) 
+   : {l1: list nat | R l1 l} * {l2 : list nat | R l2 l}
+   := (* ... *) .
+Definition concat (l1 l2 : list nat) : list nat := (* ... *) .
+Definition merge_step (l : list nat) (f: forall l':list nat, R l' l -> list nat) :=
+  let (lH1,lH2) := (split l) in
+  let (l1,H1) := lH1 in
+  let (l2,H2) := lH2 in
+  concat (f l1 H1) (f l2 H2).
+\end{coq_example*}
+
+\item Define the recursive function by fixpoint on the step function.
+
+\begin{coq_example*}
+Definition merge := Fix Rwf (fun _ => list nat) merge_step.
+\end{coq_example*}
+
+\end{itemize}
+
+\Question{What is behind the accessibility and well-foundedness proofs?}
+
+ Well-foundedness of some relation {\tt R} on some type {\tt A}
+is defined as the accessibility of all elements of {\tt A} along {\tt R}.
+
+\begin{coq_example}
+Print well_founded.
+Print Acc.
+\end{coq_example}
+
+The structure of the accessibility predicate is a well-founded tree
+branching at each node {\tt x} in {\tt A} along all the nodes {\tt x'}
+less than {\tt x} along {\tt R}. Any sequence of elements of {\tt A}
+decreasing along the order {\tt R} are branches in the accessibility
+tree. Hence any decreasing along {\tt R} is mapped into a structural
+decreasing in the accessibility tree of {\tt R}. This is emphasised in
+the definition of {\tt fix} which recurs not on its argument {\tt x:A}
+but on the accessibility of this argument along {\tt R}.
+
+See file \vfile{\InitWf}{Wf}.
+
+\Question{How to perform simultaneous double induction?}
+
+ In general a (simultaneous) double induction is simply solved by an
+induction on the first hypothesis followed by an inversion over the
+second hypothesis. Here is an example
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+
+\begin{coq_example}
+Inductive even : nat -> Prop :=
+  | even_O : even 0
+  | even_S : forall n:nat, even n -> even (S (S n)).
+
+Inductive odd : nat -> Prop :=
+  | odd_SO : odd 1
+  | odd_S : forall n:nat, odd n -> odd (S (S n)).
+
+Lemma not_even_and_odd : forall n:nat, even n -> odd n -> False.
+induction 1.
+  inversion 1.
+  inversion 1. apply IHeven; trivial.
+\end{coq_example}
+\begin{coq_eval}
+Qed.
+\end{coq_eval}
+
+In case the type of the second induction hypothesis is not
+dependent, {\tt inversion} can just be replaced by {\tt destruct}.
+
+\Question{How to define a function by simultaneous double recursion?}
+
+ The same trick applies, you can even use the pattern-matching
+compilation algorithm to do the work for you. Here is an example:
+
+\begin{coq_example}
+Fixpoint minus (n m:nat) {struct n} : nat :=
+  match n, m with
+  | O, _ => 0
+  | S k, O => S k
+  | S k, S l => minus k l
+  end.
+Print  minus.
+\end{coq_example}
+
+In case of dependencies in the type of the induction objects
+$t_1$ and $t_2$, an extra argument stating $t_1=t_2$ must be given to
+the fixpoint definition
+
+\Question{How to perform nested and double induction?}
+
+ To reason by nested (i.e. lexicographic) induction, just reason by
+induction on the successive components.
+
+\smallskip
+
+Double induction (or induction on pairs) is a restriction of the
+lexicographic induction. Here is an example of double induction.
+
+\begin{coq_example}
+Lemma nat_double_ind : 
+forall P : nat -> nat -> Prop, P 0 0 -> 
+  (forall m n, P m n -> P m (S n)) -> 
+  (forall m n, P m n -> P (S m) n) -> 
+     forall m n, P m n.
+intros P H00 HmS HSn; induction m.
+(* case 0 *)
+induction n; [assumption | apply HmS; apply IHn].
+(* case Sm *)
+intro n; apply HSn; apply IHm.
+\end{coq_example}
+\begin{coq_eval}
+Qed.
+\end{coq_eval}
+
+\Question{How to define a function by nested recursion?}
+
+ The same trick applies. Here is the example of Ackermann
+function.
+
+\begin{coq_example}
+Fixpoint ack (n:nat) : nat -> nat :=
+  match n with
+  | O => S
+  | S n' =>
+     (fix ack' (m:nat) : nat :=
+        match m with
+        | O => ack n' 1
+        | S m' => ack n' (ack' m')
+        end)
+  end.
+\end{coq_example}
+
+
+\subsection{Co-inductive types}
+
+\Question{I have a cofixpoint $t:=F(t)$ and I want to prove $t=F(t)$. How to do it?}
+
+Just case-expand $F({\tt t})$ then complete by a trivial case analysis.
+Here is what it gives on e.g. the type of streams on naturals
+
+\begin{coq_eval}
+Set Implicit Arguments.
+\end{coq_eval}
+\begin{coq_example}
+CoInductive Stream (A:Set) : Set :=
+  Cons : A -> Stream A -> Stream A.
+CoFixpoint nats (n:nat) : Stream nat := Cons n (nats (S n)).
+Lemma Stream_unfold : 
+   forall n:nat, nats n = Cons n (nats (S n)).
+Proof.
+  intro;
+  change (nats n = match nats n with
+                  | Cons x s => Cons x s
+                  end).
+  case (nats n); reflexivity.
+Qed.
+\end{coq_example}
+
+
+
+\section{Syntax and notations}
+
+\Question{I do not want to type ``forall'' because it is too long, what can I do?}
+
+You can define your own notation for forall:
+\begin{verbatim}
+Notation "fa x : t, P" := (forall x:t, P) (at level 200, x ident).
+\end{verbatim}
+or if your are using {\CoqIde} you can define a pretty symbol for for all and an input method (see \ref{forallcoqide}).
+
+
+
+\Question{How can I define a notation for square?}
+
+You can use for instance:
+\begin{verbatim}
+Notation "x ^2" := (Rmult x x) (at level 20).
+\end{verbatim}
+Note that you can not use:
+\begin{texttt}
+Notation "x $^²$" := (Rmult x x) (at level 20).
+\end{texttt}
+because ``$^2$'' is an iso-latin character. If you really want this kind of notation you should use UTF-8.
+
+
+\Question{Why ``no associativity'' and  ``left associativity'' at the same level does not work?}
+
+Because we relie on camlp4 for syntactical analysis and camlp4 does not really implement no associativity. By default, non associative operators are defined as right associative.
+
+
+
+\Question{How can I know the associativity associated with a level?}
+
+You can do ``Print Grammar constr'', and decode the output from camlp4, good luck !
+
+\section{Modules}
+
+
+
+
+%%%%%%%
+\section{\Ltac}
+
+\Question{What is {\Ltac}?}
+
+{\Ltac} is the tactic language for \Coq. It provides the user with a
+high-level ``toolbox'' for tactic creation.
+
+\Question{Why do I always get the same error message?}
+
+
+\Question{Is there any printing command in {\Ltac}?}
+
+You can use the {\idtac} tactic with a string argument. This string
+will be printed out. The same applies to the {\fail} tactic
+
+\Question{What is the syntax for let in {\Ltac}?}
+
+If $x_i$ are identifiers and $e_i$ and $expr$ are tactic expressions, then let reads:
+\begin{center}
+{\tt let $x_1$:=$e_1$ with $x_2$:=$e_2$\ldots with $x_n$:=$e_n$ in
+$expr$}.
+\end{center}
+Beware that if $expr$ is complex (i.e. features at least a sequence) parenthesis
+should be added around it. For example: 
+\begin{coq_example}
+Ltac twoIntro := let x:=intro in (x;x).
+\end{coq_example}
+
+\Question{What is the syntax for pattern matching in {\Ltac}?}
+
+Pattern matching on a term $expr$ (non-linear first order unification)
+with patterns $p_i$ and tactic expressions $e_i$ reads:
+\begin{center}
+\hspace{10ex}
+{\tt match $expr$ with
+\hspace*{2ex}$p_1$ => $e_1$
+\hspace*{1ex}\textbar$p_2$ => $e_2$
+\hspace*{1ex}\ldots
+\hspace*{1ex}\textbar$p_n$ => $e_n$
+\hspace*{1ex}\textbar\ \textunderscore\ => $e_{n+1}$
+end.
+}
+\end{center}
+Underscore matches all terms.
+
+\Question{What is the semantics for ``match goal''?}
+
+The semantics of {\tt match goal} depends on whether it returns
+tactics or not.  The {\tt match goal} expression matches the current
+goal against a series of patterns: {$hyp_1 {\ldots} hyp_n$ \textbar-
+$ccl$}. It uses a first-order unification algorithm and in case of
+success, if the right-hand-side is an expression, it tries to type it
+while if the right-hand-side is a tactic, it tries to apply it.  If the
+typing or the tactic application fails, the {\tt match goal} tries all
+the possible combinations of $hyp_i$ before dropping the branch and
+moving to the next one. Underscore matches all terms.
+
+\Question{Why can't I use a ``match goal'' returning a tactic in a non
+tail-recursive position?}
+
+This is precisely because the semantics of {\tt match goal} is to
+apply the tactic on the right as soon as a pattern unifies what is
+meaningful only in tail-recursive uses.
+
+The semantics in non tail-recursive call could have been the one used
+for terms (i.e. fail if the tactic expression is not typable, but
+don't try to apply it). For uniformity of semantics though, this has
+been rejected.
+
+\Question{How can I generate a new name?}
+
+You can use the following syntax:
+{\tt let id:=fresh in \ldots}\\
+For example:
+\begin{coq_example}
+Ltac introIdGen := let id:=fresh in intro id.
+\end{coq_example}
+
+
+\iffalse
+\Question{How can I access the type of a term?}
+
+You can use typeof.
+todo
+\fi
+
+\Question{How can I define static and dynamic code?}
+
+\section{Tactics written in Ocaml}
+
+\Question{Can you show me an example of a tactic written in OCaml?}
+
+You have some examples of tactics written in Ocaml in the ``contrib'' directory of {\Coq} sources. 
+
+
+
+
+\section{Case studies}
+
+
+\Question{How can I define vectors or lists of size n?}
+
+\Question{How to prove that 2 sets are different?}
+
+ You need to find a property true on one set and false on the
+other one. As an example we show how to prove that {\tt bool} and {\tt
+nat} are discriminable. As discrimination property we take the
+property to have no more than 2 elements.
+
+\begin{coq_example*}
+Theorem nat_bool_discr : bool <> nat.
+Proof.
+  pose (discr :=
+    fun X:Set =>
+      ~ (forall a b:X, ~ (forall x:X, x <> a -> x <> b -> False))).
+  intro Heq; assert (H: discr bool).
+  intro H; apply (H true false); destruct x; auto.
+  rewrite Heq in H; apply H; clear H.
+  destruct a; destruct b as [|n]; intro H0; eauto.
+  destruct n; [ apply (H0 2); discriminate | eauto ].
+Qed.
+\end{coq_example*}
+
+\Question{Is there an axiom-free proof of Streicher's axiom $K$ for
+the equality on {\tt nat}?}
+\label{K-nat}
+
+Yes, because equality is decidable on {\tt nat}. Here is the proof.
+
+\begin{coq_example*}
+Require Import Eqdep_dec.
+Require Import Peano_dec.
+Theorem K_nat :
+  forall (x:nat) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p.
+Proof.
+intros; apply K_dec_set with (p := p).
+apply eq_nat_dec.
+assumption.
+Qed.
+\end{coq_example*}
+
+Similarly, we have
+
+\begin{coq_example*}
+Theorem eq_rect_eq_nat :
+  forall (p:nat) (Q:nat->Type) (x:Q p) (h:p=p), x = eq_rect p Q x p h.
+Proof.
+intros; apply K_nat with (p := h); reflexivity.
+Qed.
+\end{coq_example*}
+
+\Question{How to prove that two proofs of {\tt n<=m} on {\tt nat} are equal?}
+\label{le-uniqueness}
+
+This is provable without requiring any axiom because axiom $K$
+directly holds on {\tt nat}. Here is a proof using question \ref{K-nat}.
+
+\begin{coq_example*}
+Scheme le_ind' := Induction for le Sort Prop.
+Theorem le_uniqueness_proof : forall (n m : nat) (p q : n <= m), p = q.
+Proof.
+induction p using le_ind'; intro q.
+ replace (le_n n) with
+  (eq_rect _ (fun n0 => n <= n0) (le_n n) _ (refl_equal n)).
+ 2:reflexivity.
+  generalize (refl_equal n).
+    pattern n at 2 4 6 10, q; case q; [intro | intros m l e].
+     rewrite <- eq_rect_eq_nat; trivial.
+     contradiction (le_Sn_n m); rewrite <- e; assumption.
+ replace (le_S n m p) with
+  (eq_rect _ (fun n0 => n <= n0) (le_S n m p) _ (refl_equal (S m))).
+ 2:reflexivity.
+  generalize (refl_equal (S m)).
+    pattern (S m) at 1 3 4 6, q; case q; [intro Heq | intros m0 l HeqS].
+     contradiction (le_Sn_n m); rewrite Heq; assumption.
+     injection HeqS; intro Heq; generalize l HeqS.
+      rewrite <- Heq; intros; rewrite <- eq_rect_eq_nat.
+      rewrite (IHp l0); reflexivity.
+Qed.
+\end{coq_example*}
+
+\Question{How to exploit equalities on sets}
+
+To extract information from an equality on sets, you need to
+find a predicate of sets satisfied by the elements of the sets. As an
+example, let's consider the following theorem.
+
+\begin{coq_example*}
+Theorem interval_discr :
+  forall m n:nat,
+    {x : nat | x <= m} = {x : nat | x <= n} -> m = n.
+\end{coq_example*}
+
+We have a proof requiring the axiom of proof-irrelevance. We
+conjecture that proof-irrelevance can be circumvented by introducing a
+primitive definition of discrimination of the proofs of
+\verb!{x : nat | x <= m}!.
+
+\begin{latexonly}%
+The proof can be found in file {\tt interval$\_$discr.v} in this directory.
+%Here is the proof
+%\begin{small}
+%\begin{flushleft}
+%\begin{texttt}
+%\def_{\ifmmode\sb\else\subscr\fi}
+%\include{interval_discr.v}
+%%% WARNING semantics of \_ has changed !
+%\end{texttt}
+%$a\_b\_c$
+%\end{flushleft}
+%\end{small}
+\end{latexonly}%
+\begin{htmlonly}%
+\ahref{./interval_discr.v}{Here} is the proof.
+\end{htmlonly}
+
+\Question{I have a problem of dependent elimination on
+proofs, how to solve it?}
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+
+\begin{coq_example*}
+Inductive Def1 : Set := c1 : Def1.
+Inductive DefProp : Def1 -> Prop :=
+  c2 : forall d:Def1, DefProp d.
+Inductive Comb : Set :=
+  c3 : forall d:Def1, DefProp d -> Comb.
+Lemma eq_comb :
+  forall (d1 d1':Def1) (d2:DefProp d1) (d2':DefProp d1'),
+    d1 = d1' -> c3 d1 d2 = c3 d1' d2'.
+\end{coq_example*}
+
+ You need to derive the dependent elimination
+scheme for DefProp by hand using {\coqtt Scheme}.
+
+\begin{coq_eval}
+Abort.
+\end{coq_eval}
+
+\begin{coq_example*}
+Scheme DefProp_elim := Induction for DefProp Sort Prop.
+Lemma eq_comb :
+  forall d1 d1':Def1,
+    d1 = d1' ->
+    forall (d2:DefProp d1) (d2':DefProp d1'), c3 d1 d2 = c3 d1' d2'.
+intros.
+destruct H.
+destruct d2 using DefProp_elim.
+destruct d2' using DefProp_elim.
+reflexivity.
+Qed.
+\end{coq_example*}
+
+
+\Question{And what if I want to prove the following?}
+
+\begin{coq_example*}
+Inductive natProp : nat -> Prop :=
+  | p0 : natProp 0
+  | pS : forall n:nat, natProp n -> natProp (S n).
+Inductive package : Set :=
+  pack : forall n:nat, natProp n -> package.
+Lemma eq_pack :
+ forall n n':nat,
+   n = n' ->
+   forall (np:natProp n) (np':natProp n'), pack n np = pack n' np'.
+\end{coq_example*}
+
+
+
+\begin{coq_eval}
+Abort.
+\end{coq_eval}
+\begin{coq_example*}
+Scheme natProp_elim := Induction for natProp Sort Prop.
+Definition pack_S : package -> package.
+destruct 1.
+apply (pack (S n)).
+apply pS; assumption.
+Defined.
+Lemma eq_pack :
+  forall n n':nat,
+    n = n' ->
+    forall (np:natProp n) (np':natProp n'), pack n np = pack n' np'.
+intros n n' Heq np np'.
+generalize dependent n'.
+induction np using natProp_elim.
+induction np' using natProp_elim; intros; auto.
+ discriminate Heq.
+induction np' using natProp_elim; intros; auto.
+ discriminate Heq.
+change (pack_S (pack n np) = pack_S (pack n0 np')).
+apply (f_equal (A:=package)).
+apply IHnp.
+auto.
+Qed.
+\end{coq_example*}
+
+
+
+
+
+
+
+\section{Publishing tools}
+
+\Question{How can I generate some latex from my development?}
+
+You can use {\tt coqdoc}.
+
+\Question{How can I generate some HTML from my development?}
+
+You can use {\tt coqdoc}.
+
+\Question{How can I generate some dependency graph from my development?}
+
+\Question{How can I cite some {\Coq} in my latex document?}
+
+You can use {\tt coq\_tex}.
+
+\Question{How can I cite the {\Coq} reference manual?}
+
+You can use this bibtex entry:
+\begin{verbatim}
+@Manual{Coq:manual,
+  title =        {The Coq proof assistant reference manual},
+  author =       {\mbox{The Coq development team}},
+  organization = {LogiCal Project},
+  note =         {Version 8.0},
+  year =         {2004},
+  url =          "http://coq.inria.fr"
+}
+\end{verbatim}
+
+\Question{Where can I publish my developments in {\Coq}?}
+
+You can submit your developments as a user contribution to the {\Coq}
+development team. This ensures its liveness along the evolution and
+possible changes of {\Coq}.
+
+You can also submit your developments to the HELM/MoWGLI repository at
+the University of Bologna (see
+\ahref{http://mowgli.cs.unibo.it}{\url{http://mowgli.cs.unibo.it}}). For
+developments submitted in this database, it is possible to visualize
+the developments in natural language and execute various retrieving
+requests.
+
+\Question{How can I read my proof in natural language?}
+
+You can submit your proof to the HELM/MoWGLI repository and use the
+rendering tool provided by the server (see
+\ahref{http://mowgli.cs.unibo.it}{\url{http://mowgli.cs.unibo.it}}).
+
+\section{\CoqIde}
+
+\Question{What is {\CoqIde}?}
+
+{\CoqIde} is a gtk based GUI for \Coq.
+
+\Question{How to enable Emacs keybindings?}
+ Insert \texttt{gtk-key-theme-name = "Emacs"}
+    in your \texttt{.coqide-gtk2rc} file. It may be in the current dir
+    or in \verb#$HOME# dir. This is done by default.
+
+%$ juste pour que la coloration emacs marche
+
+\Question{How to enable antialiased fonts?}
+
+ Set the \verb#GDK_USE_XFT# variable to \verb#1#. This is by default with \verb#Gtk >= 2.2#.
+    If some of your fonts are not available, set \verb#GDK_USE_XFT# to \verb#0#.
+
+\Question{How to use those Forall and Exists pretty symbols?}\label{forallcoqide}
+ Thanks to the notation features in \Coq, you just need to insert these
+lines in your {\Coq} buffer:\\
+\begin{texttt}
+Notation "$\forall$ x : t, P" := (forall x:t, P) (at level 200, x ident).
+\end{texttt}\\
+\begin{texttt}
+Notation "$\exists$ x : t, P" := (exists x:t, P) (at level 200, x ident).
+\end{texttt}
+
+Copy/Paste of these lines from this file will not work outside of \CoqIde.
+You need to load a file containing these lines or to enter the $\forall$
+using an input method (see \ref{inputmeth}). To try it just use \verb#Require Import utf8# from inside
+\CoqIde. 
+To enable these notations automatically start coqide with
+\begin{verbatim}
+	coqide -l utf8
+\end{verbatim}
+In the ide subdir of {\Coq} library, you will find a sample utf8.v with some 
+pretty simple notations.
+
+\Question{How to define an input method for non ASCII symbols?}\label{inputmeth}
+
+\begin{itemize}
+\item First solution: type \verb#<CONTROL><SHIFT>2200# to enter a forall in the script widow. 
+	2200 is the hexadecimal code for forall in unicode charts and is encoded as 	
+	in UTF-8.
+	2203 is for exists. See \ahref{http://www.unicode.org}{\url{http://www.unicode.org}} for more codes.
+\item Second solution: rebind \verb#<AltGr>a# to forall and \verb#<AltGr>e# to exists. 
+	Under X11, you need to use something like
+\begin{verbatim}
+		xmodmap -e "keycode  24 = a A F13 F13" 
+		xmodmap -e "keycode  26 = e E F14 F14"
+\end{verbatim}
+	and then to add   
+\begin{verbatim}
+		bind "F13" {"insert-at-cursor" ("")}
+		bind "F14" {"insert-at-cursor" ("")}
+\end{verbatim}
+	to your "binding "text"" section in \verb#.coqiderc-gtk2rc.#
+	The strange ("") argument is the UTF-8 encoding for
+	0x2200. 
+	You can compute these encodings using the lablgtk2 toplevel with 
+\begin{verbatim}		
+Glib.Utf8.from_unichar 0x2200;;
+\end{verbatim}
+	Further symbols can be bound on higher Fxx keys or on even on other keys you
+	do not need .
+\end{itemize}
+
+\Question{How to build a custom {\CoqIde} with user ml code?}
+ Use 
+	coqmktop -ide -byte m1.cmo...mi.cmo
+    or 
+	coqmktop -ide -opt m1.cmx...mi.cmx
+
+\Question{How to customize the shortcuts for menus?}
+ Two solutions are offered:
+\begin{itemize}
+\item Edit \$HOME/.coqide.keys by hand or
+\item Add "gtk-can-change-accels = 1" in your .coqide-gtk2rc file. Then
+    from \CoqIde, you may select a menu entry and press the desired 
+    shortcut. 
+\end{itemize}
+
+\Question{What encoding should I use? What is this $\backslash$x\{iiii\} in my file?}
+ The encoding option is related to the way files are saved. 
+ Keep it as UTF-8 until it becomes important for you to exchange files 
+ with non UTF-8 aware applications.
+ If you choose something else than UTF-8, then missing characters will 
+ be encoded by $\backslash$x\{....\} or $\backslash$x\{........\}
+ where each dot is an hex. digit. 
+ The number between braces is the hexadecimal UNICODE index for the
+  missing character.
+    
+
+
+
+\section{Extraction}
+
+\Question{What is program extraction?}
+
+Program extraction consist in generating a program from a constructive proof.
+
+\Question{Which language can I extract to?}
+
+You can extract your programs to Objective Caml and Haskell.
+
+\Question{How can I extract an incomplete proof?}
+
+You can provide programs for your axioms.
+
+
+
+%%%%%%%
+\section{Glossary}
+
+\Question{Can you explain me what an evaluable constant is?}
+
+An evaluable constant is a constant which is unfoldable.
+
+\Question{What is a goal?}
+
+The goal is the statement to be proved.
+
+\Question{What is a meta variable?}
+
+A meta variable in {\Coq} represents a ``hole'', i.e. a part of a proof
+that is still unknown. 
+
+\Question{What is Gallina?}  
+
+Gallina is the specification language of \Coq. Complete documentation
+of this language can be found in the Reference Manual.
+
+\Question{What is The Vernacular?}  
+
+It is the language of commands of Gallina i.e. definitions, lemmas, {\ldots}  
+
+
+\Question{What is a dependent type?}
+
+A dependant type is a type which depends on some term. For instance
+``vector of size n'' is a dependant type representing all the vectors
+of size $n$. Its type depends on $n$
+
+\Question{What is a proof by reflection?}
+
+This is a proof generated by some computation which is done using the
+internal reduction of {\Coq} (not using the tactic language of {\Coq}
+(\Ltac) nor the implementation language for \Coq).  An example of
+tactic using the reflection mechanism is the {\ring} tactic. The
+reflection method consist in reflecting a subset of {\Coq} language (for
+example the arithmetical expressions) into an object of the \Coq
+language itself (in this case an inductive type denoting arithmetical
+expressions).  For more information see~\cite{howe,harrison,boutin}
+and the last chapter of the Coq'Art.
+
+\Question{What is intuitionistic logic?}
+
+This is any logic which does not assume that ``A or not A''.
+
+
+\Question{What is proof-irrelevance?}
+
+See question \ref{proof-irrelevance}
+
+
+\Question{What is the difference between opaque and transparent?}{\label{opaque}}	
+
+Opaque definitions can not be unfolded but transparent ones can.
+
+
+\section{Troubleshooting}
+
+\Question{What can I do when {\tt Qed.} is slow?}
+
+Sometime you can use the {\abstracttac} tactic, which makes as if you had
+stated some local lemma, this speeds up the typing process.
+
+\Question{Why \texttt{Reset Initial.} does not work when using \texttt{coqc}?}
+
+The initial state corresponds to the state of coqtop when the interactive
+session began. It does not make sense in files to compile.
+
+
+\Question{What can I do if I get ``No more subgoals but non-instantiated existential variables''?}
+
+This means that {\eauto} or {\eapply} didn't instantiate an
+existential variable which eventually got erased by some computation.
+You have to backtrack to the faulty occurrence of {\eauto} or
+{\eapply} and give the missing argument an explicit value.
+
+\Question{What can I do if I get ``Cannot solve a second-order unification problem''?}
+
+You can help {\Coq} using the {\pattern} tactic.
+
+\Question{Why does {\Coq} tell me that \texttt{\{x:A|(P x)\}} is not convertible with \texttt{(sig A P)}?}
+
+ This is because \texttt{\{x:A|P x\}} is a notation for
+\texttt{sig (fun x:A => P x)}. Since {\Coq} does not reason up to
+$\eta$-conversion, this is different from \texttt{sig P}.
+
+
+\Question{I copy-paste a term and {\Coq} says it is not convertible
+  to the original term. Sometimes it even says the copied term is not
+well-typed.}
+
+ This is probably due to invisible implicit information (implicit
+arguments, coercions and Cases annotations) in the printed term, which
+is not re-synthesised from the copied-pasted term in the same way as
+it is in the original term.
+
+  Consider for instance {\tt (@eq Type True True)}. This term is
+printed as {\tt True=True} and re-parsed as {\tt (@eq Prop True
+True)}. The two terms are not convertible (hence they fool tactics
+like {\tt pattern}).
+
+  There is currently no satisfactory answer to the problem. However,
+the command {\tt Set Printing All} is useful for diagnosing the
+problem.
+ 
+  Due to coercions, one may even face type-checking errors. In some
+rare cases, the criterion to hide coercions is a bit too loose, which
+may result in a typing error message if the parser is not able to find
+again the missing coercion.
+
+
+
+\section{Conclusion and Farewell.}
+\label{ccl}
+
+\Question{What if my question isn't answered here?} 
+\label{lastquestion}
+
+Don't panic \verb+:-)+. You can try the {\Coq} manual~\cite{Coq:manual} for a technical
+description of the prover. The Coq'Art~\cite{Coq:coqart} is the first
+book written on {\Coq} and provides a comprehensive review of the
+theorem prover as well as a number of example and exercises. Finally,
+the tutorial~\cite{Coq:Tutorial} provides a smooth introduction to
+theorem proving in \Coq.
+
+
+%%%%%%%
+\newpage
+\nocite{LaTeX:intro}
+\nocite{LaTeX:symb}
+\bibliography{fk}
+
+%%%%%%%
+\typeout{*********************************************}
+\typeout{********* That makes \thequestion{\space} questions **********}
+\typeout{*********************************************}
+
+\end{document}
diff --git a/doc/faq/axioms.eps b/doc/faq/axioms.eps
new file mode 100644
index 000000000..3f3c01c43
--- /dev/null
+++ b/doc/faq/axioms.eps
@@ -0,0 +1,378 @@
+%!PS-Adobe-2.0 EPSF-2.0
+%%Title: axioms.fig
+%%Creator: fig2dev Version 3.2 Patchlevel 4
+%%CreationDate: Wed May  5 18:30:03 2004
+%%For: herbelin@limoux.polytechnique.fr (Hugo Herbelin)
+%%BoundingBox: 0 0 437 372
+%%Magnification: 1.0000
+%%EndComments
+/$F2psDict 200 dict def
+$F2psDict begin
+$F2psDict /mtrx matrix put
+/col-1 {0 setgray} bind def
+/col0 {0.000 0.000 0.000 srgb} bind def
+/col1 {0.000 0.000 1.000 srgb} bind def
+/col2 {0.000 1.000 0.000 srgb} bind def
+/col3 {0.000 1.000 1.000 srgb} bind def
+/col4 {1.000 0.000 0.000 srgb} bind def
+/col5 {1.000 0.000 1.000 srgb} bind def
+/col6 {1.000 1.000 0.000 srgb} bind def
+/col7 {1.000 1.000 1.000 srgb} bind def
+/col8 {0.000 0.000 0.560 srgb} bind def
+/col9 {0.000 0.000 0.690 srgb} bind def
+/col10 {0.000 0.000 0.820 srgb} bind def
+/col11 {0.530 0.810 1.000 srgb} bind def
+/col12 {0.000 0.560 0.000 srgb} bind def
+/col13 {0.000 0.690 0.000 srgb} bind def
+/col14 {0.000 0.820 0.000 srgb} bind def
+/col15 {0.000 0.560 0.560 srgb} bind def
+/col16 {0.000 0.690 0.690 srgb} bind def
+/col17 {0.000 0.820 0.820 srgb} bind def
+/col18 {0.560 0.000 0.000 srgb} bind def
+/col19 {0.690 0.000 0.000 srgb} bind def
+/col20 {0.820 0.000 0.000 srgb} bind def
+/col21 {0.560 0.000 0.560 srgb} bind def
+/col22 {0.690 0.000 0.690 srgb} bind def
+/col23 {0.820 0.000 0.820 srgb} bind def
+/col24 {0.500 0.190 0.000 srgb} bind def
+/col25 {0.630 0.250 0.000 srgb} bind def
+/col26 {0.750 0.380 0.000 srgb} bind def
+/col27 {1.000 0.500 0.500 srgb} bind def
+/col28 {1.000 0.630 0.630 srgb} bind def
+/col29 {1.000 0.750 0.750 srgb} bind def
+/col30 {1.000 0.880 0.880 srgb} bind def
+/col31 {1.000 0.840 0.000 srgb} bind def
+
+end
+save
+newpath 0 372 moveto 0 0 lineto 437 0 lineto 437 372 lineto closepath clip newpath
+-90.0 435.2 translate
+1 -1 scale
+
+/cp {closepath} bind def
+/ef {eofill} bind def
+/gr {grestore} bind def
+/gs {gsave} bind def
+/sa {save} bind def
+/rs {restore} bind def
+/l {lineto} bind def
+/m {moveto} bind def
+/rm {rmoveto} bind def
+/n {newpath} bind def
+/s {stroke} bind def
+/sh {show} bind def
+/slc {setlinecap} bind def
+/slj {setlinejoin} bind def
+/slw {setlinewidth} bind def
+/srgb {setrgbcolor} bind def
+/rot {rotate} bind def
+/sc {scale} bind def
+/sd {setdash} bind def
+/ff {findfont} bind def
+/sf {setfont} bind def
+/scf {scalefont} bind def
+/sw {stringwidth} bind def
+/tr {translate} bind def
+/tnt {dup dup currentrgbcolor
+  4 -2 roll dup 1 exch sub 3 -1 roll mul add
+  4 -2 roll dup 1 exch sub 3 -1 roll mul add
+  4 -2 roll dup 1 exch sub 3 -1 roll mul add srgb}
+  bind def
+/shd {dup dup currentrgbcolor 4 -2 roll mul 4 -2 roll mul
+  4 -2 roll mul srgb} bind def
+/reencdict 12 dict def /ReEncode { reencdict begin
+/newcodesandnames exch def /newfontname exch def /basefontname exch def
+/basefontdict basefontname findfont def /newfont basefontdict maxlength dict def
+basefontdict { exch dup /FID ne { dup /Encoding eq
+{ exch dup length array copy newfont 3 1 roll put }
+{ exch newfont 3 1 roll put } ifelse } { pop pop } ifelse } forall
+newfont /FontName newfontname put newcodesandnames aload pop
+128 1 255 { newfont /Encoding get exch /.notdef put } for
+newcodesandnames length 2 idiv { newfont /Encoding get 3 1 roll put } repeat
+newfontname newfont definefont pop end } def
+/isovec [
+8#055 /minus 8#200 /grave 8#201 /acute 8#202 /circumflex 8#203 /tilde
+8#204 /macron 8#205 /breve 8#206 /dotaccent 8#207 /dieresis
+8#210 /ring 8#211 /cedilla 8#212 /hungarumlaut 8#213 /ogonek 8#214 /caron
+8#220 /dotlessi 8#230 /oe 8#231 /OE
+8#240 /space 8#241 /exclamdown 8#242 /cent 8#243 /sterling
+8#244 /currency 8#245 /yen 8#246 /brokenbar 8#247 /section 8#250 /dieresis
+8#251 /copyright 8#252 /ordfeminine 8#253 /guillemotleft 8#254 /logicalnot
+8#255 /hyphen 8#256 /registered 8#257 /macron 8#260 /degree 8#261 /plusminus
+8#262 /twosuperior 8#263 /threesuperior 8#264 /acute 8#265 /mu 8#266 /paragraph
+8#267 /periodcentered 8#270 /cedilla 8#271 /onesuperior 8#272 /ordmasculine
+8#273 /guillemotright 8#274 /onequarter 8#275 /onehalf
+8#276 /threequarters 8#277 /questiondown 8#300 /Agrave 8#301 /Aacute
+8#302 /Acircumflex 8#303 /Atilde 8#304 /Adieresis 8#305 /Aring
+8#306 /AE 8#307 /Ccedilla 8#310 /Egrave 8#311 /Eacute
+8#312 /Ecircumflex 8#313 /Edieresis 8#314 /Igrave 8#315 /Iacute
+8#316 /Icircumflex 8#317 /Idieresis 8#320 /Eth 8#321 /Ntilde 8#322 /Ograve
+8#323 /Oacute 8#324 /Ocircumflex 8#325 /Otilde 8#326 /Odieresis 8#327 /multiply
+8#330 /Oslash 8#331 /Ugrave 8#332 /Uacute 8#333 /Ucircumflex
+8#334 /Udieresis 8#335 /Yacute 8#336 /Thorn 8#337 /germandbls 8#340 /agrave
+8#341 /aacute 8#342 /acircumflex 8#343 /atilde 8#344 /adieresis 8#345 /aring
+8#346 /ae 8#347 /ccedilla 8#350 /egrave 8#351 /eacute
+8#352 /ecircumflex 8#353 /edieresis 8#354 /igrave 8#355 /iacute
+8#356 /icircumflex 8#357 /idieresis 8#360 /eth 8#361 /ntilde 8#362 /ograve
+8#363 /oacute 8#364 /ocircumflex 8#365 /otilde 8#366 /odieresis 8#367 /divide
+8#370 /oslash 8#371 /ugrave 8#372 /uacute 8#373 /ucircumflex
+8#374 /udieresis 8#375 /yacute 8#376 /thorn 8#377 /ydieresis] def
+/Times-Roman /Times-Roman-iso isovec ReEncode
+/$F2psBegin {$F2psDict begin /$F2psEnteredState save def} def
+/$F2psEnd {$F2psEnteredState restore end} def
+
+$F2psBegin
+10 setmiterlimit
+0 slj 0 slc
+ 0.06000 0.06000 sc
+%
+% Fig objects follow
+%
+% 
+% here starts figure with depth 50
+% Arc
+7.500 slw
+gs  clippath
+3599 6933 m 3626 6879 l 3492 6812 l 3586 6893 l 3465 6865 l cp
+eoclip
+n 3600.0 6750.0 150.0 90.0 -90.0 arc
+gs col0 s gr
+ gr
+
+% arrowhead
+n 3465 6865 m 3586 6893 l 3492 6812 l 3465 6865 l  cp gs 0.00 setgray ef gr  col0 s
+% Arc
+gs  clippath
+3599 6633 m 3626 6579 l 3492 6512 l 3586 6593 l 3465 6565 l cp
+eoclip
+n 3600.0 6450.0 150.0 90.0 -90.0 arc
+gs col0 s gr
+ gr
+
+% arrowhead
+n 3465 6565 m 3586 6593 l 3492 6512 l 3465 6565 l  cp gs 0.00 setgray ef gr  col0 s
+% Arc
+gs  clippath
+3626 6020 m 3599 5966 l 3465 6034 l 3586 6007 l 3492 6087 l cp
+3599 6333 m 3626 6279 l 3492 6212 l 3586 6293 l 3465 6265 l cp
+eoclip
+n 3600.0 6150.0 150.0 90.0 -90.0 arc
+gs col0 s gr
+ gr
+
+% arrowhead
+n 3492 6087 m 3586 6007 l 3465 6034 l 3492 6087 l  cp gs 0.00 setgray ef gr  col0 s
+% arrowhead
+n 3465 6265 m 3586 6293 l 3492 6212 l 3465 6265 l  cp gs 0.00 setgray ef gr  col0 s
+% Arc
+gs  clippath
+3626 6320 m 3599 6266 l 3465 6334 l 3586 6307 l 3492 6387 l cp
+3599 6633 m 3626 6579 l 3492 6512 l 3586 6593 l 3465 6565 l cp
+eoclip
+n 3600.0 6450.0 150.0 90.0 -90.0 arc
+gs col0 s gr
+ gr
+
+% arrowhead
+n 3492 6387 m 3586 6307 l 3465 6334 l 3492 6387 l  cp gs 0.00 setgray ef gr  col0 s
+% arrowhead
+n 3465 6565 m 3586 6593 l 3492 6512 l 3465 6565 l  cp gs 0.00 setgray ef gr  col0 s
+% Arc
+gs  clippath
+3626 6620 m 3599 6566 l 3465 6634 l 3586 6607 l 3492 6687 l cp
+3599 6933 m 3626 6879 l 3492 6812 l 3586 6893 l 3465 6865 l cp
+eoclip
+n 3600.0 6750.0 150.0 90.0 -90.0 arc
+gs col0 s gr
+ gr
+
+% arrowhead
+n 3492 6687 m 3586 6607 l 3465 6634 l 3492 6687 l  cp gs 0.00 setgray ef gr  col0 s
+% arrowhead
+n 3465 6865 m 3586 6893 l 3492 6812 l 3465 6865 l  cp gs 0.00 setgray ef gr  col0 s
+% Arc
+gs  clippath
+3626 6920 m 3599 6866 l 3465 6934 l 3586 6907 l 3492 6987 l cp
+3599 7233 m 3626 7179 l 3492 7112 l 3586 7193 l 3465 7165 l cp
+eoclip
+n 3600.0 7050.0 150.0 90.0 -90.0 arc
+gs col0 s gr
+ gr
+
+% arrowhead
+n 3492 6987 m 3586 6907 l 3465 6934 l 3492 6987 l  cp gs 0.00 setgray ef gr  col0 s
+% arrowhead
+n 3465 7165 m 3586 7193 l 3492 7112 l 3465 7165 l  cp gs 0.00 setgray ef gr  col0 s
+% Arc
+gs  clippath
+4168 4060 m 4227 4068 l 4247 3919 l 4202 4034 l 4188 3911 l cp
+eoclip
+n 14032.5 5272.5 9908.2 -159.9 -172.9 arcn
+gs col0 s gr
+ gr
+
+% arrowhead
+n 4188 3911 m 4202 4034 l 4247 3919 l 4188 3911 l  cp gs 0.00 setgray ef gr  col0 s
+% Polyline
+gs  clippath
+4170 5790 m 4230 5790 l 4230 5639 l 4200 5759 l 4170 5639 l cp
+eoclip
+n 4200 5175 m
+ 4200 5775 l gs col0 s gr gr
+
+% arrowhead
+n 4170 5639 m 4200 5759 l 4230 5639 l 4170 5639 l  cp gs 0.00 setgray ef gr  col0 s
+% Polyline
+gs  clippath
+4553 5749 m 4567 5807 l 4714 5771 l 4591 5771 l 4700 5713 l cp
+eoclip
+n 7050 5175 m
+ 4575 5775 l gs col0 s gr gr
+
+% arrowhead
+n 4700 5713 m 4591 5771 l 4714 5771 l 4700 5713 l  cp gs 0.00 setgray ef gr  col0 s
+% Polyline
+gs  clippath
+4170 4890 m 4230 4890 l 4230 4739 l 4200 4859 l 4170 4739 l cp
+eoclip
+n 4200 4275 m
+ 4200 4875 l gs col0 s gr gr
+
+% arrowhead
+n 4170 4739 m 4200 4859 l 4230 4739 l 4170 4739 l  cp gs 0.00 setgray ef gr  col0 s
+% Polyline
+gs  clippath
+7131 4907 m 7147 4850 l 7001 4810 l 7109 4871 l 6985 4868 l cp
+eoclip
+n 4950 4275 m
+ 7125 4875 l gs col0 s gr gr
+
+% arrowhead
+n 6985 4868 m 7109 4871 l 7001 4810 l 6985 4868 l  cp gs 0.00 setgray ef gr  col0 s
+% Polyline
+gs  clippath
+7167 4057 m 7225 4071 l 7262 3924 l 7204 4034 l 7204 3910 l cp
+eoclip
+n 7725 1950 m
+ 7200 4050 l gs col0 s gr gr
+
+% arrowhead
+n 7204 3910 m 7204 4034 l 7262 3924 l 7204 3910 l  cp gs 0.00 setgray ef gr  col0 s
+% Polyline
+n 4350 3075 m
+ 7350 1950 l gs col0 s gr 
+% Polyline
+gs  clippath
+7170 4890 m 7230 4890 l 7230 4739 l 7200 4859 l 7170 4739 l cp
+eoclip
+n 7200 4275 m
+ 7200 4875 l gs col0 s gr gr
+
+% arrowhead
+n 7170 4739 m 7200 4859 l 7230 4739 l 7170 4739 l  cp gs 0.00 setgray ef gr  col0 s
+% Polyline
+n 3075 1875 m
+ 3975 1875 l gs col0 s gr 
+% Polyline
+gs  clippath
+5520 4065 m 5580 4065 l 5580 3914 l 5550 4034 l 5520 3914 l cp
+5580 3660 m 5520 3660 l 5520 3811 l 5550 3691 l 5580 3811 l cp
+eoclip
+n 5550 3675 m
+ 5550 4050 l gs col0 s gr gr
+
+% arrowhead
+n 5580 3811 m 5550 3691 l 5520 3811 l 5580 3811 l  cp gs 0.00 setgray ef gr  col0 s
+% arrowhead
+n 5520 3914 m 5550 4034 l 5580 3914 l 5520 3914 l  cp gs 0.00 setgray ef gr  col0 s
+% Polyline
+n 4575 4050 m
+ 6450 4050 l gs col0 s gr 
+% Polyline
+gs  clippath
+3495 2265 m 3555 2265 l 3555 2114 l 3525 2234 l 3495 2114 l cp
+3555 1860 m 3495 1860 l 3495 2011 l 3525 1891 l 3555 2011 l cp
+eoclip
+n 3525 1875 m
+ 3525 2250 l gs col0 s gr gr
+
+% arrowhead
+n 3555 2011 m 3525 1891 l 3495 2011 l 3555 2011 l  cp gs 0.00 setgray ef gr  col0 s
+% arrowhead
+n 3495 2114 m 3525 2234 l 3555 2114 l 3495 2114 l  cp gs 0.00 setgray ef gr  col0 s
+% Polyline
+gs  clippath
+2219 3988 m 2279 3991 l 2285 3840 l 2251 3959 l 2225 3838 l cp
+eoclip
+n 2325 1875 m
+ 2250 3975 l gs col0 s gr gr
+
+% arrowhead
+n 2225 3838 m 2251 3959 l 2285 3840 l 2225 3838 l  cp gs 0.00 setgray ef gr  col0 s
+% Polyline
+n 7800 1275 m
+ 2100 1275 l gs col0 s gr 
+/Times-Roman-iso ff 180.00 scf sf
+6600 5100 m
+gs 1 -1 sc (Proof-irrelevance) col0 sh gr
+/Times-Roman-iso ff 180.00 scf sf
+3675 4200 m
+gs 1 -1 sc (Excluded-middle) col0 sh gr
+/Times-Roman-iso ff 180.00 scf sf
+6900 1800 m
+gs 1 -1 sc (Predicate extensionality) col0 sh gr
+/Times-Roman-iso ff 180.00 scf sf
+3375 3525 m
+gs 1 -1 sc (\(Diaconescu\)) col0 sh gr
+/Times-Roman-iso ff 180.00 scf sf
+4650 3600 m
+gs 1 -1 sc (Propositional degeneracy) col0 sh gr
+/Times-Roman-iso ff 180.00 scf sf
+3825 1800 m
+gs 1 -1 sc (Relational choice axiom) col0 sh gr
+/Times-Roman-iso ff 180.00 scf sf
+1725 1800 m
+gs 1 -1 sc (Description principle) col0 sh gr
+/Times-Roman-iso ff 180.00 scf sf
+2550 2400 m
+gs 1 -1 sc (Functional choice axiom) col0 sh gr
+/Times-Roman-iso ff 180.00 scf sf
+3600 5100 m
+gs 1 -1 sc (Decidability of equality on $A$) col0 sh gr
+/Times-Roman-iso ff 180.00 scf sf
+4425 4575 m
+gs 1 -1 sc (\(needs Prop-impredicativity\)) col0 sh gr
+/Times-Roman-iso ff 180.00 scf sf
+5025 4725 m
+gs 1 -1 sc (\(Berardi\)) col0 sh gr
+/Times-Roman-iso ff 180.00 scf sf
+1500 3075 m
+gs 1 -1 sc (\(if Set impredicative\)) col0 sh gr
+/Times-Roman-iso ff 180.00 scf sf
+1500 4200 m
+gs 1 -1 sc (Not excluded-middle) col0 sh gr
+/Times-Roman-iso ff 180.00 scf sf
+3600 6000 m
+gs 1 -1 sc (Axiom K on A) col0 sh gr
+/Times-Roman-iso ff 180.00 scf sf
+3600 7200 m
+gs 1 -1 sc (Invariance by substitution of reflexivity proofs for equality on A) col0 sh gr
+/Times-Roman-iso ff 180.00 scf sf
+6150 4200 m
+gs 1 -1 sc (Propositional extensionality) col0 sh gr
+/Times-Roman-iso ff 180.00 scf sf
+2100 1200 m
+gs 1 -1 sc (The dependency graph of axioms in the Calculus of Inductive Constructions) col0 sh gr
+/Times-Roman-iso ff 180.00 scf sf
+3600 6900 m
+gs 1 -1 sc (Injectivity of equality on sigma-types on A) col0 sh gr
+/Times-Roman-iso ff 180.00 scf sf
+3600 6300 m
+gs 1 -1 sc (Uniqueness of reflexivity proofs for equality on A) col0 sh gr
+/Times-Roman-iso ff 180.00 scf sf
+3600 6600 m
+gs 1 -1 sc (Uniqueness of equality proofs on A) col0 sh gr
+% here ends figure;
+$F2psEnd
+rs
+showpage
diff --git a/doc/faq/axioms.fig b/doc/faq/axioms.fig
new file mode 100644
index 000000000..f07759302
--- /dev/null
+++ b/doc/faq/axioms.fig
@@ -0,0 +1,84 @@
+#FIG 3.2
+Landscape
+Center
+Inches
+Letter  
+100.00
+Single
+-2
+1200 2
+5 1 0 1 0 7 50 -1 -1 0.000 0 0 0 1 3600.000 6750.000 3600 6900 3450 6750 3600 6600
+	1 1 1.00 60.00 120.00
+5 1 0 1 0 7 50 -1 -1 0.000 0 0 0 1 3600.000 6450.000 3600 6600 3450 6450 3600 6300
+	1 1 1.00 60.00 120.00
+5 1 0 1 0 7 50 -1 -1 0.000 0 0 1 1 3600.000 6150.000 3600 6300 3450 6150 3600 6000
+	1 1 1.00 60.00 120.00
+	1 1 1.00 60.00 120.00
+5 1 0 1 0 7 50 -1 -1 0.000 0 0 1 1 3600.000 6450.000 3600 6600 3450 6450 3600 6300
+	1 1 1.00 60.00 120.00
+	1 1 1.00 60.00 120.00
+5 1 0 1 0 7 50 -1 -1 0.000 0 0 1 1 3600.000 6750.000 3600 6900 3450 6750 3600 6600
+	1 1 1.00 60.00 120.00
+	1 1 1.00 60.00 120.00
+5 1 0 1 0 7 50 -1 -1 0.000 0 0 1 1 3600.000 7050.000 3600 7200 3450 7050 3600 6900
+	1 1 1.00 60.00 120.00
+	1 1 1.00 60.00 120.00
+5 1 0 1 0 7 50 -1 -1 0.000 0 1 1 0 14032.500 5272.500 4725 1875 4425 2850 4200 4050
+	1 1 1.00 60.00 120.00
+2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
+	1 1 1.00 60.00 120.00
+	 4200 5175 4200 5775
+2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
+	1 1 1.00 60.00 120.00
+	 7050 5175 4575 5775
+2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
+	1 1 1.00 60.00 120.00
+	 4200 4275 4200 4875
+2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
+	1 1 1.00 60.00 120.00
+	 4950 4275 7125 4875
+2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
+	1 1 1.00 60.00 120.00
+	 7725 1950 7200 4050
+2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2
+	 4350 3075 7350 1950
+2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
+	1 1 1.00 60.00 120.00
+	 7200 4275 7200 4875
+2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2
+	 3075 1875 3975 1875
+2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 1 2
+	1 1 1.00 60.00 120.00
+	1 1 1.00 60.00 120.00
+	 5550 3675 5550 4050
+2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2
+	 4575 4050 6450 4050
+2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 1 2
+	1 1 1.00 60.00 120.00
+	1 1 1.00 60.00 120.00
+	 3525 1875 3525 2250
+2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
+	1 1 1.00 60.00 120.00
+	 2325 1875 2250 3975
+2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2
+	 7800 1275 2100 1275
+4 0 0 50 -1 0 12 0.0000 4 135 1305 6600 5100 Proof-irrelevance\001
+4 0 0 50 -1 0 12 0.0000 4 135 1260 3675 4200 Excluded-middle\001
+4 0 0 50 -1 0 12 0.0000 4 180 1830 6900 1800 Predicate extensionality\001
+4 0 0 50 -1 0 12 0.0000 4 180 1050 3375 3525 (Diaconescu)\001
+4 0 0 50 -1 0 12 0.0000 4 180 1905 4650 3600 Propositional degeneracy\001
+4 0 0 50 -1 0 12 0.0000 4 135 1800 3825 1800 Relational choice axiom\001
+4 0 0 50 -1 0 12 0.0000 4 180 1575 1725 1800 Description principle\001
+4 0 0 50 -1 0 12 0.0000 4 135 1830 2550 2400 Functional choice axiom\001
+4 0 0 50 -1 0 12 0.0000 4 195 2340 3600 5100 Decidability of equality on $A$\001
+4 0 0 50 -1 0 12 0.0000 4 180 2175 4425 4575 (needs Prop-impredicativity)\001
+4 0 0 50 -1 0 12 0.0000 4 180 705 5025 4725 (Berardi)\001
+4 0 0 50 -1 0 12 0.0000 4 180 1620 1500 3075 (if Set impredicative)\001
+4 0 0 50 -1 0 12 0.0000 4 135 1560 1500 4200 Not excluded-middle\001
+4 0 0 50 -1 0 12 0.0000 4 135 1080 3600 6000 Axiom K on A\001
+4 0 0 50 -1 0 12 0.0000 4 180 4800 3600 7200 Invariance by substitution of reflexivity proofs for equality on A\001
+4 0 0 50 -1 0 12 0.0000 4 180 2100 6150 4200 Propositional extensionality\001
+4 0 0 50 -1 0 12 0.0000 4 180 5700 2100 1200 The dependency graph of axioms in the Calculus of Inductive Constructions\001
+4 0 0 50 -1 0 12 0.0000 4 180 3210 3600 6900 Injectivity of equality on sigma-types on A\001
+4 0 0 50 -1 0 12 0.0000 4 180 3735 3600 6300 Uniqueness of reflexivity proofs for equality on A\001
+4 0 0 50 -1 0 12 0.0000 4 180 2670 3600 6600 Uniqueness of equality proofs on A\001
diff --git a/doc/faq/axioms.png b/doc/faq/axioms.png
new file mode 100644
index 000000000..2aee09166
--- /dev/null
+++ b/doc/faq/axioms.png
diff --git a/doc/faq/fk.bib b/doc/faq/fk.bib
new file mode 100644
index 000000000..392e401fc
--- /dev/null
+++ b/doc/faq/fk.bib
@@ -0,0 +1,2215 @@
+%%%%%%% FAQ %%%%%%%
+
+@book{ProofsTypes,
+  Author="Girard, Jean-Yves and Yves Lafont and Paul Taylor",
+  Title="Proofs and Types",
+  Publisher="Cambrige Tracts in Theoretical Computer Science, Cambridge University Press",
+  Year="1989"
+}
+
+@misc{Types:Dowek,
+  author = "Gilles Dowek",
+  title = "Th{\'e}orie des types",
+  year = 2002,
+  howpublished = "Lecture notes",
+  url= "http://www.lix.polytechnique.fr/~dowek/Cours/theories_des_types.ps.gz"
+}
+
+@PHDTHESIS{EGThese,
+  author = {Eduardo Giménez},
+  title = {Un Calcul de Constructions Infinies et son application
+a la vérification de systèmes communicants},
+  type = {thèse d'Université},
+  school = {Ecole Normale Supérieure de Lyon},
+  month = {December},
+  year = {1996},
+}
+
+
+%%%%%%% Semantique %%%%%%%
+
+@misc{Sem:cours,
+  author = "François Pottier",
+  title =  "{Typage et Programmation}",
+  year = "2002",
+  howpublished = "Lecture notes",
+  note = "DEA PSPL"
+}
+
+@inproceedings{Sem:Dubois,
+  author    = {Catherine Dubois},
+  editor    = {Mark Aagaard and
+               John Harrison},
+  title     = "{Proving ML Type Soundness Within Coq}",
+  pages     = {126-144},
+  booktitle = {TPHOLs},
+  publisher = {Springer},
+  series    = {Lecture Notes in Computer Science},
+  volume    = {1869},
+  year      = {2000},
+  isbn      = {3-540-67863-8},
+  bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@techreport{Sem:Plotkin, 
+author = {Gordon D. Plotkin}, 
+institution = {Aarhus University}, 
+number = {{DAIMI FN-19}}, 
+title = {{A structural approach to operational semantics}}, 
+year = {1981} 
+} 
+
+@article{Sem:RemyV98,
+  author     = "Didier R{\'e}my and J{\'e}r{\^o}me Vouillon",
+  title =        "Objective {ML}: 
+                  An effective object-oriented extension to {ML}",
+  journal =      "Theory And Practice of Object Systems",
+  year =         1998,
+  volume =    "4",
+  number =    "1",
+  pages =     "27--50",
+  note =      {A preliminary version appeared in the proceedings
+                  of the 24th ACM Conference on Principles
+                  of Programming Languages, 1997}
+}
+
+@book{Sem:Winskel,
+  AUTHOR      = {Winskel, Glynn},
+  TITLE       = {The Formal Semantics of Programming Languages},
+  NOTE        = {WIN g2 93:1 P-Ex},
+  YEAR        = {1993},
+  PUBLISHER   = {The MIT Press},
+  SERIES      = {Foundations of Computing},
+ }
+
+@Article{Sem:WrightFelleisen,
+  refkey =       "C1210",
+  title =        "A Syntactic Approach to Type Soundness",
+  author =       "Andrew K. Wright and Matthias Felleisen",
+  pages =        "38--94",
+  journal =      "Information and Computation",
+  month =        "15~" # nov,
+  year =         "1994",
+  volume =       "115",
+  number =       "1"
+}
+
+@inproceedings{Sem:Nipkow-MOD,
+  author={Tobias Nipkow},
+  title={Jinja: Towards a Comprehensive Formal Semantics for a
+       {J}ava-like Language},
+  booktitle={Proc.\ Marktobderdorf Summer School 2003},
+  publisher={IOS Press},editor={H. Schwichtenberg and K. Spies},
+  year=2003,
+  note={To appear}
+}
+
+%%%%%%% Coq %%%%%%%
+
+@book{Coq:coqart,
+  title = "Interactive Theorem Proving and Program Development,
+	  Coq'Art: The Calculus of Inductive Constructions",
+  author = "Yves Bertot and Pierre Castéran",
+  publisher = "Springer Verlag",
+  series = "Texts in Theoretical Computer Science. An
+	  EATCS series",
+  year = 2004
+}
+			 
+@phdthesis{Coq:Del01,
+	AUTHOR = "David Delahaye",
+	TITLE = "Conception de langages pour décrire les preuves et les 
+                  automatisations dans les outils d'aide à la preuve",
+	SCHOOL = {Universit\'e Paris~6},
+	YEAR = "2001",
+        Type = {Th\`ese de Doctorat}
+}
+
+@techreport{Coq:gimenez-tut,
+    author = "Eduardo Gim\'enez",
+    title = "A Tutorial on Recursive Types in Coq",
+    number = "RT-0221",
+    pages = "42 p.",
+    url = "citeseer.nj.nec.com/gimenez98tutorial.html" }
+
+@phdthesis{Coq:Mun97,
+	AUTHOR = "César Mu{\~{n}}oz",
+	TITLE = "Un calcul de substitutions pour la repr\'esentation
+                  de preuves partielles en th\'eorie de types",
+	SCHOOL = {Universit\'e Paris~7},
+        Number = {Unit\'e de recherche INRIA-Rocquencourt, TU-0488},
+	YEAR = "1997",
+        Note = {English version available as INRIA research report RR-3309},
+        Type = {Th\`ese de Doctorat}
+}
+
+@PHDTHESIS{Coq:Filliatre99,
+  AUTHOR = {J.-C. Filli\^atre},
+  TITLE = {{Preuve de programmes imp\'eratifs en th\'eorie des types}},
+  TYPE = {Th{\`e}se de Doctorat},
+  SCHOOL = {Universit\'e Paris-Sud},
+  YEAR = 1999,
+  MONTH = {July},
+}
+
+@manual{Coq:Tutorial,
+  AUTHOR = {G\'erard Huet and Gilles Kahn and Christine Paulin-Mohring},
+  TITLE = {{The Coq Proof Assistant A Tutorial}},
+  YEAR = 2004  
+}
+
+%%%%%%% PVS %%%%%%%
+
+@manual{PVS:prover,
+  title =        "{PVS} Prover Guide",
+  author =       "N. Shankar and S. Owre and J. M. Rushby and D. W. J.
+                 Stringer-Calvert",
+  month =        sep,
+  year =         "1999",
+  organization = "Computer Science Laboratory, SRI International",
+  address =      "Menlo Park, CA",
+}
+
+@techreport{PVS-Semantics:TR,
+  TITLE = {The Formal Semantics of {PVS}},
+  AUTHOR = {Sam Owre and Natarajan Shankar},
+  NUMBER = {CR-1999-209321},
+  INSTITUTION = {Computer Science Laboratory, SRI International},
+  ADDRESS = {Menlo Park, CA},
+  MONTH = may,
+  YEAR = 1999,
+}
+
+@techreport{PVS-Tactics:DiVito,
+  TITLE = {A {PVS} Prover Strategy Package for Common Manipulations},
+  AUTHOR = {Ben L. Di Vito},
+  NUMBER = {TM-2002-211647},
+  INSTITUTION = {Langley Research Center},
+  ADDRESS = {Hampton, VA},
+  MONTH = apr,
+  YEAR = 2002,
+}
+
+@misc{PVS-Tactics:cours,
+  author = "César Muñoz",
+  title = "Strategies in {PVS}",
+  howpublished = "Lecture notes",
+  note = "National Institute of Aerospace",
+  year = 2002
+}
+
+@techreport{PVS-Tactics:field,
+  author = "C. Mu{\~n}oz and M. Mayero",
+  title = "Real Automation in the Field",
+  institution = "ICASE-NASA Langley",
+  number = "NASA/CR-2001-211271 Interim ICASE Report No. 39",
+  month =  "dec",
+  year = "2001"
+}
+
+%%%%%%% Autres Prouveurs %%%%%%%
+
+@misc{ACL2:repNuPrl,
+  author = "James L. Caldwell and John Cowles",
+  title = "{Representing Nuprl Proof Objects in ACL2: toward a proof checker for Nuprl}",
+  url = "http://www.cs.uwyo.edu/~jlc/papers/proof_checking.ps" }
+
+@inproceedings{Elan:ckl-strat,
+  author    = {H. Cirstea and C. Kirchner and L. Liquori},
+  title     = "{Rewrite Strategies in the Rewriting Calculus}",
+  booktitle = {WRLA'02},
+  publisher = "{Elsevier Science B.V.}",
+  series    = {Electronic Notes in Theoretical Computer Science},
+  volume    = {71},
+  year      = {2003},
+}
+
+@book{LCF:GMW,
+  author = {M. Gordon and R. Milner and C. Wadsworth},
+  publisher = {sv},
+  series = {lncs},
+  volume = 78,
+  title = {Edinburgh {LCF}: A Mechanized Logic of Computation},
+  year = 1979
+}
+
+%%%%%%% LaTeX %%%%%%%
+
+@manual{LaTeX:symb,
+  title = "The Great, Big List of \LaTeX\ Symbols",
+  author = "David Carlisle and Scott Pakin and Alexander Holt",
+  month = feb,
+  year = 2001,
+}
+
+@manual{LaTeX:intro,
+  title = "The Not So Short Introduction to \LaTeX2e",
+  author = "Tobias Oetiker",
+  month = jan,
+  year = 1999,
+}
+
+@MANUAL{CoqManualV7,
+  AUTHOR = {{The {Coq} Development Team}},
+  TITLE = {{The Coq Proof Assistant Reference Manual -- Version
+ V7.1}},
+  YEAR = {2001},
+  MONTH = OCT,
+  NOTE = {http://coq.inria.fr}
+}
+
+@MANUAL{CoqManual96,
+  TITLE = {The {Coq Proof Assistant Reference Manual} Version 6.1},
+  AUTHOR = {B. Barras and S. Boutin and C. Cornes and J. Courant and 
+                  J.-C. Filli\^atre and 
+                  H. Herbelin and G. Huet and P. Manoury and C. Mu{\~{n}}oz and
+                  C. Murthy and C. Parent and C. Paulin-Mohring and
+                  A. Sa{\"\i}bi and B. Werner},
+  ORGANIZATION = {{INRIA-Rocquencourt}-{CNRS-ENS Lyon}},
+  URL = {ftp://ftp.inria.fr/INRIA/coq/V6.1/doc/Reference-Manual.dvi.gz},
+  YEAR = 1996,
+  MONTH = DEC
+}
+
+@MANUAL{CoqTutorial99,
+  AUTHOR = {G.~Huet and G.~Kahn and Ch.~Paulin-Mohring},
+  TITLE = {The {\sf Coq} Proof Assistant - A tutorial - Version 6.3},
+  MONTH = JUL,
+  YEAR = {1999},
+  ABSTRACT = {http://coq.inria.fr/doc/tutorial.html}
+}
+
+@MANUAL{CoqTutorialV7,
+  AUTHOR = {G.~Huet and G.~Kahn and Ch.~Paulin-Mohring},
+  TITLE = {The {\sf Coq} Proof Assistant - A tutorial - Version 7.1},
+  MONTH = OCT,
+  YEAR = {2001},
+  NOTE = {http://coq.inria.fr}
+}
+
+@TECHREPORT{modelpa2000,
+  AUTHOR = {B. Bérard and P. Castéran and E. Fleury and L. Fribourg 
+                  and J.-F. Monin and C. Paulin and A. Petit and D. Rouillard},
+  TITLE = {Automates temporisés CALIFE},
+  INSTITUTION = {Calife},
+  YEAR = 2000,
+  URL = {http://www.loria.fr/projets/calife/WebCalifePublic/FOURNITURES/F1.1.ps.gz},
+  TYPE = {Fourniture {F1.1}}
+}
+
+@TECHREPORT{CaFrPaRo2000,
+  AUTHOR = {P. Castéran and E. Freund and C. Paulin and D. Rouillard},
+  TITLE = {Bibliothèques Coq et Isabelle-HOL pour les systèmes de transitions              et les p-automates},
+  INSTITUTION = {Calife},
+  YEAR = 2000,
+  URL = {http://www.loria.fr/projets/calife/WebCalifePublic/FOURNITURES/F5.4.ps.gz},
+  TYPE = {Fourniture {F5.4}}
+}
+
+@PROCEEDINGS{TPHOLs99,
+  TITLE = {International Conference on 
+                  Theorem Proving in Higher Order Logics (TPHOLs'99)},
+  YEAR = 1999,
+  EDITOR = {Y. Bertot and G. Dowek and C. Paulin-Mohring and L. Th{\'e}ry},
+  SERIES = {Lecture Notes in Computer Science},
+  MONTH = SEP,
+  PUBLISHER = {{Sprin\-ger-Verlag}},
+  ADDRESS = {Nice},
+  TYPE_PUBLI = {editeur}
+}
+
+@INPROCEEDINGS{Pau01,
+  AUTHOR = {Christine Paulin-Mohring},
+  TITLE = {Modelisation of Timed Automata in {Coq}},
+  BOOKTITLE = {Theoretical Aspects of Computer Software (TACS'2001)},
+  PAGES = {298--315},
+  YEAR = 2001,
+  EDITOR = {N. Kobayashi and B. Pierce},
+  VOLUME = 2215,
+  SERIES = {Lecture Notes in Computer Science},
+  PUBLISHER = {Springer-Verlag}
+}
+
+@PHDTHESIS{Moh89b,
+  AUTHOR = {C. Paulin-Mohring},
+  MONTH = JAN,
+  SCHOOL = {{Paris 7}},
+  TITLE = {Extraction de programmes dans le {Calcul des Constructions}},
+  TYPE = {Thèse d'université},
+  YEAR = {1989},
+  URL = {http://www.lri.fr/~paulin/these.ps.gz}
+}
+
+@ARTICLE{HuMo92,
+  AUTHOR = {G. Huet and C. Paulin-Mohring},
+  EDITION = {INRIA},
+  JOURNAL = {Courrier du CNRS - Informatique},
+  TITLE = {Preuves et Construction de Programmes},
+  YEAR = {1992},
+  CATEGORY = {national}
+}
+
+@INPROCEEDINGS{LePa94,
+  AUTHOR = {F. Leclerc and C. Paulin-Mohring},
+  TITLE = {Programming with Streams in {Coq}. A case study : The Sieve of Eratosthenes},
+  EDITOR = {H. Barendregt and T. Nipkow},
+  VOLUME = 806,
+  SERIES = {Lecture Notes in Computer Science},
+  BOOKTITLE = {{Types for Proofs and Programs, Types' 93}},
+  YEAR = 1994,
+  PUBLISHER = {Springer-Verlag}
+}
+
+@INPROCEEDINGS{Moh86,
+  AUTHOR = {C. Mohring},
+  ADDRESS = {Cambridge, MA},
+  BOOKTITLE = {Symposium on Logic in Computer Science},
+  PUBLISHER = {IEEE Computer Society Press},
+  TITLE = {Algorithm Development in the {Calculus of Constructions}},
+  YEAR = {1986}
+}
+
+@INPROCEEDINGS{Moh89a,
+  AUTHOR = {C. Paulin-Mohring},
+  ADDRESS = {Austin},
+  BOOKTITLE = {Sixteenth Annual ACM Symposium on Principles of Programming Languages},
+  MONTH = JAN,
+  PUBLISHER = {ACM},
+  TITLE = {Extracting ${F}_{\omega}$'s programs from proofs in the {Calculus of Constructions}},
+  YEAR = {1989}
+}
+
+@INCOLLECTION{Moh89c,
+  AUTHOR = {C. Paulin-Mohring},
+  TITLE = {{R\'ealisabilit\'e et extraction de programmes}},
+  BOOKTITLE = {Logique et Informatique : une introduction},
+  PUBLISHER = {INRIA},
+  YEAR = 1991,
+  EDITOR = {B. Courcelle},
+  VOLUME = 8,
+  SERIES = {Collection Didactique},
+  PAGES = {163-180},
+  CATEGORY = {national}
+}
+
+@INPROCEEDINGS{Moh93,
+  AUTHOR = {C. Paulin-Mohring},
+  BOOKTITLE = {Proceedings of the conference Typed Lambda Calculi a
+nd Applications},
+  EDITOR = {M. Bezem and J.-F. Groote},
+  INSTITUTION = {LIP-ENS Lyon},
+  NOTE = {LIP research report 92-49},
+  NUMBER = 664,
+  SERIES = {Lecture Notes in Computer Science},
+  TITLE = {{Inductive Definitions in the System {Coq} - Rules and Properties}},
+  TYPE = {research report},
+  YEAR = 1993
+}
+
+@ARTICLE{PaWe92,
+  AUTHOR = {C. Paulin-Mohring and B. Werner},
+  JOURNAL = {Journal of Symbolic Computation},
+  TITLE = {{Synthesis of ML programs in the system Coq}},
+  VOLUME = {15},
+  YEAR = {1993},
+  PAGES = {607--640}
+}
+
+@INPROCEEDINGS{Pau96,
+  AUTHOR = {C. Paulin-Mohring},
+  TITLE = {Circuits as streams in {Coq} : Verification of a sequential multiplier},
+  BOOKTITLE = {Types for Proofs and Programs, TYPES'95},
+  EDITOR = {S. Berardi and M. Coppo},
+  SERIES = {Lecture Notes in Computer Science},
+  YEAR = 1996,
+  VOLUME = 1158
+}
+
+@PHDTHESIS{Pau96b,
+  AUTHOR = {Christine Paulin-Mohring},
+  TITLE = {Définitions Inductives en Théorie des Types d'Ordre Supérieur},
+  SCHOOL = {Université Claude Bernard Lyon I},
+  YEAR = 1996,
+  MONTH = DEC,
+  TYPE = {Habilitation à diriger les recherches},
+  URL = {http://www.lri.fr/~paulin/habilitation.ps.gz}
+}
+
+@INPROCEEDINGS{PfPa89,
+  AUTHOR = {F. Pfenning and C. Paulin-Mohring},
+  BOOKTITLE = {Proceedings of Mathematical Foundations of Programming Semantics},
+  NOTE = {technical report CMU-CS-89-209},
+  PUBLISHER = {Springer-Verlag},
+  SERIES = {Lecture Notes in Computer Science},
+  VOLUME = 442,
+  TITLE = {Inductively defined types in the {Calculus of Constructions}},
+  YEAR = {1990}
+}
+
+@MISC{krakatoa02,
+  AUTHOR = {Claude March\'e and Christine Paulin and Xavier Urbain},
+  TITLE = {The \textsc{Krakatoa} proof tool},
+  YEAR = 2002,
+  NOTE = {\url{http://krakatoa.lri.fr/}}
+}
+
+@ARTICLE{marche03jlap,
+  AUTHOR = {Claude March{\'e} and Christine Paulin-Mohring and Xavier Urbain},
+  TITLE = {The \textsc{Krakatoa} Tool for Certification of \textsc{Java/JavaCard} Programs annotated in \textsc{JML}},
+  JOURNAL = {Journal of Logic and Algebraic Programming},
+  YEAR = 2003,
+  NOTE = {To appear},
+  URL = {http://krakatoa.lri.fr},
+  TOPICS = {team}
+}
+@ARTICLE{marche04jlap,
+  AUTHOR = {Claude March{\'e} and Christine Paulin-Mohring and Xavier Urbain},
+  TITLE = {The \textsc{Krakatoa} Tool for Certification of \textsc{Java/JavaCard} Programs annotated in \textsc{JML}},
+  JOURNAL = {Journal of Logic and Algebraic Programming},
+  YEAR = 2004,
+  VOLUME = 58,
+  NUMBER = {1--2},
+  PAGES = {89--106},
+  URL = {http://krakatoa.lri.fr},
+  TOPICS = {team}
+}
+
+@TECHREPORT{catano03deliv,
+  AUTHOR = {N{\'e}stor Cata{\~n}o and Marek Gawkowski and
+Marieke Huisman and Bart Jacobs and Claude March{\'e} and Christine Paulin
+and Erik Poll and Nicole Rauch and Xavier Urbain},
+  TITLE = {Logical Techniques for Applet Verification},
+  INSTITUTION = {VerifiCard Project},
+  YEAR = 2003,
+  TYPE = {Deliverable},
+  NUMBER = {5.2},
+  TOPICS = {team},
+  NOTE = {Available from \url{http://www.verificard.org}}
+}
+
+@TECHREPORT{kmu2002rr,
+  AUTHOR = {Keiichirou Kusakari and Claude Marché and Xavier Urbain},
+  TITLE = {Termination of Associative-Commutative Rewriting using Dependency Pairs Criteria},
+  INSTITUTION = {LRI},
+  YEAR = 2002,
+  TYPE = {Research Report},
+  NUMBER = 1304,
+  TYPE_PUBLI = {interne},
+  TOPICS = {team},
+  NOTE = {\url{http://www.lri.fr/~urbain/textes/rr1304.ps.gz}},
+  URL = {http://www.lri.fr/~urbain/textes/rr1304.ps.gz}
+}
+
+@ARTICLE{marche2004jsc,
+  AUTHOR = {Claude March\'e and Xavier Urbain},
+  TITLE = {Modular {\&} Incremental Proofs of {AC}-Termination},
+  JOURNAL = {Journal of Symbolic Computation},
+  YEAR = 2004,
+  TOPICS = {team}
+}
+
+@INPROCEEDINGS{contejean03wst,
+  AUTHOR = {Evelyne Contejean and Claude Marché and Benjamin Monate and Xavier Urbain},
+  TITLE = {{Proving Termination of Rewriting with {\sc C\textit{i}ME}}},
+  CROSSREF = {wst03},
+  PAGES = {71--73},
+  NOTE = {\url{http://cime.lri.fr/}},
+  URL = {http://cime.lri.fr/},
+  YEAR = 2003,
+  TYPE_PUBLI = {icolcomlec},
+  TOPICS = {team}
+}
+
+@TECHREPORT{contejean04rr,
+  AUTHOR = {Evelyne Contejean and Claude March{\'e} and Ana-Paula Tom{\'a}s and Xavier Urbain},
+  TITLE = {Mechanically proving termination using polynomial interpretations},
+  INSTITUTION = {LRI},
+  YEAR = {2004},
+  TYPE = {Research Report},
+  NUMBER = {1382},
+  TYPE_PUBLI = {interne},
+  TOPICS = {team},
+  URL = {http://www.lri.fr/~urbain/textes/rr1382.ps.gz}
+}
+
+@UNPUBLISHED{duran_sub,
+  AUTHOR = {Francisco Duran and Salvador Lucas and
+  Claude {March\'e} and {Jos\'e} Meseguer and Xavier Urbain},
+  TITLE = {Termination of Membership Equational Programs},
+  NOTE = {Submitted}
+}
+
+@PROCEEDINGS{comon95lncs,
+  TITLE = {Term Rewriting},
+  BOOKTITLE = {Term Rewriting},
+  TOPICS = {team, cclserver},
+  YEAR = 1995,
+  EDITOR = {Hubert Comon and Jean-Pierre Jouannaud},
+  SERIES = {Lecture Notes in Computer Science},
+  VOLUME = {909},
+  PUBLISHER = {{Sprin\-ger-Verlag}},
+  ORGANIZATION = {French Spring School of Theoretical Computer
+		  Science},
+  TYPE_PUBLI = {editeur},
+  CLEF_LABO = {CJ95}
+}
+
+@PROCEEDINGS{lics94,
+  TITLE = {Proceedings of the Ninth Annual IEEE Symposium on Logic
+			in Computer Science},
+  BOOKTITLE = {Proceedings of the Ninth Annual IEEE Symposium on Logic
+			in Computer Science},
+  YEAR = 1994,
+  MONTH = JUL,
+  ADDRESS = {Paris, France},
+  ORGANIZATION = {{IEEE} Comp. Soc. Press}
+}
+
+@PROCEEDINGS{rta91,
+  TITLE = {4th International Conference on Rewriting Techniques and
+                        Applications},
+  BOOKTITLE = {4th International Conference on Rewriting Techniques and
+                        Applications},
+  EDITOR = {Ronald. V. Book},
+  YEAR = 1991,
+  MONTH = APR,
+  ADDRESS = {Como, Italy},
+  PUBLISHER = {{Sprin\-ger-Verlag}},
+  SERIES = {Lecture Notes in Computer Science},
+  VOLUME = 488
+}
+
+@PROCEEDINGS{rta96,
+  TITLE = {7th International Conference on Rewriting Techniques and
+			Applications},
+  BOOKTITLE = {7th International Conference on Rewriting Techniques and
+			Applications},
+  EDITOR = {Harald Ganzinger},
+  PUBLISHER = {{Sprin\-ger-Verlag}},
+  YEAR = 1996,
+  MONTH = JUL,
+  ADDRESS = {New Brunswick, NJ, USA},
+  SERIES = {Lecture Notes in Computer Science},
+  VOLUME = 1103
+}
+
+@PROCEEDINGS{rta97,
+  TITLE = {8th International Conference on Rewriting Techniques and
+			Applications},
+  BOOKTITLE = {8th International Conference on Rewriting Techniques and
+			Applications},
+  EDITOR = {Hubert Comon},
+  PUBLISHER = {{Sprin\-ger-Verlag}},
+  YEAR = 1997,
+  MONTH = JUN,
+  ADDRESS = {Barcelona, Spain},
+  SERIES = {Lecture Notes in Computer Science},
+  VOLUME = {1232}
+}
+
+@PROCEEDINGS{rta98,
+  TITLE = {9th International Conference on Rewriting Techniques and
+			Applications},
+  BOOKTITLE = {9th International Conference on Rewriting Techniques and
+			Applications},
+  EDITOR = {Tobias Nipkow},
+  PUBLISHER = {{Sprin\-ger-Verlag}},
+  YEAR = 1998,
+  MONTH = APR,
+  ADDRESS = {Tsukuba, Japan},
+  SERIES = {Lecture Notes in Computer Science},
+  VOLUME = {1379}
+}
+
+@PROCEEDINGS{rta00,
+  TITLE = {11th International Conference on Rewriting Techniques and Applications},
+  BOOKTITLE = {11th International Conference on Rewriting Techniques and Applications},
+  EDITOR = {Leo Bachmair},
+  PUBLISHER = {{Sprin\-ger-Verlag}},
+  SERIES = {Lecture Notes in Computer Science},
+  VOLUME = 1833,
+  MONTH = JUL,
+  YEAR = 2000,
+  ADDRESS = {Norwich, UK}
+}
+
+@PROCEEDINGS{srt95,
+  TITLE = {Proceedings of the Conference on Symbolic Rewriting
+		  Techniques},
+  BOOKTITLE = {Proceedings of the Conference on Symbolic Rewriting
+		  Techniques},
+  YEAR = 1995,
+  EDITOR = {Manuel Bronstein and Volker Weispfenning},
+  ADDRESS = {Monte Verita, Switzerland}
+}
+
+@BOOK{comon01cclbook,
+  BOOKTITLE = {Constraints in Computational Logics},
+  TITLE = {Constraints in Computational Logics},
+  EDITOR = {Hubert Comon and Claude March{\'e} and Ralf Treinen},
+  YEAR = 2001,
+  PUBLISHER = {{Sprin\-ger-Verlag}},
+  SERIES = {Lecture Notes in Computer Science},
+  VOLUME = 2002,
+  TOPICS = {team},
+  TYPE_PUBLI = {editeur}
+}
+
+@PROCEEDINGS{wst03,
+  BOOKTITLE = {{Extended Abstracts of the 6th International Workshop on Termination, WST'03}},
+  TITLE = {{Extended Abstracts of the 6th International Workshop on Termination, WST'03}},
+  YEAR = {2003},
+  EDITOR = {Albert Rubio},
+  MONTH = JUN,
+  NOTE = {Technical Report DSIC II/15/03, Universidad Politécnica de Valencia, Spain}
+}
+
+@INPROCEEDINGS{FilliatreLetouzey03,
+  AUTHOR = {J.-C. Filli\^atre and P. Letouzey},
+  TITLE = {{Functors for Proofs and Programs}},
+  BOOKTITLE = {Proceedings of The European Symposium on Programming},
+  YEAR = 2004,
+  ADDRESS = {Barcelona, Spain},
+  MONTH = {March 29-April 2},
+  NOTE = {To appear},
+  URL = {http://www.lri.fr/~filliatr/ftp/publis/fpp.ps.gz}
+}
+
+@TECHREPORT{Filliatre03,
+  AUTHOR = {J.-C. Filli\^atre},
+  TITLE = {{Why: a multi-language multi-prover verification tool}},
+  INSTITUTION = {{LRI, Universit\'e Paris Sud}},
+  TYPE = {{Research Report}},
+  NUMBER = {1366},
+  MONTH = {March},
+  YEAR = 2003,
+  URL = {http://www.lri.fr/~filliatr/ftp/publis/why-tool.ps.gz}
+}
+
+@ARTICLE{FilliatrePottier02,
+  AUTHOR = {J.-C. Filli{\^a}tre and F. Pottier},
+  TITLE = {{Producing All Ideals of a Forest, Functionally}},
+  JOURNAL = {Journal of Functional Programming},
+  VOLUME = 13,
+  NUMBER = 5,
+  PAGES = {945--956},
+  MONTH = {September},
+  YEAR = 2003,
+  URL = {http://www.lri.fr/~filliatr/ftp/publis/kr-fp.ps.gz},
+  ABSTRACT = {
+  We present a functional implementation of Koda and Ruskey's
+  algorithm for generating all ideals of a forest poset as a Gray
+  code. Using a continuation-based approach, we give an extremely
+  concise formulation of the algorithm's core. Then, in a number of
+  steps, we derive a first-order version whose efficiency is
+  comparable to a C implementation given by Knuth.}
+}
+
+@UNPUBLISHED{FORS01,
+  AUTHOR = {J.-C. Filli{\^a}tre and S. Owre and H. Rue{\ss} and N. Shankar},
+  TITLE = {Deciding Propositional Combinations of Equalities and Inequalities},
+  NOTE = {Unpublished},
+  MONTH = OCT,
+  YEAR = 2001,
+  URL = {http://www.lri.fr/~filliatr/ftp/publis/ics.ps},
+  ABSTRACT = { 
+  We address the problem of combining individual decision procedures
+  into a single decision procedure.  Our combination approach is based
+  on using the canonizer obtained from Shostak's combination algorithm
+  for equality.  We illustrate our approach with a combination
+  algorithm for equality, disequality, arithmetic inequality, and
+  propositional logic.  Unlike the Nelson--Oppen combination where the
+  processing of equalities is distributed across different closed
+  decision procedures, our combination involves the centralized
+  processing of equalities in a single procedure.  The termination
+  argument for the combination is based on that for Shostak's
+  algorithm.  We also give soundness and completeness arguments.}
+}
+
+@INPROCEEDINGS{ICS,
+  AUTHOR = {J.-C. Filli{\^a}tre and S. Owre and H. Rue{\ss} and N. Shankar},
+  TITLE = {{ICS: Integrated Canonization and Solving (Tool presentation)}},
+  BOOKTITLE = {Proceedings of CAV'2001},
+  EDITOR = {G. Berry and H. Comon and A. Finkel},
+  PUBLISHER = {Springer-Verlag},
+  SERIES = {Lecture Notes in Computer Science},
+  VOLUME = 2102,
+  PAGES = {246--249},
+  YEAR = 2001
+}
+
+@INPROCEEDINGS{Filliatre01a,
+  AUTHOR = {J.-C. Filli\^atre},
+  TITLE = {La supériorité de l'ordre supérieur},
+  BOOKTITLE = {Journées Francophones des Langages Applicatifs},
+  PAGES = {15--26},
+  MONTH = {Janvier},
+  YEAR = 2002,
+  ADDRESS = {Anglet, France},
+  URL = {http://www.lri.fr/~filliatr/ftp/publis/sos.ps.gz},
+  CODE = {http://www.lri.fr/~filliatr/ftp/ocaml/misc/koda-ruskey.ps},
+  ABSTRACT = {
+  Nous présentons ici une écriture fonctionnelle de l'algorithme de
+  Koda-Ruskey, un algorithme pour engendrer une large famille
+  de codes de Gray. En s'inspirant de techniques de programmation par
+  continuation, nous aboutissons à un code de neuf lignes seulement,
+  bien plus élégant que les implantations purement impératives
+  proposées jusqu'ici, notamment par Knuth. Dans un second temps,
+  nous montrons comment notre code peut être légèrement modifié pour
+  aboutir à une version de complexité optimale.
+  Notre implantation en Objective Caml rivalise d'efficacité avec les
+  meilleurs codes C. Nous détaillons les calculs de complexité,
+  un exercice intéressant en présence d'ordre supérieur et d'effets de
+  bord combinés.}
+}
+
+@TECHREPORT{Filliatre00c,
+  AUTHOR = {J.-C. Filli\^atre},
+  TITLE = {{Design of a proof assistant: Coq version 7}},
+  INSTITUTION = {{LRI, Universit\'e Paris Sud}},
+  TYPE = {{Research Report}},
+  NUMBER = {1369},
+  MONTH = {October},
+  YEAR = 2000,
+  URL = {http://www.lri.fr/~filliatr/ftp/publis/coqv7.ps.gz},
+  ABSTRACT = {
+  We present the design and implementation of the new version of the
+  Coq proof assistant. The main novelty is the isolation of the
+  critical part of the system, which consists in a type checker for
+  the Calculus of Inductive Constructions. This kernel is now
+  completely independent of the rest of the system and has been
+  rewritten in a purely functional way. This leads to greater clarity
+  and safety, without compromising efficiency. It also opens the way to
+  the ``bootstrap'' of the Coq system, where the kernel will be
+  certified using Coq itself.}
+}
+
+@TECHREPORT{Filliatre00b,
+  AUTHOR = {J.-C. Filli\^atre},
+  TITLE = {{Hash consing in an ML framework}},
+  INSTITUTION = {{LRI, Universit\'e Paris Sud}},
+  TYPE = {{Research Report}},
+  NUMBER = {1368},
+  MONTH = {September},
+  YEAR = 2000,
+  URL = {http://www.lri.fr/~filliatr/ftp/publis/hash-consing.ps.gz},
+  ABSTRACT = {
+  Hash consing is a technique to share values that are structurally
+  equal. Beyond the obvious advantage of saving memory blocks, hash
+  consing may also be used to gain speed in several operations (like
+  equality test) and data structures (like sets or maps) when sharing is
+  maximal. However, physical adresses cannot be used directly for this
+  purpose when the garbage collector is likely to move blocks
+  underneath. We present an easy solution in such a framework, with
+  many practical benefits.}
+}
+
+@MISC{ocamlweb,
+  AUTHOR = {J.-C. Filli\^atre and C. March\'e},
+  TITLE = {{ocamlweb, a literate programming tool for Objective Caml}},
+  NOTE = {Available at \url{http://www.lri.fr/~filliatr/ocamlweb/}},
+  URL = {http://www.lri.fr/~filliatr/ocamlweb/}
+}
+
+@ARTICLE{Filliatre00a,
+  AUTHOR = {J.-C. Filli\^atre},
+  TITLE = {{Verification of Non-Functional Programs 
+                   using Interpretations in Type Theory}},
+  JOURNAL = {Journal of Functional Programming},
+  VOLUME = 13,
+  NUMBER = 4,
+  PAGES = {709--745},
+  MONTH = {July},
+  YEAR = 2003,
+  NOTE = {English translation of~\cite{Filliatre99}.},
+  URL = {http://www.lri.fr/~filliatr/ftp/publis/jphd.ps.gz},
+  ABSTRACT = {We study the problem of certifying programs combining imperative and
+  functional features within the general framework of type theory.
+  
+  Type theory constitutes a powerful specification language, which is
+  naturally suited for the proof of purely functional programs. To
+  deal with imperative programs, we propose a logical interpretation
+  of an annotated program as a partial proof of its specification. The
+  construction of the corresponding partial proof term is based on a
+  static analysis of the effects of the program, and on the use of
+  monads. The usual notion of monads is refined in order to account
+  for the notion of effect. The missing subterms in the partial proof
+  term are seen as proof obligations, whose actual proofs are left to
+  the user. We show that the validity of those proof obligations
+  implies the total correctness of the program.
+  We also establish a result of partial completeness.
+  
+  This work has been implemented in the Coq proof assistant.
+  It appears as a tactic taking an annotated program as argument and
+  generating a set of proof obligations. Several nontrivial
+  algorithms have been certified using this tactic.}
+}
+
+@ARTICLE{Filliatre99c,
+  AUTHOR = {J.-C. Filli\^atre},
+  TITLE = {{Formal Proof of a Program: Find}},
+  JOURNAL = {Science of Computer Programming},
+  YEAR = 2001,
+  NOTE = {To appear},
+  URL = {http://www.lri.fr/~filliatr/ftp/publis/find.ps.gz},
+  ABSTRACT = {In 1971, C.~A.~R.~Hoare gave the proof of correctness and termination of a
+  rather complex algorithm, in a paper entitled \emph{Proof of a
+    program: Find}. It is a hand-made proof, where the
+  program is given together with its formal specification and where
+  each step is fully 
+  justified by a mathematical reasoning.  We present here a formal
+  proof of the same program in the system Coq, using the
+  recent tactic of the system developed to establishing the total
+  correctness of 
+  imperative programs. We follow Hoare's paper as close as
+  possible, keeping the same program and the same specification. We
+  show that we get exactly the same proof obligations, which are
+  proved in a straightforward way, following the original paper.
+  We also explain how more informal reasonings of Hoare's proof are
+  formalized in the system Coq.
+  This demonstrates the adequacy of the system Coq in the
+  process of certifying imperative programs.}
+}
+
+@TECHREPORT{Filliatre99b,
+  AUTHOR = {J.-C. Filli\^atre},
+  TITLE = {{A theory of monads parameterized by effects}},
+  INSTITUTION = {{LRI, Universit\'e Paris Sud}},
+  TYPE = {{Research Report}},
+  NUMBER = {1367},
+  MONTH = {November},
+  YEAR = 1999,
+  URL = {http://www.lri.fr/~filliatr/ftp/publis/monads.ps.gz},
+  ABSTRACT = {Monads were introduced in computer science to express the semantics
+  of programs with computational effects, while type and effect
+  inference was introduced to mark out those effects.
+  In this article, we propose a combination of the notions of effects
+  and monads, where the monadic operators are parameterized by effects.
+  We establish some relationships between those generalized monads and
+  the classical ones.
+  Then we use a generalized monad to translate imperative programs
+  into purely functional ones. We establish the correctness of that
+  translation. This work has been put into practice in the Coq proof
+  assistant to establish the correctness of imperative programs.}
+}
+
+@PHDTHESIS{Filliatre99,
+  AUTHOR = {J.-C. Filli\^atre},
+  TITLE = {{Preuve de programmes imp\'eratifs en th\'eorie des types}},
+  TYPE = {Th{\`e}se de Doctorat},
+  SCHOOL = {Universit\'e Paris-Sud},
+  YEAR = 1999,
+  MONTH = {July},
+  URL = {http://www.lri.fr/~filliatr/ftp/publis/these.ps.gz},
+  ABSTRACT = {Nous étudions le problème de la certification de programmes mêlant
+  traits impératifs et fonctionnels dans le cadre de la théorie des
+  types.
+
+  La théorie des types constitue un puissant langage de spécification,
+  naturellement adapté à la preuve de programmes purement
+  fonctionnels.  Pour y certifier également des programmes impératifs,
+  nous commençons par exprimer leur sémantique de manière purement
+  fonctionnelle. Cette traduction repose sur une analyse statique des
+  effets de bord des programmes, et sur l'utilisation de la notion de
+  monade, notion que nous raffinons en l'associant à la notion d'effet
+  de manière générale.  Nous montrons que cette traduction est
+  sémantiquement correcte.
+
+  Puis, à partir d'un programme annoté, nous construisons une preuve
+  de sa spécification, traduite de manière fonctionnelle. Cette preuve
+  est bâtie sur la traduction fonctionnelle précédemment
+  introduite. Elle est presque toujours incomplète, les parties
+  manquantes étant autant d'obligations de preuve qui seront laissées
+  à la charge de l'utilisateur.  Nous montrons que la validité de ces
+  obligations entraîne la correction totale du programme.
+
+  Nous avons implanté notre travail dans l'assistant de preuve
+  Coq, avec lequel il est dès à présent distribué. Cette
+  implantation se présente sous la forme d'une tactique prenant en
+  argument un programme annoté et engendrant les obligations de
+  preuve.  Plusieurs algorithmes non triviaux ont été certifiés à
+  l'aide de cet outil (Find, Quicksort, Heapsort, algorithme de
+  Knuth-Morris-Pratt).}
+}
+
+@INPROCEEDINGS{FilliatreMagaud99,
+  AUTHOR = {J.-C. Filli\^atre and N. Magaud},
+  TITLE = {{Certification of sorting algorithms in the system Coq}},
+  BOOKTITLE = {Theorem Proving in Higher Order Logics: 
+                  Emerging Trends},
+  YEAR = 1999,
+  ABSTRACT = {We present the formal proofs of total correctness of three sorting
+  algorithms in the system Coq, namely \textit{insertion sort},
+  \textit{quicksort} and \textit{heapsort}. The implementations are
+  imperative programs working in-place on a given array. Those
+  developments demonstrate the usefulness of inductive types and higher-order
+  logic in the process of software certification. They also
+  show that the proof of rather complex algorithms may be done in a
+  small amount of time --- only a few days for each development ---
+  and without great difficulty.},
+  URL = {http://www.lri.fr/~filliatr/ftp/publis/Filliatre-Magaud.ps.gz}
+}
+
+@INPROCEEDINGS{Filliatre98,
+  AUTHOR = {J.-C. Filli\^atre},
+  TITLE = {{Proof of Imperative Programs in Type Theory}},
+  BOOKTITLE = {International Workshop, TYPES '98, Kloster Irsee, Germany},
+  PUBLISHER = {Springer-Verlag},
+  VOLUME = 1657,
+  SERIES = {Lecture Notes in Computer Science},
+  MONTH = MAR,
+  YEAR = {1998},
+  ABSTRACT = {We present a new approach to certifying imperative programs,
+  in the context of Type Theory.
+  The key is a functional translation of imperative programs, which is
+  made possible by an analysis of their effects.
+  On sequential imperative programs, we get the same proof
+  obligations as those given by Floyd-Hoare logic,
+  but our approach also includes functional constructions.
+  As a side-effect, we propose a way to eradicate the use of auxiliary
+  variables in specifications.
+  This work has been implemented in the Coq Proof Assistant and applied
+  on non-trivial examples.},
+  URL = {http://www.lri.fr/~filliatr/ftp/publis/types98.ps.gz}
+}
+
+@TECHREPORT{Filliatre97,
+  AUTHOR = {J.-C. Filli\^atre},
+  INSTITUTION = {LIP - ENS Lyon},
+  NUMBER = {97--04},
+  TITLE = {{Finite Automata Theory in Coq: 
+                              A constructive proof of Kleene's theorem}},
+  TYPE = {Research Report},
+  MONTH = {February},
+  YEAR = {1997},
+  ABSTRACT = {We describe here a development in the system Coq
+  of a piece of Finite Automata Theory. The main result is the Kleene's
+  theorem, expressing that regular expressions and finite automata
+  define the same languages. From a constructive proof of this result,
+  we automatically obtain a functional program that compiles any
+  regular expression into a finite automata, which constitutes the main
+  part of the implementation of {\tt grep}-like programs. This
+  functional program is obtained by the automatic method of {\em
+  extraction} which removes the logical parts of the proof to keep only
+  its informative contents.  Starting with an idea of what we would
+  have written in ML, we write the specification and do the proofs in
+  such a way that we obtain the expected program, which is therefore
+  efficient.},
+  URL = {ftp://ftp.ens-lyon.fr/pub/LIP/Rapports/RR/RR97/RR97-04.ps.Z}
+}
+
+@TECHREPORT{Filliatre95,
+  AUTHOR = {J.-C. Filli\^atre},
+  INSTITUTION = {LIP - ENS Lyon},
+  NUMBER = {96--25},
+  TITLE = {{A decision procedure for Direct Predicate
+                              Calculus: study and implementation in
+                              the Coq system}},
+  TYPE = {Research Report},
+  MONTH = {February},
+  YEAR = {1995},
+  ABSTRACT = {The paper of J. Ketonen and R. Weyhrauch \emph{A
+  decidable fragment of Predicate Calculus} defines a decidable
+  fragment of first-order predicate logic - Direct Predicate Calculus
+  - as the subset which is provable in Gentzen sequent calculus
+  without the contraction rule, and gives an effective decision
+  procedure for it. This report is a detailed study of this
+  procedure. We extend the decidability to non-prenex formulas. We
+  prove that the intuitionnistic fragment is still decidable, with a
+  refinement of the same procedure. An intuitionnistic version has
+  been implemented in the Coq system using a translation into
+  natural deduction.},
+  URL = {ftp://ftp.ens-lyon.fr/pub/LIP/Rapports/RR/RR96/RR96-25.ps.Z}
+}
+
+@TECHREPORT{Filliatre94,
+  AUTHOR = {J.-C. Filli\^atre},
+  MONTH = {Juillet},
+  INSTITUTION = {Ecole Normale Sup\'erieure},
+  TITLE = {{Une proc\'edure de d\'ecision pour le Calcul des Pr\'edicats Direct~: \'etude et impl\'ementation dans le syst\`eme Coq}},
+  TYPE = {Rapport de {DEA}},
+  YEAR = {1994},
+  URL = {ftp://ftp.lri.fr/LRI/articles/filliatr/memoire.dvi.gz}
+}
+
+@TECHREPORT{CourantFilliatre93,
+  AUTHOR = {J. Courant et J.-C. Filli\^atre},
+  MONTH = {Septembre},
+  INSTITUTION = {Ecole Normale Sup\'erieure},
+  TITLE = {{Formalisation de la th\'eorie des langages 
+                              formels en Coq}},
+  TYPE = {Rapport de ma\^{\i}trise},
+  YEAR = {1993},
+  URL = {http://www.ens-lyon.fr/~jcourant/stage_maitrise.dvi.gz},
+  URL2 = {http://www.ens-lyon.fr/~jcourant/stage_maitrise.ps.gz}
+}
+
+@INPROCEEDINGS{tphols2000-Letouzey,
+        crossref        = "tphols2000",
+        title           = "Formalizing {S}t{\aa}lmarck's algorithm in {C}oq",
+        author          = "Pierre Letouzey and Laurent Th{\'e}ry",
+        pages           = "387--404"}
+
+@PROCEEDINGS{tphols2000,
+        editor          = "J. Harrison and M. Aagaard",
+        booktitle       = "Theorem Proving in Higher Order Logics:
+                           13th International Conference, TPHOLs 2000",
+        series          = "Lecture Notes in Computer Science",
+        volume          = 1869,
+        year            = 2000,
+        publisher       = "Springer-Verlag"}
+
+@InCollection{howe,
+  author =       {Doug Howe},
+  title =        {Computation Meta theory in Nuprl},
+  booktitle =    {The Proceedings of the Ninth International Conference of Autom
+ated Deduction},
+  volume =       {310},
+  editor =       {E. Lusk and R. Overbeek},
+  publisher =    {Springer-Verlag},
+  pages =        {238--257},
+  year =         {1988}
+}
+
+@TechReport{harrison,
+  author =       {John Harrison},
+  title =        {Meta theory and Reflection in Theorem Proving:a Survey and Cri
+tique},
+  institution =  {SRI International Cambridge Computer Science Research Center},
+  year =         {1995},
+  number =       {CRC-053}
+}
+
+@InCollection{cc,
+  author =       {Thierry Coquand and Gérard Huet},
+  title =        {The Calculus of Constructions},
+  booktitle =    {Information and Computation},
+  year =         {1988},
+  volume =       {76},
+  number =       {2/3}
+}
+
+
+@InProceedings{coquandcci,
+  author =       {Thierry Coquand and Christine Paulin-Mohring},
+  title =        {Inductively defined types},
+  booktitle =    {Proceedings of Colog'88},
+  year =         {1990},
+  editor =       {P. Martin-Löf and G. Mints},
+  volume =       {417},
+  series =       {LNCS},
+  publisher = {Springer-Verlag}
+}
+
+
+@InProceedings{boutin,
+  author =       {Samuel Boutin},
+  title =        {Using reflection to build efficient and certified decision pro
+cedures.},
+  booktitle =    {Proceedings of TACS'97},
+  year =         {1997},
+  editor =       {M. Abadi and T. Ito},
+  volume =       {1281},
+  series =       {LNCS},
+  publisher =    {Springer-Verlag}
+}
+
+@Manual{Coq:manual,
+  title =        {The Coq proof assistant reference manual},
+  author =       {\mbox{The Coq development team}},
+  organization = {LogiCal Project},
+  note =         {Version 8.0},
+  year =         {2004},
+  url =          "http://coq.inria.fr"
+}
+
+@string{jfp = "Journal of Functional Programming"}
+@STRING{lncs="Lecture Notes in Computer Science"}
+@STRING{lnai="Lecture Notes in Artificial Intelligence"}
+@string{SV = "{Sprin\-ger-Verlag}"}
+
+@INPROCEEDINGS{Aud91,
+        AUTHOR             = {Ph. Audebaud},
+        BOOKTITLE          = {Proceedings of the sixth Conf. on Logic in Computer Science.},
+        PUBLISHER          = {IEEE},
+        TITLE              = {Partial {Objects} in the {Calculus of Constructions}},
+        YEAR               = {1991}
+}
+
+@PHDTHESIS{Aud92,
+        AUTHOR             = {Ph. Audebaud},
+        SCHOOL             = {{Universit\'e} Bordeaux I},
+        TITLE              = {Extension du Calcul des Constructions par Points fixes},
+        YEAR               = {1992}
+}
+
+@INPROCEEDINGS{Audebaud92b,
+        AUTHOR             = {Ph. Audebaud},
+        BOOKTITLE          = {{Proceedings of the 1992 Workshop on Types for Proofs and Programs}},
+        EDITOR             = {{B. Nordstr\"om and K. Petersson and G. Plotkin}},
+        NOTE               = {Also Research Report LIP-ENS-Lyon},
+        PAGES              = {pp 21--34},
+        TITLE              = {{CC+ : an extension of the Calculus of Constructions with fixpoints}},
+        YEAR               = {1992}
+}
+
+@INPROCEEDINGS{Augustsson85,
+        AUTHOR             = {L. Augustsson},
+        TITLE              = {{Compiling Pattern Matching}},
+        BOOKTITLE          = {Conference Functional Programming and
+Computer Architecture},
+        YEAR               = {1985}
+}
+
+@ARTICLE{BaCo85,
+        AUTHOR             = {J.L. Bates and R.L. Constable},
+        JOURNAL            = {ACM transactions on Programming Languages and Systems},
+        TITLE              = {Proofs as {Programs}},
+        VOLUME             = {7},
+        YEAR               = {1985}
+}
+
+@BOOK{Bar81,
+        AUTHOR             = {H.P. Barendregt},
+        PUBLISHER          = {North-Holland},
+        TITLE              = {The Lambda Calculus its Syntax and Semantics},
+        YEAR               = {1981}
+}
+
+@TECHREPORT{Bar91,
+        AUTHOR             = {H. Barendregt},
+        INSTITUTION        = {Catholic University Nijmegen},
+        NOTE               = {In Handbook of Logic in Computer Science, Vol II},
+        NUMBER             = {91-19},
+        TITLE              = {Lambda {Calculi with Types}},
+        YEAR               = {1991}
+}
+
+@ARTICLE{BeKe92,
+        AUTHOR             = {G. Bellin and J. Ketonen},
+        JOURNAL            = {Theoretical Computer Science},
+        PAGES              = {115--142},
+        TITLE              = {A decision procedure revisited : Notes on direct logic, linear logic and its implementation},
+        VOLUME             = {95},
+        YEAR               = {1992}
+}
+
+@BOOK{Bee85,
+        AUTHOR             = {M.J. Beeson},
+        PUBLISHER          = SV,
+        TITLE              = {Foundations of Constructive Mathematics, Metamathematical Studies},
+        YEAR               = {1985}
+}
+
+@BOOK{Bis67,
+        AUTHOR             = {E. Bishop},
+        PUBLISHER          = {McGraw-Hill},
+        TITLE              = {Foundations of Constructive Analysis},
+        YEAR               = {1967}
+}
+
+@BOOK{BoMo79,
+        AUTHOR             = {R.S. Boyer and J.S. Moore},
+        KEY                = {BoMo79},
+        PUBLISHER          = {Academic Press},
+        SERIES             = {ACM Monograph},
+        TITLE              = {A computational logic},
+        YEAR               = {1979}
+}
+
+@MASTERSTHESIS{Bou92,
+        AUTHOR             = {S. Boutin},
+        MONTH              = sep,
+        SCHOOL             = {{Universit\'e Paris 7}},
+        TITLE              = {Certification d'un compilateur {ML en Coq}},
+        YEAR               = {1992}
+}
+
+@inproceedings{Bou97,
+   title = {Using reflection to build efficient and certified decision procedure
+s},
+   author = {S. Boutin},
+   booktitle = {TACS'97},
+   editor = {Martin Abadi and Takahashi Ito},
+   publisher = SV,
+   series = lncs,
+   volume=1281, 
+   PS={http://pauillac.inria.fr/~boutin/public_w/submitTACS97.ps.gz}, 
+   year = {1997}
+}
+
+@PhdThesis{Bou97These,
+  author =       {S. Boutin},
+  title =        {R\'eflexions sur les quotients},
+  school =       {Paris 7},
+  year =         1997,
+  type =         {th\`ese d'Universit\'e},
+  month =        apr
+}
+
+@ARTICLE{Bru72,
+        AUTHOR             = {N.J. de Bruijn},
+        JOURNAL            = {Indag. Math.},
+        TITLE              = {{Lambda-Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem}},
+        VOLUME             = {34},
+        YEAR               = {1972}
+}
+
+
+@INCOLLECTION{Bru80,
+        AUTHOR             = {N.J. de Bruijn},
+        BOOKTITLE          = {to H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism.},
+        EDITOR             = {J.P. Seldin and J.R. Hindley},
+        PUBLISHER          = {Academic Press},
+        TITLE              = {A survey of the project {Automath}},
+        YEAR               = {1980}
+}
+
+@TECHREPORT{COQ93,
+        AUTHOR             = {G. Dowek and A. Felty and H. Herbelin and G. Huet and C. Murthy and C. Parent and C. Paulin-Mohring and B. Werner},
+        INSTITUTION        = {INRIA},
+        MONTH              = may,
+        NUMBER             = {154},
+        TITLE              = {{The Coq Proof Assistant User's Guide Version 5.8}},
+        YEAR               = {1993}
+}
+
+@TECHREPORT{CPar93,
+        AUTHOR             = {C. Parent},
+        INSTITUTION        = {Ecole {Normale} {Sup\'erieure} de {Lyon}},
+        MONTH              = oct,
+        NOTE               = {Also in~\cite{Nijmegen93}},
+        NUMBER             = {93-29},
+        TITLE              = {Developing certified programs in the system {Coq}- {The} {Program} tactic},
+        YEAR               = {1993}
+}
+
+@PHDTHESIS{CPar95,
+        AUTHOR             = {C. Parent},
+        SCHOOL             = {Ecole {Normale} {Sup\'erieure} de {Lyon}},
+        TITLE              = {{Synth\`ese de preuves de programmes dans le Calcul des Constructions Inductives}},
+        YEAR               = {1995}
+}
+
+@BOOK{Caml,
+        AUTHOR             = {P. Weis and X. Leroy},
+        PUBLISHER          = {InterEditions},
+        TITLE              = {Le langage Caml},
+        YEAR               = {1993}
+}
+
+@INPROCEEDINGS{ChiPotSimp03,
+  AUTHOR    = {Laurent Chicli and Lo\"{\i}c Pottier and Carlos Simpson},
+  ADDRESS   = {Berg en Dal, The Netherlands},
+  TITLE     = {Mathematical Quotients and Quotient Types in Coq},
+  BOOKTITLE = {TYPES'02},
+  PUBLISHER = SV,
+  SERIES    = LNCS,
+  VOLUME    = {2646},
+  YEAR      = {2003}
+}
+
+@TECHREPORT{CoC89,
+        AUTHOR             = {Projet Formel},
+        INSTITUTION        = {INRIA},
+        NUMBER             = {110},
+        TITLE              = {{The Calculus of Constructions. Documentation and user's guide, Version 4.10}},
+        YEAR               = {1989}
+}
+
+@INPROCEEDINGS{CoHu85a,
+        AUTHOR             = {Thierry Coquand and Gérard Huet},
+        ADDRESS            = {Linz},
+        BOOKTITLE          = {EUROCAL'85},
+        PUBLISHER          = SV,
+        SERIES             = LNCS,
+        TITLE              = {{Constructions : A Higher Order Proof System for Mechanizing Mathematics}},
+        VOLUME             = {203},
+        YEAR               = {1985}
+}
+
+@INPROCEEDINGS{CoHu85b,
+        AUTHOR             = {Thierry Coquand and Gérard Huet},
+        BOOKTITLE          = {Logic Colloquium'85},
+        EDITOR             = {The Paris Logic Group},
+        PUBLISHER          = {North-Holland},
+        TITLE              = {{Concepts Math\'ematiques et Informatiques formalis\'es dans le Calcul des Constructions}},
+        YEAR               = {1987}
+}
+
+@ARTICLE{CoHu86,
+        AUTHOR             = {Thierry Coquand and Gérard Huet},
+        JOURNAL            = {Information and Computation},
+        NUMBER             = {2/3},
+        TITLE              = {The {Calculus of Constructions}},
+        VOLUME             = {76},
+        YEAR               = {1988}
+}
+
+@INPROCEEDINGS{CoPa89,
+        AUTHOR             = {Thierry Coquand and Christine Paulin-Mohring},
+        BOOKTITLE          = {Proceedings of Colog'88},
+        EDITOR             = {P. Martin-L\"of and G. Mints},
+        PUBLISHER          = SV,
+        SERIES             = LNCS,
+        TITLE              = {Inductively defined types},
+        VOLUME             = {417},
+        YEAR               = {1990}
+}
+
+@BOOK{Con86,
+        AUTHOR             = {R.L. {Constable et al.}},
+        PUBLISHER          = {Prentice-Hall},
+        TITLE              = {{Implementing Mathematics with the Nuprl Proof Development System}},
+        YEAR               = {1986}
+}
+
+@PHDTHESIS{Coq85,
+        AUTHOR             = {Thierry Coquand},
+        MONTH              = jan,
+        SCHOOL             = {Universit\'e Paris~7},
+        TITLE              = {Une Th\'eorie des Constructions},
+        YEAR               = {1985}
+}
+
+@INPROCEEDINGS{Coq86,
+        AUTHOR             = {Thierry Coquand},
+        ADDRESS            = {Cambridge, MA},
+        BOOKTITLE          = {Symposium on Logic in Computer Science},
+        PUBLISHER          = {IEEE Computer Society Press},
+        TITLE              = {{An Analysis of Girard's Paradox}},
+        YEAR               = {1986}
+}
+
+@INPROCEEDINGS{Coq90,
+        AUTHOR             = {Thierry Coquand},
+        BOOKTITLE          = {Logic and Computer Science},
+        EDITOR             = {P. Oddifredi},
+        NOTE               = {INRIA Research Report 1088, also in~\cite{CoC89}},
+        PUBLISHER          = {Academic Press},
+        TITLE              = {{Metamathematical Investigations of a Calculus of Constructions}},
+        YEAR               = {1990}
+}
+
+@INPROCEEDINGS{Coq91,
+        AUTHOR             = {Thierry Coquand},
+        BOOKTITLE          = {Proceedings 9th Int. Congress of Logic, Methodology and Philosophy of Science},
+        TITLE              = {{A New Paradox in Type Theory}},
+        MONTH              = {August},
+        YEAR               = {1991}
+}
+
+@INPROCEEDINGS{Coq92,
+        AUTHOR             = {Thierry Coquand},
+        TITLE              = {{Pattern Matching with Dependent Types}},
+        YEAR               = {1992},
+        crossref = {Bastad92}
+}
+
+@INPROCEEDINGS{Coquand93,
+        AUTHOR             = {Thierry Coquand},
+        TITLE              = {{Infinite Objects in Type Theory}},
+        YEAR               = {1993},
+        crossref = {Nijmegen93}
+}
+
+@MASTERSTHESIS{Cou94a,
+        AUTHOR             = {J. Courant},
+        MONTH              = sep,
+        SCHOOL             = {DEA d'Informatique, ENS Lyon},
+        TITLE              = {Explicitation de preuves par r\'ecurrence implicite},
+        YEAR               = {1994}
+}
+
+@INPROCEEDINGS{Del99,
+  author    = "Delahaye, D.",
+  title     = "Information Retrieval in a Coq Proof Library using
+               Type Isomorphisms",
+  booktitle = {Proceedings of TYPES'99, L\"okeberg},
+  publisher = SV,
+  series = lncs,
+  year      = "1999",
+  url      =
+    "\\{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"#
+    "{\sf TYPES99-SIsos.ps.gz}"
+}
+
+@INPROCEEDINGS{Del00,
+  author    = "Delahaye, D.",
+  title     = "A {T}actic {L}anguage for the {S}ystem {{\sf Coq}}",
+  booktitle = "Proceedings of Logic for Programming and Automated Reasoning
+               (LPAR), Reunion Island",
+  publisher = SV,
+  series =  LNCS,
+  volume    = "1955",
+  pages     = "85--95",
+  month     = "November",
+  year      = "2000",
+  url      =
+    "{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"#
+    "{\sf LPAR2000-ltac.ps.gz}"
+}
+
+@INPROCEEDINGS{DelMay01,
+  author    = "Delahaye, D. and Mayero, M.",
+  title     = {{\tt Field}: une proc\'edure de d\'ecision pour les nombres r\'eels
+               en {\Coq}},
+  booktitle = "Journ\'ees Francophones des Langages Applicatifs, Pontarlier",
+  publisher = "INRIA",
+  month     = "Janvier",
+  year      = "2001",
+  url      =
+    "\\{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"#
+    "{\sf JFLA2000-Field.ps.gz}"
+}
+
+@TECHREPORT{Dow90,
+        AUTHOR             = {G. Dowek},
+        INSTITUTION        = {INRIA},
+        NUMBER             = {1283},
+        TITLE              = {Naming and Scoping in a Mathematical Vernacular},
+        TYPE               = {Research Report},
+        YEAR               = {1990}
+}
+
+@ARTICLE{Dow91a,
+        AUTHOR             = {G. Dowek},
+        JOURNAL            = {Compte-Rendus de l'Acad\'emie des Sciences},
+        NOTE               = {The undecidability of Third Order Pattern Matching in Calculi with Dependent Types or Type Constructors},
+        NUMBER             = {12},
+        PAGES              = {951--956},
+        TITLE              = {L'Ind\'ecidabilit\'e du Filtrage du Troisi\`eme Ordre dans les Calculs avec Types D\'ependants ou Constructeurs de Types}, 
+        VOLUME             = {I, 312},
+        YEAR               = {1991}
+}		  
+
+@INPROCEEDINGS{Dow91b,
+        AUTHOR             = {G. Dowek},
+        BOOKTITLE          = {Proceedings of Mathematical Foundation of Computer Science},
+        NOTE               = {Also INRIA Research Report},
+        PAGES              = {151--160},
+        PUBLISHER          = SV,
+        SERIES             = LNCS,
+        TITLE              = {A Second Order Pattern Matching Algorithm in the Cube of Typed $\lambda$-calculi},
+        VOLUME             = {520},
+        YEAR               = {1991}
+}
+                  
+@PHDTHESIS{Dow91c,
+        AUTHOR             = {G. Dowek},
+        MONTH              = dec,
+        SCHOOL             = {Universit\'e Paris 7},
+        TITLE              = {D\'emonstration automatique dans le Calcul des Constructions},
+        YEAR               = {1991}
+}
+
+@article{Dow92a,
+        AUTHOR             = {G. Dowek},
+        TITLE              = {The Undecidability of Pattern Matching in Calculi where Primitive Recursive Functions are Representable},
+        YEAR               = 1993,
+        journal = tcs,
+        volume = 107,
+        number = 2,
+        pages = {349-356}
+}
+
+
+@ARTICLE{Dow94a,
+        AUTHOR             = {G. Dowek},
+        JOURNAL            = {Annals of Pure and Applied Logic},
+        VOLUME             = {69},
+        PAGES              = {135--155},
+        TITLE              = {Third order matching is decidable},
+        YEAR               = {1994}
+}
+
+@INPROCEEDINGS{Dow94b,
+        AUTHOR             = {G. Dowek},
+        BOOKTITLE          = {Proceedings of the second international conference on typed lambda calculus and applications},
+        TITLE              = {Lambda-calculus, Combinators and the Comprehension Schema},
+        YEAR               = {1995}
+}
+
+@INPROCEEDINGS{Dyb91,
+        AUTHOR             = {P. Dybjer},
+        BOOKTITLE          = {Logical Frameworks},
+        EDITOR             = {G. Huet and G. Plotkin},
+        PAGES              = {59--79},
+        PUBLISHER          = {Cambridge University Press},
+        TITLE              = {Inductive sets and families in {Martin-L{\"o}f's}
+ Type Theory and their set-theoretic semantics: An inversion principle for {Martin-L\"of's} type theory}, 
+        VOLUME             = {14},
+        YEAR               = {1991}
+}
+
+@ARTICLE{Dyc92,
+        AUTHOR             = {Roy Dyckhoff},
+        JOURNAL            = {The Journal of Symbolic Logic},
+        MONTH              = sep,
+        NUMBER             = {3},
+        TITLE              = {Contraction-free sequent calculi for intuitionistic logic},
+        VOLUME             = {57},
+        YEAR               = {1992}
+}
+
+@MASTERSTHESIS{Fil94,
+        AUTHOR             = {J.-C. Filli\^atre},
+        MONTH              = sep,
+        SCHOOL             = {DEA d'Informatique, ENS Lyon},
+        TITLE              = {Une proc\'edure de d\'ecision pour le Calcul des Pr\'edicats Direct. {\'E}tude et impl\'ementation dans le syst\`eme {\Coq}},
+        YEAR               = {1994}
+}
+
+@TECHREPORT{Filliatre95,
+        AUTHOR             = {J.-C. Filli\^atre},
+        INSTITUTION        = {LIP-ENS-Lyon},
+        TITLE              = {A decision procedure for Direct Predicate Calculus},
+        TYPE               = {Research report},
+        NUMBER             = {96--25},
+        YEAR               = {1995}
+}
+
+@Article{Filliatre03jfp,
+  author = 	 {J.-C. Filli{\^a}tre},
+  title = 	 {Verification of Non-Functional Programs 
+                   using Interpretations in Type Theory},
+  journal =      jfp,
+  volume =       13,
+  number =       4,
+  pages =        {709--745},
+  month =	 jul,
+  year =	 2003,
+  note = 	 {[English translation of \cite{Filliatre99}]},
+  url =          {http://www.lri.fr/~filliatr/ftp/publis/jphd.ps.gz},
+  topics =       "team, lri",
+  type_publi =   "irevcomlec"
+}
+
+
+@PhdThesis{Filliatre99,
+  author = 	 {J.-C. Filli\^atre},
+  title = 	 {Preuve de programmes imp\'eratifs en th\'eorie des types},
+  type =         {Th{\`e}se de Doctorat},
+  school = 	 {Universit\'e Paris-Sud},
+  year = 	 1999,
+  month =	 {July},
+  url =         {\url{http://www.lri.fr/~filliatr/ftp/publis/these.ps.gz}}
+}
+
+@Unpublished{Filliatre99c,
+  author = 	 {J.-C. Filli\^atre},
+  title = 	 {{Formal Proof of a Program: Find}},
+  month =        {January},
+  year =         2000,
+  note = 	 {Submitted to \emph{Science of Computer Programming}},
+  url =         {\url{http://www.lri.fr/~filliatr/ftp/publis/find.ps.gz}}
+}
+
+@InProceedings{FilliatreMagaud99,
+  author = 	 {J.-C. Filli\^atre and N. Magaud},
+  title = 	 {Certification of sorting algorithms in the system {\Coq}},
+  booktitle =    {Theorem Proving in Higher Order Logics: 
+                  Emerging Trends},
+  year =	 1999,
+  url = {\url{http://www.lri.fr/~filliatr/ftp/publis/Filliatre-Magaud.ps.gz}}
+}
+
+@UNPUBLISHED{Fle90,
+        AUTHOR             = {E. Fleury},
+        MONTH              = jul,
+        NOTE               = {Rapport de Stage},
+        TITLE              = {Implantation des algorithmes de {Floyd et de Dijkstra} dans le {Calcul des Constructions}},
+        YEAR               = {1990}
+}
+
+@BOOK{Fourier,
+        AUTHOR             = {Jean-Baptiste-Joseph Fourier},
+        PUBLISHER          = {Gauthier-Villars},
+        TITLE              = {Fourier's method to solve linear 
+                              inequations/equations systems.},
+        YEAR               = {1890}
+}
+
+@INPROCEEDINGS{Gim94,
+        AUTHOR             = {Eduardo Gim\'enez},
+        BOOKTITLE          = {Types'94 : Types for Proofs and Programs},
+        NOTE               = {Extended version in LIP research report 95-07, ENS Lyon},
+        PUBLISHER          = SV,
+        SERIES             = LNCS,
+        TITLE              = {Codifying guarded definitions with recursive schemes},
+        VOLUME             = {996},
+        YEAR               = {1994}
+}
+
+@TechReport{Gim98,
+  author = 	 {E. Gim\'enez},
+  title = 	 {A Tutorial on Recursive Types in Coq},
+  institution =  {INRIA},
+  year = 	 1998,
+  month =	 mar
+}
+
+@INPROCEEDINGS{Gimenez95b,
+        AUTHOR             = {E. Gim\'enez},
+        BOOKTITLE          = {Workshop on Types for Proofs and Programs},
+        SERIES             = LNCS,
+        NUMBER             = {1158},
+        PAGES              = {135-152},
+        TITLE              = {An application of co-Inductive types in Coq: 
+		               verification of the Alternating Bit Protocol},
+        EDITORS            = {S. Berardi and M. Coppo},
+        PUBLISHER          = SV,
+        YEAR               = {1995}
+}
+
+@INPROCEEDINGS{Gir70,
+        AUTHOR             = {Jean-Yves Girard},
+        BOOKTITLE          = {Proceedings of the 2nd Scandinavian Logic Symposium},
+        PUBLISHER          = {North-Holland},
+        TITLE              = {Une extension de l'interpr\'etation de {G\"odel} \`a l'analyse, et son application \`a l'\'elimination des coupures dans l'analyse et la th\'eorie des types},
+        YEAR               = {1970}
+}
+
+@PHDTHESIS{Gir72,
+        AUTHOR             = {Jean-Yves Girard},
+        SCHOOL             = {Universit\'e Paris~7},
+        TITLE              = {Interpr\'etation fonctionnelle et \'elimination des coupures de l'arithm\'etique d'ordre sup\'erieur},
+        YEAR               = {1972}
+}
+
+
+
+@BOOK{Gir89,
+        AUTHOR             = {Jean-Yves Girard and Yves Lafont and Paul Taylor},
+        PUBLISHER          = {Cambridge University Press},
+        SERIES             = {Cambridge Tracts in Theoretical Computer Science 7},
+        TITLE              = {Proofs and Types},
+        YEAR               = {1989}
+}
+
+@TechReport{Har95,
+  author = 	 {John Harrison},
+  title = 	 {Metatheory and Reflection in Theorem Proving: A Survey and Critique},
+  institution =  {SRI International Cambridge Computer Science Research Centre,},
+  year = 	 1995,
+  type =	 {Technical Report},
+  number =	 {CRC-053},
+  abstract =	 {http://www.cl.cam.ac.uk/users/jrh/papers.html}
+}
+
+@MASTERSTHESIS{Hir94,
+        AUTHOR             = {Daniel Hirschkoff},
+        MONTH              = sep,
+        SCHOOL             = {DEA IARFA, Ecole des Ponts et Chauss\'ees, Paris},
+        TITLE              = {{\'E}criture d'une tactique arithm\'etique pour le syst\`eme {\Coq}},
+        YEAR               = {1994}
+}
+
+@INPROCEEDINGS{HofStr98,
+        AUTHOR        = {Martin Hofmann and Thomas Streicher},
+        TITLE         = {The groupoid interpretation of type theory},
+        BOOKTITLE     = {Proceedings of the meeting Twenty-five years of constructive type theory},
+        PUBLISHER     = {Oxford University Press},
+        YEAR          = {1998}
+} 
+
+@INCOLLECTION{How80,
+        AUTHOR             = {W.A. Howard},
+        BOOKTITLE          = {to H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism.},
+        EDITOR             = {J.P. Seldin and J.R. Hindley},
+        NOTE               = {Unpublished 1969 Manuscript},
+        PUBLISHER          = {Academic Press},
+        TITLE              = {The Formulae-as-Types Notion of Constructions},
+        YEAR               = {1980}
+}
+
+
+
+@InProceedings{Hue87tapsoft,
+  author = 	 {G. Huet},
+  title = 	 {Programming of Future Generation Computers},
+  booktitle = 	 {Proceedings of TAPSOFT87},
+       series = LNCS,
+        volume = 249,
+  pages =	 {276--286},
+  year =	 1987,
+  publisher =	 SV
+}
+
+@INPROCEEDINGS{Hue87,
+        AUTHOR             = {G. Huet},
+        BOOKTITLE          = {Programming of Future Generation Computers},
+        EDITOR             = {K. Fuchi and M. Nivat},
+        NOTE               = {Also in \cite{Hue87tapsoft}},
+        PUBLISHER          = {Elsevier Science},
+        TITLE              = {Induction Principles Formalized in the {Calculus of Constructions}},
+        YEAR               = {1988}
+}
+
+
+
+@INPROCEEDINGS{Hue88,
+        AUTHOR             = {G. Huet},
+        BOOKTITLE          = {A perspective in Theoretical Computer Science. Commemorative Volume for Gift Siromoney},
+        EDITOR             = {R. Narasimhan},
+        NOTE               = {Also in~\cite{CoC89}},
+        PUBLISHER          = {World Scientific Publishing},
+        TITLE              = {{The Constructive Engine}},
+        YEAR               = {1989}
+}
+
+@BOOK{Hue89,
+        EDITOR             = {G. Huet},
+        PUBLISHER          = {Addison-Wesley},
+        SERIES             = {The UT Year of Programming Series},
+        TITLE              = {Logical Foundations of Functional Programming},
+        YEAR               = {1989}
+}
+
+@INPROCEEDINGS{Hue92,
+        AUTHOR             = {G. Huet},
+        BOOKTITLE          = {Proceedings of 12th FST/TCS Conference, New Delhi},
+        PAGES              = {229--240},
+        PUBLISHER          = SV,
+        SERIES             = LNCS,
+        TITLE              = {The Gallina Specification Language : A case study},
+        VOLUME             = {652},
+        YEAR               = {1992}
+}
+
+@ARTICLE{Hue94,
+        AUTHOR             = {G. Huet},
+        JOURNAL            = {J. Functional Programming},
+        PAGES              = {371--394},
+        PUBLISHER          = {Cambridge University Press},
+        TITLE              = {Residual theory in $\lambda$-calculus: a formal development},
+        VOLUME             = {4,3},
+        YEAR               = {1994}
+}
+
+@INCOLLECTION{HuetLevy79,
+        AUTHOR             = {G. Huet and J.-J. L\'{e}vy},
+        TITLE              = {Call by Need Computations in Non-Ambigous
+Linear Term Rewriting Systems},
+        NOTE               = {Also research report 359, INRIA, 1979},
+        BOOKTITLE          = {Computational Logic, Essays in Honor of
+Alan Robinson},
+        EDITOR             = {J.-L. Lassez and G. Plotkin},
+        PUBLISHER          = {The MIT press},
+        YEAR               = {1991}
+}
+
+@ARTICLE{KeWe84,
+        AUTHOR             = {J. Ketonen and R. Weyhrauch},
+        JOURNAL            = {Theoretical Computer Science},
+        PAGES              = {297--307},
+        TITLE              = {A decidable fragment of {P}redicate {C}alculus},
+        VOLUME             = {32},
+        YEAR               = {1984}
+}
+
+@BOOK{Kle52,
+        AUTHOR             = {S.C. Kleene},
+        PUBLISHER          = {North-Holland},
+        SERIES             = {Bibliotheca Mathematica},
+        TITLE              = {Introduction to Metamathematics},
+        YEAR               = {1952}
+}
+
+@BOOK{Kri90,
+        AUTHOR             = {J.-L. Krivine},
+        PUBLISHER          = {Masson},
+        SERIES             = {Etudes et recherche en informatique},
+        TITLE              = {Lambda-calcul {types et mod\`eles}},
+        YEAR               = {1990}
+}
+
+@BOOK{LE92,
+        EDITOR             = {G. Huet and G. Plotkin},
+        PUBLISHER          = {Cambridge University Press},
+        TITLE              = {Logical Environments},
+        YEAR               = {1992}
+}
+
+@BOOK{LF91,
+        EDITOR             = {G. Huet and G. Plotkin},
+        PUBLISHER          = {Cambridge University Press},
+        TITLE              = {Logical Frameworks},
+        YEAR               = {1991}
+}
+
+@ARTICLE{Laville91,
+        AUTHOR             = {A. Laville},
+        TITLE              = {Comparison of Priority Rules in Pattern
+Matching and Term Rewriting},
+        JOURNAL            = {Journal of Symbolic Computation},
+        VOLUME             = {11},
+        PAGES              = {321--347},
+        YEAR               = {1991}
+}
+
+@INPROCEEDINGS{LePa94,
+        AUTHOR             = {F. Leclerc and C. Paulin-Mohring},
+        BOOKTITLE          = {{Types for Proofs and Programs, Types' 93}},
+        EDITOR             = {H. Barendregt and T. Nipkow},
+        PUBLISHER          = SV,
+        SERIES             = {LNCS},
+        TITLE              = {{Programming with Streams in Coq. A case study : The Sieve of Eratosthenes}},
+        VOLUME             = {806},
+        YEAR               = {1994}
+}
+
+@TECHREPORT{Leroy90,
+        AUTHOR             = {X. Leroy},
+        TITLE              = {The {ZINC} experiment: an economical implementation
+of the {ML} language},
+        INSTITUTION        = {INRIA},
+        NUMBER             = {117},
+        YEAR               = {1990}
+}
+
+@INPROCEEDINGS{Let02,
+        author          = {P. Letouzey},
+        title           = {A New Extraction for Coq},
+        booktitle       = {Proceedings of the TYPES'2002 workshop},
+        year            = 2002,
+        note            = {to appear},
+        url            = {draft at \url{http://www.lri.fr/~letouzey/download/extraction2002.ps.gz}}
+}
+
+@BOOK{MaL84,
+        AUTHOR             = {{P. Martin-L\"of}},
+        PUBLISHER          = {Bibliopolis},
+        SERIES             = {Studies in Proof Theory},
+        TITLE              = {Intuitionistic Type Theory},
+        YEAR               = {1984}
+}
+
+@ARTICLE{MaSi94,
+        AUTHOR             = {P. Manoury and M. Simonot},
+        JOURNAL            = {TCS},
+        TITLE              = {Automatizing termination proof of recursively defined function},
+        YEAR               = {To appear}
+}
+
+@INPROCEEDINGS{Moh89a,
+        AUTHOR             = {Christine Paulin-Mohring},
+        ADDRESS            = {Austin},
+        BOOKTITLE          = {Sixteenth Annual ACM Symposium on Principles of Programming Languages},
+        MONTH              = jan,
+        PUBLISHER          = {ACM},
+        TITLE              = {Extracting ${F}_{\omega}$'s programs from proofs in the {Calculus of Constructions}},
+        YEAR               = {1989}
+}
+
+@PHDTHESIS{Moh89b,
+        AUTHOR             = {Christine Paulin-Mohring},
+        MONTH              = jan,
+        SCHOOL             = {{Universit\'e Paris 7}},
+        TITLE              = {Extraction de programmes dans le {Calcul des Constructions}},
+        YEAR               = {1989}
+}
+
+@INPROCEEDINGS{Moh93,
+        AUTHOR             = {Christine Paulin-Mohring},
+        BOOKTITLE          = {Proceedings of the conference Typed Lambda Calculi and Applications},
+        EDITOR             = {M. Bezem and J.-F. Groote},
+        NOTE               = {Also LIP research report 92-49, ENS Lyon},
+        NUMBER             = {664},
+        PUBLISHER          = SV,
+        SERIES             = {LNCS},
+        TITLE              = {{Inductive Definitions in the System Coq - Rules and Properties}},
+        YEAR               = {1993}
+}
+
+@BOOK{Moh97,
+        AUTHOR             = {Christine Paulin-Mohring},
+        MONTH              = jan,
+        PUBLISHER          = {{ENS Lyon}},
+        TITLE              = {{Le syst\`eme Coq. \mbox{Th\`ese d'habilitation}}},
+        YEAR               = {1997}
+}
+
+@MASTERSTHESIS{Mun94,
+        AUTHOR             = {C. Mu{\~n}oz},
+        MONTH              = sep,
+        SCHOOL             = {DEA d'Informatique Fondamentale, Universit\'e Paris 7},
+        TITLE              = {D\'emonstration automatique dans la logique propositionnelle intuitionniste},
+        YEAR               = {1994}
+}
+
+@PHDTHESIS{Mun97d,
+        AUTHOR = "C. Mu{\~{n}}oz",
+        TITLE = "Un calcul de substitutions pour la repr\'esentation
+                  de preuves partielles en th\'eorie de types",
+        SCHOOL = {Universit\'e Paris 7},
+        YEAR = "1997",
+        Note = {Version en anglais disponible comme rapport de 
+                recherche INRIA RR-3309},        
+        Type = {Th\`ese de Doctorat}
+}
+
+@BOOK{NoPS90,
+        AUTHOR             = {B. {Nordstr\"om} and K. Peterson and J. Smith},
+        BOOKTITLE          = {Information Processing 83},
+        PUBLISHER          = {Oxford Science Publications},
+        SERIES             = {International Series of Monographs on Computer Science},
+        TITLE              = {Programming in {Martin-L\"of's} Type Theory},
+        YEAR               = {1990}
+}
+
+@ARTICLE{Nor88,
+        AUTHOR             = {B. {Nordstr\"om}},
+        JOURNAL            = {BIT},
+        TITLE              = {Terminating General Recursion},
+        VOLUME             = {28},
+        YEAR               = {1988}
+}
+
+@BOOK{Odi90,
+        EDITOR             = {P. Odifreddi},
+        PUBLISHER          = {Academic Press},
+        TITLE              = {Logic and Computer Science},
+        YEAR               = {1990}
+}
+
+@INPROCEEDINGS{PaMS92,
+        AUTHOR             = {M. Parigot and P. Manoury and M. Simonot},
+        ADDRESS            = {St. Petersburg, Russia},
+        BOOKTITLE          = {Logic Programming and automated reasoning},
+        EDITOR             = {A. Voronkov},
+        MONTH              = jul,
+        NUMBER             = {624},
+        PUBLISHER          = SV,
+        SERIES             = {LNCS},
+        TITLE              = {{ProPre : A Programming language with proofs}},
+        YEAR               = {1992}
+}
+
+@ARTICLE{PaWe92,
+        AUTHOR             = {Christine Paulin-Mohring and Benjamin Werner},
+        JOURNAL            = {Journal of Symbolic Computation},
+        PAGES              = {607--640},
+        TITLE              = {{Synthesis of ML programs in the system Coq}},
+        VOLUME             = {15},
+        YEAR               = {1993}
+}
+
+@ARTICLE{Par92,
+        AUTHOR             = {M. Parigot},
+        JOURNAL            = {Theoretical Computer Science},
+        NUMBER             = {2},
+        PAGES              = {335--356},
+        TITLE              = {{Recursive Programming with Proofs}},
+        VOLUME             = {94},
+        YEAR               = {1992}
+}
+
+@INPROCEEDINGS{Parent95b,
+        AUTHOR             = {C. Parent},
+        BOOKTITLE          = {{Mathematics of Program Construction'95}},
+        PUBLISHER          = SV,
+        SERIES             = {LNCS},
+        TITLE              = {{Synthesizing proofs from programs in
+the Calculus of Inductive Constructions}},
+        VOLUME             = {947},
+        YEAR               = {1995}
+}
+
+@INPROCEEDINGS{Prasad93,
+        AUTHOR             = {K.V. Prasad},
+        BOOKTITLE          = {{Proceedings of CONCUR'93}},
+        PUBLISHER          = SV,
+        SERIES             = {LNCS},
+        TITLE              = {{Programming with broadcasts}},
+        VOLUME             = {715},
+        YEAR               = {1993}
+}
+
+@BOOK{RC95,
+  author = "di~Cosmo, R.",
+  title  = "Isomorphisms of Types: from $\lambda$-calculus to information
+            retrieval and language design",
+  series = "Progress in Theoretical Computer Science",
+  publisher = "Birkhauser",
+  year = "1995",
+  note = "ISBN-0-8176-3763-X"
+}
+
+@TECHREPORT{Rou92,
+        AUTHOR             = {J. Rouyer},
+        INSTITUTION        = {INRIA},
+        MONTH              = nov,
+        NUMBER             = {1795},
+        TITLE              = {{D{\'e}veloppement de l'Algorithme d'Unification dans le Calcul des Constructions}},
+        YEAR               = {1992}
+}
+
+@TECHREPORT{Saibi94,
+        AUTHOR             = {A. Sa\"{\i}bi},
+        INSTITUTION        = {INRIA},
+        MONTH              = dec,
+        NUMBER             = {2345},
+        TITLE              = {{Axiomatization of a lambda-calculus with explicit-substitutions in the Coq System}},
+        YEAR               = {1994}
+}
+
+
+@MASTERSTHESIS{Ter92,
+        AUTHOR             = {D. Terrasse},
+        MONTH              = sep,
+        SCHOOL             = {IARFA},
+        TITLE              = {{Traduction de TYPOL en COQ. Application \`a Mini ML}},
+        YEAR               = {1992}
+}
+
+@TECHREPORT{ThBeKa92,
+        AUTHOR             = {L. Th\'ery and Y. Bertot and G. Kahn},
+        INSTITUTION        = {INRIA Sophia},
+        MONTH              = may,
+        NUMBER             = {1684},
+        TITLE              = {Real theorem provers deserve real user-interfaces},
+        TYPE               = {Research Report},
+        YEAR               = {1992}
+}
+
+@BOOK{TrDa89,
+        AUTHOR             = {A.S. Troelstra and D. van Dalen},
+        PUBLISHER          = {North-Holland},
+        SERIES             = {Studies in Logic and the foundations of Mathematics, volumes 121 and 123},
+        TITLE              = {Constructivism in Mathematics, an introduction},
+        YEAR               = {1988}
+}
+
+@PHDTHESIS{Wer94,
+        AUTHOR             = {B. Werner},
+        SCHOOL             = {Universit\'e Paris 7},
+        TITLE              = {Une th\'eorie des constructions inductives},
+        TYPE               = {Th\`ese de Doctorat},
+        YEAR               = {1994}
+}
+
+@PHDTHESIS{Bar99,
+        AUTHOR             = {B. Barras},
+        SCHOOL             = {Universit\'e Paris 7},
+        TITLE              = {Auto-validation d'un système de preuves avec familles inductives},
+        TYPE               = {Th\`ese de Doctorat},
+        YEAR               = {1999}
+}
+
+@UNPUBLISHED{ddr98,
+	AUTHOR	           = {D. de Rauglaudre},
+        TITLE              = {Camlp4 version 1.07.2},
+        YEAR               = {1998},
+        NOTE               = {In Camlp4 distribution}
+}
+
+@ARTICLE{dowek93,
+        AUTHOR             = {G. Dowek},
+        TITLE              = {{A Complete Proof Synthesis Method for the Cube of Type Systems}},
+        JOURNAL            = {Journal Logic Computation},
+        VOLUME             = {3},
+        NUMBER             = {3},
+        PAGES              = {287--315},
+        MONTH              = {June},
+        YEAR               = {1993}
+}
+
+@INPROCEEDINGS{manoury94,
+        AUTHOR             = {P. Manoury},
+        TITLE              = {{A User's Friendly Syntax to Define
+Recursive Functions as Typed $\lambda-$Terms}},
+        BOOKTITLE          = {{Types for Proofs and Programs, TYPES'94}},
+        SERIES             = {LNCS},
+        VOLUME             = {996},
+        MONTH              = jun,
+        YEAR               = {1994}
+}
+
+@TECHREPORT{maranget94,
+        AUTHOR             = {L. Maranget},
+        INSTITUTION        = {INRIA},
+        NUMBER             = {2385},
+        TITLE              = {{Two Techniques for Compiling Lazy Pattern Matching}},
+        YEAR               = {1994}
+}
+
+@INPROCEEDINGS{puel-suarez90,
+        AUTHOR             = {L.Puel and A. Su\'arez},
+        BOOKTITLE          = {{Conference Lisp and Functional Programming}},
+        SERIES             = {ACM},
+        PUBLISHER          = SV,
+        TITLE              = {{Compiling Pattern Matching by Term
+Decomposition}},
+        YEAR               = {1990}
+}
+
+@MASTERSTHESIS{saidi94,
+        AUTHOR             = {H. Saidi},
+        MONTH              = sep,
+        SCHOOL             = {DEA d'Informatique Fondamentale, Universit\'e Paris 7},
+        TITLE              = {R\'esolution d'\'equations dans le syst\`eme T
+ de G\"odel},
+        YEAR               = {1994}
+}
+
+@misc{streicher93semantical,
+  author = "T. Streicher",
+  title = "Semantical Investigations into Intensional Type Theory",
+  note = "Habilitationsschrift, LMU Munchen.",
+  year = "1993" }
+
+
+
+@Misc{Pcoq,
+  author =	 {Lemme Team},
+  title =	 {Pcoq a graphical user-interface for {Coq}},
+  note =	 {\url{http://www-sop.inria.fr/lemme/pcoq/}}
+}
+
+
+@Misc{ProofGeneral,
+  author =	 {David Aspinall},
+  title =	 {Proof General},
+  note =	 {\url{http://proofgeneral.inf.ed.ac.uk/}}
+}
+
+
+
+@Book{CoqArt,
+  author =	 {Yves bertot and Pierre Castéran},
+  title = 	 {Coq'Art},
+  publisher = 	 {Springer-Verlag},
+  year = 	 2004,
+  note =	 {To appear}
+}
+
+@INCOLLECTION{wadler87,
+        AUTHOR             = {P. Wadler},
+        TITLE              = {Efficient  Compilation of Pattern Matching},
+        BOOKTITLE          = {The Implementation of Functional Programming
+Languages},
+        EDITOR             = {S.L. Peyton Jones},
+        PUBLISHER          = {Prentice-Hall},
+        YEAR               = {1987}
+}
+
+
+@COMMENT{cross-references, must be at end}
+
+@BOOK{Bastad92,
+        EDITOR             = {B. Nordstr\"om and K. Petersson and G. Plotkin},
+        PUBLISHER          = {Available by ftp at site ftp.inria.fr},
+        TITLE              = {Proceedings of the 1992 Workshop on Types for Proofs and Programs},
+        YEAR               = {1992}
+}
+
+@BOOK{Nijmegen93,
+        EDITOR             = {H. Barendregt and T. Nipkow},
+        PUBLISHER          = SV,
+        SERIES             = LNCS,
+        TITLE              = {Types for Proofs and Programs},
+        VOLUME             = {806},
+        YEAR               = {1994}
+}
+
diff --git a/doc/faq/hevea.sty b/doc/faq/hevea.sty
new file mode 100644
index 000000000..6d49aa8ce
--- /dev/null
+++ b/doc/faq/hevea.sty
@@ -0,0 +1,78 @@
+% hevea  : hevea.sty
+% This is a very basic style file for latex document to be processed
+% with hevea. It contains definitions of LaTeX environment which are
+% processed in a special way by the translator. 
+%  Mostly :
+%     - latexonly, not processed by hevea, processed by latex.
+%     - htmlonly , the reverse.
+%     - rawhtml,  to include raw HTML in hevea output.
+%     - toimage, to send text to the image file.
+% The package also provides hevea logos, html related commands (ahref
+% etc.), void cutting and image commands.
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{hevea}[2002/01/11]
+\RequirePackage{comment}
+\newif\ifhevea\heveafalse
+\@ifundefined{ifimagen}{\newif\ifimagen\imagenfalse}
+\makeatletter%
+\newcommand{\heveasmup}[2]{%
+\raise #1\hbox{$\m@th$%
+  \csname S@\f@size\endcsname
+  \fontsize\sf@size 0%
+  \math@fontsfalse\selectfont
+#2%
+}}%
+\DeclareRobustCommand{\hevea}{H\kern-.15em\heveasmup{.2ex}{E}\kern-.15emV\kern-.15em\heveasmup{.2ex}{E}\kern-.15emA}%
+\DeclareRobustCommand{\hacha}{H\kern-.15em\heveasmup{.2ex}{A}\kern-.15emC\kern-.1em\heveasmup{.2ex}{H}\kern-.15emA}%
+\DeclareRobustCommand{\html}{\protect\heveasmup{0.ex}{HTML}}
+%%%%%%%%% Hyperlinks hevea style
+\newcommand{\ahref}[2]{{#2}}
+\newcommand{\ahrefloc}[2]{{#2}}
+\newcommand{\aname}[2]{{#2}}
+\newcommand{\ahrefurl}[1]{\texttt{#1}}
+\newcommand{\footahref}[2]{#2\footnote{\texttt{#1}}}
+\newcommand{\mailto}[1]{\texttt{#1}}
+\newcommand{\imgsrc}[2][]{}
+\newcommand{\home}[1]{\protect\raisebox{-.75ex}{\char126}#1}
+\AtBeginDocument
+{\@ifundefined{url}
+{%url package is not loaded
+\let\url\ahref\let\oneurl\ahrefurl\let\footurl\footahref}
+{}}
+%% Void cutting instructions
+\newcounter{cuttingdepth}
+\newcommand{\tocnumber}{}
+\newcommand{\notocnumber}{}
+\newcommand{\cuttingunit}{}
+\newcommand{\cutdef}[2][]{}
+\newcommand{\cuthere}[2]{}
+\newcommand{\cutend}{}
+\newcommand{\htmlhead}[1]{}
+\newcommand{\htmlfoot}[1]{}
+\newcommand{\htmlprefix}[1]{}
+\newenvironment{cutflow}[1]{}{}
+\newcommand{\cutname}[1]{}
+\newcommand{\toplinks}[3]{}
+%%%% Html only
+\excludecomment{rawhtml}
+\newcommand{\rawhtmlinput}[1]{}
+\excludecomment{htmlonly}
+%%%% Latex only
+\newenvironment{latexonly}{}{}
+\newenvironment{verblatex}{}{}
+%%%% Image file stuff
+\def\toimage{\endgroup}
+\def\endtoimage{\begingroup\def\@currenvir{toimage}}
+\def\verbimage{\endgroup}
+\def\endverbimage{\begingroup\def\@currenvir{verbimage}}
+\newcommand{\imageflush}[1][]{}
+%%% Bgcolor definition
+\newsavebox{\@bgcolorbin}
+\newenvironment{bgcolor}[2][]
+  {\newcommand{\@mycolor}{#2}\begin{lrbox}{\@bgcolorbin}\vbox\bgroup}
+  {\egroup\end{lrbox}%
+   \begin{flushleft}%
+   \colorbox{\@mycolor}{\usebox{\@bgcolorbin}}%
+   \end{flushleft}}
+%%% Postlude
+\makeatother
diff --git a/doc/faq/interval_discr.v b/doc/faq/interval_discr.v
new file mode 100644
index 000000000..972300dac
--- /dev/null
+++ b/doc/faq/interval_discr.v
@@ -0,0 +1,419 @@
+(** Sketch of the proof of {p:nat|p<=n} = {p:nat|p<=m} -> n=m
+
+  - preliminary results on the irrelevance of boundedness proofs
+  - introduce the notion of finite cardinal |A|
+  - prove that |{p:nat|p<=n}| = n
+  - prove that |A| = n /\ |A| = m -> n = m if equality is decidable on A
+  - prove that equality is decidable on A
+  - conclude
+*)
+
+(** * Preliminary results on [nat] and [le] *)
+
+(** Proving axiom K on [nat] *)
+
+Require Import Eqdep_dec.
+Require Import Arith.
+
+Theorem eq_rect_eq_nat :
+  forall (p:nat) (Q:nat->Type) (x:Q p) (h:p=p), x = eq_rect p Q x p h.
+Proof.
+intros.
+apply K_dec_set with (p := h).
+apply eq_nat_dec.
+reflexivity.
+Qed.
+
+(** Proving unicity of proofs of [(n<=m)%nat] *)
+
+Scheme le_ind' := Induction for le Sort Prop.
+
+Theorem le_uniqueness_proof : forall (n m : nat) (p q : n <= m), p = q.
+Proof.
+induction p using le_ind'; intro q.
+ replace (le_n n) with
+  (eq_rect _ (fun n0 => n <= n0) (le_n n) _ (refl_equal n)).
+ 2:reflexivity.
+  generalize (refl_equal n).
+    pattern n at 2 4 6 10, q; case q; [intro | intros m l e].
+     rewrite <- eq_rect_eq_nat; trivial.
+     contradiction (le_Sn_n m); rewrite <- e; assumption.
+ replace (le_S n m p) with
+  (eq_rect _ (fun n0 => n <= n0) (le_S n m p) _ (refl_equal (S m))).
+ 2:reflexivity.
+  generalize (refl_equal (S m)).
+    pattern (S m) at 1 3 4 6, q; case q; [intro Heq | intros m0 l HeqS].
+     contradiction (le_Sn_n m); rewrite Heq; assumption.
+     injection HeqS; intro Heq; generalize l HeqS.
+      rewrite <- Heq; intros; rewrite <- eq_rect_eq_nat.
+      rewrite (IHp l0); reflexivity.
+Qed.
+
+(** Proving irrelevance of boundedness proofs while building
+    elements of interval *)
+
+Lemma dep_pair_intro :
+  forall (n x y:nat) (Hx : x<=n) (Hy : y<=n), x=y ->
+    exist (fun x => x <= n) x Hx = exist (fun x => x <= n) y Hy.
+Proof.
+intros n x y Hx Hy Heq.
+generalize Hy.
+rewrite <- Heq.
+intros.
+rewrite (le_uniqueness_proof x n Hx Hy0).
+reflexivity.
+Qed.
+
+(** * Proving that {p:nat|p<=n} = {p:nat|p<=m} -> n=m *)
+
+(** Definition of having finite cardinality [n+1] for a set [A] *)
+
+Definition card (A:Set) n :=
+  exists f, 
+    (forall x:A, f x <= n) /\
+    (forall x y:A, f x = f y -> x = y) /\
+    (forall m, m <= n -> exists x:A, f x = m).
+
+Require Import Arith.
+
+(** Showing that the interval [0;n] has cardinality [n+1] *)
+
+Theorem card_interval : forall n, card {x:nat|x<=n} n.
+Proof.
+intro n.
+exists (fun x:{x:nat|x<=n} => proj1_sig x).
+split.
+(* bounded *)
+intro x; apply (proj2_sig x).
+split.
+(* injectivity *) 
+intros (p,Hp) (q,Hq).
+simpl.
+intro Hpq.
+apply dep_pair_intro; assumption.
+(* surjectivity *)
+intros m Hmn.
+exists (exist (fun x : nat => x <= n) m Hmn).
+reflexivity.
+Qed.
+
+(** Showing that equality on the interval [0;n] is decidable *)
+
+Lemma interval_dec :
+  forall n (x y : {m:nat|m<=n}), {x=y}+{x<>y}.
+Proof.
+intros n (p,Hp).
+induction p; intros ([|q],Hq).
+left.
+  apply dep_pair_intro.
+  reflexivity.
+right.
+  intro H; discriminate H.
+right.
+  intro H; discriminate H.
+assert (Hp' : p <= n).
+  apply le_Sn_le; assumption.
+assert (Hq' : q <= n).
+  apply le_Sn_le; assumption.
+destruct (IHp Hp' (exist (fun m => m <= n) q Hq'))
+  as [Heq|Hneq].
+left.
+  injection Heq; intro Heq'.
+  apply dep_pair_intro.
+  apply eq_S.
+  assumption.
+right.
+  intro HeqS. 
+  injection HeqS; intro Heq.
+  apply Hneq.
+  apply dep_pair_intro.
+  assumption.
+Qed.
+
+(** Showing that the cardinality relation is functional on decidable sets *)
+
+Lemma card_inj_aux :
+  forall (A:Type) f g n, 
+    (forall x:A, f x <= 0) ->
+    (forall x y:A, f x = f y -> x = y) ->
+    (forall m, m <= S n -> exists x:A, g x = m)
+     -> False.
+Proof.
+intros A f g n Hfbound Hfinj Hgsurj.
+destruct (Hgsurj (S n) (le_n _)) as (x,Hx).
+destruct (Hgsurj n (le_S _ _ (le_n _))) as (x',Hx').
+assert (Hfx : 0 = f x).
+apply le_n_O_eq.
+apply Hfbound.
+assert (Hfx' : 0 = f x').
+apply le_n_O_eq.
+apply Hfbound.
+assert (x=x').
+apply Hfinj.
+rewrite <- Hfx.
+rewrite <- Hfx'.
+reflexivity.
+rewrite H in Hx.
+rewrite Hx' in Hx.
+apply (n_Sn _ Hx).
+Qed.
+
+(** For [dec_restrict], we use a lemma on the negation of equality
+that requires proof-irrelevance. It should be possible to avoid this
+lemma by generalizing over a first-order definition of [x<>y], say
+[neq] such that [{x=y}+{neq x y}] and [~(x=y /\ neq x y)]; for such
+[neq], unicity of proofs could be proven *)
+
+  Require Import Classical.
+  Lemma neq_dep_intro :
+   forall (A:Set) (z x y:A) (p:x<>z) (q:y<>z), x=y ->
+      exist (fun x => x <> z) x p = exist (fun x => x <> z) y q.
+  Proof.
+  intros A z x y p q Heq.
+   generalize q; clear q; rewrite <- Heq; intro q.
+   rewrite (proof_irrelevance _ p q); reflexivity.
+  Qed.
+
+Lemma dec_restrict :
+  forall (A:Set), 
+    (forall x y :A, {x=y}+{x<>y}) ->
+     forall z (x y :{a:A|a<>z}), {x=y}+{x<>y}.
+Proof.
+intros A Hdec z (x,Hx) (y,Hy).
+destruct (Hdec x y) as [Heq|Hneq].
+left; apply neq_dep_intro; assumption.
+right; intro Heq; injection Heq; exact Hneq.
+Qed.
+
+Lemma pred_inj : forall n m, 
+  0 <> n -> 0 <> m -> pred m = pred n -> m = n.
+Proof.
+destruct n.
+intros m H; destruct H; reflexivity.
+destruct m.
+intros _ H; destruct H; reflexivity.
+simpl; intros _ _ H.
+rewrite H.
+reflexivity.
+Qed.
+
+Lemma le_neq_lt : forall n m, n <= m -> n<>m -> n < m.
+Proof.
+intros n m Hle Hneq.
+destruct (le_lt_eq_dec n m Hle).
+assumption.
+contradiction.
+Qed.
+
+Lemma inj_restrict :
+  forall (A:Set) (f:A->nat) x y z,
+    (forall x y : A, f x = f y -> x = y)
+    -> x <> z -> f y < f z -> f z <= f x
+    -> pred (f x) = f y
+    -> False.
+
+(* Search error sans le type de f !! *)
+Proof.
+intros A f x y z Hfinj Hneqx Hfy Hfx Heq.
+assert (f z <> f x).
+  apply sym_not_eq.
+  intro Heqf.
+  apply Hneqx.
+  apply Hfinj.
+  assumption.
+assert (f x = S (f y)).
+  assert (0 < f x).
+    apply le_lt_trans with (f z).
+    apply le_O_n.
+    apply le_neq_lt; assumption.
+  apply pred_inj.
+  apply O_S.
+  apply lt_O_neq; assumption.
+  exact Heq.
+assert (f z <= f y).
+destruct (le_lt_or_eq _ _ Hfx).
+  apply lt_n_Sm_le.
+  rewrite <- H0.
+  assumption.
+  contradiction Hneqx.
+  symmetry.
+  apply Hfinj.
+  assumption.
+contradiction (lt_not_le (f y) (f z)).
+Qed.
+
+Theorem card_inj : forall m n (A:Set), 
+  (forall x y :A, {x=y}+{x<>y}) ->
+  card A m -> card A n -> m = n. 
+Proof.
+induction m; destruct n; 
+intros A Hdec
+ (f,(Hfbound,(Hfinj,Hfsurj))) 
+ (g,(Hgbound,(Hginj,Hgsurj))).
+(* 0/0 *)
+reflexivity.
+(* 0/Sm *)
+destruct (card_inj_aux _ _ _ _ Hfbound Hfinj Hgsurj).
+(* Sn/0 *)
+destruct (card_inj_aux _ _ _ _ Hgbound Hginj Hfsurj).
+(* Sn/Sm *)
+destruct (Hgsurj (S n) (le_n _)) as (xSn,HSnx).
+rewrite IHm with (n:=n) (A := {x:A|x<>xSn}).
+reflexivity.
+(* decidability of eq on {x:A|x<>xSm} *)
+apply dec_restrict.
+assumption.
+(* cardinality of {x:A|x<>xSn} is m *)
+pose (f' := fun x' : {x:A|x<>xSn} =>
+    let (x,Hneq) := x' in 
+    if le_lt_dec (f xSn) (f x)
+    then pred (f x)
+    else f x).
+exists f'.
+split.
+(* f' is bounded *)
+unfold f'.
+intros (x,_).
+destruct (le_lt_dec (f xSn) (f x)) as [Hle|Hge].
+change m with (pred (S m)).
+apply le_pred.
+apply Hfbound.
+apply le_S_n.
+apply le_trans with (f xSn).
+exact Hge.
+apply Hfbound.
+split.
+(* f' is injective *)
+unfold f'.
+intros (x,Hneqx) (y,Hneqy) Heqf'.
+destruct (le_lt_dec (f xSn) (f x)) as [Hlefx|Hgefx];
+destruct (le_lt_dec (f xSn) (f y)) as [Hlefy|Hgefy].
+(* f xSn <= f x et f xSn <= f y *)
+assert (Heq : x = y).
+  apply Hfinj.
+  assert (f xSn <> f y).
+    apply sym_not_eq.
+    intro Heqf.
+    apply Hneqy.
+    apply Hfinj.
+    assumption.
+  assert (0 < f y).
+    apply le_lt_trans with (f xSn).
+    apply le_O_n.
+    apply le_neq_lt; assumption.
+  assert (f xSn <> f x).
+    apply sym_not_eq.
+    intro Heqf.
+    apply Hneqx.
+    apply Hfinj.
+    assumption.
+  assert (0 < f x).
+    apply le_lt_trans with (f xSn).
+    apply le_O_n.
+    apply le_neq_lt; assumption.
+  apply pred_inj.
+  apply lt_O_neq; assumption.
+  apply lt_O_neq; assumption.
+  assumption.
+apply neq_dep_intro; assumption.
+(* f y < f xSn <= f x *)
+destruct (inj_restrict A f x y xSn); assumption.
+(* f x < f xSn <= f y *)
+symmetry in Heqf'.
+destruct (inj_restrict A f y x xSn); assumption.
+(* f x < f xSn et f y < f xSn *)
+assert (Heq : x=y).
+  apply Hfinj; assumption.
+apply neq_dep_intro; assumption.
+(* f' is surjective *)
+intros p Hlep.
+destruct (le_lt_dec (f xSn) p) as [Hle|Hlt].
+(* case f xSn <= p *)
+destruct (Hfsurj (S p) (le_n_S _ _ Hlep)) as (x,Hx).
+assert (Hneq : x <> xSn).
+  intro Heqx.
+  rewrite Heqx in Hx.
+  rewrite Hx in Hle.
+  apply le_Sn_n with p; assumption.
+exists (exist (fun a => a<>xSn) x Hneq).
+unfold f'.
+destruct (le_lt_dec (f xSn) (f x)) as [Hle'|Hlt'].
+rewrite Hx; reflexivity.
+rewrite Hx in Hlt'.
+contradiction (le_not_lt (f xSn) p).
+apply lt_trans with (S p).
+apply lt_n_Sn.
+assumption.
+(* case p < f xSn *)
+destruct (Hfsurj p (le_S _ _ Hlep)) as (x,Hx).
+assert (Hneq : x <> xSn).
+  intro Heqx.
+  rewrite Heqx in Hx.
+  rewrite Hx in Hlt.
+  apply (lt_irrefl p).
+  assumption.
+exists (exist (fun a => a<>xSn) x Hneq).
+unfold f'.
+destruct (le_lt_dec (f xSn) (f x)) as [Hle'|Hlt'].
+  rewrite Hx in Hle'.
+  contradiction (lt_irrefl p).
+  apply lt_le_trans with (f xSn); assumption.
+  assumption.
+(* cardinality of {x:A|x<>xSn} is n *)
+pose (g' := fun x' : {x:A|x<>xSn} =>
+   let (x,Hneq) := x' in 
+   if Hdec x xSn then 0 else g x).
+exists g'.
+split.
+(* g is bounded *)
+unfold g'.
+intros (x,_).
+destruct (Hdec x xSn) as [_|Hneq].
+apply le_O_n.
+assert (Hle_gx:=Hgbound x).
+destruct (le_lt_or_eq _ _ Hle_gx).
+apply lt_n_Sm_le.
+assumption.
+contradiction Hneq.
+apply Hginj.
+rewrite HSnx.
+assumption.
+split.
+(* g is injective *)
+unfold g'.
+intros (x,Hneqx) (y,Hneqy) Heqg'.
+destruct (Hdec x xSn) as [Heqx|_].
+contradiction Hneqx.
+destruct (Hdec y xSn) as [Heqy|_].
+contradiction Hneqy.
+assert (Heq : x=y).
+  apply Hginj; assumption.
+apply neq_dep_intro; assumption.
+(* g is surjective *)
+intros p Hlep.
+destruct (Hgsurj p (le_S _ _ Hlep)) as (x,Hx).
+assert (Hneq : x<>xSn).
+  intro Heq.
+  rewrite Heq in Hx.
+  rewrite Hx in HSnx.
+  rewrite HSnx in Hlep.
+  contradiction (le_Sn_n _ Hlep).
+exists (exist (fun a => a<>xSn) x Hneq).
+simpl.
+destruct (Hdec x xSn) as [Heqx|_].
+contradiction Hneq.
+assumption.
+Qed.
+
+(** Conclusion *)
+
+Theorem interval_discr :
+  forall n m, {p:nat|p<=n} = {p:nat|p<=m} -> n=m.
+Proof.
+intros n m Heq.
+apply card_inj with (A := {p:nat|p<=n}).
+apply interval_dec.
+apply card_interval.
+rewrite Heq.
+apply card_interval.
+Qed.