mise a jour V8

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

3 files changed, 76 insertions, 60 deletions

diff --git a/doc/Cases.tex b/doc/Cases.tex
index 3007f2e91..4e8918433 100644
--- a/doc/Cases.tex
+++ b/doc/Cases.tex
@@ -8,7 +8,7 @@
 This section describes the full form of pattern-matching in {\Coq} terms.
 
 \asection{Patterns}\label{implementation} The full syntax of {\tt
-Cases} is presented in figure \ref{cases-grammar}.  Identifiers in
+match} is presented in figure \ref{cases-grammar}.  Identifiers in
 patterns are either constructor names or variables. Any identifier
 that is not the constructor of an inductive or coinductive type is
 considered to be a variable. A variable name cannot occur more than
@@ -18,7 +18,7 @@ a lowercase letter.
 If a pattern has the form $(c~\vec{x})$ where $c$ is a constructor
 symbol and $\vec{x}$ is a linear vector of variables, it is called
 {\em simple}: it is the kind of pattern recognized by the basic
-version of {\tt Cases}. If a pattern is
+version of {\tt match}. If a pattern is
 not simple we call it {\em nested}.
 
 A variable pattern matches any value, and the identifier is bound to
@@ -58,24 +58,24 @@ empty.
 \end{tabular}
 \end{minipage}}
 \end{center}
-\caption{Extended Cases syntax}
+\caption{Extended match syntax}
 \label{cases-grammar}
 \end{figure}
 
-Since extended {\tt Cases} expressions are compiled into the primitive
+Since extended {\tt match} expressions are compiled into the primitive
 ones, the expressiveness of the theory remains the same. Once the
 stage of parsing has finished only simple patterns remain. An easy way
 to see the result of the expansion is by printing the term with
 \texttt{Print} if the term is a constant, or using the command
 \texttt{Check}.
 
-The extended \texttt{Cases} still accepts an optional {\em elimination
-predicate} enclosed between brackets \texttt{<>}.  Given a pattern
+The extended \texttt{match} still accepts an optional {\em elimination
+predicate} given after the keyword \texttt{return}.  Given a pattern
 matching expression, if all the right hand sides of \texttt{=>} ({\em
 rhs} in short) have the same type, then this type can be sometimes
 synthesized, and so we can omit the \texttt{<>}. Otherwise 
-the predicate between \texttt{<>} has to be provided, like for the basic
-\texttt{Cases}.
+the predicate after \texttt{return} has to be provided, like for the basic
+\texttt{match}.
 
 Let us illustrate through examples the different aspects of extended
 pattern matching. Consider for example the function that computes the
@@ -108,9 +108,9 @@ Fixpoint max (n m:nat) {struct m} : nat :=
 which will be compiled into the previous form.
 
 The pattern-matching compilation strategy examines patterns from left
-to right. A \texttt{Cases} expression is generated {\bf only} when
+to right. A \texttt{match} expression is generated {\bf only} when
 there is at least one constructor in the column of patterns. E.g. the
-following example does not build a \texttt{Cases} expression.
+following example does not build a \texttt{match} expression.
 
 \begin{coq_example}
 Check (fun x:nat => match x return nat with
@@ -432,7 +432,7 @@ Fixpoint concat
 In all the previous examples the elimination predicate does not depend
 on the object(s) matched. But it may depend and the typical case 
 is when we write a proof by induction or a function that yields an
-object of dependent type. An example of proof using \texttt{Cases} in
+object of dependent type. An example of proof using \texttt{match} in
 given in section \ref{refine-example}
 
 For example, we can write 
@@ -476,20 +476,20 @@ Fixpoint dec (n m:nat) {struct n} : LE n m \/ LE m n :=
 \end{coq_example}
 In the example of \texttt{dec} the elimination predicate is binary
 because we destructure two arguments of \texttt{nat} which is a
-non-dependent type. Notice that the first \texttt{Cases} is dependent while 
+non-dependent type. Notice that the first \texttt{match} is dependent while 
 the second is not.
 
 In general, consider the terms $e_1\ldots e_n$,
 where  the type of $e_i$ is an instance of a family type
 $[\vec{d_i}:\vec{D_i}]T_i$  ($1\leq i
-\leq n$). Then, in expression \texttt{<}${\cal P}$\texttt{>Cases}  $e_1\ldots
+\leq n$). Then, in expression \texttt{<}${\cal P}$\texttt{>match}  $e_1\ldots
 e_n$ \texttt{of} \ldots \texttt{end}, the 
 elimination predicate ${\cal P}$ should be of the form:
 $[\vec{d_1}:\vec{D_1}][x_1:T_1]\ldots [\vec{d_n}:\vec{D_n}][x_n:T_n]Q.$
 
-The user can also use \texttt{Cases} in combination with the tactic
+The user can also use \texttt{match} in combination with the tactic
 \texttt{refine} (see section \ref{refine}) to build incomplete proofs
-beginning with a \texttt{Cases} construction.
+beginning with a \texttt{match} construction.
 
 \asection{Pattern-matching on inductive objects involving local
 definitions}
@@ -603,7 +603,7 @@ the pattern matching is not exhaustive
     of arity } {\sl num} \sverb{(for non dependent case) or } {\sl
     num} \sverb{(for dependent case)}
 
-The elimination predicate provided to \texttt{Cases} has not the
+The elimination predicate provided to \texttt{match} has not the
   expected arity
 
 
@@ -620,9 +620,9 @@ The elimination predicate provided to \texttt{Cases} has not the
 %   $T$.  Then, the strategy may fail to find out a correct elimination
 %   predicate during some step of compilation.  In this situation we
 %   recommend the user to rewrite the nested dependent patterns into
-%   several \texttt{Cases} with {\em simple patterns}.
+%   several \texttt{match} with {\em simple patterns}.
   
-\item {\tt Unable to infer a Cases predicate\\
+\item {\tt Unable to infer a match predicate\\
     Either there is a type incompatiblity or the problem involves\\
     dependencies}
  
@@ -657,14 +657,14 @@ The elimination predicate provided to \texttt{Cases} has not the
 % This is because the strategy generates a term that is correct w.r.t.
 % the initial term but which does not pass the guard condition.  In
 % this situation we recommend the user to transform the nested dependent
-% patterns into {\em several \texttt{Cases} of simple patterns}.  Let us
+% patterns into {\em several \texttt{match} of simple patterns}.  Let us
 % explain this with an example.  Consider the following definition of a
 % function that yields the last element of a list and \texttt{O} if it is
 % empty:
 
 % \begin{coq_example}
 %   Fixpoint last [n:nat; l:(listn n)] : nat :=
-%    Cases l of 
+%    match l of 
 %      (consn _ a niln) => a
 %    | (consn m _ x) => (last m x) | niln => O
 %    end.
@@ -676,7 +676,7 @@ The elimination predicate provided to \texttt{Cases} has not the
 
 % \begin{coq_example*}
 %   Fixpoint last [n:nat; l:(listn n)] : nat :=
-%    Cases l of
+%    match l of
 %      (consn _ a niln) => a
 %    | (consn n _ (consn m b x)) => (last n (consn m b x))
 %    | niln => O
@@ -700,7 +700,7 @@ The elimination predicate provided to \texttt{Cases} has not the
 
 % \begin{coq_example}
 %   Fixpoint last [n:nat; l:(listn n)] : nat :=
-%   <[_:nat]nat>Cases l of
+%   <[_:nat]nat>match l of
 %     (consn m a x) => Cases x of niln => a | _ => (last m x) end
 %   | niln => O
 %   end.
diff --git a/doc/RefMan-cic.tex b/doc/RefMan-cic.tex
index 791de51eb..b8f445968 100755
--- a/doc/RefMan-cic.tex
+++ b/doc/RefMan-cic.tex
@@ -815,6 +815,10 @@ Inductive exProp (P:Prop->Prop) : Prop
   := exP_intro : forall X:Prop, P X -> exProp P.
 \end{coq_example*}
 The same definition on \Set{} is not allowed and fails~:
+\begin{coq_eval}
+(********** The following is not correct and should produce **********)
+(*** Error: Large non-propositional inductive types must be in Type***)
+\end{coq_eval}
 \begin{coq_example}
 Inductive exSet (P:Set->Prop) : Set 
   := exS_intro : forall X:Set, P X -> exSet P.
@@ -1076,23 +1080,23 @@ eliminations are allowed.
 \item[\Prop-extended] 
 \inference{
    \frac{I \mbox{~is an empty or singleton
-       definition}}{\compat{I:\Prop}{I\ra \Set}}~~~~~
-   \frac{I \mbox{~is an empty or small singleton
-       definition}}{\compat{I:\Prop}{I\ra \Type(i)}}
+       definition}~~~s\in\Sort}{\compat{I:\Prop}{I\ra s}}
 }
 \end{description}
 
-A {\em singleton definition} has always an informative content,
-even if it is a proposition.
+% A {\em singleton definition} has always an informative content,
+% even if it is a proposition.
 
 A {\em singleton
-definition} has only one constructor and all the argument of this
-constructor are non informative. In that case, there is a canonical
+definition} has only one constructor and all the arguments of this
+constructor have type \Prop. In that case, there is a canonical
 way to interpret the informative extraction on an object in that type,
 such that the elimination on any sort $s$ is legal.  Typical examples are
-the conjunction of non-informative propositions and the equality. In
-that case, the term \verb!eq_rec! which was defined as an axiom, is
-now a term of the calculus.
+the conjunction of non-informative propositions and the equality. 
+If there is an hypothesis $h:a=b$ in the context, it can be used for
+rewriting not only in logical propositions but also in any type.
+% In that case, the term \verb!eq_rec! which was defined as an axiom, is
+% now a term of the calculus.
 \begin{coq_example}
 Print eq_rec.
 Extraction eq_rec.
@@ -1117,32 +1121,34 @@ branch corresponding to the $c:C$ constructor.
 We write \CI{c}{P} for \CI{c:C}{P} with $C$ the type of $c$.
 
 \paragraph{Examples.}
-For $\ListA$ the type of $P$ will be $\ListA\ra s$ for $s \in
-\{\Prop,\Set,\Type(i)\}$. \\ 
+For $\ListA$ the type of $P$ will be $\ListA\ra s$ for $s \in \Sort$. \\ 
 $ \CI{(\cons~A)}{P} \equiv
-(a:A)(l:\ListA)(P~(\cons~A~a~l))$.
+\forall a:A, \forall l:\ListA,(P~(\cons~A~a~l))$.
 
 For $\LengthA$, the type of $P$ will be
-$(l:\ListA)(n:\nat)(\LengthA~l~n)\ra \Prop$ and the expression
+$\forall l:\ListA,\forall n:\nat, (\LengthA~l~n)\ra \Prop$ and the expression
 \CI{(\LCons~A)}{P} is defined as:\\ 
-$(a:A)(l:\ListA)(n:\nat)(h:(\LengthA~l~n))(P~(\cons~A~a~l)~(\nS~n)~(\LCons~A~a~l~n~l))$.\\ 
+$\forall a:A, \forall l:\ListA, \forall n:\nat, \forall
+h:(\LengthA~l~n), (P~(\cons~A~a~l)~(\nS~n)~(\LCons~A~a~l~n~l))$.\\ 
 If $P$ does not depend on its third argument, we find the more natural
 expression:\\ 
-$(a:A)(l:\ListA)(n:\nat)(\LengthA~l~n)\ra(P~(\cons~A~a~l)~(\nS~n))$.
+$\forall a:A, \forall l:\ListA, \forall n:\nat,
+(\LengthA~l~n)\ra(P~(\cons~A~a~l)~(\nS~n))$.
 
 \paragraph{Typing rule.}
 
 Our very general destructor for inductive definition enjoys the
-following typing rule, where we write 
-\[
-\Case{P}{c}{[x_{11}:T_{11}]\ldots[x_{1p_1}:T_{1p_1}]g_1\ldots
-  [x_{n1}:T_{n1}]\ldots[x_{np_n}:T_{np_n}]g_n}
-\]
-for 
-\[
-\Case{P}{c}{(c_1~x_{11}~...~x_{1p_1}) \Ra g_1 ~|~\ldots~|~
-(c_n~x_{n1}...x_{np_n}) \Ra g_n }
-\]
+following typing rule
+% , where we write 
+% \[
+% \Case{P}{c}{[x_{11}:T_{11}]\ldots[x_{1p_1}:T_{1p_1}]g_1\ldots
+%   [x_{n1}:T_{n1}]\ldots[x_{np_n}:T_{np_n}]g_n}
+% \]
+% for 
+% \[
+% \Case{P}{c}{(c_1~x_{11}~...~x_{1p_1}) \Ra g_1 ~|~\ldots~|~
+% (c_n~x_{n1}...x_{np_n}) \Ra g_n }
+% \]
 
 \begin{description}
 \item[match] \label{elimdep} \index{Typing rules!match}
@@ -1165,7 +1171,7 @@ are (writing just $t:M$ instead of \WTEG{t}{M}, the environment and
 context being the same in all the judgments).
 
 \[\frac{l:\ListA~~P:\ListA\ra s~~~f_1:(P~(\Nil~A))~~
-      f_2:(a:A)(l:\ListA)(P~(\cons~A~a~l))}
+      f_2:\forall a:A, \forall l:\ListA, (P~(\cons~A~a~l))}
     {\Case{P}{l}{f_1~f_2}:(P~l)}\]
 
 \[\frac{
@@ -1173,7 +1179,8 @@ context being the same in all the judgments).
 H:(\LengthA~L~N) \\ P:(l:\ListA)(n:\nat)(\LengthA~l~n)\ra
   \Prop\\
  f_1:(P~(\Nil~A)~\nO~\LNil) \\
-   f_2:(a:A)(l:\ListA)(n:\nat)(h:(\LengthA~l~n))(P~(\cons~A~a~n)~(\nS~n)~(\LCons~A~a~l~n~h)) 
+   f_2:\forall a:A, \forall l:\ListA, \forall n:\nat, \forall
+  h:(\LengthA~l~n), (P~(\cons~A~a~n)~(\nS~n)~(\LCons~A~a~l~n~h)) 
       \end{array}}
     {\Case{P}{H}{f_1~f_2}:(P~L~N~H)}\]
 
@@ -1226,8 +1233,8 @@ principle of type
 \[(P:\nat\ra\Prop)(P~\nO)\ra((n:\nat)(P~n)\ra(P~(\nS~n)))\ra(n:\nat)(P~n)\]
 can be represented by the term:
 \[\begin{array}{l}
-[P:\nat\ra\Prop][f:(P~\nO)][g:(n:\nat)(P~n)\ra(P~(\nS~n))]\\
-\Fix{h}{h:(n:\nat)(P~n):=[n:\nat]\Case{P}{n}{f~[p:\nat](g~p~(h~p))}}
+[P:\nat\ra\Prop][f:(P~\nO)][g:\forall n:\nat, (P~n)\ra(P~(\nS~n))]\\
+\Fix{h}{h:\forall n:\nat, (P~n):=\lb n:\nat\mto \Case{P}{n}{f~[p:\nat](g~p~(h~p))}}
 \end{array}
 \]
 
@@ -1243,7 +1250,8 @@ For doing this the syntax of fixpoints is extended and becomes
  \[\Fix{f_i}{f_1/k_1:A_1:=t_1 \ldots f_n/k_n:A_n:=t_n}\]
 where $k_i$ are positive integers.
 Each $A_i$ should be a type (reducible to a term) starting with at least
-$k_i$ products $(y_1:B_1)\ldots (y_{k_i}:B_{k_i}) A'_i$ and $B_{k_i}$
+$k_i$ products $\forall y_1:B_1,\ldots \forall y_{k_i}:B_{k_i}, A'_i$ 
+and $B_{k_i}$
 being an instance of an inductive definition.
 
 Now in the definition $t_i$, if $f_j$ occurs then it should be applied
@@ -1256,7 +1264,8 @@ One needs first to  define the notion of
 {\em recursive arguments of a constructor}\index{Recursive arguments}.
 For an inductive definition \Ind{\Gamma}{\Gamma_P}{\Gamma_I}{\Gamma_C},
 the type of a constructor $c$ have the form
-$(p_1:P_1)\ldots(p_r:P_r)(x_1:T_1)\ldots (x_r:T_r)(I_j~p_1\ldots 
+$\forall p_1:P_1,\ldots \forall p_r:P_r, 
+\forall x_1:T_1, \ldots \forall x_r:T_r, (I_j~p_1\ldots 
 p_r~t_1\ldots  t_s)$ the recursive arguments will correspond to $T_i$ in
 which one of the $I_l$ occurs.
 
@@ -1269,15 +1278,16 @@ where $\Gamma_I$ is $[I_1:A_1;\ldots;I_k:A_k]$, and $\Gamma_C$ is
   $[c_1:C_1;\ldots;c_n:C_n]$.
 The terms structurally smaller than $y$ are:
 \begin{itemize}
-\item $(t~u), [x:u]t$ when $t$ is structurally smaller than $y$ .
+\item $(t~u), \lb x:u \mto t$ when $t$ is structurally smaller than $y$ .
 \item \Case{P}{c}{f_1\ldots f_n} when each $f_i$ is structurally
   smaller than $y$. \\
   If $c$ is $y$ or is structurally smaller than $y$, its type is an inductive
   definition $I_p$ part of the inductive
   declaration corresponding to $y$. 
   Each $f_i$ corresponds to a type of constructor $C_q \equiv
-  (y_1:B_1)\ldots (y_k:B_k)(I~a_1\ldots a_k)$ and can consequently be
-  written $[y_1:B'_1]\ldots [y_k:B'_k]g_i$.
+  \forall y_1:B_1, \ldots \forall y_k:B_k, (I~a_1\ldots a_k)$ 
+  and can consequently be
+  written $\lb y_1:B'_1\mto \ldots \lb y_k:B'_k\mto g_i$.
   ($B'_i$ is obtained from $B_i$ by substituting parameters variables)
   the variables $y_j$ occurring
   in $g_i$ corresponding to recursive arguments $B_i$ (the ones in
@@ -1397,6 +1407,12 @@ by using the compiler option \texttt{-impredicative-set}.
 
 For example, using the ordinary \texttt{coqtop} command, the following
 is rejected.
+\begin{coq_eval}
+(** This example should fail *******************************
+    Error: The term forall X:Set, X -> X has type Type
+    while it is expected to have type Set
+***)
+\end{coq_eval}
 \begin{coq_example}
 Definition id: Set := forall (X:Set),X->X.
 \end{coq_example}
@@ -1404,7 +1420,7 @@ while it will type-check, if one use instead the \texttt{coqtop
   -impredicative-set} command.
 
 The major change in the theory concerns the rule for product formation
-in the sort \Set, which is extendet to a domain in any sort~:
+in the sort \Set, which is extended to a domain in any sort~:
 \begin{description}
 \item [Prod]  \index{Typing rules!Prod (impredicative Set)}
 \inference{\frac{\WTEG{T}{s}~~~~s\in\Sort~~~~~~
diff --git a/doc/RefMan.txt b/doc/RefMan.txt
index b2ce8a139..61f05cc13 100644
--- a/doc/RefMan.txt
+++ b/doc/RefMan.txt
@@ -3,8 +3,8 @@ TUTORIAL				N. Oury
 GUIDE PASSAGE V7-V8			BB
 
 MANUEL DE REFERENCE
-\include{RefMan-int}% Introduction	HH
-\include{RefMan-pre}% Credits		HH
+\include{RefMan-int}% Introduction	HH - relu CP 
+\include{RefMan-pre}% Credits		HH - relu CP
 
 \tableofcontents