Merge PR #12148: Consolidate funind documentation onto a single page.

Reviewed-by: jfehrle

3 files changed, 239 insertions, 242 deletions

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 7da453b7af..9dcfea4fe7 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -2076,7 +2076,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
 
    Now we are in a contradictory context and the proof can be solved.
 
-   .. coqtop:: all
+   .. coqtop:: all abort
 
       inversion H.
 
@@ -2104,68 +2104,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
 See also the larger example of :tacn:`dependent induction`
 and an explanation of the underlying technique.
 
-.. tacn:: function induction (@qualid {+ @term})
-   :name: function induction
-
-   The tactic functional induction performs case analysis and induction
-   following the definition of a function. It makes use of a principle
-   generated by ``Function`` (see :ref:`advanced-recursive-functions`) or
-   ``Functional Scheme`` (see :ref:`functional-scheme`).
-   Note that this tactic is only available after a ``Require Import FunInd``.
-
-.. example::
-
-   .. coqtop:: reset all
-
-      Require Import FunInd.
-      Functional Scheme minus_ind := Induction for minus Sort Prop.
-      Check minus_ind.
-      Lemma le_minus (n m:nat) : n - m <= n.
-      functional induction (minus n m) using minus_ind; simpl; auto.
-      Qed.
-
-.. note::
-   :n:`(@qualid {+ @term})` must be a correct full application
-   of :n:`@qualid`. In particular, the rules for implicit arguments are the
-   same as usual. For example use :n:`@qualid` if you want to write implicit
-   arguments explicitly.
-
-.. note::
-   Parentheses around :n:`@qualid {+ @term}` are not mandatory and can be skipped.
-
-.. note::
-   :n:`functional induction (f x1 x2 x3)` is actually a wrapper for
-   :n:`induction x1, x2, x3, (f x1 x2 x3) using @qualid` followed by a cleaning
-   phase, where :n:`@qualid` is the induction principle registered for :g:`f`
-   (by the ``Function`` (see :ref:`advanced-recursive-functions`) or
-   ``Functional Scheme`` (see :ref:`functional-scheme`)
-   command) corresponding to the sort of the goal. Therefore
-   ``functional induction`` may fail if the induction scheme :n:`@qualid` is not
-   defined. See also :ref:`advanced-recursive-functions` for the function
-   terms accepted by ``Function``.
-
-.. note::
-   There is a difference between obtaining an induction scheme
-   for a function by using :g:`Function` (see :ref:`advanced-recursive-functions`)
-   and by using :g:`Functional Scheme` after a normal definition using
-   :g:`Fixpoint` or :g:`Definition`. See :ref:`advanced-recursive-functions`
-   for details.
-
-.. seealso:: :ref:`advanced-recursive-functions`, :ref:`functional-scheme` and :tacn:`inversion`
-
-.. exn:: Cannot find induction information on @qualid.
-   :undocumented:
-
-.. exn:: Not the right number of induction arguments.
-   :undocumented:
-
-.. tacv:: functional induction (@qualid {+ @term}) as @simple_intropattern using @term with @bindings_list
-
-   Similarly to :tacn:`induction` and :tacn:`elim`, this allows giving
-   explicitly the name of the introduced variables, the induction principle, and
-   the values of dependent premises of the elimination scheme, including
-   *predicates* for mutual induction when :n:`@qualid` is part of a mutually
-   recursive definition.
+.. seealso:: :tacn:`functional induction`
 
 .. tacn:: discriminate @term
    :name: discriminate
@@ -2672,6 +2611,8 @@ and an explanation of the underlying technique.
       assumption.
       Qed.
 
+.. seealso:: :tacn:`functional inversion`
+
 .. tacn:: fix @ident @num
    :name: fix
 
@@ -4604,42 +4545,6 @@ symbol :g:`=`.
    Analogous to :tacn:`dependent rewrite ->` but uses the equality from right to
    left.
 
-Inversion
----------
-
-.. tacn:: functional inversion @ident
-   :name: functional inversion
-
-   :tacn:`functional inversion` is a tactic that performs inversion on hypothesis
-   :n:`@ident` of the form :n:`@qualid {+ @term} = @term` or :n:`@term = @qualid
-   {+ @term}` where :n:`@qualid` must have been defined using Function (see
-   :ref:`advanced-recursive-functions`). Note that this tactic is only
-   available after a ``Require Import FunInd``.
-
-   .. exn:: Hypothesis @ident must contain at least one Function.
-      :undocumented:
-
-   .. exn:: Cannot find inversion information for hypothesis @ident.
-
-      This error may be raised when some inversion lemma failed to be generated by
-      Function.
-
-
-   .. tacv:: functional inversion @num
-
-      This does the same thing as :n:`intros until @num` followed by
-      :n:`functional inversion @ident` where :token:`ident` is the
-      identifier for the last introduced hypothesis.
-
-   .. tacv:: functional inversion @ident @qualid
-             functional inversion @num @qualid
-
-      If the hypothesis :token:`ident` (or :token:`num`) has a type of the form
-      :n:`@qualid__1 {+ @term__i } = @qualid__2 {+ @term__j }` where
-      :n:`@qualid__1` and :n:`@qualid__2` are valid candidates to
-      functional inversion, this variant allows choosing which :token:`qualid`
-      is inverted.
-
 Classical tactics
 -----------------
 
diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst
index 34197c4fcf..e05be7c2c2 100644
--- a/doc/sphinx/user-extensions/proof-schemes.rst
+++ b/doc/sphinx/user-extensions/proof-schemes.rst
@@ -190,146 +190,7 @@ Combined Scheme
 
      Check tree_forest_mutrect.
 
-.. _functional-scheme:
-
-Generation of induction principles with ``Functional`` ``Scheme``
------------------------------------------------------------------
-
-
-.. cmd:: Functional Scheme @ident__0 := Induction for @ident' Sort @sort {* with @ident__i := Induction for @ident__i' Sort @sort}
-
-   This 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``.
-   Each :n:`@ident__i` 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 :n:`@ident__i`, following
-   the recursive structure and case analyses of the corresponding function
-   :n:`@ident__i'`.
-
-.. warning::
-
-   There is a difference between induction schemes generated by the command
-   :cmd:`Functional Scheme` and these generated by the :cmd:`Function`. Indeed,
-   :cmd:`Function` generally produces smaller principles that are closer to how
-   a user would implement them. See :ref:`advanced-recursive-functions` for details.
-
-.. 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 (:tacn:`function induction`) 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.
-
-.. 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.
-
-  Notice that the induction principles ``tree_size_ind`` and ``forest_size_ind``
-  generated by ``Function`` are not mutual.
-
-  .. coqtop:: all
-
-    Check tree_size_ind.
-
-  Mutual induction principles following the recursive structure of ``tree_size``
-  and ``forest_size`` can be generated by the following 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.
+.. seealso:: :ref:`functional-scheme`
 
 .. _derive-inversion:
 
diff --git a/doc/sphinx/using/libraries/funind.rst b/doc/sphinx/using/libraries/funind.rst
index ed00f3d455..40f9eedcf0 100644
--- a/doc/sphinx/using/libraries/funind.rst
+++ b/doc/sphinx/using/libraries/funind.rst
@@ -13,7 +13,7 @@ The following command is available when the ``FunInd`` library has been loaded v
    This command is a generalization of :cmd:`Fixpoint`. It is a wrapper
    for several ways of defining a function *and* other useful related
    objects, namely: an induction principle that reflects the recursive
-   structure of the function (see :tacn:`function induction`) and its fixpoint equality.
+   structure of the function (see :tacn:`functional induction`) and its fixpoint equality.
    This defines a function similar to those defined by :cmd:`Fixpoint`.
    As in :cmd:`Fixpoint`, the decreasing argument must
    be given (unless the function is not recursive), but it might not
@@ -27,7 +27,7 @@ The following command is available when the ``FunInd`` library has been loaded v
    to structurally recursive functions (i.e. when :n:`@fixannot` is a :n:`struct`
    clause).
 
-   See :tacn:`function induction` and :cmd:`Functional Scheme` for how to use
+   See :tacn:`functional induction` and :cmd:`Functional Scheme` for how to use
    the induction principle to reason easily about the function.
 
    The form of the :n:`@fixannot` clause determines which definition mechanism :cmd:`Function` uses.
@@ -166,4 +166,235 @@ terminating functions.
 
    :tacn:`functional inversion` will not be available for the function.
 
-.. seealso:: :ref:`functional-scheme` and :tacn:`function induction`
+Tactics
+-------
+
+.. tacn:: functional induction (@qualid {+ @term})
+   :name: functional induction
+
+   The tactic functional induction performs case analysis and induction
+   following the definition of a function. It makes use of a principle
+   generated by :cmd:`Function` or :cmd:`Functional Scheme`.
+   Note that this tactic is only available after a ``Require Import FunInd``.
+
+   .. example::
+
+      .. coqtop:: reset all
+
+         Require Import FunInd.
+         Functional Scheme minus_ind := Induction for minus Sort Prop.
+         Check minus_ind.
+         Lemma le_minus (n m:nat) : n - m <= n.
+         functional induction (minus n m) using minus_ind; simpl; auto.
+         Qed.
+
+   .. note::
+      :n:`(@qualid {+ @term})` must be a correct full application
+         of :n:`@qualid`. In particular, the rules for implicit arguments are the
+         same as usual. For example use :n:`@qualid` if you want to write implicit
+         arguments explicitly.
+
+   .. note::
+      Parentheses around :n:`@qualid {+ @term}` are not mandatory and can be skipped.
+
+   .. note::
+      :n:`functional induction (f x1 x2 x3)` is actually a wrapper for
+      :n:`induction x1, x2, x3, (f x1 x2 x3) using @qualid` followed by a cleaning
+      phase, where :n:`@qualid` is the induction principle registered for :g:`f`
+      (by the :cmd:`Function` or :cmd:`Functional Scheme` command)
+      corresponding to the sort of the goal. Therefore
+      :tacn:`functional induction` may fail if the induction scheme :n:`@qualid` is not
+      defined.
+
+   .. note::
+      There is a difference between obtaining an induction scheme
+      for a function by using :cmd:`Function`
+      and by using :cmd:`Functional Scheme` after a normal definition using
+      :cmd:`Fixpoint` or :cmd:`Definition`.
+
+   .. exn:: Cannot find induction information on @qualid.
+      :undocumented:
+
+   .. exn:: Not the right number of induction arguments.
+      :undocumented:
+
+   .. tacv:: functional induction (@qualid {+ @term}) as @simple_intropattern using @term with @bindings_list
+
+      Similarly to :tacn:`induction` and :tacn:`elim`, this allows giving
+      explicitly the name of the introduced variables, the induction principle, and
+      the values of dependent premises of the elimination scheme, including
+      *predicates* for mutual induction when :n:`@qualid` is part of a mutually
+      recursive definition.
+
+.. tacn:: functional inversion @ident
+   :name: functional inversion
+
+   :tacn:`functional inversion` is a tactic that performs inversion on hypothesis
+   :n:`@ident` of the form :n:`@qualid {+ @term} = @term` or :n:`@term = @qualid
+   {+ @term}` where :n:`@qualid` must have been defined using :cmd:`Function`.
+   Note that this tactic is only available after a ``Require Import FunInd``.
+
+   .. exn:: Hypothesis @ident must contain at least one Function.
+      :undocumented:
+
+   .. exn:: Cannot find inversion information for hypothesis @ident.
+
+      This error may be raised when some inversion lemma failed to be generated by
+      Function.
+
+
+   .. tacv:: functional inversion @num
+
+      This does the same thing as :n:`intros until @num` followed by
+      :n:`functional inversion @ident` where :token:`ident` is the
+      identifier for the last introduced hypothesis.
+
+   .. tacv:: functional inversion @ident @qualid
+             functional inversion @num @qualid
+
+      If the hypothesis :token:`ident` (or :token:`num`) has a type of the form
+      :n:`@qualid__1 {+ @term__i } = @qualid__2 {+ @term__j }` where
+      :n:`@qualid__1` and :n:`@qualid__2` are valid candidates to
+      functional inversion, this variant allows choosing which :token:`qualid`
+      is inverted.
+
+.. _functional-scheme:
+
+Generation of induction principles with ``Functional`` ``Scheme``
+-----------------------------------------------------------------
+
+
+.. cmd:: Functional Scheme @ident__0 := Induction for @ident' Sort @sort {* with @ident__i := Induction for @ident__i' Sort @sort}
+
+   This 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``.
+   Each :n:`@ident__i` 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 :n:`@ident__i`, following
+   the recursive structure and case analyses of the corresponding function
+   :n:`@ident__i'`.
+
+.. warning::
+
+   There is a difference between induction schemes generated by the command
+   :cmd:`Functional Scheme` and these generated by the :cmd:`Function`. Indeed,
+   :cmd:`Function` generally produces smaller principles that are closer to how
+   a user would implement them. See :ref:`advanced-recursive-functions` for details.
+
+.. 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 (:tacn:`functional induction`) 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.
+
+.. 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.
+
+  Notice that the induction principles ``tree_size_ind`` and ``forest_size_ind``
+  generated by ``Function`` are not mutual.
+
+  .. coqtop:: all
+
+    Check tree_size_ind.
+
+  Mutual induction principles following the recursive structure of ``tree_size``
+  and ``forest_size`` can be generated by the following 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.