Update the Tutorial.

1 files changed, 106 insertions, 112 deletions

diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex
index 30b6304c1..75318c896 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,23 +33,23 @@ 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.}.
+Coq can be tested through a REPL (Read-Eval-Print-Loop) called
+\texttt{coqtop} but for actual developments it is preferable to use
+a graphical user interface such as CoqIDE or
+Proof General\footnote{See \url{https://proofgeneral.github.io/}.}.
 
 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
+The following examples are executed within \texttt{coqtop}.
+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
+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{}
@@ -61,7 +61,7 @@ invocation of \Coq{} delivers a message such as:
 \begin{flushleft}
 \begin{verbatim}
 unix:~> coqtop
-Welcome to Coq 8.2 (January 2009)
+Welcome to Coq 8.7 (June 2017)
 
 Coq < 
 \end{verbatim}
@@ -69,8 +69,8 @@ Coq <
 \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
+used. You should always return this version number when you report an
+anomaly to our bug-tracking system
 \url{https://coq.inria.fr/bugs/}.
 
 \chapter{Basic Predicate Calculus}
@@ -175,7 +175,7 @@ arrow function constructor, in order to get a functional type
 \begin{coq_example}
 Check (nat -> Prop).
 \end{coq_example}
-which may be composed one more times with \verb:nat: in order to obtain the
+which may be composed once more 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):. 
@@ -340,17 +340,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 to \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,14 +378,14 @@ We may thus complete the proof of \verb:distr_impl: with one composite tactic:
 apply H; [ assumption | apply H0; assumption ].
 \end{coq_example}
 
+It is discouraged though to rely on automatically generated names in finished
+proof scripts. And be careful not to abuse \verb:;:.
+
 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.
-
 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:
@@ -410,18 +405,8 @@ 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: 
-\begin{coq_example}
-Inspect 3.
-\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.
+backtrack n steps. None of these commands should be left in a finished proof
+document.
 
 \section{Propositional Calculus}
 
@@ -438,7 +423,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,
@@ -465,7 +450,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 +483,14 @@ 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_example}
+Restart.
+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
@@ -542,7 +535,7 @@ 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 =>+, 
+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,7 +565,7 @@ 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. 
@@ -652,15 +645,11 @@ function and predicate symbols.
 
 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 
+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:.
+respectively 1 and 2.
 
 \begin{coq_example}
 Reset Initial.
@@ -669,8 +658,7 @@ Reset Initial.
 Set Printing Width 60.
 \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 +674,18 @@ 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 +699,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.
@@ -802,7 +790,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 +808,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 +824,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 +835,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 +849,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;
@@ -935,12 +925,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,7 +941,7 @@ 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
+\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:. 
@@ -1011,8 +1001,8 @@ $t$ is an assumption
 corresponding goal will not appear. For instance:
 \begin{coq_example}
 Restart.
-replace (f 0) with 0.
-rewrite f10; rewrite foo; trivial.
+replace (f 1) with (f 0).
+replace (f 0) with 0; trivial.
 Qed.
 \end{coq_example}
 
@@ -1033,20 +1023,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.
@@ -1166,11 +1156,11 @@ 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_example}
 Restart.
-simple induction b; auto.
+destruct b; auto.
 Qed.
 \end{coq_example}
 
@@ -1194,7 +1184,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 +1195,25 @@ 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.
+\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:
@@ -1269,9 +1262,9 @@ 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
 exactly Peano's induction scheme. Pattern-matching instantiated the 
-corresponding predicate \verb:P: to \verb+fun n:nat => n = n + 0+, and we get
+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)+.
+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
 argument starts with a constructor, and is thus amenable to simplification
 by primitive recursion. The \Coq{} tactic \verb:simpl: can be used for
@@ -1305,12 +1298,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 +1317,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; simpl; auto.
 \end{coq_example}
 
 Here \verb:auto: succeeded on the base case, thanks to our hint
@@ -1332,7 +1325,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,10 +1337,10 @@ 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
@@ -1403,12 +1396,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 
@@ -1442,10 +1436,11 @@ 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_example}
 Restart.
-Hint Resolve le_n le_S .
+Hint Constructors le.
 \end{coq_example}
 
 We have a slight problem however. We want to say ``Do an induction on
@@ -1453,7 +1448,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}
 
@@ -1562,14 +1557,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
+The \verb:Search: commands also allows finding the theorems
+containing a given pattern, where \verb:_: can be used in
 place of an arbitrary term. We remark in this example, that \Coq{}
 provides usual infix notations for arithmetic operators.
 
 \begin{coq_example}
-SearchPattern (_ + _ = _).
+Search (_ + _ = _).
 \end{coq_example}
 
 \section{Now you are on your own}