Updating the doc about Function and co

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

3 files changed, 159 insertions, 97 deletions

diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index 8f79af2be1..6fcb219072 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -1362,7 +1362,7 @@ can be seen as a generalization of {\tt Fixpoint}.  It is actually a
 wrapper for several ways of defining a function \emph{and other useful
   related objects}, namely: an induction principle that reflects the
 recursive structure of the function (see \ref{FunInduction}), and its
-fixpoint equality (not always, see below).  The meaning of this
+fixpoint equality.  The meaning of this
 declaration is to define a function {\it ident}, similarly to {\tt
   Fixpoint}. Like in {\tt Fixpoint}, the decreasing argument must be
 given (unless the function is not recursive), but it must not
@@ -1406,40 +1406,43 @@ Function plus (n m : nat) {struct n} : nat :=
 \paragraph{Limitations}
 \label{sec:Function-limitations}
 \term$_0$ must be build as a \emph{pure pattern-matching tree}
-(\texttt{match...with}) with $\lambda$-abstractions and applications only
-\emph{at the end} of each branch.  For now dependent cases are not
-treated.
+(\texttt{match...with}) with applications only \emph{at the end} of
+each branch.  For now dependent cases are not treated.
 
-\paragraph{Difference with \texttt{Functional Scheme}} 
-There is a difference between obtaining an induction scheme for a
-function by using \texttt{Function} (section~\ref{Function}) and
-by using \texttt{Functional Scheme} after a usual definition using
-\texttt{Fixpoint} or \texttt{Definition}. Indeed \texttt{Function}
-generally produces smaller principles, closer to the definition
-written by the user. This is because \texttt{Functional Scheme} works
-by analyzing the term \texttt{div2} after the compilation of pattern
-matching into exhaustive expanded ones, whereas \texttt{Function}
-analyzes the pseudo-term \emph{before} pattern matching expansion.
 
 
-\ErrMsg 
+\begin{ErrMsgs}
+\item \errindex{The recursive argument must be specified}
+\item \errindex{No argument name \ident}
+\item \errindex{Cannot use mutual definition with well-founded
+    recursion or measure}
 
-\errindex{while trying to define Inductive R\_\ident ...}
+\item \errindex{Cannot define graph for \ident\dots} (warning)
 
-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.
+  The generation of the graph relation \texttt{(R\_\ident)} used to
+  compute the induction scheme of \ident\ raised a typing error. Only
+  the ident is defined, the induction scheme will not be generated.
 
-This error happens generally when: 
+  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}
+  \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}
+
+\item \errindex{Cannot define principle(s) for \ident\dots} (warning)
+
+  The generation of the graph relation \texttt{(R\_\ident)} succeeded
+  but the induction principle could not be built. Only the ident is
+  defined. Please report.
+
+\item \errindex{Cannot built inversion information} (warning)
 
+  \texttt{functional inversion} will not be available for the
+  function.
+\end{ErrMsgs}
 
 
 \SeeAlso{\ref{FunScheme},\ref{FunScheme-examples},\ref{FunInduction}}
@@ -1453,20 +1456,27 @@ given below.
     : type$_0$ := \term$_0$}
 
   Defines the not recursive function \ident\ as if declared with
-  \texttt{Definition}.  Three elimination schemes {\tt\ident\_rect},
-  {\tt\ident\_rec} and {\tt\ident\_ind} are generated (see the
-  documentation of {\tt Inductive} \ref{Inductive}), which reflect the
-  pattern matching structure of \term$_0$.
-
+  \texttt{Definition}.  Moreover the following are defined:
+
+  \begin{itemize}
+  \item {\tt\ident\_rect}, {\tt\ident\_rec} and {\tt\ident\_ind},
+    which reflect the pattern matching structure of \term$_0$ (see the
+    documentation of {\tt Inductive} \ref{Inductive});
+  \item The inductive \texttt{R\_\ident} corresponding to the graph of
+    \ident\ (silently);
+  \item \texttt{\ident\_complete} and \texttt{\ident\_correct} which are
+    inversion information linking the function and its graph.
+  \end{itemize}
 \item \texttt{Function {\ident} {\binder$_1$}\ldots{\binder$_n$}
     {\tt \{}{\tt struct} \ident$_0${\tt\}} : type$_0$ := \term$_0$}
   
   Defines the structural recursive function \ident\ as if declared
-  with \texttt{Fixpoint}.  Three induction schemes {\tt\ident\_rect},
-  {\tt\ident\_rec} and {\tt\ident\_ind} are generated (see the
-  documentation of {\tt Inductive} \ref{Inductive}), which reflect the
-  recursive structure of \term$_0$. When there is only one parameter,
-  {\tt \{struct} \ident$_0${\tt\}} can be omitted.
+  with \texttt{Fixpoint}.  Moreover the following are defined:
+
+  \begin{itemize}
+  \item The same objects as above;
+  \item The fixpoint equation of \ident: \texttt{\ident\_equation}.
+  \end{itemize}
   
 \item \texttt{Function {\ident} {\binder$_1$}\ldots{\binder$_n$} {\tt
       \{}{\tt measure \term$_1$} \ident$_0${\tt\}} : type$_0$ :=
@@ -1502,12 +1512,16 @@ proof that the ordering relation is well founded.
 
 %Completer sur measure et wf
 
-The fixpoint equality  \texttt{\ident\_equation}, which is not trivial
-to prove in this case, is automatically generated and proved, together
-with three  induction schemes {\tt\ident\_rect},  {\tt\ident\_rec} and
-{\tt\ident\_ind} as explained above  (see  the   documentation  of  {\tt
-  Inductive} \ref{Inductive}), which  reflect the recursive structure
-of \term$_0$.
+Once proof obligations are discharged, the following objects are
+defined:
+
+\begin{itemize}
+\item The same objects as with the \texttt{struct};
+\item The lemma \texttt{\ident\_tcc} which collects all proof
+  obligations in one property;
+\item The lemmas \texttt{\ident\_terminate} and \texttt{\ident\_F}
+  which is needed to be inlined during extraction of \ident.
+\end{itemize}
 
 
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 10e32675b1..8b3c6cbdb6 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1452,7 +1452,7 @@ Qed.
 \end{Variants}
 
 
-\subsection{\tt functional induction (\ident\ \term$_1$ \dots\ \term$_n$).
+\subsection{\tt functional induction (\qualid\ \term$_1$ \dots\ \term$_n$).
 \tacindex{functional induction}
 \label{FunInduction}}
 
@@ -1460,8 +1460,7 @@ The \emph{experimental} tactic \texttt{functional induction} performs
 case analysis and induction following the definition of a function. It
 makes use of a principle generated by \texttt{Function}
 (section~\ref{Function}) or \texttt{Functional Scheme}
-(section~\ref{FunScheme}). This principle is named \ident\_ind by
-default but you can give it explicitly, see variants below.
+(section~\ref{FunScheme}).
 
 \begin{coq_eval}
 Reset Initial.
@@ -1477,22 +1476,22 @@ functional induction (minus n m); simpl; auto.
 Qed.
 \end{coq_example*}
 
-\Rem \texttt{(\ident\ \term$_1$ \dots\ \term$_n$)} must be a correct
-full application of \ident. In particular, the rules for implicit
-arguments are the same as usual. For example use \texttt{@\ident} if
+\Rem \texttt{(\qualid\ \term$_1$ \dots\ \term$_n$)} must be a correct
+full application of \qualid. In particular, the rules for implicit
+arguments are the same as usual. For example use \texttt{@\qualid} if
 you want to write implicit arguments explicitly.
 
-\Rem Parenthesis over \ident \dots \term$_n$ are not mandatory, but if
-there are not written then implicit arguments must be given.
+\Rem Parenthesis over \qualid \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} (section~\ref{Function}) or \texttt{Functional
-  Scheme} (section~\ref{FunScheme}) command . 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}.
+\Rem \texttt{functional induction (f x1 x2 x3)} is actually a wrapper
+for \texttt{induction x1 x2 x3 (f x1 x2 x3) using \qualid} followed by
+a cleaning phase, where $\qualid$ is the induction principle
+registered for $f$ (by the \texttt{Function} (section~\ref{Function})
+or \texttt{Functional Scheme} (section~\ref{FunScheme}) command)
+corresponding to the sort of the goal.  Therefore \texttt{functional
+  induction} may fail if the induction scheme (\texttt{\qualid}) is
+not defined. See also section~\ref{Function} for the function terms
+accepted by \texttt{Function}.
 
 \Rem There is a difference between obtaining an induction scheme for a
 function by using \texttt{Function} (section~\ref{Function}) and by
@@ -1500,36 +1499,42 @@ using \texttt{Functional Scheme} after a normal definition using
 \texttt{Fixpoint} or \texttt{Definition}. See \ref{Function} for
 details.
 
-\SeeAlso{\ref{Function},\ref{FunScheme},\ref{FunScheme-examples}}
+\SeeAlso{\ref{Function},\ref{FunScheme},\ref{FunScheme-examples},
+  \ref{sec:functional-inversion}}
 
-\ErrMsg 
-
-\errindex{The reference \ident\_ind was not found in the current
-environment}
+\begin{ErrMsgs}
+\item \errindex{Cannot find induction information on \qualid}
 
-~
+  ~
 
-\errindex{Not the right number of induction arguments}
- 
+\item \errindex{Not the right number of induction arguments}
+\end{ErrMsgs}
 
 \begin{Variants}
-\item {\tt functional induction (\ident\ \term$_1$ \dots\ \term$_n$)
+\item {\tt functional induction (\qualid\ \term$_1$ \dots\ \term$_n$)
    using \term$_{m+1}$ with {\term$_{n+1}$} \dots {\term$_m$}}
 
  Similar to \texttt{Induction} and \texttt{elim}
  (section~\ref{Tac-induction}), allows to give explicitly the
  induction principle and the values of dependent premises of the
  elimination scheme, including \emph{predicates} for mutual induction
- when \ident is mutually recursive.
+ when \qualid is mutually recursive.
 
-\item {\tt functional induction (\ident\ \term$_1$ \dots\ \term$_n$)
+\item {\tt functional induction (\qualid\ \term$_1$ \dots\ \term$_n$)
     using \term$_{m+1}$ with {\vref$_1$} := {\term$_{n+1}$} \dots\
     {\vref$_m$} := {\term$_n$}}
 
   Similar to \texttt{induction} and \texttt{elim}
   (section~\ref{Tac-induction}).
+
+\item All previous variants can be extended by the usual \texttt{as
+    \intropattern} construction, similarly for example to
+  \texttt{induction} and \texttt{elim} (section~\ref{Tac-induction}).
+    
 \end{Variants}
 
+
+
 \section{Equality}
 
 These tactics use the equality {\tt eq:forall A:Type, A->A->Prop}
@@ -2167,6 +2172,42 @@ the instance with the tactic {\tt inversion}.
 
 \SeeAlso \ref{inversion-examples} for examples
 
+
+
+\subsection{\tt functional inversion \ident}
+\label{sec:functional-inversion}
+
+\texttt{functional inversion} is a \emph{highly} experimental tactic
+which performs inversion on hypothesis \ident\ of the form
+\texttt{\qualid\ \term$_1$\dots\term$_n$\ = \term} or \texttt{\term\ =
+  \qualid\ \term$_1$\dots\term$_n$} where \qualid\ must have been
+defined using \texttt{Function} (section~\ref{Function}).
+
+\begin{ErrMsgs}
+\item \errindex{Hypothesis \ident must contain at least one Function}
+\item \errindex{Cannot find inversion information for hypothesis \ident}
+  This error may be raised when  some inversion lemma failed to be
+  generated by Function.
+\end{ErrMsgs}
+
+\begin{Variants}
+\item {\tt functional inversion \num}
+
+  This does the same thing as \texttt{intros until \num} then
+  \texttt{functional inversion \ident} where {\ident} is the
+  identifier for the last introduced hypothesis.
+\item {\tt functional inversion \ident\ \qualid}\\
+  {\tt functional inversion \num\ \qualid}
+
+  In case the hypothesis \ident (or \num) has a type of the form
+  \texttt{\qualid$_1$\ \term$_1$\dots\term$_n$\ =\qualid$_2$\
+    \term$_{n+1}$\dots\term$_{n+m}$} where \qualid$_1$ and \qualid$_2$
+  are valid candidates to functional inversion, this variant allows to
+  chose which must be inverted.
+\end{Variants}
+
+
+
 \subsection{\tt quote \ident
 \tacindex{quote}
 \index{2-level approach}}
@@ -3254,27 +3295,25 @@ tool for generating automatically induction principles
 corresponding to (possibly mutually recursive) functions.  Its
 syntax follows the schema:
 \begin{tabbing}
-{\tt Functional Scheme {\ident$_i$} := Induction for
-    \ident'$_i$ with \ident'$_1$ \dots\ \ident'$_m$.}
+{\tt Functional Scheme {\ident$_1$} := Induction for \ident'$_1$ Sort {\sort$_1$} \\
+  with\\
+  \mbox{}\hspace{0.1cm} \dots\ \\
+        with {\ident$_m$} := Induction for {\ident'$_m$} Sort
+        {\sort$_m$}}
 \end{tabbing}  
-\ident'$_1$ \dots\ \ident'$_m$ are the names of mutually recursive
-functions (they must be in the same order as when they were defined),
-\ident'$_i$ being one of them. This command generates the induction
-principle \ident$_i$, following the recursive structure and case
-analyses of the functions \ident'$_1$ \dots\ \ident'$_m$, and having
-\ident'$_i$ as entry point.
+\ident'$_1$ \dots\ \ident'$_m$ are different mutually defined function
+names (they must be in the same order as when they were defined).
+This command generates the induction principles
+\ident$_1$\dots\ident$_m$, following the recursive structure and case
+analyses of the functions \ident'$_1$ \dots\ \ident'$_m$.
 
-\begin{Variants}
-\item {\tt Functional Scheme {\ident$_1$} := Induction for \ident'$_1$.}
-  
-  This command is a shortcut for:
-  \begin{tabbing} 
-  {\tt Functional Scheme {\ident$_1$} := Induction for
-    \ident'$_1$ with \ident'$_1$.}
-\end{tabbing}
 
-This variant can be used for non mutually recursive functions only.
-\end{Variants}
+\paragraph{\texttt{Functional Scheme}} 
+There is a difference between obtaining an induction scheme by using
+\texttt{Functional Scheme} on a function defined by \texttt{Function}
+or not. Indeed \texttt{Function} generally produces smaller
+principles, closer to the definition written by the user.
+
 
 \SeeAlso Section~\ref{FunScheme-examples}
 
diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex
index 57155d21c9..0aee431785 100644
--- a/doc/refman/RefMan-tacex.tex
+++ b/doc/refman/RefMan-tacex.tex
@@ -373,10 +373,11 @@ with forest : Set :=
 \end{coq_example*}
 
 We define the function \texttt{tree\_size} that computes the size
-of a tree or a forest.
+of a tree or a forest. Note that we use \texttt{Function} which
+generally produces better principles.
 
 \begin{coq_example*}                
-Fixpoint tree_size (t:tree) : nat :=
+Function tree_size (t:tree) : nat :=
   match t with
   | node A f => S (forest_size f)
   end
@@ -387,23 +388,31 @@ Fixpoint tree_size (t:tree) : nat :=
   end.
 \end{coq_example*}
 
-The definition of principle of mutual induction following the
-recursive structure of \texttt{tree\_size} is defined by the
-command:
+Remark: \texttt{Function} generates itself non mutual induction
+principles {\tt tree\_size\_ind} and {\tt forest\_size\_ind}:
+
+\begin{coq_example}
+Check tree_size_ind.
+\end{coq_example}
+
+The definition of mutual induction principles following the recursive
+structure of \texttt{tree\_size} and \texttt{forest\_size} is defined
+by the command:
 
 \begin{coq_example*}
-Functional Scheme tree_size_ind := Induction for tree_size Sort Prop
-with forest_size_ind := Induction for forest_size Sort Prop.
+Functional Scheme tree_size_ind2 := Induction for tree_size Sort Prop
+with forest_size_ind2 := Induction for forest_size Sort Prop.
 \end{coq_example*}
 
-You may now look at the type of {\tt tree\_size\_ind}:
+You may now look at the type of {\tt tree\_size\_ind2}:
 
 \begin{coq_example}
-Check tree_size_ind.
+Check tree_size_ind2.
 \end{coq_example}
 
 
 
+
 \section{{\tt inversion}}
 \tacindex{inversion}
 \label{inversion-examples}