2 files changed, 203 insertions, 2 deletions
diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex
index b014ded70..00cd5b134 100644
--- a/doc/RefMan-tac.tex
+++ b/doc/RefMan-tac.tex
@@ -806,8 +806,8 @@ Applies the conversion tactic {\convtactic} to the
 hypotheses \ident$_1$, \ldots, \ident$_n$. The tactic {\convtactic} is
 any of the conversion tactics listed in this section. 
 
-If $\ident$_i$ is a local definition, then $\ident$_i$ can be replaced
-by $(Type of \ident$_i)$ to adress not the body but the type of the
+If \ident$_i$ is a local definition, then \ident$_i$ can be replaced
+by (Type of \ident$_i$) to adress not the body but the type of the
 local definition. Example: {\tt Unfold not in (Type of H1) (Type of H3).}
 
 \begin{ErrMsgs}
@@ -1102,6 +1102,37 @@ Qed.
   \texttt{Record} macro, see p. \pageref{Record}).
 \end{Variants}
 
+
+\subsection{\tt Functional Induction \ident\ \term$_1$ \dots\ \term$_n$.}
+\tacindex{Functional Scheme}
+\label{FunScheme}
+
+The tactic \texttt{Functional Induction} performs case analysis
+and induction following the definition of a function.
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+\begin{coq_example}
+Lemma moins_le : (n,m:nat) (le (minus n m) n).
+Intros n m.
+Functional Induction minus n m;Simpl;Auto.
+\end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
+
+\texttt{Functional Induction} is a shorthand for the more general
+command \texttt{Functional Scheme} which builds induction
+principles following the recursive structure of (possibly
+mutually recursive) functions.
+
+\texttt{Functional Induction} does not work on dependently typed
+function yet. It may also fail on functions built by certain
+tactics.
+
+\SeeAlso{\ref{FunScheme},\ref{FunScheme-examples}}
+
 \section{Equality}
 These tactics use the equality {\tt
 eq:(A:Set)A->A->Prop} defined in file {\tt Logic.v} and the equality
@@ -1788,6 +1819,7 @@ incompatibilities.
 % \end{ErrMsgs}
 
 
+
 \subsection{\tt Omega}
 \tacindex{Omega}
 \label{Omega}
@@ -2400,6 +2432,42 @@ of mutual induction for objects in type {\term$_i$}.
 
 \SeeAlso \ref{Scheme-examples}
 
+
+\section{Generation of induction principles with {\tt functional Scheme}}
+\label{FunScheme}
+\comindex{Functional Scheme}
+
+The {\tt Functional Scheme} command is a high-level experimental
+tool for generating automatically induction principles
+corresponding to (possibly mutually recursive) functions.  Its
+syntax follows the schema:\bigskip
+
+\noindent
+{\tt Functional Scheme {\ident$_i$} := Induction for
+    \ident'$_i$ with \ident'$_1$ \dots\ \ident'$_m$.}\\
+  
+  \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.
+
+\begin{Variants}
+\item {\tt Functional Scheme {\ident$_1$} := Induction for \ident'$_1$.}\\
+  
+  This command is a shortcut for:
+  
+  {\tt Functional Scheme {\ident$_1$} := Induction for
+    \ident'$_1$ with \ident'$_1$.}
+
+  This variant can be used for non mutually recursive functions only.
+\end{Variants}
+
+\SeeAlso \ref{FunScheme-examples}
+
+
 \section{Simple tactic macros}
 \index[tactic]{tactic macros}
 \index{tactic macros}
diff --git a/doc/RefMan-tacex.tex b/doc/RefMan-tacex.tex
index c74206ab6..3614aca9a 100644
--- a/doc/RefMan-tacex.tex
+++ b/doc/RefMan-tacex.tex
@@ -259,6 +259,139 @@ Check odd_even.
 The type of {\tt even\_odd} shares the same premises but the
 conclusion is {\tt (n:nat)(even n)->(Q n)}.
 
+\section{{\tt Functional Scheme and Functional Induction}}
+\comindex{FunScheme}
+\label{FunScheme-examples}
+
+\firstexample
+\example{Induction scheme for \texttt{div2}}
+
+We define the function \texttt{div2} as follows:
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+
+\begin{coq_example*}
+Require Arith.
+Fixpoint div2 [n:nat] : nat :=
+ Cases n of
+   (0) => (0)
+   | (S n0) => Cases n0 of
+                    (0) => (0)
+                  | (S n') => (S (div2 n'))
+                 end
+ end.
+\end{coq_example*}
+
+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.
+\end{coq_example}
+
+You may now look at the type of {\tt div2\_ind}:
+
+\begin{coq_example}
+Check div2_ind.
+\end{coq_example}
+
+We can now prove the following lemma using this principle:
+
+
+\begin{coq_example*}
+Lemma div2_le' : (n:nat)(le (div2 n) n).
+Intro n. Pattern n.
+\end{coq_example*}
+
+
+\begin{coq_example}
+Apply div2_ind;Intros.
+\end{coq_example}
+
+\begin{coq_example*}
+Auto with arith.
+Auto with arith.
+Simpl;Auto with arith.
+Save.
+\end{coq_example*}
+
+Since \texttt{div2} is not mutually recursive, we can use
+directly the \texttt{Functional Induction} tactic instead of
+building the principle:
+
+\begin{coq_example*}
+Reset div2_ind.
+Lemma div2_le : (n:nat)(le (div2 n) n).
+Intro n.
+\end{coq_example*}
+
+\begin{coq_example}
+Functional Induction div2 n.
+\end{coq_example}
+
+\begin{coq_example*}
+Auto with arith.
+Auto with arith.
+Auto with arith.
+Save.
+\end{coq_example*}
+
+\paragraph{remark:} \texttt{Functional Induction} makes no use of
+a induction principle, so be warned that each time it is used, 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 simplification
+steps that \texttt{Functional Scheme} doesn't.
+
+
+
+\example{Induction scheme for \texttt{tree\_size}}
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+
+We define trees by the following mutual inductive type:
+
+\begin{coq_example*}
+Variable A : Set.
+Mutual Inductive 
+     tree   : Set := node : A -> forest -> tree
+with forest : Set := empty : forest 
+                  | cons : tree -> forest -> forest.
+\end{coq_example*}
+
+We define the function \texttt{tree\_size} that computes the size
+of a tree or a forest.
+
+\begin{coq_example*}                
+Fixpoint tree_size  [t:tree] : nat := 
+ Cases t of (node A f) => (S (forest_size f)) end
+  with  forest_size [f:forest]: nat := 
+ Cases f of
+  empty => O
+ | (cons t f') => (plus (tree_size t) (forest_size f'))
+ end.
+\end{coq_example*}
+
+The definition of principle of mutual induction following the
+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.
+\end{coq_example*}
+
+You may now look at the type of {\tt treeInd}:
+
+\begin{coq_example}
+Check treeInd.
+\end{coq_example}
+
+
 
 \section{{\tt Inversion}}
 \tacindex{Inversion}