From e978da8c41d8a3c19a29036d9c569fbe2a4616b0 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 16 Jun 2006 14:41:51 +0000
Subject: Imported Upstream version 8.0pl3+8.1beta

---
 doc/refman/RefMan-gal.tex | 278 ++++++++++++++++++++++++++++++++++++++++++----
 1 file changed, 257 insertions(+), 21 deletions(-)

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

diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index ce2b75b8..2214864a 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -851,7 +851,8 @@ The type {\tt nat} is defined as the least \verb:Set: containing {\tt
   O} and closed by the {\tt S} constructor. The constants {\tt nat},
 {\tt O} and {\tt S} are added to the environment.
 
-Now let us have a look at the elimination principles. They are three :
+Now let us have a look at the elimination principles. They are three
+of them:
 {\tt nat\_ind}, {\tt nat\_rec} and {\tt nat\_rect}.  The type of {\tt
   nat\_ind} is:
 \begin{coq_example}
@@ -880,8 +881,9 @@ Reset Initial.
 Inductive nat : Set := O | S (_:nat).
 \end{coq_example*}
 In the case where inductive types have no annotations (next section
-gives an example of such annotations), the positivity condition
-implies that a constructor can be defined by only giving the type of
+gives an example of such annotations), 
+%the positivity condition implies that 
+a constructor can be defined by only giving the type of
 its arguments.
 \end{Variants}
 
@@ -910,13 +912,13 @@ Check even_ind.
 \end{coq_example}
 
 From a mathematical point of view it asserts that the natural numbers
-satisfying the predicate {\tt even} are exactly the naturals satisfying
-the clauses {\tt even\_0} or {\tt even\_SS}. This is why, when we want
-to prove any predicate {\tt P} over elements of {\tt even}, it is
-enough to prove it for {\tt O} and to prove that if any natural number
-{\tt n} satisfies {\tt P} its double successor {\tt (S (S n))}
-satisfies also {\tt P}. This is indeed analogous to the structural
-induction principle we got for {\tt nat}.
+satisfying the predicate {\tt even} are exactly in the smallest set of
+naturals satisfying the clauses {\tt even\_0} or {\tt even\_SS}. This
+is why, when we want to prove any predicate {\tt P} over elements of
+{\tt even}, it is enough to prove it for {\tt O} and to prove that if
+any natural number {\tt n} satisfies {\tt P} its double successor {\tt
+  (S (S n))} satisfies also {\tt P}. This is indeed analogous to the
+structural induction principle we got for {\tt nat}.
 
 \begin{ErrMsgs}
 \item \errindex{Non strictly positive occurrence of {\ident} in {\type}}
@@ -925,11 +927,17 @@ built from {\ident}}
 \end{ErrMsgs}
 
 \subsubsection{Parameterized inductive types}
-
-Inductive types may be parameterized. Parameters differ from inductive
-type annotations in the fact that recursive invokations of inductive
-types must always be done with the same values of parameters as its
-specification.
+In the previous example, each constructor introduces a
+different instance of the predicate {\tt even}. In some cases, 
+all the constructors introduces the same generic instance of the
+inductive definition, in which case, instead of an annotation, we use
+a context of parameters which are binders shared by all the
+constructors of the definition.
+
+% Inductive types may be parameterized. Parameters differ from inductive
+% type annotations in the fact that recursive invokations of inductive
+% types must always be done with the same values of parameters as its
+% specification.
 
 The general scheme is:
 \begin{center}
@@ -937,6 +945,11 @@ The general scheme is:
     {\ident$_1$}: {\term$_1$} | {\ldots} | {\ident$_n$}: \term$_n$
 {\tt .}
 \end{center}
+Parameters differ from inductive type annotations in the fact that the
+conclusion of each type of constructor {\term$_i$} invoke the inductive
+type with the same values of parameters as its specification.
+
+
 
 A typical example is the definition of polymorphic lists:
 \begin{coq_example*}
@@ -972,7 +985,39 @@ arguments of the constructors rather than their full type.
 \item \errindex{The {\num}th argument of {\ident} must be {\ident'} in {\type}}
 \end{ErrMsgs}
 
-\SeeAlso Sections~\ref{Cic-inductive-definitions} and~\ref{elim}.
+\paragraph{New from \Coq{} V8.1} The condition on parameters for
+inductive definitions has been relaxed since \Coq{} V8.1. It is now
+possible in the type of a constructor, to invoke recursively the
+inductive definition on an argument which is not the parameter itself.
+
+One can define~:
+\begin{coq_example}
+Inductive list2 (A:Set) : Set :=
+  | nil2 : list2 A
+  | cons2 : A -> list2 (A*A) -> list2 A.
+\end{coq_example}
+\begin{coq_eval}
+Reset list2.
+\end{coq_eval}
+that can also be written by specifying only the type of the arguments:
+\begin{coq_example*}
+Inductive list2 (A:Set) : Set := nil2 | cons2 (_:A) (_:list2 (A*A)).
+\end{coq_example*}
+But the following definition will give an error:
+\begin{coq_example}
+Inductive listw (A:Set) : Set :=
+  | nilw : listw (A*A)
+  | consw : A -> listw (A*A) -> listw (A*A).
+\end{coq_example}
+Because the conclusion of the type of constructors should be {\tt
+  listw A} in both cases. 
+
+A parameterized inductive definition can be defined using
+annotations instead of parameters but it will sometimes give a
+different (bigger) sort for the inductive definition and will produce
+a less convenient rule for case elimination.
+
+\SeeAlso Sections~\ref{Cic-inductive-definitions} and~\ref{Tac-induction}.
 
 
 \subsubsection{Mutually defined inductive types
@@ -1091,7 +1136,7 @@ definition.
 
 The objects of an inductive type are well-founded with respect to the
 constructors of the type. In other words, such objects contain only a
-{\it finite} number constructors. Co-inductive types arise from
+{\it finite} number of constructors. Co-inductive types arise from
 relaxing this condition, and admitting types whose objects contain an
 infinity of constructors. Infinite objects are introduced by a
 non-ending (but effective) process of construction, defined in terms
@@ -1130,7 +1175,7 @@ CoInductive EqSt : Stream -> Stream -> Prop :=
 \end{coq_example}
 
 In order to prove the extensionally equality of two streams $s_1$ and
-$s_2$ we have to construct and infinite proof of equality, that is,
+$s_2$ we have to construct an infinite proof of equality, that is,
 an infinite object of type $(\texttt{EqSt}\;s_1\;s_2)$. We will see
 how to introduce infinite objects in Section~\ref{CoFixpoint}.
 
@@ -1146,8 +1191,9 @@ how to introduce infinite objects in Section~\ref{CoFixpoint}.
 
 This command allows to define inductive objects using a fixed point
 construction. The meaning of this declaration is to define {\it ident}
-a recursive function with arguments specified by
-{\binder$_1$}\ldots{\binder$_n$} such that {\it ident} applied to
+a recursive function with arguments specified by the binders in
+\params{} % {\binder$_1$}\ldots{\binder$_n$} 
+such that {\it ident} applied to
 arguments corresponding to these binders has type \type$_0$, and is
 equivalent to the expression \term$_0$. The type of the {\ident} is
 consequently {\tt forall {\params} {\tt,} \type$_0$}
@@ -1277,6 +1323,196 @@ Fixpoint tree_size (t:tree) : nat :=
 A generic command {\tt Scheme} is useful to build automatically various
 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}
+
+This \emph{experimental} command 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 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 $\lambda$-abstractions and 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 
+
+\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}}
+
+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}
+}
+
+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$.
+
+
+\subsubsection{\tt Function {\ident} {\binder$_1$}\ldots{\binder$_n$}
+ {\tt \{}{\tt struct} \ident$_0${\tt\}} : type$_0$ := \term$_0$.
+\comindex{Function}
+}
+
+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.
+
+\subsubsection{\tt Function {\ident} {\binder$_1$}\ldots{\binder$_n$}
+ {\tt \{}{\tt measure \term$_1$} \ident$_0${\tt\}} : type$_0$ := \term$_0$.
+\comindex{Function}}
+
+\subsubsection{\tt Function {\ident} {\binder$_1$}\ldots{\binder$_n$}
+ {\tt \{}{\tt wf \term$_1$} \ident$_0${\tt\}} : type$_0$ := \term$_0$.
+\comindex{Function}}
+
+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
+
+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$.
+
+
+
+%Complete!!
+The way this recursive function is defined is the subject of several
+papers by Yves Bertot, Julien Forest, David Pichardie.
+
+%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
+
+
+
+
+
 \subsubsection{\tt CoFixpoint {\ident} : \type$_0$ := \term$_0$.
 \comindex{CoFixpoint}
 \label{CoFixpoint}}
@@ -1448,4 +1684,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 8606 2006-02-23 13:58:10Z herbelin $ 
+% $Id: RefMan-gal.tex 8915 2006-06-07 15:17:13Z courtieu $ 
-- 
cgit v1.2.3

