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

Reviewed-by: jfehrle

1 files changed, 234 insertions, 3 deletions

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.