From e978da8c41d8a3c19a29036d9c569fbe2a4616b0 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 16 Jun 2006 14:41:51 +0000
Subject: Imported Upstream version 8.0pl3+8.1beta

---
 doc/tutorial/Tutorial.tex | 37 ++++---------------------------------
 1 file changed, 4 insertions(+), 33 deletions(-)

(limited to 'doc/tutorial/Tutorial.tex')

diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex
index 7c840509..73d833c4 100755
--- a/doc/tutorial/Tutorial.tex
+++ b/doc/tutorial/Tutorial.tex
@@ -96,7 +96,6 @@ of the system, called respectively \verb:Prop:, \verb:Set:, and
 Every valid expression $e$ in Gallina is associated with a specification,
 itself a valid expression, called its {\sl type} $\tau(E)$. We write
 $e:\tau(E)$ for the judgment that $e$ is of type $E$. 
-%CP Le role de \tau n'est pas clair.
 You may request \Coq~ to return to you the type of a valid expression by using
 the command \verb:Check::
 
@@ -271,7 +270,6 @@ Goal (A -> B -> C) -> (A -> B) -> A -> C.
 The system displays the current goal below a double line, local hypotheses
 (there are none initially) being displayed above the line. We call 
 the combination of local hypotheses with a goal a {\sl judgment}.
-%The new prompt \verb:Unnamed_thm <: indicates that.
 We are now in an inner 
 loop of the system, in proof mode. 
 New commands are available in this
@@ -287,10 +285,6 @@ of the application to the list of local hypotheses:
 intro H.
 \end{coq_example}
 
-%{\bf Warning} to users of \Coq~ previous versions: The display of a sequent in
-%older versions of \Coq~ is inverse of this convention: the goal is displayed
-%above the double line, the hypotheses below.
-
 Several introductions may be done in one step:
 \begin{coq_example}
 intros H' HA.
@@ -337,7 +331,7 @@ Save trivial_lemma.
 \end{coq_example}
 
 As a comment, the system shows the proof script listing all tactic
-commands used in the proof. % ligne blanche apres exact HA??
+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:
@@ -345,9 +339,6 @@ the initial goal as a conjectured lemma:
 Lemma distr_impl : (A -> B -> C) -> (A -> B) -> A -> C.
 \end{coq_example}
 
-%{\bf Warning} to users of \Coq~ older versions: In order to enter the proof
-%engine, at this point a dummy \verb:Goal.: command had to be typed in.
-
 Next, we may omit the names of local assumptions created by the introduction
 tactics, they can be automatically created by the proof engine as new
 non-clashing names.
@@ -407,7 +398,7 @@ 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: % Attention ici ??
+notions: 
 \begin{coq_example}
 Inspect 3.
 \end{coq_example}
@@ -522,8 +513,6 @@ 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. 
-%In order to get this facility, we have to import a library module 
-%called ``Dyckhoff'':
 \begin{coq_example}
 Restart.
 tauto.
@@ -1024,7 +1013,6 @@ more specialised properties.
 
 Assume that we want to develop the theory of sets represented as characteristic
 predicates over some universe \verb:U:. For instance:
-%CP Une petite explication pour le codage de element ?
 \begin{coq_example}
 Variable U : Type.
 Definition set := U -> Prop.
@@ -1099,9 +1087,6 @@ mathematical justification of a logical development relies only on
 
 Conversely, ordinary mathematical definitions can be unfolded at will, they
 are {\sl transparent}. 
-%It is possible to enforce the reverse convention by
-%declaring a definition as {\sl opaque} or a lemma as {\sl transparent}.
-
 \chapter{Induction}
 
 \section{Data Types as Inductively Defined Mathematical Collections}
@@ -1244,8 +1229,7 @@ Reset bool.
 
 
 \subsection{Simple proofs by induction}
-%CP  Pourquoi ne pas commencer par des preuves d'egalite entre termes
-%    convertibles. 
+
 \begin{coq_eval}
 Reset Initial.
 \end{coq_eval}
@@ -1427,7 +1411,6 @@ elim n_le_m.
 What happens here is similar to the behaviour of \verb:elim: on natural
 numbers: it appeals to the relevant induction principle, here \verb:le_ind:,
 which generates the two subgoals, which may then be solved easily
-%as if ``backchaining'' the current goal
 with the help of the defining clauses of \verb:le:.
 \begin{coq_example}
 apply le_n; trivial.
@@ -1519,8 +1502,6 @@ development is not type-checked again.
 You may create your own modules, by writing \Coq~ commands in a file,
 say \verb:my_module.v:. Such a module may be simply loaded in the current
 context, with command \verb:Load my_module:. It may also be compiled,
-%using the command \verb:Compile Module my_module: directly at the
-%\Coq~ toplevel, or else 
 in ``batch'' mode, using the UNIX command
 \verb:coqc:. Compiling the module \verb:my_module.v: creates a 
 file \verb:my_module.vo:{} that can be reloaded with command
@@ -1559,16 +1540,6 @@ provides usual infix notations for arithmetic operators.
 SearchPattern (_ + _ = _).
 \end{coq_example}
 
-% The argument to give is a type and it searches in the current context all
-% constants having the same type modulo certain notion of
-% \textit{isomorphism}. For example~:
-
-% \begin{coq_example}
-% Require Arith.
-% SearchIsos nat -> nat -> Prop.
-% SearchIsos (x,y,z:nat)(le x y) -> (le y z) -> (le x z).
-% \end{coq_example} 
- 
 \section{Now you are on your own}
 
 This tutorial is necessarily incomplete. If you wish to pursue serious
@@ -1581,4 +1552,4 @@ with \Coq, in order to acquaint yourself with various proof techniques.
 
 \end{document}
 
-% $Id: Tutorial.tex 8607 2006-02-23 14:21:14Z herbelin $ 
+% $Id: Tutorial.tex 8715 2006-04-14 12:43:23Z cpaulin $ 
-- 
cgit v1.2.3

