Merge PR #6993: Sphinx doc chapter 13

5 files changed, 376 insertions, 446 deletions

diff --git a/Makefile.doc b/Makefile.doc
index 64b43f5ea..077ae965c 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -60,7 +60,7 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \
   RefMan-gal.v.tex \
   RefMan-lib.v.tex \
   RefMan-oth.v.tex RefMan-ltac.v.tex \
-  RefMan-pro.v.tex RefMan-sch.v.tex \
+  RefMan-pro.v.tex \
   Cases.v.tex Coercion.v.tex CanonicalStructures.v.tex Extraction.v.tex \
   Program.v.tex Omega.v.tex Micromega.v.tex Polynom.v.tex Nsatz.v.tex \
   Setoid.v.tex Classes.v.tex Universes.v.tex \
diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex
deleted file mode 100644
index 600471123..000000000
--- a/doc/refman/RefMan-sch.tex
+++ /dev/null
@@ -1,444 +0,0 @@
-\chapter{Proof schemes}
-%HEVEA\cutname{schemes.html}
-
-\section{Generation of induction principles with {\tt Scheme}}
-\label{Scheme}
-\index{Schemes}
-\comindex{Scheme}
-
-The {\tt Scheme} command is a high-level tool for generating
-automatically (possibly mutual) induction principles for given types
-and sorts.  Its syntax follows the schema:
-\begin{quote}
-{\tt Scheme {\ident$_1$} := Induction for \ident'$_1$ Sort {\sort$_1$} \\
-  with\\
-  \mbox{}\hspace{0.1cm} \dots\\
-        with {\ident$_m$} := Induction for {\ident'$_m$} Sort
-        {\sort$_m$}}
-\end{quote}
-where \ident'$_1$ \dots\ \ident'$_m$ are different inductive type
-identifiers belonging to the same package of mutual inductive
-definitions. This command generates {\ident$_1$}\dots{} {\ident$_m$}
-to be mutually recursive definitions. Each term {\ident$_i$} proves a
-general principle of mutual induction for objects in type {\term$_i$}.
-
-\begin{Variants}
-\item {\tt Scheme {\ident$_1$} := Minimality for \ident'$_1$ Sort {\sort$_1$} \\
-    with\\
-    \mbox{}\hspace{0.1cm} \dots\ \\
-    with {\ident$_m$} := Minimality for {\ident'$_m$} Sort
-    {\sort$_m$}}
-
-  Same as before but defines a non-dependent elimination principle more
-  natural in case of inductively defined relations.
-
-\item {\tt Scheme Equality for \ident$_1$\comindex{Scheme Equality}}
-
-  Tries to generate a Boolean equality and a proof of the
-  decidability of the usual equality. If \ident$_i$ involves
-  some other inductive types, their equality has to be defined first.
-
-\item {\tt Scheme Induction for \ident$_1$ Sort {\sort$_1$} \\
-  with\\
-  \mbox{}\hspace{0.1cm} \dots\\
-        with Induction for {\ident$_m$} Sort
-        {\sort$_m$}}
-
-  If you do not provide the name of the schemes, they will be automatically
-  computed from the sorts involved (works also with Minimality).
-
-\end{Variants}
-\label{Scheme-examples}
-
-\firstexample
-\example{Induction scheme for \texttt{tree} and \texttt{forest}}
-
-The definition of principle of mutual induction for {\tt tree} and
-{\tt forest} over the sort {\tt Set} is defined by the command:
-
-\begin{coq_eval}
-Reset Initial.
-Variables A B : Set.
-\end{coq_eval}
-
-\begin{coq_example*}
-Inductive tree : Set :=
-    node : A -> forest -> tree
-with forest : Set :=
-  | leaf : B -> forest
-  | cons : tree -> forest -> forest.
-
-Scheme tree_forest_rec := Induction for tree Sort Set
-  with forest_tree_rec := Induction for forest Sort Set.
-\end{coq_example*}
-
-You may now look at the type of {\tt tree\_forest\_rec}:
-
-\begin{coq_example}
-Check tree_forest_rec.
-\end{coq_example}
-
-This principle involves two different predicates for {\tt trees} and
-{\tt forests}; it also has three premises each one corresponding to a
-constructor of one of the inductive definitions.
-
-The principle {\tt forest\_tree\_rec} shares exactly the same
-premises, only the conclusion now refers to the property of forests.
-
-\begin{coq_example}
-Check forest_tree_rec.
-\end{coq_example}
-
-\example{Predicates {\tt odd} and {\tt even} on naturals}
-
-Let {\tt odd} and {\tt even} be inductively defined as:
-
-% Reset Initial.
-\begin{coq_eval}
-Open Scope nat_scope.
-\end{coq_eval}
-
-\begin{coq_example*}
-Inductive odd : nat -> Prop :=
-    oddS : forall n:nat, even n -> odd (S n)
-with even : nat -> Prop :=
-  | evenO : even 0
-  | evenS : forall n:nat, odd n -> even (S n).
-\end{coq_example*}
-
-The following command generates a powerful elimination
-principle:
-
-\begin{coq_example}
-Scheme odd_even := Minimality for   odd Sort Prop
-  with even_odd := Minimality for even Sort Prop.
-\end{coq_example}
-
-The type of {\tt odd\_even} for instance will be:
-
-\begin{coq_example}
-Check odd_even.
-\end{coq_example}
-
-The type of {\tt even\_odd} shares the same premises but the
-conclusion is {\tt (n:nat)(even n)->(Q n)}.
-
-\subsection{Automatic declaration of schemes
-\optindex{Boolean Equality Schemes}
-\optindex{Elimination Schemes}
-\optindex{Nonrecursive Elimination Schemes}
-\optindex{Case Analysis Schemes}
-\optindex{Decidable Equality Schemes}
-\optindex{Rewriting Schemes}
-\label{set-nonrecursive-elimination-schemes}
-}
-
-It is possible to deactivate the automatic declaration of the induction
- principles when defining a new inductive type  with the
- {\tt Unset Elimination Schemes} command. It may be
-reactivated at any time with {\tt Set Elimination Schemes}.
-
-The types declared with the keywords {\tt Variant} (see~\ref{Variant})
-and {\tt Record} (see~\ref{Record}) do not have an automatic
-declaration of the induction principles. It can be activated with the
-command {\tt Set Nonrecursive Elimination Schemes}. It can be
-deactivated again with {\tt Unset Nonrecursive Elimination Schemes}.
-
-In addition, the {\tt Case Analysis Schemes} flag governs the generation of
-case analysis lemmas for inductive types, i.e. corresponding to the
-pattern-matching term alone and without fixpoint.
-\\
-
-You can also activate the automatic declaration of those Boolean equalities
-(see the second variant of {\tt Scheme})
-with respectively the commands {\tt Set Boolean Equality Schemes} and
-{\tt Set Decidable Equality Schemes}.
-However you have to be careful with this option since
-\Coq~ may now reject well-defined inductive types because it cannot compute
-a Boolean equality for them.
-
-The {\tt Rewriting Schemes} flag governs generation of equality
-related schemes such as congruence.
-
-\subsection{\tt Combined Scheme}
-\label{CombinedScheme}
-\comindex{Combined Scheme}
-
-The {\tt Combined Scheme} command is a tool for combining
-induction principles generated by the {\tt Scheme} command.
-Its syntax follows the schema :
-\begin{quote}
-{\tt Combined Scheme {\ident$_0$} from {\ident$_1$}, .., {\ident$_n$}}
-\end{quote}
-where
-\ident$_1$ \ldots \ident$_n$ are different inductive principles that must belong to
-the same package of mutual inductive principle definitions. This command
-generates {\ident$_0$} to be the conjunction of the principles: it is
-built from the common premises of the principles and concluded by the
-conjunction of their conclusions.
-
-\Example
-We can define the induction principles for trees and forests using:
-\begin{coq_example}
-Scheme tree_forest_ind := Induction for tree Sort Prop
-  with forest_tree_ind := Induction for forest Sort Prop.
-\end{coq_example}
-
-Then we can build the combined induction principle which gives the
-conjunction of the conclusions of each individual principle:
-\begin{coq_example}
-Combined Scheme tree_forest_mutind from tree_forest_ind, forest_tree_ind.
-\end{coq_example}
-
-The type of {\tt tree\_forest\_mutrec} will be:
-\begin{coq_example}
-Check tree_forest_mutind.
-\end{coq_example}
-
-\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.
-First, it must be made available via {\tt Require Import FunInd}.
- Its
-syntax then follows the schema:
-\begin{quote}
-{\tt Functional Scheme {\ident$_1$} := Induction for \ident'$_1$ Sort {\sort$_1$} \\
-  with\\
-  \mbox{}\hspace{0.1cm} \dots\ \\
-        with {\ident$_m$} := Induction for {\ident'$_m$} Sort
-        {\sort$_m$}}
-\end{quote}
-where \ident'$_1$ \dots\ \ident'$_m$ are different mutually defined function
-names (they must be in the same order as when they were defined).
-This command generates the induction principles
-\ident$_1$\dots\ident$_m$, following the recursive structure and case
-analyses of the functions \ident'$_1$ \dots\ \ident'$_m$.
-
-\Rem
-There is a difference between obtaining an induction scheme by using
-\texttt{Functional Scheme} on a function defined by \texttt{Function}
-or not. Indeed \texttt{Function} generally produces smaller
-principles, closer to the definition written by the user.
-
-\firstexample
-\example{Induction scheme for \texttt{div2}}
-\label{FunScheme-examples}
-
-We define the function \texttt{div2} as follows:
-
-\begin{coq_eval}
-Reset Initial.
-Require Import FunInd.
-\end{coq_eval}
-
-\begin{coq_example*}
-Require Import Arith.
-Fixpoint div2 (n:nat) : nat :=
-  match n with
-  | O => 0
-  | S O => 0
-  | S (S n') => S (div2 n')
-  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 Sort Prop.
-\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' : forall n:nat, div2 n <= n.
-intro n.
- pattern n , (div2 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.
-Qed.
-\end{coq_example*}
-
-We can use directly the \texttt{functional induction}
-(\ref{FunInduction}) tactic instead of the pattern/apply trick:
-\tacindex{functional induction}
-
-\begin{coq_example*}
-Reset div2_le'.
-Lemma div2_le : forall n:nat, 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.
-Qed.
-\end{coq_example*}
-
-\Rem There is a difference between obtaining an induction scheme for a
-function by using \texttt{Function} (see 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}}
-
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-
-We define trees by the following mutual inductive type:
-
-\begin{coq_example*}
-Variable A : Set.
-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. Note that we use \texttt{Function} which
-generally produces better principles.
-
-\begin{coq_example*}
-Require Import FunInd.
-Function tree_size (t:tree) : nat :=
-  match t with
-  | node A f => S (forest_size f)
-  end
- with forest_size (f:forest) : nat :=
-  match f with
-  | empty => 0
-  | cons t f' => (tree_size t + forest_size f')
-  end.
-\end{coq_example*}
-
-\Rem \texttt{Function} generates itself non mutual induction
-principles {\tt tree\_size\_ind} and {\tt forest\_size\_ind}:
-
-\begin{coq_example}
-Check tree_size_ind.
-\end{coq_example}
-
-The definition of mutual induction principles following the recursive
-structure of \texttt{tree\_size} and \texttt{forest\_size} is defined
-by the command:
-
-\begin{coq_example*}
-Functional Scheme tree_size_ind2 := Induction for tree_size Sort Prop
-with forest_size_ind2 := Induction for forest_size Sort Prop.
-\end{coq_example*}
-
-You may now look at the type of {\tt tree\_size\_ind2}:
-
-\begin{coq_example}
-Check tree_size_ind2.
-\end{coq_example}
-
-\section{Generation of inversion principles with \tt Derive Inversion}
-\label{Derive-Inversion}
-\comindex{Derive Inversion}
-
-The syntax of {\tt Derive Inversion} follows the schema:
-\begin{quote}
-{\tt Derive Inversion {\ident} with forall
-  $(\vec{x} : \vec{T})$, $I~\vec{t}$ Sort \sort}
-\end{quote}
-
-This command generates an inversion principle for the
-\texttt{inversion \dots\ using} tactic.
-\tacindex{inversion \dots\ using}
-Let $I$ be an inductive predicate and $\vec{x}$ the variables
-occurring in $\vec{t}$. This command generates and stocks the
-inversion lemma for the sort \sort~ corresponding to the instance
-$\forall (\vec{x}:\vec{T}), I~\vec{t}$ with the name {\ident} in the {\bf
-global} environment. When applied, it is equivalent to having inverted
-the instance with the tactic {\tt inversion}.
-
-\begin{Variants}
-\item \texttt{Derive Inversion\_clear {\ident} with forall
-  $(\vec{x}:\vec{T})$, $I~\vec{t}$ Sort \sort}\\
-  \comindex{Derive Inversion\_clear}
-  When applied, it is equivalent to having
-  inverted the instance with the tactic \texttt{inversion}
-  replaced by the tactic \texttt{inversion\_clear}.
-\item \texttt{Derive Dependent Inversion {\ident} with forall
-  $(\vec{x}:\vec{T})$, $I~\vec{t}$ Sort \sort}\\
-  \comindex{Derive Dependent Inversion}
-  When applied, it is equivalent to having
-  inverted the instance with the tactic \texttt{dependent inversion}.
-\item \texttt{Derive Dependent Inversion\_clear {\ident} with forall
-  $(\vec{x}:\vec{T})$, $I~\vec{t}$ Sort \sort}\\
-  \comindex{Derive Dependent Inversion\_clear}
-  When applied, it is equivalent to having
-  inverted the instance with the tactic \texttt{dependent inversion\_clear}.
-\end{Variants}
-
-\Example
-
-Let us consider the relation \texttt{Le} over natural numbers and the
-following variable:
-
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-
-\begin{coq_example*}
-Inductive Le : nat -> nat -> Set :=
-  | LeO : forall n:nat, Le 0 n
-  | LeS : forall n m:nat, Le n m -> Le (S n) (S m).
-Variable P : nat -> nat -> Prop.
-\end{coq_example*}
-
-To generate the inversion lemma for the instance
-\texttt{(Le (S n) m)} and the sort \texttt{Prop}, we do:
-
-\begin{coq_example*}
-Derive Inversion_clear leminv with (forall n m:nat, Le (S n) m) Sort Prop.
-\end{coq_example*}
-
-\begin{coq_example}
-Check leminv.
-\end{coq_example}
-
-Then we can use the proven inversion lemma:
-
-\begin{coq_eval}
-Lemma ex : forall n m:nat, Le (S n) m -> P n m.
-intros.
-\end{coq_eval}
-
-\begin{coq_example}
-Show.
-\end{coq_example}
-
-\begin{coq_example}
-inversion H using leminv.
-\end{coq_example}
-
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index 9545a47c9..357272aa4 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -110,7 +110,6 @@ Options A and B of the licence are {\em not} elected.}
 
 \part{User extensions}
 %%SUPPRIME \include{RefMan-tus.v}% Writing tactics
-\include{RefMan-sch.v}% The Scheme commands
 
 \part{Practical tools}
 \include{RefMan-com}% The coq commands (coqc coqtop)
diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst
index f3b852d45..443e5c10f 100644
--- a/doc/sphinx/index.rst
+++ b/doc/sphinx/index.rst
@@ -30,6 +30,7 @@ Table of contents
    :caption: User extensions
 
    user-extensions/syntax-extensions
+   user-extensions/proof-schemes
 
 .. toctree::
    :caption: Practical tools
diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst
new file mode 100644
index 000000000..583b73e53
--- /dev/null
+++ b/doc/sphinx/user-extensions/proof-schemes.rst
@@ -0,0 +1,374 @@
+.. _proofschemes:
+
+Proof schemes
+===============
+
+Generation of induction principles with ``Scheme``
+--------------------------------------------------------
+
+The ``Scheme`` command is a high-level tool for generating automatically
+(possibly mutual) induction principles for given types and sorts. Its
+syntax follows the schema:
+
+.. cmd:: Scheme ident := Induction for ident' Sort sort {* with ident := Induction for ident' Sort sort}
+
+where each `ident'ᵢ` is a different inductive type identifier 
+belonging to the same package of mutual inductive definitions. This
+command generates the `identᵢ`s to be mutually recursive
+definitions. Each term `identᵢ` proves a general principle of mutual
+induction for objects in type `identᵢ`.
+
+.. cmdv:: Scheme ident := Minimality for ident' Sort sort {* with ident := Minimality for ident' Sort sort}
+
+  Same as before but defines a non-dependent elimination principle more
+  natural in case of inductively defined relations.
+
+.. cmdv:: Scheme Equality for ident
+
+   Tries to generate a Boolean equality and a proof of the decidability of the usual equality. If `ident`
+   involves some other inductive types, their equality has to be defined first.
+
+.. cmdv:: Scheme Induction for ident Sort sort {* with Induction for ident Sort sort}
+
+   If you do not provide the name of the schemes, they will be automatically computed from the
+   sorts involved (works also with Minimality).
+
+.. example::
+
+   Induction scheme for tree and forest.
+
+   The definition of principle of mutual induction for tree and forest
+   over the sort Set is defined by the command:
+
+    .. coqtop:: none
+
+     Axiom A : Set.	       
+     Axiom B : Set.	       
+   
+    .. coqtop:: all
+
+     Inductive tree : Set := node : A -> forest -> tree
+     with forest : Set :=
+         leaf : B -> forest
+       | cons : tree -> forest -> forest.
+
+     Scheme tree_forest_rec := Induction for tree Sort Set
+       with forest_tree_rec := Induction for forest Sort Set.
+
+  You may now look at the type of tree_forest_rec:
+
+  .. coqtop:: all
+
+    Check tree_forest_rec.
+
+  This principle involves two different predicates for trees andforests;
+  it also has three premises each one corresponding to a constructor of
+  one of the inductive definitions.
+
+  The principle `forest_tree_rec` shares exactly the same premises, only
+  the conclusion now refers to the property of forests.
+
+.. example::
+
+  Predicates odd and even on naturals.
+
+  Let odd and even be inductively defined as:
+
+   .. coqtop:: all
+
+      Inductive odd : nat -> Prop := oddS : forall n:nat, even n -> odd (S n)
+      with even : nat -> Prop := 
+        | evenO : even 0
+        | evenS : forall n:nat, odd n -> even (S n).
+
+  The following command generates a powerful elimination principle:
+
+   .. coqtop:: all
+
+    Scheme odd_even := Minimality for odd Sort Prop
+    with even_odd := Minimality for even Sort Prop.
+
+  The type of odd_even for instance will be:
+
+  .. coqtop:: all
+
+    Check odd_even.
+
+  The type of `even_odd` shares the same premises but the conclusion is
+  `(n:nat)(even n)->(P0 n)`.
+
+
+Automatic declaration of schemes
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+It is possible to deactivate the automatic declaration of the
+induction principles when defining a new inductive type with the
+``Unset Elimination Schemes`` command. It may be reactivated at any time with
+``Set Elimination Schemes``.
+
+The types declared with the keywords ``Variant`` (see :ref:`TODO-1.3.3`) and ``Record``
+(see :ref:`Record Types <record-types>`) do not have an automatic declaration of the induction
+principles. It can be activated with the command
+``Set Nonrecursive Elimination Schemes``. It can be deactivated again with
+``Unset Nonrecursive Elimination Schemes``.
+
+In addition, the ``Case Analysis Schemes`` flag governs the generation of
+case analysis lemmas for inductive types, i.e. corresponding to the
+pattern-matching term alone and without fixpoint.
+You can also activate the automatic declaration of those Boolean
+equalities (see the second variant of ``Scheme``) with respectively the
+commands ``Set Boolean Equality Schemes`` and ``Set Decidable Equality
+Schemes``. However you have to be careful with this option since Coq may
+now reject well-defined inductive types because it cannot compute a
+Boolean equality for them.
+
+.. opt:: Rewriting Schemes
+
+   This flag governs generation of equality-related schemes such as congruence.
+
+Combined Scheme
+~~~~~~~~~~~~~~~~~~~~~~
+
+The ``Combined Scheme`` command is a tool for combining induction
+principles generated by the ``Scheme command``. Its syntax follows the
+schema :
+
+.. cmd:: Combined Scheme ident from {+, ident}
+
+where each identᵢ after the ``from`` is a different inductive principle that must
+belong to the same package of mutual inductive principle definitions.
+This command generates the leftmost `ident` to be the conjunction of the
+principles: it is built from the common premises of the principles and
+concluded by the conjunction of their conclusions.
+
+.. example:: 
+
+  We can define the induction principles for trees and forests using:
+
+  .. coqtop:: all
+
+    Scheme tree_forest_ind := Induction for tree Sort Prop
+    with forest_tree_ind := Induction for forest Sort Prop.
+
+  Then we can build the combined induction principle which gives the
+  conjunction of the conclusions of each individual principle:
+
+  .. coqtop:: all
+
+    Combined Scheme tree_forest_mutind from tree_forest_ind,forest_tree_ind.
+
+  The type of tree_forest_mutrec will be:
+
+  .. coqtop:: all
+
+    Check tree_forest_mutind.
+
+Generation of induction principles with ``Functional`` ``Scheme``
+-----------------------------------------------------------------
+
+The ``Functional Scheme`` command is a high-level experimental tool for
+generating automatically induction principles corresponding to
+(possibly mutually recursive) functions. First, it must be made
+available via ``Require Import FunInd``. Its syntax then follows the
+schema:
+
+.. cmd:: Functional Scheme ident := Induction for ident' Sort sort {* with ident := Induction for ident' Sort sort}
+
+where each `ident'ᵢ` is a different mutually defined function
+name (the names must be in the same order as when they were defined). This
+command generates the induction principle for each `identᵢ`, following
+the recursive structure and case analyses of the corresponding function 
+identᵢ’.
+
+Remark: There is a difference between obtaining an induction scheme by
+using ``Functional Scheme`` on a function defined by ``Function`` or not.
+Indeed, ``Function`` generally produces smaller principles, closer to the
+definition written by the user.
+
+.. example:: 
+
+  Induction scheme for div2.
+
+  We define the function div2 as follows:
+
+  .. coqtop:: all
+
+   Require Import FunInd.
+   Require Import Arith.
+
+   Fixpoint div2 (n:nat) : nat :=
+   match n with
+   | O => 0
+   | S O => 0
+   | S (S n') => S (div2 n')
+   end.
+
+  The definition of a principle of induction corresponding to the
+  recursive structure of `div2` is defined by the command:
+
+  .. coqtop:: all
+
+    Functional Scheme div2_ind := Induction for div2 Sort Prop.
+
+  You may now look at the type of div2_ind:
+
+  .. coqtop:: all
+
+    Check div2_ind.
+
+  We can now prove the following lemma using this principle:
+
+  .. coqtop:: all
+
+    Lemma div2_le' : forall n:nat, div2 n <= n.
+    intro n.
+    pattern n, (div2 n).
+    apply div2_ind; intros.
+    auto with arith.
+    auto with arith.
+    simpl; auto with arith.
+    Qed.
+
+  We can use directly the functional induction (:ref:`TODO-8.5.5`) tactic instead
+  of the pattern/apply trick:
+
+  .. coqtop:: all
+
+    Reset div2_le'.
+
+    Lemma div2_le : forall n:nat, div2 n <= n.
+    intro n.
+    functional induction (div2 n).
+    auto with arith.
+    auto with arith.
+    auto with arith.
+    Qed.
+
+  Remark: There is a difference between obtaining an induction scheme
+  for a function by using ``Function`` (see :ref:`advanced-recursive-functions`) and by using
+  ``Functional Scheme`` after a normal definition using ``Fixpoint`` or
+  ``Definition``. See :ref:`advanced-recursive-functions` for details.
+
+.. example::
+
+  Induction scheme for tree_size.
+
+  We define trees by the following mutual inductive type:
+
+  .. original LaTeX had "Variable" instead of "Axiom", which generates an ugly warning
+   
+  .. coqtop:: reset all
+
+     Axiom A : Set.
+     
+     Inductive tree : Set :=
+     node : A -> forest -> tree
+     with forest : Set :=
+     | empty : forest
+     | cons : tree -> forest -> forest.
+
+  We define the function tree_size that computes the size of a tree or a
+  forest. Note that we use ``Function`` which generally produces better
+  principles.
+
+  .. coqtop:: all
+
+    Require Import FunInd.
+
+    Function tree_size (t:tree) : nat :=
+    match t with
+    | node A f => S (forest_size f)
+    end
+    with forest_size (f:forest) : nat :=
+    match f with
+    | empty => 0
+    | cons t f' => (tree_size t + forest_size f')
+    end.
+
+  Remark: Function generates itself non mutual induction principles
+  tree_size_ind and forest_size_ind:
+
+  .. coqtop:: all
+
+    Check tree_size_ind.
+
+  The definition of mutual induction principles following the recursive
+  structure of `tree_size` and `forest_size` is defined by the command:
+
+  .. coqtop:: all
+
+    Functional Scheme tree_size_ind2 := Induction for tree_size Sort Prop
+    with forest_size_ind2 := Induction for forest_size Sort Prop.
+
+  You may now look at the type of `tree_size_ind2`:
+
+  .. coqtop:: all
+
+    Check tree_size_ind2.
+     
+Generation of inversion principles with ``Derive`` ``Inversion``
+-----------------------------------------------------------------
+
+The syntax of ``Derive`` ``Inversion`` follows the schema:
+
+.. cmd:: Derive Inversion ident with forall (x : T), I t Sort sort
+
+This command generates an inversion principle for the `inversion … using` 
+tactic. Let `I` be an inductive predicate and `x` the variables occurring
+in t. This command generates and stocks the inversion lemma for the
+sort `sort` corresponding to the instance `∀ (x:T), I t` with the name
+`ident` in the global environment. When applied, it is equivalent to
+having inverted the instance with the tactic `inversion`.
+
+.. cmdv:: Derive Inversion_clear ident with forall (x:T), I t Sort sort
+
+   When applied, it is equivalent to having inverted the instance with the
+   tactic inversion replaced by the tactic `inversion_clear`.
+
+.. cmdv:: Derive Dependent Inversion ident with forall (x:T), I t Sort sort
+
+   When applied, it is equivalent to having inverted the instance with
+   the tactic `dependent inversion`.
+
+.. cmdv:: Derive Dependent Inversion_clear ident with forall(x:T), I t Sort sort
+
+   When applied, it is equivalent to having inverted the instance
+   with the tactic `dependent inversion_clear`.
+
+.. example::
+
+  Let us consider the relation `Le` over natural numbers and the following
+  variable:
+
+  .. original LaTeX had "Variable" instead of "Axiom", which generates an ugly warning
+  
+  .. coqtop:: all
+
+    Inductive Le : nat -> nat -> Set :=
+    | LeO : forall n:nat, Le 0 n
+    | LeS : forall n m:nat, Le n m -> Le (S n) (S m).
+
+    Axiom P : nat -> nat -> Prop.
+
+  To generate the inversion lemma for the instance `(Le (S n) m)` and the
+  sort `Prop`, we do:
+
+  .. coqtop:: all
+
+    Derive Inversion_clear leminv with (forall n m:nat, Le (S n) m) Sort Prop.
+    Check leminv.
+
+  Then we can use the proven inversion lemma:
+
+  .. the original LaTeX did not have any Coq code to setup the goal
+
+  .. coqtop:: none
+
+    Goal forall (n m : nat) (H : Le (S n) m), P n m.			  
+    intros.
+  
+  .. coqtop:: all
+
+    Show.
+
+    inversion H using leminv.