diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/credits.rst | 149 | ||||
| -rw-r--r-- | doc/sphinx/language/cic.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 39 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 4 |
5 files changed, 175 insertions, 26 deletions
diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst index ffdc4f3ec6..4f5064839b 100644 --- a/doc/sphinx/credits.rst +++ b/doc/sphinx/credits.rst @@ -120,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 @@ -1404,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/language/cic.rst b/doc/sphinx/language/cic.rst index 381f8bb661..835d6dcaa6 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 diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index c802f44ac1..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 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/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. |