Extract funind tactics to funind section of the Libraries chapter.

1 files changed, 87 insertions, 0 deletions

diff --git a/doc/sphinx/using/libraries/funind.rst b/doc/sphinx/using/libraries/funind.rst
new file mode 100644
index 0000000000..adabc56c50
--- /dev/null
+++ b/doc/sphinx/using/libraries/funind.rst
@@ -0,0 +1,87 @@
+.. 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.