Relecture/nettoyage chapitre Gallina; déplacement section Function

dans extensions de Gallina. Divers. (report revisions 9614 et 9594 de
la branche 8.1 vers le trunk)



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

1 files changed, 198 insertions, 1 deletions

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index e0acef5503..e05183ce91 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -214,7 +214,7 @@ To deactivate the printing of projections, use
 {\tt Unset Printing Projections}.
 
 
-\section{Variants and extensions of {\tt match}
+\section{Variants and extensions of {\mbox{\tt match}}
 \label{Extensions-of-match}
 \index{match@{\tt match\ldots with\ldots end}}}
 
@@ -235,6 +235,7 @@ section~\ref{SetPrintingMatching}).
 \SeeAlso chapter \ref{Mult-match-full}.
 
 \subsection{Pattern-matching on boolean values: the {\tt if} expression
+\label{if-then-else}
 \index{if@{\tt if ... then ... else}}}
 
 For inductive types with exactly two constructors and for
@@ -555,6 +556,202 @@ Print fst.
 %% Check id.
 %% \end{coq_example}
 
+\section{Advanced recursive functions}
+
+The \emph{experimental} command 
+\begin{center}
+   \texttt{Function {\ident} {\binder$_1$}\ldots{\binder$_n$}
+     \{decrease\_annot\} : type$_0$ := \term$_0$}
+   \comindex{Function}
+   \label{Function}
+\end{center}
+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.  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
+necessary be \emph{structurally} decreasing. The point of the {\tt
+  \{\}} annotation is to name the decreasing argument \emph{and} to
+describe which kind of decreasing criteria must be used to ensure
+termination of recursive calls.
+
+The {\tt Function} construction enjoys also the {\tt with} extension
+to define mutually recursive definitions. However, this feature does
+not work for non structural recursive functions. % VRAI??
+
+See the documentation of {\tt functional induction} (section
+\ref{FunInduction}) and {\tt Functional Scheme} (section
+\ref{FunScheme} and \ref{FunScheme-examples}) for how to use the 
+induction principle to easily reason about the function.
+
+\noindent {\bf Remark: } To obtain the right principle, it is better
+to put rigid parameters of the function as first arguments. For
+example it is better to define plus like this:
+
+\begin{coq_example*}
+Function plus (m n : nat) {struct n} : nat :=
+  match n with
+  | 0 => m
+  | S p => S (plus m p)
+  end.
+\end{coq_example*}
+\noindent than like this:
+\begin{coq_eval}
+Reset plus.
+\end{coq_eval}
+\begin{coq_example*}
+Function plus (n m : nat) {struct n} : nat :=
+  match n with
+  | 0 => m
+  | S p => S (plus p m)
+  end.
+\end{coq_example*}
+
+\paragraph{Limitations}
+\label{sec:Function-limitations}
+\term$_0$ must be build as a \emph{pure pattern-matching tree}
+(\texttt{match...with}) with applications only \emph{at the end} of
+each branch.  For now dependent cases are not treated.
+
+
+
+\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}
+
+\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. Only
+  the ident is defined, the induction 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}
+
+\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}}
+
+Depending on the {\tt \{$\ldots$\}} annotation, different definition
+mechanisms are used by {\tt Function}. More precise description
+given below.
+
+\begin{Variants}
+\item \texttt{ Function {\ident} {\binder$_1$}\ldots{\binder$_n$}
+    : type$_0$ := \term$_0$}
+
+  Defines the not recursive function \ident\ as if declared with
+  \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}.  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$ :=
+    \term$_0$}
+\item \texttt{Function {\ident} {\binder$_1$}\ldots{\binder$_n$}
+ {\tt \{}{\tt wf \term$_1$} \ident$_0${\tt\}} : type$_0$ := \term$_0$}
+
+Defines a recursive function by well founded recursion. \textbf{The
+module \texttt{Recdef} of the standard library must be loaded for this
+feature}. The {\tt \{\}} annotation is mandatory and must be one of
+the following:
+\begin{itemize}
+\item {\tt \{measure} \term$_1$ \ident$_0${\tt\}} with \ident$_0$
+      being the decreasing argument and \term$_1$ being a function
+      from type of \ident$_0$ to \texttt{nat} for which value on the
+      decreasing argument decreases (for the {\tt lt} order on {\tt
+      nat}) at each recursive call of \term$_0$, parameters of the
+      function are bound in  \term$_0$;
+\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}$
+      $\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$.
+\end{itemize} 
+
+Depending on the annotation, the user is left with some proof
+obligations that will be used to define the function. These proofs
+are: proofs that each recursive call is actually decreasing with
+respect to the given criteria, and (if the criteria is \texttt{wf}) a
+proof that the ordering relation is well founded.
+
+%Completer sur measure et wf
+
+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}
+
+
+
+%Complete!!
+The way this recursive function is defined is the subject of several
+papers by Yves Bertot and Antonia Balaa on one hand and  Gilles Barthe, Julien Forest, David Pichardie and Vlad Rusu on the other hand.
+
+%Exemples ok ici
+
+\bigskip
+
+\noindent {\bf Remark: } Proof obligations are presented as several
+subgoals belonging to a Lemma {\ident}{\tt\_tcc}. % These subgoals are independent which means that in order to
+% abort them you will have to abort each separately.
+
+
+
+%The decreasing argument cannot be dependent of another??
+
+%Exemples faux ici
+\end{Variants}
+
+
 \section{Section mechanism
 \index{Sections}
 \label{Section}}