From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Tue, 21 Nov 2006 21:38:49 +0000
Subject: Imported Upstream version 8.1~gamma

---
 doc/refman/RefMan-gal.tex | 104 ++++++++++++++++++++++++++--------------------
 1 file changed, 59 insertions(+), 45 deletions(-)

(limited to 'doc/refman/RefMan-gal.tex')

diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index e7b825d7..1c258b20 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,18 +1512,22 @@ 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}
 
 
 
 %Complete!!
 The way this recursive function is defined is the subject of several
-papers by Yves Bertot, Julien Forest, David Pichardie.
+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
 
@@ -1706,4 +1720,4 @@ To be able to unfold a proof, you should end the proof by {\tt Defined}
 % TeX-master: "Reference-Manual"
 % End: 
 
-% $Id: RefMan-gal.tex 9040 2006-07-11 18:06:49Z notin $ 
+% $Id: RefMan-gal.tex 9127 2006-09-07 15:47:14Z courtieu $ 
-- 
cgit v1.2.3

