diff options
Diffstat (limited to 'doc/sphinx/using')
| -rw-r--r-- | doc/sphinx/using/libraries/funind.rst | 94 | ||||
| -rw-r--r-- | doc/sphinx/using/libraries/index.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/using/libraries/writing.rst | 10 | ||||
| -rw-r--r-- | doc/sphinx/using/tools/coqdoc.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/using/tools/index.rst | 8 |
5 files changed, 59 insertions, 65 deletions
diff --git a/doc/sphinx/using/libraries/funind.rst b/doc/sphinx/using/libraries/funind.rst index 738d64bfc3..93571ecebb 100644 --- a/doc/sphinx/using/libraries/funind.rst +++ b/doc/sphinx/using/libraries/funind.rst @@ -169,13 +169,24 @@ terminating functions. Tactics ------- -.. tacn:: functional induction (@qualid {+ @term}) +.. tacn:: functional induction @term {? using @one_term {? with @bindings } } {? as @simple_intropattern } :name: functional induction - The tactic functional induction performs case analysis and induction - following the definition of a function. It makes use of a principle + Performs case analysis and induction following the definition of a function + :token:`qualid`, which must be fully applied to its arguments as part of + :token:`term`. It uses a principle generated by :cmd:`Function` or :cmd:`Functional Scheme`. Note that this tactic is only available after a ``Require Import FunInd``. + See the :cmd:`Function` command. + + :n:`using @one_term` + Specifies the induction principle (aka elimination scheme). + + :n:`with @bindings` + Specifies the arguments of the induction principle. + + :n:`as @simple_intropattern` + Provides names for the introduced variables. .. example:: @@ -189,15 +200,6 @@ Tactics 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` @@ -218,22 +220,27 @@ Tactics .. 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 +.. tacn:: functional inversion {| @ident | @natural } {? @qualid } :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`. + Performs inversion on hypothesis + :n:`@ident` of the form :n:`@qualid {+ @term} = @term` or + :n:`@term = @qualid {+ @term}` when :n:`@qualid` is defined using :cmd:`Function`. Note that this tactic is only available after a ``Require Import FunInd``. + :n:`@natural` + Does the same thing as :n:`intros until @natural` followed by + :n:`functional inversion @ident` where :token:`ident` is the + identifier for the last introduced hypothesis. + + :n:`@qualid` + If the hypothesis :token:`ident` (or :token:`natural`) 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. + + .. exn:: Hypothesis @ident must contain at least one Function. :undocumented: @@ -242,39 +249,26 @@ Tactics This error may be raised when some inversion lemma failed to be generated by Function. - - .. tacv:: functional inversion @natural - - This does the same thing as :n:`intros until @natural` followed by - :n:`functional inversion @ident` where :token:`ident` is the - identifier for the last introduced hypothesis. - - .. tacv:: functional inversion @ident @qualid - functional inversion @natural @qualid - - If the hypothesis :token:`ident` (or :token:`natural`) 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} +.. cmd:: Functional Scheme @func_scheme_def {* with @func_scheme_def } + + .. insertprodn func_scheme_def func_scheme_def + + .. prodn:: + func_scheme_def ::= @ident := Induction for @qualid Sort @sort_family + + An experimental high-level tool that + automatically generates induction principles corresponding to functions that + may be mutually recursive. The command generates an + induction principle named :n:`@ident` for each given function named :n:`@qualid`. + The :n:`@qualid`\s must be given in the same order as when they were defined. - 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'`. + Note the command must be made available via :cmd:`Require Import` ``FunInd``. .. warning:: diff --git a/doc/sphinx/using/libraries/index.rst b/doc/sphinx/using/libraries/index.rst index 0bd3054788..95218322ff 100644 --- a/doc/sphinx/using/libraries/index.rst +++ b/doc/sphinx/using/libraries/index.rst @@ -4,15 +4,15 @@ Libraries and plugins ===================== -Coq is distributed with a standard library and a set of internal +|Coq| is distributed with a standard library and a set of internal plugins (most of which provide tactics that have already been presented in :ref:`writing-proofs`). This chapter presents this standard library and some of these internal plugins which provide features that are not tactics. -In addition, Coq has a rich ecosystem of external libraries and +In addition, |Coq| has a rich ecosystem of external libraries and plugins. These libraries and plugins can be browsed online through -the `Coq Package Index <https://coq.inria.fr/opam/www/>`_ and +the `|Coq| Package Index <https://coq.inria.fr/opam/www/>`_ and installed with the `opam package manager <https://coq.inria.fr/opam-using.html>`_. diff --git a/doc/sphinx/using/libraries/writing.rst b/doc/sphinx/using/libraries/writing.rst index 325ea2af60..724bcd0488 100644 --- a/doc/sphinx/using/libraries/writing.rst +++ b/doc/sphinx/using/libraries/writing.rst @@ -1,9 +1,9 @@ -Writing Coq libraries and plugins -================================= +Writing |Coq| libraries and plugins +=================================== -This section presents the part of the Coq language that is useful only -to library and plugin authors. A tutorial for writing Coq plugins is -available in the Coq repository in `doc/plugin_tutorial +This section presents the part of the |Coq| language that is useful only +to library and plugin authors. A tutorial for writing |Coq| plugins is +available in the |Coq| repository in `doc/plugin_tutorial <https://github.com/coq/coq/tree/master/doc/plugin_tutorial>`_. Deprecating library objects or tactics diff --git a/doc/sphinx/using/tools/coqdoc.rst b/doc/sphinx/using/tools/coqdoc.rst index 9ac3d2adda..88c1a575d9 100644 --- a/doc/sphinx/using/tools/coqdoc.rst +++ b/doc/sphinx/using/tools/coqdoc.rst @@ -253,7 +253,7 @@ The latter cannot be used around some inner parts of a proof, but can be used around a whole proof. Lastly, it is possible to adopt a middle-ground approach when the -desired output is HTML, where a given snippet of Coq material is +desired output is HTML, where a given snippet of |Coq| material is hidden by default, but can be made visible with user interaction. :: @@ -358,11 +358,11 @@ Command line options **Hyperlink options** :--glob-from file: Make references using |Coq| globalizations from file - file. (Such globalizations are obtained with Coq option ``-dump-glob``). + file. (Such globalizations are obtained with |Coq| option ``-dump-glob``). :--no-externals: Do not insert links to the |Coq| standard library. :--external url coqdir: Use given URL for linking references whose name starts with prefix ``coqdir``. - :--coqlib url: Set base URL for the Coq standard library (default is + :--coqlib url: Set base URL for the |Coq| standard library (default is `<http://coq.inria.fr/library/>`_). This is equivalent to ``--external url Coq``. :-R dir coqdir: Recursively map physical directory dir to |Coq| logical diff --git a/doc/sphinx/using/tools/index.rst b/doc/sphinx/using/tools/index.rst index dfe38dfce9..8543c5de8a 100644 --- a/doc/sphinx/using/tools/index.rst +++ b/doc/sphinx/using/tools/index.rst @@ -5,11 +5,11 @@ Command-line and graphical tools ================================ This chapter presents the command-line tools that users will need to -build their Coq project, the documentation of the CoqIDE standalone +build their |Coq| project, the documentation of the |CoqIDE| standalone user interface and the documentation of the parallel proof processing -feature that is supported by CoqIDE and several other user interfaces. -A list of available user interfaces to interact with Coq is available -on the `Coq website <https://coq.inria.fr/user-interfaces.html>`_. +feature that is supported by |CoqIDE| and several other user interfaces. +A list of available user interfaces to interact with |Coq| is available +on the `|Coq| website <https://coq.inria.fr/user-interfaces.html>`_. .. toctree:: :maxdepth: 1 |