Changements sur Functional xxx. Plus précis et plus exact.

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

3 files changed, 65 insertions, 55 deletions

diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index be80e7eb7..584485108 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -1349,8 +1349,8 @@ 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-examples}) for how to use the induction principle to
-easily reason about the function.
+\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
@@ -1382,6 +1382,17 @@ Function plus (n m : nat) {struct n} : nat :=
 \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 the \texttt{Function} (section~\ref{Function}) and
+by using Functional Scheme after a normal 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 
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index cf1099169..1663b975a 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1393,43 +1393,47 @@ Qed.
 
 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}
+makes use of a principle generated by \texttt{Function}
 (section~\ref{Function}) or \texttt{Functional Scheme}
-(section~\ref{FunScheme}).
+(section~\ref{FunScheme}). This principle is named \ident\_ind by
+default but you can give it explicitly, see variants below.
 
 \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.
+Functional Scheme minus_ind := Induction for minus Sort Prop.
 
 Lemma le_minus : forall n m:nat, (n - m <= n).
 intros n m.
-functional induction minus n m; simpl; auto.
+functional induction (minus n m); simpl; auto.
 \end{coq_example}
 \begin{coq_example*}
 Qed.
 \end{coq_example*}
 
-\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}.
+\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
+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 \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 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 normal definition using
+\texttt{Fixpoint} or \texttt{Definition}. See \ref{Function} for
+details.
 
 \SeeAlso{\ref{Function},\ref{FunScheme},\ref{FunScheme-examples}}
 
@@ -1445,16 +1449,17 @@ environment}
 
 \begin{Variants}
 \item {\tt functional induction (\ident\ \term$_1$ \dots\ \term$_n$)
-    with {\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 values
-  of dependent premises of the elimination scheme, including
-  \emph{predicates} for mutual induction when \ident is mutually
-  recursive.
+ 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.
 
 \item {\tt functional induction (\ident\ \term$_1$ \dots\ \term$_n$)
-    with {\vref$_1$} := {\term$_1$} \dots\ {\vref$_n$} := {\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}).
diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex
index c25c275d6..57155d21c 100644
--- a/doc/refman/RefMan-tacex.tex
+++ b/doc/refman/RefMan-tacex.tex
@@ -289,10 +289,8 @@ Require Import Arith.
 Fixpoint div2 (n:nat) : nat :=
   match n with
   | O => 0
-  | S n0 => match n0 with
-            | O => 0
-            | S n' => S (div2 n')
-            end
+  | S O => 0
+  | S (S n') => S (div2 n')
   end.
 \end{coq_example*}
 
@@ -300,7 +298,7 @@ The definition of a principle of induction corresponding to the
 recursive structure of \texttt{div2} is defined by the command:
 
 \begin{coq_example}
-Functional Scheme div2_ind := Induction for div2.
+Functional Scheme div2_ind := Induction for div2 Sort Prop.
 \end{coq_example}
 
 You may now look at the type of {\tt div2\_ind}:
@@ -315,7 +313,7 @@ We can now prove the following lemma using this principle:
 \begin{coq_example*}
 Lemma div2_le' : forall n:nat, div2 n <= n.
 intro n.
- pattern n.
+ pattern n , (div2 n).
 \end{coq_example*}
 
 
@@ -330,18 +328,17 @@ simpl; auto with arith.
 Qed.
 \end{coq_example*}
 
-Since \texttt{div2} is not mutually recursive, we can use
-directly the \texttt{functional induction} tactic instead of
-building the principle:
+We can use directly the \texttt{functional induction}
+(\ref{FunInduction}) tactic instead of the pattern/apply trick:
 
 \begin{coq_example*}
-Reset div2_ind.
+Reset div2_le'.
 Lemma div2_le : forall n:nat, div2 n <= n.
 intro n.
 \end{coq_example*}
 
 \begin{coq_example}
-functional induction div2 n.
+functional induction (div2 n).
 \end{coq_example}
 
 \begin{coq_example*}
@@ -351,14 +348,11 @@ auto with arith.
 Qed.
 \end{coq_example*}
 
-\paragraph{remark:} \texttt{functional induction} makes no use of
-an induction principle, so be warned that each time it is
-applied, a term mimicking the structure of \texttt{div2} (roughly
-the size of {\tt div2\_ind}) is built. Using \texttt{Functional
-  Scheme} is generally faster and less memory consuming.  On the
-other hand \texttt{functional induction} performs some extra
-simplifications that \texttt{Functional Scheme} does not, and as
-it is a tactic it can be used in tactic definitions.
+\Rem 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 normal definition using
+\texttt{Fixpoint} or \texttt{Definition}. See \ref{Function} for
+details.
 
 
 \example{Induction scheme for \texttt{tree\_size}}
@@ -398,14 +392,14 @@ recursive structure of \texttt{tree\_size} is defined by the
 command:
 
 \begin{coq_example*}
-Functional Scheme treeInd := Induction for tree_size
- with tree_size forest_size.
+Functional Scheme tree_size_ind := Induction for tree_size Sort Prop
+with forest_size_ind := Induction for forest_size Sort Prop.
 \end{coq_example*}
 
-You may now look at the type of {\tt treeInd}:
+You may now look at the type of {\tt tree\_size\_ind}:
 
 \begin{coq_example}
-Check treeInd.
+Check tree_size_ind.
 \end{coq_example}