diff options
Diffstat (limited to 'doc/sphinx/using')
| -rw-r--r-- | doc/sphinx/using/libraries/funind.rst | 169 | ||||
| -rw-r--r-- | doc/sphinx/using/libraries/index.rst | 1 | ||||
| -rw-r--r-- | doc/sphinx/using/tools/coqdoc.rst | 484 | ||||
| -rw-r--r-- | doc/sphinx/using/tools/index.rst | 1 |
4 files changed, 655 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..ed00f3d455 --- /dev/null +++ b/doc/sphinx/using/libraries/funind.rst @@ -0,0 +1,169 @@ +Functional induction +==================== + +.. _advanced-recursive-functions: + +Advanced recursive functions +---------------------------- + +The following command is available when the ``FunInd`` library has been loaded via ``Require Import FunInd``: + +.. cmd:: Function @fix_definition {* with @fix_definition } + + 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. + 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 + necessarily be *structurally* decreasing. Use the :n:`@fixannot` clause + to name the decreasing argument *and* to describe which kind of + decreasing criteria to use to ensure termination of recursive + calls. + + :cmd:`Function` also supports the :n:`with` clause to create + mutually recursive definitions, however this feature is limited + 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 + the induction principle to reason easily about the function. + + The form of the :n:`@fixannot` clause determines which definition mechanism :cmd:`Function` uses. + (Note that references to :n:`ident` below refer to the name of the function being defined.): + + * If :n:`@fixannot` is not specified, :cmd:`Function` + defines the nonrecursive function :token:`ident` as if it was declared with + :cmd:`Definition`. In addition, the following are defined: + + + :token:`ident`\ ``_rect``, :token:`ident`\ ``_rec`` and :token:`ident`\ ``_ind``, + which reflect the pattern matching structure of :token:`term` (see :cmd:`Inductive`); + + The inductive :n:`R_@ident` corresponding to the graph of :token:`ident` (silently); + + :token:`ident`\ ``_complete`` and :token:`ident`\ ``_correct`` which + are inversion information linking the function and its graph. + + * If :n:`{ struct ... }` is specified, :cmd:`Function` + defines the structural recursive function :token:`ident` as if it was declared + with :cmd:`Fixpoint`. In addition, the following are defined: + + + The same objects as above; + + The fixpoint equation of :token:`ident`: :n:`@ident`\ ``_equation``. + + * If :n:`{ measure ... }` or :n:`{ wf ... }` are specified, :cmd:`Function` + defines a recursive function by well-founded recursion. The module ``Recdef`` + of the standard library must be loaded for this feature. + + + :n:`{measure @one_term__1 {? @ident } {? @one_term__2 } }`\: where :n:`@ident` is the decreasing argument + and :n:`@one_term__1` is a function from the type of :n:`@ident` to :g:`nat` for which + the decreasing argument decreases (for the :g:`lt` order on :g:`nat`) + for each recursive call of the function. The parameters of the function are + bound in :n:`@one_term__1`. + + :n:`{wf @one_term @ident }`\: where :n:`@ident` is the decreasing argument and + :n:`@one_term` is an ordering relation on the type of :n:`@ident` (i.e. of type + `T`\ :math:`_{\sf ident}` → `T`\ :math:`_{\sf ident}` → ``Prop``) for which the decreasing argument + decreases for each recursive call of the function. The order must be well-founded. + The parameters of the function are bound in :n:`@one_term`. + + If the clause is ``measure`` or ``wf``, the user is left with some proof + obligations that will be used to define the function. These proofs + are: proofs that each recursive call is actually decreasing with + respect to the given criteria, and (if the criteria is `wf`) a proof + that the ordering relation is well-founded. Once proof obligations are + discharged, the following objects are defined: + + + The same objects as with the ``struct`` clause; + + The lemma :n:`@ident`\ ``_tcc`` which collects all proof obligations in one + property; + + The lemmas :n:`@ident`\ ``_terminate`` and :n:`@ident`\ ``_F`` which will be inlined + during extraction of :n:`@ident`. + + The way this recursive function is defined is the subject of several + papers by Yves Bertot and Antonia Balaa on the one hand, and Gilles + Barthe, Julien Forest, David Pichardie, and Vlad Rusu on the other + hand. + +.. note:: + + To obtain the right principle, it is better to put rigid + parameters of the function as first arguments. For example it is + better to define plus like this: + + .. coqtop:: reset none + + Require Import FunInd. + + .. coqtop:: all + + Function plus (m n : nat) {struct n} : nat := + match n with + | 0 => m + | S p => S (plus m p) + end. + + than like this: + + .. coqtop:: reset none + + Require Import FunInd. + + .. coqtop:: all + + Function plus (n m : nat) {struct n} : nat := + match n with + | 0 => m + | S p => S (plus p m) + end. + + +*Limitations* + +:token:`term` must be built as a *pure pattern matching tree* (:g:`match … with`) +with applications only *at the end* of each branch. + +:cmd:`Function` does not support partial application of the function being +defined. Thus, the following example cannot be accepted due to the +presence of partial application of :g:`wrong` in the body of :g:`wrong`: + +.. coqtop:: none + + Require List. + Import List.ListNotations. + +.. coqtop:: all fail + + Function wrong (C:nat) : nat := + List.hd 0 (List.map wrong (C::nil)). + +For now, dependent cases are not treated for non structurally +terminating functions. + +.. exn:: The recursive argument must be specified. + :undocumented: + +.. exn:: No argument name @ident. + :undocumented: + +.. exn:: Cannot use mutual definition with well-founded recursion or measure. + :undocumented: + +.. warn:: Cannot define graph for @ident. + + The generation of the graph relation (:n:`R_@ident`) used to compute the induction scheme of ident + raised a typing error. Only :token:`ident` is defined; the induction scheme + will not be generated. This error happens generally when: + + - the definition uses pattern matching on dependent types, + which :cmd:`Function` cannot deal with yet. + - the definition is not a *pattern matching tree* as explained above. + +.. warn:: Cannot define principle(s) for @ident. + + The generation of the graph relation (:n:`R_@ident`) succeeded but the induction principle + could not be built. Only :token:`ident` is defined. Please report. + +.. warn:: Cannot build functional inversion principle. + + :tacn:`functional inversion` will not be available for the function. + +.. seealso:: :ref:`functional-scheme` and :tacn:`function induction` diff --git a/doc/sphinx/using/libraries/index.rst b/doc/sphinx/using/libraries/index.rst index d0848e6c3f..ad10869439 100644 --- a/doc/sphinx/using/libraries/index.rst +++ b/doc/sphinx/using/libraries/index.rst @@ -22,3 +22,4 @@ installed with the `opam package manager ../../language/coq-library ../../addendum/extraction ../../addendum/miscellaneous-extensions + funind diff --git a/doc/sphinx/using/tools/coqdoc.rst b/doc/sphinx/using/tools/coqdoc.rst new file mode 100644 index 0000000000..b4b14fb392 --- /dev/null +++ b/doc/sphinx/using/tools/coqdoc.rst @@ -0,0 +1,484 @@ +.. _coqdoc: + +Documenting |Coq| files with coqdoc +----------------------------------- + +coqdoc is a documentation tool for the proof assistant |Coq|, similar to +``javadoc`` or ``ocamldoc``. The task of coqdoc is + + +#. to produce a nice |Latex| and/or HTML document from |Coq| source files, + readable for a human and not only for the proof assistant; +#. to help the user navigate his own (or third-party) sources. + + + +Principles +~~~~~~~~~~ + +Documentation is inserted into |Coq| files as *special comments*. Thus +your files will compile as usual, whether you use coqdoc or not. coqdoc +presupposes that the given |Coq| files are well-formed (at least +lexically). Documentation starts with ``(**``, followed by a space, and +ends with ``*)``. The documentation format is inspired by Todd +A. Coram’s *Almost Free Text (AFT)* tool: it is mainly ``ASCII`` text with +some syntax-light controls, described below. coqdoc is robust: it +shouldn’t fail, whatever the input is. But remember: “garbage in, +garbage out”. + + +|Coq| material inside documentation. +++++++++++++++++++++++++++++++++++++ + +|Coq| material is quoted between the delimiters ``[`` and ``]``. Square brackets +may be nested, the inner ones being understood as being part of the +quoted code (thus you can quote a term like ``fun x => u`` by writing ``[fun +x => u]``). Inside quotations, the code is pretty-printed in the same +way as it is in code parts. + +Preformatted vernacular is enclosed by ``[[`` and ``]]``. The former must be +followed by a newline and the latter must follow a newline. + + +Pretty-printing. +++++++++++++++++ + +coqdoc uses different faces for identifiers and keywords. The pretty- +printing of |Coq| tokens (identifiers or symbols) can be controlled +using one of the following commands: + +:: + + + (** printing *token* %...LATEX...% #...html...# *) + + +or + +:: + + + (** printing *token* $...LATEX math...$ #...html...# *) + + +It gives the |Latex| and HTML texts to be produced for the given |Coq| +token. Either the |Latex| or the HTML rule may be omitted, causing the +default pretty-printing to be used for this token. + +The printing for one token can be removed with + +:: + + + (** remove printing *token* *) + + +Initially, the pretty-printing table contains the following mapping: + +===== === ==== ===== === ==== ==== === +`->` → `<-` ← `*` × +`<=` ≤ `>=` ≥ `=>` ⇒ +`<>` ≠ `<->` ↔ `|-` ⊢ +`\\/` ∨ `/\\` ∧ `~` ¬ +===== === ==== ===== === ==== ==== === + +Any of these can be overwritten or suppressed using the printing +commands. + +.. note:: + + The recognition of tokens is done by a (``ocaml``) lex + automaton and thus applies the longest-match rule. For instance, `->~` + is recognized as a single token, where |Coq| sees two tokens. It is the + responsibility of the user to insert space between tokens *or* to give + pretty-printing rules for the possible combinations, e.g. + + :: + + (** printing ->~ %\ensuremath{\rightarrow\lnot}% *) + + + +Sections +++++++++ + +Sections are introduced by 1 to 4 asterisks at the beginning of a line +followed by a space and the title of the section. One asterisk is a section, +two a subsection, etc. + +.. example:: + + :: + + (** * Well-founded relations + + In this section, we introduce... *) + + +Lists. +++++++ + +List items are introduced by a leading dash. coqdoc uses whitespace to +determine the depth of a new list item and which text belongs in which +list items. A list ends when a line of text starts at or before the +level of indenting of the list’s dash. A list item’s dash must always +be the first non-space character on its line (so, in particular, a +list can not begin on the first line of a comment - start it on the +second line instead). + +.. example:: + + :: + + We go by induction on [n]: + - If [n] is 0... + - If [n] is [S n'] we require... + + two paragraphs of reasoning, and two subcases: + + - In the first case... + - In the second case... + + So the theorem holds. + + + +Rules. +++++++ + +More than 4 leading dashes produce a horizontal rule. + + +Emphasis. ++++++++++ + +Text can be italicized by enclosing it in underscores. A non-identifier +character must precede the leading underscore and follow the trailing +underscore, so that uses of underscores in names aren’t mistaken for +emphasis. Usually, these are spaces or punctuation. + +:: + + This sentence contains some _emphasized text_. + + + +Escaping to |Latex| and HTML. ++++++++++++++++++++++++++++++++ + +Pure |Latex| or HTML material can be inserted using the following +escape sequences: + + ++ ``$...LATEX stuff...$`` inserts some |Latex| material in math mode. + Simply discarded in HTML output. ++ ``%...LATEX stuff...%`` inserts some |Latex| material. Simply + discarded in HTML output. ++ ``#...HTML stuff...#`` inserts some HTML material. Simply discarded in + |Latex| output. + +.. note:: + to simply output the characters ``$``, ``%`` and ``#`` and escaping + their escaping role, these characters must be doubled. + + +Verbatim +++++++++ + +Verbatim material is introduced by a leading ``<<`` and closed by ``>>`` +at the beginning of a line. + +.. example:: + + :: + + Here is the corresponding caml code: + << + let rec fact n = + if n <= 1 then 1 else n * fact (n-1) + >> + + + +Hyperlinks +++++++++++ + +Hyperlinks can be inserted into the HTML output, so that any +identifier is linked to the place of its definition. + +``coqc file.v`` automatically dumps localization information in +``file.glob`` or appends it to a file specified using the option ``--dump-glob +file``. Take care of erasing this global file, if any, when starting +the whole compilation process. + +Then invoke coqdoc or ``coqdoc --glob-from file`` to tell coqdoc to look +for name resolutions in the file ``file`` (it will look in ``file.glob`` +by default). + +Identifiers from the |Coq| standard library are linked to the Coq website +`<http://coq.inria.fr/library/>`_. This behavior can be changed +using command line options ``--no-externals`` and ``--coqlib``; see below. + + +Hiding / Showing parts of the source. ++++++++++++++++++++++++++++++++++++++ + +Some parts of the source can be hidden using command line options ``-g`` +and ``-l`` (see below), or using such comments: + +:: + + + (* begin hide *) + *some Coq material* + (* end hide *) + + +Conversely, some parts of the source which would be hidden can be +shown using such comments: + +:: + + + (* begin show *) + *some Coq material* + (* end show *) + + +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 +hidden by default, but can be made visible with user interaction. + +:: + + + (* begin details *) + *some Coq material* + (* end details *) + + +There is also an alternative syntax available. + +:: + + + (* begin details : Some summary describing the snippet *) + *some Coq material* + (* end details *) + + +Usage +~~~~~ + +coqdoc is invoked on a shell command line as follows: +``coqdoc <options and files>``. +Any command line argument which is not an option is considered to be a +file (even if it starts with a ``-``). |Coq| files are identified by the +suffixes ``.v`` and ``.g`` and |Latex| files by the suffix ``.tex``. + + +:HTML output: This is the default output format. One HTML file is created for + each |Coq| file given on the command line, together with a file + ``index.html`` (unless ``option-no-index is passed``). The HTML pages use a + style sheet named ``style.css``. Such a file is distributed with coqdoc. +:|Latex| output: A single |Latex| file is created, on standard + output. It can be redirected to a file using the option ``-o``. The order of + files on the command line is kept in the final document. |Latex| + files given on the command line are copied ‘as is’ in the final + document . DVI and PostScript can be produced directly with the + options ``-dvi`` and ``-ps`` respectively. +:TEXmacs output: To translate the input files to TEXmacs format, + to be used by the TEXmacs |Coq| interface. + + + +Command line options +++++++++++++++++++++ + + +**Overall options** + + + :--HTML: Select a HTML output. + :--|Latex|: Select a |Latex| output. + :--dvi: Select a DVI output. + :--ps: Select a PostScript output. + :--texmacs: Select a TEXmacs output. + :--stdout: Write output to stdout. + :-o file, --output file: Redirect the output into the file ‘file’ + (meaningless with ``-html``). + :-d dir, --directory dir: Output files into directory ‘dir’ instead of + the current directory (option ``-d`` does not change the filename specified + with the option ``-o``, if any). + :--body-only: Suppress the header and trailer of the final document. + Thus, you can insert the resulting document into a larger one. + :-p string, --preamble string: Insert some material in the |Latex| + preamble, right before ``\begin{document}`` (meaningless with ``-html``). + :--vernac-file file,--tex-file file: Considers the file ‘file’ + respectively as a ``.v`` (or ``.g``) file or a ``.tex`` file. + :--files-from file: Read filenames to be processed from the file ‘file’ as if + they were given on the command line. Useful for program sources split + up into several directories. + :-q, --quiet: Be quiet. Do not print anything except errors. + :-h, --help: Give a short summary of the options and exit. + :-v, --version: Print the version and exit. + + + +**Index options** + + The default behavior is to build an index, for the HTML output only, + into ``index.html``. + + :--no-index: Do not output the index. + :--multi-index: Generate one page for each category and each letter in + the index, together with a top page ``index.html``. + :--index string: Make the filename of the index string instead of + “index”. Useful since “index.html” is special. + + + +**Table of contents option** + + :-toc, --table-of-contents: Insert a table of contents. For a |Latex| + output, it inserts a ``\tableofcontents`` at the beginning of the + document. For a HTML output, it builds a table of contents into + ``toc.html``. + :--toc-depth int: Only include headers up to depth ``int`` in the table of + contents. + + +**Hyperlink options** + + :--glob-from file: Make references using |Coq| globalizations from file + 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 + `<http://coq.inria.fr/library/>`_). This is equivalent to ``--external url + Coq``. + :-R dir coqdir: Recursively map physical directory dir to |Coq| logical + directory ``coqdir`` (similarly to |Coq| option ``-R``). + :-Q dir coqdir: Map physical directory dir to |Coq| logical + directory ``coqdir`` (similarly to |Coq| option ``-Q``). + + .. note:: + + options ``-R`` and ``-Q`` only have + effect on the files *following* them on the command line, so you will + probably need to put this option first. + + +**Title options** + + :-s , --short: Do not insert titles for the files. The default + behavior is to insert a title like “Library Foo” for each file. + :--lib-name string: Print “string Foo” instead of “Library Foo” in + titles. For example “Chapter” and “Module” are reasonable choices. + :--no-lib-name: Print just “Foo” instead of “Library Foo” in titles. + :--lib-subtitles: Look for library subtitles. When enabled, the + beginning of each file is checked for a comment of the form: + + :: + + (** * ModuleName : text *) + + where ``ModuleName`` must be the name of the file. If it is present, the + text is used as a subtitle for the module in appropriate places. + :-t string, --title string: Set the document title. + + +**Contents options** + + :-g, --gallina: Do not print proofs. + :-l, --light: Light mode. Suppress proofs (as with ``-g``) and the following commands: + + + [Recursive] Tactic Definition + + Hint / Hints + + Require + + Transparent / Opaque + + Implicit Argument / Implicits + + Section / Variable / Hypothesis / End + + + + The behavior of options ``-g`` and ``-l`` can be locally overridden using the + ``(* begin show *) … (* end show *)`` environment (see above). + + There are a few options that control the parsing of comments: + + :--parse-comments: Parse regular comments delimited by ``(*`` and ``*)`` as + well. They are typeset inline. + :--plain-comments: Do not interpret comments, simply copy them as + plain-text. + :--interpolate: Use the globalization information to typeset + identifiers appearing in |Coq| escapings inside comments. + +**Language options** + + + The default behavior is to assume ASCII 7 bit input files. + + :-latin1, --latin1: Select ISO-8859-1 input files. It is equivalent to + --inputenc latin1 --charset iso-8859-1. + :-utf8, --utf8: Set --inputenc utf8x for |Latex| output and--charset + utf-8 for HTML output. Also use Unicode replacements for a couple of + standard plain ASCII notations such as → for ``->`` and ∀ for ``forall``. |Latex| + UTF-8 support can be found + at `<http://www.ctan.org/pkg/unicode>`_. For the interpretation of Unicode + characters by |Latex|, extra packages which coqdoc does not provide + by default might be required, such as textgreek for some Greek letters + or ``stmaryrd`` for some mathematical symbols. If a Unicode character is + missing an interpretation in the utf8x input encoding, add + ``\DeclareUnicodeCharacter{code}{LATEX-interpretation}``. Packages + and declarations can be added with option ``-p``. + :--inputenc string: Give a |Latex| input encoding, as an option to |Latex| + package ``inputenc``. + :--charset string: Specify the HTML character set, to be inserted in + the HTML header. + + + +The coqdoc |Latex| style file +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +In case you choose to produce a document without the default |Latex| +preamble (by using option ``--no-preamble``), then you must insert into +your own preamble the command + +:: + + \usepackage{coqdoc} + +The package optionally takes the argument ``[color]`` to typeset +identifiers with colors (this requires the ``xcolor`` package). + +Then you may alter the rendering of the document by redefining some +macros: + +:coqdockw, coqdocid, …: The one-argument macros for typesetting + keywords and identifiers. Defaults are sans-serif for keywords and + italic for identifiers.For example, if you would like a slanted font + for keywords, you may insert + + :: + + \renewcommand{\coqdockw}[1]{\textsl{#1}} + + + anywhere between ``\usepackage{coqdoc}`` and ``\begin{document}``. + + +:coqdocmodule: + One-argument macro for typesetting the title of a ``.v`` + file. Default is + + :: + + \newcommand{\coqdocmodule}[1]{\section*{Module #1}} + + and you may redefine it using ``\renewcommand``. diff --git a/doc/sphinx/using/tools/index.rst b/doc/sphinx/using/tools/index.rst index 4381c4d63d..dfe38dfce9 100644 --- a/doc/sphinx/using/tools/index.rst +++ b/doc/sphinx/using/tools/index.rst @@ -16,5 +16,6 @@ on the `Coq website <https://coq.inria.fr/user-interfaces.html>`_. ../../practical-tools/coq-commands ../../practical-tools/utilities + coqdoc ../../practical-tools/coqide ../../addendum/parallel-proof-processing |