aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
diff options
context:
space:
mode:
Diffstat (limited to 'doc/sphinx')
-rw-r--r--doc/sphinx/addendum/sprop.rst7
-rw-r--r--doc/sphinx/addendum/universe-polymorphism.rst15
-rw-r--r--doc/sphinx/changes.rst4
-rw-r--r--doc/sphinx/coqdoc.css338
-rw-r--r--doc/sphinx/practical-tools/utilities.rst16
-rw-r--r--doc/sphinx/proof-engine/ssreflect-proof-language.rst10
-rw-r--r--doc/sphinx/proof-engine/tactics.rst104
-rw-r--r--doc/sphinx/proof-engine/vernacular-commands.rst26
-rw-r--r--doc/sphinx/user-extensions/proof-schemes.rst141
-rw-r--r--doc/sphinx/using/libraries/funind.rst237
10 files changed, 304 insertions, 594 deletions
diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst
index 9acdd18b89..b2d3687780 100644
--- a/doc/sphinx/addendum/sprop.rst
+++ b/doc/sphinx/addendum/sprop.rst
@@ -240,3 +240,10 @@ so correctly converts ``x`` and ``y``.
the kernel when it is passed a term with incorrect relevance marks.
To avoid conversion issues as in ``late_mark`` you may wish to use
it to find when your tactics are producing incorrect marks.
+
+.. flag:: Cumulative StrictProp
+ :name: Cumulative StrictProp
+
+ Set this flag (it is off by default) to make the kernel accept
+ cumulativity between |SProp| and other universes. This makes
+ typechecking incomplete.
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index a08495badd..2958d866ac 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -227,7 +227,7 @@ constraints by prefixing the level names with symbols.
Because inductive subtypings are only produced by comparing inductives
to themselves with universes changed, they amount to variance
information: each universe is either invariant, covariant or
-irrelevant (there are no contravariant subtypings in Coq),
+irrelevant (there are no contravariant subtypings in |Coq|),
respectively represented by the symbols `=`, `+` and `*`.
Here we see that :g:`list` binds an irrelevant universe, so any two
@@ -426,6 +426,19 @@ mode, introduced universe names can be referred to in terms. Note that
local universe names shadow global universe names. During a proof, one
can use :cmd:`Show Universes` to display the current context of universes.
+It is possible to provide only some universe levels and let |Coq| infer the others
+by adding a :g:`+` in the list of bound universe levels:
+
+.. coqtop:: all
+
+ Fail Definition foobar@{u} : Type@{u} := Type.
+ Definition foobar@{u +} : Type@{u} := Type.
+ Set Printing Universes.
+ Print foobar.
+
+This can be used to find which universes need to be explicitly bound in a given
+definition.
+
Definitions can also be instantiated explicitly, giving their full
instance:
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index f72654b33b..6615b98660 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -482,10 +482,12 @@ Changes in 8.11+beta1
.. _811Reals:
- **Added:**
- Module `Reals.ConstructiveCauchyReals` defines constructive real numbers
+ Module `Reals.Cauchy.ConstructiveCauchyReals` defines constructive real numbers
by Cauchy sequences of rational numbers
(`#10445 <https://github.com/coq/coq/pull/10445>`_, by Vincent Semeria,
with the help and review of Guillaume Melquiond and Bas Spitters).
+ This module is not meant to be imported directly, please import
+ `Reals.Abstract.ConstructiveReals` instead.
- **Added:**
New module `Reals.ClassicalDedekindReals` defines Dedekind real
numbers as boolean-valued functions along with 3 logical axioms:
diff --git a/doc/sphinx/coqdoc.css b/doc/sphinx/coqdoc.css
deleted file mode 100644
index a325a33842..0000000000
--- a/doc/sphinx/coqdoc.css
+++ /dev/null
@@ -1,338 +0,0 @@
-/************************************************************************/
-/* * The Coq Proof Assistant / The Coq Development Team */
-/* v * Copyright INRIA, CNRS and contributors */
-/* <O___,, * (see version control and CREDITS file for authors & dates) */
-/* \VV/ **************************************************************/
-/* // * This file is distributed under the terms of the */
-/* * GNU Lesser General Public License Version 2.1 */
-/* * (see LICENSE file for the text of the license) */
-/************************************************************************/
-body { padding: 0px 0px;
- margin: 0px 0px;
- background-color: white }
-
-#page { display: block;
- padding: 0px;
- margin: 0px;
- padding-bottom: 10px; }
-
-#header { display: block;
- position: relative;
- padding: 0;
- margin: 0;
- vertical-align: middle;
- border-bottom-style: solid;
- border-width: thin }
-
-#header h1 { padding: 0;
- margin: 0;}
-
-
-/* Contents */
-
-#main{ display: block;
- padding: 10px;
- font-family: sans-serif;
- font-size: 100%;
- line-height: 100% }
-
-#main h1 { line-height: 95% } /* allow for multi-line headers */
-
-#main a.idref:visited {color : #416DFF; text-decoration : none; }
-#main a.idref:link {color : #416DFF; text-decoration : none; }
-#main a.idref:hover {text-decoration : none; }
-#main a.idref:active {text-decoration : none; }
-
-#main a.modref:visited {color : #416DFF; text-decoration : none; }
-#main a.modref:link {color : #416DFF; text-decoration : none; }
-#main a.modref:hover {text-decoration : none; }
-#main a.modref:active {text-decoration : none; }
-
-#main .keyword { color : #cf1d1d }
-#main { color: black }
-
-.section { background-color: rgb(60%,60%,100%);
- padding-top: 13px;
- padding-bottom: 13px;
- padding-left: 3px;
- margin-top: 5px;
- margin-bottom: 5px;
- font-size : 175% }
-
-h2.section { background-color: rgb(80%,80%,100%);
- padding-left: 3px;
- padding-top: 12px;
- padding-bottom: 10px;
- font-size : 130% }
-
-h3.section { background-color: rgb(90%,90%,100%);
- padding-left: 3px;
- padding-top: 7px;
- padding-bottom: 7px;
- font-size : 115% }
-
-h4.section {
-/*
- background-color: rgb(80%,80%,80%);
- max-width: 20em;
- padding-left: 5px;
- padding-top: 5px;
- padding-bottom: 5px;
-*/
- background-color: white;
- padding-left: 0px;
- padding-top: 0px;
- padding-bottom: 0px;
- font-size : 100%;
- font-weight : bold;
- text-decoration : underline;
- }
-
-#main .doc { margin: 0px;
- font-family: sans-serif;
- font-size: 100%;
- line-height: 125%;
- max-width: 40em;
- color: black;
- padding: 10px;
- background-color: #90bdff }
-
-.inlinecode {
- display: inline;
-/* font-size: 125%; */
- color: #666666;
- font-family: monospace }
-
-.doc .inlinecode {
- display: inline;
- font-size: 120%;
- color: rgb(30%,30%,70%);
- font-family: monospace }
-
-.doc .inlinecode .id {
- color: rgb(30%,30%,70%);
-}
-
-.inlinecodenm {
- display: inline;
- color: #444444;
-}
-
-.doc .code {
- display: inline;
- font-size: 120%;
- color: rgb(30%,30%,70%);
- font-family: monospace }
-
-.comment {
- display: inline;
- font-family: monospace;
- color: rgb(50%,50%,80%);
-}
-
-.code {
- display: block;
-/* padding-left: 15px; */
- font-size: 110%;
- font-family: monospace;
- }
-
-table.infrule {
- border: 0px;
- margin-left: 50px;
- margin-top: 10px;
- margin-bottom: 10px;
-}
-
-td.infrule {
- font-family: monospace;
- text-align: center;
-/* color: rgb(35%,35%,70%); */
- padding: 0px;
- line-height: 100%;
-}
-
-tr.infrulemiddle hr {
- margin: 1px 0 1px 0;
-}
-
-.infrulenamecol {
- color: rgb(60%,60%,60%);
- font-size: 80%;
- padding-left: 1em;
- padding-bottom: 0.1em
-}
-
-/* Pied de page */
-
-#footer { font-size: 65%;
- font-family: sans-serif; }
-
-/* Identifiers: <span class="id" title="...">) */
-
-.id { display: inline; }
-
-.id[title="constructor"] {
- color: rgb(60%,0%,0%);
-}
-
-.id[title="var"] {
- color: rgb(40%,0%,40%);
-}
-
-.id[title="variable"] {
- color: rgb(40%,0%,40%);
-}
-
-.id[title="definition"] {
- color: rgb(0%,40%,0%);
-}
-
-.id[title="abbreviation"] {
- color: rgb(0%,40%,0%);
-}
-
-.id[title="lemma"] {
- color: rgb(0%,40%,0%);
-}
-
-.id[title="instance"] {
- color: rgb(0%,40%,0%);
-}
-
-.id[title="projection"] {
- color: rgb(0%,40%,0%);
-}
-
-.id[title="method"] {
- color: rgb(0%,40%,0%);
-}
-
-.id[title="inductive"] {
- color: rgb(0%,0%,80%);
-}
-
-.id[title="record"] {
- color: rgb(0%,0%,80%);
-}
-
-.id[title="class"] {
- color: rgb(0%,0%,80%);
-}
-
-.id[title="keyword"] {
- color : #cf1d1d;
-/* color: black; */
-}
-
-/* Deprecated rules using the 'type' attribute of <span> (not xhtml valid) */
-
-.id[type="constructor"] {
- color: rgb(60%,0%,0%);
-}
-
-.id[type="var"] {
- color: rgb(40%,0%,40%);
-}
-
-.id[type="variable"] {
- color: rgb(40%,0%,40%);
-}
-
-.id[type="definition"] {
- color: rgb(0%,40%,0%);
-}
-
-.id[type="abbreviation"] {
- color: rgb(0%,40%,0%);
-}
-
-.id[type="lemma"] {
- color: rgb(0%,40%,0%);
-}
-
-.id[type="instance"] {
- color: rgb(0%,40%,0%);
-}
-
-.id[type="projection"] {
- color: rgb(0%,40%,0%);
-}
-
-.id[type="method"] {
- color: rgb(0%,40%,0%);
-}
-
-.id[type="inductive"] {
- color: rgb(0%,0%,80%);
-}
-
-.id[type="record"] {
- color: rgb(0%,0%,80%);
-}
-
-.id[type="class"] {
- color: rgb(0%,0%,80%);
-}
-
-.id[type="keyword"] {
- color : #cf1d1d;
-/* color: black; */
-}
-
-.inlinecode .id {
- color: rgb(0%,0%,0%);
-}
-
-
-/* TOC */
-
-#toc h2 {
- padding: 10px;
- background-color: rgb(60%,60%,100%);
-}
-
-#toc li {
- padding-bottom: 8px;
-}
-
-/* Index */
-
-#index {
- margin: 0;
- padding: 0;
- width: 100%;
-}
-
-#index #frontispiece {
- margin: 1em auto;
- padding: 1em;
- width: 60%;
-}
-
-.booktitle { font-size : 140% }
-.authors { font-size : 90%;
- line-height: 115%; }
-.moreauthors { font-size : 60% }
-
-#index #entrance {
- text-align: center;
-}
-
-#index #entrance .spacer {
- margin: 0 30px 0 30px;
-}
-
-#index #footer {
- position: absolute;
- bottom: 0;
-}
-
-.paragraph {
- height: 0.75em;
-}
-
-ul.doclist {
- margin-top: 0em;
- margin-bottom: 0em;
-}
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index 921c7bbbf7..bc77e2e58c 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -245,9 +245,9 @@ file timing data:
COQDEP Fast.v
COQDEP Slow.v
COQC Slow.v
- Slow (user: 0.34 mem: 395448 ko)
+ Slow.vo (user: 0.34 mem: 395448 ko)
COQC Fast.v
- Fast (user: 0.01 mem: 45184 ko)
+ Fast.vo (user: 0.01 mem: 45184 ko)
+ ``pretty-timed``
this target stores the output of ``make TIMED=1`` into
@@ -280,15 +280,15 @@ file timing data:
COQDEP Fast.v
COQDEP Slow.v
COQC Slow.v
- Slow (user: 0.36 mem: 393912 ko)
+ Slow.vo (user: 0.36 mem: 393912 ko)
COQC Fast.v
- Fast (user: 0.05 mem: 45992 ko)
+ Fast.vo (user: 0.05 mem: 45992 ko)
Time | File Name
--------------------
0m00.41s | Total
--------------------
- 0m00.36s | Slow
- 0m00.05s | Fast
+ 0m00.36s | Slow.vo
+ 0m00.05s | Fast.vo
+ ``print-pretty-timed-diff``
@@ -338,8 +338,8 @@ file timing data:
--------------------------------------------------------
0m00.39s | Total | 0m00.35s || +0m00.03s | +11.42%
--------------------------------------------------------
- 0m00.37s | Slow | 0m00.01s || +0m00.36s | +3600.00%
- 0m00.02s | Fast | 0m00.34s || -0m00.32s | -94.11%
+ 0m00.37s | Slow.vo | 0m00.01s || +0m00.36s | +3600.00%
+ 0m00.02s | Fast.vo | 0m00.34s || -0m00.32s | -94.11%
The following targets and ``Makefile`` variables allow collection of per-
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index b5d1e8bffd..28c5359a04 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -1624,9 +1624,15 @@ previous :token:`i_item` have been performed.
The second entry in the :token:`i_view` grammar rule,
``/ltac:(`` :token:`tactic` ``)``, executes :token:`tactic`.
-Notations can be used to name tactics, for example::
+Notations can be used to name tactics, for example
- Notation myop := (ltac:(some ltac code)) : ssripat_scope.
+.. coqtop:: none
+
+ Tactic Notation "my" "ltac" "code" := idtac.
+
+.. coqtop:: in warn
+
+ Notation "'myop'" := (ltac:(my ltac code)) : ssripat_scope.
lets one write just ``/myop`` in the intro pattern. Note the scope
annotation: views are interpreted opening the ``ssripat`` scope.
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 1ecfa05f99..7e6da490fb 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -1875,6 +1875,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
Lemma induction_test : forall n:nat, n = n -> n <= n.
intros n H.
induction n.
+ exact (le_n 0).
.. exn:: Not an inductive product.
:undocumented:
@@ -2076,7 +2077,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 +2105,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 +2612,8 @@ and an explanation of the underlying technique.
assumption.
Qed.
+.. seealso:: :tacn:`functional inversion`
+
.. tacn:: fix @ident @num
:name: fix
@@ -4604,42 +4546,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/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 7d031b9b7a..60fdbf0a9d 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -91,9 +91,15 @@ capital letter.
This command supports the :attr:`local`, :attr:`global` and :attr:`export` attributes.
They are described :ref:`here <set_unset_scope_qualifiers>`.
- .. warn:: There is no option @setting_name.
+ .. warn:: There is no flag or option with this name: "@setting_name".
- This message also appears for unknown flags.
+ This warning message can be raised by :cmd:`Set` and
+ :cmd:`Unset` when :n:`@setting_name` is unknown. It is a
+ warning rather than an error because this helps library authors
+ produce Coq code that is compatible with several Coq versions.
+ To preserve the same behavior, they may need to set some
+ compatibility flags or options that did not exist in previous
+ Coq versions.
.. cmd:: Unset @setting_name
:name: Unset
@@ -119,6 +125,20 @@ capital letter.
whether the table contains each specified value, otherise this is equivalent to
:cmd:`Print Table`. The `for` clause is not valid for flags and options.
+ .. exn:: There is no flag, option or table with this name: "@setting_name".
+
+ This error message is raised when calling the :cmd:`Test`
+ command (without the `for` clause), or the :cmd:`Print Table`
+ command, for an unknown :n:`@setting_name`.
+
+ .. exn:: There is no qualid-valued table with this name: "@setting_name".
+ There is no string-valued table with this name: "@setting_name".
+
+ These error messages are raised when calling the :cmd:`Add` or
+ :cmd:`Remove` commands, or the :cmd:`Test` command with the
+ `for` clause, if :n:`@setting_name` is unknown or does not have
+ the right type.
+
.. cmd:: Print Options
Prints the current value of all flags and options, and the names of all tables.
@@ -1076,6 +1096,8 @@ Controlling Typing Flags
Print the status of the three typing flags: guard checking, positivity checking
and universe checking.
+See also :flag:`Cumulative StrictProp` in the |SProp| chapter.
+
.. example::
.. coqtop:: all reset
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 01:33:15 +0000