From 7d3e6fefd7dab20c433fb7ae1baec5fa3ff2f0d7 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 27 Apr 2019 12:56:30 +0200 Subject: CoqIDE: updating documentation of the Preference windows. In particular, we explicitly mention the existence of an Emacs mode. --- doc/sphinx/practical-tools/coqide.rst | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index 97d86943fb..d3d75dddd8 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -181,7 +181,14 @@ presented as a notebook. The first section is for selecting the text font used for scripts, goal and message windows. -The second section is devoted to file management: you may configure +The second and third sections are for controlling colors and style. + +The fourth section is for customizing the editor. It includes in +particular the ability to activate an Emacs mode named +micro-Proof-General (use the Help menu to know more about the +available bindings). + +The next section is devoted to file management: you may configure automatic saving of files, by periodically saving the contents into files named `#f#` for each opened file `f`. You may also activate the *revert* feature: in case a opened file is modified on the disk by a -- cgit v1.2.3 From 5610158cf3e256888184d44ae7e09bf626fd6102 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 10 Apr 2019 01:31:21 -0300 Subject: Credits for 8.10 --- doc/sphinx/changes.rst | 447 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 447 insertions(+) (limited to 'doc/sphinx') diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 57b9e45342..10cbbcfcaa 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -2,6 +2,453 @@ Recent changes -------------- +Version 8.10 +------------ + +Summary of changes +~~~~~~~~~~~~~~~~~~ + +|Coq| version 8.10 contains two major new features: support for a native +fixed-precision integer type and a new sort `SProp` of strict +propositions. It is also the result of refinements and stabilization of +previous features, deprecations or removals of deprecated features, +cleanups of the internals of the system and API. This release includes +many user-visible changes, including deprecations that are documented in +the following section, and new features that are documented in the +reference manual. Here are the most important user-visible changes: + +- Kernel: + + - A notion of primitive object was added to the calculus. Its first + instance is primitive cyclic unsigned integers, axiomatized in + module UInt63(link), by Maxime Dénès, Benjamin Grégoire and Vincent + Laporte. See Section :ref:`primitive-integers`. + + - The :math:`\SProp` sort of definitionally proof-irrelevant propositions was + introduced by Gaëtan Gilbert. :math:`\SProp` allows to mark proof + terms as irrelevant for conversion, and is treated like `Prop` + during extraction. It is enabled using the `-allow-sprop` + command-line flag. See Section :ref:`sprop`. + + - The unfolding heuristic in termination checking was made more complete + by Enrico Tassi, allowing more constants to be unfolded to discover + valid recursive calls. + +- Universes: + + - Added :cmd:`Print Universes Subgraph` variant of :cmd:`Print Universes` and + private universes for opaque polymorphic constants, by Gaëtan Gilbert. + +- Notations: + + - New command :cmd:`String Notation` to register string syntax for custom + inductive types, by Jason Gross. + + - Numeral Notations now parse decimal constants, by Pierre Roux. + +- Ltac: + + - Ltac backtraces can be turned on using the :opt:`Ltac Backtrace` option, + by Pierre-Marie Pédrot. + + +- The tactics :tac:`lia`, :tac:`nia`, :tac:`lra`, :tac:`nra` are now using a novel + Simplex-based proof engine, by Fréderic Besson. + +- SSReflect has new intro patterns and a consistent clear discipline, by + Enrico Tassi. + +- :cmd:`Combined Scheme` now works when inductive schemes are generated in sort + `Type`, by Théo Winterhalter. + +- A new registration mechanism for reference from ML code to Coq + constructs has been added, by Emilio Jesús Gallego Arias. + +- CoqIDE: + + - Migrated to gtk+3 and lablgtk3 by Hugo Herbelin and Jacques Garrigue. + + - Supports smart input for Unicode characters by Arthur Charguéraud. + +- Infrastructure: + + - Coq 8.10 requires OCaml >= 4.05.0, bumped from 4.02.3 See the + `INSTALL` file for more information on dependencies. + + - Coq now supports building with Dune, in addition to the traditional + Makefile which is scheduled for deprecation, by Emilio Jesús Gallego + Arias and Rudi Grinberg. Experimental support for building Coq + projects has been integrated in Dune at the same time, providing an + [improved + experience](`https://coq.discourse.group/t/a-guide-to-building-your-coq-libraries-and-plugins-with-dune/` + for plugin developers. We thank the Dune team for their work + supporting Coq. + + +Version 8.10 also comes with a bunch of smaller-scale changes and +improvements regarding the different components of the system, including +many additions to the standard library (see the next subsection for details). + +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 originally made by Yves Bertot +is now in `doc/plugin_tutorial`. The ``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 and package building infrastructure. + +The OPAM repository for |Coq| packages has been maintained by Guillaume +Melquiond, Matthieu Sozeau, Enrico Tassi (who migrated it to opam 2) +with contributions from many users. A list of packages is available at +https://coq.inria.fr/opam/www/. + +The 61 contributors to this version are David A. Dalrymple, Tanaka +Akira, Benjamin Barenblat, Yves Bertot, Frédéric Besson, Lasse +Blaauwbroek, Martin Bodin, Joachim Breitner, Tej Chajed, Frédéric +Chapoton, Arthur Charguéraud, Cyril Cohen, Lukasz Czajka, Christian +Doczkal, Maxime Dénès, Andres Erbsen, Jim Fehrle, Gaëtan Gilbert, Matěj +Grabovský, Simon Gregersen, Jason Gross, Samuel Gruetter, Hugo Herbelin, +Jasper Hugunin, Mirai Ikebuchi, Emilio Jesus Gallego Arias, Chantal +Keller, Matej Košík, Vincent Laporte, Olivier Laurent, Larry Darryl Lee +Jr, Pierre Letouzey, Nick Lewycky, Yao Li, Yishuai Li, Xia Li-yao, Assia +Mahboubi, Simon Marechal, Erik Martin-Dorel, Thierry Martinez, Guillaume +Melquiond, Kayla Ngan, Sam Pablo Kuper, Karl Palmskog, Clément +Pit-Claudel, Pierre-Marie Pédrot, Pierre Roux, Kazuhiko Sakaguchi, Ryan +Scott, Vincent Semeria, Gan Shen, Michael Soegtrop, Matthieu Sozeau, +Enrico Tassi, Laurent Théry, Kamil Trzciński, whitequark, Théo +Winterhalter, Beta Ziliani and 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, +the coq-club@inria.fr mailing list or the new Discourse forum. It would +be impossible to mention exhaustively the names of everybody who to some +extent influenced the development. + +Version 8.10 is the fifth release of |Coq| developed on a time-based +development cycle. Its development spanned 6 months from the release of +|Coq| 8.9. Vincent Laport is the release manager and maintainer of this +release. This release is the result of ??? commits and ??? PRs +merged, closing ??? issues. + +| Santiago de Chile, April 2019, +| Matthieu Sozeau for the |Coq| development team +| + +Details of changes +~~~~~~~~~~~~~~~~~~ + +OCaml and dependencies + +- Coq 8.10 doesn't need Camlp5 to build anymore. It now includes a + fork of the core parsing library that Coq uses, which is a small + subset of the whole Camlp5 distribution. In particular, this subset + doesn't depend on the OCaml AST, allowing easier compilation and + testing on experimental OCaml versions. + + The Coq developers would like to thank Daniel de Rauglaudre for many + years of continued support. + +Coqide + +- CoqIDE now depends on gtk+3 and lablgtk3, rather than gtk+2 and lablgtk2. + +- CoqIDE now properly sets the module name for a given file based on + its path, see `-topfile` change entry for more details. + +Coqtop + +- the use of `coqtop` as a compiler has been deprecated, in favor of + `coqc`. Consequently option `-compile` will stop to be accepted in + the next release. `coqtop` is now reserved to interactive + use. (@ejgallego #9095) + +- new option -topfile filename, which will set the current module name + (à la -top) based on the filename passed, taking into account the + proper -R/-Q options. For example, given -R Foo foolib using + -topfile foolib/bar.v will set the module name to Foo.Bar. + +Specification language, type inference + +- Fixing a missing check in interpreting instances of existential + variables that are bound to local definitions might exceptionally + induce an overhead if the cost of checking the conversion of the + corresponding definitions is additionally high (PR #8215). + +- A few improvements in inference of the return clause of `match` can + exceptionally introduce incompatibilities (PR #262). This can be + solved by writing an explicit `return` clause, sometimes even simply + an explicit `return _` clause. + +- Using non-projection values with the projection syntax is not + allowed. For instance "0.(S)" is not a valid way to write "S 0". + Projections from non-primitive (emulated) records are allowed with + warning "nonprimitive-projection-syntax". + +Kernel + +- Added primitive integers + +- Unfolding heuristic in termination checking made more complete. + In particular Coq is now more aggressive in unfolding constants + when it looks for a iota redex. Performance regression may occur + in Fixpoint declarations without an explicit {struct} annotation, + since guessing the decreasing argument can now be more expensive. + (PR #9602) + +Notations + +- New command `Declare Scope` to explicitly declare a scope name + before any use of it. Implicit declaration of a scope at the time of + `Bind Scope`, `Delimit Scope`, `Undelimit Scope`, or `Notation` is + deprecated. + +- New command `String Notation` to register string syntax for custom + inductive types. + +- Numeral notations now parse decimal constants such as 1.02e+01 or + 10.2. Parsers added for Q and R. This should be considered as an + experimental feature currently. + Note: in -- the rare -- case when such numeral notations were used + in a development along with Q or R, they may have to be removed or + deconflicted through explicit scope annotations (1.23%Q, + 45.6%R,...). + +- Various bugs have been fixed (e.g. PR #9214 on removing spurious + parentheses on abbreviations shortening a strict prefix of an application). + +- Numeral Notations now support inductive types in the input to + printing functions (e.g., numeral notations can be defined for terms + containing things like `@cons nat O O`), and parsing functions now + fully normalize terms including parameters of constructors (so that, + e.g., a numeral notation whose parsing function outputs a proof of + `Nat.gcd x y = 1` will no longer fail to parse due to containing the + constant `Nat.gcd` in the parameter-argument of `eq_refl`). See + #9840 for more details. + +- Deprecated compatibility notations have actually been removed. Uses + of these notations are generally easy to fix thanks to the hint + contained in the deprecation warnings. For projects that require + more than a handful of such fixes, there is [a + script](https://gist.github.com/JasonGross/9770653967de3679d131c59d42de6d17#file-replace-notations-py) + that will do it automatically, using the output of coqc. The script + contains documentation on its usage in a comment at the top. + +Plugins + +- The quote plugin (https://coq.inria.fr/distrib/V8.8.1/refman/proof-engine/detailed-tactic-examples.html#quote) + was removed. If some users are interested in maintaining this plugin + externally, the Coq development team can provide assistance for extracting + the plugin and setting up a new repository. + +Tactics + +- Removed the deprecated `romega` tactics. +- Tactic names are no longer allowed to clash, even if they are not defined in + the same section. For example, the following is no longer accepted: + `Ltac foo := idtac. Section S. Ltac foo := fail. End S.` + +- The tactics 'lia','nia','lra','nra' are now using a novel + Simplex-based proof engine. In case of regression, 'Unset Simplex' + to get the venerable Fourier-based engine. + +- Names of existential variables occurring in Ltac functions + (e.g. `?[n]` or `?n` in terms - not in patterns) are now interpreted + the same way as other variable names occurring in Ltac functions. + +- Hint declaration and removal should now specify a database (e.g. `Hint Resolve + foo : database`). When the database name is omitted, the hint is added to the + core database (as previously), but a deprecation warning is emitted. + +- There are now tactics in `PreOmega.v` called + `Z.div_mod_to_equations`, `Z.quot_rem_to_equations`, and + `Z.to_euclidean_division_equations` (which combines the `div_mod` + and `quot_rem` variants) which allow `lia`, `nia`, `romega`, etc to + support `Z.div` and `Z.modulo` (`Z.quot` and `Z.rem`, respectively), + by posing the specifying equation for `Z.div` and `Z.modulo` before + replacing them with atoms. + +- Ltac backtraces can be turned on using the "Ltac Backtrace" option. + +- The syntax of the `autoapply` tactic was fixed to conform with preexisting + documentation: it now takes a `with` clause instead of a `using` clause. + + + +Vernacular commands + +- `Combined Scheme` can now work when inductive schemes are generated in sort + `Type`. It used to be limited to sort `Prop`. + +- Binders for an `Instance` now act more like binders for a `Theorem`. + Names may not be repeated, and may not overlap with section variable names. + +- Removed the deprecated `Implicit Tactic` family of commands. + +- The `Automatic Introduction` option has been removed and is now the + default. + +- `Arguments` now accepts names for arguments provided with `extra_scopes`. + +- The naming scheme for anonymous binders in a `Theorem` has changed to + avoid conflicts with explicitly named binders. + +- Computation of implicit arguments now properly handles local definitions in the + binders for an `Instance`, and can be mixed with implicit binders `{x : T}`. + +- `Declare Instance` now requires an instance name. + +- Option `Refine Instance Mode` has been turned off by default, meaning that + `Instance` no longer opens a proof when a body is provided. + +- `Instance`, when no body is provided, now always opens a proof. This is a + breaking change, as instance of `Instance foo : C.` where `C` is a trivial + class will have to be changed into `Instance foo : C := {}.` or + `Instance foo : C. Proof. Qed.`. + +- Option `Program Mode` now means that the `Program` attribute is enabled + for all commands that support it. In particular, it does not have any effect + on tactics anymore. May cause some incompatibilities. + +- The algorithm computing implicit arguments now behaves uniformly for primitive + projection and application nodes (bug #9508). + +- `Hypotheses` and `Variables` can now take implicit binders inside sections. + +- Removed deprecated option `Automatic Coercions Import`. + +- The `Show Script` command has been deprecated. + +- Option `Refine Instance Mode` has been deprecated and will be removed in + the next version. + +- `Coercion` does not warn ambiguous paths which are obviously convertible with + existing ones. + +- A new flag `Fast Name Printing` has been introduced. It changes the + algorithm used for allocating bound variable names for a faster but less + clever one. + +Tools + +- The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values: + - `no` disables native_compute + - `yes` enables native_compute and precompiles `.v` files to native code + - `ondemand` enables native_compute but compiles code only when `native_compute` is called + + The default value is `ondemand`. + + Note that this flag now has priority over the configure flag of the same name. + +- A new `-bytecode-compiler` flag for `coqc` and `coqtop` controls whether + conversion can use the VM. The default value is `yes`. + +- CoqIDE now supports input for Unicode characters. For example, typing + "\alpha" then the "Shift+Space" will insert the greek letter alpha. + In fact, typing the prefix string "\a" is sufficient. + A larger number of default bindings are provided, following the latex + naming convention. Bindings can be customized, either globally, or on a + per-project basis, with the requirement is that keys must begin with a + backslash and contain no space character. Bindings may be assigned custom + priorities, so that prefixes resolve to the most convenient bindings. + The documentation pages for CoqIDE provides further details. + +- The pretty timing diff scripts (flag `TIMING=1` to a + `coq_makefile`-made `Makefile`, also + `tools/make-both-single-timing-files.py`, + `tools/make-both-time-files.py`, and `tools/make-one-time-file.py`) + now correctly support non-UTF-8 characters in the output of + `coqc`/`make` as well as printing to stdout, on both python2 and + python3. + +Standard Library + +- Added lemmas about monotonicity of `N.double` and `N.succ_double`, and about + the upper bound of number represented by a vector. + Allowed implicit vector length argument in `Ndigits.Bv2N`. + +- Added `Bvector.BVeq` that decides whether two `Bvector`s are equal. + +- Added notations for `BVxor`, `BVand`, `BVor`, `BVeq` and `BVneg`. + +- Added `ByteVector` type that can convert to and from [string]. + +- The prelude used to be automatically Exported and is now only + Imported. This should be relevant only when importing files which + don't use -noinit into files which do. + +- Added `Coq.Structures.OrderedTypeEx.String_as_OT` to make strings an + ordered type (using lexical order). + +- The `Coq.Numbers.Cyclic.Int31` library is deprecated. + +- Added lemmas about `Z.testbit`, `Z.ones`, and `Z.modulo`. + +- Moved the `auto` hints of the `FSet` library into a new + `fset` database. + +Universes + +- Added `Print Universes Subgraph` variant of `Print Universes`. + Try for instance `Print Universes Subgraph(sigT2.u1 sigT_of_sigT2.u1 projT3_eq.u1 eq_sigT2_rect.u1).` + +- Added private universes for opaque polymorphic constants, see doc + for the "Private Polymorphic Universes" option (and Unset it to get + the previous behaviour). + +SProp + +- Added a universe "SProp" for definitionally proof irrelevant + propositions. Use with -allow-sprop. See manual for details. + +Inductives + +- An option and attributes to control the automatic decision to declare + an inductive type as template polymorphic were added. Warning + "auto-template" (off by default) can trigger when an inductive is + automatically declared template polymorphic without the attribute. + +Funind + +- Inductive types declared by Funind will never be template polymorphic. + +Misc + +- Option "Typeclasses Axioms Are Instances" is deprecated. Use Declare Instance for axioms which should be instances. + +- Removed option "Printing Primitive Projection Compatibility" + +SSReflect + +- New intro patterns: + - temporary introduction: `=> +` + - block introduction: `=> [^ prefix ] [^~ suffix ]` + - fast introduction: `=> >` + - tactics as views: `=> /ltac:mytac` + - replace hypothesis: `=> {}H` + See the reference manual for the actual documentation. + +- Clear discipline made consistent across the entire proof language. + Whenever a clear switch `{x..}` comes immediately before an existing proof + context entry (used as a view, as a rewrite rule or as name for a new + context entry) then such entry is cleared too. + + E.g. The following sentences are elaborated as follows (when H is an existing + proof context entry): + - `=> {x..} H` -> `=> {x..H} H` + - `=> {x..} /H` -> `=> /v {x..H}` + - `rewrite {x..} H` -> `rewrite E {x..H}` + +Diffs + +- Some error messages that show problems with a pair of non-matching values will now + highlight the differences. + Version 8.9 ----------- -- cgit v1.2.3 From fd864160d128836abf34f07eacc1e085e3f774b0 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 17 Apr 2019 08:03:26 -0400 Subject: Apply suggestions from code review Mainly markup fixes by Theo Co-Authored-By: mattam82 --- doc/sphinx/changes.rst | 36 ++++++++++++++++++------------------ 1 file changed, 18 insertions(+), 18 deletions(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 10cbbcfcaa..7f68d1a25d 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -132,7 +132,7 @@ extent influenced the development. Version 8.10 is the fifth release of |Coq| developed on a time-based development cycle. Its development spanned 6 months from the release of -|Coq| 8.9. Vincent Laport is the release manager and maintainer of this +|Coq| 8.9. Vincent Laporte is the release manager and maintainer of this release. This release is the result of ??? commits and ??? PRs merged, closing ??? issues. @@ -166,7 +166,7 @@ Coqtop - the use of `coqtop` as a compiler has been deprecated, in favor of `coqc`. Consequently option `-compile` will stop to be accepted in the next release. `coqtop` is now reserved to interactive - use. (@ejgallego #9095) + use. Change by Emilio Gallego Arías. - new option -topfile filename, which will set the current module name (à la -top) based on the filename passed, taking into account the @@ -186,7 +186,7 @@ Specification language, type inference an explicit `return _` clause. - Using non-projection values with the projection syntax is not - allowed. For instance "0.(S)" is not a valid way to write "S 0". + allowed. For instance :g:`0.(S)` is not a valid way to write :g:`S 0`. Projections from non-primitive (emulated) records are allowed with warning "nonprimitive-projection-syntax". @@ -203,9 +203,9 @@ Kernel Notations -- New command `Declare Scope` to explicitly declare a scope name +- New command :cmd:`Declare Scope` to explicitly declare a scope name before any use of it. Implicit declaration of a scope at the time of - `Bind Scope`, `Delimit Scope`, `Undelimit Scope`, or `Notation` is + :cmd:`Bind Scope`, :cmd:`Delimit Scope`, :cmd:`Undelimit Scope`, or :cmd:`Notation` is deprecated. - New command `String Notation` to register string syntax for custom @@ -233,7 +233,7 @@ Notations - Deprecated compatibility notations have actually been removed. Uses of these notations are generally easy to fix thanks to the hint - contained in the deprecation warnings. For projects that require + contained in the deprecation warning emitted by the previous version of Coq. For projects that require more than a handful of such fixes, there is [a script](https://gist.github.com/JasonGross/9770653967de3679d131c59d42de6d17#file-replace-notations-py) that will do it automatically, using the output of coqc. The script @@ -263,7 +263,7 @@ Tactics - Hint declaration and removal should now specify a database (e.g. `Hint Resolve foo : database`). When the database name is omitted, the hint is added to the - core database (as previously), but a deprecation warning is emitted. + `core` database (as previously), but a deprecation warning is emitted. - There are now tactics in `PreOmega.v` called `Z.div_mod_to_equations`, `Z.quot_rem_to_equations`, and @@ -275,7 +275,7 @@ Tactics - Ltac backtraces can be turned on using the "Ltac Backtrace" option. -- The syntax of the `autoapply` tactic was fixed to conform with preexisting +- The syntax of the :tacn:`autoapply` tactic was fixed to conform with preexisting documentation: it now takes a `with` clause instead of a `using` clause. @@ -285,7 +285,7 @@ Vernacular commands - `Combined Scheme` can now work when inductive schemes are generated in sort `Type`. It used to be limited to sort `Prop`. -- Binders for an `Instance` now act more like binders for a `Theorem`. +- Binders for an :cmd:`Instance` now act more like binders for a :cmd:`Theorem`. Names may not be repeated, and may not overlap with section variable names. - Removed the deprecated `Implicit Tactic` family of commands. @@ -301,9 +301,9 @@ Vernacular commands - Computation of implicit arguments now properly handles local definitions in the binders for an `Instance`, and can be mixed with implicit binders `{x : T}`. -- `Declare Instance` now requires an instance name. +- :cmd:`Declare Instance` now requires an instance name. -- Option `Refine Instance Mode` has been turned off by default, meaning that +- Option :opt:`Refine Instance Mode` has been turned off by default, meaning that `Instance` no longer opens a proof when a body is provided. - `Instance`, when no body is provided, now always opens a proof. This is a @@ -311,7 +311,7 @@ Vernacular commands class will have to be changed into `Instance foo : C := {}.` or `Instance foo : C. Proof. Qed.`. -- Option `Program Mode` now means that the `Program` attribute is enabled +- Option :opt:`Program Mode` now means that the `Program` attribute is enabled for all commands that support it. In particular, it does not have any effect on tactics anymore. May cause some incompatibilities. @@ -327,10 +327,10 @@ Vernacular commands - Option `Refine Instance Mode` has been deprecated and will be removed in the next version. -- `Coercion` does not warn ambiguous paths which are obviously convertible with +- :cmd:`Coercion` does not warn ambiguous paths which are obviously convertible with existing ones. -- A new flag `Fast Name Printing` has been introduced. It changes the +- A new flag :opt:`Fast Name Printing` has been introduced. It changes the algorithm used for allocating bound variable names for a faster but less clever one. @@ -380,7 +380,7 @@ Standard Library - The prelude used to be automatically Exported and is now only Imported. This should be relevant only when importing files which - don't use -noinit into files which do. + don't use `-noinit` into files which do. - Added `Coq.Structures.OrderedTypeEx.String_as_OT` to make strings an ordered type (using lexical order). @@ -398,7 +398,7 @@ Universes Try for instance `Print Universes Subgraph(sigT2.u1 sigT_of_sigT2.u1 projT3_eq.u1 eq_sigT2_rect.u1).` - Added private universes for opaque polymorphic constants, see doc - for the "Private Polymorphic Universes" option (and Unset it to get + for the :opt"`Private Polymorphic Universes` option (and Unset it to get the previous behaviour). SProp @@ -419,9 +419,9 @@ Funind Misc -- Option "Typeclasses Axioms Are Instances" is deprecated. Use Declare Instance for axioms which should be instances. +- Option :opt`Typeclasses Axioms Are Instances` (compatibility option introduced in the previous version) is deprecated. Use :cmd:`Declare Instance` for axioms which should be instances. -- Removed option "Printing Primitive Projection Compatibility" +- Removed option `Printing Primitive Projection Compatibility` SSReflect -- cgit v1.2.3 From 61c780ad8138bfa768977d652c25741dad35d448 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 18 Apr 2019 14:26:39 +0200 Subject: First fixing pass, and experiment with dune-style PR number and author listing. --- doc/sphinx/addendum/sprop.rst | 8 +-- doc/sphinx/changes.rst | 111 +++++++++++++++++------------ doc/sphinx/language/gallina-extensions.rst | 1 + 3 files changed, 72 insertions(+), 48 deletions(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst index c0c8c2d79c..8935ba27e3 100644 --- a/doc/sphinx/addendum/sprop.rst +++ b/doc/sphinx/addendum/sprop.rst @@ -10,9 +10,9 @@ SProp (proof irrelevant propositions) This section describes the extension of |Coq| with definitionally proof irrelevant propositions (types in the sort :math:`\SProp`, also known as strict propositions). To use :math:`\SProp` you must pass -``-allow-sprop`` to the |Coq| program or use :opt:`Allow StrictProp`. +``-allow-sprop`` to the |Coq| program or use :flag:`Allow StrictProp`. -.. opt:: Allow StrictProp +.. flag:: Allow StrictProp :name: Allow StrictProp Allows using :math:`\SProp` when set and forbids it when unset. The @@ -201,10 +201,10 @@ This means that some errors will be delayed until ``Qed``: Abort. -.. opt:: Elaboration StrictProp Cumulativity +.. flag:: Elaboration StrictProp Cumulativity :name: Elaboration StrictProp Cumulativity - Unset this option (it's on by default) to be strict with regard to + Unset this flag (it is on by default) to be strict with regard to :math:`\SProp` cumulativity during elaboration. The implementation of proof irrelevance uses inferred "relevance" diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 7f68d1a25d..4797363063 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -9,82 +9,104 @@ Summary of changes ~~~~~~~~~~~~~~~~~~ |Coq| version 8.10 contains two major new features: support for a native -fixed-precision integer type and a new sort `SProp` of strict +fixed-precision integer type and a new sort :math:`\SProp` of strict propositions. It is also the result of refinements and stabilization of previous features, deprecations or removals of deprecated features, cleanups of the internals of the system and API. This release includes many user-visible changes, including deprecations that are documented in -the following section, and new features that are documented in the +the next section, and new features that are documented in the reference manual. Here are the most important user-visible changes: - Kernel: - A notion of primitive object was added to the calculus. Its first instance is primitive cyclic unsigned integers, axiomatized in - module UInt63(link), by Maxime Dénès, Benjamin Grégoire and Vincent - Laporte. See Section :ref:`primitive-integers`. + module :g:`UInt63`. See Section :ref:`primitive-integers` + (`#6914 `_, by Maxime Dénès, + Benjamin Grégoire and Vincent Laporte). - The :math:`\SProp` sort of definitionally proof-irrelevant propositions was - introduced by Gaëtan Gilbert. :math:`\SProp` allows to mark proof - terms as irrelevant for conversion, and is treated like `Prop` + introduced. :math:`\SProp` allows to mark proof + terms as irrelevant for conversion, and is treated like :math:`\Prop` during extraction. It is enabled using the `-allow-sprop` - command-line flag. See Section :ref:`sprop`. + command-line flag or the :flag:`Allow StrictProp` flag. + See Chapter :ref:`sprop` + (`#8817 `_, by Gaëtan Gilbert). - - The unfolding heuristic in termination checking was made more complete - by Enrico Tassi, allowing more constants to be unfolded to discover - valid recursive calls. + - The unfolding heuristic in termination checking was made more + complete, allowing more constants to be unfolded to discover valid + recursive calls + (`#9602 `_, by Enrico Tassi). - Universes: - Added :cmd:`Print Universes Subgraph` variant of :cmd:`Print Universes` and - private universes for opaque polymorphic constants, by Gaëtan Gilbert. + private universes for opaque polymorphic constants + (`#8451 `_, by Gaëtan Gilbert). - Notations: - New command :cmd:`String Notation` to register string syntax for custom - inductive types, by Jason Gross. + inductive types + (`#8965 `_, by Jason Gross). - - Numeral Notations now parse decimal constants, by Pierre Roux. + - Numeral Notations now parse decimal constants + (`#8764 `_, by Pierre Roux). - Ltac: - - Ltac backtraces can be turned on using the :opt:`Ltac Backtrace` option, - by Pierre-Marie Pédrot. + - Ltac backtraces can be turned on using the :flag:`Ltac Backtrace` + flag, which is off by default + (`#9142 `_, + fixes `#7769 `_ + and `#7385 `_, + by Pierre-Marie Pédrot). +- The tactics :tacn:`lia`, :tacn:`nia`, :tacn:`lra`, :tacn:`nra` are now using a novel + Simplex-based proof engine + (`#8457 `_, by Fréderic Besson). -- The tactics :tac:`lia`, :tac:`nia`, :tac:`lra`, :tac:`nra` are now using a novel - Simplex-based proof engine, by Fréderic Besson. - -- SSReflect has new intro patterns and a consistent clear discipline, by - Enrico Tassi. +- SSReflect has new intro patterns and a consistent clear discipline + (`#6705 `_ + and `#9341 `_, + by Enrico Tassi). - :cmd:`Combined Scheme` now works when inductive schemes are generated in sort - `Type`, by Théo Winterhalter. + :math:`\Type` + (`#7634 `_, by Théo Winterhalter). - A new registration mechanism for reference from ML code to Coq - constructs has been added, by Emilio Jesús Gallego Arias. + constructs has been added + (`#186 `_, + by Emilio Jesús Gallego Arias, Maxime Dénès and Vincent Laporte). - CoqIDE: - - Migrated to gtk+3 and lablgtk3 by Hugo Herbelin and Jacques Garrigue. + - Migrated to gtk+3 and lablgtk3 + (`#9279 `_, + by Hugo Herbelin, with help of Jacques Garrigue, + Emilio Jesús Gallego Arias, Michael Sogetrop and Vincent Laporte). - - Supports smart input for Unicode characters by Arthur Charguéraud. + - Supports smart input for Unicode characters + (`#8560 `_, by Arthur Charguéraud). - Infrastructure: - Coq 8.10 requires OCaml >= 4.05.0, bumped from 4.02.3 See the - `INSTALL` file for more information on dependencies. + `INSTALL` file for more information on dependencies + (`#7522 `_, by Emilio Jesús Gallego Arías). - Coq now supports building with Dune, in addition to the traditional - Makefile which is scheduled for deprecation, by Emilio Jesús Gallego - Arias and Rudi Grinberg. Experimental support for building Coq - projects has been integrated in Dune at the same time, providing an - [improved - experience](`https://coq.discourse.group/t/a-guide-to-building-your-coq-libraries-and-plugins-with-dune/` + Makefile which is scheduled for deprecation + (`#6857 `_, + by Emilio Jesús Gallego Arias and Rudi Grinberg). + + Experimental support for building Coq projects has been integrated + in Dune at the same time, providing an `improved experience + `_ for plugin developers. We thank the Dune team for their work supporting Coq. - Version 8.10 also comes with a bunch of smaller-scale changes and improvements regarding the different components of the system, including many additions to the standard library (see the next subsection for details). @@ -140,8 +162,8 @@ merged, closing ??? issues. | Matthieu Sozeau for the |Coq| development team | -Details of changes -~~~~~~~~~~~~~~~~~~ +Details of changes in 8.10+beta1 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ OCaml and dependencies @@ -303,15 +325,16 @@ Vernacular commands - :cmd:`Declare Instance` now requires an instance name. -- Option :opt:`Refine Instance Mode` has been turned off by default, meaning that - `Instance` no longer opens a proof when a body is provided. +- The flag :flag:`Refine Instance Mode` has been turned off by default, meaning that + :cmd:`Instance` no longer opens a proof when a body is provided. -- `Instance`, when no body is provided, now always opens a proof. This is a - breaking change, as instance of `Instance foo : C.` where `C` is a trivial - class will have to be changed into `Instance foo : C := {}.` or - `Instance foo : C. Proof. Qed.`. +- Command :cmd:`Instance`, when no body is provided, now always opens + a proof. This is a breaking change, as instance of :n:`Instance + @ident__1 : @ident__2.` where :n:`@ident__2` is a trivial class will + have to be changed into :n:`Instance @ident__1 : @ident__2 := {}.` + or :n:`Instance @ident__1 : @ident__2. Proof. Qed.`. -- Option :opt:`Program Mode` now means that the `Program` attribute is enabled +- The flag :flag:`Program Mode` now means that the `Program` attribute is enabled for all commands that support it. In particular, it does not have any effect on tactics anymore. May cause some incompatibilities. @@ -330,7 +353,7 @@ Vernacular commands - :cmd:`Coercion` does not warn ambiguous paths which are obviously convertible with existing ones. -- A new flag :opt:`Fast Name Printing` has been introduced. It changes the +- A new flag :flag:`Fast Name Printing` has been introduced. It changes the algorithm used for allocating bound variable names for a faster but less clever one. @@ -372,7 +395,7 @@ Standard Library the upper bound of number represented by a vector. Allowed implicit vector length argument in `Ndigits.Bv2N`. -- Added `Bvector.BVeq` that decides whether two `Bvector`s are equal. +- Added `Bvector.BVeq` that decides whether two `Bvector`\s are equal. - Added notations for `BVxor`, `BVand`, `BVor`, `BVeq` and `BVneg`. @@ -599,8 +622,8 @@ engineer working with Maxime Dénès in the |Coq| consortium. | Matthieu Sozeau for the |Coq| development team | -Details of changes -~~~~~~~~~~~~~~~~~~ +Details of changes in 8.9+beta1 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Kernel diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 695dea222f..5308330820 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -2244,6 +2244,7 @@ Printing universes unspecified if `string` doesn’t end in ``.dot`` or ``.gv``. .. cmdv:: Print Universes Subgraph(@names) + :name: Print Universes Subgraph Prints the graph restricted to the requested names (adjusting constraints to preserve the implied transitive constraints between -- cgit v1.2.3 From bb4b9469ddf45d76385cdcddf27dc82266a8c73b Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 18 Apr 2019 15:10:06 +0200 Subject: Remove 8.10 entries from CHANGES file. --- doc/sphinx/changes.rst | 3 +++ 1 file changed, 3 insertions(+) (limited to 'doc/sphinx') diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 4797363063..645be500fd 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -195,6 +195,9 @@ Coqtop proper -R/-Q options. For example, given -R Foo foolib using -topfile foolib/bar.v will set the module name to Foo.Bar. +- Experimental: Coq flags and options can now be set on the + command-line, e.g. `-set "Universe Polymorphism=true"`. + Specification language, type inference - Fixing a missing check in interpreting instances of existential -- cgit v1.2.3 From 890f206ebea4a14f5be8b273cee4ae8f99ca25e1 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Fri, 19 Apr 2019 18:52:26 +0200 Subject: Split changes between main changes and other changes (no repetition). Add more links to PRs and credits of authors. --- doc/sphinx/changes.rst | 568 +++++++++++------------ doc/sphinx/practical-tools/coqide.rst | 2 + doc/sphinx/user-extensions/syntax-extensions.rst | 2 + 3 files changed, 282 insertions(+), 290 deletions(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 645be500fd..d8ea9c1552 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -12,9 +12,9 @@ Summary of changes fixed-precision integer type and a new sort :math:`\SProp` of strict propositions. It is also the result of refinements and stabilization of previous features, deprecations or removals of deprecated features, -cleanups of the internals of the system and API. This release includes -many user-visible changes, including deprecations that are documented in -the next section, and new features that are documented in the +cleanups of the internals of the system and API, and many documentation improvements. +This release includes many user-visible changes, including deprecations that are +documented in the next subsection, and new features that are documented in the reference manual. Here are the most important user-visible changes: - Kernel: @@ -35,44 +35,63 @@ reference manual. Here are the most important user-visible changes: - The unfolding heuristic in termination checking was made more complete, allowing more constants to be unfolded to discover valid - recursive calls + recursive calls. Performance regression may occur in Fixpoint + declarations without an explicit ``{struct}`` annotation, since + guessing the decreasing argument can now be more expensive (`#9602 `_, by Enrico Tassi). - Universes: - - Added :cmd:`Print Universes Subgraph` variant of :cmd:`Print Universes` and - private universes for opaque polymorphic constants + - Added :cmd:`Print Universes Subgraph` variant of :cmd:`Print Universes`. + Try for instance + :g:`Print Universes Subgraph(sigT2.u1 sigT_of_sigT2.u1 projT3_eq.u1).` (`#8451 `_, by Gaëtan Gilbert). + - Added private universes for opaque polymorphic constants, see the + documentation for the :flag:`Private Polymorphic Universes` flag, + and unset it to get the previous behaviour + (`#8850 `_, by Gaëtan Gilbert). + - Notations: - New command :cmd:`String Notation` to register string syntax for custom inductive types (`#8965 `_, by Jason Gross). - - Numeral Notations now parse decimal constants + - Experimental: :ref:`Numeral Notations ` now parse decimal + constants such as ``1.02e+01`` or ``10.2``. Parsers added for :g:`Q` and :g:`R`. + In the rare case when such numeral notations were used + in a development along with :g:`Q` or :g:`R`, they may have to be removed or + disambiguated through explicit scope annotations (`#8764 `_, by Pierre Roux). -- Ltac: - - - Ltac backtraces can be turned on using the :flag:`Ltac Backtrace` - flag, which is off by default - (`#9142 `_, - fixes `#7769 `_ - and `#7385 `_, - by Pierre-Marie Pédrot). +- Ltac backtraces can be turned on using the :flag:`Ltac Backtrace` + flag, which is off by default + (`#9142 `_, + fixes `#7769 `_ + and `#7385 `_, + by Pierre-Marie Pédrot). - The tactics :tacn:`lia`, :tacn:`nia`, :tacn:`lra`, :tacn:`nra` are now using a novel - Simplex-based proof engine + Simplex-based proof engine. In case of regression, unset :flag:`Simplex` + to get the venerable Fourier-based engine (`#8457 `_, by Fréderic Besson). -- SSReflect has new intro patterns and a consistent clear discipline - (`#6705 `_ - and `#9341 `_, - by Enrico Tassi). +- New SSReflect intro patterns: + + - temporary introduction: `=> +` + - block introduction: `=> [^ prefix ] [^~ suffix ]` + - fast introduction: `=> >` + - tactics as views: `=> /ltac:mytac` + - replace hypothesis: `=> {}H` + + See Section :ref:`introduction_ssr` + (`#6705 `_, by Enrico Tassi, + with help from Maxime Dénès, + ideas coming from various users). - :cmd:`Combined Scheme` now works when inductive schemes are generated in sort - :math:`\Type` + :math:`\Type`. It used to be limited to sort `Prop` (`#7634 `_, by Théo Winterhalter). - A new registration mechanism for reference from ML code to Coq @@ -82,24 +101,44 @@ reference manual. Here are the most important user-visible changes: - CoqIDE: - - Migrated to gtk+3 and lablgtk3 + - CoqIDE now depends on gtk+3 and lablgtk3 instead of gtk+2 and lablgtk2 (`#9279 `_, - by Hugo Herbelin, with help of Jacques Garrigue, + by Hugo Herbelin, with help from Jacques Garrigue, Emilio Jesús Gallego Arias, Michael Sogetrop and Vincent Laporte). - - Supports smart input for Unicode characters + - Smart input for Unicode characters. For example, typing + ``\alpha`` then ``Shift+Space`` will insert the greek letter alpha. + A larger number of default bindings are provided, following the latex + naming convention. Bindings can be customized, either globally, or on a + per-project basis. See Section :ref:`coqide-unicode` for details (`#8560 `_, by Arthur Charguéraud). -- Infrastructure: +- Infrastructure and dependencies: - Coq 8.10 requires OCaml >= 4.05.0, bumped from 4.02.3 See the `INSTALL` file for more information on dependencies (`#7522 `_, by Emilio Jesús Gallego Arías). + - Coq 8.10 doesn't need Camlp5 to build anymore. It now includes a + fork of the core parsing library that Coq uses, which is a small + subset of the whole Camlp5 distribution. In particular, this subset + doesn't depend on the OCaml AST, allowing easier compilation and + testing on experimental OCaml versions. Coq also ships a new parser + `coqpp` that plugin authors must switch to + (`#7902 `_, + `#7979 `_, + `#8161 `_, + `#8667 `_, + and `#8945 `_, + by Pierre-Marie Pédrot and Emilio Jesús Gallego Arias). + + The Coq developers would like to thank Daniel de Rauglaudre for many + years of continued support. + - Coq now supports building with Dune, in addition to the traditional Makefile which is scheduled for deprecation (`#6857 `_, - by Emilio Jesús Gallego Arias and Rudi Grinberg). + by Emilio Jesús Gallego Arias, with help from Rudi Grinberg). Experimental support for building Coq projects has been integrated in Dune at the same time, providing an `improved experience @@ -162,318 +201,267 @@ merged, closing ??? issues. | Matthieu Sozeau for the |Coq| development team | -Details of changes in 8.10+beta1 -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -OCaml and dependencies - -- Coq 8.10 doesn't need Camlp5 to build anymore. It now includes a - fork of the core parsing library that Coq uses, which is a small - subset of the whole Camlp5 distribution. In particular, this subset - doesn't depend on the OCaml AST, allowing easier compilation and - testing on experimental OCaml versions. - - The Coq developers would like to thank Daniel de Rauglaudre for many - years of continued support. - -Coqide - -- CoqIDE now depends on gtk+3 and lablgtk3, rather than gtk+2 and lablgtk2. - -- CoqIDE now properly sets the module name for a given file based on - its path, see `-topfile` change entry for more details. - -Coqtop - -- the use of `coqtop` as a compiler has been deprecated, in favor of - `coqc`. Consequently option `-compile` will stop to be accepted in - the next release. `coqtop` is now reserved to interactive - use. Change by Emilio Gallego Arías. - -- new option -topfile filename, which will set the current module name - (à la -top) based on the filename passed, taking into account the - proper -R/-Q options. For example, given -R Foo foolib using - -topfile foolib/bar.v will set the module name to Foo.Bar. - -- Experimental: Coq flags and options can now be set on the - command-line, e.g. `-set "Universe Polymorphism=true"`. - -Specification language, type inference - -- Fixing a missing check in interpreting instances of existential - variables that are bound to local definitions might exceptionally - induce an overhead if the cost of checking the conversion of the - corresponding definitions is additionally high (PR #8215). - -- A few improvements in inference of the return clause of `match` can - exceptionally introduce incompatibilities (PR #262). This can be - solved by writing an explicit `return` clause, sometimes even simply - an explicit `return _` clause. - -- Using non-projection values with the projection syntax is not - allowed. For instance :g:`0.(S)` is not a valid way to write :g:`S 0`. - Projections from non-primitive (emulated) records are allowed with - warning "nonprimitive-projection-syntax". - -Kernel - -- Added primitive integers +Other changes in 8.10+beta1 +~~~~~~~~~~~~~~~~~~~~~~~~~~~ -- Unfolding heuristic in termination checking made more complete. - In particular Coq is now more aggressive in unfolding constants - when it looks for a iota redex. Performance regression may occur - in Fixpoint declarations without an explicit {struct} annotation, - since guessing the decreasing argument can now be more expensive. - (PR #9602) +- Command-line tools and options: + + - The use of `coqtop` as a compiler has been deprecated, in favor of + `coqc`. Consequently option `-compile` will stop to be accepted in + the next release. `coqtop` is now reserved to interactive + use + (`#9095 `_, + by Emilio Jesús Gallego Arias). + + - New option ``-topfile filename``, which will set the current module name + (*à la* ``-top``) based on the filename passed, taking into account the + proper ``-R``/``-Q`` options. For example, given ``-R Foo foolib`` using + ``-topfile foolib/bar.v`` will set the module name to ``Foo.Bar``. + CoqIDE now properly sets the module name for a given file based on + its path + (`#8991 `_, + closes `#8989 `_, + by Gaëtan Gilbert). + + - Experimental: Coq flags and options can now be set on the + command-line, e.g. ``-set "Universe Polymorphism=true"`` + (`#9876 `_, by Gaëtan Gilbert). + + - The `-native-compiler` flag of `coqc` and `coqtop` now takes an + argument which can have three values: + + - `no` disables native_compute + - `yes` enables native_compute and precompiles `.v` files to + native code + - `ondemand` enables native_compute but compiles code only when + `native_compute` is called + + The default value is `ondemand`. Note that this flag now has + priority over the configure flag of the same name. + + A new `-bytecode-compiler` flag for `coqc` and `coqtop` controls + whether conversion can use the VM. The default value is `yes`. + + (`#8870 `_, by Maxime Dénès) + + - The pretty timing diff scripts (flag `TIMING=1` to a + `coq_makefile`\-made `Makefile`, also + `tools/make-both-single-timing-files.py`, + `tools/make-both-time-files.py`, and `tools/make-one-time-file.py`) + now correctly support non-UTF-8 characters in the output of + `coqc` / `make` as well as printing to stdout, on both python2 and + python3 + (`#9872 `_, + closes `#9767 `_ + and `#9705 `_, + by Jason Gross) + +- Specification language, type inference: + + - Fixing a missing check in interpreting instances of existential + variables that are bound to local definitions. Might exceptionally + induce an overhead if the cost of checking the conversion of the + corresponding definitions is additionally high + (`#8217 `_, + closes `#8215 `_, + by Hugo Herbelin). + + - A few improvements in inference of the return clause of `match` that + can exceptionally introduce incompatibilities. This can be + solved by writing an explicit `return` clause, sometimes even simply + an explicit `return _` clause + (`#262 `_, by Hugo Herbelin). + + - Using non-projection values with the projection syntax is not + allowed. For instance :g:`0.(S)` is not a valid way to write :g:`S 0`. + Projections from non-primitive (emulated) records are allowed with + warning "nonprimitive-projection-syntax" + (`#8829 `_, by Gaëtan Gilbert). + + - An option and attributes to control the automatic decision to declare + an inductive type as template polymorphic were added. Warning + "auto-template" (off by default) can trigger when an inductive is + automatically declared template polymorphic without the attribute. + + Inductive types declared by Funind will never be template polymorphic. + + (`#8488 `_, by Gaëtan Gilbert) -Notations - -- New command :cmd:`Declare Scope` to explicitly declare a scope name - before any use of it. Implicit declaration of a scope at the time of - :cmd:`Bind Scope`, :cmd:`Delimit Scope`, :cmd:`Undelimit Scope`, or :cmd:`Notation` is - deprecated. - -- New command `String Notation` to register string syntax for custom - inductive types. - -- Numeral notations now parse decimal constants such as 1.02e+01 or - 10.2. Parsers added for Q and R. This should be considered as an - experimental feature currently. - Note: in -- the rare -- case when such numeral notations were used - in a development along with Q or R, they may have to be removed or - deconflicted through explicit scope annotations (1.23%Q, - 45.6%R,...). - -- Various bugs have been fixed (e.g. PR #9214 on removing spurious - parentheses on abbreviations shortening a strict prefix of an application). - -- Numeral Notations now support inductive types in the input to - printing functions (e.g., numeral notations can be defined for terms - containing things like `@cons nat O O`), and parsing functions now - fully normalize terms including parameters of constructors (so that, - e.g., a numeral notation whose parsing function outputs a proof of - `Nat.gcd x y = 1` will no longer fail to parse due to containing the - constant `Nat.gcd` in the parameter-argument of `eq_refl`). See - #9840 for more details. - -- Deprecated compatibility notations have actually been removed. Uses - of these notations are generally easy to fix thanks to the hint - contained in the deprecation warning emitted by the previous version of Coq. For projects that require - more than a handful of such fixes, there is [a - script](https://gist.github.com/JasonGross/9770653967de3679d131c59d42de6d17#file-replace-notations-py) - that will do it automatically, using the output of coqc. The script - contains documentation on its usage in a comment at the top. - -Plugins +- Notations: -- The quote plugin (https://coq.inria.fr/distrib/V8.8.1/refman/proof-engine/detailed-tactic-examples.html#quote) + - New command :cmd:`Declare Scope` to explicitly declare a scope name + before any use of it. Implicit declaration of a scope at the time of + :cmd:`Bind Scope`, :cmd:`Delimit Scope`, :cmd:`Undelimit Scope`, + or :cmd:`Notation` is deprecated + (`#7135 `_, by Hugo Herbelin). + + - Various bugs have been fixed (e.g. `#9214 + `_ on removing spurious + parentheses on abbreviations shortening a strict prefix of an + application, by Hugo Herbelin). + + - :cmd:`Numeral Notation` now support inductive types in the input to + printing functions (e.g., numeral notations can be defined for terms + containing things like :g:`@cons nat O O`), and parsing functions now + fully normalize terms including parameters of constructors (so that, + e.g., a numeral notation whose parsing function outputs a proof of + :g:`Nat.gcd x y = 1` will no longer fail to parse due to containing the + constant :g:`Nat.gcd` in the parameter-argument of :g:`eq_refl`) + (`#9874 `_, + closes `#9840 `_ + and `#9844 `_, + by Jason Gross). + + - Deprecated compatibility notations have actually been + removed. Uses of these notations are generally easy to fix thanks + to the hint contained in the deprecation warning emitted by Coq + 8.8 and 8.9. For projects that require more than a handful of + such fixes, there is `a script + `_ + that will do it automatically, using the output of ``coqc`` + (`#8638 `_, by Jason Gross). + +- The `quote plugin + `_ was removed. If some users are interested in maintaining this plugin - externally, the Coq development team can provide assistance for extracting - the plugin and setting up a new repository. - -Tactics - -- Removed the deprecated `romega` tactics. -- Tactic names are no longer allowed to clash, even if they are not defined in - the same section. For example, the following is no longer accepted: - `Ltac foo := idtac. Section S. Ltac foo := fail. End S.` - -- The tactics 'lia','nia','lra','nra' are now using a novel - Simplex-based proof engine. In case of regression, 'Unset Simplex' - to get the venerable Fourier-based engine. - -- Names of existential variables occurring in Ltac functions - (e.g. `?[n]` or `?n` in terms - not in patterns) are now interpreted - the same way as other variable names occurring in Ltac functions. - -- Hint declaration and removal should now specify a database (e.g. `Hint Resolve - foo : database`). When the database name is omitted, the hint is added to the - `core` database (as previously), but a deprecation warning is emitted. - -- There are now tactics in `PreOmega.v` called - `Z.div_mod_to_equations`, `Z.quot_rem_to_equations`, and - `Z.to_euclidean_division_equations` (which combines the `div_mod` - and `quot_rem` variants) which allow `lia`, `nia`, `romega`, etc to - support `Z.div` and `Z.modulo` (`Z.quot` and `Z.rem`, respectively), - by posing the specifying equation for `Z.div` and `Z.modulo` before - replacing them with atoms. - -- Ltac backtraces can be turned on using the "Ltac Backtrace" option. + externally, the Coq development team can provide assistance for + extracting the plugin and setting up a new repository + (`#7894 `_, by Maxime Dénès). -- The syntax of the :tacn:`autoapply` tactic was fixed to conform with preexisting - documentation: it now takes a `with` clause instead of a `using` clause. - - - -Vernacular commands - -- `Combined Scheme` can now work when inductive schemes are generated in sort - `Type`. It used to be limited to sort `Prop`. - -- Binders for an :cmd:`Instance` now act more like binders for a :cmd:`Theorem`. - Names may not be repeated, and may not overlap with section variable names. - -- Removed the deprecated `Implicit Tactic` family of commands. - -- The `Automatic Introduction` option has been removed and is now the - default. - -- `Arguments` now accepts names for arguments provided with `extra_scopes`. - -- The naming scheme for anonymous binders in a `Theorem` has changed to - avoid conflicts with explicitly named binders. - -- Computation of implicit arguments now properly handles local definitions in the - binders for an `Instance`, and can be mixed with implicit binders `{x : T}`. +- Ltac: -- :cmd:`Declare Instance` now requires an instance name. + - Tactic names are no longer allowed to clash, even if they are not defined in + the same section. For example, the following is no longer accepted: + :g:`Ltac foo := idtac. Section S. Ltac foo := fail. End S.` -- The flag :flag:`Refine Instance Mode` has been turned off by default, meaning that - :cmd:`Instance` no longer opens a proof when a body is provided. + - Names of existential variables occurring in Ltac functions + (e.g. :g:`?[n]` or :g:`?n` in terms - not in patterns) are now interpreted + the same way as other variable names occurring in Ltac functions + (`#7309 `_, by Hugo Herbelin). -- Command :cmd:`Instance`, when no body is provided, now always opens - a proof. This is a breaking change, as instance of :n:`Instance - @ident__1 : @ident__2.` where :n:`@ident__2` is a trivial class will - have to be changed into :n:`Instance @ident__1 : @ident__2 := {}.` - or :n:`Instance @ident__1 : @ident__2. Proof. Qed.`. +- Tactics: -- The flag :flag:`Program Mode` now means that the `Program` attribute is enabled - for all commands that support it. In particular, it does not have any effect - on tactics anymore. May cause some incompatibilities. + - Removed the deprecated `romega` tactic + (`#8419 `_, + by Maxime Dénès and Vincent Laporte). -- The algorithm computing implicit arguments now behaves uniformly for primitive - projection and application nodes (bug #9508). + - Hint declaration and removal should now specify a database (e.g. `Hint Resolve + foo : database`). When the database name is omitted, the hint is added to the + `core` database (as previously), but a deprecation warning is emitted. -- `Hypotheses` and `Variables` can now take implicit binders inside sections. + - There are now tactics in `PreOmega.v` called + `Z.div_mod_to_equations`, `Z.quot_rem_to_equations`, and + `Z.to_euclidean_division_equations` (which combines the `div_mod` + and `quot_rem` variants) which allow `lia`, `nia`, `romega`, etc to + support `Z.div` and `Z.modulo` (`Z.quot` and `Z.rem`, respectively), + by posing the specifying equation for `Z.div` and `Z.modulo` before + replacing them with atoms. -- Removed deprecated option `Automatic Coercions Import`. + - The syntax of the :tacn:`autoapply` tactic was fixed to conform with preexisting + documentation: it now takes a `with` clause instead of a `using` clause. -- The `Show Script` command has been deprecated. + - SSReflect clear discipline made consistent across the entire proof language. + Whenever a clear switch `{x..}` comes immediately before an existing proof + context entry (used as a view, as a rewrite rule or as name for a new + context entry) then such entry is cleared too. -- Option `Refine Instance Mode` has been deprecated and will be removed in - the next version. + E.g. The following sentences are elaborated as follows (when H is an existing + proof context entry): -- :cmd:`Coercion` does not warn ambiguous paths which are obviously convertible with - existing ones. + - `=> {x..} H` -> `=> {x..H} H` + - `=> {x..} /H` -> `=> /v {x..H}` + - `rewrite {x..} H` -> `rewrite E {x..H}` -- A new flag :flag:`Fast Name Printing` has been introduced. It changes the - algorithm used for allocating bound variable names for a faster but less - clever one. + (`#9341 `_, by Enrico Tassi). -Tools +- Vernacular commands: -- The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values: - - `no` disables native_compute - - `yes` enables native_compute and precompiles `.v` files to native code - - `ondemand` enables native_compute but compiles code only when `native_compute` is called + - Binders for an :cmd:`Instance` now act more like binders for a :cmd:`Theorem`. + Names may not be repeated, and may not overlap with section variable names. - The default value is `ondemand`. + - Removed the deprecated `Implicit Tactic` family of commands. - Note that this flag now has priority over the configure flag of the same name. - -- A new `-bytecode-compiler` flag for `coqc` and `coqtop` controls whether - conversion can use the VM. The default value is `yes`. + - The `Automatic Introduction` option has been removed and is now the + default. -- CoqIDE now supports input for Unicode characters. For example, typing - "\alpha" then the "Shift+Space" will insert the greek letter alpha. - In fact, typing the prefix string "\a" is sufficient. - A larger number of default bindings are provided, following the latex - naming convention. Bindings can be customized, either globally, or on a - per-project basis, with the requirement is that keys must begin with a - backslash and contain no space character. Bindings may be assigned custom - priorities, so that prefixes resolve to the most convenient bindings. - The documentation pages for CoqIDE provides further details. + - `Arguments` now accepts names for arguments provided with `extra_scopes`. -- The pretty timing diff scripts (flag `TIMING=1` to a - `coq_makefile`-made `Makefile`, also - `tools/make-both-single-timing-files.py`, - `tools/make-both-time-files.py`, and `tools/make-one-time-file.py`) - now correctly support non-UTF-8 characters in the output of - `coqc`/`make` as well as printing to stdout, on both python2 and - python3. + - The naming scheme for anonymous binders in a `Theorem` has changed to + avoid conflicts with explicitly named binders. -Standard Library + - Computation of implicit arguments now properly handles local definitions in the + binders for an `Instance`, and can be mixed with implicit binders `{x : T}`. -- Added lemmas about monotonicity of `N.double` and `N.succ_double`, and about - the upper bound of number represented by a vector. - Allowed implicit vector length argument in `Ndigits.Bv2N`. + - :cmd:`Declare Instance` now requires an instance name. -- Added `Bvector.BVeq` that decides whether two `Bvector`\s are equal. + - The flag :flag:`Refine Instance Mode` has been turned off by default, meaning that + :cmd:`Instance` no longer opens a proof when a body is provided. -- Added notations for `BVxor`, `BVand`, `BVor`, `BVeq` and `BVneg`. + - Command :cmd:`Instance`, when no body is provided, now always opens + a proof. This is a breaking change, as instance of :n:`Instance + @ident__1 : @ident__2.` where :n:`@ident__2` is a trivial class will + have to be changed into :n:`Instance @ident__1 : @ident__2 := {}.` + or :n:`Instance @ident__1 : @ident__2. Proof. Qed.`. -- Added `ByteVector` type that can convert to and from [string]. + - The flag :flag:`Program Mode` now means that the `Program` attribute is enabled + for all commands that support it. In particular, it does not have any effect + on tactics anymore. May cause some incompatibilities. -- The prelude used to be automatically Exported and is now only - Imported. This should be relevant only when importing files which - don't use `-noinit` into files which do. + - The algorithm computing implicit arguments now behaves uniformly for primitive + projection and application nodes (bug #9508). -- Added `Coq.Structures.OrderedTypeEx.String_as_OT` to make strings an - ordered type (using lexical order). + - :cmd:`Hypotheses` and :cmd:`Variables` can now take implicit + binders inside sections. -- The `Coq.Numbers.Cyclic.Int31` library is deprecated. + - Removed deprecated option `Automatic Coercions Import`. -- Added lemmas about `Z.testbit`, `Z.ones`, and `Z.modulo`. + - The ``Show Script`` command has been deprecated. -- Moved the `auto` hints of the `FSet` library into a new - `fset` database. + - The flag :flag:`Refine Instance Mode` has been deprecated and will + be removed in the next version. -Universes + - :cmd:`Coercion` does not warn ambiguous paths which are obviously convertible with + existing ones. -- Added `Print Universes Subgraph` variant of `Print Universes`. - Try for instance `Print Universes Subgraph(sigT2.u1 sigT_of_sigT2.u1 projT3_eq.u1 eq_sigT2_rect.u1).` + - A new flag :flag:`Fast Name Printing` has been introduced. It changes the + algorithm used for allocating bound variable names for a faster but less + clever one. -- Added private universes for opaque polymorphic constants, see doc - for the :opt"`Private Polymorphic Universes` option (and Unset it to get - the previous behaviour). + - Option ``Typeclasses Axioms Are Instances`` (compatibility option + introduced in the previous version) is deprecated. Use :cmd:`Declare + Instance` for axioms which should be instances. -SProp + - Removed option `Printing Primitive Projection Compatibility` -- Added a universe "SProp" for definitionally proof irrelevant - propositions. Use with -allow-sprop. See manual for details. +- Standard Library: -Inductives + - Added lemmas about monotonicity of `N.double` and `N.succ_double`, and about + the upper bound of number represented by a vector. + Allowed implicit vector length argument in `Ndigits.Bv2N`. -- An option and attributes to control the automatic decision to declare - an inductive type as template polymorphic were added. Warning - "auto-template" (off by default) can trigger when an inductive is - automatically declared template polymorphic without the attribute. + - Added `Bvector.BVeq` that decides whether two `Bvector`\s are equal. -Funind + - Added notations for `BVxor`, `BVand`, `BVor`, `BVeq` and `BVneg`. -- Inductive types declared by Funind will never be template polymorphic. + - Added `ByteVector` type that can convert to and from [string]. -Misc + - The prelude used to be automatically Exported and is now only + Imported. This should be relevant only when importing files which + don't use `-noinit` into files which do. -- Option :opt`Typeclasses Axioms Are Instances` (compatibility option introduced in the previous version) is deprecated. Use :cmd:`Declare Instance` for axioms which should be instances. + - Added `Coq.Structures.OrderedTypeEx.String_as_OT` to make strings an + ordered type (using lexical order). -- Removed option `Printing Primitive Projection Compatibility` - -SSReflect - -- New intro patterns: - - temporary introduction: `=> +` - - block introduction: `=> [^ prefix ] [^~ suffix ]` - - fast introduction: `=> >` - - tactics as views: `=> /ltac:mytac` - - replace hypothesis: `=> {}H` - See the reference manual for the actual documentation. + - The `Coq.Numbers.Cyclic.Int31` library is deprecated. -- Clear discipline made consistent across the entire proof language. - Whenever a clear switch `{x..}` comes immediately before an existing proof - context entry (used as a view, as a rewrite rule or as name for a new - context entry) then such entry is cleared too. + - Added lemmas about `Z.testbit`, `Z.ones`, and `Z.modulo`. - E.g. The following sentences are elaborated as follows (when H is an existing - proof context entry): - - `=> {x..} H` -> `=> {x..H} H` - - `=> {x..} /H` -> `=> /v {x..H}` - - `rewrite {x..} H` -> `rewrite E {x..H}` + - Moved the `auto` hints of the `FSet` library into a new + `fset` database. -Diffs +- Some error messages that show problems with a pair of non-matching + values will now highlight the differences. -- Some error messages that show problems with a pair of non-matching values will now - highlight the differences. Version 8.9 ----------- diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index 97d86943fb..6cbd00f45d 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -252,6 +252,8 @@ use antialiased fonts or not, by setting the environment variable `GDK_USE_XFT` to 1 or 0 respectively. +.. _coqide-unicode: + Bindings for input of Unicode symbols ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 3ca1dda4d6..ac079ea7d5 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1376,6 +1376,8 @@ Abbreviations denoted expression is performed at definition time. Type checking is done only at the time of use of the abbreviation. +.. _numeral-notations: + Numeral notations ----------------- -- cgit v1.2.3 From deb35e4fc79909e0695fa719847394f1f8567442 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 23 Apr 2019 19:05:53 +0200 Subject: Change entry for #9906. --- doc/sphinx/changes.rst | 3 +++ 1 file changed, 3 insertions(+) (limited to 'doc/sphinx') diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index d8ea9c1552..0a9e9b55ff 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -256,6 +256,9 @@ Other changes in 8.10+beta1 and `#9705 `_, by Jason Gross) + - coq_makefile's install target now errors if any file to install is missing + (`#9906 `_, by Gaëtan Gilbert). + - Specification language, type inference: - Fixing a missing check in interpreting instances of existential -- cgit v1.2.3 From 13d6db12f4e40e995572b15af52e3c31dd0c5182 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 24 Apr 2019 11:18:55 +0200 Subject: Finish adding authors and links to PRs. --- doc/sphinx/changes.rst | 122 +++++++++++++++++++++++++++++++++---------------- 1 file changed, 83 insertions(+), 39 deletions(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 0a9e9b55ff..7adc1b5f08 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -21,7 +21,8 @@ reference manual. Here are the most important user-visible changes: - A notion of primitive object was added to the calculus. Its first instance is primitive cyclic unsigned integers, axiomatized in - module :g:`UInt63`. See Section :ref:`primitive-integers` + module :g:`UInt63`. See Section :ref:`primitive-integers`. + The `Coq.Numbers.Cyclic.Int31` library is deprecated (`#6914 `_, by Maxime Dénès, Benjamin Grégoire and Vincent Laporte). @@ -336,6 +337,7 @@ Other changes in 8.10+beta1 - Tactic names are no longer allowed to clash, even if they are not defined in the same section. For example, the following is no longer accepted: :g:`Ltac foo := idtac. Section S. Ltac foo := fail. End S.` + (`#8555 `_, by Maxime Dénès). - Names of existential variables occurring in Ltac functions (e.g. :g:`?[n]` or :g:`?n` in terms - not in patterns) are now interpreted @@ -350,18 +352,23 @@ Other changes in 8.10+beta1 - Hint declaration and removal should now specify a database (e.g. `Hint Resolve foo : database`). When the database name is omitted, the hint is added to the - `core` database (as previously), but a deprecation warning is emitted. + `core` database (as previously), but a deprecation warning is emitted + (`#8987 `_, by Maxime Dénès). - There are now tactics in `PreOmega.v` called `Z.div_mod_to_equations`, `Z.quot_rem_to_equations`, and `Z.to_euclidean_division_equations` (which combines the `div_mod` - and `quot_rem` variants) which allow `lia`, `nia`, `romega`, etc to + and `quot_rem` variants) which allow :tacn:`lia`, :tacn:`nia`, etc to support `Z.div` and `Z.modulo` (`Z.quot` and `Z.rem`, respectively), by posing the specifying equation for `Z.div` and `Z.modulo` before - replacing them with atoms. + replacing them with atoms + (`#8062 `_, by Jason Gross). - The syntax of the :tacn:`autoapply` tactic was fixed to conform with preexisting - documentation: it now takes a `with` clause instead of a `using` clause. + documentation: it now takes a `with` clause instead of a `using` clause + (`#9524 `_, + closes `#7632 `_, + by Théo Zimmermann). - SSReflect clear discipline made consistent across the entire proof language. Whenever a clear switch `{x..}` comes immediately before an existing proof @@ -380,90 +387,127 @@ Other changes in 8.10+beta1 - Vernacular commands: - Binders for an :cmd:`Instance` now act more like binders for a :cmd:`Theorem`. - Names may not be repeated, and may not overlap with section variable names. + Names may not be repeated, and may not overlap with section variable names + (`#8820 `_, + closes `#8791 `_, + by Jasper Hugunin). - - Removed the deprecated `Implicit Tactic` family of commands. + - Removed the deprecated `Implicit Tactic` family of commands + (`#8779 `_, by Pierre-Marie Pédrot). - The `Automatic Introduction` option has been removed and is now the - default. + default + (`#9001 `_, + by Emilio Jesús Gallego Arias). - - `Arguments` now accepts names for arguments provided with `extra_scopes`. + - `Arguments` now accepts names for arguments provided with `extra_scopes` + (`#9117 `_, by Maxime Dénès). - The naming scheme for anonymous binders in a `Theorem` has changed to - avoid conflicts with explicitly named binders. + avoid conflicts with explicitly named binders + (`#9160 `_, + closes `#8819 `_, + by Jasper Hugunin). - Computation of implicit arguments now properly handles local definitions in the - binders for an `Instance`, and can be mixed with implicit binders `{x : T}`. + binders for an `Instance`, and can be mixed with implicit binders `{x : T}` + (`#9307 `_, + closes `#9300 `_, + by Jasper Hugunin). - :cmd:`Declare Instance` now requires an instance name. - - The flag :flag:`Refine Instance Mode` has been turned off by default, meaning that - :cmd:`Instance` no longer opens a proof when a body is provided. + The flag :flag:`Refine Instance Mode` has been turned off by default, + meaning that :cmd:`Instance` no longer opens a proof when a body is + provided. The flag has been deprecated and will be removed in the next + version. + + (`#9270 `_, + and `#9825 `_, + by Maxime Dénès) - Command :cmd:`Instance`, when no body is provided, now always opens a proof. This is a breaking change, as instance of :n:`Instance @ident__1 : @ident__2.` where :n:`@ident__2` is a trivial class will have to be changed into :n:`Instance @ident__1 : @ident__2 := {}.` - or :n:`Instance @ident__1 : @ident__2. Proof. Qed.`. + or :n:`Instance @ident__1 : @ident__2. Proof. Qed.` + (`#9274 `_, by Maxime Dénès). - The flag :flag:`Program Mode` now means that the `Program` attribute is enabled for all commands that support it. In particular, it does not have any effect - on tactics anymore. May cause some incompatibilities. + on tactics anymore. May cause some incompatibilities + (`#9410 `_, by Maxime Dénès). - The algorithm computing implicit arguments now behaves uniformly for primitive - projection and application nodes (bug #9508). + projection and application nodes + (`#9509 `_, + closes `#9508 `_, + by Pierre-Marie Pédrot). - :cmd:`Hypotheses` and :cmd:`Variables` can now take implicit - binders inside sections. + binders inside sections + (`#9364 `_, + closes `#9363 `_, + by Jasper Hugunin). - - Removed deprecated option `Automatic Coercions Import`. + - Removed deprecated option `Automatic Coercions Import` + (`#8094 `_, by Maxime Dénès). - - The ``Show Script`` command has been deprecated. + - The ``Show Script`` command has been deprecated + (`#9829 `_, by Vincent Laporte). - - The flag :flag:`Refine Instance Mode` has been deprecated and will - be removed in the next version. - - - :cmd:`Coercion` does not warn ambiguous paths which are obviously convertible with - existing ones. + - :cmd:`Coercion` does not warn ambiguous paths which are obviously + convertible with existing ones + (`#9743 `_, + closes `#3219 `_, + by Kazuhiko Sakaguchi). - A new flag :flag:`Fast Name Printing` has been introduced. It changes the algorithm used for allocating bound variable names for a faster but less - clever one. + clever one + (`#9078 `_, by Pierre-Marie Pédrot). - Option ``Typeclasses Axioms Are Instances`` (compatibility option introduced in the previous version) is deprecated. Use :cmd:`Declare - Instance` for axioms which should be instances. + Instance` for axioms which should be instances + (`#8920 `_, by Gaëtan Gilbert). - Removed option `Printing Primitive Projection Compatibility` + (`#9306 `_, by Gaëtan Gilbert). - Standard Library: - - Added lemmas about monotonicity of `N.double` and `N.succ_double`, and about - the upper bound of number represented by a vector. - Allowed implicit vector length argument in `Ndigits.Bv2N`. - - Added `Bvector.BVeq` that decides whether two `Bvector`\s are equal. + Added notations for `BVxor`, `BVand`, `BVor`, `BVeq` and `BVneg` + (`#8171 `_, by Yishuai Li). - - Added notations for `BVxor`, `BVand`, `BVor`, `BVeq` and `BVneg`. + - Added `ByteVector` type that can convert to and from `string` + (`#8365 `_, by Yishuai Li). - - Added `ByteVector` type that can convert to and from [string]. + - Added lemmas about monotonicity of `N.double` and `N.succ_double`, and about + the upper bound of number represented by a vector. + Allowed implicit vector length argument in `Ndigits.Bv2N` + (`#8815 `_, by Yishuai Li). - The prelude used to be automatically Exported and is now only Imported. This should be relevant only when importing files which - don't use `-noinit` into files which do. + don't use `-noinit` into files which do + (`#9013 `_, by Gaëtan Gilert). - Added `Coq.Structures.OrderedTypeEx.String_as_OT` to make strings an - ordered type (using lexical order). - - - The `Coq.Numbers.Cyclic.Int31` library is deprecated. + ordered type, using lexical order + (`#7221 `_, by Li Yao). - - Added lemmas about `Z.testbit`, `Z.ones`, and `Z.modulo`. + - Added lemmas about `Z.testbit`, `Z.ones`, and `Z.modulo` + (`#9425 `_, by Andres Erbsen). - Moved the `auto` hints of the `FSet` library into a new - `fset` database. + `fset` database + (`#9725 `_, by Frédéric Besson). - Some error messages that show problems with a pair of non-matching - values will now highlight the differences. + values will now highlight the differences + (`#8669 `_, by Jim Fehrle). Version 8.9 -- cgit v1.2.3 From 50654fc1917e8fc475973c9066280839aa0e2d88 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 25 Apr 2019 09:17:59 +0200 Subject: Remove misplaced CHANGES entry and fix links formatting. PR #8187 misplaced its CHANGES entry. We remove it in this commit instead of moving it to the right place because it is reverted in #9987. --- doc/sphinx/changes.rst | 18 +++++++----------- 1 file changed, 7 insertions(+), 11 deletions(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 7adc1b5f08..648561fbb5 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -675,16 +675,12 @@ Notations - Deprecated compatibility notations will actually be removed in the next version of Coq. Uses of these notations are generally easy to fix thanks to the hint contained in the deprecation warnings. For - projects that require more than a handful of such fixes, there is [a - script](https://gist.github.com/JasonGross/9770653967de3679d131c59d42de6d17#file-replace-notations-py) - that will do it automatically, using the output of coqc. The script + projects that require more than a handful of such fixes, there is `a + script + `_ + that will do it automatically, using the output of ``coqc``. The script contains documentation on its usage in a comment at the top. -- When several notations are available for the same expression, - priority is given to latest notations defined in the scopes being - opened, in order, rather than to the latest notations defined - independently of whether they are in an opened scope or not. - Tactics - Added toplevel goal selector `!` which expects a single focused goal. @@ -768,7 +764,7 @@ Standard Library `Require Import Coq.Compat.Coq88` will make these notations available. Users wishing to port their developments automatically may download `fix.py` from - + https://gist.github.com/JasonGross/5d4558edf8f5c2c548a3d96c17820169 and run a command like `while true; do make -Okj 2>&1 | /path/to/fix.py; done` and get a cup of coffee. (This command must be manually interrupted once the build finishes all the way though. @@ -792,8 +788,8 @@ Tools If you would like to maintain this tool externally, please contact us. - Removed the Emacs modes distributed with Coq. You are advised to - use [Proof-General](https://proofgeneral.github.io/) (and optionally - [Company-Coq](https://github.com/cpitclaudel/company-coq)) instead. + use `Proof-General `_ (and optionally + `Company-Coq `_) instead. If your use case is not covered by these alternative Emacs modes, please open an issue. We can help set up external maintenance as part of Proof-General, or independently as part of coq-community. -- cgit v1.2.3 From 93209c4352ef2634156c8899c391778747254e14 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 25 Apr 2019 09:22:15 +0200 Subject: Remove remaining references to CHANGES.md from the Recent changes chapter. --- doc/sphinx/changes.rst | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 648561fbb5..8aaa39f36c 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -520,7 +520,7 @@ Summary of changes 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 +deprecations that are documented in the next subsection and new features that are documented in the reference manual. Here are the most important changes: @@ -534,7 +534,7 @@ changes: 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 + next version of |Coq|, see the next subsection for a script to ease porting, by Jason Gross and Jean-Christophe Léchenet. - Added the :cmd:`Numeral Notation` command for registering decimal @@ -587,7 +587,7 @@ changes: - Library: additions and changes in the ``VectorDef``, ``Ascii``, and ``String`` libraries. 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). + contributors (source of incompatibility, see the next subsection for details). - Toplevels: ``coqtop`` and ``coqide`` can now display diffs between proof steps in color, using the :opt:`Diffs` option, by Jim Fehrle. @@ -604,7 +604,7 @@ changes: 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. +important ones are documented in the next subsection file. On the implementation side, the ``dev/doc/changes.md`` file documents the numerous changes to the implementation and improvements of @@ -932,7 +932,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.md`` file. +Most important ones are documented in the next subsection 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 @@ -1292,7 +1292,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.md`` file. +others, documented in the next subsection file. The mathematical proof language/declarative mode plugin was removed from the archive. -- cgit v1.2.3 From 0473775ea96088fc13c99d0082f26f5be6eaec85 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 25 Apr 2019 09:31:07 +0200 Subject: More review suggestions. --- doc/sphinx/changes.rst | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 8aaa39f36c..5d267b37fa 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -24,7 +24,8 @@ reference manual. Here are the most important user-visible changes: module :g:`UInt63`. See Section :ref:`primitive-integers`. The `Coq.Numbers.Cyclic.Int31` library is deprecated (`#6914 `_, by Maxime Dénès, - Benjamin Grégoire and Vincent Laporte). + Benjamin Grégoire and Vincent Laporte, + with help and reviews from many others). - The :math:`\SProp` sort of definitionally proof-irrelevant propositions was introduced. :math:`\SProp` allows to mark proof @@ -164,6 +165,8 @@ 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 and package building infrastructure. +Coq is now continuously tested against OCaml trunk, in addition to the +oldest supported and latest OCaml releases. The OPAM repository for |Coq| packages has been maintained by Guillaume Melquiond, Matthieu Sozeau, Enrico Tassi (who migrated it to opam 2) -- cgit v1.2.3 From eda7d026b6919b8bef13512f5e324c7174f81a7e Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 25 Apr 2019 16:51:35 +0200 Subject: Advertize continuous deployment of documentation. --- doc/sphinx/changes.rst | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'doc/sphinx') diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 5d267b37fa..f433df0978 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -168,6 +168,12 @@ continuous integration system and package building infrastructure. Coq is now continuously tested against OCaml trunk, in addition to the oldest supported and latest OCaml releases. +Coq's documentation for the development branch is now deployed +continously at https://coq.github.io/doc/master/api (documentation of +the ML API), https://coq.github.io/doc/master/refman (reference +manual), and https://coq.github.io/doc/master/stdlib (documentation of +the standard library). Similar links exist for the `v8.10` branch. + The OPAM repository for |Coq| packages has been maintained by Guillaume Melquiond, Matthieu Sozeau, Enrico Tassi (who migrated it to opam 2) with contributions from many users. A list of packages is available at -- cgit v1.2.3 From 5e37ef7fedf16a10b18d08c87a20e2dc42dde19a Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 29 Apr 2019 11:13:55 +0200 Subject: Add number of commits, PRs and issues closed. --- doc/sphinx/changes.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index f433df0978..441170e419 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -204,8 +204,8 @@ extent influenced the development. Version 8.10 is the fifth release of |Coq| developed on a time-based development cycle. Its development spanned 6 months from the release of |Coq| 8.9. Vincent Laporte is the release manager and maintainer of this -release. This release is the result of ??? commits and ??? PRs -merged, closing ??? issues. +release. This release is the result of ~2500 commits and ~650 PRs merged, +closing 150+ issues. | Santiago de Chile, April 2019, | Matthieu Sozeau for the |Coq| development team -- cgit v1.2.3 From 73a0d923563b5ec157d517eb5e8ea1c794be64a9 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 29 Apr 2019 17:24:26 +0200 Subject: Change entry for #10014. --- doc/sphinx/changes.rst | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'doc/sphinx') diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 441170e419..3b34973306 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -269,6 +269,10 @@ Other changes in 8.10+beta1 - coq_makefile's install target now errors if any file to install is missing (`#9906 `_, by Gaëtan Gilbert). + - Preferences from ``coqide.keys`` are no longer overridden by + modifiers preferences in ``coqiderc`` + (`#10014 `_, by Hugo Herbelin). + - Specification language, type inference: - Fixing a missing check in interpreting instances of existential -- cgit v1.2.3 From 9af92ba8374e51f00a58fe97abce18c67884db25 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 29 Apr 2019 17:46:38 +0200 Subject: Change entry from #9651. --- doc/sphinx/changes.rst | 37 +++++++++++++++++++++++++------------ 1 file changed, 25 insertions(+), 12 deletions(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 3b34973306..1c4c748295 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -79,18 +79,31 @@ reference manual. Here are the most important user-visible changes: to get the venerable Fourier-based engine (`#8457 `_, by Fréderic Besson). -- New SSReflect intro patterns: - - - temporary introduction: `=> +` - - block introduction: `=> [^ prefix ] [^~ suffix ]` - - fast introduction: `=> >` - - tactics as views: `=> /ltac:mytac` - - replace hypothesis: `=> {}H` - - See Section :ref:`introduction_ssr` - (`#6705 `_, by Enrico Tassi, - with help from Maxime Dénès, - ideas coming from various users). +- SSReflect: + + - New intro patterns: + + - temporary introduction: `=> +` + - block introduction: `=> [^ prefix ] [^~ suffix ]` + - fast introduction: `=> >` + - tactics as views: `=> /ltac:mytac` + - replace hypothesis: `=> {}H` + + See Section :ref:`introduction_ssr` + (`#6705 `_, by Enrico Tassi, + with help from Maxime Dénès, + ideas coming from various users). + + - New tactic :tacn:`under` to rewrite under binders, given an + extensionality lemma: + + - interactive mode: :n:`under @term`, associated terminator: :tacn:`over` + - one-liner mode: `under @term do [@tactic | ...]` + + It can take occurrence switches, contextual patterns, and intro patterns: + :g:`under {2}[in RHS]eq_big => [i|i ?] do ...` + (`#9651 `_, + by Erik Martin-Dorel and Enrico Tassi). - :cmd:`Combined Scheme` now works when inductive schemes are generated in sort :math:`\Type`. It used to be limited to sort `Prop` -- cgit v1.2.3 From 321d26480444c947ffdaaf849157fd373e40c988 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 25 Apr 2019 10:36:21 +0200 Subject: Fix #5752: `Hint Mode` ignored for type classes that appear as assumptions The creation of the local hint db now inherits the union of the modes from the dbs passed to `typeclasses eauto`. We could probably go further and define in a more systematic way the metadata that should be inherited. A lot of this code could also be cleaned-up by defining the merge of databases, so that the search code is parametrized by just one db (the merge of the input ones). --- doc/sphinx/addendum/type-classes.rst | 2 ++ 1 file changed, 2 insertions(+) (limited to 'doc/sphinx') diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index a5e9023732..77a6ee79cc 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -405,6 +405,8 @@ few other commands related to typeclasses. resolution with the local hypotheses use full conversion during unification. + + When considering local hypotheses, we use the union of all the modes + declared in the given databases. .. cmdv:: typeclasses eauto @num -- cgit v1.2.3 From 70e01149ad4c74d086f042f0cced74b1d0e228bf Mon Sep 17 00:00:00 2001 From: Paolo G. Giarrusso Date: Sat, 27 Apr 2019 16:11:05 +0200 Subject: Document _no_check tactics (#3225) Triggered by trying to understand https://gitlab.mpi-sws.org/iris/iris/merge_requests/235. - Add a new section at the end - Document change_no_check, and convert_concl_no_check, address review comments --- doc/sphinx/proof-engine/tactics.rst | 80 +++++++++++++++++++++++++++++++++++++ 1 file changed, 80 insertions(+) (limited to 'doc/sphinx') diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 8d9e99b9d5..02a0867341 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -4811,3 +4811,83 @@ references to automatically generated names. :name: Mangle Names Prefix Specifies the prefix to use when generating names. + +Performance-oriented tactic variants +------------------------------------ + +.. tacn:: change_no_check @term + :name: change_no_check + + For advanced usage. Similar to :n:`change @term`, but as an optimization, + it skips checking that :n:`@term` is convertible to the goal. + + Recall the Coq kernel typechecks proofs again when they are concluded to + ensure safety. Hence, using :tacn:`change` checks convertibility twice + overall, while :tacn:`convert_concl_no_check` can produce ill-typed terms, + but checks convertibility only once. + Hence, :tacn:`convert_concl_no_check` can be useful to speed up certain proof + scripts, especially if one knows by construction that the argument is + indeed convertible to the goal. + + In the following example, :tacn:`convert_concl_no_check` replaces :g:`False` by + :g:`True`, but :g:`Qed` then rejects the proof, ensuring consistency. + + .. example:: + + .. coqtop:: all abort + + Goal False. + change_no_check True. + exact I. + Fail Qed. + + .. tacv:: convert_concl_no_check @term + :name: convert_concl_no_check + + Deprecated old name for :tacn:`change_no_check`. Does not support any of its + variants. + +.. tacn:: exact_no_check @term + :name: exact_no_check + + For advanced usage. Similar to :n:`exact @term`, but as an optimization, + it skips checking that :n:`@term` has the goal's type, relying on the kernel + check instead. See :tacn:`convert_concl_no_check` for more explanations. + + .. example:: + + .. coqtop:: all abort + + Goal False. + exact_no_check I. + Fail Qed. + + .. tacv:: vm_cast_no_check @term + :name: vm_cast_no_check + + For advanced usage. Similar to :n:`exact_no_check @term`, but additionally + instructs the kernel to use :tacn:`vm_compute` to compare the + goal's type with the :n:`@term`'s type. + + .. example:: + + .. coqtop:: all abort + + Goal False. + vm_cast_no_check I. + Fail Qed. + + .. tacv:: native_cast_no_check @term + :name: native_cast_no_check + + for advanced usage. similar to :n:`exact_no_check @term`, but additionally + instructs the kernel to use :tacn:`native_compute` to compare the goal's + type with the :n:`@term`'s type. + + .. example:: + + .. coqtop:: all abort + + Goal False. + native_cast_no_check I. + Fail Qed. -- cgit v1.2.3 From 590ee35546f3528ac7ccb32306fb86e78fdce93b Mon Sep 17 00:00:00 2001 From: Paolo G. Giarrusso Date: Fri, 3 May 2019 01:13:48 +0200 Subject: Documentation for change_no_check untested variants Copy change's variants in change_no_check, since supposedly they should all be supported. But they haven't been tested, and my example fails. --- doc/sphinx/proof-engine/tactics.rst | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) (limited to 'doc/sphinx') diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 02a0867341..bb7cac17b0 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -4841,6 +4841,26 @@ Performance-oriented tactic variants exact I. Fail Qed. + :tacn:`change_no_check` supports all of `change`'s variants. + + .. tacv:: change_no_check @term with @term’ + :undocumented: + + .. tacv:: change_no_check @term at {+ @num} with @term’ + :undocumented: + + .. tacv:: change_no_check @term {? {? at {+ @num}} with @term} in @ident + + .. example:: + + .. coqtop:: all abort + + Goal True -> False. + intro H. + change_no_check False in H. + exact H. + Fail Qed. + .. tacv:: convert_concl_no_check @term :name: convert_concl_no_check -- cgit v1.2.3 From f247ae382ccf7a292f15195646ff7302a7c2bd69 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 3 May 2019 03:27:05 +0200 Subject: Copy-editing from code review Co-Authored-By: Blaisorblade --- doc/sphinx/proof-engine/tactics.rst | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 02a0867341..1f339e7761 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -4821,15 +4821,15 @@ Performance-oriented tactic variants For advanced usage. Similar to :n:`change @term`, but as an optimization, it skips checking that :n:`@term` is convertible to the goal. - Recall the Coq kernel typechecks proofs again when they are concluded to + Recall that the Coq kernel typechecks proofs again when they are concluded to ensure safety. Hence, using :tacn:`change` checks convertibility twice - overall, while :tacn:`convert_concl_no_check` can produce ill-typed terms, + overall, while :tacn:`change_no_check` can produce ill-typed terms, but checks convertibility only once. - Hence, :tacn:`convert_concl_no_check` can be useful to speed up certain proof + Hence, :tacn:`change_no_check` can be useful to speed up certain proof scripts, especially if one knows by construction that the argument is indeed convertible to the goal. - In the following example, :tacn:`convert_concl_no_check` replaces :g:`False` by + In the following example, :tacn:`change_no_check` replaces :g:`False` by :g:`True`, but :g:`Qed` then rejects the proof, ensuring consistency. .. example:: @@ -4852,7 +4852,7 @@ Performance-oriented tactic variants For advanced usage. Similar to :n:`exact @term`, but as an optimization, it skips checking that :n:`@term` has the goal's type, relying on the kernel - check instead. See :tacn:`convert_concl_no_check` for more explanations. + check instead. See :tacn:`change_no_check` for more explanations. .. example:: -- cgit v1.2.3 From 30d6ffdd4546d56c517bef5b31a862c5454240f0 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 16 Apr 2019 18:27:14 +0200 Subject: New infrastructure for the unreleased changelog. Move existing entries. --- doc/sphinx/changes.rst | 2 ++ 1 file changed, 2 insertions(+) (limited to 'doc/sphinx') diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 1c4c748295..5704587ae0 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -2,6 +2,8 @@ Recent changes -------------- +.. include:: ../unreleased.rst + Version 8.10 ------------ -- cgit v1.2.3 From 9779c0bf4945693bfd37b141e2c9f0fea200ba4d Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 25 Apr 2019 14:09:42 +0200 Subject: Integrate build and documentation of Ltac2 Since Ltac2 cannot be put under the stdlib logical root (some file names would clash), we move it to the `user-contrib` directory, to avoid adding another hardcoded path in `coqinit.ml`, following a suggestion by @ejgallego. Thanks to @Zimmi48 for the thorough documentation review and the numerous suggestions. --- doc/sphinx/biblio.bib | 17 + doc/sphinx/index.html.rst | 1 + doc/sphinx/index.latex.rst | 1 + doc/sphinx/proof-engine/ltac.rst | 4 +- doc/sphinx/proof-engine/ltac2.rst | 992 ++++++++++++++++++++++++++++++++++++++ 5 files changed, 1013 insertions(+), 2 deletions(-) create mode 100644 doc/sphinx/proof-engine/ltac2.rst (limited to 'doc/sphinx') diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib index 0467852b19..85b02013d8 100644 --- a/doc/sphinx/biblio.bib +++ b/doc/sphinx/biblio.bib @@ -551,3 +551,20 @@ the Calculus of Inductive Constructions}}, biburl = {http://dblp.uni-trier.de/rec/bib/conf/cpp/BoespflugDG11}, bibsource = {dblp computer science bibliography, http://dblp.org} } + +@inproceedings{MilnerPrincipalTypeSchemes, + author = {Damas, Luis and Milner, Robin}, + title = {Principal Type-schemes for Functional Programs}, + booktitle = {Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, + series = {POPL '82}, + year = {1982}, + isbn = {0-89791-065-6}, + location = {Albuquerque, New Mexico}, + pages = {207--212}, + numpages = {6}, + url = {http://doi.acm.org/10.1145/582153.582176}, + doi = {10.1145/582153.582176}, + acmid = {582176}, + publisher = {ACM}, + address = {New York, NY, USA}, +} diff --git a/doc/sphinx/index.html.rst b/doc/sphinx/index.html.rst index a91c6a9c5f..0a20d1c47b 100644 --- a/doc/sphinx/index.html.rst +++ b/doc/sphinx/index.html.rst @@ -42,6 +42,7 @@ Contents proof-engine/proof-handling proof-engine/tactics proof-engine/ltac + proof-engine/ltac2 proof-engine/detailed-tactic-examples proof-engine/ssreflect-proof-language diff --git a/doc/sphinx/index.latex.rst b/doc/sphinx/index.latex.rst index 708820fff7..5562736997 100644 --- a/doc/sphinx/index.latex.rst +++ b/doc/sphinx/index.latex.rst @@ -41,6 +41,7 @@ The proof engine proof-engine/proof-handling proof-engine/tactics proof-engine/ltac + proof-engine/ltac2 proof-engine/detailed-tactic-examples proof-engine/ssreflect-proof-language diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 0322b43694..d3562b52c5 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -1,7 +1,7 @@ .. _ltac: -The tactic language -=================== +Ltac +==== This chapter gives a compact documentation of |Ltac|, the tactic language available in |Coq|. We start by giving the syntax, and next, we present the diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst new file mode 100644 index 0000000000..6e33862b39 --- /dev/null +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -0,0 +1,992 @@ +.. _ltac2: + +.. coqtop:: none + + From Ltac2 Require Import Ltac2. + +Ltac2 +===== + +The Ltac tactic language is probably one of the ingredients of the success of +Coq, yet it is at the same time its Achilles' heel. Indeed, Ltac: + +- has often unclear semantics +- is very non-uniform due to organic growth +- lacks expressivity (data structures, combinators, types, ...) +- is slow +- is error-prone and fragile +- has an intricate implementation + +Following the need of users that start developing huge projects relying +critically on Ltac, we believe that we should offer a proper modern language +that features at least the following: + +- at least informal, predictable semantics +- a typing system +- standard programming facilities (i.e. datatypes) + +This new language, called Ltac2, is described in this chapter. It is still +experimental but we encourage nonetheless users to start testing it, +especially wherever an advanced tactic language is needed. The previous +implementation of Ltac, described in the previous chapter, will be referred to +as Ltac1. + +.. _ltac2_design: + +General design +-------------- + +There are various alternatives to Ltac1, such that Mtac or Rtac for instance. +While those alternatives can be quite distinct from Ltac1, we designed +Ltac2 to be closest as reasonably possible to Ltac1, while fixing the +aforementioned defects. + +In particular, Ltac2 is: + +- a member of the ML family of languages, i.e. + + * a call-by-value functional language + * with effects + * together with Hindley-Milner type system + +- a language featuring meta-programming facilities for the manipulation of + Coq-side terms +- a language featuring notation facilities to help writing palatable scripts + +We describe more in details each point in the remainder of this document. + +ML component +------------ + +Overview +~~~~~~~~ + +Ltac2 is a member of the ML family of languages, in the sense that it is an +effectful call-by-value functional language, with static typing à la +Hindley-Milner (see :cite:`MilnerPrincipalTypeSchemes`). It is commonly accepted +that ML constitutes a sweet spot in PL design, as it is relatively expressive +while not being either too lax (unlike dynamic typing) nor too strict +(unlike, say, dependent types). + +The main goal of Ltac2 is to serve as a meta-language for Coq. As such, it +naturally fits in the ML lineage, just as the historical ML was designed as +the tactic language for the LCF prover. It can also be seen as a general-purpose +language, by simply forgetting about the Coq-specific features. + +Sticking to a standard ML type system can be considered somewhat weak for a +meta-language designed to manipulate Coq terms. In particular, there is no +way to statically guarantee that a Coq term resulting from an Ltac2 +computation will be well-typed. This is actually a design choice, motivated +by retro-compatibility with Ltac1. Instead, well-typedness is deferred to +dynamic checks, allowing many primitive functions to fail whenever they are +provided with an ill-typed term. + +The language is naturally effectful as it manipulates the global state of the +proof engine. This allows to think of proof-modifying primitives as effects +in a straightforward way. Semantically, proof manipulation lives in a monad, +which allows to ensure that Ltac2 satisfies the same equations as a generic ML +with unspecified effects would do, e.g. function reduction is substitution +by a value. + +Type Syntax +~~~~~~~~~~~ + +At the level of terms, we simply elaborate on Ltac1 syntax, which is quite +close to e.g. the one of OCaml. Types follow the simply-typed syntax of OCaml. + +The non-terminal :production:`lident` designates identifiers starting with a +lowercase. + +.. productionlist:: coq + ltac2_type : ( `ltac2_type`, ... , `ltac2_type` ) `ltac2_typeconst` + : ( `ltac2_type` * ... * `ltac2_type` ) + : `ltac2_type` -> `ltac2_type` + : `ltac2_typevar` + ltac2_typeconst : ( `modpath` . )* `lident` + ltac2_typevar : '`lident` + ltac2_typeparams : ( `ltac2_typevar`, ... , `ltac2_typevar` ) + +The set of base types can be extended thanks to the usual ML type +declarations such as algebraic datatypes and records. + +Built-in types include: + +- ``int``, machine integers (size not specified, in practice inherited from OCaml) +- ``string``, mutable strings +- ``'a array``, mutable arrays +- ``exn``, exceptions +- ``constr``, kernel-side terms +- ``pattern``, term patterns +- ``ident``, well-formed identifiers + +Type declarations +~~~~~~~~~~~~~~~~~ + +One can define new types by the following commands. + +.. cmd:: Ltac2 Type @ltac2_typeparams @lident + :name: Ltac2 Type + + This command defines an abstract type. It has no use for the end user and + is dedicated to types representing data coming from the OCaml world. + +.. cmdv:: Ltac2 Type {? rec} @ltac2_typeparams @lident := @ltac2_typedef + + This command defines a type with a manifest. There are four possible + kinds of such definitions: alias, variant, record and open variant types. + + .. productionlist:: coq + ltac2_typedef : `ltac2_type` + : [ `ltac2_constructordef` | ... | `ltac2_constructordef` ] + : { `ltac2_fielddef` ; ... ; `ltac2_fielddef` } + : [ .. ] + ltac2_constructordef : `uident` [ ( `ltac2_type` , ... , `ltac2_type` ) ] + ltac2_fielddef : [ mutable ] `ident` : `ltac2_type` + + Aliases are just a name for a given type expression and are transparently + unfoldable to it. They cannot be recursive. The non-terminal + :production:`uident` designates identifiers starting with an uppercase. + + Variants are sum types defined by constructors and eliminated by + pattern-matching. They can be recursive, but the `rec` flag must be + explicitly set. Pattern-maching must be exhaustive. + + Records are product types with named fields and eliminated by projection. + Likewise they can be recursive if the `rec` flag is set. + + .. cmdv:: Ltac2 Type @ltac2_typeparams @ltac2_qualid := [ @ltac2_constructordef ] + + Open variants are a special kind of variant types whose constructors are not + statically defined, but can instead be extended dynamically. A typical example + is the standard `exn` type. Pattern-matching must always include a catch-all + clause. They can be extended by this command. + +Term Syntax +~~~~~~~~~~~ + +The syntax of the functional fragment is very close to the one of Ltac1, except +that it adds a true pattern-matching feature, as well as a few standard +constructions from ML. + +.. productionlist:: coq + ltac2_var : `lident` + ltac2_qualid : ( `modpath` . )* `lident` + ltac2_constructor: `uident` + ltac2_term : `ltac2_qualid` + : `ltac2_constructor` + : `ltac2_term` `ltac2_term` ... `ltac2_term` + : fun `ltac2_var` => `ltac2_term` + : let `ltac2_var` := `ltac2_term` in `ltac2_term` + : let rec `ltac2_var` := `ltac2_term` in `ltac2_term` + : match `ltac2_term` with `ltac2_branch` ... `ltac2_branch` end + : `int` + : `string` + : `ltac2_term` ; `ltac2_term` + : [| `ltac2_term` ; ... ; `ltac2_term` |] + : ( `ltac2_term` , ... , `ltac2_term` ) + : { `ltac2_field` `ltac2_field` ... `ltac2_field` } + : `ltac2_term` . ( `ltac2_qualid` ) + : `ltac2_term` . ( `ltac2_qualid` ) := `ltac2_term` + : [; `ltac2_term` ; ... ; `ltac2_term` ] + : `ltac2_term` :: `ltac2_term` + : ... + ltac2_branch : `ltac2_pattern` => `ltac2_term` + ltac2_pattern : `ltac2_var` + : _ + : ( `ltac2_pattern` , ... , `ltac2_pattern` ) + : `ltac2_constructor` `ltac2_pattern` ... `ltac2_pattern` + : [ ] + : `ltac2_pattern` :: `ltac2_pattern` + ltac2_field : `ltac2_qualid` := `ltac2_term` + +In practice, there is some additional syntactic sugar that allows e.g. to +bind a variable and match on it at the same time, in the usual ML style. + +There is a dedicated syntax for list and array literals. + +.. note:: + + For now, deep pattern matching is not implemented. + +Ltac Definitions +~~~~~~~~~~~~~~~~ + +.. cmd:: Ltac2 {? mutable} {? rec} @lident := @ltac2_term + :name: Ltac2 + + This command defines a new global Ltac2 value. + + For semantic reasons, the body of the Ltac2 definition must be a syntactical + value, i.e. a function, a constant or a pure constructor recursively applied to + values. + + If ``rec`` is set, the tactic is expanded into a recursive binding. + + If ``mutable`` is set, the definition can be redefined at a later stage (see below). + +.. cmd:: Ltac2 Set @qualid := @ltac2_term + :name: Ltac2 Set + + This command redefines a previous ``mutable`` definition. + Mutable definitions act like dynamic binding, i.e. at runtime, the last defined + value for this entry is chosen. This is useful for global flags and the like. + +Reduction +~~~~~~~~~ + +We use the usual ML call-by-value reduction, with an otherwise unspecified +evaluation order. This is a design choice making it compatible with OCaml, +if ever we implement native compilation. The expected equations are as follows:: + + (fun x => t) V ≡ t{x := V} (βv) + + let x := V in t ≡ t{x := V} (let) + + match C V₀ ... Vₙ with ... | C x₀ ... xₙ => t | ... end ≡ t {xᵢ := Vᵢ} (ι) + + (t any term, V values, C constructor) + +Note that call-by-value reduction is already a departure from Ltac1 which uses +heuristics to decide when evaluating an expression. For instance, the following +expressions do not evaluate the same way in Ltac1. + +:n:`foo (idtac; let x := 0 in bar)` + +:n:`foo (let x := 0 in bar)` + +Instead of relying on the :n:`idtac` idiom, we would now require an explicit thunk +not to compute the argument, and :n:`foo` would have e.g. type +:n:`(unit -> unit) -> unit`. + +:n:`foo (fun () => let x := 0 in bar)` + +Typing +~~~~~~ + +Typing is strict and follows Hindley-Milner system. Unlike Ltac1, there +are no type casts at runtime, and one has to resort to conversion +functions. See notations though to make things more palatable. + +In this setting, all usual argument-free tactics have type :n:`unit -> unit`, but +one can return as well a value of type :n:`t` thanks to terms of type :n:`unit -> t`, +or take additional arguments. + +Effects +~~~~~~~ + +Effects in Ltac2 are straightforward, except that instead of using the +standard IO monad as the ambient effectful world, Ltac2 is going to use the +tactic monad. + +Note that the order of evaluation of application is *not* specified and is +implementation-dependent, as in OCaml. + +We recall that the `Proofview.tactic` monad is essentially a IO monad together +with backtracking state representing the proof state. + +Intuitively a thunk of type :n:`unit -> 'a` can do the following: + +- It can perform non-backtracking IO like printing and setting mutable variables +- It can fail in a non-recoverable way +- It can use first-class backtrack. The proper way to figure that is that we + morally have the following isomorphism: + :n:`(unit -> 'a) ~ (unit -> exn + ('a * (exn -> 'a)))` + i.e. thunks can produce a lazy list of results where each + tail is waiting for a continuation exception. +- It can access a backtracking proof state, made out amongst other things of + the current evar assignation and the list of goals under focus. + +We describe more thoroughly the various effects existing in Ltac2 hereafter. + +Standard IO ++++++++++++ + +The Ltac2 language features non-backtracking IO, notably mutable data and +printing operations. + +Mutable fields of records can be modified using the set syntax. Likewise, +built-in types like `string` and `array` feature imperative assignment. See +modules `String` and `Array` respectively. + +A few printing primitives are provided in the `Message` module, allowing to +display information to the user. + +Fatal errors +++++++++++++ + +The Ltac2 language provides non-backtracking exceptions, also known as *panics*, +through the following primitive in module `Control`.:: + + val throw : exn -> 'a + +Unlike backtracking exceptions from the next section, this kind of error +is never caught by backtracking primitives, that is, throwing an exception +destroys the stack. This is materialized by the following equation, where `E` +is an evaluation context.:: + + E[throw e] ≡ throw e + + (e value) + +There is currently no way to catch such an exception and it is a design choice. +There might be at some future point a way to catch it in a brutal way, +destroying all backtrack and return values. + +Backtrack ++++++++++ + +In Ltac2, we have the following backtracking primitives, defined in the +`Control` module.:: + + Ltac2 Type 'a result := [ Val ('a) | Err (exn) ]. + + val zero : exn -> 'a + val plus : (unit -> 'a) -> (exn -> 'a) -> 'a + val case : (unit -> 'a) -> ('a * (exn -> 'a)) result + +If one sees thunks as lazy lists, then `zero` is the empty list and `plus` is +list concatenation, while `case` is pattern-matching. + +The backtracking is first-class, i.e. one can write +:n:`plus (fun () => "x") (fun _ => "y") : string` producing a backtracking string. + +These operations are expected to satisfy a few equations, most notably that they +form a monoid compatible with sequentialization.:: + + plus t zero ≡ t () + plus (fun () => zero e) f ≡ f e + plus (plus t f) g ≡ plus t (fun e => plus (f e) g) + + case (fun () => zero e) ≡ Err e + case (fun () => plus (fun () => t) f) ≡ Val (t,f) + + let x := zero e in u ≡ zero e + let x := plus t f in u ≡ plus (fun () => let x := t in u) (fun e => let x := f e in u) + + (t, u, f, g, e values) + +Goals ++++++ + +A goal is given by the data of its conclusion and hypotheses, i.e. it can be +represented as `[Γ ⊢ A]`. + +The tactic monad naturally operates over the whole proofview, which may +represent several goals, including none. Thus, there is no such thing as +*the current goal*. Goals are naturally ordered, though. + +It is natural to do the same in Ltac2, but we must provide a way to get access +to a given goal. This is the role of the `enter` primitive, that applies a +tactic to each currently focused goal in turn.:: + + val enter : (unit -> unit) -> unit + +It is guaranteed that when evaluating `enter f`, `f` is called with exactly one +goal under focus. Note that `f` may be called several times, or never, depending +on the number of goals under focus before the call to `enter`. + +Accessing the goal data is then implicit in the Ltac2 primitives, and may panic +if the invariants are not respected. The two essential functions for observing +goals are given below.:: + + val hyp : ident -> constr + val goal : unit -> constr + +The two above functions panic if there is not exactly one goal under focus. +In addition, `hyp` may also fail if there is no hypothesis with the +corresponding name. + +Meta-programming +---------------- + +Overview +~~~~~~~~ + +One of the major implementation issues of Ltac1 is the fact that it is +never clear whether an object refers to the object world or the meta-world. +This is an incredible source of slowness, as the interpretation must be +aware of bound variables and must use heuristics to decide whether a variable +is a proper one or referring to something in the Ltac context. + +Likewise, in Ltac1, constr parsing is implicit, so that ``foo 0`` is +not ``foo`` applied to the Ltac integer expression ``0`` (Ltac does have a +notion of integers, though it is not first-class), but rather the Coq term +:g:`Datatypes.O`. + +The implicit parsing is confusing to users and often gives unexpected results. +Ltac2 makes these explicit using quoting and unquoting notation, although there +are notations to do it in a short and elegant way so as not to be too cumbersome +to the user. + +Generic Syntax for Quotations +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +In general, quotations can be introduced in terms using the following syntax, where +:production:`quotentry` is some parsing entry. + +.. prodn:: + ltac2_term += @ident : ( @quotentry ) + +Built-in quotations ++++++++++++++++++++ + +The current implementation recognizes the following built-in quotations: + +- ``ident``, which parses identifiers (type ``Init.ident``). +- ``constr``, which parses Coq terms and produces an-evar free term at runtime + (type ``Init.constr``). +- ``open_constr``, which parses Coq terms and produces a term potentially with + holes at runtime (type ``Init.constr`` as well). +- ``pattern``, which parses Coq patterns and produces a pattern used for term + matching (type ``Init.pattern``). +- ``reference``, which parses either a :n:`@qualid` or :n:`& @ident`. Qualified names + are globalized at internalization into the corresponding global reference, + while ``&id`` is turned into ``Std.VarRef id``. This produces at runtime a + ``Std.reference``. + +The following syntactic sugar is provided for two common cases. + +- ``@id`` is the same as ``ident:(id)`` +- ``'t`` is the same as ``open_constr:(t)`` + +Strict vs. non-strict mode +++++++++++++++++++++++++++ + +Depending on the context, quotations producing terms (i.e. ``constr`` or +``open_constr``) are not internalized in the same way. There are two possible +modes, respectively called the *strict* and the *non-strict* mode. + +- In strict mode, all simple identifiers appearing in a term quotation are + required to be resolvable statically. That is, they must be the short name of + a declaration which is defined globally, excluding section variables and + hypotheses. If this doesn't hold, internalization will fail. To work around + this error, one has to specifically use the ``&`` notation. +- In non-strict mode, any simple identifier appearing in a term quotation which + is not bound in the global context is turned into a dynamic reference to a + hypothesis. That is to say, internalization will succeed, but the evaluation + of the term at runtime will fail if there is no such variable in the dynamic + context. + +Strict mode is enforced by default, e.g. for all Ltac2 definitions. Non-strict +mode is only set when evaluating Ltac2 snippets in interactive proof mode. The +rationale is that it is cumbersome to explicitly add ``&`` interactively, while it +is expected that global tactics enforce more invariants on their code. + +Term Antiquotations +~~~~~~~~~~~~~~~~~~~ + +Syntax +++++++ + +One can also insert Ltac2 code into Coq terms, similarly to what is possible in +Ltac1. + +.. prodn:: + term += ltac2:( @ltac2_term ) + +Antiquoted terms are expected to have type ``unit``, as they are only evaluated +for their side-effects. + +Semantics ++++++++++ + +Interpretation of a quoted Coq term is done in two phases, internalization and +evaluation. + +- Internalization is part of the static semantics, i.e. it is done at Ltac2 + typing time. +- Evaluation is part of the dynamic semantics, i.e. it is done when + a term gets effectively computed by Ltac2. + +Note that typing of Coq terms is a *dynamic* process occurring at Ltac2 +evaluation time, and not at Ltac2 typing time. + +Static semantics +**************** + +During internalization, Coq variables are resolved and antiquotations are +type-checked as Ltac2 terms, effectively producing a ``glob_constr`` in Coq +implementation terminology. Note that although it went through the +type-checking of **Ltac2**, the resulting term has not been fully computed and +is potentially ill-typed as a runtime **Coq** term. + +.. example:: + + The following term is valid (with type `unit -> constr`), but will fail at runtime: + + .. coqtop:: in + + Ltac2 myconstr () := constr:(nat -> 0). + +Term antiquotations are type-checked in the enclosing Ltac2 typing context +of the corresponding term expression. + +.. example:: + + The following will type-check, with type `constr`. + + .. coqdoc:: + + let x := '0 in constr:(1 + ltac2:(exact x)) + +Beware that the typing environment of antiquotations is **not** +expanded by the Coq binders from the term. + + .. example:: + + The following Ltac2 expression will **not** type-check:: + + `constr:(fun x : nat => ltac2:(exact x))` + `(* Error: Unbound variable 'x' *)` + +There is a simple reason for that, which is that the following expression would +not make sense in general. + +`constr:(fun x : nat => ltac2:(clear @x; exact x))` + +Indeed, a hypothesis can suddenly disappear from the runtime context if some +other tactic pulls the rug from under you. + +Rather, the tactic writer has to resort to the **dynamic** goal environment, +and must write instead explicitly that she is accessing a hypothesis, typically +as follows. + +`constr:(fun x : nat => ltac2:(exact (hyp @x)))` + +This pattern is so common that we provide dedicated Ltac2 and Coq term notations +for it. + +- `&x` as an Ltac2 expression expands to `hyp @x`. +- `&x` as a Coq constr expression expands to + `ltac2:(Control.refine (fun () => hyp @x))`. + +Dynamic semantics +***************** + +During evaluation, a quoted term is fully evaluated to a kernel term, and is +in particular type-checked in the current environment. + +Evaluation of a quoted term goes as follows. + +- The quoted term is first evaluated by the pretyper. +- Antiquotations are then evaluated in a context where there is exactly one goal + under focus, with the hypotheses coming from the current environment extended + with the bound variables of the term, and the resulting term is fed into the + quoted term. + +Relative orders of evaluation of antiquotations and quoted term are not +specified. + +For instance, in the following example, `tac` will be evaluated in a context +with exactly one goal under focus, whose last hypothesis is `H : nat`. The +whole expression will thus evaluate to the term :g:`fun H : nat => H`. + +`let tac () := hyp @H in constr:(fun H : nat => ltac2:(tac ()))` + +Many standard tactics perform type-checking of their argument before going +further. It is your duty to ensure that terms are well-typed when calling +such tactics. Failure to do so will result in non-recoverable exceptions. + +**Trivial Term Antiquotations** + +It is possible to refer to a variable of type `constr` in the Ltac2 environment +through a specific syntax consistent with the antiquotations presented in +the notation section. + +.. prodn:: term += $@lident + +In a Coq term, writing :g:`$x` is semantically equivalent to +:g:`ltac2:(Control.refine (fun () => x))`, up to re-typechecking. It allows to +insert in a concise way an Ltac2 variable of type :n:`constr` into a Coq term. + +Match over terms +~~~~~~~~~~~~~~~~ + +Ltac2 features a construction similar to Ltac1 :n:`match` over terms, although +in a less hard-wired way. + +.. productionlist:: coq + ltac2_term : match! `ltac2_term` with `constrmatching` .. `constrmatching` end + : lazy_match! `ltac2_term` with `constrmatching` .. `constrmatching` end + : multi_match! `ltac2_term` with `constrmatching` .. `constrmatching` end + constrmatching : | `constrpattern` => `ltac2_term` + constrpattern : `term` + : context [ `term` ] + : context `lident` [ `term` ] + +This construction is not primitive and is desugared at parsing time into +calls to term matching functions from the `Pattern` module. Internally, it is +implemented thanks to a specific scope accepting the :n:`@constrmatching` syntax. + +Variables from the :n:`@constrpattern` are statically bound in the body of the branch, to +values of type `constr` for the variables from the :n:`@constr` pattern and to a +value of type `Pattern.context` for the variable :n:`@lident`. + +Note that unlike Ltac, only lowercase identifiers are valid as Ltac2 +bindings, so that there will be a syntax error if one of the bound variables +starts with an uppercase character. + +The semantics of this construction is otherwise the same as the corresponding +one from Ltac1, except that it requires the goal to be focused. + +Match over goals +~~~~~~~~~~~~~~~~ + +Similarly, there is a way to match over goals in an elegant way, which is +just a notation desugared at parsing time. + +.. productionlist:: coq + ltac2_term : match! [ reverse ] goal with `goalmatching` ... `goalmatching` end + : lazy_match! [ reverse ] goal with `goalmatching` ... `goalmatching` end + : multi_match! [ reverse ] goal with `goalmatching` ... `goalmatching` end + goalmatching : | [ `hypmatching` ... `hypmatching` |- `constrpattern` ] => `ltac2_term` + hypmatching : `lident` : `constrpattern` + : _ : `constrpattern` + +Variables from :n:`@hypmatching` and :n:`@constrpattern` are bound in the body of the +branch. Their types are: + +- ``constr`` for pattern variables appearing in a :n:`@term` +- ``Pattern.context`` for variables binding a context +- ``ident`` for variables binding a hypothesis name. + +The same identifier caveat as in the case of matching over constr applies, and +this features has the same semantics as in Ltac1. In particular, a ``reverse`` +flag can be specified to match hypotheses from the more recently introduced to +the least recently introduced one. + +Notations +--------- + +Notations are the crux of the usability of Ltac1. We should be able to recover +a feeling similar to the old implementation by using and abusing notations. + +Scopes +~~~~~~ + +A scope is a name given to a grammar entry used to produce some Ltac2 expression +at parsing time. Scopes are described using a form of S-expression. + +.. prodn:: + ltac2_scope ::= @string %| @integer %| @lident ({+, @ltac2_scope}) + +A few scopes contain antiquotation features. For sake of uniformity, all +antiquotations are introduced by the syntax :n:`$@lident`. + +The following scopes are built-in. + +- :n:`constr`: + + + parses :n:`c = @term` and produces :n:`constr:(c)` + +- :n:`ident`: + + + parses :n:`id = @ident` and produces :n:`ident:(id)` + + parses :n:`$(x = @ident)` and produces the variable :n:`x` + +- :n:`list0(@ltac2_scope)`: + + + if :n:`@ltac2_scope` parses :production:`entry`, parses :n:`(@entry__0, ..., @entry__n)` and produces + :n:`[@entry__0; ...; @entry__n]`. + +- :n:`list0(@ltac2_scope, sep = @string__sep)`: + + + if :n:`@ltac2_scope` parses :n:`@entry`, parses :n:`(@entry__0 @string__sep ... @string__sep @entry__n)` + and produces :n:`[@entry__0; ...; @entry__n]`. + +- :n:`list1`: same as :n:`list0` (with or without separator) but parses :n:`{+ @entry}` instead + of :n:`{* @entry}`. + +- :n:`opt(@ltac2_scope)` + + + if :n:`@ltac2_scope` parses :n:`@entry`, parses :n:`{? @entry}` and produces either :n:`None` or + :n:`Some x` where :n:`x` is the parsed expression. + +- :n:`self`: + + + parses a Ltac2 expression at the current level and return it as is. + +- :n:`next`: + + + parses a Ltac2 expression at the next level and return it as is. + +- :n:`tactic(n = @integer)`: + + + parses a Ltac2 expression at the provided level :n:`n` and return it as is. + +- :n:`thunk(@ltac2_scope)`: + + + parses the same as :n:`scope`, and if :n:`e` is the parsed expression, returns + :n:`fun () => e`. + +- :n:`STRING`: + + + parses the corresponding string as an identifier and returns :n:`()`. + +- :n:`keyword(s = @string)`: + + + parses the string :n:`s` as a keyword and returns `()`. + +- :n:`terminal(s = @string)`: + + + parses the string :n:`s` as a keyword, if it is already a + keyword, otherwise as an :n:`@ident`. Returns `()`. + +- :n:`seq(@ltac2_scope__1, ..., @ltac2_scope__2)`: + + + parses :n:`scope__1`, ..., :n:`scope__n` in this order, and produces a tuple made + out of the parsed values in the same order. As an optimization, all + subscopes of the form :n:`STRING` are left out of the returned tuple, instead + of returning a useless unit value. It is forbidden for the various + subscopes to refer to the global entry using self or next. + +A few other specific scopes exist to handle Ltac1-like syntax, but their use is +discouraged and they are thus not documented. + +For now there is no way to declare new scopes from Ltac2 side, but this is +planned. + +Notations +~~~~~~~~~ + +The Ltac2 parser can be extended by syntactic notations. + +.. cmd:: Ltac2 Notation {+ @lident (@ltac2_scope) %| @string } {? : @integer} := @ltac2_term + :name: Ltac2 Notation + + A Ltac2 notation adds a parsing rule to the Ltac2 grammar, which is expanded + to the provided body where every token from the notation is let-bound to the + corresponding generated expression. + + .. example:: + + Assume we perform: + + .. coqdoc:: + + Ltac2 Notation "foo" c(thunk(constr)) ids(list0(ident)) := Bar.f c ids. + + Then the following expression + + `let y := @X in foo (nat -> nat) x $y` + + will expand at parsing time to + + `let y := @X in` + `let c := fun () => constr:(nat -> nat) with ids := [@x; y] in Bar.f c ids` + + Beware that the order of evaluation of multiple let-bindings is not specified, + so that you may have to resort to thunking to ensure that side-effects are + performed at the right time. + +Abbreviations +~~~~~~~~~~~~~ + +.. cmdv:: Ltac2 Notation @lident := @ltac2_term + + This command introduces a special kind of notations, called abbreviations, + that is designed so that it does not add any parsing rules. It is similar in + spirit to Coq abbreviations, insofar as its main purpose is to give an + absolute name to a piece of pure syntax, which can be transparently referred + by this name as if it were a proper definition. + + The abbreviation can then be manipulated just as a normal Ltac2 definition, + except that it is expanded at internalization time into the given expression. + Furthermore, in order to make this kind of construction useful in practice in + an effectful language such as Ltac2, any syntactic argument to an abbreviation + is thunked on-the-fly during its expansion. + +For instance, suppose that we define the following. + +:n:`Ltac2 Notation foo := fun x => x ().` + +Then we have the following expansion at internalization time. + +:n:`foo 0 ↦ (fun x => x ()) (fun _ => 0)` + +Note that abbreviations are not typechecked at all, and may result in typing +errors after expansion. + +Evaluation +---------- + +Ltac2 features a toplevel loop that can be used to evaluate expressions. + +.. cmd:: Ltac2 Eval @ltac2_term + :name: Ltac2 Eval + + This command evaluates the term in the current proof if there is one, or in the + global environment otherwise, and displays the resulting value to the user + together with its type. This command is pure in the sense that it does not + modify the state of the proof, and in particular all side-effects are discarded. + +Debug +----- + +.. opt:: Ltac2 Backtrace + + When this option is set, toplevel failures will be printed with a backtrace. + +Compatibility layer with Ltac1 +------------------------------ + +Ltac1 from Ltac2 +~~~~~~~~~~~~~~~~ + +Simple API +++++++++++ + +One can call Ltac1 code from Ltac2 by using the :n:`ltac1` quotation. It parses +a Ltac1 expression, and semantics of this quotation is the evaluation of the +corresponding code for its side effects. In particular, it cannot return values, +and the quotation has type :n:`unit`. + +Beware, Ltac1 **cannot** access variables from the Ltac2 scope. One is limited +to the use of standalone function calls. + +Low-level API ++++++++++++++ + +There exists a lower-level FFI into Ltac1 that is not recommended for daily use, +which is available in the `Ltac2.Ltac1` module. This API allows to directly +manipulate dynamically-typed Ltac1 values, either through the function calls, +or using the `ltac1val` quotation. The latter parses the same as `ltac1`, but +has type `Ltac2.Ltac1.t` instead of `unit`, and dynamically behaves as an Ltac1 +thunk, i.e. `ltac1val:(foo)` corresponds to the tactic closure that Ltac1 +would generate from `idtac; foo`. + +Due to intricate dynamic semantics, understanding when Ltac1 value quotations +focus is very hard. This is why some functions return a continuation-passing +style value, as it can dispatch dynamically between focused and unfocused +behaviour. + +Ltac2 from Ltac1 +~~~~~~~~~~~~~~~~ + +Same as above by switching Ltac1 by Ltac2 and using the `ltac2` quotation +instead. + +Note that the tactic expression is evaluated eagerly, if one wants to use it as +an argument to a Ltac1 function, she has to resort to the good old +:n:`idtac; ltac2:(foo)` trick. For instance, the code below will fail immediately +and won't print anything. + +.. coqtop:: in + + From Ltac2 Require Import Ltac2. + Set Default Proof Mode "Classic". + +.. coqtop:: all + + Ltac mytac tac := idtac "wow"; tac. + + Goal True. + Proof. + Fail mytac ltac2:(fail). + +Transition from Ltac1 +--------------------- + +Owing to the use of a lot of notations, the transition should not be too +difficult. In particular, it should be possible to do it incrementally. That +said, we do *not* guarantee you it is going to be a blissful walk either. +Hopefully, owing to the fact Ltac2 is typed, the interactive dialogue with Coq +will help you. + +We list the major changes and the transition strategies hereafter. + +Syntax changes +~~~~~~~~~~~~~~ + +Due to conflicts, a few syntactic rules have changed. + +- The dispatch tactical :n:`tac; [foo|bar]` is now written :n:`tac > [foo|bar]`. +- Levels of a few operators have been revised. Some tacticals now parse as if + they were a normal function, i.e. one has to put parentheses around the + argument when it is complex, e.g an abstraction. List of affected tacticals: + :n:`try`, :n:`repeat`, :n:`do`, :n:`once`, :n:`progress`, :n:`time`, :n:`abstract`. +- :n:`idtac` is no more. Either use :n:`()` if you expect nothing to happen, + :n:`(fun () => ())` if you want a thunk (see next section), or use printing + primitives from the :n:`Message` module if you want to display something. + +Tactic delay +~~~~~~~~~~~~ + +Tactics are not magically delayed anymore, neither as functions nor as +arguments. It is your responsibility to thunk them beforehand and apply them +at the call site. + +A typical example of a delayed function: + +:n:`Ltac foo := blah.` + +becomes + +:n:`Ltac2 foo () := blah.` + +All subsequent calls to `foo` must be applied to perform the same effect as +before. + +Likewise, for arguments: + +:n:`Ltac bar tac := tac; tac; tac.` + +becomes + +:n:`Ltac2 bar tac := tac (); tac (); tac ().` + +We recommend the use of syntactic notations to ease the transition. For +instance, the first example can alternatively be written as: + +:n:`Ltac2 foo0 () := blah.` +:n:`Ltac2 Notation foo := foo0 ().` + +This allows to keep the subsequent calls to the tactic as-is, as the +expression `foo` will be implicitly expanded everywhere into `foo0 ()`. Such +a trick also works for arguments, as arguments of syntactic notations are +implicitly thunked. The second example could thus be written as follows. + +:n:`Ltac2 bar0 tac := tac (); tac (); tac ().` +:n:`Ltac2 Notation bar := bar0.` + +Variable binding +~~~~~~~~~~~~~~~~ + +Ltac1 relies on complex dynamic trickery to be able to tell apart bound +variables from terms, hypotheses, etc. There is no such thing in Ltac2, +as variables are recognized statically and other constructions do not live in +the same syntactic world. Due to the abuse of quotations, it can sometimes be +complicated to know what a mere identifier represents in a tactic expression. We +recommend tracking the context and letting the compiler print typing errors to +understand what is going on. + +We list below the typical changes one has to perform depending on the static +errors produced by the typechecker. + +In Ltac expressions ++++++++++++++++++++ + +.. exn:: Unbound ( value | constructor ) X + + * if `X` is meant to be a term from the current stactic environment, replace + the problematic use by `'X`. + * if `X` is meant to be a hypothesis from the goal context, replace the + problematic use by `&X`. + +In quotations ++++++++++++++ + +.. exn:: The reference X was not found in the current environment + + * if `X` is meant to be a tactic expression bound by a Ltac2 let or function, + replace the problematic use by `$X`. + * if `X` is meant to be a hypothesis from the goal context, replace the + problematic use by `&X`. + +Exception catching +~~~~~~~~~~~~~~~~~~ + +Ltac2 features a proper exception-catching mechanism. For this reason, the +Ltac1 mechanism relying on `fail` taking integers, and tacticals decreasing it, +has been removed. Now exceptions are preserved by all tacticals, and it is +your duty to catch them and reraise them depending on your use. -- cgit v1.2.3 From 7b1feee5963633bbbfcfeefd6eca0d344e1c1b8d Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 7 May 2019 13:11:42 +0200 Subject: [refman] Add a note reminding about the typeclass_instances database. Closes #10072. --- doc/sphinx/proof-engine/tactics.rst | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 1f339e7761..7d884fd929 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3863,9 +3863,9 @@ The general command to add a hint to some databases :n:`{+ @ident}` is terms and input heads *must not* contain existential variables or be existential variables respectively, while outputs can be any term. Multiple modes can be declared for a single identifier, in that case only one mode - needs to match the arguments for the hints to be applied.The head of a term + needs to match the arguments for the hints to be applied. The head of a term is understood here as the applicative head, or the match or projection - scrutinee’s head, recursively, casts being ignored. ``Hint Mode`` is + scrutinee’s head, recursively, casts being ignored. :cmd:`Hint Mode` is especially useful for typeclasses, when one does not want to support default instances and avoid ambiguity in general. Setting a parameter of a class as an input forces proof-search to be driven by that index of the class, with ``!`` @@ -3874,8 +3874,14 @@ The general command to add a hint to some databases :n:`{+ @ident}` is .. note:: - One can use an ``Extern`` hint with no pattern to do pattern matching on - hypotheses using ``match goal with`` inside the tactic. + + One can use a :cmd:`Hint Extern` with no pattern to do + pattern matching on hypotheses using ``match goal with`` + inside the tactic. + + + If you want to add hints such as :cmd:`Hint Transparent`, + :cmd:`Hint Cut`, or :cmd:`Hint Mode`, for typeclass + resolution, do not forget to put them in the + ``typeclass_instances`` hint database. Hint databases defined in the Coq standard library -- cgit v1.2.3 From e9d6aef75963126d7a856f5b88db8fd1e550f596 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 7 May 2019 14:40:02 +0200 Subject: Define minimum Sphinx version in conf.py. We set the minimum Sphinx version in conf.py to the one that we test in our CI and the one that is documented in doc/README.md. Hopefully, it will allow users with lower Sphinx verisons get better error messages. --- doc/sphinx/conf.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 48ad60c6dd..972a53ae36 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -47,7 +47,7 @@ with open("refman-preamble.rst") as s: # -- General configuration ------------------------------------------------ # If your documentation needs a minimal Sphinx version, state it here. -#needs_sphinx = '1.0' +needs_sphinx = '1.7.8' # Add any Sphinx extension module names here, as strings. They can be # extensions coming with Sphinx (named 'sphinx.ext.*') or your custom -- cgit v1.2.3 From f958d281ab57acfb37e69bbe92ed603d87962ce6 Mon Sep 17 00:00:00 2001 From: Robert Rand Date: Tue, 7 May 2019 12:44:09 -0400 Subject: Added description of Q Note that this description is identical to that of R. R should maybe start with the word "Recursively"?--- doc/sphinx/practical-tools/utilities.rst | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 35231610fe..f799091af3 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -911,11 +911,13 @@ Command line options Coq``. :-R dir coqdir: Map physical directory dir to |Coq| logical directory ``coqdir`` (similarly to |Coq| option ``-R``). + :-Q dir coqdir: Map physical directory dir to |Coq| logical + directory ``coqdir`` (similarly to |Coq| option ``-Q``). .. note:: - option ``-R`` only has - effect on the files *following* it on the command line, so you will + options ``-R`` and ``-Q`` only have + effect on the files *following* them on the command line, so you will probably need to put this option first. -- cgit v1.2.3 From 8f7559931d79588328049586b389d4109c59a9d2 Mon Sep 17 00:00:00 2001 From: Robert Rand Date: Tue, 7 May 2019 13:05:19 -0400 Subject: Added "Recursively" for the R option --- doc/sphinx/practical-tools/utilities.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index f799091af3..554f6bf230 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -909,7 +909,7 @@ Command line options :--coqlib url: Set base URL for the Coq standard library (default is ``_). This is equivalent to ``--external url Coq``. - :-R dir coqdir: Map physical directory dir to |Coq| logical + :-R dir coqdir: Recursively map physical directory dir to |Coq| logical directory ``coqdir`` (similarly to |Coq| option ``-R``). :-Q dir coqdir: Map physical directory dir to |Coq| logical directory ``coqdir`` (similarly to |Coq| option ``-Q``). -- cgit v1.2.3 From 50a89e6882e319cf6107147b49d387dd41e81805 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 8 May 2019 20:50:36 +0200 Subject: Define a new `is_a_released_version` variable in configure.ml. Use it to not include unreleased changes when building a released version. --- doc/sphinx/changes.rst | 4 +++- doc/sphinx/conf.py | 2 ++ 2 files changed, 5 insertions(+), 1 deletion(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 5704587ae0..574b943a78 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -2,7 +2,9 @@ Recent changes -------------- -.. include:: ../unreleased.rst +.. ifconfig:: not coq_config.is_a_released_version + + .. include:: ../unreleased.rst Version 8.10 ------------ diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 48ad60c6dd..25800d3a7d 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -53,6 +53,7 @@ with open("refman-preamble.rst") as s: # extensions coming with Sphinx (named 'sphinx.ext.*') or your custom # ones. extensions = [ + 'sphinx.ext.ifconfig', 'sphinx.ext.mathjax', 'sphinx.ext.todo', 'sphinxcontrib.bibtex', @@ -100,6 +101,7 @@ def copy_formatspecific_files(app): def setup(app): app.connect('builder-inited', copy_formatspecific_files) + app.add_config_value('coq_config', coq_config, 'env') # The master toctree document. # We create this file in `copy_master_doc` above. -- cgit v1.2.3 From d3a33d5d5177d301d0fbae08fde7e82be2bf3351 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 7 May 2019 14:27:30 +0200 Subject: [refman] Move all the Ltac examples to the Ltac chapter. The Detailed examples of tactics chapter can be removed when the remaining examples are moved closer to the definitions of the corresponding tactics. This commit also moves back the footnotes from the Tactics chapter at the end of the chapter, and removes an old footnote that doesn't matter anymore. --- .../proof-engine/detailed-tactic-examples.rst | 378 ------------------- doc/sphinx/proof-engine/ltac.rst | 407 ++++++++++++++++++++- doc/sphinx/proof-engine/tactics.rst | 53 +-- 3 files changed, 414 insertions(+), 424 deletions(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst index b629d15b11..0ace9ef5b9 100644 --- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst +++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst @@ -396,381 +396,3 @@ the optional tactic of the ``Hint Rewrite`` command. .. coqtop:: none Qed. - -Using the tactic language -------------------------- - - -About the cardinality of the set of natural numbers -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -The first example which shows how to use pattern matching over the -proof context is a proof of the fact that natural numbers have more -than two elements. This can be done as follows: - -.. coqtop:: in reset - - Lemma card_nat : - ~ exists x : nat, exists y : nat, forall z:nat, x = z \/ y = z. - Proof. - -.. coqtop:: in - - red; intros (x, (y, Hy)). - -.. coqtop:: in - - elim (Hy 0); elim (Hy 1); elim (Hy 2); intros; - - match goal with - | _ : ?a = ?b, _ : ?a = ?c |- _ => - cut (b = c); [ discriminate | transitivity a; auto ] - end. - -.. coqtop:: in - - Qed. - -We can notice that all the (very similar) cases coming from the three -eliminations (with three distinct natural numbers) are successfully -solved by a match goal structure and, in particular, with only one -pattern (use of non-linear matching). - - -Permutations of lists -~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -A more complex example is the problem of permutations of -lists. The aim is to show that a list is a permutation of -another list. - -.. coqtop:: in reset - - Section Sort. - -.. coqtop:: in - - Variable A : Set. - -.. coqtop:: in - - Inductive perm : list A -> list A -> Prop := - | perm_refl : forall l, perm l l - | perm_cons : forall a l0 l1, perm l0 l1 -> perm (a :: l0) (a :: l1) - | perm_append : forall a l, perm (a :: l) (l ++ a :: nil) - | perm_trans : forall l0 l1 l2, perm l0 l1 -> perm l1 l2 -> perm l0 l2. - -.. coqtop:: in - - End Sort. - -First, we define the permutation predicate as shown above. - -.. coqtop:: none - - Require Import List. - - -.. coqtop:: in - - Ltac perm_aux n := - match goal with - | |- (perm _ ?l ?l) => apply perm_refl - | |- (perm _ (?a :: ?l1) (?a :: ?l2)) => - let newn := eval compute in (length l1) in - (apply perm_cons; perm_aux newn) - | |- (perm ?A (?a :: ?l1) ?l2) => - match eval compute in n with - | 1 => fail - | _ => - let l1' := constr:(l1 ++ a :: nil) in - (apply (perm_trans A (a :: l1) l1' l2); - [ apply perm_append | compute; perm_aux (pred n) ]) - end - end. - -Next we define an auxiliary tactic ``perm_aux`` which takes an argument -used to control the recursion depth. This tactic behaves as follows. If -the lists are identical (i.e. convertible), it concludes. Otherwise, if -the lists have identical heads, it proceeds to look at their tails. -Finally, if the lists have different heads, it rotates the first list by -putting its head at the end if the new head hasn't been the head previously. To check this, we keep track of the -number of performed rotations using the argument ``n``. We do this by -decrementing ``n`` each time we perform a rotation. It works because -for a list of length ``n`` we can make exactly ``n - 1`` rotations -to generate at most ``n`` distinct lists. Notice that we use the natural -numbers of Coq for the rotation counter. From :ref:`ltac-syntax` we know -that it is possible to use the usual natural numbers, but they are only -used as arguments for primitive tactics and they cannot be handled, so, -in particular, we cannot make computations with them. Thus the natural -choice is to use Coq data structures so that Coq makes the computations -(reductions) by ``eval compute in`` and we can get the terms back by match. - -.. coqtop:: in - - Ltac solve_perm := - match goal with - | |- (perm _ ?l1 ?l2) => - match eval compute in (length l1 = length l2) with - | (?n = ?n) => perm_aux n - end - end. - -The main tactic is ``solve_perm``. It computes the lengths of the two lists -and uses them as arguments to call ``perm_aux`` if the lengths are equal (if they -aren't, the lists cannot be permutations of each other). Using this tactic we -can now prove lemmas as follows: - -.. coqtop:: in - - Lemma solve_perm_ex1 : - perm nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil). - Proof. solve_perm. Qed. - -.. coqtop:: in - - Lemma solve_perm_ex2 : - perm nat - (0 :: 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: nil) - (0 :: 2 :: 4 :: 6 :: 8 :: 9 :: 7 :: 5 :: 3 :: 1 :: nil). - Proof. solve_perm. Qed. - -Deciding intuitionistic propositional logic -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -Pattern matching on goals allows a powerful backtracking when returning tactic -values. An interesting application is the problem of deciding intuitionistic -propositional logic. Considering the contraction-free sequent calculi LJT* of -Roy Dyckhoff :cite:`Dyc92`, it is quite natural to code such a tactic using the -tactic language as shown below. - -.. coqtop:: in reset - - Ltac basic := - match goal with - | |- True => trivial - | _ : False |- _ => contradiction - | _ : ?A |- ?A => assumption - end. - -.. coqtop:: in - - Ltac simplify := - repeat (intros; - match goal with - | H : ~ _ |- _ => red in H - | H : _ /\ _ |- _ => - elim H; do 2 intro; clear H - | H : _ \/ _ |- _ => - elim H; intro; clear H - | H : ?A /\ ?B -> ?C |- _ => - cut (A -> B -> C); - [ intro | intros; apply H; split; assumption ] - | H: ?A \/ ?B -> ?C |- _ => - cut (B -> C); - [ cut (A -> C); - [ intros; clear H - | intro; apply H; left; assumption ] - | intro; apply H; right; assumption ] - | H0 : ?A -> ?B, H1 : ?A |- _ => - cut B; [ intro; clear H0 | apply H0; assumption ] - | |- _ /\ _ => split - | |- ~ _ => red - end). - -.. coqtop:: in - - Ltac my_tauto := - simplify; basic || - match goal with - | H : (?A -> ?B) -> ?C |- _ => - cut (B -> C); - [ intro; cut (A -> B); - [ intro; cut C; - [ intro; clear H | apply H; assumption ] - | clear H ] - | intro; apply H; intro; assumption ]; my_tauto - | H : ~ ?A -> ?B |- _ => - cut (False -> B); - [ intro; cut (A -> False); - [ intro; cut B; - [ intro; clear H | apply H; assumption ] - | clear H ] - | intro; apply H; red; intro; assumption ]; my_tauto - | |- _ \/ _ => (left; my_tauto) || (right; my_tauto) - end. - -The tactic ``basic`` tries to reason using simple rules involving truth, falsity -and available assumptions. The tactic ``simplify`` applies all the reversible -rules of Dyckhoff’s system. Finally, the tactic ``my_tauto`` (the main -tactic to be called) simplifies with ``simplify``, tries to conclude with -``basic`` and tries several paths using the backtracking rules (one of the -four Dyckhoff’s rules for the left implication to get rid of the contraction -and the right ``or``). - -Having defined ``my_tauto``, we can prove tautologies like these: - -.. coqtop:: in - - Lemma my_tauto_ex1 : - forall A B : Prop, A /\ B -> A \/ B. - Proof. my_tauto. Qed. - -.. coqtop:: in - - Lemma my_tauto_ex2 : - forall A B : Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B. - Proof. my_tauto. Qed. - - -Deciding type isomorphisms -~~~~~~~~~~~~~~~~~~~~~~~~~~ - -A more tricky problem is to decide equalities between types modulo -isomorphisms. Here, we choose to use the isomorphisms of the simply -typed λ-calculus with Cartesian product and unit type (see, for -example, :cite:`RC95`). The axioms of this λ-calculus are given below. - -.. coqtop:: in reset - - Open Scope type_scope. - -.. coqtop:: in - - Section Iso_axioms. - -.. coqtop:: in - - Variables A B C : Set. - -.. coqtop:: in - - Axiom Com : A * B = B * A. - - Axiom Ass : A * (B * C) = A * B * C. - - Axiom Cur : (A * B -> C) = (A -> B -> C). - - Axiom Dis : (A -> B * C) = (A -> B) * (A -> C). - - Axiom P_unit : A * unit = A. - - Axiom AR_unit : (A -> unit) = unit. - - Axiom AL_unit : (unit -> A) = A. - -.. coqtop:: in - - Lemma Cons : B = C -> A * B = A * C. - - Proof. - - intro Heq; rewrite Heq; reflexivity. - - Qed. - -.. coqtop:: in - - End Iso_axioms. - -.. coqtop:: in - - Ltac simplify_type ty := - match ty with - | ?A * ?B * ?C => - rewrite <- (Ass A B C); try simplify_type_eq - | ?A * ?B -> ?C => - rewrite (Cur A B C); try simplify_type_eq - | ?A -> ?B * ?C => - rewrite (Dis A B C); try simplify_type_eq - | ?A * unit => - rewrite (P_unit A); try simplify_type_eq - | unit * ?B => - rewrite (Com unit B); try simplify_type_eq - | ?A -> unit => - rewrite (AR_unit A); try simplify_type_eq - | unit -> ?B => - rewrite (AL_unit B); try simplify_type_eq - | ?A * ?B => - (simplify_type A; try simplify_type_eq) || - (simplify_type B; try simplify_type_eq) - | ?A -> ?B => - (simplify_type A; try simplify_type_eq) || - (simplify_type B; try simplify_type_eq) - end - with simplify_type_eq := - match goal with - | |- ?A = ?B => try simplify_type A; try simplify_type B - end. - -.. coqtop:: in - - Ltac len trm := - match trm with - | _ * ?B => let succ := len B in constr:(S succ) - | _ => constr:(1) - end. - -.. coqtop:: in - - Ltac assoc := repeat rewrite <- Ass. - -.. coqtop:: in - - Ltac solve_type_eq n := - match goal with - | |- ?A = ?A => reflexivity - | |- ?A * ?B = ?A * ?C => - apply Cons; let newn := len B in solve_type_eq newn - | |- ?A * ?B = ?C => - match eval compute in n with - | 1 => fail - | _ => - pattern (A * B) at 1; rewrite Com; assoc; solve_type_eq (pred n) - end - end. - -.. coqtop:: in - - Ltac compare_structure := - match goal with - | |- ?A = ?B => - let l1 := len A - with l2 := len B in - match eval compute in (l1 = l2) with - | ?n = ?n => solve_type_eq n - end - end. - -.. coqtop:: in - - Ltac solve_iso := simplify_type_eq; compare_structure. - -The tactic to judge equalities modulo this axiomatization is shown above. -The algorithm is quite simple. First types are simplified using axioms that -can be oriented (this is done by ``simplify_type`` and ``simplify_type_eq``). -The normal forms are sequences of Cartesian products without Cartesian product -in the left component. These normal forms are then compared modulo permutation -of the components by the tactic ``compare_structure``. If they have the same -lengths, the tactic ``solve_type_eq`` attempts to prove that the types are equal. -The main tactic that puts all these components together is called ``solve_iso``. - -Here are examples of what can be solved by ``solve_iso``. - -.. coqtop:: in - - Lemma solve_iso_ex1 : - forall A B : Set, A * unit * B = B * (unit * A). - Proof. - intros; solve_iso. - Qed. - -.. coqtop:: in - - Lemma solve_iso_ex2 : - forall A B C : Set, - (A * unit -> B * (C * unit)) = - (A * unit -> (C -> unit) * C) * (unit -> A -> B). - Proof. - intros; solve_iso. - Qed. diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index d3562b52c5..d35e4ab782 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -3,12 +3,25 @@ Ltac ==== -This chapter gives a compact documentation of |Ltac|, the tactic language -available in |Coq|. We start by giving the syntax, and next, we present the -informal semantics. If you want to know more regarding this language and -especially about its foundations, you can refer to :cite:`Del00`. Chapter -:ref:`detailedexamplesoftactics` is devoted to giving small but nontrivial -use examples of this language. +This chapter documents the tactic language |Ltac|. + +We start by giving the syntax, and next, we present the informal +semantics. If you want to know more regarding this language and +especially about its foundations, you can refer to :cite:`Del00`. + +.. example:: + + Here are some examples of the kind of tactic macros that this + language allows to write. + + .. coqdoc:: + + Ltac reduce_and_try_to_solve := simpl; intros; auto. + + Ltac destruct_bool_and_rewrite b H1 H2 := + destruct b; [ rewrite H1; eauto | rewrite H2; eauto ]. + + Some more advanced examples are given in Section :ref:`ltac-examples`. .. _ltac-syntax: @@ -1160,6 +1173,388 @@ Printing |Ltac| tactics This command displays a list of all user-defined tactics, with their arguments. + +.. _ltac-examples: + +Examples of using |Ltac| +------------------------- + + +About the cardinality of the set of natural numbers +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The first example which shows how to use pattern matching over the +proof context is a proof of the fact that natural numbers have more +than two elements. This can be done as follows: + +.. coqtop:: in reset + + Lemma card_nat : + ~ exists x : nat, exists y : nat, forall z:nat, x = z \/ y = z. + Proof. + +.. coqtop:: in + + red; intros (x, (y, Hy)). + +.. coqtop:: in + + elim (Hy 0); elim (Hy 1); elim (Hy 2); intros; + + match goal with + | _ : ?a = ?b, _ : ?a = ?c |- _ => + cut (b = c); [ discriminate | transitivity a; auto ] + end. + +.. coqtop:: in + + Qed. + +We can notice that all the (very similar) cases coming from the three +eliminations (with three distinct natural numbers) are successfully +solved by a match goal structure and, in particular, with only one +pattern (use of non-linear matching). + + +Permutations of lists +~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +A more complex example is the problem of permutations of +lists. The aim is to show that a list is a permutation of +another list. + +.. coqtop:: in reset + + Section Sort. + +.. coqtop:: in + + Variable A : Set. + +.. coqtop:: in + + Inductive perm : list A -> list A -> Prop := + | perm_refl : forall l, perm l l + | perm_cons : forall a l0 l1, perm l0 l1 -> perm (a :: l0) (a :: l1) + | perm_append : forall a l, perm (a :: l) (l ++ a :: nil) + | perm_trans : forall l0 l1 l2, perm l0 l1 -> perm l1 l2 -> perm l0 l2. + +.. coqtop:: in + + End Sort. + +First, we define the permutation predicate as shown above. + +.. coqtop:: none + + Require Import List. + + +.. coqtop:: in + + Ltac perm_aux n := + match goal with + | |- (perm _ ?l ?l) => apply perm_refl + | |- (perm _ (?a :: ?l1) (?a :: ?l2)) => + let newn := eval compute in (length l1) in + (apply perm_cons; perm_aux newn) + | |- (perm ?A (?a :: ?l1) ?l2) => + match eval compute in n with + | 1 => fail + | _ => + let l1' := constr:(l1 ++ a :: nil) in + (apply (perm_trans A (a :: l1) l1' l2); + [ apply perm_append | compute; perm_aux (pred n) ]) + end + end. + +Next we define an auxiliary tactic ``perm_aux`` which takes an argument +used to control the recursion depth. This tactic behaves as follows. If +the lists are identical (i.e. convertible), it concludes. Otherwise, if +the lists have identical heads, it proceeds to look at their tails. +Finally, if the lists have different heads, it rotates the first list by +putting its head at the end if the new head hasn't been the head previously. To check this, we keep track of the +number of performed rotations using the argument ``n``. We do this by +decrementing ``n`` each time we perform a rotation. It works because +for a list of length ``n`` we can make exactly ``n - 1`` rotations +to generate at most ``n`` distinct lists. Notice that we use the natural +numbers of Coq for the rotation counter. From :ref:`ltac-syntax` we know +that it is possible to use the usual natural numbers, but they are only +used as arguments for primitive tactics and they cannot be handled, so, +in particular, we cannot make computations with them. Thus the natural +choice is to use Coq data structures so that Coq makes the computations +(reductions) by ``eval compute in`` and we can get the terms back by match. + +.. coqtop:: in + + Ltac solve_perm := + match goal with + | |- (perm _ ?l1 ?l2) => + match eval compute in (length l1 = length l2) with + | (?n = ?n) => perm_aux n + end + end. + +The main tactic is ``solve_perm``. It computes the lengths of the two lists +and uses them as arguments to call ``perm_aux`` if the lengths are equal (if they +aren't, the lists cannot be permutations of each other). Using this tactic we +can now prove lemmas as follows: + +.. coqtop:: in + + Lemma solve_perm_ex1 : + perm nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil). + Proof. solve_perm. Qed. + +.. coqtop:: in + + Lemma solve_perm_ex2 : + perm nat + (0 :: 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: nil) + (0 :: 2 :: 4 :: 6 :: 8 :: 9 :: 7 :: 5 :: 3 :: 1 :: nil). + Proof. solve_perm. Qed. + +Deciding intuitionistic propositional logic +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Pattern matching on goals allows a powerful backtracking when returning tactic +values. An interesting application is the problem of deciding intuitionistic +propositional logic. Considering the contraction-free sequent calculi LJT* of +Roy Dyckhoff :cite:`Dyc92`, it is quite natural to code such a tactic using the +tactic language as shown below. + +.. coqtop:: in reset + + Ltac basic := + match goal with + | |- True => trivial + | _ : False |- _ => contradiction + | _ : ?A |- ?A => assumption + end. + +.. coqtop:: in + + Ltac simplify := + repeat (intros; + match goal with + | H : ~ _ |- _ => red in H + | H : _ /\ _ |- _ => + elim H; do 2 intro; clear H + | H : _ \/ _ |- _ => + elim H; intro; clear H + | H : ?A /\ ?B -> ?C |- _ => + cut (A -> B -> C); + [ intro | intros; apply H; split; assumption ] + | H: ?A \/ ?B -> ?C |- _ => + cut (B -> C); + [ cut (A -> C); + [ intros; clear H + | intro; apply H; left; assumption ] + | intro; apply H; right; assumption ] + | H0 : ?A -> ?B, H1 : ?A |- _ => + cut B; [ intro; clear H0 | apply H0; assumption ] + | |- _ /\ _ => split + | |- ~ _ => red + end). + +.. coqtop:: in + + Ltac my_tauto := + simplify; basic || + match goal with + | H : (?A -> ?B) -> ?C |- _ => + cut (B -> C); + [ intro; cut (A -> B); + [ intro; cut C; + [ intro; clear H | apply H; assumption ] + | clear H ] + | intro; apply H; intro; assumption ]; my_tauto + | H : ~ ?A -> ?B |- _ => + cut (False -> B); + [ intro; cut (A -> False); + [ intro; cut B; + [ intro; clear H | apply H; assumption ] + | clear H ] + | intro; apply H; red; intro; assumption ]; my_tauto + | |- _ \/ _ => (left; my_tauto) || (right; my_tauto) + end. + +The tactic ``basic`` tries to reason using simple rules involving truth, falsity +and available assumptions. The tactic ``simplify`` applies all the reversible +rules of Dyckhoff’s system. Finally, the tactic ``my_tauto`` (the main +tactic to be called) simplifies with ``simplify``, tries to conclude with +``basic`` and tries several paths using the backtracking rules (one of the +four Dyckhoff’s rules for the left implication to get rid of the contraction +and the right ``or``). + +Having defined ``my_tauto``, we can prove tautologies like these: + +.. coqtop:: in + + Lemma my_tauto_ex1 : + forall A B : Prop, A /\ B -> A \/ B. + Proof. my_tauto. Qed. + +.. coqtop:: in + + Lemma my_tauto_ex2 : + forall A B : Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B. + Proof. my_tauto. Qed. + + +Deciding type isomorphisms +~~~~~~~~~~~~~~~~~~~~~~~~~~ + +A more tricky problem is to decide equalities between types modulo +isomorphisms. Here, we choose to use the isomorphisms of the simply +typed λ-calculus with Cartesian product and unit type (see, for +example, :cite:`RC95`). The axioms of this λ-calculus are given below. + +.. coqtop:: in reset + + Open Scope type_scope. + +.. coqtop:: in + + Section Iso_axioms. + +.. coqtop:: in + + Variables A B C : Set. + +.. coqtop:: in + + Axiom Com : A * B = B * A. + + Axiom Ass : A * (B * C) = A * B * C. + + Axiom Cur : (A * B -> C) = (A -> B -> C). + + Axiom Dis : (A -> B * C) = (A -> B) * (A -> C). + + Axiom P_unit : A * unit = A. + + Axiom AR_unit : (A -> unit) = unit. + + Axiom AL_unit : (unit -> A) = A. + +.. coqtop:: in + + Lemma Cons : B = C -> A * B = A * C. + + Proof. + + intro Heq; rewrite Heq; reflexivity. + + Qed. + +.. coqtop:: in + + End Iso_axioms. + +.. coqtop:: in + + Ltac simplify_type ty := + match ty with + | ?A * ?B * ?C => + rewrite <- (Ass A B C); try simplify_type_eq + | ?A * ?B -> ?C => + rewrite (Cur A B C); try simplify_type_eq + | ?A -> ?B * ?C => + rewrite (Dis A B C); try simplify_type_eq + | ?A * unit => + rewrite (P_unit A); try simplify_type_eq + | unit * ?B => + rewrite (Com unit B); try simplify_type_eq + | ?A -> unit => + rewrite (AR_unit A); try simplify_type_eq + | unit -> ?B => + rewrite (AL_unit B); try simplify_type_eq + | ?A * ?B => + (simplify_type A; try simplify_type_eq) || + (simplify_type B; try simplify_type_eq) + | ?A -> ?B => + (simplify_type A; try simplify_type_eq) || + (simplify_type B; try simplify_type_eq) + end + with simplify_type_eq := + match goal with + | |- ?A = ?B => try simplify_type A; try simplify_type B + end. + +.. coqtop:: in + + Ltac len trm := + match trm with + | _ * ?B => let succ := len B in constr:(S succ) + | _ => constr:(1) + end. + +.. coqtop:: in + + Ltac assoc := repeat rewrite <- Ass. + +.. coqtop:: in + + Ltac solve_type_eq n := + match goal with + | |- ?A = ?A => reflexivity + | |- ?A * ?B = ?A * ?C => + apply Cons; let newn := len B in solve_type_eq newn + | |- ?A * ?B = ?C => + match eval compute in n with + | 1 => fail + | _ => + pattern (A * B) at 1; rewrite Com; assoc; solve_type_eq (pred n) + end + end. + +.. coqtop:: in + + Ltac compare_structure := + match goal with + | |- ?A = ?B => + let l1 := len A + with l2 := len B in + match eval compute in (l1 = l2) with + | ?n = ?n => solve_type_eq n + end + end. + +.. coqtop:: in + + Ltac solve_iso := simplify_type_eq; compare_structure. + +The tactic to judge equalities modulo this axiomatization is shown above. +The algorithm is quite simple. First types are simplified using axioms that +can be oriented (this is done by ``simplify_type`` and ``simplify_type_eq``). +The normal forms are sequences of Cartesian products without Cartesian product +in the left component. These normal forms are then compared modulo permutation +of the components by the tactic ``compare_structure``. If they have the same +lengths, the tactic ``solve_type_eq`` attempts to prove that the types are equal. +The main tactic that puts all these components together is called ``solve_iso``. + +Here are examples of what can be solved by ``solve_iso``. + +.. coqtop:: in + + Lemma solve_iso_ex1 : + forall A B : Set, A * unit * B = B * (unit * A). + Proof. + intros; solve_iso. + Qed. + +.. coqtop:: in + + Lemma solve_iso_ex2 : + forall A B C : Set, + (A * unit -> B * (C * unit)) = + (A * unit -> (C -> unit) * C) * (unit -> A -> B). + Proof. + intros; solve_iso. + Qed. + + Debugging |Ltac| tactics ------------------------ diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 0f78a9b84a..c728b925ac 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3561,7 +3561,7 @@ Automation .. tacn:: autorewrite with {+ @ident} :name: autorewrite - This tactic [4]_ carries out rewritings according to the rewriting rule + This tactic carries out rewritings according to the rewriting rule bases :n:`{+ @ident}`. Each rewriting rule from the base :n:`@ident` is applied to the main subgoal until @@ -4661,9 +4661,12 @@ Non-logical tactics .. example:: - .. coqtop:: all reset + .. coqtop:: none reset Parameter P : nat -> Prop. + + .. coqtop:: all abort + Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5. repeat split. all: cycle 2. @@ -4679,9 +4682,8 @@ Non-logical tactics .. example:: - .. coqtop:: reset all + .. coqtop:: all abort - Parameter P : nat -> Prop. Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5. repeat split. all: swap 1 3. @@ -4694,9 +4696,8 @@ Non-logical tactics .. example:: - .. coqtop:: all reset + .. coqtop:: all abort - Parameter P : nat -> Prop. Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5. repeat split. all: revgoals. @@ -4717,7 +4718,7 @@ Non-logical tactics .. example:: - .. coqtop:: all reset + .. coqtop:: all abort Goal exists n, n=0. refine (ex_intro _ _ _). @@ -4746,39 +4747,6 @@ Non-logical tactics The ``give_up`` tactic can be used while editing a proof, to choose to write the proof script in a non-sequential order. -Simple tactic macros -------------------------- - -A simple example has more value than a long explanation: - -.. example:: - - .. coqtop:: reset all - - Ltac Solve := simpl; intros; auto. - - Ltac ElimBoolRewrite b H1 H2 := - elim b; [ intros; rewrite H1; eauto | intros; rewrite H2; eauto ]. - -The tactics macros are synchronous with the Coq section mechanism: a -tactic definition is deleted from the current environment when you -close the section (see also :ref:`section-mechanism`) where it was -defined. If you want that a tactic macro defined in a module is usable in the -modules that require it, you should put it outside of any section. - -:ref:`ltac` gives examples of more complex -user-defined tactics. - -.. [1] Actually, only the second subgoal will be generated since the - other one can be automatically checked. -.. [2] This corresponds to the cut rule of sequent calculus. -.. [3] Reminder: opaque constants will not be expanded by δ reductions. -.. [4] The behavior of this tactic has changed a lot compared to the - versions available in the previous distributions (V6). This may cause - significant changes in your theories to obtain the same result. As a - drawback of the re-engineering of the code, this tactic has also been - completely revised to get a very compact and readable version. - Delaying solving unification constraints ---------------------------------------- @@ -4917,3 +4885,8 @@ Performance-oriented tactic variants Goal False. native_cast_no_check I. Fail Qed. + +.. [1] Actually, only the second subgoal will be generated since the + other one can be automatically checked. +.. [2] This corresponds to the cut rule of sequent calculus. +.. [3] Reminder: opaque constants will not be expanded by δ reductions. -- cgit v1.2.3 From f39ff2b2390a6a5634dbf60ea0383fae4b9f3069 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 9 May 2019 13:11:56 +0200 Subject: Rewording, language improvements. Co-Authored-By: Jim Fehrle --- doc/sphinx/proof-engine/ltac.rst | 34 +++++++++++++++++----------------- 1 file changed, 17 insertions(+), 17 deletions(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index d35e4ab782..b02f9661e2 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -6,13 +6,13 @@ Ltac This chapter documents the tactic language |Ltac|. We start by giving the syntax, and next, we present the informal -semantics. If you want to know more regarding this language and -especially about its foundations, you can refer to :cite:`Del00`. +semantics. To learn more about the language and +especially about its foundations, please refer to :cite:`Del00`. .. example:: - Here are some examples of the kind of tactic macros that this - language allows to write. + Here are some examples of simple tactic macros that the + language lets you write. .. coqdoc:: @@ -21,7 +21,7 @@ especially about its foundations, you can refer to :cite:`Del00`. Ltac destruct_bool_and_rewrite b H1 H2 := destruct b; [ rewrite H1; eauto | rewrite H2; eauto ]. - Some more advanced examples are given in Section :ref:`ltac-examples`. + See Section :ref:`ltac-examples` for more advanced examples. .. _ltac-syntax: @@ -1183,8 +1183,8 @@ Examples of using |Ltac| About the cardinality of the set of natural numbers ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The first example which shows how to use pattern matching over the -proof context is a proof of the fact that natural numbers have more +The first example shows how to use pattern matching over the +proof context to prove that natural numbers have more than two elements. This can be done as follows: .. coqtop:: in reset @@ -1210,7 +1210,7 @@ than two elements. This can be done as follows: Qed. -We can notice that all the (very similar) cases coming from the three +Notice that all the (very similar) cases coming from the three eliminations (with three distinct natural numbers) are successfully solved by a match goal structure and, in particular, with only one pattern (use of non-linear matching). @@ -1269,9 +1269,9 @@ First, we define the permutation predicate as shown above. end. Next we define an auxiliary tactic ``perm_aux`` which takes an argument -used to control the recursion depth. This tactic behaves as follows. If +used to control the recursion depth. This tactic works as follows: If the lists are identical (i.e. convertible), it concludes. Otherwise, if -the lists have identical heads, it proceeds to look at their tails. +the lists have identical heads, it looks at their tails. Finally, if the lists have different heads, it rotates the first list by putting its head at the end if the new head hasn't been the head previously. To check this, we keep track of the number of performed rotations using the argument ``n``. We do this by @@ -1296,8 +1296,8 @@ choice is to use Coq data structures so that Coq makes the computations end. The main tactic is ``solve_perm``. It computes the lengths of the two lists -and uses them as arguments to call ``perm_aux`` if the lengths are equal (if they -aren't, the lists cannot be permutations of each other). Using this tactic we +and uses them as arguments to call ``perm_aux`` if the lengths are equal. (If they +aren't, the lists cannot be permutations of each other.) Using this tactic we can now prove lemmas as follows: .. coqtop:: in @@ -1317,7 +1317,7 @@ can now prove lemmas as follows: Deciding intuitionistic propositional logic ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Pattern matching on goals allows a powerful backtracking when returning tactic +Pattern matching on goals allows powerful backtracking when returning tactic values. An interesting application is the problem of deciding intuitionistic propositional logic. Considering the contraction-free sequent calculi LJT* of Roy Dyckhoff :cite:`Dyc92`, it is quite natural to code such a tactic using the @@ -1405,7 +1405,7 @@ Having defined ``my_tauto``, we can prove tautologies like these: Deciding type isomorphisms ~~~~~~~~~~~~~~~~~~~~~~~~~~ -A more tricky problem is to decide equalities between types modulo +A trickier problem is to decide equalities between types modulo isomorphisms. Here, we choose to use the isomorphisms of the simply typed λ-calculus with Cartesian product and unit type (see, for example, :cite:`RC95`). The axioms of this λ-calculus are given below. @@ -1528,11 +1528,11 @@ example, :cite:`RC95`). The axioms of this λ-calculus are given below. The tactic to judge equalities modulo this axiomatization is shown above. The algorithm is quite simple. First types are simplified using axioms that can be oriented (this is done by ``simplify_type`` and ``simplify_type_eq``). -The normal forms are sequences of Cartesian products without Cartesian product +The normal forms are sequences of Cartesian products without a Cartesian product in the left component. These normal forms are then compared modulo permutation of the components by the tactic ``compare_structure``. If they have the same -lengths, the tactic ``solve_type_eq`` attempts to prove that the types are equal. -The main tactic that puts all these components together is called ``solve_iso``. +length, the tactic ``solve_type_eq`` attempts to prove that the types are equal. +The main tactic that puts all these components together is ``solve_iso``. Here are examples of what can be solved by ``solve_iso``. -- cgit v1.2.3 From 7843c21c9568f49a78d7c306978f446618ef8d25 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 9 May 2019 18:11:01 +0200 Subject: Improve the first two Ltac examples. --- doc/sphinx/proof-engine/ltac.rst | 193 +++++++++++++++++++++------------------ 1 file changed, 102 insertions(+), 91 deletions(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index b02f9661e2..83b8bc2308 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -9,7 +9,7 @@ We start by giving the syntax, and next, we present the informal semantics. To learn more about the language and especially about its foundations, please refer to :cite:`Del00`. -.. example:: +.. example:: Basic tactic macros Here are some examples of simple tactic macros that the language lets you write. @@ -1179,140 +1179,151 @@ Printing |Ltac| tactics Examples of using |Ltac| ------------------------- - About the cardinality of the set of natural numbers ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The first example shows how to use pattern matching over the -proof context to prove that natural numbers have more -than two elements. This can be done as follows: +.. example:: About the cardinality of the set of natural numbers -.. coqtop:: in reset + The first example shows how to use pattern matching over the proof + context to prove that natural numbers have at least two + elements. This can be done as follows: - Lemma card_nat : - ~ exists x : nat, exists y : nat, forall z:nat, x = z \/ y = z. - Proof. + .. coqtop:: reset all -.. coqtop:: in + Lemma card_nat : + ~ exists x y : nat, forall z:nat, x = z \/ y = z. + Proof. + intros (x & y & Hz). + destruct (Hz 0), (Hz 1), (Hz 2). - red; intros (x, (y, Hy)). + At this point, the :tacn:`congruence` tactic would finish the job: -.. coqtop:: in + .. coqtop:: all abort - elim (Hy 0); elim (Hy 1); elim (Hy 2); intros; + all: congruence. - match goal with - | _ : ?a = ?b, _ : ?a = ?c |- _ => - cut (b = c); [ discriminate | transitivity a; auto ] - end. + But for the purpose of the example, let's craft our own custom + tactic to solve this: -.. coqtop:: in + .. coqtop:: none - Qed. + Lemma card_nat : + ~ exists x y : nat, forall z:nat, x = z \/ y = z. + Proof. + intros (x & y & Hz). + destruct (Hz 0), (Hz 1), (Hz 2). -Notice that all the (very similar) cases coming from the three -eliminations (with three distinct natural numbers) are successfully -solved by a match goal structure and, in particular, with only one -pattern (use of non-linear matching). + .. coqtop:: all abort + all: match goal with + | _ : ?a = ?b, _ : ?a = ?c |- _ => assert (b = c) by now transitivity a + end. + all: discriminate. -Permutations of lists -~~~~~~~~~~~~~~~~~~~~~~~~~~~ + Notice that all the (very similar) cases coming from the three + eliminations (with three distinct natural numbers) are successfully + solved by a ``match goal`` structure and, in particular, with only one + pattern (use of non-linear matching). -A more complex example is the problem of permutations of -lists. The aim is to show that a list is a permutation of -another list. -.. coqtop:: in reset +Proving that a list is a permutation of a second list +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - Section Sort. +.. example:: Proving that a list is a permutation of a second list -.. coqtop:: in + Let's first define the permutation predicate: - Variable A : Set. + .. coqtop:: in reset -.. coqtop:: in + Section Sort. - Inductive perm : list A -> list A -> Prop := - | perm_refl : forall l, perm l l - | perm_cons : forall a l0 l1, perm l0 l1 -> perm (a :: l0) (a :: l1) - | perm_append : forall a l, perm (a :: l) (l ++ a :: nil) - | perm_trans : forall l0 l1 l2, perm l0 l1 -> perm l1 l2 -> perm l0 l2. + Variable A : Set. -.. coqtop:: in + Inductive perm : list A -> list A -> Prop := + | perm_refl : forall l, perm l l + | perm_cons : forall a l0 l1, perm l0 l1 -> perm (a :: l0) (a :: l1) + | perm_append : forall a l, perm (a :: l) (l ++ a :: nil) + | perm_trans : forall l0 l1 l2, perm l0 l1 -> perm l1 l2 -> perm l0 l2. - End Sort. + End Sort. -First, we define the permutation predicate as shown above. + .. coqtop:: none -.. coqtop:: none + Require Import List. - Require Import List. + Next we define an auxiliary tactic :g:`perm_aux` which takes an + argument used to control the recursion depth. This tactic works as + follows: If the lists are identical (i.e. convertible), it + completes the proof. Otherwise, if the lists have identical heads, + it looks at their tails. Finally, if the lists have different + heads, it rotates the first list by putting its head at the end. -.. coqtop:: in + Every time we perform a rotation, we decrement :g:`n`. When :g:`n` + drops down to :g:`1`, we stop performing rotations and we fail. + The idea is to give the length of the list as the initial value of + :g:`n`. This way of counting the number of rotations will avoid + going back to a head that had been considered before. - Ltac perm_aux n := - match goal with - | |- (perm _ ?l ?l) => apply perm_refl - | |- (perm _ (?a :: ?l1) (?a :: ?l2)) => + From Section :ref:`ltac-syntax` we know that Ltac has a primitive + notion of integers, but they are only used as arguments for + primitive tactics and we cannot make computations with them. Thus, + instead, we use Coq's natural number type :g:`nat`. + + .. coqtop:: in + + Ltac perm_aux n := + match goal with + | |- (perm _ ?l ?l) => apply perm_refl + | |- (perm _ (?a :: ?l1) (?a :: ?l2)) => let newn := eval compute in (length l1) in (apply perm_cons; perm_aux newn) - | |- (perm ?A (?a :: ?l1) ?l2) => + | |- (perm ?A (?a :: ?l1) ?l2) => match eval compute in n with - | 1 => fail - | _ => - let l1' := constr:(l1 ++ a :: nil) in - (apply (perm_trans A (a :: l1) l1' l2); - [ apply perm_append | compute; perm_aux (pred n) ]) + | 1 => fail + | _ => + let l1' := constr:(l1 ++ a :: nil) in + (apply (perm_trans A (a :: l1) l1' l2); + [ apply perm_append | compute; perm_aux (pred n) ]) end - end. + end. -Next we define an auxiliary tactic ``perm_aux`` which takes an argument -used to control the recursion depth. This tactic works as follows: If -the lists are identical (i.e. convertible), it concludes. Otherwise, if -the lists have identical heads, it looks at their tails. -Finally, if the lists have different heads, it rotates the first list by -putting its head at the end if the new head hasn't been the head previously. To check this, we keep track of the -number of performed rotations using the argument ``n``. We do this by -decrementing ``n`` each time we perform a rotation. It works because -for a list of length ``n`` we can make exactly ``n - 1`` rotations -to generate at most ``n`` distinct lists. Notice that we use the natural -numbers of Coq for the rotation counter. From :ref:`ltac-syntax` we know -that it is possible to use the usual natural numbers, but they are only -used as arguments for primitive tactics and they cannot be handled, so, -in particular, we cannot make computations with them. Thus the natural -choice is to use Coq data structures so that Coq makes the computations -(reductions) by ``eval compute in`` and we can get the terms back by match. -.. coqtop:: in + The main tactic is :g:`solve_perm`. It computes the lengths of the + two lists and uses them as arguments to call :g:`perm_aux` if the + lengths are equal. (If they aren't, the lists cannot be + permutations of each other.) - Ltac solve_perm := - match goal with - | |- (perm _ ?l1 ?l2) => + .. coqtop:: in + + Ltac solve_perm := + match goal with + | |- (perm _ ?l1 ?l2) => match eval compute in (length l1 = length l2) with - | (?n = ?n) => perm_aux n + | (?n = ?n) => perm_aux n end - end. + end. -The main tactic is ``solve_perm``. It computes the lengths of the two lists -and uses them as arguments to call ``perm_aux`` if the lengths are equal. (If they -aren't, the lists cannot be permutations of each other.) Using this tactic we -can now prove lemmas as follows: + And now, here is how we can use the tactic :g:`solve_perm`: -.. coqtop:: in + .. coqtop:: out - Lemma solve_perm_ex1 : - perm nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil). - Proof. solve_perm. Qed. + Goal perm nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil). -.. coqtop:: in + .. coqtop:: all abort + + solve_perm. + + .. coqtop:: out + + Goal perm nat + (0 :: 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: nil) + (0 :: 2 :: 4 :: 6 :: 8 :: 9 :: 7 :: 5 :: 3 :: 1 :: nil). + + .. coqtop:: all abort + + solve_perm. - Lemma solve_perm_ex2 : - perm nat - (0 :: 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: nil) - (0 :: 2 :: 4 :: 6 :: 8 :: 9 :: 7 :: 5 :: 3 :: 1 :: nil). - Proof. solve_perm. Qed. Deciding intuitionistic propositional logic ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -- cgit v1.2.3 From 3603a6d3324aa54c385f3f84a9fb4d5b9c2fde57 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Fri, 10 May 2019 00:15:23 +0200 Subject: Better title for the first example of the Ltac examples section. --- doc/sphinx/proof-engine/ltac.rst | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 83b8bc2308..a7eb7c2319 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -1179,10 +1179,10 @@ Printing |Ltac| tactics Examples of using |Ltac| ------------------------- -About the cardinality of the set of natural numbers -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Proof that the natural numbers have at least two elements +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. example:: About the cardinality of the set of natural numbers +.. example:: Proof that the natural numbers have at least two elements The first example shows how to use pattern matching over the proof context to prove that natural numbers have at least two -- cgit v1.2.3 From 4c642b5c27d4f9c355044cb585a645b50dd844f2 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Mon, 6 May 2019 17:38:39 +0000 Subject: [User manual] Fix two warnings related to canonical structures --- doc/sphinx/addendum/canonical-structures.rst | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst index dd21ea09bd..d81dafa4db 100644 --- a/doc/sphinx/addendum/canonical-structures.rst +++ b/doc/sphinx/addendum/canonical-structures.rst @@ -209,7 +209,7 @@ We need to define a new class that inherits from both ``EQ`` and ``LE``. LE_class : LE.class T; extra : mixin (EQ.Pack T EQ_class) (LE.cmp T LE_class) }. - Structure type := _Pack { obj : Type; class_of : class obj }. + Structure type := _Pack { obj : Type; #[not_canonical] class_of : class obj }. Arguments Mixin {e le} _. @@ -219,6 +219,9 @@ The mixin component of the ``LEQ`` class contains all the extra content we are adding to ``EQ`` and ``LE``. In particular it contains the requirement that the two relations we are combining are compatible. +The `class_of` projection of the `type` structure is annotated as *not canonical*; +it plays no role in the search for instances. + Unfortunately there is still an obstacle to developing the algebraic theory of this new class. @@ -313,9 +316,7 @@ constructor ``*``. It also tests that they work as expected. Unfortunately, these declarations are very verbose. In the following subsection we show how to make them more compact. -.. FIXME shouldn't warn - -.. coqtop:: all warn +.. coqtop:: all Module Add_instance_attempt. @@ -420,9 +421,7 @@ the reader can refer to :cite:`CSwcu`. The declaration of canonical instances can now be way more compact: -.. FIXME should not warn - -.. coqtop:: all warn +.. coqtop:: all Canonical Structure nat_LEQty := Eval hnf in Pack nat nat_LEQmx. -- cgit v1.2.3 From 34e84eafe6615055071fbdc4aaee70c4c161a0fb Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Thu, 9 May 2019 13:39:25 +0000 Subject: [Attributes] Allow explicit value for two-valued attributes Attributes that enable/disable a feature can have an explicit value (default is enable when the attribute is present). Three-valued boolean attributes do not support this: what would `#[local(false)]` mean? --- doc/sphinx/addendum/canonical-structures.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst index d81dafa4db..b593b0cef1 100644 --- a/doc/sphinx/addendum/canonical-structures.rst +++ b/doc/sphinx/addendum/canonical-structures.rst @@ -209,7 +209,7 @@ We need to define a new class that inherits from both ``EQ`` and ``LE``. LE_class : LE.class T; extra : mixin (EQ.Pack T EQ_class) (LE.cmp T LE_class) }. - Structure type := _Pack { obj : Type; #[not_canonical] class_of : class obj }. + Structure type := _Pack { obj : Type; #[canonical(false)] class_of : class obj }. Arguments Mixin {e le} _. -- cgit v1.2.3 From 4895bf8bb5d0acfaee499991973fc6537657427d Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Fri, 10 May 2019 08:48:54 +0000 Subject: [refman] Mention the `#[canonical(false)]` attribute --- doc/sphinx/language/gallina-extensions.rst | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) (limited to 'doc/sphinx') diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 5308330820..ba766c8c3d 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -2048,6 +2048,21 @@ in :ref:`canonicalstructures`; here only a simple example is given. If a same field occurs in several canonical structures, then only the structure declared first as canonical is considered. + .. note:: + To prevent a field from being involved in the inference of canonical instances, + its declaration can be annotated with the :g:`#[canonical(false)]` attribute. + + .. example:: + + For instance, when declaring the :g:`Setoid` structure above, the + :g:`Prf_equiv` field declaration could be written as follows. + + .. coqdoc:: + + #[canonical(false)] Prf_equiv : equivalence Carrier Equal + + See :ref:`canonicalstructures` for a more realistic example. + .. cmdv:: Canonical {? Structure } @ident {? : @type } := @term This is equivalent to a regular definition of :token:`ident` followed by the @@ -2067,6 +2082,10 @@ in :ref:`canonicalstructures`; here only a simple example is given. Print Canonical Projections. + .. note:: + + The last line would not show up if the corresponding projection (namely + :g:`Prf_equiv`) were annotated as not canonical, as described above. Implicit types of variables ~~~~~~~~~~~~~~~~~~~~~~~~~~~ -- cgit v1.2.3 From beb5bdec79ff371f48a478df3c24f2cf9d68aa1f Mon Sep 17 00:00:00 2001 From: Jasper Hugunin Date: Tue, 7 May 2019 15:04:04 -0700 Subject: Use Print Custom Grammar to inspect custom entries --- doc/sphinx/user-extensions/syntax-extensions.rst | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index ac079ea7d5..edec13f681 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -840,10 +840,11 @@ gives a way to let any arbitrary expression which is not handled by the custom entry ``expr`` be parsed or printed by the main grammar of term up to the insertion of a pair of curly brackets. -.. cmd:: Print Grammar @ident. +.. cmd:: Print Custom Grammar @ident. + :name: Print Custom Grammar - This displays the state of the grammar for terms and grammar for - patterns associated to the custom entry :token:`ident`. + This displays the state of the grammar for terms associated to + the custom entry :token:`ident`. Summary ~~~~~~~ -- cgit v1.2.3 From a101fdc131bd5d7a8ed1470cd7fa705ad6979e92 Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Fri, 10 May 2019 09:47:02 -0400 Subject: [refman] Use 'flag' instead of 'opt' for 'Ltac2 Debug' --- doc/sphinx/proof-engine/ltac2.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 6e33862b39..945ffd6307 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -823,9 +823,9 @@ Ltac2 features a toplevel loop that can be used to evaluate expressions. Debug ----- -.. opt:: Ltac2 Backtrace +.. flag:: Ltac2 Backtrace - When this option is set, toplevel failures will be printed with a backtrace. + When this flag is set, toplevel failures will be printed with a backtrace. Compatibility layer with Ltac1 ------------------------------ -- cgit v1.2.3 From d0f2961b1e4c4f8153d1deb3ea7a3e5fc1eb22cc Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 13 May 2019 15:36:43 +0200 Subject: Move last changelog entries for 8.10+beta1. --- doc/sphinx/changes.rst | 50 +++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 49 insertions(+), 1 deletion(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 574b943a78..be22071f66 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -355,6 +355,11 @@ Other changes in 8.10+beta1 that will do it automatically, using the output of ``coqc`` (`#8638 `_, by Jason Gross). + - Allow inspecting custom grammar entries by :cmd:`Print Custom Grammar` + (`#10061 `_, + fixes `#9681 `_, + by Jasper Hugunin, review by Pierre-Marie Pédrot and Hugo Herbelin). + - The `quote plugin `_ was removed. If some users are interested in maintaining this plugin @@ -400,7 +405,23 @@ Other changes in 8.10+beta1 closes `#7632 `_, by Théo Zimmermann). - - SSReflect clear discipline made consistent across the entire proof language. + - Modes are now taken into account by :tacn:`typeclasses eauto` for + local hypotheses + (`#9996 `_, + fixes `#5752 `_, + by Maxime Dénès, review by Pierre-Marie Pédrot). + + - New variant :tacn:`change_no_check` of :tacn:`change`, usable as a + documented replacement of :tacn:`convert_concl_no_check` + (`#10012 `_, + `#10017 `_, + `#10053 `_, and + `#10059 `_, + by Hugo Herbelin and Paolo G. Giarrusso). + +- SSReflect: + + - Clear discipline made consistent across the entire proof language. Whenever a clear switch `{x..}` comes immediately before an existing proof context entry (used as a view, as a rewrite rule or as name for a new context entry) then such entry is cleared too. @@ -414,6 +435,15 @@ Other changes in 8.10+beta1 (`#9341 `_, by Enrico Tassi). + - `inE` now expands `y \in r x` when `r` is a `simpl_rel`. + New `{pred T}` notation for a `pred T` alias in the `pred_sort` coercion + class, simplified `predType` interface: `pred_class` and `mkPredType` + deprecated, `{pred T}` and `PredType` should be used instead. + `if c return t then ...` now expects `c` to be a variable bound in `t`. + New `nonPropType` interface matching types that do _not_ have sort `Prop`. + New `relpre R f` definition for the preimage of a relation R under f + (`#9995 `_, by Georges Gonthier). + - Vernacular commands: - Binders for an :cmd:`Instance` now act more like binders for a :cmd:`Theorem`. @@ -535,10 +565,28 @@ Other changes in 8.10+beta1 `fset` database (`#9725 `_, by Frédéric Besson). + - Added :g:`Coq.Structures.EqualitiesFacts.PairUsualDecidableTypeFull` + (`#9984 `_, + by Jean-Christophe Léchenet and Oliver Nash). + - Some error messages that show problems with a pair of non-matching values will now highlight the differences (`#8669 `_, by Jim Fehrle). +- Changelog has been moved from a specific file `CHANGES.md` to the + reference manual; former Credits chapter of the reference manual has + been split in two parts: a History chapter which was enriched with + additional historical information about Coq versions 1 to 5, and a + Changes chapter which was enriched with the content formerly in + `CHANGES.md` and `COMPATIBILITY` + (`#9133 `_, + `#9668 `_, + `#9939 `_, + `#9964 `_, + and `#10085 `_, + by Théo Zimmermann, + with help and ideas from Emilio Jesús Gallego Arias, Gaëtan + Gilbert, Clément Pit-Claudel, Matthieu Sozeau, and Enrico Tassi). Version 8.9 ----------- -- cgit v1.2.3 From 5a172d9afaddf44e702af66f80bd5649031c9e4a Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 13 May 2019 16:38:40 +0200 Subject: Missing change entry for #9854. --- doc/sphinx/changes.rst | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'doc/sphinx') diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index be22071f66..cca3b2e06b 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -419,6 +419,15 @@ Other changes in 8.10+beta1 `#10059 `_, by Hugo Herbelin and Paolo G. Giarrusso). + - The simplified value returned by :tacn:`field_simplify` is not + always a fraction anymore. When the denominator is :g:`1`, it + returns :g:`x` while previously it was returning :g:`x/1`. This + change could break codes that were post-processing application of + :tacn:`field_simplify` to get rid of these :g:`x/1` + (`#9854 `_, + by Laurent Théry, + with help from Michael Soegtrop, Maxime Dénès, and Vincent Laporte). + - SSReflect: - Clear discipline made consistent across the entire proof language. -- cgit v1.2.3 From feb9c50b5812a01e9dc60e2408f4f9f38986ce8c Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Fri, 10 May 2019 22:29:57 -0400 Subject: [refman] Introduce syntax for alternatives in notations Closes GH-8482. --- doc/sphinx/README.rst | 9 ++++-- doc/sphinx/README.template.rst | 7 ++-- doc/sphinx/_static/coqnotations.sty | 29 ++++++++++++++++- doc/sphinx/_static/notations.css | 37 ++++++++++++++++++++-- doc/sphinx/addendum/extraction.rst | 2 +- doc/sphinx/addendum/generalized-rewriting.rst | 2 +- doc/sphinx/addendum/program.rst | 2 +- doc/sphinx/addendum/type-classes.rst | 8 ++--- doc/sphinx/changes.rst | 4 +-- doc/sphinx/language/gallina-extensions.rst | 12 +++---- doc/sphinx/proof-engine/ltac2.rst | 6 ++-- doc/sphinx/proof-engine/proof-handling.rst | 8 ++--- .../proof-engine/ssreflect-proof-language.rst | 20 ++++++------ doc/sphinx/proof-engine/tactics.rst | 8 ++--- doc/sphinx/proof-engine/vernacular-commands.rst | 20 ++++++------ 15 files changed, 119 insertions(+), 55 deletions(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index 881f7a310d..b20669c7f1 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -60,8 +60,11 @@ The signatures of most objects can be written using a succinct DSL for Coq notat ``{*, …}``, ``{+, …}`` an optional or mandatory repeatable block, with repetitions separated by commas -``%|``, ``%{``, … - an escaped character (rendered without the leading ``%``) +``{| … | … | … }`` + an alternative, indicating than one of multiple constructs can be used + +``%{``, ``%}``, ``%|`` + an escaped character (rendered without the leading ``%``). In most cases, escaping is not necessary. In particular, the following expressions are all parsed as plain text, and do not need escaping: ``{ xyz }``, ``x |- y``. But the following escapes *are* needed: ``{| a b %| c | d }``, ``all: %{``. (We use ``%`` instead of the usual ``\`` because you'd have to type ``\`` twice in your reStructuredText file.) .. FIXME document the new subscript support @@ -148,7 +151,7 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica Example:: .. prodn:: term += let: @pattern := @term in @term - .. prodn:: occ_switch ::= { {? + %| - } {* @num } } + .. prodn:: occ_switch ::= { {? {| + | - } } {* @num } } ``.. table::`` :black_nib: A Coq table, i.e. a setting that is a set of values. Example:: diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst index 78803a927f..2093765608 100644 --- a/doc/sphinx/README.template.rst +++ b/doc/sphinx/README.template.rst @@ -60,8 +60,11 @@ The signatures of most objects can be written using a succinct DSL for Coq notat ``{*, …}``, ``{+, …}`` an optional or mandatory repeatable block, with repetitions separated by commas -``%|``, ``%{``, … - an escaped character (rendered without the leading ``%``) +``{| … | … | … }`` + an alternative, indicating than one of multiple constructs can be used + +``%{``, ``%}``, ``%|`` + an escaped character (rendered without the leading ``%``). In most cases, escaping is not necessary. In particular, the following expressions are all parsed as plain text, and do not need escaping: ``{ xyz }``, ``x |- y``. But the following escapes *are* needed: ``{| a b %| c | d }``, ``all: %{``. (We use ``%`` instead of the usual ``\`` because you'd have to type ``\`` twice in your reStructuredText file.) .. FIXME document the new subscript support diff --git a/doc/sphinx/_static/coqnotations.sty b/doc/sphinx/_static/coqnotations.sty index 75eac1f724..3548b8754c 100644 --- a/doc/sphinx/_static/coqnotations.sty +++ b/doc/sphinx/_static/coqnotations.sty @@ -18,6 +18,9 @@ \newlength{\nscriptsize} \setlength{\nscriptsize}{0.8em} +\newlength{\nboxsep} +\setlength{\nboxsep}{2pt} + \newcommand*{\scriptsmallsquarebox}[1]{% % Force width \makebox[\nscriptsize]{% @@ -31,7 +34,8 @@ \newcommand*{\nsup}[1]{^{\nscript{0.15}{#1}}} \newcommand*{\nsub}[1]{_{\nscript{0.35}{#1}}} \newcommand*{\nnotation}[1]{#1} -\newcommand*{\nrepeat}[1]{\text{\adjustbox{cfbox=nbordercolor 0.5pt 2pt,bgcolor=nbgcolor}{#1\hspace{.5\nscriptsize}}}} +\newcommand*{\nbox}[1]{\adjustbox{cfbox=nbordercolor 0.5pt \nboxsep,bgcolor=nbgcolor}{#1}} +\newcommand*{\nrepeat}[1]{\text{\nbox{#1\hspace{.5\nscriptsize}}}} \newcommand*{\nwrapper}[1]{\ensuremath{\displaystyle#1}} % https://tex.stackexchange.com/questions/310877/ \newcommand*{\nhole}[1]{\textit{\color{nholecolor}#1}} @@ -42,9 +46,32 @@ } % +% https://tex.stackexchange.com/questions/490262/ +\def\naltsep{} +\newsavebox{\nsavedalt} +\newlength{\naltvruleht} +\newlength{\naltvruledp} +\def\naltvrule{\smash{\vrule height\naltvruleht depth\naltvruledp}} +\newcommand{\nalternative}[2]{% + % First measure the contents of the box without the bar + \bgroup% + \def\naltsep{}% + \savebox{\nsavedalt}{#1}% + \setlength{\naltvruleht}{\ht\nsavedalt}% + \setlength{\naltvruledp}{\dp\nsavedalt}% + \addtolength{\naltvruleht}{#2}% + \addtolength{\naltvruledp}{#2}% + % Then redraw it with the bar + \def\naltsep{\naltvrule}% + #1\egroup} + \newcssclass{notation-sup}{\nsup{#1}} \newcssclass{notation-sub}{\nsub{#1}} \newcssclass{notation}{\nnotation{#1}} \newcssclass{repeat}{\nrepeat{#1}} \newcssclass{repeat-wrapper}{\nwrapper{#1}} \newcssclass{hole}{\nhole{#1}} +\newcssclass{alternative}{\nalternative{\nbox{#1}}{0pt}} +\newcssclass{alternative-block}{#1} +\newcssclass{repeated-alternative}{\nalternative{#1}{\nboxsep}} +\newcssclass{alternative-separator}{\quad\naltsep{}\quad} diff --git a/doc/sphinx/_static/notations.css b/doc/sphinx/_static/notations.css index dcb47d1786..8322ab0137 100644 --- a/doc/sphinx/_static/notations.css +++ b/doc/sphinx/_static/notations.css @@ -45,15 +45,46 @@ width: 2.2em; } -.notation .repeat { +.notation .repeat, .notation .alternative { background: #EAEAEA; border: 1px solid #AAA; display: inline-block; - padding-right: 0.6em; /* Space for the left half of the sub- and sup-scripts */ - padding-left: 0.2em; + padding: 0 0.2em 0 0.3em; margin: 0.25em 0; } +.notation .repeated-alternative { + display: inline-table; +} + +.notation .alternative { + display: inline-table; + padding: 0 0.2em; +} + +.notation .alternative-block { + display: table-cell; + padding: 0 0.5em; +} + +.notation .alternative-separator { + border-left: 1px solid black; /* Display a thin bar */ + display: table-cell; + width: 0; +} + +.alternative-block:first-child { + padding-left: 0; +} + +.alternative-block:last-child { + padding-right: 0; +} + +.notation .repeat { + padding-right: 0.6em; /* Space for the left half of the sub- and sup-scripts */ +} + .notation .repeat-wrapper { display: inline-block; position: relative; diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index e93b01f14d..8a895eb515 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -99,7 +99,7 @@ Extraction Options Setting the target language ~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: Extraction Language ( OCaml | Haskell | Scheme ) +.. cmd:: Extraction Language {| OCaml | Haskell | Scheme } :name: Extraction Language The ability to fix target language is the first and more important diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index b474c51f17..4d9e8d8b3a 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -809,7 +809,7 @@ Usage ~~~~~ -.. tacn:: rewrite_strat @s [in @ident] +.. tacn:: rewrite_strat @s {? in @ident } :name: rewrite_strat Rewrite using the strategy s in hypothesis ident or the conclusion. diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index b410833d25..22ddcae584 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -283,7 +283,7 @@ optional identifier is used when multiple functions have unsolved obligations (e.g. when defining mutually recursive blocks). The optional tactic is replaced by the default one if not specified. -.. cmd:: {? Local|Global} Obligation Tactic := @tactic +.. cmd:: {? {| Local | Global } } Obligation Tactic := @tactic :name: Obligation Tactic Sets the default obligation solving tactic applied to all obligations diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 77a6ee79cc..9219aa21ca 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -311,7 +311,7 @@ Summary of the commands This command has no effect when used on a typeclass. -.. cmd:: Instance @ident {? @binders} : @class t1 … tn [| priority] := { field1 := b1 ; …; fieldi := bi } +.. cmd:: Instance @ident {? @binders} : @class t1 … tn {? | priority } := { field1 := b1 ; …; fieldi := bi } This command is used to declare a typeclass instance named :token:`ident` of the class :token:`class` with parameters ``t1`` to ``tn`` and @@ -324,7 +324,7 @@ Summary of the commands :tacn:`auto` hints. If the priority is not specified, it defaults to the number of non-dependent binders of the instance. - .. cmdv:: Instance @ident {? @binders} : forall {? @binders}, @class @term__1 … @term__n [| priority] := @term + .. cmdv:: Instance @ident {? @binders} : forall {? @binders}, @class @term__1 … @term__n {? | priority } := @term This syntax is used for declaration of singleton class instances or for directly giving an explicit term of type :n:`forall @binders, @class @@ -356,7 +356,7 @@ Summary of the commands Besides the :cmd:`Class` and :cmd:`Instance` vernacular commands, there are a few other commands related to typeclasses. -.. cmd:: Existing Instance {+ @ident} [| priority] +.. cmd:: Existing Instance {+ @ident} {? | priority } This command adds an arbitrary list of constants whose type ends with an applied typeclass to the instance database with an optional @@ -579,7 +579,7 @@ Settings Typeclasses eauto `:=` ~~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: Typeclasses eauto := {? debug} {? (dfs) | (bfs) } @num +.. cmd:: Typeclasses eauto := {? debug} {? {| (dfs) | (bfs) } } @num :name: Typeclasses eauto This command allows more global customization of the typeclass diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 5704587ae0..e54c1a4eec 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -457,7 +457,7 @@ Other changes in 8.10+beta1 - Command :cmd:`Instance`, when no body is provided, now always opens a proof. This is a breaking change, as instance of :n:`Instance @ident__1 : @ident__2.` where :n:`@ident__2` is a trivial class will - have to be changed into :n:`Instance @ident__1 : @ident__2 := {}.` + have to be changed into :n:`Instance @ident__1 : @ident__2 := %{%}.` or :n:`Instance @ident__1 : @ident__2. Proof. Qed.` (`#9274 `_, by Maxime Dénès). @@ -3881,7 +3881,7 @@ Vernacular commands Equality Schemes", this replaces deprecated option "Equality Scheme"). - Made support for automatic generation of case analysis schemes available to user (governed by option "Set Case Analysis Schemes"). -- New command :n:`{? Global } Generalizable [All|No] [Variable|Variables] {* @ident}` to +- New command :n:`{? Global } Generalizable {| All | No } {| Variable | Variables } {* @ident}` to declare which identifiers are generalizable in `` `{} `` and `` `() `` binders. - New command "Print Opaque Dependencies" to display opaque constants in addition to all variables, parameters or axioms a theorem or diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 5308330820..af658b4698 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -931,7 +931,7 @@ In the syntax of module application, the ! prefix indicates that any :token:`module_binding`. The output module type is verified against each :token:`module_type`. -.. cmdv:: Module [ Import | Export ] +.. cmdv:: Module {| Import | Export } Behaves like :cmd:`Module`, but automatically imports or exports the module. @@ -1648,7 +1648,7 @@ Declaring Implicit Arguments -.. cmd:: Arguments @qualid {* [ @ident ] | { @ident } | @ident } +.. cmd:: Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } } :name: Arguments (implicits) This command is used to set implicit arguments *a posteriori*, @@ -1665,20 +1665,20 @@ Declaring Implicit Arguments This command clears implicit arguments. -.. cmdv:: Global Arguments @qualid {* [ @ident ] | { @ident } | @ident } +.. cmdv:: Global Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } } This command is used to recompute the implicit arguments of :token:`qualid` after ending of the current section if any, enforcing the implicit arguments known from inside the section to be the ones declared by the command. -.. cmdv:: Local Arguments @qualid {* [ @ident ] | { @ident } | @ident } +.. cmdv:: Local Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } } When in a module, tell not to activate the implicit arguments of :token:`qualid` declared by this command to contexts that require the module. -.. cmdv:: {? Global | Local } Arguments @qualid {*, {+ [ @ident ] | { @ident } | @ident } } +.. cmdv:: {? {| Global | Local } } Arguments @qualid {*, {+ {| [ @ident ] | { @ident } | @ident } } } For names of constants, inductive types, constructors, lemmas which can only be applied to a fixed number of @@ -2148,7 +2148,7 @@ that specify which variables should be generalizable. Disable implicit generalization entirely. This is the default behavior. -.. cmd:: Generalizable (Variable | Variables) {+ @ident } +.. cmd:: Generalizable {| Variable | Variables } {+ @ident } Allow generalization of the given identifiers only. Calling this command multiple times adds to the allowed identifiers. diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 945ffd6307..aa603fc966 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -668,7 +668,7 @@ A scope is a name given to a grammar entry used to produce some Ltac2 expression at parsing time. Scopes are described using a form of S-expression. .. prodn:: - ltac2_scope ::= @string %| @integer %| @lident ({+, @ltac2_scope}) + ltac2_scope ::= {| @string | @integer | @lident ({+, @ltac2_scope}) } A few scopes contain antiquotation features. For sake of uniformity, all antiquotations are introduced by the syntax :n:`$@lident`. @@ -751,7 +751,7 @@ Notations The Ltac2 parser can be extended by syntactic notations. -.. cmd:: Ltac2 Notation {+ @lident (@ltac2_scope) %| @string } {? : @integer} := @ltac2_term +.. cmd:: Ltac2 Notation {+ {| @lident (@ltac2_scope) | @string } } {? : @integer} := @ltac2_term :name: Ltac2 Notation A Ltac2 notation adds a parsing rule to the Ltac2 grammar, which is expanded @@ -966,7 +966,7 @@ errors produced by the typechecker. In Ltac expressions +++++++++++++++++++ -.. exn:: Unbound ( value | constructor ) X +.. exn:: Unbound {| value | constructor } X * if `X` is meant to be a term from the current stactic environment, replace the problematic use by `'X`. diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 16b158c397..139506723e 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -322,7 +322,7 @@ Navigation in the proof tree .. index:: { } -.. cmd:: %{ %| %} +.. cmd:: {| %{ | %} } The command ``{`` (without a terminating period) focuses on the first goal, much like :cmd:`Focus` does, however, the subproof can only be @@ -430,7 +430,7 @@ not go beyond enclosing ``{`` and ``}``, so bullets can be reused as further nesting levels provided they are delimited by these. Bullets are made of repeated ``-``, ``+`` or ``*`` symbols: -.. prodn:: bullet ::= {+ - } %| {+ + } %| {+ * } +.. prodn:: bullet ::= {| {+ - } | {+ + } | {+ * } } 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 @@ -492,7 +492,7 @@ The following example script illustrates all these features: Set Bullet Behavior ``````````````````` -.. opt:: Bullet Behavior %( "None" %| "Strict Subproofs" %) +.. opt:: Bullet Behavior {| "None" | "Strict Subproofs" } :name: Bullet Behavior This option controls the bullet behavior and can take two possible values: @@ -680,7 +680,7 @@ This image shows an error message with diff highlighting in CoqIDE: How to enable diffs ``````````````````` -.. opt:: Diffs %( "on" %| "off" %| "removed" %) +.. opt:: Diffs {| "on" | "off" | "removed" } :name: Diffs The “on” setting highlights added tokens in green, while the “removed” setting diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 4e40df6f94..d6247d1bc5 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -617,7 +617,7 @@ Abbreviations selected occurrences of a term. .. prodn:: - occ_switch ::= { {? + %| - } {* @num } } + occ_switch ::= { {? {| + | - } } {* @num } } where: @@ -2273,7 +2273,7 @@ to the others. Iteration ~~~~~~~~~ -.. tacn:: do {? @num } ( @tactic | [ {+| @tactic } ] ) +.. tacn:: do {? @num } {| @tactic | [ {+| @tactic } ] } :name: do (ssreflect) This tactical offers an accurate control on the repetition of tactics. @@ -2300,7 +2300,7 @@ tactic should be repeated on the current subgoal. There are four kinds of multipliers: .. prodn:: - mult ::= @num ! %| ! %| @num ? %| ? + mult ::= {| @num ! | ! | @num ? | ? } Their meaning is: @@ -5444,7 +5444,7 @@ equivalences are indeed taken into account, otherwise only single |SSR| searching tool -------------------- -.. cmd:: Search {? @pattern } {* {? - } %( @string %| @pattern %) {? % @ident} } {? in {+ {? - } @qualid } } +.. cmd:: Search {? @pattern } {* {? - } {| @string | @pattern } {? % @ident} } {? in {+ {? - } @qualid } } :name: Search (ssreflect) This is the |SSR| extension of the Search command. :token:`qualid` is the @@ -5686,7 +5686,7 @@ respectively. local cofix definition -.. tacn:: set @ident {? : @term } := {? @occ_switch } %( @term %| ( @c_pattern) %) +.. tacn:: set @ident {? : @term } := {? @occ_switch } {| @term | ( @c_pattern) } abbreviation (see :ref:`abbreviations_ssr`) @@ -5714,26 +5714,26 @@ introduction see :ref:`introduction_ssr` localization see :ref:`localization_ssr` -.. prodn:: tactic += do {? @mult } %( @tactic %| [ {+| @tactic } ] %) +.. prodn:: tactic += do {? @mult } {| @tactic | [ {+| @tactic } ] } iteration see :ref:`iteration_ssr` -.. prodn:: tactic += @tactic ; %( first %| last %) {? @num } %( @tactic %| [ {+| @tactic } ] %) +.. prodn:: tactic += @tactic ; {| first | last } {? @num } {| @tactic | [ {+| @tactic } ] } selector see :ref:`selectors_ssr` -.. prodn:: tactic += @tactic ; %( first %| last %) {? @num } +.. prodn:: tactic += @tactic ; {| first | last } {? @num } rotation see :ref:`selectors_ssr` -.. prodn:: tactic += by %( @tactic %| [ {*| @tactic } ] %) +.. prodn:: tactic += by {| @tactic | [ {*| @tactic } ] } closing see :ref:`terminators_ssr` Commands ~~~~~~~~ -.. cmd:: Hint View for %( move %| apply %) / @ident {? | @num } +.. cmd:: Hint View for {| move | apply } / @ident {? | @num } view hint declaration (see :ref:`declaring_new_hints_ssr`) diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 0f78a9b84a..c8442d7ea1 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3777,8 +3777,8 @@ The general command to add a hint to some databases :n:`{+ @ident}` is discrimination network to relax or constrain it in the case of discriminated databases. - .. cmdv:: Hint Variables %( Transparent %| Opaque %) : @ident - Hint Constants %( Transparent %| Opaque %) : @ident + .. cmdv:: Hint Variables {| Transparent | Opaque } : @ident + Hint Constants {| Transparent | Opaque } : @ident :name: Hint Variables; Hint Constants This sets the transparency flag used during unification of @@ -3850,7 +3850,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is semantics of :n:`Hint Cut @regexp` is to set the cut expression to :n:`c | regexp`, the initial cut expression being `emp`. - .. cmdv:: Hint Mode @qualid {* (+ | ! | -)} : @ident + .. cmdv:: Hint Mode @qualid {* {| + | ! | - } } : @ident :name: Hint Mode This sets an optional mode of use of the identifier :n:`@qualid`. When @@ -4016,7 +4016,7 @@ We propose a smooth transitional path by providing the :opt:`Loose Hint Behavior option which accepts three flags allowing for a fine-grained handling of non-imported hints. -.. opt:: Loose Hint Behavior %( "Lax" %| "Warn" %| "Strict" %) +.. opt:: Loose Hint Behavior {| "Lax" | "Warn" | "Strict" } :name: Loose Hint Behavior This option accepts three values, which control the behavior of hints w.r.t. diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index e207a072cc..4e4a10f590 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -91,13 +91,13 @@ and tables: Flags, options and tables are identified by a series of identifiers, each with an initial capital letter. -.. cmd:: {? Local | Global | Export } Set @flag +.. cmd:: {? {| Local | Global | Export } } Set @flag :name: Set Sets :token:`flag` on. Scoping qualifiers are described :ref:`here `. -.. cmd:: {? Local | Global | Export } Unset @flag +.. cmd:: {? {| Local | Global | Export } } Unset @flag :name: Unset Sets :token:`flag` off. Scoping qualifiers are @@ -108,13 +108,13 @@ capital letter. Prints the current value of :token:`flag`. -.. cmd:: {? Local | Global | Export } Set @option ( @num | @string ) +.. cmd:: {? {| Local | Global | Export } } Set @option {| @num | @string } :name: Set @option Sets :token:`option` to the specified value. Scoping qualifiers are described :ref:`here `. -.. cmd:: {? Local | Global | Export } Unset @option +.. cmd:: {? {| Local | Global | Export } } Unset @option :name: Unset @option Sets :token:`option` to its default value. Scoping qualifiers are @@ -129,17 +129,17 @@ capital letter. Prints the current value of all flags and options, and the names of all tables. -.. cmd:: Add @table ( @string | @qualid ) +.. cmd:: Add @table {| @string | @qualid } :name: Add @table Adds the specified value to :token:`table`. -.. cmd:: Remove @table ( @string | @qualid ) +.. cmd:: Remove @table {| @string | @qualid } :name: Remove @table Removes the specified value from :token:`table`. -.. cmd:: Test @table for ( @string | @qualid ) +.. cmd:: Test @table for {| @string | @qualid } :name: Test @table for Reports whether :token:`table` contains the specified value. @@ -162,7 +162,7 @@ capital letter. Scope qualifiers for :cmd:`Set` and :cmd:`Unset` ````````````````````````````````````````````````` -:n:`{? Local | Global | Export }` +:n:`{? {| Local | Global | Export } }` Flag and option settings can be global in scope or local to nested scopes created by :cmd:`Module` and :cmd:`Section` commands. There are four alternatives: @@ -622,7 +622,7 @@ file is a particular case of module called *library file*. but if a further module, say `A`, contains a command :cmd:`Require Export` `B`, then the command :cmd:`Require Import` `A` also imports the module `B.` - .. cmdv:: Require [Import | Export] {+ @qualid } + .. cmdv:: Require {| Import | Export } {+ @qualid } This loads the modules named by the :token:`qualid` sequence and their recursive @@ -988,7 +988,7 @@ Controlling display This option controls the normal displaying. -.. opt:: Warnings "{+, {? %( - %| + %) } @ident }" +.. opt:: Warnings "{+, {? {| - | + } } @ident }" :name: Warnings This option configures the display of warnings. It is experimental, and -- cgit v1.2.3 From 942621f7747bd56a7da35cacc21f0e5fdbf93413 Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Sun, 12 May 2019 19:38:36 -0400 Subject: [refman] Misc fixes (indentation, whitespace, notation syntax) --- doc/sphinx/addendum/generalized-rewriting.rst | 23 +++++++++--------- doc/sphinx/addendum/type-classes.rst | 12 +++++----- doc/sphinx/language/gallina-extensions.rst | 10 ++++---- .../language/gallina-specification-language.rst | 26 ++++++++++---------- doc/sphinx/proof-engine/ltac.rst | 28 +++++++++++----------- doc/sphinx/proof-engine/proof-handling.rst | 4 ++-- .../proof-engine/ssreflect-proof-language.rst | 2 +- doc/sphinx/proof-engine/tactics.rst | 18 +++++++------- doc/sphinx/proof-engine/vernacular-commands.rst | 12 +++++----- doc/sphinx/user-extensions/proof-schemes.rst | 27 +++++++++++---------- 10 files changed, 83 insertions(+), 79 deletions(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index 4d9e8d8b3a..847abb33fc 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -170,12 +170,12 @@ compatibility constraints. Adding new relations and morphisms ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: Add Parametric Relation (x1 : T1) ... (xn : Tk) : (A t1 ... tn) (Aeq t′1 ... t′m) {? reflexivity proved by refl} {? symmetry proved by sym} {? transitivity proved by trans} as @ident +.. cmd:: Add Parametric Relation @binders : (A t1 ... tn) (Aeq t′1 ... t′m) {? reflexivity proved by @term} {? symmetry proved by @term} {? transitivity proved by @term} as @ident This command declares a parametric relation :g:`Aeq: forall (y1 : β1 ... ym : βm)`, :g:`relation (A t1 ... tn)` over :g:`(A : αi -> ... αn -> Type)`. - The :token:`ident` gives a unique name to the morphism and it is used + The final :token:`ident` gives a unique name to the morphism and it is used by the command to generate fresh names for automatically provided lemmas used internally. @@ -219,15 +219,16 @@ replace terms with related ones only in contexts that are syntactic compositions of parametric morphism instances declared with the following command. -.. cmd:: Add Parametric Morphism (x1 : T1) ... (xk : Tk) : (f t1 ... tn) with signature sig as @ident +.. cmd:: Add Parametric Morphism @binders : (@ident {+ @term__1}) with signature @term__2 as @ident - This command declares ``f`` as a parametric morphism of signature ``sig``. The - identifier :token:`ident` gives a unique name to the morphism and it is used as - the base name of the typeclass instance definition and as the name of - the lemma that proves the well-definedness of the morphism. The - parameters of the morphism as well as the signature may refer to the - context of variables. The command asks the user to prove interactively - that ``f`` respects the relations identified from the signature. + This command declares a parametric morphism :n:`@ident {+ @term__1}` of + signature :n:`@term__2`. The final identifier :token:`ident` gives a unique + name to the morphism and it is used as the base name of the typeclass + instance definition and as the name of the lemma that proves the + well-definedness of the morphism. The parameters of the morphism as well as + the signature may refer to the context of variables. The command asks the + user to prove interactively that the function denoted by the first + :token:`ident` respects the relations identified from the signature. .. example:: @@ -577,7 +578,7 @@ Deprecated syntax and backward incompatibilities Notice that the syntax is not completely backward compatible since the identifier was not required. -.. cmd:: Add Morphism f : @ident +.. cmd:: Add Morphism @ident : @ident :name: Add Morphism This command is restricted to the declaration of morphisms diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 9219aa21ca..f0c9ba5735 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -311,7 +311,7 @@ Summary of the commands This command has no effect when used on a typeclass. -.. cmd:: Instance @ident {? @binders} : @class t1 … tn {? | priority } := { field1 := b1 ; …; fieldi := bi } +.. cmd:: Instance @ident {? @binders} : @class t1 … tn {? | priority} := { field1 := b1 ; …; fieldi := bi } This command is used to declare a typeclass instance named :token:`ident` of the class :token:`class` with parameters ``t1`` to ``tn`` and @@ -324,11 +324,11 @@ Summary of the commands :tacn:`auto` hints. If the priority is not specified, it defaults to the number of non-dependent binders of the instance. - .. cmdv:: Instance @ident {? @binders} : forall {? @binders}, @class @term__1 … @term__n {? | priority } := @term + .. cmdv:: Instance @ident {? @binders} : forall {? @binders}, @class {+ @term} {? | @priority } := @term This syntax is used for declaration of singleton class instances or for directly giving an explicit term of type :n:`forall @binders, @class - @term__1 … @term__n`. One need not even mention the unique field name for + {+ @term}`. One need not even mention the unique field name for singleton classes. .. cmdv:: Global Instance @@ -356,7 +356,7 @@ Summary of the commands Besides the :cmd:`Class` and :cmd:`Instance` vernacular commands, there are a few other commands related to typeclasses. -.. cmd:: Existing Instance {+ @ident} {? | priority } +.. cmd:: Existing Instance {+ @ident} {? | @priority} This command adds an arbitrary list of constants whose type ends with an applied typeclass to the instance database with an optional @@ -408,7 +408,7 @@ few other commands related to typeclasses. + When considering local hypotheses, we use the union of all the modes declared in the given databases. - .. cmdv:: typeclasses eauto @num + .. tacv:: typeclasses eauto @num .. warning:: The semantics for the limit :n:`@num` @@ -417,7 +417,7 @@ few other commands related to typeclasses. counted, which might result in larger limits being necessary when searching with ``typeclasses eauto`` than with :tacn:`auto`. - .. cmdv:: typeclasses eauto with {+ @ident} + .. tacv:: typeclasses eauto with {+ @ident} This variant runs resolution with the given hint databases. It treats typeclass subgoals the same as other subgoals (no shelving of diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index ccd25ec9f3..96e74bf118 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -831,16 +831,16 @@ Sections create local contexts which can be shared across multiple definitions. Links :token:`type` to each :token:`ident`. - .. cmdv:: Variable {+ ( {+ @ident } : @type ) } + .. cmdv:: Variable {+ ( {+ @ident } : @type ) } Declare one or more variables with various types. - .. cmdv:: Variables {+ ( {+ @ident } : @type) } - Hypothesis {+ ( {+ @ident } : @type) } - Hypotheses {+ ( {+ @ident } : @type) } + .. cmdv:: Variables {+ ( {+ @ident } : @type) } + Hypothesis {+ ( {+ @ident } : @type) } + Hypotheses {+ ( {+ @ident } : @type) } :name: Variables; Hypothesis; Hypotheses - These variants are synonyms of :n:`Variable {+ ( {+ @ident } : @type) }`. + These variants are synonyms of :n:`Variable {+ ( {+ @ident } : @type) }`. .. cmd:: Let @ident := @term diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 5a1af9f9fa..8acbcbec8f 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -616,34 +616,34 @@ has type :token:`type`. Adds several parameters with specification :token:`type`. - .. cmdv:: Parameter {+ ( {+ @ident } : @type ) } + .. cmdv:: Parameter {+ ( {+ @ident } : @type ) } Adds blocks of parameters with different specifications. - .. cmdv:: Local Parameter {+ ( {+ @ident } : @type ) } + .. cmdv:: Local Parameter {+ ( {+ @ident } : @type ) } :name: Local Parameter Such parameters are never made accessible through their unqualified name by :cmd:`Import` and its variants. You have to explicitly give their fully qualified name to refer to them. - .. cmdv:: {? Local } Parameters {+ ( {+ @ident } : @type ) } - {? Local } Axiom {+ ( {+ @ident } : @type ) } - {? Local } Axioms {+ ( {+ @ident } : @type ) } - {? Local } Conjecture {+ ( {+ @ident } : @type ) } - {? Local } Conjectures {+ ( {+ @ident } : @type ) } + .. cmdv:: {? Local } Parameters {+ ( {+ @ident } : @type ) } + {? Local } Axiom {+ ( {+ @ident } : @type ) } + {? Local } Axioms {+ ( {+ @ident } : @type ) } + {? Local } Conjecture {+ ( {+ @ident } : @type ) } + {? Local } Conjectures {+ ( {+ @ident } : @type ) } :name: Parameters; Axiom; Axioms; Conjecture; Conjectures - These variants are synonyms of :n:`{? Local } Parameter {+ ( {+ @ident } : @type ) }`. + These variants are synonyms of :n:`{? Local } Parameter {+ ( {+ @ident } : @type ) }`. - .. cmdv:: Variable {+ ( {+ @ident } : @type ) } - Variables {+ ( {+ @ident } : @type ) } - Hypothesis {+ ( {+ @ident } : @type ) } - Hypotheses {+ ( {+ @ident } : @type ) } + .. cmdv:: Variable {+ ( {+ @ident } : @type ) } + Variables {+ ( {+ @ident } : @type ) } + Hypothesis {+ ( {+ @ident } : @type ) } + Hypotheses {+ ( {+ @ident } : @type ) } :name: Variable (outside a section); Variables (outside a section); Hypothesis (outside a section); Hypotheses (outside a section) Outside of any section, these variants are synonyms of - :n:`Local Parameter {+ ( {+ @ident } : @type ) }`. + :n:`Local Parameter {+ ( {+ @ident } : @type ) }`. For their meaning inside a section, see :cmd:`Variable` in :ref:`section-mechanism`. diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index a7eb7c2319..bbd7e0ba3d 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -360,7 +360,7 @@ Detecting progress We can check if a tactic made progress with: -.. tacn:: progress expr +.. tacn:: progress @expr :name: progress :n:`@expr` is evaluated to v which must be a tactic value. The tactic value ``v`` @@ -555,7 +555,7 @@ Identity The constant :n:`idtac` is the identity tactic: it leaves any goal unchanged but it appears in the proof script. -.. tacn:: idtac {* message_token} +.. tacn:: idtac {* @message_token} :name: idtac This prints the given tokens. Strings and integers are printed @@ -684,7 +684,7 @@ Timing a tactic that evaluates to a term Tactic expressions that produce terms can be timed with the experimental tactic -.. tacn:: time_constr expr +.. tacn:: time_constr @expr :name: time_constr which evaluates :n:`@expr ()` and displays the time the tactic expression @@ -880,7 +880,7 @@ We can perform pattern matching on goals using the following expression: .. we should provide the full grammar here -.. tacn:: match goal with {+| {+ hyp} |- @cpattern => @expr } | _ => @expr end +.. tacn:: match goal with {+| {+, @context_hyp} |- @cpattern => @expr } | _ => @expr end :name: match goal If each hypothesis pattern :n:`hyp`\ :sub:`1,i`, with i = 1, ..., m\ :sub:`1` is @@ -918,7 +918,7 @@ We can perform pattern matching on goals using the following expression: first), but it possible to reverse this order (oldest first) with the :n:`match reverse goal with` variant. - .. tacv:: multimatch goal with {+| {+ hyp} |- @cpattern => @expr } | _ => @expr end + .. tacv:: multimatch goal with {+| {+, @context_hyp} |- @cpattern => @expr } | _ => @expr end Using :n:`multimatch` instead of :n:`match` will allow subsequent tactics to backtrack into a right-hand side tactic which has backtracking points @@ -929,7 +929,7 @@ We can perform pattern matching on goals using the following expression: The syntax :n:`match [reverse] goal …` is, in fact, a shorthand for :n:`once multimatch [reverse] goal …`. - .. tacv:: lazymatch goal with {+| {+ hyp} |- @cpattern => @expr } | _ => @expr end + .. tacv:: lazymatch goal with {+| {+, @context_hyp} |- @cpattern => @expr } | _ => @expr end Using lazymatch instead of match will perform the same pattern matching procedure but will commit to the first matching branch with the first @@ -1135,33 +1135,33 @@ Defining |Ltac| functions Basically, |Ltac| toplevel definitions are made as follows: -.. cmd:: Ltac @ident {* @ident} := @expr +.. cmd:: {? Local} Ltac @ident {* @ident} := @expr + :name: Ltac This defines a new |Ltac| function that can be used in any tactic script or new |Ltac| toplevel definition. + If preceded by the keyword ``Local``, the tactic definition will not be + exported outside the current module. + .. note:: The preceding definition can equivalently be written: :n:`Ltac @ident := fun {+ @ident} => @expr` - Recursive and mutual recursive function definitions are also possible - with the syntax: - .. cmdv:: Ltac @ident {* @ident} {* with @ident {* @ident}} := @expr - It is also possible to *redefine* an existing user-defined tactic using the syntax: + This syntax allows recursive and mutual recursive function definitions. .. cmdv:: Ltac @qualid {* @ident} ::= @expr + This syntax *redefines* an existing user-defined tactic. + A previous definition of qualid must exist in the environment. The new definition will always be used instead of the old one and it goes across module boundaries. - If preceded by the keyword Local the tactic definition will not be - exported outside the current module. - Printing |Ltac| tactics ~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 139506723e..4a2f9c0db3 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -544,9 +544,9 @@ Requesting information ````. - .. deprecated:: 8.10 + .. deprecated:: 8.10 - Please use a text editor. + Please use a text editor. .. cmdv:: Show Proof :name: Show Proof diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index d6247d1bc5..75e019592f 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -2571,7 +2571,7 @@ destruction of existential assumptions like in the tactic: An alternative use of the ``have`` tactic is to provide the explicit proof term for the intermediate lemma, using tactics of the form: -.. tacv:: have {? @ident } := term +.. tacv:: have {? @ident } := @term This tactic creates a new assumption of type the type of :token:`term`. If the diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 537a40c53c..4297e5a64b 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -1749,7 +1749,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) They combine the effects of the ``with``, ``as``, ``eqn:``, ``using``, and ``in`` clauses. -.. tacn:: case term +.. tacn:: case @term :name: case The tactic :n:`case` is a more basic tactic to perform case analysis without @@ -1982,7 +1982,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) :n:`induction @ident; induction @ident` (or :n:`induction @ident ; destruct @ident` depending on the exact needs). -.. tacv:: double induction num1 num2 +.. tacv:: double induction @num__1 @num__2 This tactic is deprecated and should be replaced by :n:`induction num1; induction num3` where :n:`num3` is the result @@ -2271,11 +2271,11 @@ and an explanation of the underlying technique. :undocumented: .. tacv:: injection @term {? with @bindings_list} as {+ @simple_intropattern} - injection @num as {+ simple_intropattern} - injection as {+ simple_intropattern} - einjection @term {? with @bindings_list} as {+ simple_intropattern} - einjection @num as {+ simple_intropattern} - einjection as {+ simple_intropattern} + injection @num as {+ @simple_intropattern} + injection as {+ @simple_intropattern} + einjection @term {? with @bindings_list} as {+ @simple_intropattern} + einjection @num as {+ @simple_intropattern} + einjection as {+ @simple_intropattern} These variants apply :n:`intros {+ @simple_intropattern}` after the call to :tacn:`injection` or :tacn:`einjection` so that all equalities generated are moved in @@ -2637,7 +2637,7 @@ and an explanation of the underlying technique. is correct at some time of the interactive development of a proof, use the command ``Guarded`` (see Section :ref:`requestinginformation`). -.. tacv:: fix @ident @num with {+ (ident {+ @binder} [{struct @ident}] : @type)} +.. tacv:: fix @ident @num with {+ (@ident {+ @binder} [{struct @ident}] : @type)} This starts a proof by mutual induction. The statements to be simultaneously proved are respectively :g:`forall binder ... binder, type`. @@ -4048,7 +4048,7 @@ Setting implicit automation tactics .. seealso:: :cmd:`Proof` in :ref:`proof-editing-mode`. - .. cmdv:: Proof with tactic using {+ @ident} + .. cmdv:: Proof with @tactic using {+ @ident} Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode` diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 4e4a10f590..26dc4e02cf 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -277,7 +277,7 @@ Requests to the environment :token:`term_pattern` (holes of the pattern are either denoted by `_` or by :n:`?@ident` when non linear patterns are expected). - .. cmdv:: Search { + [-]@term_pattern_string } + .. cmdv:: Search {+ {? -}@term_pattern_string} where :n:`@term_pattern_string` is a term_pattern, a string, or a string followed @@ -289,17 +289,17 @@ Requests to the environment 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 } + .. cmdv:: Search {+ {? -}@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 } + .. cmdv:: Search {+ {? -}@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 + .. cmdv:: @selector: Search {+ {? -}@term_pattern_string} This specifies the goal on which to search hypothesis (see Section :ref:`invocation-of-tactics`). @@ -353,7 +353,7 @@ Requests to the environment This restricts the search to constructions defined in the modules named by the given :n:`qualid` sequence. - .. cmdv:: SearchHead term outside {+ @qualid } + .. cmdv:: SearchHead @term outside {+ @qualid } This restricts the search to constructions not defined in the modules named by the given :n:`qualid` sequence. @@ -443,7 +443,7 @@ Requests to the environment SearchRewrite (_ + _ + _). - .. cmdv:: SearchRewrite term inside {+ @qualid } + .. cmdv:: SearchRewrite @term inside {+ @qualid } This restricts the search to constructions defined in the modules named by the given :n:`qualid` sequence. diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index 418922e9b3..3a12ee288a 100644 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ b/doc/sphinx/user-extensions/proof-schemes.rst @@ -336,29 +336,32 @@ Generation of induction principles with ``Functional`` ``Scheme`` Generation of inversion principles with ``Derive`` ``Inversion`` ----------------------------------------------------------------- -.. cmd:: Derive Inversion @ident with forall (x : T), I t Sort sort +.. cmd:: Derive Inversion @ident with @ident Sort @sort + Derive Inversion @ident with (forall @binders, @ident @term) Sort @sort 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`. - + :tacn:`inversion ... using ...` tactic. The first :token:`ident` is the name + of the generated principle. The second :token:`ident` should be an inductive + predicate, and :token:`binders` the variables occurring in the term + :token:`term`. This command generates the inversion lemma for the sort + :token:`sort` corresponding to the instance :n:`forall @binders, @ident @term`. + 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 +.. cmdv:: Derive Inversion_clear @ident with @ident Sort @sort + Derive Inversion_clear @ident with (forall @binders, @ident @term) Sort @sort When applied, it is equivalent to having inverted the instance with the tactic inversion replaced by the tactic `inversion_clear`. -.. cmdv:: Derive Dependent Inversion @ident with forall (x:T), I t Sort @sort +.. cmdv:: Derive Dependent Inversion @ident with @ident Sort @sort + Derive Dependent Inversion @ident with (forall @binders, @ident @term) Sort @sort When applied, it is equivalent to having inverted the instance with the tactic `dependent inversion`. -.. cmdv:: Derive Dependent Inversion_clear @ident with forall(x:T), I t Sort @sort +.. cmdv:: Derive Dependent Inversion_clear @ident with @ident Sort @sort + Derive Dependent Inversion_clear @ident with (forall @binders, @ident @term) Sort @sort When applied, it is equivalent to having inverted the instance with the tactic `dependent inversion_clear`. -- cgit v1.2.3 From b381e8d1c601659ce1a864cc51edece23b1a7fd2 Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Thu, 16 May 2019 10:59:17 -0400 Subject: [refman] Fix up the documentation of Instance and Existing Instance --- doc/sphinx/addendum/type-classes.rst | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index f0c9ba5735..ee417f269d 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -311,23 +311,23 @@ Summary of the commands This command has no effect when used on a typeclass. -.. cmd:: Instance @ident {? @binders} : @class t1 … tn {? | priority} := { field1 := b1 ; …; fieldi := bi } +.. cmd:: Instance @ident {? @binders} : @term__0 {+ @term} {? | @num} := { {*; @field_def} } This command is used to declare a typeclass instance named - :token:`ident` of the class :token:`class` with parameters ``t1`` to ``tn`` and - fields ``b1`` to ``bi``, where each field must be a declared field of + :token:`ident` of the class :n:`@term__0` with parameters :token:`term` and + fields defined by :token:`field_def`, where each field must be a declared field of the class. Missing fields must be filled in interactive proof mode. An arbitrary context of :token:`binders` can be put after the name of the instance and before the colon to declare a parameterized instance. An optional priority can be declared, 0 being the highest priority as for - :tacn:`auto` hints. If the priority is not specified, it defaults to the number + :tacn:`auto` hints. If the priority :token:`num` is not specified, it defaults to the number of non-dependent binders of the instance. - .. cmdv:: Instance @ident {? @binders} : forall {? @binders}, @class {+ @term} {? | @priority } := @term + .. cmdv:: Instance @ident {? @binders} : forall {? @binders}, @term__0 {+ @term} {? | @num } := @term This syntax is used for declaration of singleton class instances or - for directly giving an explicit term of type :n:`forall @binders, @class + for directly giving an explicit term of type :n:`forall @binders, @term__0 {+ @term}`. One need not even mention the unique field name for singleton classes. @@ -356,11 +356,11 @@ Summary of the commands Besides the :cmd:`Class` and :cmd:`Instance` vernacular commands, there are a few other commands related to typeclasses. -.. cmd:: Existing Instance {+ @ident} {? | @priority} +.. cmd:: Existing Instance {+ @ident} {? | @num} This command adds an arbitrary list of constants whose type ends with an applied typeclass to the instance database with an optional - priority. It can be used for redeclaring instances at the end of + priority :token:`num`. It can be used for redeclaring instances at the end of sections, or declaring structure projections as instances. This is equivalent to ``Hint Resolve ident : typeclass_instances``, except it registers instances for :cmd:`Print Instances`. -- cgit v1.2.3 From 2a4bd4861d0ebf0b5d5a63774ac964b431e94fbb Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Thu, 16 May 2019 10:59:33 -0400 Subject: [refman] Add a .. cmd:: header for Reserved Notation and Reserved Infix Co-Authored-By: Théo Zimmermann --- doc/sphinx/user-extensions/syntax-extensions.rst | 31 +++++++++++++++--------- 1 file changed, 19 insertions(+), 12 deletions(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index edec13f681..cda228a7da 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -327,22 +327,29 @@ symbols. Reserving notations ~~~~~~~~~~~~~~~~~~~ -A given notation may be used in different contexts. Coq expects all -uses of the notation to be defined at the same precedence and with the -same associativity. To avoid giving the precedence and associativity -every time, it is possible to declare a parsing rule in advance -without giving its interpretation. Here is an example from the initial -state of Coq. +.. cmd:: Reserved Notation @string {? (@modifiers) } -.. coqtop:: in + A given notation may be used in different contexts. Coq expects all + uses of the notation to be defined at the same precedence and with the + same associativity. To avoid giving the precedence and associativity + every time, this command declares a parsing rule (:token:`string`) in advance + without giving its interpretation. Here is an example from the initial + state of Coq. + + .. coqtop:: in + + Reserved Notation "x = y" (at level 70, no associativity). + + Reserving a notation is also useful for simultaneously defining an + inductive type or a recursive constant and a notation for it. - Reserved Notation "x = y" (at level 70, no associativity). + .. note:: The notations mentioned in the module :ref:`init-notations` are reserved. Hence + their precedence and associativity cannot be changed. -Reserving a notation is also useful for simultaneously defining an -inductive type or a recursive constant and a notation for it. + .. cmdv:: Reserved Infix "@symbol" {* @modifiers} -.. note:: The notations mentioned in the module :ref:`init-notations` are reserved. Hence - their precedence and associativity cannot be changed. + This command declares an infix parsing rule without giving its + interpretation. Simultaneous definition of terms and notations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -- cgit v1.2.3 From 4a69c594b484cb7e9af28b8ba9608a228e2376f1 Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Thu, 16 May 2019 11:00:05 -0400 Subject: [refman] Fix up the grammar entry for field_def --- doc/sphinx/language/gallina-extensions.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 96e74bf118..5e214f6f7f 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -85,7 +85,7 @@ To build an object of type :token:`ident`, one should provide the constructor .. productionlist:: record_term : {| [`field_def` ; … ; `field_def`] |} - field_def : name [binders] := `record_term` + field_def : `ident` [`binders`] := `term` Alternatively, the following syntax allows creating objects by using named fields, as shown in this grammar. The fields do not have to be in any particular order, nor do they have -- cgit v1.2.3 From 8aeaf2d184f95037021a644cf03e7ae340d8c790 Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Thu, 16 May 2019 11:00:19 -0400 Subject: [refman] Document etransitivity --- doc/sphinx/proof-engine/tactics.rst | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'doc/sphinx') diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 4297e5a64b..4e47621938 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -4400,6 +4400,11 @@ Equality This tactic applies to a goal that has the form :g:`t=u` and transforms it into the two subgoals :n:`t=@term` and :n:`@term=u`. + .. tacv:: etransitivity + + This tactic behaves like :tacn:`transitivity`, using a fresh evar instead of + a concrete :token:`term`. + Equality and inductive sets --------------------------- -- cgit v1.2.3 From a6757b089e1d268517bcba48a9fe33aa47526de2 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 25 Jan 2019 00:06:32 +0100 Subject: Remove Refine Instance Mode option --- doc/sphinx/addendum/type-classes.rst | 15 +-------------- doc/sphinx/changes.rst | 7 +++---- 2 files changed, 4 insertions(+), 18 deletions(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index ee417f269d..65934efaa6 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -316,7 +316,7 @@ Summary of the commands This command is used to declare a typeclass instance named :token:`ident` of the class :n:`@term__0` with parameters :token:`term` and fields defined by :token:`field_def`, where each field must be a declared field of - the class. Missing fields must be filled in interactive proof mode. + the class. An arbitrary context of :token:`binders` can be put after the name of the instance and before the colon to declare a parameterized instance. An @@ -563,19 +563,6 @@ Settings of goals. Setting this option to 1 or 2 turns on :flag:`Typeclasses Debug`; setting this option to 0 turns that option off. -.. flag:: Refine Instance Mode - - .. deprecated:: 8.10 - - This flag allows to switch the behavior of instance declarations made through - the Instance command. - - + When it is off (the default), they fail with an error instead. - - + When it is on, instances that have unsolved holes in - their proof-term silently open the proof mode with the remaining - obligations to prove. - Typeclasses eauto `:=` ~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 5e337bcef0..cc2c43e7dd 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -486,10 +486,9 @@ Other changes in 8.10+beta1 - :cmd:`Declare Instance` now requires an instance name. - The flag :flag:`Refine Instance Mode` has been turned off by default, - meaning that :cmd:`Instance` no longer opens a proof when a body is - provided. The flag has been deprecated and will be removed in the next - version. + The flag `Refine Instance Mode` has been turned off by default, meaning that + :cmd:`Instance` no longer opens a proof when a body is provided. The flag + has been deprecated and will be removed in the next version. (`#9270 `_, and `#9825 `_, -- cgit v1.2.3