Merge PR #842: Update the Tutorial.

1 files changed, 217 insertions, 228 deletions

diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex
index 30b6304c1..8337b1c48 100644
--- a/doc/tutorial/Tutorial.tex
+++ b/doc/tutorial/Tutorial.tex
@@ -23,7 +23,7 @@ of Inductive Constructions. It allows the interactive construction of
 formal proofs, and also the manipulation of functional programs 
 consistently with their specifications. It runs as a computer program
 on many architectures.
-%, and mainly on Unix machines. 
+
 It is available with a variety of user interfaces. The present
 document does not attempt to present a comprehensive view of all the
 possibilities of \Coq, but rather to present in the most elementary
@@ -33,63 +33,34 @@ proof tools.  For more advanced information, the reader could refer to
 the \Coq{} Reference Manual or the \textit{Coq'Art}, a book by Y.
 Bertot and P. Castéran on practical uses of the \Coq{} system.
 
-Coq can be used from a standard teletype-like shell window but
-preferably through the graphical user interface
-CoqIde\footnote{Alternative graphical interfaces exist: Proof General
-and Pcoq.}.
-
 Instructions on installation procedures, as well as more comprehensive
 documentation, may be found in the standard distribution of \Coq,
-which may be obtained from \Coq{} web site \url{https://coq.inria.fr/}.
-
-In the following, we assume that \Coq{} is called from a standard
-teletype-like shell window. All examples preceded by the prompting
-sequence \verb:Coq < : represent user input, terminated by a
-period. 
-
-The following lines usually show \Coq's answer as it appears on the
-users screen. When used from a graphical user interface such as
-CoqIde, the prompt is not displayed: user input is given in one window
+which may be obtained from \Coq{} web site
+\url{https://coq.inria.fr/}\footnote{You can report any bug you find
+while using \Coq{} at \url{https://coq.inria.fr/bugs}. Make sure to
+always provide a way to reproduce it and to specify the exact version
+you used. You can get this information by running \texttt{coqc -v}}.
+\Coq{} is distributed together with a graphical user interface called
+CoqIDE. Alternative interfaces exist such as
+Proof General\footnote{See \url{https://proofgeneral.github.io/}.}.
+
+In the following examples, lines preceded by the prompt \verb:Coq < :
+represent user input, terminated by a period.
+The following lines usually show \Coq's answer.
+When used from a graphical user interface such as
+CoqIDE, the prompt is not displayed: user input is given in one window
 and \Coq's answers are displayed in a different window.
 
-The sequence of such examples is a valid \Coq{}
-session, unless otherwise specified. This version of the tutorial has
-been prepared on a PC workstation running Linux.  The standard
-invocation of \Coq{} delivers a message such as:
-
-\begin{small}
-\begin{flushleft}
-\begin{verbatim}
-unix:~> coqtop
-Welcome to Coq 8.2 (January 2009)
-
-Coq < 
-\end{verbatim}
-\end{flushleft}
-\end{small}
-
-The first line gives a banner stating the precise version of \Coq{}
-used. You should always return this banner when you report an anomaly
-to our bug-tracking system
-\url{https://coq.inria.fr/bugs/}.
-
 \chapter{Basic Predicate Calculus}
 
 \section{An overview of the specification language Gallina}
 
 A formal development in Gallina consists in a sequence of {\sl declarations}
-and {\sl definitions}. You may also send \Coq{} {\sl commands} which are
-not really part of the formal development, but correspond to information
-requests, or service routine invocations. For instance, the command:
-\begin{verbatim}
-Coq < Quit.
-\end{verbatim}
-terminates the current session.
+and {\sl definitions}.
 
 \subsection{Declarations}
 
-A declaration associates a {\sl name} with 
-a {\sl specification}. 
+A declaration associates a {\sl name} with a {\sl specification}.
 A name corresponds roughly to an identifier in a programming
 language, i.e. to a string of letters, digits, and a few ASCII symbols like
 underscore (\verb"_") and prime (\verb"'"), starting with a letter. 
@@ -165,25 +136,25 @@ in the current context:
 Check gt.
 \end{coq_example}
 
-which tells us that \verb:gt: is a function expecting two arguments of
-type \verb:nat: in order to build a logical proposition.
+which tells us that \texttt{gt} is a function expecting two arguments of
+type \texttt{nat} in order to build a logical proposition.
 What happens here is similar to what we are used to in a functional
-programming language: we may compose the (specification) type \verb:nat:
-with the (abstract) type \verb:Prop: of logical propositions through the
+programming language: we may compose the (specification) type \texttt{nat}
+with the (abstract) type \texttt{Prop} of logical propositions through the
 arrow function constructor, in order to get a functional type
-\verb:nat->Prop::
+\texttt{nat -> Prop}:
 \begin{coq_example}
 Check (nat -> Prop).
 \end{coq_example}
-which may be composed one more times with \verb:nat: in order to obtain the
-type \verb:nat->nat->Prop: of binary relations over natural numbers.
-Actually the type \verb:nat->nat->Prop: is an abbreviation for 
-\verb:nat->(nat->Prop):. 
+which may be composed once more with \verb:nat: in order to obtain the
+type \texttt{nat -> nat -> Prop} of binary relations over natural numbers.
+Actually the type \texttt{nat -> nat -> Prop} is an abbreviation for 
+\texttt{nat -> (nat -> Prop)}.
 
 Functional notions may be composed in the usual way. An expression $f$
 of type $A\ra B$ may be applied to an expression $e$ of type $A$ in order
 to form the expression $(f~e)$ of type $B$. Here we get that
-the expression \verb:(gt n): is well-formed of type \verb:nat->Prop:,
+the expression \verb:(gt n): is well-formed of type \texttt{nat -> Prop},
 and thus that the expression \verb:(gt n O):, which abbreviates
 \verb:((gt n) O):, is a well-formed proposition.
 \begin{coq_example}
@@ -193,11 +164,12 @@ Check gt n O.
 \subsection{Definitions}
 
 The initial prelude contains a few arithmetic definitions:
-\verb:nat: is defined as a mathematical collection (type \verb:Set:), constants
-\verb:O:, \verb:S:, \verb:plus:, are defined as objects of types
-respectively \verb:nat:, \verb:nat->nat:, and \verb:nat->nat->nat:.
+\texttt{nat} is defined as a mathematical collection (type \texttt{Set}),
+constants \texttt{O}, \texttt{S}, \texttt{plus}, are defined as objects of
+types respectively \texttt{nat}, \texttt{nat -> nat}, and \texttt{nat ->
+nat -> nat}.
 You may introduce new definitions, which link a name to a well-typed value.
-For instance, we may introduce the constant \verb:one: as being defined
+For instance, we may introduce the constant \texttt{one} as being defined
 to be equal to the successor of zero:
 \begin{coq_example}
 Definition one := (S O).
@@ -217,17 +189,18 @@ argument \verb:m: of type \verb:nat: in order to build its result as
 \verb:(plus m m)::
 
 \begin{coq_example}
-Definition double (m:nat) := plus m m.
+Definition double (m : nat) := plus m m.
 \end{coq_example}
 This introduces the constant \texttt{double} defined as the
-expression \texttt{fun m:nat => plus m m}.
-The abstraction introduced by \texttt{fun} is explained as follows. The expression
-\verb+fun x:A => e+ is well formed of type \verb+A->B+ in a context
-whenever the expression \verb+e+ is well-formed of type \verb+B+ in 
-the given context to which we add the declaration that \verb+x+
-is of type \verb+A+. Here \verb+x+ is a bound, or dummy variable in
-the expression \verb+fun x:A => e+. For instance we could as well have
-defined \verb:double: as \verb+fun n:nat => (plus n n)+.
+expression \texttt{fun m : nat => plus m m}.
+The abstraction introduced by \texttt{fun} is explained as follows.
+The expression \texttt{fun x : A => e} is well formed of type
+\texttt{A -> B} in a context whenever the expression \texttt{e} is
+well-formed of type \texttt{B} in the given context to which we add the
+declaration that \texttt{x} is of type \texttt{A}. Here \texttt{x} is a
+bound, or dummy variable in the expression \texttt{fun x : A => e}.
+For instance we could as well have defined \texttt{double} as
+\texttt{fun n : nat => (plus n n)}.
 
 Bound (local) variables and free (global) variables may be mixed.
 For instance, we may define the function which adds the constant \verb:n:
@@ -243,19 +216,17 @@ Binding operations are well known for instance in logic, where they
 are called quantifiers.  Thus we may universally quantify a
 proposition such as $m>0$ in order to get a universal proposition
 $\forall m\cdot m>0$. Indeed this operator is available in \Coq, with
-the following syntax: \verb+forall m:nat, gt m O+. Similarly to the
+the following syntax: \texttt{forall m : nat, gt m O}. Similarly to the
 case of the functional abstraction binding, we are obliged to declare
 explicitly the type of the quantified variable. We check:
 \begin{coq_example}
-Check (forall m:nat, gt m 0).
-\end{coq_example}
-We may revert to the clean state of
-our initial session using the \Coq{} \verb:Reset: command:
-\begin{coq_example}
-Reset Initial.
+Check (forall m : nat, gt m 0).
 \end{coq_example}
+
 \begin{coq_eval}
+Reset Initial.
 Set Printing Width 60.
+Set Printing Compact Contexts.
 \end{coq_eval}
 
 \section{Introduction to the proof engine: Minimal Logic}
@@ -340,17 +311,12 @@ the current goal is solvable from the current local assumptions:
 assumption.
 \end{coq_example}
 
-The proof is now finished. We may either discard it, by using the
-command \verb:Abort: which returns to the standard \Coq{} toplevel loop
-without further ado, or else save it as a lemma in the current context,
-under name say \verb:trivial_lemma::
+The proof is now finished. We are now going to ask \Coq{}'s kernel
+to check and save the proof.
 \begin{coq_example}
-Save trivial_lemma.
+Qed.
 \end{coq_example}
 
-As a comment, the system shows the proof script listing all tactic
-commands used in the proof. 
-
 Let us redo the same proof with a few variations. First of all we may name
 the initial goal as a conjectured lemma:
 \begin{coq_example}
@@ -383,46 +349,30 @@ We may thus complete the proof of \verb:distr_impl: with one composite tactic:
 apply H; [ assumption | apply H0; assumption ].
 \end{coq_example}
 
-Let us now save lemma \verb:distr_impl::
-\begin{coq_example}
-Qed.
-\end{coq_example}
-
-Here \verb:Qed: needs no argument, since we gave the name \verb:distr_impl: 
-in advance.
+You should be aware however that relying on automatically generated names is
+not robust to slight updates to this proof script. Consequently, it is
+discouraged in finished proof scripts. As for the composition of tactics with
+\texttt{:} it may hinder the readability of the proof script and it is also
+harder to see what's going on when replaying the proof because composed
+tactics are evaluated in one go.
 
 Actually, such an easy combination of tactics \verb:intro:, \verb:apply:
 and \verb:assumption: may be found completely automatically by an automatic
 tactic, called \verb:auto:, without user guidance:
-\begin{coq_example}
-Lemma distr_imp : (A -> B -> C) -> (A -> B) -> A -> C.
-auto.
-\end{coq_example}
-
-This time, we do not save the proof, we just discard it with the \verb:Abort: 
-command:
 
-\begin{coq_example}
+\begin{coq_eval}
 Abort.
+\end{coq_eval}
+\begin{coq_example}
+Lemma distr_impl : (A -> B -> C) -> (A -> B) -> A -> C.
+auto.
 \end{coq_example}
 
-At any point during a proof, we may use \verb:Abort: to exit the proof mode
-and go back to Coq's main loop. We may also use \verb:Restart: to restart
-from scratch the proof of the same lemma. We may also use \verb:Undo: to
-backtrack one step, and more generally \verb:Undo n: to
-backtrack n steps.
-
-We end this section by showing a useful command, \verb:Inspect n.:,
-which inspects the global \Coq{} environment, showing the last \verb:n: declared
-notions: 
+Let us now save lemma \verb:distr_impl::
 \begin{coq_example}
-Inspect 3.
+Qed.
 \end{coq_example}
 
-The declarations, whether global parameters or axioms, are shown preceded by 
-\verb:***:; definitions and lemmas are stated with their specification, but
-their value (or proof-term) is omitted.
-
 \section{Propositional Calculus}
 
 \subsection{Conjunction}
@@ -438,7 +388,7 @@ connective. Let us show how to use these ideas for the propositional connectives
 
 \begin{coq_example}
 Lemma and_commutative : A /\ B -> B /\ A.
-intro.
+intro H.
 \end{coq_example}
 
 We make use of the conjunctive hypothesis \verb:H: with the \verb:elim: tactic,
@@ -453,8 +403,11 @@ conjunctive goal into the two subgoals:
 split.
 \end{coq_example}
 and the proof is now trivial. Indeed, the whole proof is obtainable as follows:
+\begin{coq_eval}
+Abort.
+\end{coq_eval}
 \begin{coq_example}
-Restart.
+Lemma and_commutative : A /\ B -> B /\ A.
 intro H; elim H; auto.
 Qed.
 \end{coq_example}
@@ -465,7 +418,7 @@ conjunction introduction operator \verb+conj+
 Check conj.
 \end{coq_example}
 
-Actually, the tactic \verb+Split+ is just an abbreviation for \verb+apply conj.+
+Actually, the tactic \verb+split+ is just an abbreviation for \verb+apply conj.+
 
 What we have just seen is that the \verb:auto: tactic is more powerful than
 just a simple application of local hypotheses; it tries to apply as well 
@@ -498,6 +451,17 @@ clear away unnecessary hypotheses which may clutter your screen.
 clear H.
 \end{coq_example}
 
+The tactic \verb:destruct: combines the effects of \verb:elim:, \verb:intros:,
+and \verb:clear::
+
+\begin{coq_eval}
+Abort.
+\end{coq_eval}
+\begin{coq_example}
+Lemma or_commutative : A \/ B -> B \/ A.
+intros H; destruct H.
+\end{coq_example}
+
 The disjunction connective has two introduction rules, since \verb:P\/Q:
 may be obtained from \verb:P: or from \verb:Q:; the two corresponding
 proof constructors are called respectively \verb:or_introl: and
@@ -528,8 +492,11 @@ such a simple tautology. The reason is that we want to keep
 
 A complete tactic for propositional
 tautologies is indeed available in \Coq{} as the \verb:tauto: tactic.
+\begin{coq_eval}
+Abort.
+\end{coq_eval}
 \begin{coq_example}
-Restart.
+Lemma or_commutative : A \/ B -> B \/ A.
 tauto.
 Qed.
 \end{coq_example}
@@ -541,8 +508,8 @@ currently defined in the context:
 Print or_commutative.
 \end{coq_example}
 
-It is not easy to understand the notation for proof terms without a few
-explanations. The \texttt{fun} prefix, such as \verb+fun H:A\/B =>+, 
+It is not easy to understand the notation for proof terms without some
+explanations. The \texttt{fun} prefix, such as \verb+fun H : A\/B =>+, 
 corresponds
 to \verb:intro H:, whereas a subterm such as 
 \verb:(or_intror: \verb:B H0):
@@ -572,15 +539,17 @@ Lemma Peirce : ((A -> B) -> A) -> A.
 try tauto.
 \end{coq_example}
 
-Note the use of the \verb:Try: tactical, which does nothing if its tactic
+Note the use of the \verb:try: tactical, which does nothing if its tactic
 argument fails.
 
 This may come as a surprise to someone familiar with classical reasoning. 
 Peirce's lemma is true in Boolean logic, i.e. it evaluates to \verb:true: for 
 every truth-assignment to \verb:A: and \verb:B:. Indeed the double negation
 of Peirce's law may be proved in \Coq{} using \verb:tauto::
-\begin{coq_example}
+\begin{coq_eval}
 Abort.
+\end{coq_eval}
+\begin{coq_example}
 Lemma NNPeirce : ~ ~ (((A -> B) -> A) -> A).
 tauto.
 Qed.
@@ -651,26 +620,20 @@ function and predicate symbols.
 \subsection{Sections and signatures}
 
 Usually one works in some domain of discourse, over which range the individual 
-variables and function symbols. In \Coq{} we speak in a language with a rich
-variety of types, so me may mix several domains of discourse, in our 
+variables and function symbols. In \Coq{}, we speak in a language with a rich
+variety of types, so we may mix several domains of discourse, in our 
 multi-sorted language. For the moment, we just do a few exercises, over a 
 domain of discourse \verb:D: axiomatised as a \verb:Set:, and we consider two 
 predicate symbols  \verb:P: and \verb:R: over \verb:D:, of arities 
-respectively 1 and 2. Such abstract entities may be entered in the context
-as global variables. But we must be careful about the pollution of our
-global environment by such declarations. For instance, we have already 
-polluted our \Coq{} session by declaring the variables
-\verb:n:, \verb:Pos_n:, \verb:A:, \verb:B:, and \verb:C:.
+1 and 2, respectively.
 
-\begin{coq_example}
-Reset Initial.
-\end{coq_example}
 \begin{coq_eval}
+Reset Initial.
 Set Printing Width 60.
+Set Printing Compact Contexts.
 \end{coq_eval}
 
-We shall now declare a new \verb:Section:, which will allow us to define
-notions local to a well-delimited scope. We start by assuming a domain of
+We start by assuming a domain of
 discourse \verb:D:, and a binary relation \verb:R:  over \verb:D:: 
 \begin{coq_example}
 Section Predicate_calculus.
@@ -686,18 +649,19 @@ a theory, but rather local hypotheses to a theorem, we open a specific
 section to this effect.
 \begin{coq_example}
 Section R_sym_trans.
-Hypothesis R_symmetric : forall x y:D, R x y -> R y x.
-Hypothesis R_transitive : forall x y z:D, R x y -> R y z -> R x z.
+Hypothesis R_symmetric : forall x y : D, R x y -> R y x.
+Hypothesis R_transitive :
+    forall x y z : D, R x y -> R y z -> R x z.
 \end{coq_example}
 
-Remark the syntax \verb+forall x:D,+ which stands for universal quantification
+Remark the syntax \verb+forall x : D,+ which stands for universal quantification
 $\forall x : D$.
 
 \subsection{Existential quantification}
 
 We now state our lemma, and enter proof mode.
 \begin{coq_example}
-Lemma refl_if : forall x:D, (exists y, R x y) -> R x x.
+Lemma refl_if : forall x : D, (exists y, R x y) -> R x x.
 \end{coq_example}
 
 Remark that the hypotheses which are local to the currently opened sections
@@ -711,13 +675,13 @@ predicate as argument:
 \begin{coq_example}
 Check ex.
 \end{coq_example}
-and the notation \verb+(exists x:D, P x)+ is just concrete syntax for 
-the expression \verb+(ex D (fun x:D => P x))+. 
+and the notation \verb+(exists x : D, P x)+ is just concrete syntax for 
+the expression \verb+(ex D (fun x : D => P x))+. 
 Existential quantification is handled in \Coq{} in a similar
-fashion to the connectives \verb:/\: and \verb:\/: : it is introduced by
+fashion to the connectives \verb:/\: and \verb:\/:: it is introduced by
 the proof combinator \verb:ex_intro:, which is invoked by the specific 
-tactic \verb:Exists:, and its elimination provides a witness \verb+a:D+ to
-\verb:P:, together with an assumption \verb+h:(P a)+ that indeed \verb+a+
+tactic \verb:exists:, and its elimination provides a witness \verb+a : D+ to
+\verb:P:, together with an assumption \verb+h : (P a)+ that indeed \verb+a+
 verifies \verb:P:. Let us see how this works on this simple example.
 \begin{coq_example}
 intros x x_Rlinked.
@@ -773,8 +737,8 @@ End R_sym_trans.
 All the local hypotheses have been
 discharged in the statement of \verb:refl_if:, which now becomes a general
 theorem in the first-order language declared in section 
-\verb:Predicate_calculus:. In this particular example, the use of section
-\verb:R_sym_trans: has not been really significant, since we could have
+\verb:Predicate_calculus:. In this particular example, section
+\verb:R_sym_trans: has not been really useful, since we could have
 instead stated theorem \verb:refl_if: in its general form, and done 
 basically the same proof, obtaining \verb:R_symmetric: and
 \verb:R_transitive: as local hypotheses by initial \verb:intros: rather
@@ -802,7 +766,7 @@ Lemma weird : (forall x:D, P x) ->  exists a, P a.
 \end{coq_example}
 
 First of all, notice the pair of parentheses around
-\verb+forall x:D, P x+ in
+\verb+forall x : D, P x+ in
 the statement of lemma \verb:weird:.
 If we had omitted them, \Coq's parser would have interpreted the
 statement as a truly trivial fact, since we would 
@@ -820,7 +784,7 @@ systematically inhabited, lemma \verb:weird: only holds in signatures
 which allow the explicit construction of an element in the domain of
 the predicate. 
 
-Let us conclude the proof, in order to show the use of the \verb:Exists:
+Let us conclude the proof, in order to show the use of the \verb:exists:
 tactic:
 \begin{coq_example}
 exists d; trivial.
@@ -836,8 +800,8 @@ We shall need classical reasoning. Instead of loading the \verb:Classical:
 module as we did above, we just state the law of excluded middle as a
 local hypothesis schema at this point:
 \begin{coq_example}
-Hypothesis EM : forall A:Prop, A \/ ~ A.
-Lemma drinker :  exists x:D, P x -> forall x:D, P x.
+Hypothesis EM : forall A : Prop, A \/ ~ A.
+Lemma drinker :  exists x : D, P x -> forall x : D, P x.
 \end{coq_example}
 The proof goes by cases on whether or not
 there is someone who does not drink. Such reasoning by cases proceeds
@@ -847,10 +811,11 @@ proper instance of \verb:EM::
 elim (EM (exists x, ~ P x)).
 \end{coq_example}
 
-We first look at the first case. Let Tom be the non-drinker:
+We first look at the first case. Let Tom be the non-drinker.
+The following combines at once the effect of \verb:intros: and
+\verb:destruct::
 \begin{coq_example}
-intro Non_drinker; elim Non_drinker;
-  intros Tom Tom_does_not_drink.
+intros (Tom, Tom_does_not_drink).
 \end{coq_example}
 
 We conclude in that case by considering Tom, since his drinking leads to
@@ -860,9 +825,10 @@ exists Tom; intro Tom_drinks.
 \end{coq_example}
 
 There are several ways in which we may eliminate a contradictory case;
-a simple one is to use the \verb:absurd: tactic as follows:
+in this case, we use \verb:contradiction: to let \Coq{} find out the
+two contradictory hypotheses:
 \begin{coq_example}
-absurd (P Tom); trivial.
+contradiction.
 \end{coq_example}
 
 We now proceed with the second case, in which actually any person will do;
@@ -904,9 +870,10 @@ Finally, the excluded middle hypothesis is discharged only in
 Note that the name \verb:d: has vanished as well from
 the statements of \verb:weird: and \verb:drinker:, 
 since \Coq's pretty-printer replaces
-systematically a quantification such as \verb+forall d:D, E+, where \verb:d:
-does not occur in \verb:E:, by the functional notation \verb:D->E:. 
-Similarly the name \verb:EM: does not appear in \verb:drinker:. 
+systematically a quantification such as \texttt{forall d : D, E},
+where \texttt{d} does not occur in \texttt{E},
+by the functional notation \texttt{D -> E}.
+Similarly the name \texttt{EM} does not appear in \texttt{drinker}.
 
 Actually, universal quantification, implication, 
 as well as function formation, are
@@ -935,12 +902,12 @@ intros.
 generalize H0.
 \end{coq_example}
 
-Sometimes it may be convenient to use a lemma, although we do not have
-a direct way to appeal to such an already proven fact. The tactic \verb:cut:
-permits to use the lemma at this point, keeping the corresponding proof
-obligation as a new subgoal:
+Sometimes it may be convenient to state an intermediate fact.
+The tactic \verb:assert: does this and introduces a new subgoal
+for this fact to be proved first. The tactic \verb:enough: does
+the same while keeping this goal for later.
 \begin{coq_example}
-cut (R x x); trivial.
+enough (R x x) by auto.
 \end{coq_example}
 We clean the goal by doing an \verb:Abort: command.
 \begin{coq_example*}
@@ -951,10 +918,10 @@ Abort.
 \subsection{Equality}
 
 The basic equality provided in \Coq{} is Leibniz equality, noted infix like
-\verb+x=y+, when \verb:x: and \verb:y: are two expressions of
-type the same Set. The replacement of \verb:x: by \verb:y: in any
-term is effected by a variety of tactics, such as \verb:rewrite:
-and \verb:replace:. 
+\texttt{x = y}, when \texttt{x} and \texttt{y} are two expressions of
+type the same Set. The replacement of \texttt{x} by \texttt{y} in any
+term is effected by a variety of tactics, such as \texttt{rewrite}
+and \texttt{replace}.
 
 Let us give a few examples of equality replacement. Let us assume that
 some arithmetic function \verb:f: is null in zero:
@@ -1009,10 +976,14 @@ In case the equality $t=u$ generated by \verb:replace: $u$ \verb:with:
 $t$ is an assumption
 (possibly modulo symmetry), it will be automatically proved and the
 corresponding goal will not appear. For instance:
-\begin{coq_example}
+
+\begin{coq_eval}
 Restart.
-replace (f 0) with 0.
-rewrite f10; rewrite foo; trivial.
+\end{coq_eval}
+\begin{coq_example}
+Lemma L2 : f (f 1) = 0.
+replace (f 1) with (f 0).
+replace (f 0) with 0; trivial.
 Qed.
 \end{coq_example}
 
@@ -1033,20 +1004,20 @@ predicates over some universe \verb:U:. For instance:
 \begin{coq_example}
 Variable U : Type.
 Definition set := U -> Prop.
-Definition element (x:U) (S:set) := S x.
-Definition subset (A B:set) := 
-  forall x:U, element x A -> element x B.
+Definition element (x : U) (S : set) := S x.
+Definition subset (A B : set) := 
+  forall x : U, element x A -> element x B.
 \end{coq_example}
 
 Now, assume that we have loaded a module of general properties about
 relations over some abstract type \verb:T:, such as transitivity:
 
 \begin{coq_example}
-Definition transitive (T:Type) (R:T -> T -> Prop) :=
-  forall x y z:T, R x y -> R y z -> R x z.
+Definition transitive (T : Type) (R : T -> T -> Prop) :=
+  forall x y z : T, R x y -> R y z -> R x z.
 \end{coq_example}
 
-Now, assume that we want to prove that \verb:subset: is a \verb:transitive:
+We want to prove that \verb:subset: is a \verb:transitive:
 relation. 
 \begin{coq_example}
 Lemma subset_transitive : transitive set subset.
@@ -1071,9 +1042,12 @@ auto.
 \end{coq_example}
 
 Many variations on \verb:unfold: are provided in \Coq. For instance,
-we may selectively unfold one designated occurrence:
-\begin{coq_example}
+instead of unfolding all occurrences of \verb:subset:, we may want to
+unfold only one designated occurrence:
+\begin{coq_eval}
 Undo 2.
+\end{coq_eval}
+\begin{coq_example}
 unfold subset at 2.
 \end{coq_example}
 
@@ -1111,6 +1085,7 @@ are {\sl transparent}.
 \begin{coq_eval}
 Reset Initial.
 Set Printing Width 60.
+Set Printing Compact Contexts.
 \end{coq_eval}
 
 \section{Data Types as Inductively Defined Mathematical Collections}
@@ -1166,11 +1141,14 @@ right; trivial.
 \end{coq_example}
 
 Indeed, the whole proof can be done with the combination of the
- \verb:simple: \verb:induction:, which combines \verb:intro: and \verb:elim:,
+ \verb:destruct:, which combines \verb:intro: and \verb:elim:,
 with good old \verb:auto::
+\begin{coq_eval}
+Abort.
+\end{coq_eval}
 \begin{coq_example}
-Restart.
-simple induction b; auto.
+Lemma duality : forall b:bool, b = true \/ b = false.
+destruct b; auto.
 Qed.
 \end{coq_example}
 
@@ -1194,7 +1172,7 @@ Check nat_rec.
 Let us start by showing how to program the standard primitive recursion
 operator \verb:prim_rec: from the more general \verb:nat_rec::
 \begin{coq_example}
-Definition prim_rec := nat_rec (fun i:nat => nat).
+Definition prim_rec := nat_rec (fun i : nat => nat).
 \end{coq_example}
 
 That is, instead of computing for natural \verb:i: an element of the indexed
@@ -1205,22 +1183,27 @@ About prim_rec.
 \end{coq_example}
 
 Oops! Instead of the expected type \verb+nat->(nat->nat->nat)->nat->nat+ we
-get an apparently more complicated expression. Indeed the type of
-\verb:prim_rec: is equivalent by rule $\beta$ to its expected type; this may
-be checked in \Coq{} by command \verb:Eval Cbv Beta:, which $\beta$-reduces
-an expression to its {\sl normal form}:
+get an apparently more complicated expression.
+In fact, the two types are convertible and one way of having the proper
+type would be to do some computation before actually defining \verb:prim_rec:
+as such:
+
+\begin{coq_eval}
+Reset Initial.
+Set Printing Width 60.
+Set Printing Compact Contexts.
+\end{coq_eval}
+
 \begin{coq_example}
-Eval cbv beta in
-  ((fun _:nat => nat) O ->
-   (forall y:nat, 
-      (fun _:nat => nat) y -> (fun _:nat => nat) (S y)) ->
-   forall n:nat, (fun _:nat => nat) n).
+Definition prim_rec :=
+    Eval compute in nat_rec (fun i : nat => nat).
+About prim_rec.
 \end{coq_example}
 
 Let us now show how to program addition with primitive recursion:
 \begin{coq_example}
 Definition addition (n m:nat) :=
-    prim_rec m (fun p rec:nat => S rec) n.
+    prim_rec m (fun p rec : nat => S rec) n.
 \end{coq_example}
 
 That is, we specify that \verb+(addition n m)+ computes by cases on \verb:n:
@@ -1244,15 +1227,11 @@ Fixpoint plus (n m:nat) {struct n} : nat :=
   end.
 \end{coq_example}
 
-For the rest of the session, we shall clean up what we did so far with 
-types \verb:bool: and \verb:nat:, in order to use the initial definitions
-given in \Coq's \verb:Prelude: module, and not to get confusing error
-messages due to our redefinitions. We thus revert to the initial state:
+\begin{coq_eval}
 \begin{coq_example}
 Reset Initial.
-\end{coq_example}
-\begin{coq_eval}
 Set Printing Width 60.
+Set Printing Compact Contexts.
 \end{coq_eval}
 
 \subsection{Simple proofs by induction}
@@ -1261,20 +1240,21 @@ Let us now show how to do proofs by structural induction. We start with easy
 properties of the \verb:plus: function we just defined. Let us first
 show that $n=n+0$.
 \begin{coq_example}
-Lemma plus_n_O : forall n:nat, n = n + 0.
+Lemma plus_n_O : forall n : nat, n = n + 0.
 intro n; elim n.
 \end{coq_example}
 
-What happened was that \verb:elim n:, in order to construct a \verb:Prop:
-(the initial goal) from a \verb:nat: (i.e. \verb:n:), appealed to the
-corresponding induction principle \verb:nat_ind: which we saw was indeed
+What happened was that \texttt{elim n}, in order to construct a \texttt{Prop}
+(the initial goal) from a \texttt{nat} (i.e. \texttt{n}), appealed to the
+corresponding induction principle \texttt{nat\_ind} which we saw was indeed
 exactly Peano's induction scheme. Pattern-matching instantiated the 
-corresponding predicate \verb:P: to \verb+fun n:nat => n = n + 0+, and we get
-as subgoals the corresponding instantiations of the base case \verb:(P O): ,
-and of the inductive step \verb+forall y:nat, P y -> P (S y)+.
-In each case we get an instance of function \verb:plus: in which its second
+corresponding predicate \texttt{P} to \texttt{fun n : nat => n = n + 0},
+and we get as subgoals the corresponding instantiations of the base case
+\texttt{(P O)}, and of the inductive step
+\texttt{forall y : nat, P y -> P (S y)}.
+In each case we get an instance of function \texttt{plus} in which its second
 argument starts with a constructor, and is thus amenable to simplification
-by primitive recursion. The \Coq{} tactic \verb:simpl: can be used for
+by primitive recursion. The \Coq{} tactic \texttt{simpl} can be used for
 this purpose:
 \begin{coq_example}
 simpl.
@@ -1305,12 +1285,12 @@ We now proceed to the similar property concerning the other constructor
 Lemma plus_n_S : forall n m:nat, S (n + m) = n + S m.
 \end{coq_example}
 
-We now go faster, remembering that tactic \verb:simple induction: does the
+We now go faster, using the tactic \verb:induction:, which does the
 necessary \verb:intros: before applying \verb:elim:. Factoring simplification
 and automation in both cases thanks to tactic composition, we prove this
 lemma in one line:
 \begin{coq_example}
-simple induction n; simpl; auto.
+induction n; simpl; auto.
 Qed.
 Hint Resolve plus_n_S .
 \end{coq_example}
@@ -1324,7 +1304,7 @@ Lemma plus_com : forall n m:nat, n + m = m + n.
 Here we have a choice on doing an induction on \verb:n: or on \verb:m:, the
 situation being symmetric. For instance:
 \begin{coq_example}
-simple induction m; simpl; auto.
+induction m as [ | m IHm ]; simpl; auto.
 \end{coq_example}
 
 Here \verb:auto: succeeded on the base case, thanks to our hint
@@ -1332,7 +1312,7 @@ Here \verb:auto: succeeded on the base case, thanks to our hint
 \verb:auto: does not handle:
 
 \begin{coq_example}
-intros m' E; rewrite <- E; auto.
+rewrite <- IHm; auto.
 Qed.
 \end{coq_example}
 
@@ -1344,13 +1324,13 @@ the constructors \verb:O: and \verb:S:: it computes to \verb:False:
 when its argument is \verb:O:, and to \verb:True: when its argument is 
 of the form \verb:(S n)::
 \begin{coq_example}
-Definition Is_S (n:nat) := match n with
-                           | O => False
-                           | S p => True
-                           end.
+Definition Is_S (n : nat) := match n with
+                             | O => False
+                             | S p => True
+                             end.
 \end{coq_example}
 
-Now we may use the computational power of \verb:Is_S: in order to prove
+Now we may use the computational power of \verb:Is_S: to prove
 trivially that \verb:(Is_S (S n))::
 \begin{coq_example}
 Lemma S_Is_S : forall n:nat, Is_S (S n).
@@ -1389,8 +1369,11 @@ Actually, a specific tactic \verb:discriminate: is provided
 to produce mechanically such proofs, without the need for the user to define
 explicitly the relevant discrimination predicates:
 
+\begin{coq_eval}
+Abort.
+\end{coq_eval}
 \begin{coq_example}
-Restart.
+Lemma no_confusion : forall n:nat, 0 <> S n.
 intro n; discriminate.
 Qed.
 \end{coq_example}
@@ -1403,12 +1386,13 @@ may define inductive families, and for instance inductive predicates.
 Here is the definition of predicate $\le$ over type \verb:nat:, as
 given in \Coq's \verb:Prelude: module:
 \begin{coq_example*}
-Inductive le (n:nat) : nat -> Prop :=
+Inductive le (n : nat) : nat -> Prop :=
   | le_n : le n n
-  | le_S : forall m:nat, le n m -> le n (S m).
+  | le_S : forall m : nat, le n m -> le n (S m).
 \end{coq_example*}
 
-This definition introduces a new predicate \verb+le:nat->nat->Prop+,
+This definition introduces a new predicate
+\verb+le : nat -> nat -> Prop+,
 and the two constructors \verb:le_n: and \verb:le_S:, which are the
 defining clauses of \verb:le:. That is, we get not only the ``axioms''
 \verb:le_n: and \verb:le_S:, but also the converse property, that 
@@ -1426,7 +1410,7 @@ Check le_ind.
 Let us show how proofs may be conducted with this principle.
 First we show that $n\le m \Rightarrow n+1\le m+1$:
 \begin{coq_example}
-Lemma le_n_S : forall n m:nat, le n m -> le (S n) (S m).
+Lemma le_n_S : forall n m : nat, le n m -> le (S n) (S m).
 intros n m n_le_m.
 elim n_le_m.
 \end{coq_example}
@@ -1442,10 +1426,14 @@ intros; apply le_S; trivial.
 
 Now we know that it is a good idea to give the defining clauses as hints,
 so that the proof may proceed with a simple combination of 
-\verb:induction: and \verb:auto:.
+\verb:induction: and \verb:auto:. \verb:Hint Constructors le:
+is just an abbreviation for \verb:Hint Resolve le_n le_S:.
+\begin{coq_eval}
+Abort.
+\end{coq_eval}
 \begin{coq_example}
-Restart.
-Hint Resolve le_n le_S .
+Hint Constructors le.
+Lemma le_n_S : forall n m : nat, le n m -> le (S n) (S m).
 \end{coq_example}
 
 We have a slight problem however. We want to say ``Do an induction on
@@ -1453,7 +1441,7 @@ hypothesis \verb:(le n m):'', but we have no explicit name for it. What we
 do in this case is to say ``Do an induction on the first unnamed hypothesis'',
 as follows.
 \begin{coq_example}
-simple induction 1; auto.
+induction 1; auto.
 Qed.
 \end{coq_example}
 
@@ -1483,6 +1471,7 @@ Qed.
 \begin{coq_eval}
 Reset Initial.
 Set Printing Width 60.
+Set Printing Compact Contexts.
 \end{coq_eval}
 
 \section{Opening library modules}
@@ -1552,6 +1541,7 @@ known lemmas about both the successor and the less or equal relation, just ask:
 \begin{coq_eval}
 Reset Initial.
 Set Printing Width 60.
+Set Printing Compact Contexts.
 \end{coq_eval}
 \begin{coq_example}
 Search S le.
@@ -1562,14 +1552,13 @@ predicate appears at the head position in the conclusion.
 SearchHead le.
 \end{coq_example}
 
-A new and more convenient search tool is \verb:SearchPattern:
-developed by Yves Bertot. It allows finding the theorems with a
-conclusion matching a given pattern, where \verb:_: can be used in
-place of an arbitrary term. We remark in this example, that \Coq{}
+The \verb:Search: commands also allows finding the theorems
+containing a given pattern, where \verb:_: can be used in
+place of an arbitrary term. As shown in this example, \Coq{}
 provides usual infix notations for arithmetic operators.
 
 \begin{coq_example}
-SearchPattern (_ + _ = _).
+Search (_ + _ = _).
 \end{coq_example}
 
 \section{Now you are on your own}