Merge all documentation on Funind into the same file.

1 files changed, 232 insertions, 0 deletions

diff --git a/doc/sphinx/using/libraries/funind.rst b/doc/sphinx/using/libraries/funind.rst
index ed00f3d455..179a4df781 100644
--- a/doc/sphinx/using/libraries/funind.rst
+++ b/doc/sphinx/using/libraries/funind.rst
@@ -167,3 +167,235 @@ terminating functions.
    :tacn:`functional inversion` will not be available for the function.
 
 .. seealso:: :ref:`functional-scheme` and :tacn:`function induction`
+
+Tactics
+-------
+
+.. 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:
+
+.. 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.
+
+.. _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.