Ajout de précisions dans la doc de functional scheme et consort +

adaptation à la nouvelle version (syntaxe + sémantique). Reste
Functional Scheme.


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

3 files changed, 84 insertions, 25 deletions

diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index cd5c2b3c4..be80e7eb7 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -1325,8 +1325,9 @@ mutual induction principles. It is described in Section~\ref{Scheme}.
 
 \subsubsection{\tt Function {\ident} {\binder$_1$}\ldots{\binder$_n$}
  {\tt \{}decrease\_annot{\tt\}} : type$_0$ := \term$_0$.
+}
 \comindex{Function}
-\label{Function}}
+\label{Function}
 
 This \emph{experimental} command can be seen as a generalization of
 {\tt Fixpoint}.  It is actually a wrapper for several ways of defining
@@ -1376,10 +1377,31 @@ Function plus (n m : nat) {struct n} : nat :=
 
 \paragraph{Limitations}
 \label{sec:Function-limitations}
-\term$_0$ must be build as an imbrication of pattern matchings
+\term$_0$ must be build as a \emph{pure pattern-matching tree}
 (\texttt{match...with}) with $\lambda$-abstraction and applications only
-\emph{at the end} of each branch.
-For now dependent cases are not treated.
+\emph{at the end} of each branch.  For now dependent cases are not
+treated.
+
+
+\ErrMsg 
+
+\errindex{while trying to define Inductive R\_\ident ...}
+
+The generation of the graph relation \texttt{(R\_\ident)} used to
+compute the induction scheme of \ident raised a typing error, the
+definition of \ident was aborted. You can use \texttt{Fixpoint}
+instead of \texttt{Function}, but the scheme will not be generated.
+
+This error happens generally when: 
+
+\begin{itemize}
+\item the definition uses pattern matching on dependent types, which
+  \texttt{Function} cannot deal with yet.
+\item the definition is not a \emph{pattern-matching tree} as
+  explained above.
+\end{itemize}
+
+
 
 \SeeAlso{\ref{FunScheme},\ref{FunScheme-examples},\ref{FunInduction}}
 
@@ -1387,6 +1409,8 @@ Depending on the {\tt \{\}} annotation, different definition
 mechanisms are used by {\tt Function}. More precise description
 given below.
 
+
+
 \subsubsection{\tt Function {\ident} {\binder$_1$}\ldots{\binder$_n$}
  : type$_0$ := \term$_0$.
 \comindex{Function}
@@ -1433,7 +1457,7 @@ the following:
 \item {\tt \{wf} \term$_1$ \ident$_0${\tt\}} with \ident$_0$ being
       the decreasing argument and \term$_1$ an ordering relation on
       the type of \ident$_0$ (i.e. of type T$_{\ident_0}$
-      $\rightarrow$ T$_{\ident_0}$ $\rightarrow$ {\tt Prop}) for which
+      $\to$ T$_{\ident_0}$ $\to$ {\tt Prop}) for which
       the decreasing argument decreases at each recursive call of
       \term$_0$. The order must be well founded. parameters of the
       function are bound in  \term$_0$.
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index b689a8f2d..cf1099169 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1387,19 +1387,29 @@ Qed.
 \end{Variants}
 
 
-\subsection{\tt functional induction \ident\ \term$_1$ \dots\ \term$_n$.
+\subsection{\tt functional induction (\ident\ \term$_1$ \dots\ \term$_n$).
 \tacindex{functional induction}
 \label{FunInduction}}
 
-The \emph{experimental} tactic \texttt{functional induction}
-performs case analysis and induction following the definition of
-a (not mutually recursive) function. It makes use of principle
-generated by \texttt{Function}\ref{Function}.
+The \emph{experimental} tactic \texttt{functional induction} performs
+case analysis and induction following the definition of a function. It
+makes use of the principle \ident\_ind generated by \texttt{Function}
+(section~\ref{Function}) or \texttt{Functional Scheme}
+(section~\ref{FunScheme}).
 
 \begin{coq_eval}
 Reset Initial.
 \end{coq_eval}
 \begin{coq_example}
+Function minus (n m : nat) {struct n} : nat :=
+match n with
+  | 0 => 0
+  | S k => match m with
+           | 0 => S k
+           | S l => minus k l
+           end
+  end.
+
 Lemma le_minus : forall n m:nat, (n - m <= n).
 intros n m.
 functional induction minus n m; simpl; auto.
@@ -1408,22 +1418,47 @@ functional induction minus n m; simpl; auto.
 Qed.
 \end{coq_example*}
 
-\texttt{functional induction} is a shorthand for the more general
-command \texttt{Functional Scheme} which builds induction
-principles following the recursive structure of (possibly
-mutually recursive)
-functions. \SeeAlso{\ref{FunScheme-examples}} for the difference
-between using one or the other.
+\Rem Arguments of the function must be given, including the implicit
+ones.
+
+\Rem Parenthesis over \ident \dots \term$_n$ are mandatory.
+
+\Rem \texttt{functional induction (f x1 x2 x3)} is actually a shorthand for
+\texttt{induction x1 x2 x3 (f x1 x2 x3) using f\_ind}. \texttt{f\_ind}
+being an induction scheme computed by the \texttt{Function} command
+(section~\ref{Function}). Therefore \texttt{functional induction} may
+fail if the induction scheme (\texttt{f\_ind}) is not defined. See also
+section~\ref{Function} for the function terms accepted by
+\texttt{Function}.
+
+\SeeAlso{\ref{Function},\ref{FunScheme},\ref{FunScheme-examples}}
+
+\ErrMsg 
+
+\errindex{The reference \ident\_ind was not found in the current
+environment}
 
-\Rem \texttt{functional induction} may fail on functions built by
-tactics. In particular case analysis of a function are considered
-only if they are not inside an application.
+~
 
-\Rem Arguments of the function must be given, including the
-implicit ones. If the function is recursive, arguments must be
-variables, otherwise they may be any term.
+\errindex{Not the right number of induction arguments}
+ 
+
+\begin{Variants}
+\item {\tt functional induction (\ident\ \term$_1$ \dots\ \term$_n$)
+    with {\term$_1$} \dots {\term$_n$}}
 
-\SeeAlso{\ref{FunScheme},\ref{FunScheme-examples}}
+  Similar to \texttt{Induction} and \texttt{elim}
+  (section~\ref{Tac-induction}), allows to give explicitly the values
+  of dependent premises of the elimination scheme, including
+  \emph{predicates} for mutual induction when \ident is mutually
+  recursive.
+
+\item {\tt functional induction (\ident\ \term$_1$ \dots\ \term$_n$)
+    with {\vref$_1$} := {\term$_1$} \dots\ {\vref$_n$} := {\term$_n$}}
+
+  Similar to \texttt{induction} and \texttt{elim}
+  (section~\ref{Tac-induction}).
+\end{Variants}
 
 \section{Equality}
 
diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex
index ecd54f449..c25c275d6 100644
--- a/doc/refman/RefMan-tacex.tex
+++ b/doc/refman/RefMan-tacex.tex
@@ -706,7 +706,7 @@ theorem \texttt{simplify\_ok: (f:formula)(interp\_f (simplify f)) ->
 \end{verbatim}
 But there is a problem with leafs: in the example above one cannot
 write a function that implements, for example, the logical simplifications 
-$A \wedge A \ra A$ or $A \wedge \neg A \ra \texttt{False}$. This is
+$A \land A \ra A$ or $A \land \lnot A \ra \texttt{False}$. This is
 because the \Prop{} is impredicative.
 
 It is better to use that type of formulas:
@@ -724,7 +724,7 @@ Inductive formula : Set :=
 \end{coq_example*}
 
 \texttt{index} is defined in module \texttt{quote}. Equality on that
-type is decidable so we are able to simplify $A \wedge A$ into $A$ at
+type is decidable so we are able to simplify $A \land A$ into $A$ at
 the abstract level. 
 
 When there are variables, there are bindings, and \texttt{quote}