Consolidate funind tactics and Functional Scheme in Funind section of the Libraries chapter.

1 files changed, 144 insertions, 0 deletions

diff --git a/doc/sphinx/using/libraries/funind.rst b/doc/sphinx/using/libraries/funind.rst
index adabc56c50..18f9ba246a 100644
--- a/doc/sphinx/using/libraries/funind.rst
+++ b/doc/sphinx/using/libraries/funind.rst
@@ -1,3 +1,6 @@
+Tactics
+-------
+
 .. tacn:: function induction (@qualid {+ @term})
    :name: function induction
 
@@ -85,3 +88,144 @@
       :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:`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.