diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/index.rst | 3 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 999 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 592 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 1414 |
5 files changed, 3009 insertions, 1 deletions
diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst index db03693ff9..15e4ff3bc5 100644 --- a/doc/sphinx/index.rst +++ b/doc/sphinx/index.rst @@ -24,6 +24,8 @@ Table of contents .. toctree:: :caption: The proof engine + proof-engine/vernacular-commands + proof-engine/proof-handling proof-engine/tactics proof-engine/detailed-tactic-examples proof-engine/ssreflect-proof-language @@ -38,6 +40,7 @@ Table of contents :caption: Practical tools practical-tools/coq-commands + practical-tools/utilities practical-tools/coqide .. toctree:: diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst new file mode 100644 index 0000000000..620c002ff3 --- /dev/null +++ b/doc/sphinx/practical-tools/utilities.rst @@ -0,0 +1,999 @@ +.. include:: ../replaces.rst + +.. _utilities: + +--------------------- + Utilities +--------------------- + +The distribution provides utilities to simplify some tedious works +beside proof development, tactics writing or documentation. + + +Using Coq as a library +---------------------- + +In previous versions, ``coqmktop`` was used to build custom +toplevels - for example for better debugging or custom static +linking. Nowadays, the preferred method is to use ``ocamlfind``. + +The most basic custom toplevel is built using: + +:: + + % ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg \ + -package coq.toplevel \ + toplevel/coqtop\_bin.ml -o my\_toplevel.native + + +For example, to statically link |L_tac|, you can just do: + +:: + + % ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg \ + -package coq.toplevel -package coq.ltac \ + toplevel/coqtop\_bin.ml -o my\_toplevel.native +and similarly for other plugins. + + +Building a |Coq| project with coq_makefile +------------------------------------------ + +The majority of |Coq| projects are very similar: a collection of ``.v`` +files and eventually some ``.ml`` ones (a |Coq| plugin). The main piece of +metadata needed in order to build the project are the command line +options to ``coqc`` (e.g. ``-R``, ``-I``, see also: Section +:ref:`bycommandline`). Collecting the list of files and options is the job +of the ``_CoqProject`` file. + +A simple example of a ``_CoqProject`` file follows: + +:: + + -R theories/ MyCode + theories/foo.v + theories/bar.v + -I src/ + src/baz.ml4 + src/bazaux.ml + src/qux_plugin.mlpack + + +Currently, both |CoqIDE| and |ProofGeneral| (version ≥ ``4.3pre``) +understand ``_CoqProject`` files and invoke |Coq| with the desired options. + +The ``coq_makefile`` utility can be used to set up a build infrastructure +for the |Coq| project based on makefiles. The recommended way of +invoking ``coq_makefile`` is the following one: + +:: + + coq_makefile -f _CoqProject -o CoqMakefile + + +Such command generates the following files: + +CoqMakefile + is a generic makefile for ``GNU Make`` that provides + targets to build the project (both ``.v`` and ``.ml*`` files), to install it + system-wide in the ``coq-contrib`` directory (i.e. where |Coq| is installed) + as well as to invoke |coqdoc| to generate |HTML| documentation. + +CoqMakefile.conf + contains make variables assignments that reflect + the contents of the ``_CoqProject`` file as well as the path relevant to + |Coq|. + + +An optional file ``CoqMakefile.local`` can be provided by the user in order to +extend ``CoqMakefile``. In particular one can declare custom actions to be +performed before or after the build process. Similarly one can customize the +install target or even provide new targets. Extension points are documented in +paragraph :ref:`coqmakefile:local`. + +The extensions of the files listed in ``_CoqProject`` is used in order to +decide how to build them. In particular: + + ++ |Coq| files must use the ``.v`` extension ++ |OCaml| files must use the ``.ml`` or ``.mli`` extension ++ |OCaml| files that require pre processing for syntax + extensions (like ``VERNAC EXTEND``) must use the ``.ml4`` extension ++ In order to generate a plugin one has to list all |OCaml| + modules (i.e. ``Baz`` for ``baz.ml``) in a ``.mlpack`` file (or ``.mllib`` + file). + + +The use of ``.mlpack`` files has to be preferred over ``.mllib`` files, +since it results in a “packed” plugin: All auxiliary modules (as +``Baz`` and ``Bazaux``) are hidden inside the plugin’s “name space” +(``Qux_plugin``). This reduces the chances of begin unable to load two +distinct plugins because of a clash in their auxiliary module names. + +.. _coqmakefilelocal: + +CoqMakefile.local ++++++++++++++++++ + + + +The optional file ``CoqMakefile.local`` is included by the generated +file ``CoqMakefile``. It can contain two kinds of directives. + +Variable assignment + The variable must belong to the variables listed in the ``Parameters`` section of the generated makefile. + Here we describe only few of them. + :CAMLPKGS: + can be used to specify third party findlib packages, and is + passed to the OCaml compiler on building or linking of modules. Eg: + ``-package yojson``. + :CAMLFLAGS: + can be used to specify additional flags to the |OCaml| + compiler, like ``-bin-annot`` or ``-w``.... + :COQC, COQDEP, COQDOC: + can be set in order to use alternative binaries + (e.g. wrappers) + :COQ_SRC_SUBDIRS: can be extended by including other paths in which ``*.cm*`` files are searched. For example ``COQ\_SRC\_SUBDIRS+=user-contrib/Unicoq`` lets you build a plugin containing OCaml code that depends on the OCaml code of ``Unicoq``. + +Rule extension + The following makefile rules can be extended. + + .. example :: + + :: + + pre-all:: + echo "This line is print before making the all target" + install-extra:: + cp ThisExtraFile /there/it/goes + + ``pre-all::`` + run before the all target. One can use this to configure + the project, or initialize sub modules or check dependencies are met. + + ``post-all::`` + run after the all target. One can use this to run a test + suite, or compile extracted code. + + + ``install-extra::`` + run after install. One can use this to install extra files. + + ``install-doc::`` + One can use this to install extra doc. + + ``uninstall::`` + \ + + ``uninstall-doc::`` + \ + + ``clean::`` + \ + + ``cleanall::`` + \ + + ``archclean::`` + \ + + ``merlin-hook::`` + One can append lines to the generated .merlin file extending this + target. + +Timing targets and performance testing +++++++++++++++++++++++++++++++++++++++ + +The generated ``Makefile`` supports the generation of two kinds of timing +data: per-file build-times, and per-line times for an individual file. + +The following targets and Makefile variables allow collection of per- +file timing data: + + ++ ``TIMED=1`` + passing this variable will cause ``make`` to emit a line + describing the user-space build-time and peak memory usage for each + file built. + + .. note:: + On ``Mac OS``, this works best if you’ve installed ``gnu-time``. + + .. example:: + For example, the output of ``make TIMED=1`` may look like + this: + + :: + + COQDEP Fast.v + COQDEP Slow.v + COQC Slow.v + Slow (user: 0.34 mem: 395448 ko) + COQC Fast.v + Fast (user: 0.01 mem: 45184 ko) + ++ ``pretty-timed`` + this target stores the output of ``make TIMED=1`` into + ``time-of-build.log``, and displays a table of the times, sorted from + slowest to fastest, which is also stored in ``time-of-build-pretty.log``. + If you want to construct the ``log`` for targets other than the default + one, you can pass them via the variable ``TGTS``, e.g., ``make pretty-timed + TGTS="a.vo b.vo"``. + + .. :: + This target requires ``python`` to build the table. + + .. note:: + This target will *append* to the timing log; if you want a + fresh start, you must remove the ``filetime-of-build.log`` or + ``run make cleanall``. + + .. example:: + + For example, the output of ``make pretty-timed`` may look like this: + + :: + + COQDEP Fast.v + COQDEP Slow.v + COQC Slow.v + Slow (user: 0.36 mem: 393912 ko) + COQC Fast.v + Fast (user: 0.05 mem: 45992 ko) + Time | File Name + -------------------- + 0m00.41s | Total + -------------------- + 0m00.36s | Slow + 0m00.05s | Fast + + ++ ``print-pretty-timed-diff`` + this target builds a table of timing + changes between two compilations; run ``make make-pretty-timed-before`` to + build the log of the “before” times, and run ``make make-pretty-timed- + after`` to build the log of the “after” times. The table is printed on + the command line, and stored in ``time-of-build-both.log``. This target is + most useful for profiling the difference between two commits to a + repo. + + .. note:: + This target requires ``python`` to build the table. + + .. note:: + The ``make-pretty-timed-before`` and ``make-pretty-timed-after`` targets will + *append* to the timing log; if you want a fresh start, you must remove + the files ``time-of-build-before.log`` and ``time-of-build-after.log`` or run + ``make cleanall`` *before* building either the “before” or “after” + targets. + + .. note:: + The table will be sorted first by absolute time + differences rounded towards zero to a whole-number of seconds, then by + times in the “after” column, and finally lexicographically by file + name. This will put the biggest changes in either direction first, and + will prefer sorting by build-time over subsecond changes in build time + (which are frequently noise); lexicographic sorting forces an order on + files which take effectively no time to compile. + + .. example:: + For example, the output table from + ``make print-pretty-timed-diff`` may look like this: + + :: + + After | File Name | Before || Change | % Change + -------------------------------------------------------- + 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% + + +The following targets and ``Makefile`` variables allow collection of per- +line timing data: + + ++ ``TIMING=1`` + passing this variable will cause ``make`` to use ``coqc -time`` to + write to a ``.v.timing`` file for each ``.v`` file compiled, which contains + line-by-line timing information. + + .. example:: + For example, running ``make all TIMING=1`` may result in a file like this: + + :: + + Chars 0 - 26 [Require~Coq.ZArith.BinInt.] 0.157 secs (0.128u,0.028s) + Chars 27 - 68 [Declare~Reduction~comp~:=~vm_c...] 0. secs (0.u,0.s) + Chars 69 - 162 [Definition~foo0~:=~Eval~comp~i...] 0.153 secs (0.136u,0.019s) + Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] 0.239 secs (0.236u,0.s) + ++ ``print-pretty-single-time-diff`` + :: + + print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing + this target will make a sorted table of the per-line timing differences + between the timing logs in the ``BEFORE`` and ``AFTER`` files, display it, and + save it to the file specified by the ``TIME_OF_PRETTY_BUILD_FILE`` variable, + which defaults to ``time-of-build-pretty.log``. + To generate the ``.v.before-timing`` or ``.v.after-timing`` files, you should + pass ``TIMING=before`` or ``TIMING=after`` rather than ``TIMING=1``. + + .. note:: + The sorting used here is the same as in the ``print-pretty-timed -diff`` target. + + .. note:: + This target requires python to build the table. + + .. example:: + For example, running ``print-pretty-single-time-diff`` might give a table like this: + + :: + + After | Code | Before || Change | % Change + --------------------------------------------------------------------------------------------------- + 0m00.50s | Total | 0m04.17s || -0m03.66s | -87.96% + --------------------------------------------------------------------------------------------------- + 0m00.145s | Chars 069 - 162 [Definition~foo0~:=~Eval~comp~i...] | 0m00.192s || -0m00.04s | -24.47% + 0m00.126s | Chars 000 - 026 [Require~Coq.ZArith.BinInt.] | 0m00.143s || -0m00.01s | -11.88% + N/A | Chars 027 - 068 [Declare~Reduction~comp~:=~nati...] | 0m00.s || +0m00.00s | N/A + 0m00.s | Chars 027 - 068 [Declare~Reduction~comp~:=~vm_c...] | N/A || +0m00.00s | N/A + 0m00.231s | Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] | 0m03.836s || -0m03.60s | -93.97% + + ++ ``all.timing.diff``, ``path/to/file.v.timing.diff`` + The ``path/to/file.v.timing.diff`` target will make a ``.v.timing.diff`` file for + the corresponding ``.v`` file, with a table as would be generated by + the ``print-pretty-single-time-diff`` target; it depends on having already + made the corresponding ``.v.before-timing`` and ``.v.after-timing`` files, + which can be made by passing ``TIMING=before`` and ``TIMING=after``. + The ``all.timing.diff`` target will make such timing difference files for + all of the ``.v`` files that the ``Makefile`` knows about. It will fail if + some ``.v.before-timing`` or ``.v.after-timing`` files don’t exist. + + .. note:: + This target requires python to build the table. + + +Reusing/extending the generated Makefile +++++++++++++++++++++++++++++++++++++++++ + +Including the generated makefile with an include directive is +discouraged. The contents of this file, including variable names and +status of rules shall change in the future. Users are advised to +include ``Makefile.conf`` or call a target of the generated Makefile as in +``make -f Makefile target`` from another Makefile. + +One way to get access to all targets of the generated ``CoqMakefile`` is to +have a generic target for invoking unknown targets. + +.. example:: + + :: + + # KNOWNTARGETS will not be passed along to CoqMakefile + KNOWNTARGETS := CoqMakefile extra-stuff extra-stuff2 + # KNOWNFILES will not get implicit targets from the final rule, and so + # depending on them won't invoke the submake + # Warning: These files get declared as PHONY, so any targets depending + # on them always get rebuilt + KNOWNFILES := Makefile _CoqProject + + .DEFAULT_GOAL := invoke-coqmakefile + + CoqMakefile: Makefile _CoqProject + $(COQBIN)coq_makefile -f _CoqProject -o CoqMakefile + + invoke-coqmakefile: CoqMakefile + $(MAKE) --no-print-directory -f CoqMakefile $(filter-out $(KNOWNTARGETS),$(MAKECMDGOALS)) + + .PHONY: invoke-coqmakefile $(KNOWNFILES) + + #################################################################### + ## Your targets here ## + #################################################################### + + # This should be the last rule, to handle any targets not declared above + %: invoke-coqmakefile + @true + + + +Building a subset of the targets with -j +++++++++++++++++++++++++++++++++++++++++ + +To build, say, two targets foo.vo and bar.vo in parallel one can use +``make only TGTS="foo.vo bar.vo" -j``. + +.. note:: + + ``make foo.vo bar.vo -j`` has a different meaning for the make + utility, in particular it may build a shared prerequisite twice. + + +.. note:: + + For users of coq_makefile with version < 8.7 + + + Support for “sub-directory” is deprecated. To perform actions before + or after the build (like invoking ``make`` on a subdirectory) one can hook + in pre-all and post-all extension points. + + ``-extra-phony`` and ``-extra`` are deprecated. To provide additional target + (``.PHONY`` or not) please use ``CoqMakefile.local``. + + + +Modules dependencies +-------------------- + +In order to compute modules dependencies (so to use ``make``), |Coq| comes +with an appropriate tool, ``coqdep``. + +``coqdep`` computes inter-module dependencies for |Coq| and |OCaml| +programs, and prints the dependencies on the standard output in a +format readable by make. When a directory is given as argument, it is +recursively looked at. + +Dependencies of |Coq| modules are computed by looking at ``Require`` +commands (``Require``, ``Require Export``, ``Require Import``), but also at the +command ``Declare ML Module``. + +Dependencies of |OCaml| modules are computed by looking at +`open` commands and the dot notation *module.value*. However, this is +done approximately and you are advised to use ``ocamldep`` instead for the +|OCaml| modules dependencies. + +See the man page of ``coqdep`` for more details and options. + +The build infrastructure generated by ``coq_makefile`` uses ``coqdep`` to +automatically compute the dependencies among the files part of the +project. + + +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 the |Coq| + sources, readable for a human and not only for the proof assistant; +#. to help the user navigating in 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 pending ``*)``. 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. + +Pre-formatted 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. One of the |Latex| or |HTML| text 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 leading stars (i.e. at the beginning +of the line) followed by a space. One star is a section, two stars a +sub-section, etc. The section title is given on the remaining of the +line. + +.. 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 placing 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 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 into the file ``file`` (it will look in ``file.glob`` +by default). + +Identifiers from the |Coq| standard library are linked to the Coq web +site at `<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. + + +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. 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 with 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 + current directory (option ``-d`` does not change the filename specified + with 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 file names to process in 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** + + 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. + + +**Hyperlinks 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: Map physical directory dir to |Coq| logical + directory ``coqdir`` (similarly to |Coq| option ``-R``). + + .. note:: + option ``-R`` only has + effect on the files *following* it 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 to drive the parsing of comments: + + :--parse-comments: Parses 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** + + + Default behavior is to assume ASCII 7 bits 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``. + +Embedded Coq phrases inside |Latex| documents +--------------------------------------------- + +When writing a documentation about a proof development, one may want +to insert |Coq| phrases inside a |Latex| document, possibly together +with the corresponding answers of the system. We provide a mechanical +way to process such |Coq| phrases embedded in |Latex| files: the ``coq-tex`` +filter. This filter extracts |Coq| phrases embedded in |Latex| files, +evaluates them, and insert the outcome of the evaluation after each +phrase. + +Starting with a file ``file.tex`` containing |Coq| phrases, the ``coq-tex`` +filter produces a file named ``file.v.tex`` with the Coq outcome. + +There are options to produce the |Coq| parts in smaller font, italic, +between horizontal rules, etc. See the man page of ``coq-tex`` for more +details. + +|Coq| and |GNU| |Emacs| +----------------------- + + +The |Coq| |Emacs| mode +~~~~~~~~~~~~~~~~~~~~~~~~~ + +|Coq| comes with a Major mode for |GNU| |Emacs|, ``gallina.el``. This mode +provides syntax highlighting and also a rudimentary indentation +facility in the style of the ``Caml`` |GNU| |Emacs| mode. + +Add the following lines to your ``.emacs`` file: + +:: + + (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist)) + (autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t) + + +The |Coq| major mode is triggered by visiting a file with extension ``.v``, +or manually with the command ``M-x coq-mode``. It gives you the correct +syntax table for the |Coq| language, and also a rudimentary indentation +facility: + + ++ pressing ``Tab`` at the beginning of a line indents the line like the + line above; ++ extra ``Tab``s increase the indentation level (by 2 spaces by default); ++ ``M-Tab`` decreases the indentation level. + + +An inferior mode to run |Coq| under |Emacs|, by Marco Maggesi, is also +included in the distribution, in file ``inferior-coq.el``. Instructions to +use it are contained in this file. + + +Proof General +~~~~~~~~~~~~~ + +|ProofGeneral| is a generic interface for proof assistants based on +|Emacs|. The main idea is that the |Coq| commands you are editing are sent +to a |Coq| toplevel running behind |Emacs| and the answers of the system +automatically inserted into other |Emacs| buffers. Thus you don’t need +to copy-paste the |Coq| material from your files to the |Coq| toplevel or +conversely from the |Coq| toplevel to some files. + +|ProofGeneral| is developed and distributed independently of the system +|Coq|. It is freely available at `<https://proofgeneral.github.io/>`_. + + +Module specification +-------------------- + +Given a |Coq| vernacular file, the gallina filter extracts its +specification (inductive types declarations, definitions, type of +lemmas and theorems), removing the proofs parts of the file. The |Coq| +file ``file.v`` gives birth to the specification file ``file.g`` (where +the suffix ``.g`` stands for |Gallina|). + +See the man page of ``gallina`` for more details and options. + + +Man pages +--------- + +There are man pages for the commands ``coqdep``, ``gallina`` and ``coq-tex``. Man +pages are installed at installation time (see installation +instructions in file ``INSTALL``, step 6). diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst new file mode 100644 index 0000000000..52cde52c69 --- /dev/null +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -0,0 +1,592 @@ +.. include:: ../replaces.rst +.. _proofhandling: + +------------------- + Proof handling +------------------- + +In |Coq|’s proof editing mode all top-level commands documented in +Chapter :ref:`vernacularcommands` remain available and the user has access to specialized +commands dealing with proof development pragmas documented in this +section. He can also use some other specialized commands called +*tactics*. They are the very tools allowing the user to deal with +logical reasoning. They are documented in Chapter :ref:`tactics`. +When switching in editing proof mode, the prompt ``Coq <`` is changed into +``ident <`` where ``ident`` is the declared name of the theorem currently +edited. + +At each stage of a proof development, one has a list of goals to +prove. Initially, the list consists only in the theorem itself. After +having applied some tactics, the list of goals contains the subgoals +generated by the tactics. + +To each subgoal is associated a number of hypotheses called the *local +context* of the goal. Initially, the local context contains the local +variables and hypotheses of the current section (see Section :ref:`TODO_gallina_assumptions`) +and the local variables and hypotheses of the theorem statement. It is +enriched by the use of certain tactics (see e.g. ``intro`` in Section +:ref:`managingthelocalcontext`). + +When a proof is completed, the message ``Proof completed`` is displayed. +One can then register this proof as a defined constant in the +environment. Because there exists a correspondence between proofs and +terms of λ-calculus, known as the *Curry-Howard isomorphism* [[How80]_, +[Bar81]_, [Gir89]_, [Hue88]_ ], |Coq| +stores proofs as terms of |Cic|. Those terms +are called *proof terms*. + + +.. exn:: No focused proof + +Coq raises this error message when one attempts to use a proof editing command +out of the proof editing mode. + +Switching on/off the proof editing mode +------------------------------------------- + +The proof editing mode is entered by asserting a statement, which +typically is the assertion of a theorem: + +.. cmd:: Theorem @ident [@binders] : @form. + +The list of assertion commands is given in Section :ref:TODO-assertions_and_proof`. The +command ``Goal`` can also be used. + +.. cmd:: Goal @form. + +This is intended for quick assertion of statements, without knowing in +advance which name to give to the assertion, typically for quick +testing of the provability of a statement. If the proof of the +statement is eventually completed and validated, the statement is then +bound to the name ``Unnamed_thm`` (or a variant of this name not already +used for another statement). + +.. cmd:: Qed. + +This command is available in interactive editing proof mode when the +proof is completed. Then ``Qed`` extracts a proof term from the proof +script, switches back to Coq top-level and attaches the extracted +proof term to the declared name of the original goal. This name is +added to the environment as an ``Opaque`` constant. + + +.. exn:: Attempt to save an incomplete proof + +.. note:: + + Sometimes an error occurs when building the proof term, because + tactics do not enforce completely the term construction + constraints. + +The user should also be aware of the fact that since the +proof term is completely rechecked at this point, one may have to wait +a while when the proof is large. In some exceptional cases one may +even incur a memory overflow. + +.. cmdv:: Defined. + +Defines the proved term as a transparent constant. + +.. cmdv:: Save @ident. + +Forces the name of the original goal to be :n:`@ident`. This +command (and the following ones) can only be used if the original goal +has been opened using the ``Goal`` command. + + +.. cmd:: Admitted. + +This command is available in interactive editing proof mode to give up +the current proof and declare the initial goal as an axiom. + + +.. cmd:: Proof @term. + +This command applies in proof editing mode. It is equivalent to + +.. cmd:: exact @term. Qed. + +That is, you have to give the full proof in one gulp, as a +proof term (see Section :ref:`applyingtheorems`). + + +.. cmdv:: Proof. + +Is a noop which is useful to delimit the sequence of tactic commands +which start a proof, after a ``Theorem`` command. It is a good practice to +use ``Proof``. as an opening parenthesis, closed in the script with a +closing ``Qed``. + + +See also: ``Proof with tactic.`` in Section +:ref:`setimpautotactics`. + + +.. cmd:: Proof using @ident1 ... @identn. + +This command applies in proof editing mode. It declares the set of +section variables (see :ref:`TODO-gallina-assumptions`) used by the proof. At ``Qed`` time, the +system will assert that the set of section variables actually used in +the proof is a subset of the declared one. + +The set of declared variables is closed under type dependency. For +example if ``T`` is variable and a is a variable of type ``T``, the commands +``Proof using a`` and ``Proof using T a``` are actually equivalent. + + +.. cmdv:: Proof using @ident1 ... @identn with @tactic. + +in Section :ref:`setimpautotactics`. + +.. cmdv:: Proof using All. + +Use all section variables. + + +.. cmdv:: Proof using Type. + +.. cmdv:: Proof using. + +Use only section variables occurring in the statement. + + +.. cmdv:: Proof using Type*. + +The ``*`` operator computes the forward transitive closure. E.g. if the +variable ``H`` has type ``p < 5`` then ``H`` is in ``p*`` since ``p`` occurs in the type +of ``H``. ``Type*`` is the forward transitive closure of the entire set of +section variables occurring in the statement. + + +.. cmdv:: Proof using -(@ident1 ... @identn). + +Use all section variables except :n:`@ident1` ... :n:`@identn`. + + +.. cmdv:: Proof using @collection1 + @collection2 . + + +.. cmdv:: Proof using @collection1 - @collection2 . + + +.. cmdv:: Proof using @collection - ( @ident1 ... @identn ). + + +.. cmdv:: Proof using @collection * . + +Use section variables being, respectively, in the set union, set +difference, set complement, set forward transitive closure. See +Section :ref:`nameaset` to know how to form a named collection. The ``*`` operator +binds stronger than ``+`` and ``-``. + + +Proof using options +``````````````````` + +The following options modify the behavior of ``Proof using``. + + +.. cmdv:: Set Default Proof Using "@expression". + +Use :n:`@expression` as the default ``Proof``` using value. E.g. ``Set Default +Proof Using "a b"``. will complete all ``Proof`` commands not followed by a +using part with using ``a`` ``b``. + + +.. cmdv:: Set Suggest Proof Using. + +When ``Qed`` is performed, suggest a using annotation if the user did not +provide one. + +.. _`nameaset`: + +Name a set of section hypotheses for ``Proof using`` +```````````````````````````````````````````````````` + +The command ``Collection`` can be used to name a set of section +hypotheses, with the purpose of making ``Proof using`` annotations more +compact. + + +.. cmdv:: Collection Some := x y z. + +Define the collection named "Some" containing ``x``, ``y`` and ``z``. + + +.. cmdv:: Collection Fewer := Some - z. + +Define the collection named "Fewer" containing only ``x`` and ``y``. + + +.. cmdv:: Collection Many := Fewer + Some. +.. cmdv:: Collection Many := Fewer - Some. + +Define the collection named "Many" containing the set union or set +difference of "Fewer" and "Some". + + +.. cmdv:: Collection Many := Fewer - (x y). + +Define the collection named "Many" containing the set difference of +"Fewer" and the unnamed collection ``x`` ``y``. + + +.. cmd:: Abort. + +This command cancels the current proof development, switching back to +the previous proof development, or to the |Coq| toplevel if no other +proof was edited. + + +.. exn:: No focused proof (No proof-editing in progress) + + + +.. cmdv:: Abort @ident. + +Aborts the editing of the proof named :n:`@ident`. + +.. cmdv:: Abort All. + +Aborts all current goals, switching back to the |Coq| +toplevel. + + + +.. cmd:: Existential @num := @term. + +This command instantiates an existential variable. :n:`@num` is an index in +the list of uninstantiated existential variables displayed by ``Show +Existentials`` (described in Section :ref:`requestinginformation`). + +This command is intended to be used to instantiate existential +variables when the proof is completed but some uninstantiated +existential variables remain. To instantiate existential variables +during proof edition, you should use the tactic instantiate. + + +See also: ``instantiate (num:= term).`` in Section +:ref:`TODO-controllingtheproofflow`. +See also: ``Grab Existential Variables.`` below. + + +.. cmd:: Grab Existential Variables. + +This command can be run when a proof has no more goal to be solved but +has remaining uninstantiated existential variables. It takes every +uninstantiated existential variable and turns it into a goal. + + +Navigation in the proof tree +-------------------------------- + + +.. cmd:: Undo. + +This command cancels the effect of the last command. Thus, it +backtracks one step. + + +.. cmdv:: Undo @num. + +Repeats Undo :n:`@num` times. + +.. cmdv:: Restart. + +This command restores the proof editing process to the original goal. + + +.. exn:: No focused proof to restart + + +.. cmd:: Focus. + +This focuses the attention on the first subgoal to prove and the +printing of the other subgoals is suspended until the focused subgoal +is solved or unfocused. This is useful when there are many current +subgoals which clutter your screen. + + +.. cmdv:: Focus @num. + +This focuses the attention on the :n:`@num` th subgoal to +prove. + +*This command is deprecated since 8.8*: prefer the use of bullets or +focusing brackets instead, including :n:`@num : %{` + +.. cmd:: Unfocus. + +This command restores to focus the goal that were suspended by the +last ``Focus`` command. + +*This command is deprecated since 8.8.* + +.. cmd:: Unfocused. + +Succeeds if the proof is fully unfocused, fails is there are some +goals out of focus. + + +.. cmd:: %{ %| %} + +The command ``{`` (without a terminating period) focuses on the first +goal, much like ``Focus.`` does, however, the subproof can only be +unfocused when it has been fully solved ( *i.e.* when there is no +focused goal left). Unfocusing is then handled by ``}`` (again, without a +terminating period). See also example in next section. + +Note that when a focused goal is proved a message is displayed +together with a suggestion about the right bullet or ``}`` to unfocus it +or focus the next one. + +.. cmdv:: @num: %{ + +This focuses on the :n:`@num` th subgoal to prove. + +Error messages: + +.. exn:: This proof is focused, but cannot be unfocused this way + +You are trying to use ``}`` but the current subproof has not been fully solved. + +.. exn:: No such goal + +.. exn:: Brackets only support the single numbered goal selector + + +See also error messages about bullets below. + +Bullets +``````` + +Alternatively to ``{`` and ``}``, proofs can be structured with bullets. The +use of a bullet ``b`` for the first time focuses on the first goal ``g``, the +same bullet cannot be used again until the proof of ``g`` is completed, +then it is mandatory to focus the next goal with ``b``. The consequence is +that ``g`` and all goals present when ``g`` was focused are focused with the +same bullet ``b``. See the example below. + +Different bullets can be used to nest levels. The scope of bullet does +not go beyond enclosing ``{`` and ``}``, so bullets can be reused as further +nesting levels provided they are delimited by these. Available bullets +are ``-``, ``+``, ``*``, ``--``, ``++``, ``**``, ``---``, ``+++``, ``***``, ... (without a terminating period). + +Note again that when a focused goal is proved a message is displayed +together with a suggestion about the right bullet or ``}`` to unfocus it +or focus the next one. + +.. note:: + + In Proof General (``Emacs`` interface to |Coq|), you must use + bullets with the priority ordering shown above to have a correct + indentation. For example ``-`` must be the outer bullet and ``**`` the inner + one in the example below. + +The following example script illustrates all these features: + +.. example:: + .. coqtop:: all + + Goal (((True /\ True) /\ True) /\ True) /\ True. + Proof. + split. + - split. + + split. + ** { split. + - trivial. + - trivial. + } + ** trivial. + + trivial. + - assert True. + { trivial. } + assumption. + + +.. exn:: Wrong bullet @bullet1 : Current bullet @bullet2 is not finished. + +Before using bullet :n:`@bullet1` again, you should first finish proving the current focused goal. Note that :n:`@bullet1` and :n:`@bullet2` may be the same. + +.. exn:: Wrong bullet @bullet1 : Bullet @bullet2 is mandatory here. + +You must put :n:`@bullet2` to focus next goal. No other bullet is allowed here. + +.. exn:: No such goal. Focus next goal with bullet @bullet. + +You tried to applied a tactic but no goal where under focus. Using :n:`@bullet` is mandatory here. + +.. exn:: No such goal. Try unfocusing with %{. + +You just finished a goal focused by ``{``, you must unfocus it with ``}``. + +Set Bullet Behavior +``````````````````` + +The bullet behavior can be controlled by the following commands. + +.. opt:: Bullet Behavior "None". + +This makes bullets inactive. + +.. opt:: Bullet Behavior "Strict Subproofs". + +This makes bullets active (this is the default behavior). + + + +Requesting information +---------------------- + + +.. cmd:: Show. + +This command displays the current goals. + + +.. cmdv:: Show @num + +Displays only the :n:`@num`-th subgoal. + +.. exn:: No such goal +.. exn:: No focused proof + +.. cmdv:: Show @ident. + +Displays the named goal :n:`@ident`. This is useful in +particular to display a shelved goal but only works if the +corresponding existential variable has been named by the user +(see :ref:`exvariables`) as in the following example. + +.. example:: + + .. coqtop:: all + + Goal exists n, n = 0. + eexists ?[n]. + Show n. + +.. cmdv:: Show Script. + +Displays the whole list of tactics applied from the +beginning of the current proof. This tactics script may contain some +holes (subgoals not yet proved). They are printed under the form + +``<Your Tactic Text here>``. + +.. cmdv:: Show Proof. + +It displays the proof term generated by the tactics +that have been applied. If the proof is not completed, this term +contain holes, which correspond to the sub-terms which are still to be +constructed. These holes appear as a question mark indexed by an +integer, and applied to the list of variables in the context, since it +may depend on them. The types obtained by abstracting away the context +from the type of each hole-placer are also printed. + +.. cmdv:: Show Conjectures. + +It prints the list of the names of all the +theorems that are currently being proved. As it is possible to start +proving a previous lemma during the proof of a theorem, this list may +contain several names. + +.. cmdv:: Show Intro. + +If the current goal begins by at least one product, +this command prints the name of the first product, as it would be +generated by an anonymous ``intro``. The aim of this command is to ease +the writing of more robust scripts. For example, with an appropriate +Proof General macro, it is possible to transform any anonymous ``intro`` +into a qualified one such as ``intro y13``. In the case of a non-product +goal, it prints nothing. + +.. cmdv:: Show Intros. + +This command is similar to the previous one, it +simulates the naming process of an intros. + +.. cmdv:: Show Existentials. + +It displays the set of all uninstantiated +existential variables in the current proof tree, along with the type +and the context of each variable. + +.. cmdv:: Show Match @ident. + +This variant displays a template of the Gallina +``match`` construct with a branch for each constructor of the type +:n:`@ident` + +.. example:: + .. coqtop:: all + + Show Match nat. + +.. exn:: Unknown inductive type + +.. exn:: Show Universes. + +It displays the set of all universe constraints and +its normalized form at the current stage of the proof, useful for +debugging universe inconsistencies. + + +.. cmd:: Guarded. + +Some tactics (e.g. refine :ref:`applyingtheorems`) allow to build proofs using +fixpoint or co-fixpoint constructions. Due to the incremental nature +of interactive proof construction, the check of the termination (or +guardedness) of the recursive calls in the fixpoint or cofixpoint +constructions is postponed to the time of the completion of the proof. + +The command ``Guarded`` allows checking if the guard condition for +fixpoint and cofixpoint is violated at some time of the construction +of the proof without having to wait the completion of the proof. + + +Controlling the effect of proof editing commands +------------------------------------------------ + + +.. opt:: Hyps Limit @num. + +This option controls the maximum number of hypotheses displayed in goals +after the application of a tactic. All the hypotheses remain usable +in the proof development. +When unset, it goes back to the default mode which is to print all +available hypotheses. + + +.. opt:: Automatic Introduction. + +This option controls the way binders are handled +in assertion commands such as ``Theorem ident [binders] : form``. When the +option is set, which is the default, binders are automatically put in +the local context of the goal to prove. + +The option can be unset by issuing ``Unset Automatic Introduction``. When +the option is unset, binders are discharged on the statement to be +proved and a tactic such as intro (see Section :ref:`managingthelocalcontext`) has to be +used to move the assumptions to the local context. + + +Controlling memory usage +------------------------ + +When experiencing high memory usage the following commands can be used +to force |Coq| to optimize some of its internal data structures. + + +.. cmd:: Optimize Proof. + +This command forces |Coq| to shrink the data structure used to represent +the ongoing proof. + + +.. cmd:: Optimize Heap. + +This command forces the |OCaml| runtime to perform a heap compaction. +This is in general an expensive operation. +See: `OCaml Gc <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_ +There is also an analogous tactic ``optimize_heap`` (see~:ref:`tactic-optimizeheap`) diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index da34e3b55b..2af73c28e5 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -1635,7 +1635,7 @@ analysis on inductive or co-inductive objects (see :ref:`TODO-4.5`). .. tacv:: elim @term using @term .. tacv:: elim @term using @term with @bindings_list - Allows the user to give explicitly an elimination predicate :n:`@term` that + Allows the user to give explicitly an induction principle :n:`@term` that is not the standard one for the underlying inductive type of :n:`@term`. The :n:`@bindings_list` clause allows instantiating premises of the type of :n:`@term`. diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst new file mode 100644 index 0000000000..0bb6eea233 --- /dev/null +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -0,0 +1,1414 @@ +.. include:: ../preamble.rst +.. include:: ../replaces.rst + +.. _vernacularcommands: + +Vernacular commands +============================= + +.. _displaying: + +Displaying +-------------- + + +.. _Print: + +.. cmd:: Print @qualid. + +This command displays on the screen information about the declared or +defined object referred by :n:`@qualid`. + + +Error messages: + + +.. exn:: @qualid not a defined object + +.. exn:: Universe instance should have length :n:`num`. + +.. exn:: This object does not support universe names. + + +Variants: + + +.. cmdv:: Print Term @qualid. + +This is a synonym to ``Print`` :n:`@qualid` when :n:`@qualid` +denotes a global constant. + +.. cmdv:: About @qualid. + +This displays various information about the object +denoted by :n:`@qualid`: its kind (module, constant, assumption, inductive, +constructor, abbreviation, …), long name, type, implicit arguments and +argument scopes. It does not print the body of definitions or proofs. + +.. cmdv:: Print @qualid\@@name + +This locally renames the polymorphic universes of :n:`@qualid`. +An underscore means the raw universe is printed. +This form can be used with ``Print Term`` and ``About``. + +.. cmd:: Print All. + +This command displays information about the current state of the +environment, including sections and modules. + + +Variants: + + +.. cmdv:: Inspect @num. + +This command displays the :n:`@num` last objects of the +current environment, including sections and modules. + +.. cmdv:: Print Section @ident. + +The name :n:`@ident` should correspond to a currently open section, +this command displays the objects defined since the beginning of this +section. + + +.. _flags-options-tables: + +Flags, Options and Tables +----------------------------- + +|Coq| configurability is based on flags (e.g. Set Printing All in +Section :ref:`TODO-2.9-printing-full`), options (e.g. ``Set Printing Widthinteger`` in Section +:ref:`TODO-6.9.6-set-printing-width`), or tables (e.g. ``Add Printing Record ident``, in Section +:ref:`TODO-2.2.4-add-printing-record`). The names of flags, options and tables are made of non-empty sequences of identifiers +(conventionally with capital initial +letter). The general commands handling flags, options and tables are +given below. + +.. TODO : flag is not a syntax entry + +.. cmd:: Set @flag. + +This command switches :n:`@flag` on. The original state of :n:`@flag` is restored +when the current module ends. + + +Variants: + + +.. cmdv:: Local Set @flag. + +This command switches :n:`@flag` on. The original state +of :n:`@flag` is restored when the current *section* ends. + +.. cmdv:: Global Set @flag. + +This command switches :n:`@flag` on. The original state +of :n:`@flag` is *not* restored at the end of the module. Additionally, if +set in a file, :n:`@flag` is switched on when the file is `Require`-d. + + + +.. cmd:: Unset @flag. + +This command switches :n:`@flag` off. The original state of :n:`@flag` is restored +when the current module ends. + + +Variants: + +.. cmdv:: Local Unset @flag. + +This command switches :n:`@flag` off. The original +state of :n:`@flag` is restored when the current *section* ends. + +.. cmdv:: Global Unset @flag. + +This command switches :n:`@flag` off. The original +state of :n:`@flag` is *not* restored at the end of the module. Additionally, +if set in a file, :n:`@flag` is switched off when the file is `Require`-d. + + + +.. cmd:: Test @flag. + +This command prints whether :n:`@flag` is on or off. + + +.. cmd:: Set @option @value. + +This command sets :n:`@option` to :n:`@value`. The original value of ` option` is +restored when the current module ends. + + +Variants: + +.. TODO : option and value are not syntax entries + +.. cmdv:: Local Set @option @value. + +This command sets :n:`@option` to :n:`@value`. The +original value of :n:`@option` is restored at the end of the module. + +.. cmdv:: Global Set @option @value. + +This command sets :n:`@option` to :n:`@value`. The +original value of :n:`@option` is *not* restored at the end of the module. +Additionally, if set in a file, :n:`@option` is set to value when the file +is `Require`-d. + + + +.. cmd:: Unset @option. + +This command resets option to its default value. + + +Variants: + + +.. cmdv:: Local Unset @option. + +This command resets :n:`@option` to its default +value. The original state of :n:`@option` is restored when the current +*section* ends. + +.. cmdv:: Global Unset @option. + +This command resets :n:`@option` to its default +value. The original state of :n:`@option` is *not* restored at the end of the +module. Additionally, if unset in a file, :n:`@option` is reset to its +default value when the file is `Require`-d. + + + +.. cmd:: Test @option. + +This command prints the current value of :n:`@option`. + + +.. TODO : table is not a syntax entry + +.. cmd:: Add @table @value. +.. cmd:: Remove @table @value. +.. cmd:: Test @table @value. +.. cmd:: Test @table for @value. +.. cmd:: Print Table @table. + +These are general commands for tables. + +.. cmd:: Print Options. + +This command lists all available flags, options and tables. + + +Variants: + + +.. cmdv:: Print Tables. + +This is a synonymous of ``Print Options``. + + +.. _requests-to-the-environment: + +Requests to the environment +------------------------------- + +.. cmd:: Check @term. + +This command displays the type of :n:`@term`. When called in proof mode, the +term is checked in the local context of the current subgoal. + + +Variants: + +.. TODO : selector is not a syntax entry + +.. cmdv:: @selector: Check @term. + +specifies on which subgoal to perform typing +(see Section :ref:`TODO-8.1-invocation-of-tactics`). + +.. TODO : convtactic is not a syntax entry + +.. cmd:: Eval @convtactic in @term. + +This command performs the specified reduction on :n:`@term`, and displays +the resulting term with its type. The term to be reduced may depend on +hypothesis introduced in the first subgoal (if a proof is in +progress). + + +See also: Section :ref:`TODO-8.7-performing-computations`. + + +.. cmd:: Compute @term. + +This command performs a call-by-value evaluation of term by using the +bytecode-based virtual machine. It is a shortcut for ``Eval vm_compute in`` +:n:`@term`. + + +See also: Section :ref:`TODO-8.7-performing-computations`. + + +.. cmd::Extraction @term. + +This command displays the extracted term from :n:`@term`. The extraction is +processed according to the distinction between ``Set`` and ``Prop``; that is +to say, between logical and computational content (see Section +:ref:`TODO-4.1.1-sorts`). The extracted term is displayed in OCaml +syntax, +where global identifiers are still displayed as in |Coq| terms. + + +Variants: + + +.. cmdv:: Recursive Extraction {+ @qualid }. + +Recursively extracts all +the material needed for the extraction of the qualified identifiers. + + +See also: Chapter ref:`TODO-23-chapter-extraction`. + + +.. cmd:: Print Assumptions @qualid. + +This commands display all the assumptions (axioms, parameters and +variables) a theorem or definition depends on. Especially, it informs +on the assumptions with respect to which the validity of a theorem +relies. + + +Variants: + + +.. cmdv:: Print Opaque Dependencies @qualid. + +Displays the set of opaque constants :n:`@qualid` relies on in addition to +the assumptions. + +.. cmdv:: Print Transparent Dependencies @qualid. + +Displays the set of +transparent constants :n:`@qualid` relies on in addition to the assumptions. + +.. cmdv:: Print All Dependencies @qualid. + +Displays all assumptions and constants :n:`@qualid` relies on. + + + +.. cmd:: Search @qualid. + +This command displays the name and type of all objects (hypothesis of +the current goal, theorems, axioms, etc) of the current context whose +statement contains :n:`@qualid`. This command is useful to remind the user +of the name of library lemmas. + + +Error messages: + + +.. exn:: The reference @qualid was not found in the current environment + +There is no constant in the environment named qualid. + +Variants: + +.. cmdv:: Search @string. + +If :n:`@string` is a valid identifier, this command +displays the name and type of all objects (theorems, axioms, etc) of +the current context whose name contains string. If string is a +notation’s string denoting some reference :n:`@qualid` (referred to by its +main symbol as in `"+"` or by its notation’s string as in `"_ + _"` or +`"_ 'U' _"`, see Section :ref:`TODO-12.1-notations`), the command works like ``Search`` :n:`@qualid`. + +.. cmdv:: Search @string%@key. + +The string string must be a notation or the main +symbol of a notation which is then interpreted in the scope bound to +the delimiting key :n:`@key` (see Section :ref:`TODO-12.2.2-local-interpretation-rules-for-notations`). + +.. cmdv:: Search @term_pattern. + +This searches for all statements or types of +definition that contains a subterm that matches the pattern +`term_pattern` (holes of the pattern are either denoted by `_` or by +`?ident` when non linear patterns are expected). + +.. cmdv:: Search { + [-]@term_pattern_string }. + +where +:n:`@term_pattern_string` is a term_pattern, a string, or a string followed +by a scope delimiting key `%key`. This generalization of ``Search`` searches +for all objects whose statement or type contains a subterm matching +:n:`@term_pattern` (or :n:`@qualid` if :n:`@string` is the notation for a reference +qualid) and whose name contains all string of the request that +correspond to valid identifiers. If a term_pattern or a string is +prefixed by `-`, the search excludes the objects that mention that +term_pattern or that string. + +.. cmdv:: Search @term_pattern_string … @term_pattern_string inside {+ @qualid } . + +This restricts the search to constructions defined in the modules named by the given :n:`qualid` sequence. + +.. cmdv:: Search @term_pattern_string … @term_pattern_string outside {+ @qualid }. + +This restricts the search to constructions not defined in the modules named by the given :n:`qualid` sequence. + +.. cmdv:: @selector: Search [-]@term_pattern_string … [-]@term_pattern_string. + +This specifies the goal on which to search hypothesis (see +Section :ref:`TODO-8.1-invocation-of-tactics`). +By default the 1st goal is searched. This variant can +be combined with other variants presented here. + + +.. coqtop:: in + + Require Import ZArith. + +.. coqtop:: all + + Search Z.mul Z.add "distr". + + Search "+"%Z "*"%Z "distr" -positive -Prop. + + Search (?x * _ + ?x * _)%Z outside OmegaLemmas. + +.. note:: Up to |Coq| version 8.4, ``Search`` had the behavior of current +``SearchHead`` and the behavior of current Search was obtained with +command ``SearchAbout``. For compatibility, the deprecated name +SearchAbout can still be used as a synonym of Search. For +compatibility, the list of objects to search when using ``SearchAbout`` +may also be enclosed by optional[ ] delimiters. + + +.. cmd:: SearchHead @term. + +This command displays the name and type of all hypothesis of the +current goal (if any) and theorems of the current context whose +statement’s conclusion has the form `(term t1 .. tn)`. This command is +useful to remind the user of the name of library lemmas. + + + +.. coqtop:: reset all + + SearchHead le. + + SearchHead (@eq bool). + + +Variants: + +.. cmdv:: SearchHead @term inside {+ @qualid }. + +This restricts the search to constructions defined in the modules named by the given :n:`qualid` sequence. + +.. cmdv:: SearchHead term outside {+ @qualid }. + +This restricts the search to constructions not defined in the modules named by the given :n:`qualid` sequence. + +Error messages: + +.. exn:: Module/section @qualid not found + +No module :n:`@qualid` has been required +(see Section :ref:`TODO-6.5.1-require`). + +.. cmdv:: @selector: SearchHead @term. + +This specifies the goal on which to +search hypothesis (see Section :ref:`TODO-8.1-invocation-of-tactics`). +By default the 1st goal is +searched. This variant can be combined with other variants presented +here. + +.. note:: Up to |Coq| version 8.4, ``SearchHead`` was named ``Search``. + + +.. cmd:: SearchPattern @term. + +This command displays the name and type of all hypothesis of the +current goal (if any) and theorems of the current context whose +statement’s conclusion or last hypothesis and conclusion matches the +expressionterm where holes in the latter are denoted by `_`. +It is a +variant of Search @term_pattern that does not look for subterms but +searches for statements whose conclusion has exactly the expected +form, or whose statement finishes by the given series of +hypothesis/conclusion. + +.. coqtop:: in + + Require Import Arith. + +.. coqtop:: all + + SearchPattern (_ + _ = _ + _). + + SearchPattern (nat -> bool). + + SearchPattern (forall l : list _, _ l l). + +Patterns need not be linear: you can express that the same expression +must occur in two places by using pattern variables `?ident`. + + +.. coqtop:: all + + SearchPattern (?X1 + _ = _ + ?X1). + +Variants: + + +.. cmdv:: SearchPattern @term inside {+ @qualid } . + +This restricts the search to constructions defined in the modules named by the given :n:`qualid` sequence. + +.. cmdv:: SearchPattern @term outside {+ @qualid }. + +This restricts the search to constructions not defined in the modules named by the given :n:`qualid` sequence. + +.. cmdv:: @selector: SearchPattern @term. + +This specifies the goal on which to +search hypothesis (see Section :ref:`TODO-8.1-invocation-of-tactics`). By default the 1st goal is +searched. This variant can be combined with other variants presented +here. + + + +.. cmdv:: SearchRewrite @term. + +This command displays the name and type of all hypothesis of the +current goal (if any) and theorems of the current context whose +statement’s conclusion is an equality of which one side matches the +expression term. Holes in term are denoted by “_”. + +.. coqtop:: in + + Require Import Arith. + +.. coqtop:: all + + SearchRewrite (_ + _ + _). + +Variants: + + +.. cmdv:: SearchRewrite term inside {+ @qualid }. + +This restricts the search to constructions defined in the modules named by the given :n:`qualid` sequence. + +.. cmdv:: SearchRewrite @term outside {+ @qualid }. + +This restricts the search to constructions not defined in the modules named by the given :n:`qualid` sequence. + +.. cmdv:: @selector: SearchRewrite @term. + +This specifies the goal on which to +search hypothesis (see Section :ref:`TODO-8.1-invocation-of-tactics`). By default the 1st goal is +searched. This variant can be combined with other variants presented +here. + +.. note:: + + For the ``Search``, ``SearchHead``, ``SearchPattern`` and ``SearchRewrite`` + queries, it + is possible to globally filter the search results via the command + ``Add Search Blacklist`` :n:`@substring`. A lemma whose fully-qualified name + contains any of the declared substrings will be removed from the + search results. The default blacklisted substrings are ``_subproof`` + ``Private_``. The command ``Remove Search Blacklist ...`` allows expunging + this blacklist. + + +.. cmd:: Locate @qualid. + +This command displays the full name of objects whose name is a prefix +of the qualified identifier :n:`@qualid`, and consequently the |Coq| module in +which they are defined. It searches for objects from the different +qualified name spaces of |Coq|: terms, modules, Ltac, etc. + +.. coqtop:: none + + Set Printing Depth 50. + +.. coqtop:: all + + Locate nat. + + Locate Datatypes.O. + + Locate Init.Datatypes.O. + + Locate Coq.Init.Datatypes.O. + + Locate I.Dont.Exist. + +Variants: + + +.. cmdv:: Locate Term @qualid. + +As Locate but restricted to terms. + +.. cmdv:: Locate Module @qualid. + +As Locate but restricted to modules. + +.. cmdv:: Locate Ltac @qualid. + +As Locate but restricted to tactics. + + +See also: Section :ref:`TODO-12.1.10-LocateSymbol` + + +.. _loading-files: + +Loading files +----------------- + +|Coq| offers the possibility of loading different parts of a whole +development stored in separate files. Their contents will be loaded as +if they were entered from the keyboard. This means that the loaded +files are ASCII files containing sequences of commands for |Coq|’s +toplevel. This kind of file is called a *script* for |Coq|. The standard +(and default) extension of |Coq|’s script files is .v. + + +.. cmd:: Load @ident. + +This command loads the file named :n:`ident`.v, searching successively in +each of the directories specified in the *loadpath*. (see Section +:ref:`TODO-2.6.3-libraries-and-filesystem`) + +Files loaded this way cannot leave proofs open, and the ``Load`` +command cannot be used inside a proof either. + +Variants: + + +.. cmdv:: Load @string. + +Loads the file denoted by the string :n:`@string`, where +string is any complete filename. Then the `~` and .. abbreviations are +allowed as well as shell variables. If no extension is specified, |Coq| +will use the default extension ``.v``. + +.. cmdv:: Load Verbose @ident. + +.. cmdv:: Load Verbose @string. + +Display, while loading, +the answers of |Coq| to each command (including tactics) contained in +the loaded file See also: Section :ref:`TODO-6.9.1-silent`. + +Error messages: + +.. exn:: Can’t find file @ident on loadpath + +.. exn:: Load is not supported inside proofs + +.. exn:: Files processed by Load cannot leave open proofs + +.. _compiled-files: + +Compiled files +------------------ + +This section describes the commands used to load compiled files (see +Chapter :ref:`TODO-14-coq-commands` for documentation on how to compile a file). A compiled +file is a particular case of module called *library file*. + + +.. cmd:: Require @qualid. + +This command looks in the loadpath for a file containing module :n:`@qualid` +and adds the corresponding module to the environment of |Coq|. As +library files have dependencies in other library files, the command +``Require`` :n:`@qualid` recursively requires all library files the module +qualid depends on and adds the corresponding modules to the +environment of |Coq| too. |Coq| assumes that the compiled files have been +produced by a valid |Coq| compiler and their contents are then not +replayed nor rechecked. + +To locate the file in the file system, :n:`@qualid` is decomposed under the +form `dirpath.ident` and the file `ident.vo` is searched in the physical +directory of the file system that is mapped in |Coq| loadpath to the +logical path dirpath (see Section :ref:`TODO-2.6.3-libraries-and-filesystem`). The mapping between +physical directories and logical names at the time of requiring the +file must be consistent with the mapping used to compile the file. If +several files match, one of them is picked in an unspecified fashion. + + +Variants: + +.. cmdv:: Require Import @qualid. + +This loads and declares the module :n:`@qualid` +and its dependencies then imports the contents of :n:`@qualid` as described +in Section :ref:`TODO-2.5.8-import`.It does not import the modules on which +qualid depends unless these modules were themselves required in module +:n:`@qualid` +using ``Require Export``, as described below, or recursively required +through a sequence of ``Require Export``. If the module required has +already been loaded, ``Require Import`` :n:`@qualid` simply imports it, as ``Import`` +:n:`@qualid` would. + +.. cmdv:: Require Export @qualid. + +This command acts as ``Require Import`` :n:`@qualid`, +but if a further module, say `A`, contains a command ``Require Export`` `B`, +then the command ``Require Import`` `A` also imports the module `B.` + +.. cmdv:: Require [Import | Export] {+ @qualid }. + +This loads the +modules named by the :n:`qualid` sequence and their recursive +dependencies. If +``Import`` or ``Export`` is given, it also imports these modules and +all the recursive dependencies that were marked or transitively marked +as ``Export``. + +.. cmdv:: From @dirpath Require @qualid. + +This command acts as ``Require``, but picks +any library whose absolute name is of the form dirpath.dirpath’.qualid +for some `dirpath’`. This is useful to ensure that the :n:`@qualid` library +comes from a given package by making explicit its absolute root. + + + +Error messages: + +.. exn:: Cannot load qualid: no physical path bound to dirpath + +.. exn:: Cannot find library foo in loadpath + +The command did not find the +file foo.vo. Either foo.v exists but is not compiled or foo.vo is in a +directory which is not in your LoadPath (see Section :ref:`TODO-2.6.3-libraries-and-filesystem`). + +.. exn:: Compiled library ident.vo makes inconsistent assumptions over library qualid + +The command tried to load library file `ident.vo` that +depends on some specific version of library :n:`@qualid` which is not the +one already loaded in the current |Coq| session. Probably `ident.v` was +not properly recompiled with the last version of the file containing +module :n:`@qualid`. + +.. exn:: Bad magic number + +The file `ident.vo` was found but either it is not a +|Coq| compiled module, or it was compiled with an incompatible +version of |Coq|. + +.. exn:: The file `ident.vo` contains library dirpath and not library dirpath’ + +The library file `dirpath’` is indirectly required by the +``Require`` command but it is bound in the current loadpath to the +file `ident.vo` which was bound to a different library name `dirpath` at +the time it was compiled. + + +.. exn:: Require is not allowed inside a module or a module type + +This command +is not allowed inside a module or a module type being defined. It is +meant to describe a dependency between compilation units. Note however +that the commands Import and Export alone can be used inside modules +(see Section :ref:`TODO-2.5.8-import`). + + + +See also: Chapter :ref:`TODO-14-coq-commands` + + +.. cmd:: Print Libraries. + +This command displays the list of library files loaded in the +current |Coq| session. For each of these libraries, it also tells if it +is imported. + + +.. cmd:: Declare ML Module {+ @string } . + +This commands loads the OCaml compiled files +with names given by the :n:`@string` sequence +(dynamic link). It is mainly used to load tactics dynamically. The +files are searched into the current OCaml loadpath (see the +command ``Add ML Path`` in Section :ref:`TODO-2.6.3-libraries-and-filesystem`). Loading of OCaml files is only possible under the bytecode version of ``coqtop`` (i.e. +``coqtop`` called with option ``-byte``, see chapter :ref:`TODO-14-coq-commands`), or when |Coq| has been compiled with a +version of OCaml that supports native Dynlink (≥ 3.11). + + +Variants: + + +.. cmdv:: Local Declare ML Module {+ @string }. + +This variant is not +exported to the modules that import the module where they occur, even +if outside a section. + + + +Error messages: + +.. exn:: File not found on loadpath : @string + +.. exn:: Loading of ML object file forbidden in a native |Coq| + + + +.. cmd:: Print ML Modules. + +This prints the name of all OCaml modules loaded with ``Declare +ML Module``. To know from where these module were loaded, the user +should use the command Locate File (see Section :ref:`TODO-6.6.10-locate-file`) + + +.. _loadpath: + +Loadpath +------------ + +Loadpaths are preferably managed using |Coq| command line options (see +Section `2.6.3-libraries-and-filesystem`) but there remain vernacular commands to manage them +for practical purposes. Such commands are only meant to be issued in +the toplevel, and using them in source files is discouraged. + + +.. cmd:: Pwd. + +This command displays the current working directory. + + +.. cmd:: Cd @string. + +This command changes the current directory according to :n:`@string` which +can be any valid path. + + +Variants: + + +.. cmdv:: Cd. + +Is equivalent to Pwd. + + + +.. cmd:: Add LoadPath @string as @dirpath. + +This command is equivalent to the command line option +``-Q`` :n:`@string` :n:`@dirpath`. It adds the physical directory string to the current +|Coq| loadpath and maps it to the logical directory dirpath. + +Variants: + + +.. cmdv:: Add LoadPath @string. + +Performs as Add LoadPath :n:`@string` as :n:`@dirpath` but +for the empty directory path. + + + +.. cmd:: Add Rec LoadPath @string as @dirpath. + +This command is equivalent to the command line option +``-R`` :n:`@string` :n:`@dirpath`. It adds the physical directory string and all its +subdirectories to the current |Coq| loadpath. + +Variants: + + +.. cmdv:: Add Rec LoadPath @string. + +Works as ``Add Rec LoadPath`` :n:`@string` as :n:`@dirpath` but for the empty +logical directory path. + + + +.. cmd:: Remove LoadPath @string. + +This command removes the path :n:`@string` from the current |Coq| loadpath. + + +.. cmd:: Print LoadPath. + +This command displays the current |Coq| loadpath. + + +Variants: + + +.. cmdv:: Print LoadPath @dirpath. + +Works as ``Print LoadPath`` but displays only +the paths that extend the :n:`@dirpath` prefix. + + +.. cmd:: Add ML Path @string. + +This command adds the path :n:`@string` to the current OCaml +loadpath (see the command `Declare ML Module`` in Section :ref:`TODO-6.5-compiled-files`). + + +.. cmd:: Add Rec ML Path @string. + +This command adds the directory :n:`@string` and all its subdirectories to +the current OCaml loadpath (see the command ``Declare ML Module`` +in Section :ref:`TODO-6.5-compiled-files`). + + +.. cmd:: Print ML Path @string. + +This command displays the current OCaml loadpath. This +command makes sense only under the bytecode version of ``coqtop``, i.e. +using option ``-byte`` +(see the command Declare ML Module in Section :ref:`TODO-6.5-compiled-files`). + + +.. cmd:: Locate File @string. + +This command displays the location of file string in the current +loadpath. Typically, string is a .cmo or .vo or .v file. + + +.. cmd:: Locate Library @dirpath. + +This command gives the status of the |Coq| module dirpath. It tells if +the module is loaded and if not searches in the load path for a module +of logical name :n:`@dirpath`. + + +.. _backtracking: + +Backtracking +---------------- + +The backtracking commands described in this section can only be used +interactively, they cannot be part of a vernacular file loaded via +``Load`` or compiled by ``coqc``. + + +.. cmd:: Reset @ident. + +This command removes all the objects in the environment since :n:`@ident` +was introduced, including :n:`@ident`. :n:`@ident` may be the name of a defined or +declared object as well as the name of a section. One cannot reset +over the name of a module or of an object inside a module. + + +Error messages: + +.. exn:: @ident: no such entry + +Variants: + +.. cmd:: Reset Initial. + +Goes back to the initial state, just after the start +of the interactive session. + + + +.. cmd:: Back. + +This commands undoes all the effects of the last vernacular command. +Commands read from a vernacular file via a ``Load`` are considered as a +single command. Proof management commands are also handled by this +command (see Chapter :ref:`TODO-7-proof-handling`). For that, Back may have to undo more than +one command in order to reach a state where the proof management +information is available. For instance, when the last command is a +``Qed``, the management information about the closed proof has been +discarded. In this case, ``Back`` will then undo all the proof steps up to +the statement of this proof. + + +Variants: + + +.. cmdv:: Back @num. + +Undoes :n:`@num` vernacular commands. As for Back, some extra +commands may be undone in order to reach an adequate state. For +instance Back :n:`@num` will not re-enter a closed proof, but rather go just +before that proof. + + + +Error messages: + + +.. exn:: Invalid backtrack + +The user wants to undo more commands than available in the history. + +.. cmd:: BackTo @num. + +This command brings back the system to the state labeled :n:`@num`, +forgetting the effect of all commands executed after this state. The +state label is an integer which grows after each successful command. +It is displayed in the prompt when in -emacs mode. Just as ``Back`` (see +above), the ``BackTo`` command now handles proof states. For that, it may +have to undo some extra commands and end on a state `num′ ≤ num` if +necessary. + + +Variants: + + +.. cmdv:: Backtrack @num @num @num. + +`Backtrack` is a *deprecated* form of +`BackTo` which allows explicitly manipulating the proof environment. The +three numbers represent the following: + + + *first number* : State label to reach, as for BackTo. + + *second number* : *Proof state number* to unbury once aborts have been done. + |Coq| will compute the number of Undo to perform (see Chapter :ref:`TODO-7-proof-handling`). + + *third number* : Number of Abort to perform, i.e. the number of currently + opened nested proofs that must be canceled (see Chapter :ref:`TODO-7-proof-handling`). + + + + +Error messages: + + +.. exn:: Invalid backtrack + + +The destination state label is unknown. + + +.. _quitting-and-debugging: + +Quitting and debugging +-------------------------- + + +.. cmd:: Quit. + +This command permits to quit |Coq|. + + +.. cmd:: Drop. + +This is used mostly as a debug facility by |Coq|’s implementors and does +not concern the casual user. This command permits to leave |Coq| +temporarily and enter the OCaml toplevel. The OCaml +command: + + +:: + + #use "include";; + + +adds the right loadpaths and loads some toplevel printers for all +abstract types of |Coq|- section_path, identifiers, terms, judgments, …. +You can also use the file base_include instead, that loads only the +pretty-printers for section_paths and identifiers. You can return back +to |Coq| with the command: + + +:: + + go();; + + + +Warnings: + + +#. It only works with the bytecode version of |Coq| (i.e. `coqtop.byte`, + see Section `TODO-14.1-interactive-use`). +#. You must have compiled |Coq| from the source package and set the + environment variable COQTOP to the root of your copy of the sources + (see Section `14.3.2-customization-by-envionment-variables`). + + + +.. TODO : command is not a syntax entry + +.. cmd:: Time @command. + +This command executes the vernacular command :n:`@command` and displays the +time needed to execute it. + + +.. cmd:: Redirect @string @command. + +This command executes the vernacular command :n:`@command`, redirecting its +output to ":n:`@string`.out". + + +.. cmd:: Timeout @num @command. + +This command executes the vernacular command :n:`@command`. If the command +has not terminated after the time specified by the :n:`@num` (time +expressed in seconds), then it is interrupted and an error message is +displayed. + + +.. cmd:: Set Default Timeout @num. + +After using this command, all subsequent commands behave as if they +were passed to a Timeout command. Commands already starting by a +`Timeout` are unaffected. + + +.. cmd:: Unset Default Timeout. + +This command turns off the use of a default timeout. + +.. cmd:: Test Default Timeout. + +This command displays whether some default timeout has been set or not. + +.. cmd:: Fail @command. + +For debugging scripts, sometimes it is desirable to know +whether a command or a tactic fails. If the given :n:`@command` +fails, the ``Fail`` statement succeeds, without changing the proof +state, and in interactive mode, the system +prints a message confirming the failure. +If the given :n:`@command` succeeds, the statement is an error, and +it prints a message indicating that the failure did not occur. + +Error messages: + +.. exn:: The command has not failed! + +.. _controlling-display: + +Controlling display +----------------------- + + +.. cmd:: Set Silent. + +This command turns off the normal displaying. + + +.. cmd:: Unset Silent. + +This command turns the normal display on. + +TODO : check that spaces are handled well + +.. cmd:: Set Warnings ‘‘(@ident {* , @ident } )’’. + +This command configures the display of warnings. It is experimental, +and expects, between quotes, a comma-separated list of warning names +or categories. Adding - in front of a warning or category disables it, +adding + makes it an error. It is possible to use the special +categories all and default, the latter containing the warnings enabled +by default. The flags are interpreted from left to right, so in case +of an overlap, the flags on the right have higher priority, meaning +that `A,-A` is equivalent to `-A`. + + +.. cmd:: Set Search Output Name Only. + +This command restricts the output of search commands to identifier +names; turning it on causes invocations of ``Search``, ``SearchHead``, +``SearchPattern``, ``SearchRewrite`` etc. to omit types from their output, +printing only identifiers. + + +.. cmd:: Unset Search Output Name Only. + +This command turns type display in search results back on. + + +.. cmd:: Set Printing Width @integer. + +This command sets which left-aligned part of the width of the screen +is used for display. + + +.. cmd:: Unset Printing Width. + +This command resets the width of the screen used for display to its +default value (which is 78 at the time of writing this documentation). + + +.. cmd:: Test Printing Width. + +This command displays the current screen width used for display. + + +.. cmd:: Set Printing Depth @integer. + +This command sets the nesting depth of the formatter used for pretty- +printing. Beyond this depth, display of subterms is replaced by dots. + + +.. cmd:: Unset Printing Depth. + +This command resets the nesting depth of the formatter used for +pretty-printing to its default value (at the time of writing this +documentation, the default value is 50). + + +.. cmd:: Test Printing Depth. + +This command displays the current nesting depth used for display. + + +.. cmd:: Unset Printing Compact Contexts. + +This command resets the displaying of goals contexts to non compact +mode (default at the time of writing this documentation). Non compact +means that consecutive variables of different types are printed on +different lines. + + +.. cmd:: Set Printing Compact Contexts. + +This command sets the displaying of goals contexts to compact mode. +The printer tries to reduce the vertical size of goals contexts by +putting several variables (even if of different types) on the same +line provided it does not exceed the printing width (See Set Printing +Width above). + + +.. cmd:: Test Printing Compact Contexts. + +This command displays the current state of compaction of goal. + + +.. cmd:: Unset Printing Unfocused. + +This command resets the displaying of goals to focused goals only +(default). Unfocused goals are created by focusing other goals with +bullets (see :ref:`TODO-7.2.7-bullets`) or curly braces (see `7.2.6-curly-braces`). + + +.. cmd:: Set Printing Unfocused. + +This command enables the displaying of unfocused goals. The goals are +displayed after the focused ones and are distinguished by a separator. + + +.. cmd:: Test Printing Unfocused. + +This command displays the current state of unfocused goals display. + + +.. cmd:: Set Printing Dependent Evars Line. + +This command enables the printing of the “(dependent evars: …)” line +when -emacs is passed. + + +.. cmd:: Unset Printing Dependent Evars Line. + +This command disables the printing of the “(dependent evars: …)” line +when -emacs is passed. + + +Controlling the reduction strategies and the conversion algorithm +---------------------------------------------------------------------- + + +|Coq| provides reduction strategies that the tactics can invoke and two +different algorithms to check the convertibility of types. The first +conversion algorithm lazily compares applicative terms while the other +is a brute-force but efficient algorithm that first normalizes the +terms before comparing them. The second algorithm is based on a +bytecode representation of terms similar to the bytecode +representation used in the ZINC virtual machine [`98`]. It is +especially useful for intensive computation of algebraic values, such +as numbers, and for reflection-based tactics. The commands to fine- +tune the reduction strategies and the lazy conversion algorithm are +described first. + +.. cmd:: Opaque {+ @qualid }. + +This command has an effect on unfoldable constants, i.e. on constants +defined by ``Definition`` or ``Let`` (with an explicit body), or by a command +assimilated to a definition such as ``Fixpoint``, ``Program Definition``, etc, +or by a proof ended by ``Defined``. The command tells not to unfold the +constants in the :n:`@qualid` sequence in tactics using δ-conversion (unfolding +a constant is replacing it by its definition). + +``Opaque`` has also an effect on the conversion algorithm of |Coq|, telling +it to delay the unfolding of a constant as much as possible when |Coq| +has to check the conversion (see Section :ref:`TODO-4.3-conversion-rules`) of two distinct +applied constants. + +The scope of ``Opaque`` is limited to the current section, or current +file, unless the variant ``Global Opaque`` is used. + + +See also: sections :ref:`TODO-8.7-performing-computations`, :ref:`TODO-8.16-automatizing`, :ref:`TODO-7.1-switching-on-off-proof-editing-mode` + + +Error messages: + + +.. exn:: The reference @qualid was not found in the current environment + +There is no constant referred by :n:`@qualid` in the environment. +Nevertheless, if you asked ``Opaque`` `foo` `bar` and if `bar` does not exist, `foo` is set opaque. + +.. cmd:: Transparent {+ @qualid }. + +This command is the converse of `Opaque`` and it applies on unfoldable +constants to restore their unfoldability after an Opaque command. + +Note in particular that constants defined by a proof ended by Qed are +not unfoldable and Transparent has no effect on them. This is to keep +with the usual mathematical practice of *proof irrelevance*: what +matters in a mathematical development is the sequence of lemma +statements, not their actual proofs. This distinguishes lemmas from +the usual defined constants, whose actual values are of course +relevant in general. + +The scope of Transparent is limited to the current section, or current +file, unless the variant ``Global Transparent`` is +used. + + +Error messages: + + +.. exn:: The reference @qualid was not found in the current environment + +There is no constant referred by :n:`@qualid` in the environment. + + + +See also: sections :ref:`TODO-8.7-performing-computations`, :ref:`TODO-8.16-automatizing`, :ref:`TODO-7.1-switching-on-off-proof-editing-mode` + + +.. cmd:: Strategy @level [ {+ @qualid } ]. + +This command generalizes the behavior of Opaque and Transparent +commands. It is used to fine-tune the strategy for unfolding +constants, both at the tactic level and at the kernel level. This +command associates a level to the qualified names in the :n:`@qualid` +sequence. Whenever two +expressions with two distinct head constants are compared (for +instance, this comparison can be triggered by a type cast), the one +with lower level is expanded first. In case of a tie, the second one +(appearing in the cast type) is expanded. + +Levels can be one of the following (higher to lower): + + + ``opaque`` : level of opaque constants. They cannot be expanded by + tactics (behaves like +∞, see next item). + + :n:`@num` : levels indexed by an integer. Level 0 corresponds to the + default behavior, which corresponds to transparent constants. This + level can also be referred to as transparent. Negative levels + correspond to constants to be expanded before normal transparent + constants, while positive levels correspond to constants to be + expanded after normal transparent constants. + + ``expand`` : level of constants that should be expanded first (behaves + like −∞) + + +These directives survive section and module closure, unless the +command is prefixed by Local. In the latter case, the behavior +regarding sections and modules is the same as for the ``Transparent`` and +``Opaque`` commands. + + +.. cmd:: Print Strategy @qualid. + +This command prints the strategy currently associated to :n:`@qualid`. It +fails if :n:`@qualid` is not an unfoldable reference, that is, neither a +variable nor a constant. + + +Error messages: + + +.. exn:: The reference is not unfoldable. + + + +Variants: + + +.. cmdv:: Print Strategies. + +Print all the currently non-transparent strategies. + + + +.. cmd:: Declare Reduction @ident := @convtactic. + +This command allows giving a short name to a reduction expression, for +instance lazy beta delta [foo bar]. This short name can then be used +in ``Eval`` :n:`@ident` ``in`` ... or ``eval`` directives. This command +accepts the +Local modifier, for discarding this reduction name at the end of the +file or module. For the moment the name cannot be qualified. In +particular declaring the same name in several modules or in several +functor applications will be refused if these declarations are not +local. The name :n:`@ident` cannot be used directly as an Ltac tactic, but +nothing prevents the user to also perform a +``Ltac`` `ident` ``:=`` `convtactic`. + + +See also: sections :ref:`TODO-8.7-performing-computations` + + +.. _controlling-locality-of-commands: + +Controlling the locality of commands +----------------------------------------- + + +.. cmd:: Local @command. +.. cmd:: Global @command. + +Some commands support a Local or Global prefix modifier to control the +scope of their effect. There are four kinds of commands: + + ++ Commands whose default is to extend their effect both outside the + section and the module or library file they occur in. For these + commands, the Local modifier limits the effect of the command to the + current section or module it occurs in. As an example, the ``Coercion`` + (see Section :ref:`TODO-2.8-coercions`) and ``Strategy`` (see Section :ref:`TODO-6.10.3-strategy`) commands belong + to this category. ++ Commands whose default behavior is to stop their effect at the end + of the section they occur in but to extent their effect outside the + module or library file they occur in. For these commands, the Local + modifier limits the effect of the command to the current module if the + command does not occur in a section and the Global modifier extends + the effect outside the current sections and current module if the + command occurs in a section. As an example, the ``Implicit Arguments`` (see + Section :ref:`TODO-2.7-implicit-arguments`), Ltac (see Chapter :ref:`TODO-9-tactic-language`) or ``Notation`` (see Section + :ref:`TODO-12.1-notations`) commands belong to this category. Notice that a subclass of + these commands do not support extension of their scope outside + sections at all and the Global is not applicable to them. ++ Commands whose default behavior is to stop their effect at the end + of the section or module they occur in. For these commands, the Global + modifier extends their effect outside the sections and modules they + occurs in. The ``Transparent`` and ``Opaque`` (see Section :ref:`TODO-6.10-opaque`) commands belong to this category. ++ Commands whose default behavior is to extend their effect outside + sections but not outside modules when they occur in a section and to + extend their effect outside the module or library file they occur in + when no section contains them.For these commands, the Local modifier + limits the effect to the current section or module while the Global + modifier extends the effect outside the module even when the command + occurs in a section. The ``Set`` and ``Unset`` commands belong to this + category. |