MAJ

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

1 files changed, 217 insertions, 179 deletions

diff --git a/doc/faq.tex b/doc/faq.tex
index 93c479d29..be2fa0ea4 100644
--- a/doc/faq.tex
+++ b/doc/faq.tex
@@ -1,12 +1,20 @@
 \documentclass{article}
-
+\def\jobname{faq.v}
 \usepackage{hevea}
 \usepackage{url}
 
+\input{./macros.tex}
+
 \newcommand{\coqtt}[1]{{\tt #1}}
 \newcommand{\coqimp}{{$->$}}
 \newcommand{\coqequiv}{{$<->$}}
 
+\newcommand{\question}[1]{
+  \subsection*{\aname{no:number}{Question:~\sf{#1}}}
+  \addcontentsline{toc}{subsection}{\ahrefloc{no:number}{#1}}}
+%{\subsubsection{Question:~\sf{#1}}}}
+\newcommand{\answer}{{\bf Answer:~}}
+
 \begin{document}
 \urldef{\refman}{\url}{http://coq.inria.fr/doc/main.html}
 
@@ -14,135 +22,176 @@
 \begin{Large}
 Frequently Asked Questions
 \end{Large}
+
 \medskip
-Coq version 7
+{\Coq} version 7
 \end{center}
 
+\tableofcontents
+
 \section{General}
 
-\paragraph{Question}: What is Coq?
+\question{What is {\Coq}?}
 
-\paragraph{Answer}: Coq is a proof assistant with two main
+\answer {\Coq} is a proof assistant with two main
 application fields: proving program correctness and formalizing mathematical
-theories. Coq offers also automatic extraction of zero-defect programs
+theories. {\Coq} offers also automatic extraction of zero-defect programs
 from a proof of their specification.
 
-\paragraph{Question}: What are the main applications done in Coq?
+\question{What are the main applications done in {\Coq}?}
 
-\paragraph{Answer}: ??
+\answer Consequent developments include Java certification, safety of
+cryptographic protocols, medical robotics, constructive and classical
+analysis, algebraic topology, ...
 
-\paragraph{Question}: What is the logic of Coq?
+\question{What is the logic of {\Coq}?}
 
-\paragraph{Answer}: Coq is based on an axiom-free type theory called
-the Calculus of Inductive Constructions (see Coquand \cite{Coquand--}
-and Coquand--Paulin-Mohring \cite{CoqMoh}). It includes higher-order
-functions and predicates, inductive and co-inductive datatypes,
-inductively and co-inductively defined propositions and a stratified
-hierarchy of sets.
+\answer {\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.
 
-\paragraph{Question}: Is Coq logic constructive?
+\question{Is {\Coq} logic constructive?}
 
-\paragraph{Answer}: Coq theory is constructive, but classical
+\answer {\Coq} theory is constructive, but classical
 reasoning on proposition can be loaded as an external module.
 
-\paragraph{Question}: Is Coq about proofs or provability?
+\question{Is {\Coq} about proofs or provability?}
 
-\paragraph{Answer}: Coq is definitely about proofs. A statement
+\answer {\Coq} is definitely about proofs. A statement
 cannot be accepted without a proof expressed in the Calculus of
 Inductive Constructions. The correctness of a proof relies on a
-relatively small proof-checker at the kernel of Coq (8000 lines of ML
-code). Even Coq decision procedures are producing proofs which are
+relatively small proof-checker at the kernel of {\Coq} (8000 lines of ML
+code). Even {\Coq} decision procedures are producing proofs which are
 double-checked by the kernel.
 
-\paragraph{Question}: Can I define non-terminating program in Coq?
+\question{Can I define non-terminating programs in {\Coq}?}
 
-\paragraph{Answer}: No, all programs in Coq are terminating. To
-reason on non-terminating programs, you must turn your program into a
-terminating one by giving a bound on ``time'' as an extra parameter.
+\answer No, all programs in {\Coq} are terminating. To reason on
+non-terminating programs, you must turn your program into a
+terminating one by explicitly giving a bound on the number of
+iterations of the program.
 
-\paragraph{Question}: Is Coq a theorem prover?
+\question{Is {\Coq} a theorem prover?}
 
-\paragraph{Answer}: Coq comes with a few decision procedures (on
-propositional calculus, Presburger arithmetic, ring simplification,
-resolution based on first-order matching, ...) but the main style for
-proving theorems is by using LCF-style tactics.
+\answer {\Coq} comes with a few decision procedures (on propositional
+calculus, Presburger arithmetic, ring and field simplification,
+resolution, ...) but the main style for proving theorems is by using
+LCF-style tactics.
 
-\paragraph{Question}: How is equational reasoning working in Coq?
+\question{How is equational reasoning working in {\Coq}?}
 
-\paragraph{Answer}: Coq is reasoning modulo sequential evaluation of
-(not necessarily closed) programs (it is decidable because Coq
+\answer {\Coq} is reasoning modulo sequential evaluation of
+(not necessarily closed) programs (it is decidable because {\Coq}
 programs are terminating). This equality is called {\em conversion}.
 Besides conversion, equations are to be treated by hand or using
 specialized tactics (e.g. simplifications on fields).
 
 \section{Equality}
 
-\subsection{Equality on Terms}
+%\subsection{Equality on Terms}
 
-\paragraph{Question}: How can I prove that 2 terms in an inductive sets are equal? Or different?
+\question{How can I prove that 2 terms in an inductive sets are equal? Or different?}
 
-\paragraph{Answer}: Cf "Decide Equality" and "Discriminate" in the Reference Manual.
+\answer Cf "Decide Equality" and "Discriminate" in the Reference Manual.
 
-\paragraph{Question}: Why is the proof of \coqtt{0+n=n} on natural numbers
-trivial but the proof of \coqtt{n+0=n} is not?
+\question{Why is the proof of \coqtt{0+n=n} on natural numbers
+trivial but the proof of \coqtt{n+0=n} is not?}
 
-\paragraph{Answer}: Since \coqtt{+} (\coqtt{plus}) on natural numbers is defined by analysis on its first argument
+\answer Since \coqtt{+} (\coqtt{plus}) on natural numbers is defined by analysis on its first argument
 
 \begin{coq_example}
 Print plus.
 \end{coq_example}
 
-the expression \coqtt{0+n} evaluates to \coqtt{n}. As Coq reasons
+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{+}.
 
-\paragraph{Question}: I have two proofs of the same proposition. Can I prove they are equal?
+\question{I have two proofs of the same proposition. Can I prove they are equal?}
+\label{proof-irrelevance}
+
+\answer In the base {\Coq} system, the answer is no. However, if
+classical logic is set, the answer is yes for propositions in {\Prop}.
+
+More precisely, the equality of all proofs of a given proposition is called
+{\em proof-irrelevance}. Proof-irrelevance (in {\Prop}) can be assumed
+  without leading to contradiction in {\Coq}.
+
+  That classical logic (what can be assumed in {\Coq} by requiring the file
+  \verb=Classical.v=) implies proof-irrelevance is shown in files
+  \verb=ProofIrrelevance.v= and \verb=Berardi.v=.
+
+  Alternatively, propositional extensionality (i.e.  \coqtt{(A
+  \coqequiv B) \coqimp A=B}, defined in \verb=ClassicalFacts.v= ),
+  also implies proof-irrelevance.
+
+  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?}
 
-\paragraph{Answer}: Let's consider two cases.
+\answer 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.
 
-  1) These are two proofs of the equality, say of $x$ and $y$. We could
-  think these proofs are equal since equality is inductively defined
-  and the only possible proof of an equality is \verb=refl_equal=:
+\question{Can I prove that the second components of equal dependent
+pairs are equal?}
+
+\answer The answer is the same as for proofs of equality
+statements. It is yes if equality on the domain of the first component
+is decidable, no in the general case. More precisely it is a
+consequence of Streicher's axiom $K$.
+
+\question{What is Streicher's axiom $K$}
+\label{Streicher}
+
+\answer Streicher's axiom $K$ \cite{HofStr98} states that the only proof of a reflexivity statement is a reflexivity proof:
 
 \begin{coq_example*}
-Theorem only_one_proof_of_an_equality : (x,y:A)(p1,p2:(x=y))p1=p2.
+Axiom K: (A:Set)(x:A)(p:x=x)p==(refl_equal ? x).
 \end{coq_example*}
 
-  If equality on A is decidable, which is the case for most inductive
-  sets: nat, list, ... and for some inductive predicates: le, lt, ,
-  then it is provable. But this is not provable in the general
-  case. Effectively, it is known from Streicher [1995] that the
-  statement is independent of Coq, that is there are models of Coq
-  (actually of the Calculus of Constructions without inductive types)
-  which invalidates it.
+In the general case, axiom $K$ is an independent statement of the
+Calculus of Inductive Constructions.
+However, it is true on decidable domains. It is also
+trivially a consequence of proof-irrelevance (see
+\ref{proof-irrelevance}) hence of classical logic.
 
-  2) More generally, if B is an arbitrary proposition and b1, b2 are
-  two proofs of B, it is not provable that b1=b2.
+Axiom $K$ is equivalent to {\em Uniqueness of Identity Proofs} which
+states that
 
-  More precisely, the fact this is always provable is known as
-  proof-irrelevance. Proof-irrelevance (in Prop) can be assumed
-  without leading to contradiction in Coq. Especially,
-  proof-irrelevance limited to the propositional world does not break
-  the computational interpretation of the Set level.
+\begin{coq_example*}
+Axiom UIP: (A:Set)(x,y:A)(p1,p2:x=y)p1==p2.
+\end{coq_example*}
 
-  Alternatively, assuming classical logic (what can be done in Coq
-  by requiring the file \verb=Classical.v=) also implies
-  proof-irrelevance (as shown in file \verb=Berardi.v=)
+Axiom $K$ is also equivalent to the following statements.
 
-  Alternatively again, assuming propositional extensionality (that is
-  \coqtt{(A \coqequiv B) \coqimp A=B}), also implies proof-irrelevance.
+\begin{coq_example*}
+Axiom eq_rec_eq : (a:A)(P:A->Set)(p:(P p))(h:a=a) x=(eq_rec A a P p a h).
+Inductive eq_dep [p:U;x:(P p)] : (q:U)(P q)->Prop :=
+   eq_dep_intro : (eq_dep p x p x).
+Axiom eq_dep_eq : (a:A)(P:A->Set)(p1,p2:(P a))(eq_dep a x a y)->x=y.
+\end{coq_example*}
+
+All of these statements can be found in file \verb=Eqdep.v=.
 
-\subsection{Equality on types}
+% \subsection{Equality on types}
 
-\paragraph{Question}: How to prove that 2 sets are differents?
+\question{How to prove that 2 sets are differents?}
 
-\paragraph{Answer}: 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 bool and nat are
-discriminable. As discrimination property we take the property to have
-no more than 2 elements.
+\answer 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.
@@ -156,20 +205,22 @@ Proof.
 Qed.
 \end{coq_example*}
 
-\paragraph{Question}: How to exploit equalities on sets
+\question{How to exploit equalities on sets}
 
-\paragraph{Answer}: To extract information from an equality on sets, you need to find a
+\answer To extract information from an equality on sets, you need to find a
 predicate satisfied by the elements of the sets. As an example we show
 the following theorem.
 
 \begin{coq_example*}
+Theorem le_le: (m,n:nat){x:nat | (le x m)} = {x:nat | (le x n)} -> m = n.
+
 Inductive discr_int_n [n:nat;X:Set] : Prop :=
   intro : (fst:X->nat)(snd:(x:X)(le (fst x) n))
             ((x,y:X)(exist ? [z](le z n) (fst x) (snd x))=
                 (exist ? [z](le z n) (fst y) (snd y))->x=y)
           -> (discr_int_n n X).
 
-Theorem le_le: (m,n:nat){x:nat | (le x m)} = {x:nat | (le x n)} -> m = n.
+Proof.
 Intros.
 Assert Hdiscr : (discr_int_n m {x:nat | (le x m)}).
 Split with (proj1_sig nat [x:?](le x m)) (proj2_sig nat [x:?](le x m)).
@@ -183,68 +234,56 @@ Assert H1:=(snd (exist nat [z](le z (S n)) (S n) (le_n (S n)))).
 
 \section{Axioms}
 
-\paragraph{Question}: Can I identify two functions that have the same behaviour?
-
-\paragraph{Answer}: This is known as extensionality of equality
-between functions.
-
-Extensionality of functions is an axiom in, say set theory, but from a
-programming point of view, extensionality cannot be {\em a priori}
-accepted since it would identify, say programs as mergesort and
-quicksort.
+\question{Can I identify two functions that have the same behaviour (extensionality)?}
 
-However, from a logical point of view, equality can be made
-extensional without breaking the consistency (see [??]). This is
-achieved by adding the following axiom to our theory:
+\answer Extensionality of functions is an axiom in, say set theory,
+but from a programming point of view, extensionality cannot be {\em a
+priori} accepted since it would identify, say programs 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*}
+%\begin{coq_example*}
+%  Axiom extensionality : (A,B:Set)(f,g:(A->B))(x:A)(f x)=(g x)->f=g.
+%\end{coq_example*}
 
-Rather than adding an axiom, a better approach could be to define
-its one extensional equality on $A \rightarrow B$:
+To deal with extensionality, the recommended approach is to define his
+own extensional equality on $A \rightarrow B$:
 
 \begin{coq_example*}
   Definition ext_eq [f,g:A->B] := (x:A)(f x)=(g x).
 \end{coq_example*}
 
-and to reason on $A \rightarrow B$ as a setoid (see the Chapter on Setoids in the
-Reference Manual).
-
+and to reason on $A \rightarrow B$ as a setoid (see the Chapter on
+Setoids in the Reference Manual).
 
-\paragraph{Question}: Can I identify the different proofs of a proposition?
 
-\paragraph{Answer}: Yes, this is known as proof-irrelevance and it is consistent with
-the core theory of Coq. See also section "Equality on terms".
+\question{Is {\Type} impredicative (that is, letting
+\coqtt{T:=(X:Type)X->X}, can I apply an expression \coqtt{t} of type \coqtt{T} to \coqtt{T} itself)?}
 
-
-\paragraph{Question}: Is \coqtt{Type} impredicative (that is, letting
-\coqtt{T:=(X:Type)X->X}, can I apply an expression \coqtt{t} of type \coqtt{T} to \coqtt{T} itself) ?
-
-\paragraph{Answer}: No, Type is stratified. This is hidden for the
-user, but Coq internally maintains a set of constraints ensuring
+\answer 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 Girard's systems U- and U could be
-encoded in Coq and it is known from Girard, Coquand, Hurkens and
+  If {\Type} were impredicative then Girard's systems U- and U could be
+encoded in {\Coq} and it is known from Girard, Coquand, Hurkens and
 Miquel that systems U- and U are inconsistent [cf Girard 1972, Coquand
 1991, Hurkens 1993, Miquel 2001].
 
   For instance, when the user see {\tt (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 {\coqtt
+occurrence of {\Type} is implicitly bound to a different level, say
+$\alpha$ and $\beta$ and the actual statement is {\tt
 (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: {\coqtt [x:=Type][y:(X;Type)X \coqimp X](z x x)}.
+inconsistency} appears. Example: {\tt [x:=Type][y:(X;Type)X \coqimp X](z x x)}.
 
 \section{Inductive types}
 
-\paragraph{Question}: What is a "large inductive definition"?
+\question{What is a "large inductive definition"?}
 
-\paragraph{Answer}: An inductive definition is called large if its constructors embed
-sets or propositions. As an example, here is a large inductive type:
+\answer 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] : Set
@@ -254,13 +293,11 @@ sets or propositions. As an example, here is a large inductive type:
    Large inductive definition have restricted elimination scheme to
 prevent inconsistencies. Especially, projecting the set or the
 proposition content of a large inductive definition is forbidden. If
-it were allowed, we could be able to construct the set of all sets
-equipped with a well-founded relation and show that this sets is
-itself equipped with a well-founded relation, leading to a
-contradiction (this is Burali-Forti paradox).
-
+it were allowed, we could be able to encode
+e.g. Burali-Forti paradox \cite{Gir70,Coq85}.
 
-\paragraph{Question}: Why Injection does not work on impredicative types? E.g. in this case:
+\question{Why Injection does not work on impredicative types?}
+ E.g. in this case:
 
 \begin{coq_example*}
   Inductive I : Set := intro : (k:Set)k -> I.
@@ -268,7 +305,7 @@ contradiction (this is Burali-Forti paradox).
   Intros x y H; Injection H.
 \end{coq_example*}
 
-\paragraph{Answer}: Injectivity of constructors is restricted to predicative types. If
+\answer 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
@@ -277,45 +314,29 @@ encode known paradoxes (such as type I above).
 
 \section{Elimination, Case Analysis and Induction}
 
-\subsection{Parametric elimination}
+%\subsection{Parametric elimination}
 
-\paragraph{Question}: What is parametric elimination?
+\question{What is parametric elimination?}
 
-\paragraph{Answer}: Parametric elimination is a 
+\answer Parametric elimination is a 
 generalisation of the substitutivity of equality. Only inductive types
 with non-constant parameters are concerned with this kind of dependent
 elimination. Typical examples of inductive types enjoying parametric
-elimination in Coq standard library are the equality predicate
+elimination in {\Coq} standard library are the equality predicate
 \verb=eq= and the less than predicate on natural numbers \verb=le=.
 
-\begin{coq_example*}
+\begin{coq_example}
 Print eq.
 Print le.
-\end{coq_example*}
-
-\begin{coq_example*}
-Inductive le [n,m] : nat]  : nat->Prop :=
-      le_n : n=m->(le n m) | le_S : (p:nat)(le n p)->(le n (S p))
-\end{coq_example*}
-
-Assuming equality defined, all other kind of parametric elimination
-can be expressed using equality. For instance, parametric
-elimination of \verb=le= can be restated as:
-
-\begin{verbatim}
-le_ind: (n:nat; n0:nat; P:(nat->Prop))
-        (n=n0->(P n0))
-        ->((m:nat)(le n m)->(P m)->n0=(S m)->(P n0))
-        ->(le n n0)->(P n0)
-\end{verbatim}
+\end{coq_example}
 
-\subsection{Dependent elimination}
+%\subsection{Dependent elimination}
 
-\paragraph{Question}: What means dependent elimination?
+\question{What means dependent elimination?}
 
-\paragraph{Answer}: Dependent elimination is a generalisation of the
+\answer Dependent elimination is a generalisation of the
 standard Peano's induction principle on natural numbers.  This
-elimination asserts that to prove a property P on say the set nat of
+elimination asserts that to prove a property P on say the set {\tt nat} of
 natural numbers, it is enough to prove the property on O and to prove
 it on successor numbers. Combined with fixpoints, this directly
 provides with usual Peano's induction scheme.
@@ -325,14 +346,15 @@ object whose type does not depend on the eliminated object. An example
 of non dependent elimination is recursion, or the simpler form of
 {\coqtt if $\ldots$ then $\ldots$ else}.
 
-The relevant tactics to deal with this kind of elimination are Elim,
-Induction, Destruct and Case.
+The relevant tactics to deal with this kind of elimination are {\tt
+Elim}, {\tt Induction}, {\tt Destruct} and {\tt Case}, {\tt
+NewInduction} and {\tt NewDestruct}.
 
 
-% \paragraph{Question}: Does the elimination in Prop follows a
-%   different rule than the elimination in Set?
+% \question{Does the elimination in Prop follows a
+%   different rule than the elimination in Set?}
 
-% \paragraph{Answer}: There are two kinds of dependent case analysis. The result type of a
+% \answer There are two kinds of dependent case analysis. The result type of a
 % case analysis may depend on the matched object (this is what is
 % usually intended by dependent) but may also depend on the non-constant
 % arguments of the type of the matched object without being dependent of
@@ -355,49 +377,62 @@ Induction, Destruct and Case.
 % argument is precisely what provides with the substitutivity schema of
 % equality.
 
-\paragraph{Question}: Why is dependent elimination in Prop not
-available by default.
+\question{Why is dependent elimination in Prop not
+available by default?}
 
-\paragraph{Answer}: 
+\answer 
 This is just because most of the time it is not needed. To derive a
-dependent elimination principle in Prop, use the command Scheme and
-apply the elimination scheme using the \verb=with= option of
+dependent elimination principle in Prop, use the command {\tt Scheme} and
+apply the elimination scheme using the \verb=using= option of
 \verb=Elim=.
 
 
 
-\subsection{Induction}
+%\subsection{Induction}
+
+\question{How to perform double induction?}
 
-\paragraph{Question}: How to perform double induction?
+\answer To reason by induction on pairs, just reason by induction on the first component then by case analysis on the second component. Here is an example:
 
-\paragraph{Answer}: To reason by induction on pairs, just reason by induction on the first component the by case analysis on the second component. Here is an example:
+\begin{coq_eval}
+Require Arith.
+\end{coq_eval}
 
 \begin{coq_example}
+Infix "<" lt (at level 5, no associativity).
+Infix "<=" le (at level 5, no associativity).
 Lemma le_or_lt : (n,n0:nat) n0<n \/ n<=n0.
 NewInduction n; NewDestruct n0; Auto with arith.
 NewDestruct (IHn n0); Auto with arith.
 \end{coq_example}
 
-\paragraph{Question}: How to define a function by recursion on 2 arguments?
+\question{How to define a function by double recursion?}
 
-\paragraph{Answer}: The same trick applies, except that you need to write by hand the nesting of two fixpoint combinators. Here is an example:
+\answer The same trick applies, you can even use the patterm-matching
+compilation algorithm to do the work for you. Here is an example:
 
 \begin{coq_example}
-TODO
+Fixpoint minus [n:nat] : nat -> nat := 
+  [m:nat]Cases n m of
+            O    _     =>  O
+         | (S k) O     => (S k)
+         | (S k) (S l) => (minus k l)
+        end. 
+Print minus.
 \end{coq_example}
 
 
 \section{Coinductive types}
 
-\paragraph{Question}: I have a cofixpoint t:=F(t) and I want to prove t=F(t). What is
-the simplest way?
+\question{I have a cofixpoint t:=F(t) and I want to prove t=F(t). What is
+the simplest way?}
 
-\paragraph{Answer}: Just case-expand F(t) then complete by a trivial case analysis.
+\answer Just case-expand F(t) then complete by a trivial case analysis.
 Here is what it gives on e.g. the type of streams on naturals
 
 \begin{coq_example}
   Set Implicit Arguments.
-  CoInductive Stream [A : Set]  : Set := Cons : A->(Stream A)->(Stream A)
+  CoInductive Stream [A : Set]  : Set := Cons : A->(Stream A)->(Stream A).
   CoFixpoint nats : nat -> (Stream nat) := [n](Cons n (nats (S n))).
 
   Lemma Stream_unfold : (n:nat)(nats n)= (Cons n (nats (S n))).
@@ -409,18 +444,19 @@ Here is what it gives on e.g. the type of streams on naturals
 
 \section{Miscellaneous}
 
-\paragraph{Question}: I copy-paste a term and Coq says it is not convertible
-to the original term. Sometimes it even say the copied term is not
-well-typed.
+\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.}
 
-\paragraph{Answer}: This is probably due to invisible implicit information (implicit
+\answer This is probably due to invisible implicit information (implicit
 arguments, coercions and Cases annotations) in the printed term, which
 is not re-synthetized from the copied-pasted term in the same way as
 it is in the original term.
 
-  Consider for instance (eqT Type True True). This term is printed as
-True==True and re-parsed as (eqT Prop True True). Both are not
-convertible and, e.g. Pattern and LetTac are beaten by that.
+  Consider for instance {\tt (eqT Type True True)}. This term is
+printed as {\tt True==True} and re-parsed as {\tt (eqT 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.
  
@@ -429,8 +465,8 @@ rare cases, the criterion to hide coercions is a bit too loosy, which
 may result in a typing error message if the parser is not able to find
 again the missing coercion.
 
-\paragraph{Question}: I have a problem of dependent elimination on
-proofs, how to solve it?
+\question{I have a problem of dependent elimination on
+proofs, how to solve it?}
 
 \begin{coq_example*}
 Inductive Def1 : Set
@@ -447,7 +483,7 @@ Lemma eq_comb
      (c3 d1 d2)=(c3 d1' d2').
 \end{coq_example*}
 
-\paragraph{Answer}: You need to derive the dependent elimination
+\answer You need to derive the dependent elimination
 scheme for DefProp by hand using {\coqtt Scheme}.
 
 \begin{coq_example*}
@@ -464,7 +500,7 @@ Reflexivity.
 Qed.
 \end{coq_example*}
 
-\paragraph{Question}: And what if I want to prove the following?
+\question{And what if I want to prove the following?}
 
 \begin{coq_example*}
 Inductive natProp : nat -> Prop
@@ -481,7 +517,7 @@ Lemma eq_pack
      (pack n np)=(pack n' np').
 \end{coq_example*}
 
-\paragraph{Answer}:
+\answer
 
 \begin{coq_example*}
 Scheme natProp_elim := Induction for natProp Sort Prop.
@@ -510,11 +546,13 @@ Auto.
 Qed.
 \end{coq_example*}
 
-\paragraph{Question}: Why does Coq tell me that \texttt{\{x:A|(P x)\}} is not convertible with \texttt{(sig A P)}
+\question{Why does {\Coq} tell me that \texttt{\{x:A|(P x)\}} is not convertible with \texttt{(sig A P)}?}
 
-\paragraph{Answer}:
-
-This is because \texttt{\{x:A|(P x)\}} is a notation for \texttt{(sig A [x:A](p x))}. Since Coq does not reason up to $\eta$-conversion, this is different from
+\answer
+This is because \texttt{\{x:A|(P x)\}} is a notation for \texttt{(sig A [x:A](p x))}. Since {\Coq} does not reason up to $\eta$-conversion, this is different from
 \texttt{(sig A P)}.
 
+\bibliographystyle{plain}
+\bibliography{biblio}
+
 \end{document}