diff options
Diffstat (limited to 'doc')
34 files changed, 617 insertions, 182 deletions
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index 4ad952bdfb..01240a062c 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -219,6 +219,9 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo Print nat. Definition a := 1. + The blank line after the directive is required. If you begin a proof, + include an ``Abort`` afterwards to reset coqtop for the next example. + Here is a list of permissible options: - Display options diff --git a/doc/sphinx/_static/diffs-coqide-compacted.png b/doc/sphinx/_static/diffs-coqide-compacted.png Binary files differnew file mode 100644 index 0000000000..b64ffeb269 --- /dev/null +++ b/doc/sphinx/_static/diffs-coqide-compacted.png diff --git a/doc/sphinx/_static/diffs-coqide-multigoal.png b/doc/sphinx/_static/diffs-coqide-multigoal.png Binary files differnew file mode 100644 index 0000000000..4020279267 --- /dev/null +++ b/doc/sphinx/_static/diffs-coqide-multigoal.png diff --git a/doc/sphinx/_static/diffs-coqide-on.png b/doc/sphinx/_static/diffs-coqide-on.png Binary files differnew file mode 100644 index 0000000000..f270397ea3 --- /dev/null +++ b/doc/sphinx/_static/diffs-coqide-on.png diff --git a/doc/sphinx/_static/diffs-coqide-removed.png b/doc/sphinx/_static/diffs-coqide-removed.png Binary files differnew file mode 100644 index 0000000000..8f2e71fdc8 --- /dev/null +++ b/doc/sphinx/_static/diffs-coqide-removed.png diff --git a/doc/sphinx/_static/diffs-coqtop-compacted.png b/doc/sphinx/_static/diffs-coqtop-compacted.png Binary files differnew file mode 100644 index 0000000000..b37f0a6771 --- /dev/null +++ b/doc/sphinx/_static/diffs-coqtop-compacted.png diff --git a/doc/sphinx/_static/diffs-coqtop-multigoal.png b/doc/sphinx/_static/diffs-coqtop-multigoal.png Binary files differnew file mode 100644 index 0000000000..cfedde02ac --- /dev/null +++ b/doc/sphinx/_static/diffs-coqtop-multigoal.png diff --git a/doc/sphinx/_static/diffs-coqtop-on.png b/doc/sphinx/_static/diffs-coqtop-on.png Binary files differnew file mode 100644 index 0000000000..bdfcf0af1a --- /dev/null +++ b/doc/sphinx/_static/diffs-coqtop-on.png diff --git a/doc/sphinx/_static/diffs-coqtop-on3.png b/doc/sphinx/_static/diffs-coqtop-on3.png Binary files differnew file mode 100644 index 0000000000..63ff869432 --- /dev/null +++ b/doc/sphinx/_static/diffs-coqtop-on3.png diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index d03a31c044..c0a57763b9 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -27,6 +27,13 @@ rationals ``Require Import Lqa`` and reals ``Require Import Lra``. generating a *proof cache* which makes it possible to rerun scripts even without `csdp`. +.. flag:: Simplex + + This option (set by default) instructs the decision procedures to + use the Simplex method for solving linear goals. If it is not set, + the decision procedures are using Fourier elimination. + + The tactics solve propositional formulas parameterized by atomic arithmetic expressions interpreted over a domain :math:`D` ∈ {ℤ, ℚ, ℝ}. The syntax of the formulas is the following: @@ -96,8 +103,7 @@ and checked to be :math:`-1`. .. tacn:: lra :name: lra - This tactic is searching for *linear* refutations using Fourier - elimination [#]_. As a result, this tactic explores a subset of the *Cone* + This tactic is searching for *linear* refutations. As a result, this tactic explores a subset of the *Cone* defined as :math:`\mathit{LinCone}(S) =\left\{ \left. \sum_{p \in S} \alpha_p \times p~\right|~\alpha_p \mbox{ are positive constants} \right\}` @@ -112,11 +118,11 @@ and checked to be :math:`-1`. .. tacn:: lia :name: lia -This tactic offers an alternative to the :tacn:`omega` and :tacn:`romega` -tactics. Roughly speaking, the deductive power of lia is the combined deductive -power of :tacn:`ring_simplify` and :tacn:`omega`. However, it solves linear -goals that :tacn:`omega` and :tacn:`romega` do not solve, such as the following -so-called *omega nightmare* :cite:`TheOmegaPaper`. + This tactic offers an alternative to the :tacn:`omega` tactic. Roughly + speaking, the deductive power of lia is the combined deductive power of + :tacn:`ring_simplify` and :tacn:`omega`. However, it solves linear goals + that :tacn:`omega` does not solve, such as the following so-called *omega + nightmare* :cite:`TheOmegaPaper`. .. coqtop:: in @@ -124,8 +130,7 @@ so-called *omega nightmare* :cite:`TheOmegaPaper`. 27 <= 11 * x + 13 * y <= 45 -> -10 <= 7 * x - 9 * y <= 4 -> False. -The estimation of the relative efficiency of :tacn:`lia` *vs* :tacn:`omega` and -:tacn:`romega` is under evaluation. +The estimation of the relative efficiency of :tacn:`lia` *vs* :tacn:`omega` is under evaluation. High level view of `lia` ~~~~~~~~~~~~~~~~~~~~~~~~ @@ -135,7 +140,7 @@ principle [#]_. However, this is not the case over :math:`\mathbb{Z}`. Actually, *positivstellensatz* refutations are not even sufficient to decide linear *integer* arithmetic. The canonical example is :math:`2 * x = 1 -> \mathtt{False}` which is a theorem of :math:`\mathbb{Z}` but not a theorem of :math:`{\mathbb{R}}`. To remedy this -weakness, the `lia` tactic is using recursively a combination of: +weakness, the :tacn:`lia` tactic is using recursively a combination of: + linear *positivstellensatz* refutations; + cutting plane proofs; @@ -189,10 +194,10 @@ a proof. .. tacn:: nra :name: nra -This tactic is an *experimental* proof procedure for non-linear -arithmetic. The tactic performs a limited amount of non-linear -reasoning before running the linear prover of `lra`. This pre-processing -does the following: + This tactic is an *experimental* proof procedure for non-linear + arithmetic. The tactic performs a limited amount of non-linear + reasoning before running the linear prover of :tacn:`lra`. This pre-processing + does the following: + If the context contains an arithmetic expression of the form @@ -201,7 +206,7 @@ does the following: + For all pairs of hypotheses :math:`e_1 \ge 0`, :math:`e_2 \ge 0`, the context is enriched with :math:`e_1 \times e_2 \ge 0`. -After this pre-processing, the linear prover of `lra` searches for a +After this pre-processing, the linear prover of :tacn:`lra` searches for a proof by abstracting monomials by variables. `nia`: a proof procedure for non-linear integer arithmetic @@ -210,9 +215,9 @@ proof by abstracting monomials by variables. .. tacn:: nia :name: nia -This tactic is a proof procedure for non-linear integer arithmetic. -It performs a pre-processing similar to `nra`. The obtained goal is -solved using the linear integer prover `lia`. + This tactic is a proof procedure for non-linear integer arithmetic. + It performs a pre-processing similar to :tacn:`nra`. The obtained goal is + solved using the linear integer prover :tacn:`lia`. `psatz`: a proof procedure for non-linear arithmetic ---------------------------------------------------- @@ -220,22 +225,22 @@ solved using the linear integer prover `lia`. .. tacn:: psatz :name: psatz -This tactic explores the :math:`\mathit{Cone}` by increasing degrees – hence the -depth parameter :math:`n`. In theory, such a proof search is complete – if the -goal is provable the search eventually stops. Unfortunately, the -external oracle is using numeric (approximate) optimization techniques -that might miss a refutation. + This tactic explores the *Cone* by increasing degrees – hence the + depth parameter *n*. In theory, such a proof search is complete – if the + goal is provable the search eventually stops. Unfortunately, the + external oracle is using numeric (approximate) optimization techniques + that might miss a refutation. -To illustrate the working of the tactic, consider we wish to prove the -following Coq goal: + To illustrate the working of the tactic, consider we wish to prove the + following Coq goal: .. coqtop:: all - Require Import ZArith Psatz. - Open Scope Z_scope. - Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False. - intro x. - psatz Z 2. + Require Import ZArith Psatz. + Open Scope Z_scope. + Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False. + intro x. + psatz Z 2. As shown, such a goal is solved by ``intro x. psatz Z 2.``. The oracle returns the cone expression :math:`2 \times (x-1) + (\mathbf{x-1}) \times (\mathbf{x−1}) + -x^2` @@ -247,7 +252,6 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid. the `zify` tactic. .. [#] Sources and binaries can be found at https://projects.coin-or.org/Csdp .. [#] Variants deal with equalities and strict inequalities. -.. [#] More efficient linear programming techniques could equally be employed. .. [#] In practice, the oracle might fail to produce such a refutation. .. comment in original TeX: diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst index 828505b850..03d4f148e3 100644 --- a/doc/sphinx/addendum/omega.rst +++ b/doc/sphinx/addendum/omega.rst @@ -23,13 +23,6 @@ Description of ``omega`` If the tactic cannot solve the goal, it fails with an error message. In any case, the computation eventually stops. -.. tacv:: romega - :name: romega - - .. deprecated:: 8.9 - - Use :tacn:`lia` instead. - Arithmetical goals recognized by ``omega`` ------------------------------------------ diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib index aa8537c92d..d9eaa2c6c6 100644 --- a/doc/sphinx/biblio.bib +++ b/doc/sphinx/biblio.bib @@ -294,6 +294,17 @@ s}, year = {1994} } +@Article{Myers, + author = {Eugene Myers}, + title = {An {O(ND)} difference algorithm and its variations}, + journal = {Algorithmica}, + volume = {1}, + number = {2}, + year = {1986}, + bibsource = {https://link.springer.com/article/10.1007\%2FBF01840446}, + url = {http://www.xmailserver.org/diff2.pdf} +} + @InProceedings{Parent95b, author = {C. Parent}, booktitle = {{Mathematics of Program Construction'95}}, diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 71f01cbb17..d98b8641e9 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -193,8 +193,9 @@ html_theme = 'sphinx_rtd_theme' # Theme options are theme-specific and customize the look and feel of a theme # further. For a list of options available for each theme, see the # documentation. -#html_theme_options = {} - +html_theme_options = { + 'collapse_navigation': False +} html_context = { 'display_github': True, 'github_user': 'coq', diff --git a/doc/sphinx/credits.html.rst b/doc/sphinx/credits.html.rst deleted file mode 100644 index 0b2b1c6ad1..0000000000 --- a/doc/sphinx/credits.html.rst +++ /dev/null @@ -1,7 +0,0 @@ -.. _credits: - -------- -Credits -------- - -.. include:: credits-contents.rst diff --git a/doc/sphinx/credits.latex.rst b/doc/sphinx/credits.latex.rst deleted file mode 100644 index 39101f9d52..0000000000 --- a/doc/sphinx/credits.latex.rst +++ /dev/null @@ -1,3 +0,0 @@ -.. _credits: - -.. include:: credits-contents.rst diff --git a/doc/sphinx/credits-contents.rst b/doc/sphinx/credits.rst index 212f0a65b0..4f5064839b 100644 --- a/doc/sphinx/credits-contents.rst +++ b/doc/sphinx/credits.rst @@ -1,3 +1,7 @@ +------- +Credits +------- + Coq is a proof assistant for higher-order logic, allowing the development of computer programs consistent with their formal specification. It is the result of about ten years of research of the @@ -116,7 +120,7 @@ G. Dowek, allowed hierarchical developments of mathematical theories. This high-level language was called the *Mathematical Vernacular*. Furthermore, an interactive *Theorem Prover* permitted the incremental construction of proof trees in a top-down manner, subgoaling recursively -and backtracking from dead-alleys. The theorem prover executed tactics +and backtracking from dead-ends. The theorem prover executed tactics written in CAML, in the LCF fashion. A basic set of tactics was predefined, which the user could extend by his own specific tactics. This system (Version 4.10) was released in 1989. Then, the system was @@ -186,7 +190,7 @@ definitions of “inversion predicates”. | Credits: addendum for version 6.1 -================================= +--------------------------------- The present version 6.1 of |Coq| is based on the V5.10 architecture. It was ported to the new language Objective Caml by Bruno Barras. The @@ -223,7 +227,7 @@ Barras. | Credits: addendum for version 6.2 -================================= +--------------------------------- In version 6.2 of |Coq|, the parsing is done using camlp4, a preprocessor and pretty-printer for CAML designed by Daniel de Rauglaudre at INRIA. @@ -268,7 +272,7 @@ Loiseleur. | Credits: addendum for version 6.3 -================================= +--------------------------------- The main changes in version V6.3 were the introduction of a few new tactics and the extension of the guard condition for fixpoint @@ -301,7 +305,7 @@ Monin from CNET Lannion. | Credits: versions 7 -=================== +------------------- The version V7 is a new implementation started in September 1999 by Jean-Christophe Filliâtre. This is a major revision with respect to the @@ -390,7 +394,7 @@ J.-F. Monin from France Telecom R & D. | Credits: version 8.0 -==================== +-------------------- Coq version 8 is a major revision of the |Coq| proof assistant. First, the underlying logic is slightly different. The so-called *impredicativity* @@ -492,7 +496,7 @@ under the responsibility of Christine Paulin. | Credits: version 8.1 -==================== +-------------------- Coq version 8.1 adds various new functionalities. @@ -571,7 +575,7 @@ and Yale University. | Credits: version 8.2 -==================== +-------------------- Coq version 8.2 adds new features, new libraries and improves on many various aspects. @@ -665,7 +669,7 @@ the Coq-Club mailing list. | Credits: version 8.3 -==================== +-------------------- Coq version 8.3 is before all a transition version with refinements or extensions of the existing features and libraries and a new tactic nsatz @@ -739,7 +743,7 @@ Pierce for the excellent teaching materials they provided. | Credits: version 8.4 -==================== +-------------------- Coq version 8.4 contains the result of three long-term projects: a new modular library of arithmetic by Pierre Letouzey, a new proof engine by @@ -895,7 +899,7 @@ Eelis van der Weegen. | Credits: version 8.5 -==================== +-------------------- Coq version 8.5 contains the result of five specific long-term projects: @@ -1049,7 +1053,7 @@ Tankink. Maxime Dénès coordinated the release process. | Credits: version 8.6 -==================== +-------------------- Coq version 8.6 contains the result of refinements, stabilization of 8.5’s features and cleanups of the internals of the system. Over the @@ -1189,7 +1193,8 @@ Dénès to put together a |Coq| consortium. | Credits: version 8.7 -==================== +-------------------- + |Coq| version 8.7 contains the result of refinements, stabilization of features and cleanups of the internals of the system along with a few new features. The main user visible changes are: @@ -1238,7 +1243,7 @@ of integers and real constants are now represented using `IZR` (work by Guillaume Melquiond). Standard library additions and improvements by Jason Gross, Pierre Letouzey and -others, documented in the `CHANGES` file. +others, documented in the ``CHANGES.md`` file. The mathematical proof language/declarative mode plugin was removed from the archive. @@ -1294,8 +1299,7 @@ system, is now upcoming and will rely on Inria’s newly created Foundation. | Credits: version 8.8 -==================== - +-------------------- |Coq| version 8.8 contains the result of refinements and stabilization of features and deprecations, cleanups of the internals of the system along @@ -1352,7 +1356,7 @@ version. Version 8.8 also comes with a bunch of smaller-scale changes and improvements regarding the different components of the system. -Most important ones are documented in the ``CHANGES`` file. +Most important ones are documented in the ``CHANGES.md`` file. The efficiency of the whole system has seen improvements thanks to contributions from Gaëtan Gilbert, Pierre-Marie Pédrot, Maxime Dénès and @@ -1400,3 +1404,150 @@ The contacts of the Coq Consortium are Yves Bertot and Maxime Dénès. | Santiago de Chile, March 2018, | Matthieu Sozeau for the |Coq| development team | + +Credits: version 8.9 +-------------------- + +|Coq| version 8.9 contains the result of refinements and stabilization +of features and deprecations or removals of deprecated features, +cleanups of the internals of the system and API along with a few new +features. This release includes many user-visible changes, including +deprecations that are documented in ``CHANGES.md`` and new features that +are documented in the reference manual. Here are the most important +changes: + +- Kernel: mutually recursive records are now supported, by Pierre-Marie + Pédrot. + +- Notations: + + - Support for autonomous grammars of terms called "custom entries", by + Hugo Herbelin (see section :ref:`custom-entries` of the reference + manual). + + - Deprecated notations of the standard library will be removed in the + next version of |Coq|, see the ``CHANGES.md`` file for a script to + ease porting, by Jason Gross and Jean-Christophe Léchenet. + + - Added the :cmd:`Numeral Notation` command for registering decimal + numeral notations for custom types, by Daniel de Rauglaudre, Pierre + Letouzey and Jason Gross. + +- Tactics: Introduction tactics :tacn:`intro`/:tacn:`intros` on a goal that is an + existential variable now force a refinement of the goal into a + dependent product rather than failing, by Hugo Herbelin. + +- Decision procedures: deprecation of tactic ``romega`` in favor of + :tacn:`lia` and removal of ``fourier``, replaced by :tacn:`lra` which + subsumes it, by Frédéric Besson, Maxime Dénès, Vincent Laporte and + Laurent Théry. + +- Proof language: focusing bracket ``{`` now supports named + :ref:`goals <curly-braces>`, e.g. ``[x]:{`` will focus + on a goal (existential variable) named ``x``, by Théo Zimmermann. + +- SSReflect: the implementation of delayed clear was simplified by + Enrico Tassi: the variables are always renamed using inaccessible + names when the clear switch is processed and finally cleared at the + end of the intro pattern. In addition to that the use-and-discard flag + `{}` typical of rewrite rules can now be also applied to views, + e.g. `=> {}/v` applies `v` and then clears `v`. See section + :ref:`introduction_ssr`. + +- Vernacular: + + - Experimental support for :ref:`attributes <gallina-attributes>` on + commands, by Vincent Laporte, as in ``#[local] Lemma foo : bar.`` + Tactics and tactic notations now support the ``deprecated`` + attribute. + + - Removed deprecated commands ``Arguments Scope`` and ``Implicit + Arguments`` in favor of :cmd:`Arguments`, with the help of Jasper + Hugunin. + + - New flag :flag:`Uniform Inductive Parameters` by Jasper Hugunin to + avoid repeating uniform parameters in constructor declarations. + + - New commands :cmd:`Hint Variables` and :cmd:`Hint Constants`, by + Matthieu Sozeau, for controlling the opacity status of variables and + constants in hint databases. It is recommended to always use these + commands after creating a hint databse with :cmd:`Create HintDb`. + + - Multiple sections with the same name are now allowed, by Jasper + Hugunin. + +- Library: additions and changes in the ``VectorDef``, ``Ascii`` and + ``String`` library. Syntax notations are now available only when using + ``Import`` of libraries and not merely ``Require``, by various + contributors (source of incompatibility, see `CHANGES.md` for details). + +- Toplevels: ``coqtop`` and ``coqide`` can now display diffs between proof + steps in color, using the :opt:`Diffs` option, by Jim Fehrle. + +- Documentation: we integrated a large number of fixes to the new Sphinx + documentation by various contributors, coordinated by Clément + Pit-Claudel and Théo Zimmermann. + +- Tools: removed the ``gallina`` utility and the homebrewed ``Emacs`` mode. + +- Packaging: as in |Coq| 8.8.2, the Windows installer now includes many + more external packages that can be individually selected for + installation, by Michael Soegtrop. + +Version 8.9 also comes with a bunch of smaller-scale changes and +improvements regarding the different components of the system. Most +important ones are documented in the ``CHANGES.md`` file. + +On the implementation side, the ``dev/doc/changes.md`` file documents +the numerous changes to the implementation and improvements of +interfaces. The file provides guidelines on porting a plugin to the new +version and a plugin development tutorial kept in sync with Coq was +introduced by Yves Bertot http://github.com/ybertot/plugin_tutorials. +The new ``dev/doc/critical-bugs`` file documents the known critical bugs +of |Coq| and affected releases. + +The efficiency of the whole system has seen improvements thanks to +contributions from Gaëtan Gilbert, Pierre-Marie Pédrot, and Maxime Dénès. + +Maxime Dénès, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Michael +Soegtrop, Théo Zimmermann worked on maintaining and improving the +continuous integration system. + +The OPAM repository for |Coq| packages has been maintained by Guillaume +Melquiond, Matthieu Sozeau, Enrico Tassi with contributions from many +users. A list of packages is available at https://coq.inria.fr/opam/www. + +The 54 contributors for this version are Léo Andrès, Rin Arakaki, +Benjamin Barenblat, Langston Barrett, Siddharth Bhat, Martin Bodin, +Simon Boulier, Timothy Bourke, Joachim Breitner, Tej Chajed, Arthur +Charguéraud, Pierre Courtieu, Maxime Dénès, Andres Erbsen, Jim Fehrle, +Julien Forest, Emilio Jesus Gallego Arias, Gaëtan Gilbert, Matěj +Grabovský, Jason Gross, Samuel Gruetter, Armaël Guéneau, Hugo Herbelin, +Jasper Hugunin, Ralf Jung, Sam Pablo Kuper, Ambroise Lafont, Leonidas +Lampropoulos, Vincent Laporte, Peter LeFanu Lumsdaine, Pierre Letouzey, +Jean-Christophe Léchenet, Nick Lewycky, Yishuai Li, Sven M. Hallberg, +Assia Mahboubi, Cyprien Mangin, Guillaume Melquiond, Perry E. Metzger, +Clément Pit-Claudel, Pierre-Marie Pédrot, Daniel R. Grayson, Kazuhiko +Sakaguchi, Michael Soegtrop, Matthieu Sozeau, Paul Steckler, Enrico +Tassi, Laurent Théry, Anton Trunov, whitequark, Théo Winterhalter, +Zeimer, Beta Ziliani, Théo Zimmermann. + +Many power users helped to improve the design of the new features via +the issue and pull request system, the |Coq| development mailing list or +the coq-club@inria.fr mailing list. It would be impossible to mention +exhaustively the names of everybody who to some extent influenced the +development. + +Version 8.9 is the fourth release of |Coq| developed on a time-based +development cycle. Its development spanned 7 months from the release of +|Coq| 8.8. The development moved to a decentralized merging process +during this cycle. Guillaume Melquiond was in charge of the release +process and is the maintainer of this release. This release is the +result of ~2,000 commits and ~500 PRs merged, closing 75+ issues. + +The |Coq| development team welcomed Vincent Laporte, a new |Coq| +engineer working with Maxime Dénès in the |Coq| consortium. + +| Paris, October 2018, +| Matthieu Sozeau for the |Coq| development team +| diff --git a/doc/sphinx/index.html.rst b/doc/sphinx/index.html.rst index cf12b57414..a652b9e1ca 100644 --- a/doc/sphinx/index.html.rst +++ b/doc/sphinx/index.html.rst @@ -1,13 +1,11 @@ -.. _introduction: - ========================== -Introduction +Introduction and Contents ========================== .. include:: introduction.rst -Table of contents ------------------ +Contents +-------- .. toctree:: :caption: Indexes @@ -82,9 +80,6 @@ Table of contents zebibliography -License -------- - .. include:: license.rst .. [#PG] Proof-General is available at https://proofgeneral.github.io/. diff --git a/doc/sphinx/index.latex.rst b/doc/sphinx/index.latex.rst index af757f8746..9e9eb330fe 100644 --- a/doc/sphinx/index.latex.rst +++ b/doc/sphinx/index.latex.rst @@ -2,26 +2,22 @@ The Coq Reference Manual ========================== +------------ Introduction ------------ .. include:: introduction.rst +.. include:: license.rst + .. [#PG] Proof-General is available at https://proofgeneral.github.io/. Optionally, you can enhance it with the minor mode Company-Coq :cite:`Pit16` (see https://github.com/cpitclaudel/company-coq). -Credits -------- - .. include:: credits.rst -License -------- - -.. include:: license.rst - +------------ The language ------------ @@ -33,6 +29,7 @@ The language language/cic language/module-system +---------------- The proof engine ---------------- @@ -45,6 +42,7 @@ The proof engine proof-engine/detailed-tactic-examples proof-engine/ssreflect-proof-language +--------------- User extensions --------------- @@ -53,6 +51,7 @@ User extensions user-extensions/syntax-extensions user-extensions/proof-schemes +--------------- Practical tools --------------- @@ -62,6 +61,7 @@ Practical tools practical-tools/utilities practical-tools/coqide +-------- Addendum -------- diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index 5bb7bf542c..bcdf3277ad 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -44,7 +44,7 @@ are processed from a file. .. seealso:: :ref:`thecoqcommands`. How to read this book -===================== +--------------------- This is a Reference Manual, so it is not intended for continuous reading. We recommend using the various indexes to quickly locate the documentation @@ -90,7 +90,7 @@ Nonetheless, the manual has some structure that is explained below. solvers and tactics. See the table of contents for a complete list. List of additional documentation -================================ +-------------------------------- This manual does not contain all the documentation the user may need about |Coq|. Various informations can be found in the following documents: diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 381f8bb661..cc5d9d6205 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -533,10 +533,10 @@ Convertibility Let us write :math:`E[Γ] ⊢ t \triangleright u` for the contextual closure of the relation :math:`t` reduces to :math:`u` in the global environment :math:`E` and local context :math:`Γ` with one of the previous -reductions β, ι, δ or ζ. +reductions β, δ, ι or ζ. We say that two terms :math:`t_1` and :math:`t_2` are -*βιδζη-convertible*, or simply *convertible*, or *equivalent*, in the +*βδιζη-convertible*, or simply *convertible*, or *equivalent*, in the global environment :math:`E` and local context :math:`Γ` iff there exist terms :math:`u_1` and :math:`u_2` such that :math:`E[Γ] ⊢ t_1 \triangleright … \triangleright u_1` and :math:`E[Γ] ⊢ t_2 \triangleright … \triangleright u_2` and either :math:`u_1` and @@ -678,7 +678,7 @@ form*. There are several ways (or strategies) to apply the reduction rules. Among them, we have to mention the *head reduction* which will play an important role (see Chapter :ref:`tactics`). Any term :math:`t` can be written as :math:`λ x_1 :T_1 . … λ x_k :T_k . (t_0~t_1 … t_n )` where :math:`t_0` is not an -application. We say then that :math:`t~0` is the *head of* :math:`t`. If we assume +application. We say then that :math:`t_0` is the *head of* :math:`t`. If we assume that :math:`t_0` is :math:`λ x:T. u_0` then one step of β-head reduction of :math:`t` is: .. math:: @@ -771,8 +771,8 @@ the sort of the inductive type t (not to be confused with :math:`\Sort` which is \odd&:&\nat → \Prop \end{array}\right]} {\left[\begin{array}{rcl} \evenO &:& \even~0\\ - \evenS &:& \forall n, \odd~n -> \even~(\kw{S}~n)\\ - \oddS &:& \forall n, \even~n -> \odd~(\kw{S}~n) + \evenS &:& \forall n, \odd~n → \even~(\kw{S}~n)\\ + \oddS &:& \forall n, \even~n → \odd~(\kw{S}~n) \end{array}\right]} which corresponds to the result of the |Coq| declaration: diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 636144e0c8..9dae7fd102 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -606,7 +606,7 @@ for several ways of defining a function *and other useful related objects*, namely: an induction principle that reflects the recursive structure of the function (see :tacn:`function induction`) and its fixpoint equality. The meaning of this declaration is to define a function ident, -similarly to ``Fixpoint`. Like in ``Fixpoint``, the decreasing argument must +similarly to ``Fixpoint``. Like in ``Fixpoint``, the decreasing argument must be given (unless the function is not recursive), but it might not necessarily be *structurally* decreasing. The point of the {} annotation is to name the decreasing argument *and* to describe which kind of diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index daf34500bf..1a33a9a46e 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -522,7 +522,7 @@ The Vernacular ============== .. productionlist:: coq - decorated-sentence : [`decoration`] `sentence` + decorated-sentence : [ `decoration` … `decoration` ] `sentence` sentence : `assumption` : | `definition` : | `inductive` @@ -1112,6 +1112,59 @@ co-inductive definitions are also allowed. object of type :g:`(EqSt s1 s2)`. We will see how to introduce infinite objects in Section :ref:`cofixpoint`. +Caveat +++++++ + +The ability to define co-inductive types by constructors, hereafter called +*positive co-inductive types*, is known to break subject reduction. The story is +a bit long: this is due to dependent pattern-matching which implies +propositional η-equality, which itself would require full η-conversion for +subject reduction to hold, but full η-conversion is not acceptable as it would +make type-checking undecidable. + +Since the introduction of primitive records in Coq 8.5, an alternative +presentation is available, called *negative co-inductive types*. This consists +in defining a co-inductive type as a primitive record type through its +projections. Such a technique is akin to the *co-pattern* style that can be +found in e.g. Agda, and preserves subject reduction. + +The above example can be rewritten in the following way. + +.. coqtop:: all + + Set Primitive Projections. + CoInductive Stream : Set := Seq { hd : nat; tl : Stream }. + CoInductive EqSt (s1 s2: Stream) : Prop := eqst { + eqst_hd : hd s1 = hd s2; + eqst_tl : EqSt (tl s1) (tl s2); + }. + +Some properties that hold over positive streams are lost when going to the +negative presentation, typically when they imply equality over streams. +For instance, propositional η-equality is lost when going to the negative +presentation. It is nonetheless logically consistent to recover it through an +axiom. + +.. coqtop:: all + + Axiom Stream_eta : forall s: Stream, s = cons (hs s) (tl s). + +More generally, as in the case of positive coinductive types, it is consistent +to further identify extensional equality of coinductive types with propositional +equality: + +.. coqtop:: all + + Axiom Stream_ext : forall (s1 s2: Stream), EqSt s1 s2 -> s1 = s2. + +As of Coq 8.9, it is now advised to use negative co-inductive types rather than +their positive counterparts. + +.. seealso:: + :ref:`primitive_projections` for more information about negative + records and primitive projections. + + Definition of recursive functions --------------------------------- @@ -1422,15 +1475,6 @@ using the keyword :cmd:`Qed`. #. One can also use :cmd:`Admitted` in place of :cmd:`Qed` to turn the current asserted statement into an axiom and exit the proof editing mode. -.. [1] - This is similar to the expression “*entry* :math:`\{` sep *entry* - :math:`\}`” in standard BNF, or “*entry* :math:`(` sep *entry* - :math:`)`\ \*” in the syntax of regular expressions. - -.. [2] - Except if the inductive type is empty in which case there is no - equation that can be used to infer the return type. - .. _gallina-attributes: Attributes @@ -1438,7 +1482,7 @@ Attributes Any vernacular command can be decorated with a list of attributes, enclosed between ``#[`` (hash and opening square bracket) and ``]`` (closing square bracket) -and separated by commas ``,``. +and separated by commas ``,``. Multiple space-separated blocks may be provided. Each attribute has a name (an identifier) and may have a value. A value is either a :token:`string` (in which case it is specified with an equal ``=`` sign), @@ -1466,12 +1510,14 @@ the following attributes names are recognized: This attribute can trigger the following warnings: .. warn:: Tactic @qualid is deprecated since @string. @string. + :undocumented: .. warn:: Tactic Notation @qualid is deprecated since @string. @string. + :undocumented: -Here are a few examples: +.. example:: -.. coqtop:: all reset + .. coqtop:: all reset From Coq Require Program. #[program] Definition one : nat := S _. @@ -1486,3 +1532,12 @@ Here are a few examples: Proof. now foo. Abort. + +.. [1] + This is similar to the expression “*entry* :math:`\{` sep *entry* + :math:`\}`” in standard BNF, or “*entry* :math:`(` sep *entry* + :math:`)`\ \*” in the syntax of regular expressions. + +.. [2] + Except if the inductive type is empty in which case there is no + equation that can be used to infer the return type. diff --git a/doc/sphinx/license.rst b/doc/sphinx/license.rst index 232b04211c..55c6d988f0 100644 --- a/doc/sphinx/license.rst +++ b/doc/sphinx/license.rst @@ -1,3 +1,6 @@ +License +------- + This material (the Coq Reference Manual) may be distributed only subject to the terms and conditions set forth in the Open Publication License, v1.0 or later (the latest version is presently available at diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 343ca9ed7d..de9e327740 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -85,6 +85,8 @@ Some |Coq| commands call other |Coq| commands. In this case, they look for the commands in directory specified by ``$COQBIN``. If this variable is not set, they look for the commands in the executable path. +.. _COQ_COLORS: + The ``$COQ_COLORS`` environment variable can be used to specify the set of colors used by ``coqtop`` to highlight its output. It uses the same syntax as the ``$LS_COLORS`` variable from GNU’s ls, that is, a colon-separated @@ -93,6 +95,15 @@ list of assignments of the form :n:`name={*; attr}` where ANSI escape code. The list of highlight tags can be retrieved with the ``-list-tags`` command-line option of ``coqtop``. +The string uses ANSI escape codes to represent attributes. For example: + + ``export COQ_COLORS=”diff.added=4;48;2;0;0;240:diff.removed=41”`` + +sets the highlights for added text in diffs to underlined (the 4) with a background RGB +color (0, 0, 240) and for removed text in diffs to a red background. +Note that if you specify ``COQ_COLORS``, the predefined attributes are ignored. + + .. _command-line-options: By command line options @@ -164,9 +175,13 @@ and ``coqtop``, unless stated otherwise: :-w (all|none|w₁,…,wₙ): Configure the display of warnings. This option expects all, none or a comma-separated list of warning names or categories (see Section :ref:`controlling-display`). -:-color (on|off|auto): Enable or not the coloring of output of `coqtop`. - Default is auto, meaning that `coqtop` dynamically decides, depending on - whether the output channel supports ANSI escape sequences. +:-color (on|off|auto): *Coqtop only*. Enable or disable color output. + Default is auto, meaning color is shown only if + the output channel supports ANSI escape sequences. +:-diffs (on|off|removed): *Coqtop only*. Controls highlighting of differences + between proof steps. ``on`` highlights added tokens, ``removed`` highlights both added and + removed tokens. Requires that ``–color`` is enabled. (see Section + :ref:`showing_diffs`). :-beautify: Pretty-print each command to *file.beautified* when compiling *file.v*, in order to get old-fashioned syntax/definitions/notations. diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 5d300c3d6d..7c78e1a50f 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -21,16 +21,16 @@ 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 + topbin/coqtop_bin.ml -o my_toplevel.native -For example, to statically link |L_tac|, you can just do: +For example, to statically link |Ltac|, you can just do: :: % ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg \ - -package coq.toplevel -package coq.ltac \ - toplevel/coqtop\_bin.ml -o my\_toplevel.native + -package coq.toplevel,coq.plugins.ltac \ + topbin/coqtop_bin.ml -o my_toplevel.native and similarly for other plugins. @@ -41,15 +41,17 @@ 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:`command-line-options`). Collecting the list of files and options is the job -of the ``_CoqProject`` file. +options to ``coqc`` (e.g. ``-R``, ``Q``, ``-I``, see :ref:`command +line options <command-line-options>`). 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 + -arg -w + -arg all theories/foo.v theories/bar.v -I src/ @@ -57,6 +59,11 @@ A simple example of a ``_CoqProject`` file follows: src/bazaux.ml src/qux_plugin.mlpack +where options ``-R``, ``-Q`` and ``-I`` are natively recognized, as well as +file names. The lines of the form ``-arg foo`` are used in order to tell +to literally pass an argument ``foo`` to ``coqc``: in the +example, this allows to pass the two-word option ``-w all`` (see +:ref:`command line options <command-line-options>`). Currently, both |CoqIDE| and Proof-General (version ≥ ``4.3pre``) understand ``_CoqProject`` files and invoke |Coq| with the desired options. diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 4b1b7719c5..741f9fe5b0 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -144,8 +144,9 @@ list of assertion commands is given in :ref:`Assertions`. The command 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. + example, if ``T`` is a variable and ``a`` is a variable of type + ``T``, then the commands ``Proof using a`` and ``Proof using T a`` + are equivalent. .. cmdv:: Proof using {+ @ident } with @tactic @@ -495,6 +496,10 @@ Requesting information eexists ?[n]. Show n. + .. coqtop:: none + + Abort. + .. cmdv:: Show Script :name: Show Script @@ -581,6 +586,163 @@ Requesting information fixpoint and cofixpoint is violated at some time of the construction of the proof without having to wait the completion of the proof. +.. _showing_diffs: + +Showing differences between proof steps +--------------------------------------- + + +Coq can automatically highlight the differences between successive proof steps. +For example, the following screenshots of CoqIDE and coqtop show the application +of the same :tacn:`intros` tactic. The tactic creates two new hypotheses, highlighted in green. +The conclusion is entirely in pale green because although it’s changed, no tokens were added +to it. The second screenshot uses the "removed" option, so it shows the conclusion a +second time with the old text, with deletions marked in red. Also, since the hypotheses are +new, no line of old text is shown for them. + +.. comment screenshot produced with: + Inductive ev : nat -> Prop := + | ev_0 : ev 0 + | ev_SS : forall n : nat, ev n -> ev (S (S n)). + + Fixpoint double (n:nat) := + match n with + | O => O + | S n' => S (S (double n')) + end. + + Goal forall n, ev n -> exists k, n = double k. + intros n E. + +.. + + .. image:: ../_static/diffs-coqide-on.png + :alt: |CoqIDE| with Set Diffs on + +.. + + .. image:: ../_static/diffs-coqide-removed.png + :alt: |CoqIDE| with Set Diffs removed + +.. + + .. image:: ../_static/diffs-coqtop-on3.png + :alt: coqtop with Set Diffs on + +How to enable diffs +``````````````````` + +.. opt:: Diffs %( "on" %| "off" %| "removed" %) + :name: Diffs + + The “on” option highlights added tokens in green, while the “removed” option + additionally reprints items with removed tokens in red. Unchanged tokens in + modified items are shown with pale green or red. (Colors are user-configurable.) + +For coqtop, showing diffs can be enabled when starting coqtop with the +``-diffs on|off|removed`` command-line option or by setting the :opt:`Diffs` option +within Coq. You will need to provide the ``-color on|auto`` command-line option when +you start coqtop in either case. + +Colors for coqtop can be configured by setting the ``COQ_COLORS`` environment +variable. See section :ref:`customization-by-environment-variables`. Diffs +use the tags ``diff.added``, ``diff.added.bg``, ``diff.removed`` and ``diff.removed.bg``. + +In CoqIDE, diffs should be enabled from the ``View`` menu. Don’t use the ``Set Diffs`` +command in CoqIDE. You can change the background colors shown for diffs from the +``Edit | Preferences | Tags`` panel by changing the settings for the ``diff.added``, +``diff.added.bg``, ``diff.removed`` and ``diff.removed.bg`` tags. This panel also +lets you control other attributes of the highlights, such as the foreground +color, bold, italic, underline and strikeout. + +Note: As of this writing (August 2018), Proof General will need minor changes +to be able to show diffs correctly. We hope it will support this feature soon. +See https://github.com/ProofGeneral/PG/issues/381 for the current status. + +How diffs are calculated +```````````````````````` + +Diffs are calculated as follows: + +1. Select the old proof state to compare to, which is the proof state before + the last tactic that changed the proof. Changes that only affect the view + of the proof, such as ``all: swap 1 2``, are ignored. + +2. For each goal in the new proof state, determine what old goal to compare + it to—the one it is derived from or is the same as. Match the hypotheses by + name (order is ignored), handling compacted items specially. + +3. For each hypothesis and conclusion (the “items”) in each goal, pass + them as strings to the lexer to break them into tokens. Then apply the + Myers diff algorithm :cite:`Myers` on the tokens and add appropriate highlighting. + +Notes: + +* Aside from the highlights, output for the "on" option should be identical + to the undiffed output. +* Goals completed in the last proof step will not be shown even with the + "removed" setting. + +.. comment The following screenshots show diffs working with multiple goals and with compacted + hypotheses. In the first one, notice that the goal ``P 1`` is not highlighted at + all after the split because it has not changed. + + .. todo: Use this script and remove the screenshots when COQ_COLORS + works for coqtop in sphinx + .. coqtop:: none + + Set Diffs "on". + Parameter P : nat -> Prop. + Goal P 1 /\ P 2 /\ P 3. + + .. coqtop:: out + + split. + + .. coqtop:: all + + 2: split. + + .. coqtop:: none + + Abort. + + .. + + .. coqtop:: none + + Set Diffs "on". + Goal forall n m : nat, n + m = m + n. + Set Diffs "on". + + .. coqtop:: out + + intros n. + + .. coqtop:: all + + intros m. + + .. coqtop:: none + + Abort. + +This screen shot shows the result of applying a :tacn:`split` tactic that replaces one goal +with 2 goals. Notice that the goal ``P 1`` is not highlighted at all after +the split because it has not changed. + +.. + + .. image:: ../_static/diffs-coqide-multigoal.png + :alt: coqide with Set Diffs on with multiple goals + +This is how diffs may appear after applying a :tacn:`intro` tactic that results +in compacted hypotheses: + +.. + + .. image:: ../_static/diffs-coqide-compacted.png + :alt: coqide with Set Diffs on with compacted hyptotheses Controlling the effect of proof editing commands ------------------------------------------------ diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 52609546d5..3ca0ffe678 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -916,11 +916,8 @@ but also folds ``x`` in the goal. .. coqtop:: reset From Coq Require Import ssreflect. - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. - .. coqtop:: all undo + .. coqtop:: all Lemma test x t (Hx : x = 3) : x + t = 4. set z := 3 in Hx. @@ -929,6 +926,10 @@ If the localization also mentions the goal, then the result is the following one .. example:: + .. coqtop:: reset + + From Coq Require Import ssreflect. + .. coqtop:: all Lemma test x t (Hx : x = 3) : x + t = 4. @@ -2485,8 +2486,7 @@ destruction of existential assumptions like in the tactic: .. coqtop:: all Lemma test : True. - have [x Px]: exists x : nat, x > 0. - Focus 2. + have [x Px]: exists x : nat, x > 0; last first. An alternative use of the ``have`` tactic is to provide the explicit proof term for the intermediate lemma, using tactics of the form: @@ -2564,8 +2564,7 @@ copying the goal itself. .. coqtop:: all Lemma test : True. - have suff H : 2 + 2 = 3. - Focus 2. + have suff H : 2 + 2 = 3; last first. Note that H is introduced in the second goal. @@ -2852,8 +2851,7 @@ pattern will be used to process its instance. .. coqtop:: all Lemma simple n (ngt0 : 0 < n ) : P n. - gen have ltnV, /andP[nge0 neq0] : n ngt0 / (0 <= n) && (n != 0). - Focus 2. + gen have ltnV, /andP[nge0 neq0] : n ngt0 / (0 <= n) && (n != 0); last first. .. _advanced_generalization_ssr: @@ -3556,6 +3554,7 @@ corresponding new goals will be generated. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. + Set Warnings "-notation-overridden". .. coqtop:: all @@ -3756,9 +3755,10 @@ which the function is supplied: :name: congr This tactic: -+ checks that the goal is a Leibniz equality -+ matches both sides of this equality with “term applied to some arguments”, inferring the right number of arguments from the goal and the type of term. This may expand some definitions or fixpoints. -+ generates the subgoals corresponding to pairwise equalities of the arguments present in the goal. + + + checks that the goal is a Leibniz equality; + + matches both sides of this equality with “term applied to some arguments”, inferring the right number of arguments from the goal and the type of term. This may expand some definitions or fixpoints; + + generates the subgoals corresponding to pairwise equalities of the arguments present in the goal. The goal can be a non dependent product ``P -> Q``. In that case, the system asserts the equation ``P = Q``, uses it to solve the goal, and @@ -4918,7 +4918,7 @@ which produces the converse implication. In both cases, the two first Prop arguments are implicit. If ``term`` is an instance of the ``reflect`` predicate, then ``A`` will be one -of the defined view hints for the ``reflec``t predicate, which are by +of the defined view hints for the ``reflect`` predicate, which are by default the ones present in the file ``ssrbool.v``. These hints are not only used for choosing the appropriate direction of the translation, but they also allow complex transformation, involving negations. @@ -4933,9 +4933,9 @@ but they also allow complex transformation, involving negations. Unset Printing Implicit Defensive. Section Test. - .. coqtop:: in + .. coqtop:: all - Lemma introN : forall (P : Prop) (b : bool), reflect P b -> ~ P -> ~~b. + Check introN. .. coqtop:: all @@ -4945,12 +4945,11 @@ but they also allow complex transformation, involving negations. In fact this last script does not exactly use the hint ``introN``, but the more general hint: - .. coqtop:: in + .. coqtop:: all - Lemma introNTF : forall (P : Prop) (b c : bool), - reflect P b -> (if c then ~ P else P) -> ~~ b = c. + Check introNTF. - The lemma ` `introN`` is an instantiation of introNF using c := true. + The lemma ``introN`` is an instantiation of ``introNF`` using ``c := true``. Note that views, being part of :token:`i_pattern`, can be used to interpret assertions too. For example the following script asserts ``a && b`` but diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index f99c539251..26f4ec6242 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -103,7 +103,7 @@ bindings_list`` where ``bindings_list`` may be of two different forms: .. exn:: Not the right number of missing arguments. -.. _occurencessets: +.. _occurrencessets: Occurrence sets and occurrence clauses ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1024,7 +1024,7 @@ Managing the local context This notation allows specifying which occurrences of :token:`term` have to be substituted in the context. The :n:`in @goal_occurrences` clause is an occurrence clause whose syntax and behavior are described in - :ref:`goal occurences <occurencessets>`. + :ref:`goal occurrences <occurrencessets>`. .. tacv:: set (@ident @binders := @term) {? in @goal_occurrences } @@ -1509,7 +1509,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) This syntax is used for selecting which occurrences of :token:`term` the case analysis has to be done on. The :n:`in @goal_occurrences` clause is an occurrence clause whose syntax and behavior is described - in :ref:`occurences sets <occurencessets>`. + in :ref:`occurrences sets <occurrencessets>`. .. tacv:: destruct @term {? with @bindings_list } {? as @disj_conj_intro_pattern } {? eqn:@naming_intro_pattern } {? using @term {? with @bindings_list } } {? in @goal_occurrences } edestruct @term {? with @bindings_list } {? as @disj_conj_intro_pattern } {? eqn:@naming_intro_pattern } {? using @term {? with @bindings_list } } {? in @goal_occurrences } @@ -1659,7 +1659,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) This syntax is used for selecting which occurrences of :n:`@term` the induction has to be carried on. The :n:`in @goal_occurrences` clause is an occurrence clause whose syntax and behavior is described in - :ref:`occurences sets <occurencessets>`. If variables or hypotheses not + :ref:`occurrences sets <occurrencessets>`. If variables or hypotheses not mentioning :n:`@term` in their type are listed in :n:`@goal_occurrences`, those are generalized as well in the statement to prove. @@ -2214,6 +2214,7 @@ and an explanation of the underlying technique. ``simple inversion``. .. tacv:: inversion @ident using @ident + :name: inversion ... using ... Let :n:`@ident` have type :g:`(I t)` (:g:`I` an inductive predicate) in the local context, and :n:`@ident` be a (dependent) inversion lemma. Then, this @@ -3512,6 +3513,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is Info 1 auto with eqdec. .. cmdv:: Hint Cut @regexp + :name: Hint Cut .. warning:: @@ -3545,6 +3547,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is initial cut expression being `emp`. .. cmdv:: Hint Mode @qualid {* (+ | ! | -)} + :name: Hint Mode This sets an optional mode of use of the identifier :n:`@qualid`. When proof-search faces a goal that ends in an application of :n:`@qualid` to diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 837d3f10a2..a69cf209c7 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -35,7 +35,7 @@ Displaying .. cmdv:: Print {? Term } @qualid\@@name This locally renames the polymorphic universes of :n:`@qualid`. - An underscore means the raw universe is printed. + An underscore means the usual name is printed. .. cmd:: About @qualid @@ -49,7 +49,7 @@ Displaying .. cmdv:: About @qualid\@@name This locally renames the polymorphic universes of :n:`@qualid`. - An underscore means the raw universe is printed. + An underscore means the usual name is printed. .. cmd:: Print All @@ -461,6 +461,7 @@ Requests to the environment .. note:: .. table:: Search Blacklist @string + :name: Search Blacklist Specifies a set of strings used to exclude lemmas from the results of :cmd:`Search`, :cmd:`SearchHead`, :cmd:`SearchPattern` and :cmd:`SearchRewrite` queries. A lemma whose @@ -1200,3 +1201,18 @@ scope of their effect. There are four kinds of commands: modifier extends the effect outside the module even when the command occurs in a section. The :cmd:`Set` and :cmd:`Unset` commands belong to this category. + +.. _exposing-constants-to-ocaml-libraries: + +Exposing constants to OCaml libraries +---------------------------------------------------------------- + +.. cmd:: Register @qualid__1 as @qualid__2 + + This command exposes the constant :n:`@qualid__1` to OCaml libraries under + the name :n:`@qualid__2`. This constant can then be dynamically located + calling :n:`Coqlib.lib_ref "@qualid__2"`; i.e., there is no need to known + where is the constant defined (file, module, library, etc.). + + Due to its internal nature, this command is not for general use. It is meant + to appear only in standard libraries and in support libraries of plug-ins. diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index 59cad3bea2..eacd7b4676 100644 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ b/doc/sphinx/user-extensions/proof-schemes.rst @@ -12,13 +12,15 @@ The ``Scheme`` command is a high-level tool for generating automatically (possibly mutual) induction principles for given types and sorts. Its syntax follows the schema: -.. cmd:: Scheme @ident := Induction for @ident Sort sort {* with @ident := Induction for @ident Sort sort} +.. cmd:: Scheme @ident__1 := Induction for @ident__2 Sort sort {* with @ident__i := Induction for @ident__j Sort sort} -where each `ident'ᵢ` is a different inductive type identifier -belonging to the same package of mutual inductive definitions. This -command generates the `identᵢ`s to be mutually recursive -definitions. Each term `identᵢ` proves a general principle of mutual -induction for objects in type `identᵢ`. + This command is a high-level tool for generating automatically + (possibly mutual) induction principles for given types and sorts. + Each :n:`@ident__j` is a different inductive type identifier belonging to + the same package of mutual inductive definitions. + The command generates the :n:`@ident__i`\s to be mutually recursive + definitions. Each term :n:`@ident__i` proves a general principle of mutual + induction for objects in type :n:`@ident__j`. .. cmdv:: Scheme @ident := Minimality for @ident Sort sort {* with @ident := Minimality for @ident' Sort sort} @@ -44,9 +46,9 @@ induction for objects in type `identᵢ`. .. coqtop:: none - Axiom A : Set. - Axiom B : Set. - + Axiom A : Set. + Axiom B : Set. + .. coqtop:: all Inductive tree : Set := node : A -> forest -> tree @@ -79,7 +81,7 @@ induction for objects in type `identᵢ`. .. coqtop:: all Inductive odd : nat -> Prop := oddS : forall n:nat, even n -> odd (S n) - with even : nat -> Prop := + with even : nat -> Prop := | evenO : even 0 | evenS : forall n:nat, odd n -> even (S n). @@ -136,19 +138,20 @@ Automatic declaration of schemes Combined Scheme ~~~~~~~~~~~~~~~~~~~~~~ -The ``Combined Scheme`` command is a tool for combining induction -principles generated by the ``Scheme command``. Its syntax follows the -schema : - -.. cmd:: Combined Scheme @ident from {+, ident} +.. cmd:: Combined Scheme @ident from {+, @ident__i} -where each identᵢ after the ``from`` is a different inductive principle that must -belong to the same package of mutual inductive principle definitions. -This command generates the leftmost `ident` to be the conjunction of the -principles: it is built from the common premises of the principles and -concluded by the conjunction of their conclusions. + This command is a tool for combining induction principles generated + by the :cmd:`Scheme` command. + Each :n:`@ident__i` is a different inductive principle that must belong + to the same package of mutual inductive principle definitions. + This command generates :n:`@ident` to be the conjunction of the + principles: it is built from the common premises of the principles + and concluded by the conjunction of their conclusions. + In the case where all the inductive principles used are in sort + ``Prop``, the propositional conjunction ``and`` is used, otherwise + the simple product ``prod`` is used instead. -.. example:: +.. example:: We can define the induction principles for trees and forests using: @@ -170,6 +173,23 @@ concluded by the conjunction of their conclusions. Check tree_forest_mutind. +.. example:: + + We can also combine schemes at sort ``Type``: + + .. coqtop:: all + + Scheme tree_forest_rect := Induction for tree Sort Type + with forest_tree_rect := Induction for forest Sort Type. + + .. coqtop:: all + + Combined Scheme tree_forest_mutrect from tree_forest_rect, forest_tree_rect. + + .. coqtop:: all + + Check tree_forest_mutrect. + .. _functional-scheme: Generation of induction principles with ``Functional`` ``Scheme`` @@ -186,7 +206,7 @@ schema: where each `ident'ᵢ` is a different mutually defined function name (the names must be in the same order as when they were defined). This command generates the induction principle for each `identᵢ`, following -the recursive structure and case analyses of the corresponding function +the recursive structure and case analyses of the corresponding function identᵢ’. .. warning:: @@ -196,7 +216,7 @@ identᵢ’. :cmd:`Function` generally produces smaller principles that are closer to how a user would implement them. See :ref:`advanced-recursive-functions` for details. -.. example:: +.. example:: Induction scheme for div2. @@ -262,11 +282,11 @@ identᵢ’. We define trees by the following mutual inductive type: .. original LaTeX had "Variable" instead of "Axiom", which generates an ugly warning - + .. coqtop:: reset all Axiom A : Set. - + Inductive tree : Set := node : A -> forest -> tree with forest : Set := @@ -313,20 +333,21 @@ identᵢ’. Check tree_size_ind2. .. _derive-inversion: - + Generation of inversion principles with ``Derive`` ``Inversion`` ----------------------------------------------------------------- -The syntax of ``Derive`` ``Inversion`` follows the schema: - .. cmd:: Derive Inversion @ident with forall (x : T), I t Sort sort -This command generates an inversion principle for the `inversion … using` -tactic. Let `I` be an inductive predicate and `x` the variables occurring -in t. This command generates and stocks the inversion lemma for the -sort `sort` corresponding to the instance `∀ (x:T), I t` with the name -`ident` in the global environment. When applied, it is equivalent to -having inverted the instance with the tactic `inversion`. + This command generates an inversion principle for the + :tacn:`inversion ... using ...` tactic. Let :g:`I` be an inductive + predicate and :g:`x` the variables occurring in t. This command + generates and stocks the inversion lemma for the sort :g:`sort` + corresponding to the instance :g:`∀ (x:T), I t` with the name + :n:`@ident` in the global environment. When applied, it is + equivalent to having inverted the instance with the tactic + :g:`inversion`. + .. cmdv:: Derive Inversion_clear @ident with forall (x:T), I t Sort sort @@ -347,7 +368,7 @@ having inverted the instance with the tactic `inversion`. Consider the relation `Le` over natural numbers and the following parameter ``P``: - + .. coqtop:: all Inductive Le : nat -> nat -> Set := @@ -370,9 +391,9 @@ having inverted the instance with the tactic `inversion`. .. coqtop:: none - Goal forall (n m : nat) (H : Le (S n) m), P n m. + Goal forall (n m : nat) (H : Le (S n) m), P n m. intros. - + .. coqtop:: all Show. diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 705d67e6c6..2214cbfb34 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -692,6 +692,8 @@ side. E.g.: Notation "'apply_id' f a1 .. an" := (.. (f a1) .. an) (at level 10, f ident, a1, an at level 9). +.. _custom-entries: + Custom entries ~~~~~~~~~~~~~~ @@ -1372,11 +1374,11 @@ Abbreviations denoted expression is performed at definition time. Type checking is done only at the time of use of the abbreviation. - Numeral notations ----------------- .. cmd:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope. + :name: Numeral Notation This command allows the user to customize the way numeral literals are parsed and printed. diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 0fa42cadad..e8f6decfbf 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -502,6 +502,7 @@ through the <tt>Require Import</tt> command.</p> theories/Strings/BinaryString.v theories/Strings/HexString.v theories/Strings/OctalString.v + theories/Strings/ByteVector.v </dd> <dt> <b>Reals</b>: @@ -600,8 +601,8 @@ through the <tt>Require Import</tt> command.</p> </dt> <dd> theories/Compat/AdmitAxiom.v - theories/Compat/Coq86.v theories/Compat/Coq87.v theories/Compat/Coq88.v + theories/Compat/Coq89.v </dd> </dl> diff --git a/doc/tools/Translator.tex b/doc/tools/Translator.tex index 3ee65d6f22..d8ac640f2a 100644 --- a/doc/tools/Translator.tex +++ b/doc/tools/Translator.tex @@ -490,7 +490,7 @@ to be applied are separated by a {\tt =>}. to turn implicit only the arguments that are {\em strictly} implicit (or rigid), i.e. that remains inferable whatever the other arguments are. For instance {\tt x} inferable from {\tt P x} is not strictly -inferable since it can disappears if {\tt P} is instanciated by a term +inferable since it can disappears if {\tt P} is instantiated by a term which erases {\tt x}. \begin{transbox} diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index edf4e6ec9d..2c69dcfe08 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -560,6 +560,9 @@ class CoqtopDirective(Directive): Print nat. Definition a := 1. + The blank line after the directive is required. If you begin a proof, + include an ``Abort`` afterwards to reset coqtop for the next example. + Here is a list of permissible options: - Display options |
