diff options
Diffstat (limited to 'doc')
54 files changed, 1151 insertions, 316 deletions
diff --git a/doc/changelog/01-kernel/09867-floats.rst b/doc/changelog/01-kernel/09867-floats.rst new file mode 100644 index 0000000000..56b5fc747a --- /dev/null +++ b/doc/changelog/01-kernel/09867-floats.rst @@ -0,0 +1,13 @@ +- A built-in support of floating-point arithmetic was added, allowing + one to devise efficient reflection tactics involving numerical + computation. Primitive floats are added in the language of terms, + following the binary64 format of the IEEE 754 standard, and the + related operations are implemented for the different reduction + engines of Coq by using the corresponding processor operators in + rounding-to-nearest-even. The properties of these operators are + axiomatized in the theory :g:`Coq.Floats.FloatAxioms` which is part + of the library :g:`Coq.Floats.Floats`. + See Section :ref:`primitive-floats` + (`#9867 <https://github.com/coq/coq/pull/9867>`_, + closes `#8276 <https://github.com/coq/coq/issues/8276>`_, + by Guillaume Bertholon, Erik Martin-Dorel, Pierre Roux). diff --git a/doc/changelog/01-kernel/10664-sections-stack-in-kernel.rst b/doc/changelog/01-kernel/10664-sections-stack-in-kernel.rst new file mode 100644 index 0000000000..bac08d12ea --- /dev/null +++ b/doc/changelog/01-kernel/10664-sections-stack-in-kernel.rst @@ -0,0 +1,6 @@ +- Section data is now part of the kernel. Solves a soundness issue + in interactive mode where global monomorphic universe constraints would be + dropped when forcing a delayed opaque proof inside a polymorphic section. Also + relaxes the nesting criterion for sections, as polymorphic sections can now + appear inside a monomorphic one + (#10664, <https://github.com/coq/coq/pull/10664> by Pierre-Marie Pédrot). diff --git a/doc/changelog/01-kernel/10811-sprop-default-on.rst b/doc/changelog/01-kernel/10811-sprop-default-on.rst new file mode 100644 index 0000000000..349c44c205 --- /dev/null +++ b/doc/changelog/01-kernel/10811-sprop-default-on.rst @@ -0,0 +1,3 @@ +- Using ``SProp`` is now allowed by default, without needing to pass + ``-allow-sprop`` or use :flag:`Allow StrictProp` (`#10811 + <https://github.com/coq/coq/pull/10811>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/02-specification-language/10758-fix-10757.rst b/doc/changelog/02-specification-language/10758-fix-10757.rst new file mode 100644 index 0000000000..4cce26aedc --- /dev/null +++ b/doc/changelog/02-specification-language/10758-fix-10757.rst @@ -0,0 +1,5 @@ +- ``Program Fixpoint`` now uses ``ex`` and ``sig`` to make telescopes + involving ``Prop`` types (`#10758 + <https://github.com/coq/coq/pull/10758>`_, by Gaëtan Gilbert, fixing + `#10757 <https://github.com/coq/coq/issues/10757>`_ reported by + Xavier Leroy). diff --git a/doc/changelog/02-specification-language/10985-about-arguments.rst b/doc/changelog/02-specification-language/10985-about-arguments.rst new file mode 100644 index 0000000000..1e05b0b0fe --- /dev/null +++ b/doc/changelog/02-specification-language/10985-about-arguments.rst @@ -0,0 +1,5 @@ +- The output of the :cmd:`Print` and :cmd:`About` commands has + changed. Arguments meta-data is now displayed as the corresponding + :cmd:`Arguments <Arguments (implicits)>` command instead of the + human-targeted prose used in previous Coq versions. (`#10985 + <https://github.com/coq/coq/pull/10985>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst b/doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst new file mode 100644 index 0000000000..43a748b365 --- /dev/null +++ b/doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst @@ -0,0 +1,3 @@ +- The unsupported attribute error is now an error-by-default warning, + meaning it can be disabled (`#10997 + <https://github.com/coq/coq/pull/10997>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/03-notations/09883-numeral-notations-sorts.rst b/doc/changelog/03-notations/09883-numeral-notations-sorts.rst new file mode 100644 index 0000000000..abc5a516ae --- /dev/null +++ b/doc/changelog/03-notations/09883-numeral-notations-sorts.rst @@ -0,0 +1,4 @@ +- Numeral Notations now support sorts in the input to printing + functions (e.g., numeral notations can be defined for terms + containing things like `@cons Set nat nil`). (`#9883 + <https://github.com/coq/coq/pull/9883>`_, by Jason Gross). diff --git a/doc/changelog/03-notations/10963-simplify-parser.rst b/doc/changelog/03-notations/10963-simplify-parser.rst new file mode 100644 index 0000000000..327a39bdb6 --- /dev/null +++ b/doc/changelog/03-notations/10963-simplify-parser.rst @@ -0,0 +1,6 @@ +- A simplification of parsing rules could cause a slight change of + parsing precedences for the very rare users who defined notations + with `constr` at level strictly between 100 and 200 and used these + notations on the right-hand side of a cast operator (`:`, `:>`, + `:>>`) (`#10963 <https://github.com/coq/coq/pull/10963>`_, by Théo + Zimmermann, simplification initially noticed by Jim Fehrle). diff --git a/doc/changelog/04-tactics/09856-zify.rst b/doc/changelog/04-tactics/09856-zify.rst new file mode 100644 index 0000000000..6b9143c77b --- /dev/null +++ b/doc/changelog/04-tactics/09856-zify.rst @@ -0,0 +1,7 @@ +- Reimplementation of the :tacn:`zify` tactic. The tactic is more efficient and copes with dependent hypotheses. + It can also be extended by redefining the tactic ``zify_post_hook``. + (`#9856 <https://github.com/coq/coq/pull/9856>`_ fixes + `#8898 <https://github.com/coq/coq/issues/8898>`_, + `#7886 <https://github.com/coq/coq/issues/7886>`_, + `#9848 <https://github.com/coq/coq/issues/9848>`_ and + `#5155 <https://github.com/coq/coq/issues/5155>`_, by Frédéric Besson). diff --git a/doc/changelog/04-tactics/10765-micromega-caches.rst b/doc/changelog/04-tactics/10765-micromega-caches.rst new file mode 100644 index 0000000000..12d8f68e63 --- /dev/null +++ b/doc/changelog/04-tactics/10765-micromega-caches.rst @@ -0,0 +1,3 @@ +- Introduction of flags :flag:`Lia Cache`, :flag:`Nia Cache` and :flag:`Nra Cache`. + (see `#10772 <https://github.com/coq/coq/issues/10772>`_ for use case) + (`#10765 <https://github.com/coq/coq/pull/10765>`_ fixes `#10772 <https://github.com/coq/coq/issues/10772>`_ , by Frédéric Besson). diff --git a/doc/changelog/04-tactics/10774-zify-Z_to_N.rst b/doc/changelog/04-tactics/10774-zify-Z_to_N.rst new file mode 100644 index 0000000000..ed46cb101e --- /dev/null +++ b/doc/changelog/04-tactics/10774-zify-Z_to_N.rst @@ -0,0 +1,3 @@ +- The :tacn:`zify` tactic is now aware of `Z.to_N`. + (`#10774 <https://github.com/coq/coq/pull/10774>`_ fixes + `#9162 <https://github.com/coq/coq/issues/9162>`_, by Kazuhiko Sakaguchi). diff --git a/doc/changelog/04-tactics/10966-assert-succeeds-once.rst b/doc/changelog/04-tactics/10966-assert-succeeds-once.rst new file mode 100644 index 0000000000..09bef82c80 --- /dev/null +++ b/doc/changelog/04-tactics/10966-assert-succeeds-once.rst @@ -0,0 +1,11 @@ +- The :tacn:`assert_succeeds` and :tacn:`assert_fails` tactics now + only run their tactic argument once, even if it has multiple + successes. This prevents blow-up and looping from using + multisuccess tactics with :tacn:`assert_succeeds`. (`#10966 + <https://github.com/coq/coq/pull/10966>`_ fixes `#10965 + <https://github.com/coq/coq/issues/10965>`_, by Jason Gross). + +- The :tacn:`assert_succeeds` and :tacn:`assert_fails` tactics now + behave correctly when their tactic fully solves the goal. (`#10966 + <https://github.com/coq/coq/pull/10966>`_ fixes `#9114 + <https://github.com/coq/coq/issues/9114>`_, by Jason Gross). diff --git a/doc/changelog/05-tactic-language/10324-ltac2-ssr-ampersand.rst b/doc/changelog/05-tactic-language/10324-ltac2-ssr-ampersand.rst new file mode 100644 index 0000000000..fba09f5e87 --- /dev/null +++ b/doc/changelog/05-tactic-language/10324-ltac2-ssr-ampersand.rst @@ -0,0 +1,5 @@ +- White spaces are forbidden in the “&ident” syntax for ltac2 references + that are described in :ref:`ltac2_built-in-quotations` + (`#10324 <https://github.com/coq/coq/pull/10324>`_, + fixes `#10088 <https://github.com/coq/coq/issues/10088>`_, + authored by Pierre-Marie Pédrot). diff --git a/doc/changelog/06-ssreflect/10932-void-type-ssr.rst b/doc/changelog/06-ssreflect/10932-void-type-ssr.rst new file mode 100644 index 0000000000..7366ef1190 --- /dev/null +++ b/doc/changelog/06-ssreflect/10932-void-type-ssr.rst @@ -0,0 +1,3 @@ +- Add a :g:`void` notation for the standard library empty type (:g:`Empty_set`) + (`#10932 <https://github.com/coq/coq/pull/10932>`_, by Arthur Azevedo de + Amorim). diff --git a/doc/changelog/07-commands-and-options/10291-typing-flags.rst b/doc/changelog/07-commands-and-options/10291-typing-flags.rst new file mode 100644 index 0000000000..ef7adde801 --- /dev/null +++ b/doc/changelog/07-commands-and-options/10291-typing-flags.rst @@ -0,0 +1,4 @@ +- Adding unsafe commands to enable/disable guard checking, positivity checking + and universes checking (providing a local `-type-in-type`). + See :ref:`controlling-typing-flags`. + (`#10291 <https://github.com/coq/coq/pull/10291>`_ by Simon Boulier). diff --git a/doc/changelog/07-commands-and-options/10336-ambiguous-paths.rst b/doc/changelog/07-commands-and-options/10336-ambiguous-paths.rst deleted file mode 100644 index 151c400b2c..0000000000 --- a/doc/changelog/07-commands-and-options/10336-ambiguous-paths.rst +++ /dev/null @@ -1,5 +0,0 @@ -- Improve the ambiguous paths warning to indicate which path is ambiguous with - new one - (`#10336 <https://github.com/coq/coq/pull/10336>`_, - closes `#3219 <https://github.com/coq/coq/issues/3219>`_, - by Kazuhiko Sakaguchi). diff --git a/doc/changelog/07-commands-and-options/10476-fix-export.rst b/doc/changelog/07-commands-and-options/10476-fix-export.rst new file mode 100644 index 0000000000..ba71e1c337 --- /dev/null +++ b/doc/changelog/07-commands-and-options/10476-fix-export.rst @@ -0,0 +1,5 @@ +- Fix two bugs in `Export`. This can have an impact on the behavior of the + `Import` command on libraries. `Import A` when `A` imports `B` which exports + `C` was importing `C`, whereas `Import` is not transitive. Also, after + `Import A B`, the import of `B` was sometimes incomplete. + (`#10476 <https://github.com/coq/coq/pull/10476>`_, by Maxime Dénès). diff --git a/doc/changelog/07-commands-and-options/10489-print_dependent_evars.rst b/doc/changelog/07-commands-and-options/10489-print_dependent_evars.rst new file mode 100644 index 0000000000..580e808baa --- /dev/null +++ b/doc/changelog/07-commands-and-options/10489-print_dependent_evars.rst @@ -0,0 +1,7 @@ +- Update output generated by :flag:`Printing Dependent Evars Line` flag + used by the Prooftree tool in Proof General. + (`#10489 <https://github.com/coq/coq/pull/10489>`_, + closes `#4504 <https://github.com/coq/coq/issues/4504>`_, + `#10399 <https://github.com/coq/coq/issues/10399>`_ and + `#10400 <https://github.com/coq/coq/issues/10400>`_, + by Jim Fehrle). diff --git a/doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst b/doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst new file mode 100644 index 0000000000..c1df728c5c --- /dev/null +++ b/doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst @@ -0,0 +1,6 @@ +- Optionally highlight the differences between successive proof steps in the + :cmd:`Show Proof` command. Experimental; only available in coqtop + and Proof General for now, may be supported in other IDEs + in the future. + (`#10494 <https://github.com/coq/coq/pull/10494>`_, + by Jim Fehrle). diff --git a/doc/changelog/08-tools/08642-vos-files.rst b/doc/changelog/08-tools/08642-vos-files.rst new file mode 100644 index 0000000000..f612096880 --- /dev/null +++ b/doc/changelog/08-tools/08642-vos-files.rst @@ -0,0 +1,7 @@ +- `coqc` now provides the ability to generate compiled interfaces. + Use `coqc -vos foo.v` to skip all opaque proofs during the + compilation of `foo.v`, and output a file called `foo.vos`. + This feature is experimental. It enables working on a Coq file without the need to + first compile the proofs contained in its dependencies + (`#8642 <https://github.com/coq/coq/pull/8642>`_ by Arthur Charguéraud, review by + Maxime Dénès and Emilio Gallego). diff --git a/doc/changelog/08-tools/10430-extraction-int63.rst b/doc/changelog/08-tools/10430-extraction-int63.rst deleted file mode 100644 index 68ae4591a4..0000000000 --- a/doc/changelog/08-tools/10430-extraction-int63.rst +++ /dev/null @@ -1,5 +0,0 @@ -- Fix extraction to OCaml of primitive machine integers; - see :ref:`primitive-integers` - (`#10430 <https://github.com/coq/coq/pull/10430>`_, - fixes `#10361 <https://github.com/coq/coq/issues/10361>`_, - by Vincent Laporte). diff --git a/doc/changelog/08-tools/10947-coq-makefile-dep.rst b/doc/changelog/08-tools/10947-coq-makefile-dep.rst new file mode 100644 index 0000000000..f620b32cb8 --- /dev/null +++ b/doc/changelog/08-tools/10947-coq-makefile-dep.rst @@ -0,0 +1,5 @@ +- Renamed `VDFILE` from `.coqdeps.d` to `.<CoqMakefile>.d` in the `coq_makefile` + utility, where `<CoqMakefile>` is the name of the output file given by the + `-o` option. In this way two generated makefiles can coexist in the same + directory. + (`#10947 <https://github.com/coq/coq/pull/10947>`_, by Kazuhiko Sakaguchi). diff --git a/doc/changelog/10-standard-library/09772-ordered_type-hint-db.rst b/doc/changelog/10-standard-library/09772-ordered_type-hint-db.rst new file mode 100644 index 0000000000..7babcdb6f1 --- /dev/null +++ b/doc/changelog/10-standard-library/09772-ordered_type-hint-db.rst @@ -0,0 +1,4 @@ +- Moved the `auto` hints of the `OrderedType` module into a new `ordered_type` + database + (`#9772 <https://github.com/coq/coq/pull/9772>`_, + by Vincent Laporte). diff --git a/doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst b/doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst new file mode 100644 index 0000000000..864c4e6a7e --- /dev/null +++ b/doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst @@ -0,0 +1,6 @@ +- New lemmas on :g:`combine`, :g:`filter`, :g:`nodup`, :g:`nth`, and + :g:`nth_error` functions on lists. The lemma :g:`filter_app` was moved to the + :g:`List` module. + + See `#10651 <https://github.com/coq/coq/pull/10651>`_, and + `#10731 <https://github.com/coq/coq/pull/10731>`_, by Oliver Nash. diff --git a/doc/changelog/10-standard-library/10827-dedekind-reals.rst b/doc/changelog/10-standard-library/10827-dedekind-reals.rst new file mode 100644 index 0000000000..5d8467025b --- /dev/null +++ b/doc/changelog/10-standard-library/10827-dedekind-reals.rst @@ -0,0 +1,11 @@ +- New module `Reals.ClassicalDedekindReals` defines Dedekind real numbers + as boolean-values functions along with 3 logical axioms: limited principle + of omniscience, excluded middle of negations and functional extensionality. + The exposed type :g:`R` in module :g:`Reals.Rdefinitions` is those + Dedekind reals, hidden behind an opaque module. + Classical Dedekind reals are a quotient of constructive reals, which allows + to transport many constructive proofs to the classical case. + + See `#10827 <https://github.com/coq/coq/pull/10827>`_, by Vincent Semeria, + based on discussions with Guillaume Melquiond, Bas Spitters and Hugo Herbelin, + code review by Hugo Herbelin. diff --git a/doc/changelog/10-standard-library/10895-master+weak-excluded-middle-de-morgan.rst b/doc/changelog/10-standard-library/10895-master+weak-excluded-middle-de-morgan.rst new file mode 100644 index 0000000000..6e87ff93c7 --- /dev/null +++ b/doc/changelog/10-standard-library/10895-master+weak-excluded-middle-de-morgan.rst @@ -0,0 +1 @@ +- ClassicalFacts: Adding the standard equivalence between weak excluded-middle and the classical instance of De Morgan's law (`#10895 <https://github.com/coq/coq/pull/10895>`_, by Hugo Herbelin). diff --git a/doc/changelog/README.md b/doc/changelog/README.md index 2891eb207e..3e0970a656 100644 --- a/doc/changelog/README.md +++ b/doc/changelog/README.md @@ -7,25 +7,28 @@ otherwise important infrastructure changes, and important bug fixes should get a changelog entry. Compatibility-breaking changes should always get a changelog entry, -which should explain what compatibility-breakage is to expect. +which should explain what compatibility breakage is to expect. Pull requests changing the ML API in significant ways should add an entry in [`dev/doc/changes.md`](../../dev/doc/changes.md). ## How to add an entry? ## -You should create a file in one of the sub-directories. The name of -the file should be `NNNNN-identifier.rst` where `NNNNN` is the number -of the pull request on five digits and `identifier` is whatever you -want. - -This file should use the same format as the reference manual (as it -will be copied in there). You may reference the documentation you just -added with `:ref:`, `:tacn:`, `:cmd:`, `:opt:`, `:token:`, etc. See +Run `./dev/tools/make-changelog.sh`: it will ask you for your PR +number, and to choose among the predefined categories. Afterward, +fill in the automatically generated entry with a short description of +your change (which should describe any compatibility issues in +particular). You may also add a reference to the relevant fixed +issue, and credit reviewers, co-authors, and anyone who helped advance +the PR. + +The format for changelog entries is the same as in the reference +manual. In particular, you may reference the documentation you just +added with `:ref:`, `:tacn:`, `:cmd:`, `:opt:`, `:token:`, etc. See the [documentation of the Sphinx format](../sphinx/README.rst) of the manual for details. -The entry should be written using the following structure: +Here is a summary of the structure of a changelog entry: ``` rst - Description of the changes, with possible link to @@ -35,7 +38,3 @@ The entry should be written using the following structure: [ and `#ISSUE2 <https://github.com/coq/coq/issues/ISSUE2>`_],] by Full Name[, with help / review of Full Name]). ``` - -The description should be kept rather short and the only additional -required meta-information are the link to the pull request and the -full name of the author. diff --git a/doc/plugin_tutorial/tuto0/src/dune b/doc/plugin_tutorial/tuto0/src/dune index 79d561061d..ab9b4dd531 100644 --- a/doc/plugin_tutorial/tuto0/src/dune +++ b/doc/plugin_tutorial/tuto0/src/dune @@ -3,7 +3,4 @@ (public_name coq.plugins.tutorial.p0) (libraries coq.plugins.ltac)) -(rule - (targets g_tuto0.ml) - (deps (:pp-file g_tuto0.mlg) ) - (action (run coqpp %{pp-file}))) +(coq.pp (modules g_tuto0)) diff --git a/doc/plugin_tutorial/tuto1/src/dune b/doc/plugin_tutorial/tuto1/src/dune index cf9c674b14..054d5ecd26 100644 --- a/doc/plugin_tutorial/tuto1/src/dune +++ b/doc/plugin_tutorial/tuto1/src/dune @@ -3,7 +3,4 @@ (public_name coq.plugins.tutorial.p1) (libraries coq.plugins.ltac)) -(rule - (targets g_tuto1.ml) - (deps (:pp-file g_tuto1.mlg) ) - (action (run coqpp %{pp-file}))) +(coq.pp (modules g_tuto1)) diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml index 9dd4700db5..307214089f 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -9,4 +9,4 @@ let edeclare ?hook ~name ~poly ~scope ~kind ~opaque sigma udecl body tyopt imps let declare_definition ~poly name sigma body = let udecl = UState.default_univ_decl in edeclare ~name ~poly ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) - ~kind:Decls.Definition ~opaque:false sigma udecl body None [] + ~kind:Decls.(IsDefinition Definition) ~opaque:false sigma udecl body None [] diff --git a/doc/plugin_tutorial/tuto2/src/dune b/doc/plugin_tutorial/tuto2/src/dune index 68ddd13947..8c4b04b1ae 100644 --- a/doc/plugin_tutorial/tuto2/src/dune +++ b/doc/plugin_tutorial/tuto2/src/dune @@ -3,7 +3,4 @@ (public_name coq.plugins.tutorial.p2) (libraries coq.plugins.ltac)) -(rule - (targets g_tuto2.ml) - (deps (:pp-file g_tuto2.mlg) ) - (action (run coqpp %{pp-file}))) +(coq.pp (modules g_tuto2)) diff --git a/doc/plugin_tutorial/tuto3/src/dune b/doc/plugin_tutorial/tuto3/src/dune index ba6d8b288f..678dd71328 100644 --- a/doc/plugin_tutorial/tuto3/src/dune +++ b/doc/plugin_tutorial/tuto3/src/dune @@ -4,7 +4,4 @@ (flags :standard -warn-error -3) (libraries coq.plugins.ltac)) -(rule - (targets g_tuto3.ml) - (deps (:pp-file g_tuto3.mlg)) - (action (run coqpp %{pp-file}))) +(coq.pp (modules g_tuto3)) diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index e56b36caad..4a691bde3a 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -9,9 +9,11 @@ Short description of the tactics -------------------------------- The Psatz module (``Require Import Psatz.``) gives access to several -tactics for solving arithmetic goals over :math:`\mathbb{Z}`, :math:`\mathbb{Q}`, and :math:`\mathbb{R}` [#]_. -It also possible to get the tactics for integers by a ``Require Import Lia``, -rationals ``Require Import Lqa`` and reals ``Require Import Lra``. +tactics for solving arithmetic goals over :math:`\mathbb{Q}`, +:math:`\mathbb{R}`, and :math:`\mathbb{Z}` but also :g:`nat` and +:g:`N`. It also possible to get the tactics for integers by a +``Require Import Lia``, rationals ``Require Import Lqa`` and reals +``Require Import Lra``. + :tacn:`lia` is a decision procedure for linear integer arithmetic; + :tacn:`nia` is an incomplete proof procedure for integer non-linear @@ -23,7 +25,7 @@ rationals ``Require Import Lqa`` and reals ``Require Import Lra``. ``n`` is an optional integer limiting the proof search depth, is an incomplete proof procedure for non-linear arithmetic. It is based on John Harrison’s HOL Light - driver to the external prover `csdp` [#]_. Note that the `csdp` driver is + driver to the external prover `csdp` [#csdp]_. Note that the `csdp` driver is generating a *proof cache* which makes it possible to rerun scripts even without `csdp`. @@ -33,6 +35,18 @@ rationals ``Require Import Lqa`` and reals ``Require Import Lra``. use the Simplex method for solving linear goals. If it is not set, the decision procedures are using Fourier elimination. +.. flag:: Lia Cache + + This option (set by default) instructs :tacn:`lia` to cache its results in the file `.lia.cache` + +.. flag:: Nia Cache + + This option (set by default) instructs :tacn:`nia` to cache its results in the file `.nia.cache` + +.. flag:: Nra Cache + + This option (set by default) instructs :tacn:`nra` to cache its results in the file `.nra.cache` + The tactics solve propositional formulas parameterized by atomic arithmetic expressions interpreted over a domain :math:`D \in \{\mathbb{Z},\mathbb{Q},\mathbb{R}\}`. @@ -78,7 +92,7 @@ closed under the following rules: \end{array}` The following theorem provides a proof principle for checking that a -set of polynomial inequalities does not have solutions [#]_. +set of polynomial inequalities does not have solutions [#fnpsatz]_. .. _psatz_thm: @@ -111,32 +125,21 @@ and checked to be :math:`-1`. The deductive power of :tacn:`lra` overlaps with the one of :tacn:`field` tactic *e.g.*, :math:`x = 10 * x / 10` is solved by :tacn:`lra`. - `lia`: a tactic for linear integer arithmetic --------------------------------------------- .. tacn:: lia :name: lia - This tactic offers an alternative to the :tacn:`omega` tactic. Roughly - speaking, the deductive power of lia is the combined deductive power of - :tacn:`ring_simplify` and :tacn:`omega`. However, it solves linear goals - that :tacn:`omega` does not solve, such as the following so-called *omega - nightmare* :cite:`TheOmegaPaper`. + This tactic solves linear goals over :g:`Z` by searching for *linear* refutations and cutting planes. + :tacn:`lia` provides support for :g:`Z`, :g:`nat`, :g:`positive` and :g:`N` by pre-processing via the :tacn:`zify` tactic. -.. coqdoc:: - - Goal forall x y, - 27 <= 11 * x + 13 * y <= 45 -> - -10 <= 7 * x - 9 * y <= 4 -> False. - -The estimation of the relative efficiency of :tacn:`lia` *vs* :tacn:`omega` is under evaluation. High level view of `lia` ~~~~~~~~~~~~~~~~~~~~~~~~ Over :math:`\mathbb{R}`, *positivstellensatz* refutations are a complete proof -principle [#]_. However, this is not the case over :math:`\mathbb{Z}`. Actually, +principle [#mayfail]_. However, this is not the case over :math:`\mathbb{Z}`. Actually, *positivstellensatz* refutations are not even sufficient to decide linear *integer* arithmetic. The canonical example is :math:`2 * x = 1 -> \mathtt{False}` which is a theorem of :math:`\mathbb{Z}` but not a theorem of :math:`{\mathbb{R}}`. To remedy this @@ -249,21 +252,55 @@ cone expression :math:`2 \times (x-1) + (\mathbf{x-1}) \times (\mathbf{x−1}) + belongs to :math:`\mathit{Cone}({−x^2,x -1})`. Moreover, by running :tacn:`ring` we obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid. -.. [#] Support for :g:`nat` and :g:`N` is obtained by pre-processing the goal with - the ``zify`` tactic. -.. [#] Support for :g:`Z.div` and :g:`Z.modulo` may be obtained by - pre-processing the goal with the ``Z.div_mod_to_equations`` tactic (you may - need to manually run ``zify`` first). -.. [#] Support for :g:`Z.quot` and :g:`Z.rem` may be obtained by pre-processing - the goal with the ``Z.quot_rem_to_equations`` tactic (you may need to manually - run ``zify`` first). -.. [#] Note that support for :g:`Z.div`, :g:`Z.modulo`, :g:`Z.quot`, and - :g:`Z.rem` may be simultaneously obtained by pre-processing the goal with the - ``Z.to_euclidean_division_equations`` tactic (you may need to manually run - ``zify`` first). -.. [#] Sources and binaries can be found at https://projects.coin-or.org/Csdp -.. [#] Variants deal with equalities and strict inequalities. -.. [#] In practice, the oracle might fail to produce such a refutation. +`zify`: pre-processing of arithmetic goals +------------------------------------------ + +.. tacn:: zify + :name: zify + + This tactic is internally called by :tacn:`lia` to support additional types e.g., :g:`nat`, :g:`positive` and :g:`N`. + By requiring the module ``ZifyBool``, the boolean type :g:`bool` and some comparison operators are also supported. + :tacn:`zify` can also be extended by rebinding the tactic `Zify.zify_post_hook` that is run immediately after :tacn:`zify`. + + + To support :g:`Z.div` and :g:`Z.modulo`: ``Ltac Zify.zify_post_hook ::= Z.div_mod_to_equations``. + + To support :g:`Z.quot` and :g:`Z.rem`: ``Ltac Zify.zify_post_hook ::= Z.quot_rem_to_equations``. + + To support :g:`Z.div`, :g:`Z.modulo`, :g:`Z.quot`, and :g:`Z.rem`: ``Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations``. + + +.. cmd:: Show Zify InjTyp + :name: Show Zify InjTyp + + This command shows the list of types that can be injected into :g:`Z`. + +.. cmd:: Show Zify BinOp + :name: Show Zify BinOp + + This command shows the list of binary operators processed by :tacn:`zify`. + +.. cmd:: Show Zify BinRel + :name: Show Zify BinRel + + This command shows the list of binary relations processed by :tacn:`zify`. + + +.. cmd:: Show Zify UnOp + :name: Show Zify UnOp + + This command shows the list of unary operators processed by :tacn:`zify`. + +.. cmd:: Show Zify CstOp + :name: Show Zify CstOp + + This command shows the list of constants processed by :tacn:`zify`. + +.. cmd:: Show Zify Spec + :name: Show Zify Spec + + This command shows the list of operators over :g:`Z` that are compiled using their specification e.g., :g:`Z.min`. + +.. [#csdp] Sources and binaries can be found at https://projects.coin-or.org/Csdp +.. [#fnpsatz] Variants deal with equalities and strict inequalities. +.. [#mayfail] In practice, the oracle might fail to produce such a refutation. .. comment in original TeX: .. %% \paragraph{The {\tt sos} tactic} -- where {\tt sos} stands for \emph{sum of squares} -- tries to prove that a diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst index 903ee115c9..cdb7ea834f 100644 --- a/doc/sphinx/addendum/parallel-proof-processing.rst +++ b/doc/sphinx/addendum/parallel-proof-processing.rst @@ -162,7 +162,7 @@ need to process all the proofs of the ``.v`` file. The asynchronous processing of proofs can decouple the generation of a compiled file (like the ``.vo`` one) that can be loaded by ``Require`` from the generation and checking of the proof objects. The ``-quick`` flag can be -passed to ``coqc`` or ``coqtop`` to produce, quickly, ``.vio`` files. +passed to ``coqc`` to produce, quickly, ``.vio`` files. Alternatively, when using a Makefile produced by ``coq_makefile``, the ``quick`` target can be used to compile all files using the ``-quick`` flag. @@ -182,7 +182,7 @@ running ``coqc`` as usual. Alternatively one can turn each ``.vio`` into the corresponding ``.vo``. All .vio files can be processed in parallel, hence this alternative might -be faster. The command ``coqtop -schedule-vio2vo 2 a b c`` can be used to +be faster. The command ``coqc -schedule-vio2vo 2 a b c`` can be used to obtain a good scheduling for two workers to produce ``a.vo``, ``b.vo``, and ``c.vo``. When using a Makefile produced by ``coq_makefile``, the ``vio2vo`` target can be used for that purpose. Variable ``J`` should be set to the number @@ -197,7 +197,7 @@ There is an extra, possibly even faster, alternative: just check the proof tasks stored in ``.vio`` files without producing the ``.vo`` files. This is possibly faster because all the proof tasks are independent, hence one can further partition the job to be done between workers. The -``coqtop -schedule-vio-checking 6 a b c`` command can be used to obtain a +``coqc -schedule-vio-checking 6 a b c`` command can be used to obtain a good scheduling for 6 workers to check all the proof tasks of ``a.vio``, ``b.vio``, and ``c.vio``. Auxiliary files are used to predict how long a proof task will take, assuming it will take the same amount of time it took diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst index 8935ba27e3..9a9ec78edc 100644 --- a/doc/sphinx/addendum/sprop.rst +++ b/doc/sphinx/addendum/sprop.rst @@ -9,15 +9,16 @@ 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 :flag:`Allow StrictProp`. +known as strict propositions). Using :math:`\SProp` may be prevented +by passing ``-disallow-sprop`` to the |Coq| program or using +:flag:`Allow StrictProp`. .. flag:: Allow StrictProp :name: Allow StrictProp Allows using :math:`\SProp` when set and forbids it when unset. The initial value depends on whether you used the command line - ``-allow-sprop``. + ``-disallow-sprop`` and ``-allow-sprop``. .. exn:: SProp not allowed, you need to Set Allow StrictProp or to use the -allow-sprop command-line-flag. :undocumented: diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 7e698bfb66..905068e316 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -147,14 +147,7 @@ Many other commands support the ``Polymorphic`` flag, including: - :cmd:`Section` will locally set the polymorphism flag inside the section. - ``Variables``, ``Context``, ``Universe`` and ``Constraint`` in a section support - polymorphism. This means that the universe variables (and associated - constraints) are discharged polymorphically over definitions that use - them. In other words, two definitions in the section sharing a common - variable will both get parameterized by the universes produced by the - variable declaration. This is in contrast to a “mononorphic” variable - which introduces global universes and constraints, making the two - definitions depend on the *same* global universes associated to the - variable. + polymorphism. See :ref:`universe-polymorphism-in-sections` for more details. - :cmd:`Hint Resolve` and :cmd:`Hint Rewrite` will use the auto/rewrite hint polymorphically, not at a single instance. @@ -375,9 +368,7 @@ to universes and explicitly instantiate polymorphic definitions. as well. Global universe names live in a separate namespace. The command supports the ``Polymorphic`` flag only in sections, meaning the universe quantification will be discharged on each section definition - independently. One cannot mix polymorphic and monomorphic - declarations in the same section. - + independently. .. cmd:: Constraint @universe_constraint Polymorphic Constraint @universe_constraint @@ -510,3 +501,51 @@ underscore or by omitting the annotation to a polymorphic definition. Lemma baz : Type@{outer}. Proof. exact Type@{inner}. Qed. About baz. + +.. _universe-polymorphism-in-sections: + +Universe polymorphism and sections +---------------------------------- + +:cmd:`Variables`, :cmd:`Context`, :cmd:`Universe` and +:cmd:`Constraint` in a section support polymorphism. This means that +the universe variables and their associated constraints are discharged +polymorphically over definitions that use them. In other words, two +definitions in the section sharing a common variable will both get +parameterized by the universes produced by the variable declaration. +This is in contrast to a “mononorphic” variable which introduces +global universes and constraints, making the two definitions depend on +the *same* global universes associated to the variable. + +It is possible to mix universe polymorphism and monomorphism in +sections, except in the following ways: + +- no monomorphic constraint may refer to a polymorphic universe: + + .. coqtop:: all reset + + Section Foo. + + Polymorphic Universe i. + Fail Constraint i = i. + + This includes constraints implictly declared by commands such as + :cmd:`Variable`, which may as a such need to be used with universe + polymorphism activated (locally by attribute or globally by option): + + .. coqtop:: all + + Fail Variable A : (Type@{i} : Type). + Polymorphic Variable A : (Type@{i} : Type). + + (in the above example the anonymous :g:`Type` constrains polymorphic + universe :g:`i` to be strictly smaller.) + +- no monomorphic constant or inductive may be declared if polymorphic + universes or universe constraints are present. + +These restrictions are required in order to produce a sensible result +when closing the section (the requirement on constants and inductives +is stricter than the one on constraints, because constants and +inductives are abstracted by *all* the section's polymorphic universes +and constraints). diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 6ac55e7bf4..80a24b997c 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -198,21 +198,21 @@ 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. +The 61 contributors to this version are 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, David A. Dalrymple, Christian +Doczkal, Maxime Dénès, Andres Erbsen, Jim Fehrle, Emilio Jesus Gallego +Arias, Gaëtan Gilbert, Matěj Grabovský, Simon Gregersen, Jason Gross, +Samuel Gruetter, Hugo Herbelin, Jasper Hugunin, Mirai Ikebuchi, +Chantal Keller, Matej Košík, Sam Pablo Kuper, Vincent Laporte, Olivier +Laurent, Larry Darryl Lee Jr, Nick Lewycky, Yao Li, Yishuai Li, Assia +Mahboubi, Simon Marechal, Erik Martin-Dorel, Thierry Martinez, +Guillaume Melquiond, Kayla Ngan, Karl Palmskog, Pierre-Marie Pédrot, +Clément Pit-Claudel, 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, +Xia Li-yao, 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, @@ -649,6 +649,121 @@ Many bug fixes and documentation improvements, in particular: (in Proof General) `#421 <https://github.com/ProofGeneral/PG/pull/421>`_, by Jim Fehrle). +Changes in 8.10+beta3 +~~~~~~~~~~~~~~~~~~~~~ + +**Kernel** + +- Fix soundness issue with template polymorphism (`#9294 + <https://github.com/coq/coq/issues/9294>`_). + + Declarations of template-polymorphic inductive types ignored the + provenance of the universes they were abstracting on and did not + detect if they should be greater or equal to :math:`\Set` in + general. Previous universes and universes introduced by the inductive + definition could have constraints that prevented their instantiation + with e.g. :math:`\Prop`, resulting in unsound instantiations later. The + implemented fix only allows abstraction over universes introduced by + the inductive declaration, and properly records all their constraints + by making them by default only :math:`>= \Prop`. It is also checked + that a template polymorphic inductive actually is polymorphic on at + least one universe. + + This prevents inductive declarations in sections to be universe + polymorphic over section parameters. For a backward compatible fix, + simply hoist the inductive definition out of the section. + An alternative is to declare the inductive as universe-polymorphic and + cumulative in a universe-polymorphic section: all universes and + constraints will be properly gathered in this case. + See :ref:`Template-polymorphism` for a detailed exposition of the + rules governing template-polymorphic types. + + To help users incrementally fix this issue, a command line option + `-no-template-check` and a global flag :flag:`Template Check` are + available to selectively disable the new check. Use at your own risk. + + (`#9918 <https://github.com/coq/coq/pull/9918>`_, by Matthieu Sozeau + and Maxime Dénès). + +**User messages** + +- Improve the ambiguous paths warning to indicate which path is ambiguous with + new one + (`#10336 <https://github.com/coq/coq/pull/10336>`_, + closes `#3219 <https://github.com/coq/coq/issues/3219>`_, + by Kazuhiko Sakaguchi). + +**Extraction** + +- Fix extraction to OCaml of primitive machine integers; + see :ref:`primitive-integers` + (`#10430 <https://github.com/coq/coq/pull/10430>`_, + fixes `#10361 <https://github.com/coq/coq/issues/10361>`_, + by Vincent Laporte). +- Fix a printing bug of OCaml extraction on dependent record projections, which + produced improper `assert false`. This change makes the OCaml extractor + internally inline record projections by default; thus the monolithic OCaml + extraction (:cmd:`Extraction` and :cmd:`Recursive Extraction`) does not + produce record projection constants anymore except for record projections + explicitly instructed to extract, and records declared in opaque modules + (`#10577 <https://github.com/coq/coq/pull/10577>`_, + fixes `#7348 <https://github.com/coq/coq/issues/7348>`_, + by Kazuhiko Sakaguchi). + +**Standard library** + +- Added ``splitat`` function and lemmas about ``splitat`` and ``uncons`` + (`#9379 <https://github.com/coq/coq/pull/9379>`_, + by Yishuai Li, with help of Konstantinos Kallas, + follow-up of `#8365 <https://github.com/coq/coq/pull/8365>`_, + which added ``uncons`` in 8.10+beta1). + +Changes in 8.10.0 +~~~~~~~~~~~~~~~~~ + +- Micromega tactics (:tacn:`lia`, :tacn:`nia`, etc) are no longer confused by + primitive projections (`#10806 <https://github.com/coq/coq/pull/10806>`_, + fixes `#9512 <https://github.com/coq/coq/issues/9512>`_ + by Vincent Laporte). + +Changes in 8.10.1 +~~~~~~~~~~~~~~~~~ + +A few bug fixes and documentation improvements, in particular: + +**Kernel** + +- Fix proof of False when using |SProp| (incorrect De Bruijn handling + when inferring the relevance mark of a function) (`#10904 + <https://github.com/coq/coq/pull/10904>`_, by Pierre-Marie Pédrot). + +**Tactics** + +- Fix an anomaly when unsolved evar in :cmd:`Add Ring` + (`#10891 <https://github.com/coq/coq/pull/10891>`_, + fixes `#9851 <https://github.com/coq/coq/issues/9851>`_, + by Gaëtan Gilbert). + +**Tactic language** + +- Fix Ltac regression in binding free names in uconstr + (`#10899 <https://github.com/coq/coq/pull/10899>`_, + fixes `#10894 <https://github.com/coq/coq/issues/10894>`_, + by Hugo Herbelin). + +**CoqIDE** + +- Fix handling of unicode input before space + (`#10852 <https://github.com/coq/coq/pull/10852>`_, + fixes `#10842 <https://github.com/coq/coq/issues/10842>`_, + by Arthur Charguéraud). + +**Extraction** + +- Fix custom extraction of inductives to JSON + (`#10897 <https://github.com/coq/coq/pull/10897>`_, + fixes `#4741 <https://github.com/coq/coq/issues/4741>`_, + by Helge Bahmann). Version 8.9 ----------- @@ -894,8 +1009,8 @@ Standard Library and other packages. They are still delimited by `%int` and `%uint`. - Syntax notations for `string`, `ascii`, `Z`, `positive`, `N`, `R`, - and `int31` are no longer available merely by `Require`ing the files - that define the inductives. You must `Import` `Coq.Strings.String.StringSyntax` + and `int31` are no longer available merely by :cmd:`Require`\ing the files + that define the inductives. You must :cmd:`Import` `Coq.Strings.String.StringSyntax` (after `Require` `Coq.Strings.String`), `Coq.Strings.Ascii.AsciiSyntax` (after `Require` `Coq.Strings.Ascii`), `Coq.ZArith.BinIntDef`, `Coq.PArith.BinPosDef`, `Coq.NArith.BinNatDef`, `Coq.Reals.Rdefinitions`, and diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index ef183174d7..6410620b40 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -70,7 +70,7 @@ and function types over these sorts. Formally, we call :math:`\Sort` the set of sorts which is defined by: .. math:: - + \Sort \equiv \{\SProp,\Prop,\Set,\Type(i)\;|\; i~∈ ℕ\} Their properties, such as: :math:`\Prop:\Type(1)`, :math:`\Set:\Type(1)`, and @@ -436,7 +436,7 @@ instance the identity function over a given type :math:`T` can be written this a *reduction* (or a *conversion*) rule we call :math:`β`: .. math:: - + E[Γ] ⊢ ((λx:T.~t)~u)~\triangleright_β~\subst{t}{x}{u} We say that :math:`\subst{t}{x}{u}` is the *β-contraction* of @@ -474,14 +474,14 @@ with its value, that is to expand (or unfold) it into its value. This reduction is called δ-reduction and shows as follows. .. inference:: Delta-Local - + \WFE{\Gamma} (x:=t:T) ∈ Γ -------------- E[Γ] ⊢ x~\triangleright_Δ~t .. inference:: Delta-Global - + \WFE{\Gamma} (c:=t:T) ∈ E -------------- @@ -499,7 +499,7 @@ destroyed, this reduction differs from δ-reduction. It is called ζ-reduction and shows as follows. .. inference:: Zeta - + \WFE{\Gamma} \WTEG{u}{U} \WTE{\Gamma::(x:=u:U)}{t}{T} @@ -533,17 +533,17 @@ for :math:`x` an arbitrary variable name fresh in :math:`t`. .. math:: f ~:~ ∀ x:\Type(2),~\Type(1) - + then .. math:: λ x:\Type(1).~(f~x) ~:~ ∀ x:\Type(1),~\Type(1) - + We could not allow .. math:: λ x:\Type(1).~(f~x) ~\triangleright_η~ f - + because the type of the reduced term :math:`∀ x:\Type(2),~\Type(1)` would not be convertible to the type of the original term :math:`∀ x:\Type(1),~\Type(1)`. @@ -665,7 +665,7 @@ a *subtyping* relation inductively defined by: .. math:: [c_1 : ∀Γ_P' ,∀ T_{1,1}' … T_{1,n_1}' ,~t'~v_{1,1}' … v_{1,m}' ;~…;~ c_k : ∀Γ_P' ,∀ T_{k,1}' … T_{k,n_k}' ,~t'~v_{k,1}' … v_{k,m}' ] - + respectively then .. math:: @@ -695,7 +695,7 @@ a *subtyping* relation inductively defined by: The conversion rule up to subtyping is now exactly: .. inference:: Conv - + E[Γ] ⊢ U : s E[Γ] ⊢ t : T E[Γ] ⊢ T ≤_{βδιζη} U @@ -716,13 +716,13 @@ that :math:`t_0` is :math:`λ x:T.~u_0` then one step of β-head reduction of :m .. math:: λ x_1 :T_1 .~… λ x_k :T_k .~(λ x:T.~u_0~t_1 … t_n ) ~\triangleright~ λ (x_1 :T_1 )…(x_k :T_k ).~(\subst{u_0}{x}{t_1}~t_2 … t_n ) - + Iterating the process of head reduction until the head of the reduced term is no more an abstraction leads to the *β-head normal form* of :math:`t`: .. math:: t \triangleright … \triangleright λ x_1 :T_1 .~…λ x_k :T_k .~(v~u_1 … u_m ) - + where :math:`v` is not an abstraction (nor an application). Note that the head normal form must not be confused with the normal form since some :math:`u_i` can be reducible. Similar notions of head-normal forms involving δ, ι @@ -828,7 +828,7 @@ We have to give the type of constants in a global environment :math:`E` which contains an inductive definition. .. inference:: Ind - + \WFE{Γ} \ind{p}{Γ_I}{Γ_C} ∈ E (a:A)∈Γ_I @@ -836,7 +836,7 @@ contains an inductive definition. E[Γ] ⊢ a : A .. inference:: Constr - + \WFE{Γ} \ind{p}{Γ_I}{Γ_C} ∈ E (c:C)∈Γ_C @@ -917,7 +917,7 @@ condition* for a constant :math:`X` in the following cases: + :math:`T=(X~t_1 … t_n )` and :math:`X` does not occur free in any :math:`t_i` + :math:`T=∀ x:U,~V` and :math:`X` occurs only strictly positively in :math:`U` and the type :math:`V` satisfies the positivity condition for :math:`X`. - + Strict positivity +++++++++++++++++ @@ -931,10 +931,10 @@ cases: strictly positively in type :math:`V` + :math:`T` converts to :math:`(I~a_1 … a_m~t_1 … t_p )` where :math:`I` is the name of an inductive definition of the form - + .. math:: \ind{m}{I:A}{c_1 :∀ p_1 :P_1 ,… ∀p_m :P_m ,~C_1 ;~…;~c_n :∀ p_1 :P_1 ,… ∀p_m :P_m ,~C_n} - + (in particular, it is not mutually defined and it has :math:`m` parameters) and :math:`X` does not occur in any of the :math:`t_i`, and the (instantiated) types of constructor @@ -998,7 +998,7 @@ such that :math:`Γ_I` is :math:`[I_1 :∀ Γ_P ,A_1 ;~…;~I_k :∀ Γ_P ,A_k]` (E[Γ_I ;Γ_P ] ⊢ C_i : s_{q_i} )_{i=1… n} ------------------------------------------ \WF{E;~\ind{p}{Γ_I}{Γ_C}}{} - + provided that the following side conditions hold: @@ -1046,36 +1046,77 @@ between universes for inductive types in the Type hierarchy. exT_intro : forall X:Type, P X -> exType P. +.. example:: Negative occurrence (first example) -.. _Template-polymorphism: + The following inductive definition is rejected because it does not + satisfy the positivity condition: -Template polymorphism -+++++++++++++++++++++ + .. coqtop:: all -Inductive types can be made polymorphic over their arguments -in :math:`\Type`. + Fail Inductive I : Prop := not_I_I (not_I : I -> False) : I. -.. flag:: Auto Template Polymorphism + If we were to accept such definition, we could derive a + contradiction from it (we can test this by disabling the + :flag:`Positivity Checking` flag): - This option, enabled by default, makes every inductive type declared - at level :math:`\Type` (without annotations or hiding it behind a - definition) template polymorphic. + .. coqtop:: none - This can be prevented using the ``notemplate`` attribute. + Unset Positivity Checking. + Inductive I : Prop := not_I_I (not_I : I -> False) : I. + Set Positivity Checking. - An inductive type can be forced to be template polymorphic using the - ``template`` attribute. + .. coqtop:: all - Template polymorphism and universe polymorphism (see Chapter - :ref:`polymorphicuniverses`) are incompatible, so if the later is - enabled it will prevail over automatic template polymorphism and - cause an error when using the ``template`` attribute. + Definition I_not_I : I -> ~ I := fun i => + match i with not_I_I not_I => not_I end. -.. warn:: Automatically declaring @ident as template polymorphic. + .. coqtop:: in - Warning ``auto-template`` can be used to find which types are - implicitly declared template polymorphic by :flag:`Auto Template - Polymorphism`. + Lemma contradiction : False. + Proof. + enough (I /\ ~ I) as [] by contradiction. + split. + - apply not_I_I. + intro. + now apply I_not_I. + - intro. + now apply I_not_I. + Qed. + +.. example:: Negative occurrence (second example) + + Here is another example of an inductive definition which is + rejected because it does not satify the positivity condition: + + .. coqtop:: all + + Fail Inductive Lam := lam (_ : Lam -> Lam). + + Again, if we were to accept it, we could derive a contradiction + (this time through a non-terminating recursive function): + + .. coqtop:: none + + Unset Positivity Checking. + Inductive Lam := lam (_ : Lam -> Lam). + Set Positivity Checking. + + .. coqtop:: all + + Fixpoint infinite_loop l : False := + match l with lam x => infinite_loop (x l) end. + + Check infinite_loop (lam (@id Lam)) : False. + +.. _Template-polymorphism: + +Template polymorphism ++++++++++++++++++++++ + +Inductive types can be made polymorphic over the universes introduced by +their parameters in :math:`\Type`, if the minimal inferred sort of the +inductive declarations either mention some of those parameter universes +or is computed to be :math:`\Prop` or :math:`\Set`. If :math:`A` is an arity of some sort and :math:`s` is a sort, we write :math:`A_{/s}` for the arity obtained from :math:`A` by replacing its sort with :math:`s`. @@ -1117,10 +1158,11 @@ provided that the following side conditions hold: + there are sorts :math:`s_i`, for :math:`1 ≤ i ≤ k` such that, for :math:`Γ_{I'} = [I_1 :∀ Γ_{P'} ,(A_1)_{/s_1} ;~…;~I_k :∀ Γ_{P'} ,(A_k)_{/s_k}]` we have :math:`(E[Γ_{I′} ;Γ_{P′}] ⊢ C_i : s_{q_i})_{i=1… n}` ; - + the sorts :math:`s_i` are such that all eliminations, to - :math:`\Prop`, :math:`\Set` and :math:`\Type(j)`, are allowed - (see Section :ref:`Destructors`). - + + the sorts :math:`s_i` are all introduced by the inductive + declaration and have no universe constraints beside being greater + than or equal to :math:`\Prop`, and such that all + eliminations, to :math:`\Prop`, :math:`\Set` and :math:`\Type(j)`, + are allowed (see Section :ref:`Destructors`). Notice that if :math:`I_j~q_1 … q_r` is typable using the rules **Ind-Const** and @@ -1141,6 +1183,61 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or :math:`C_i~q_1 … q_r` is mapped to the names chosen in the specific instance of :math:`\ind{p}{Γ_I}{Γ_C}`. +.. warning:: + + The restriction that sorts are introduced by the inductive + declaration prevents inductive types declared in sections to be + template-polymorphic on universes introduced previously in the + section: they cannot parameterize over the universes introduced with + section variables that become parameters at section closing time, as + these may be shared with other definitions from the same section + which can impose constraints on them. + +.. flag:: Auto Template Polymorphism + + This option, enabled by default, makes every inductive type declared + at level :math:`\Type` (without annotations or hiding it behind a + definition) template polymorphic if possible. + + This can be prevented using the ``notemplate`` attribute. + +.. warn:: Automatically declaring @ident as template polymorphic. + + Warning ``auto-template`` can be used to find which types are + implicitly declared template polymorphic by :flag:`Auto Template + Polymorphism`. + + An inductive type can be forced to be template polymorphic using the + ``template`` attribute: it should then fulfill the criterion to + be template polymorphic or an error is raised. + +.. exn:: Inductive @ident cannot be made template polymorphic. + + This error is raised when the `#[universes(template)]` attribute is + on but the inductive cannot be made polymorphic on any universe or be + inferred to live in :math:`\Prop` or :math:`\Set`. + + Template polymorphism and universe polymorphism (see Chapter + :ref:`polymorphicuniverses`) are incompatible, so if the later is + enabled it will prevail over automatic template polymorphism and + cause an error when using the ``template`` attribute. + +.. flag:: Template Check + + Unsetting option :flag:`Template Check` disables the check of + locality of the sorts when abstracting the inductive over its + parameters. This is a deprecated and *unsafe* flag that can introduce + inconsistencies, it is only meant to help users incrementally update + code from Coq versions < 8.10 which did not implement this check. + The `Coq89.v` compatibility file sets this flag globally. A global + ``-no-template-check`` command line option is also available. Use at + your own risk. Use of this flag is recorded in the typing flags + associated to a definition but is *not* supported by the |Coq| + checker (`coqchk`). It will appear in :g:`Print Assumptions` and + :g:`About @ident` output involving inductive declarations that were + (potentially unsoundly) assumed to be template polymorphic. + + In practice, the rule **Ind-Family** is used by |Coq| only when all the inductive types of the inductive definition are declared with an arity whose sort is in the Type hierarchy. Then, the polymorphism is over @@ -1154,10 +1251,10 @@ inductive type is set in :math:`\Set` (even in case :math:`\Set` is impredicativ Section The-Calculus-of-Inductive-Construction-with-impredicative-Set_), and otherwise in the Type hierarchy. -Note that the side-condition about allowed elimination sorts in the -rule **Ind-Family** is just to avoid to recompute the allowed elimination -sorts at each instance of a pattern matching (see Section :ref:`Destructors`). As -an example, let us consider the following definition: +Note that the side-condition about allowed elimination sorts in the rule +**Ind-Family** avoids to recompute the allowed elimination sorts at each +instance of a pattern matching (see Section :ref:`Destructors`). As an +example, let us consider the following definition: .. example:: @@ -1320,7 +1417,7 @@ using the syntax: \Match~m~\as~x~\In~I~\_~a~\return~P~\with~ (c_1~x_{11} ... x_{1p_1} ) ⇒ f_1 | … | (c_n~x_{n1} ... x_{np_n} ) ⇒ f_n~\kwend - + The :math:`\as` part can be omitted if either the result type does not depend on :math:`m` (non-dependent elimination) or :math:`m` is a variable (in this case, :math:`m` can occur in :math:`P` where it is considered a bound variable). The :math:`\In` part @@ -1360,7 +1457,7 @@ There is no restriction on the sort of the predicate to be eliminated. ----------------------- [I:∀ x:A,~A′|∀ x:A,~B′] - + .. inference:: Set & Type s_1 ∈ \{\Set,\Type(j)\} @@ -1376,7 +1473,7 @@ is also of sort :math:`\Prop` or is of the morally smaller sort :math:`\SProp`. .. inference:: Prop - + s ∈ \{\SProp,\Prop\} -------------------- [I:\Prop|I→s] @@ -1404,7 +1501,7 @@ the proof of :g:`or A B` is not accepted: Fail Definition choice (A B: Prop) (x:or A B) := match x with or_introl _ _ a => true | or_intror _ _ b => false end. - + From the computational point of view, the structure of the proof of :g:`(or A B)` in this term is needed for computing the boolean value. @@ -1441,7 +1538,7 @@ this type. :math:`\Prop` for which more eliminations are allowed. .. inference:: Prop-extended - + I~\kw{is an empty or singleton definition} s ∈ \Sort ------------------------------------- @@ -1589,7 +1686,7 @@ An ι-redex is a term of the following form: .. math:: \case((c_{p_i}~q_1 … q_r~a_1 … a_m ),P,f_1 |… |f_l ) - + with :math:`c_{p_i}` the :math:`i`-th constructor of the inductive type :math:`I` with :math:`r` parameters. @@ -1636,7 +1733,7 @@ Typing rule The typing rule is the expected one for a fixpoint. .. inference:: Fix - + (E[Γ] ⊢ A_i : s_i )_{i=1… n} (E[Γ;~f_1 :A_1 ;~…;~f_n :A_n ] ⊢ t_i : A_i )_{i=1… n} ------------------------------------------------------- @@ -1749,7 +1846,7 @@ The reduction for fixpoints is: .. math:: (\Fix~f_i \{F\}~a_1 …a_{k_i}) ~\triangleright_ι~ \subst{t_i}{f_k}{\Fix~f_k \{F\}}_{k=1… n} ~a_1 … a_{k_i} - + when :math:`a_{k_i}` starts with a constructor. This last restriction is needed in order to keep strong normalization and corresponds to the reduction for primitive recursive operators. The following reductions are now @@ -1808,11 +1905,11 @@ and :math:`\subst{E}{|Γ|}{|Γ|c}` to mean the parallel substitution {\WF{E;~c:U;~E′;~c′:=λ x:U.~\subst{t}{c}{x}:∀x:U,~\subst{T}{c}{x};~\subst{E″}{c′}{(c′~c)}} {\subst{Γ}{c′}{(c′~c)}}} - + .. math:: \frac{\WF{E;~c:U;~E′;~c′:T;~E″}{Γ}} {\WF{E;~c:U;~E′;~c′:∀ x:U,~\subst{T}{c}{x};~\subst{E″}{c′}{(c′~c)}}{\subst{Γ}{c′}{(c′~c)}}} - + .. math:: \frac{\WF{E;~c:U;~E′;~\ind{p}{Γ_I}{Γ_C};~E″}{Γ}} {\WFTWOLINES{E;~c:U;~E′;~\ind{p+1}{∀ x:U,~\subst{Γ_I}{c}{x}}{∀ x:U,~\subst{Γ_C}{c}{x}};~ @@ -1853,7 +1950,7 @@ One can consequently derive the following property. .. _First-pruning-property: .. inference:: First pruning property: - + \WF{E;~c:U;~E′}{Γ} c~\kw{does not occur in}~E′~\kw{and}~Γ -------------------------------------- @@ -1933,5 +2030,3 @@ impredicative system for sort :math:`\Set` become: s ∈ \{\Type(i)\} ---------------- [I:\Set|I→ s] - - diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index ac75240cfb..cad5e4e67e 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -756,6 +756,7 @@ subdirectories: * **Sets** : Sets (classical, constructive, finite, infinite, power set, etc.) * **FSets** : Specification and implementations of finite sets and finite maps (by lists and by AVL trees) * **Reals** : Axiomatization of real numbers (classical, basic functions, integer part, fractional part, limit, derivative, Cauchy series, power series and results,...) + * **Floats** : Machine implementation of floating-point arithmetic (for the binary64 format) * **Relations** : Relations (definitions and basic results) * **Sorting** : Sorted list (basic definitions and heapsort correctness) * **Strings** : 8-bits characters and strings @@ -768,7 +769,7 @@ are directly accessible with the command ``Require`` (see Section :ref:`compiled-files`). The different modules of the |Coq| standard library are documented -online at http://coq.inria.fr/stdlib. +online at https://coq.inria.fr/stdlib. Peano’s arithmetic (nat) ~~~~~~~~~~~~~~~~~~~~~~~~ @@ -988,6 +989,106 @@ Notation Interpretation Precedence Associativity ``_ :: _`` ``cons`` 60 right ========== ============== ========== ============= +.. _floats_library: + +Floats library +~~~~~~~~~~~~~~ + +The library of primitive floating-point arithmetic can be loaded by +requiring module ``Floats``: + +.. coqtop:: in + + Require Import Floats. + +It exports the module ``PrimFloat`` that provides a primitive type +named ``float``, defined in the kernel (see section :ref:`primitive-floats`), +as well as two variant types ``float_comparison`` and ``float_class``: + + +.. coqtop:: all + + Print float. + Print float_comparison. + Print float_class. + +It then defines the primitive operators below, using the processor +floating-point operators for binary64 in rounding-to-nearest even: + +* ``abs`` +* ``opp`` +* ``sub`` +* ``add`` +* ``mul`` +* ``div`` +* ``sqrt`` +* ``compare`` : compare two floats and return a ``float_comparison`` +* ``classify`` : analyze a float and return a ``float_class`` +* ``of_int63`` : round a primitive integer and convert it into a float +* ``normfr_mantissa`` : take a float in ``[0.5; 1.0)`` and return its mantissa +* ``frshiftexp`` : convert a float to fractional part in ``[0.5; 1.0)`` and integer part +* ``ldshiftexp`` : multiply a float by an integral power of ``2`` +* ``next_up`` : return the next float towards positive infinity +* ``next_down`` : return the next float towards negative infinity + +For special floating-point values, the following constants are also +defined: + +* ``zero`` +* ``neg_zero`` +* ``one`` +* ``two`` +* ``infinity`` +* ``neg_infinity`` +* ``nan`` : Not a Number (assumed to be unique: the "payload" of NaNs is ignored) + +The following table shows the notations available when opening scope +``float_scope``. + +=========== ============== +Notation Interpretation +=========== ============== +``- _`` ``opp`` +``_ - _`` ``sub`` +``_ + _`` ``add`` +``_ * _`` ``mul`` +``_ / _`` ``div`` +``_ == _`` ``eqb`` +``_ < _`` ``ltb`` +``_ <= _`` ``leb`` +``_ ?= _`` ``compare`` +=========== ============== + +Floating-point constants are parsed and pretty-printed as (17-digit) +decimal constants. This ensures that the composition +:math:`\text{parse} \circ \text{print}` amounts to the identity. + +.. example:: + + .. coqtop:: all + + Open Scope float_scope. + Eval compute in 1 + 0.5. + Eval compute in 1 / 0. + Eval compute in 1 / -0. + Eval compute in 0 / 0. + Eval compute in 0 ?= -0. + Eval compute in nan ?= nan. + Eval compute in next_down (-1). + +The primitive operators are specified with respect to their Gallina +counterpart, using the variant type ``spec_float``, and the injection +``Prim2SF``: + +.. coqtop:: all + + Print spec_float. + Check Prim2SF. + Check mul_spec. + +For more details on the available definitions and lemmas, see the +online documentation of the ``Floats`` library. + .. _userscontributions: Users’ contributions diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index dc4f91e66b..54669534c7 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -182,7 +182,7 @@ other arguments are the parameters of the inductive type. recursive (references to the record's name in the type of its field raises an error). To define recursive records, one can use the ``Inductive`` and ``CoInductive`` keywords, resulting in an inductive or co-inductive record. - Definition of mutal inductive or co-inductive records are also allowed, as long + Definition of mutually inductive or co-inductive records are also allowed, as long as all of the types in the block are records. .. note:: Induction schemes are automatically generated for inductive records. @@ -638,7 +638,11 @@ the induction principle to easily reason about the function. than like this: - .. coqtop:: reset all + .. coqtop:: reset none + + Require Import FunInd. + + .. coqtop:: all Function plus (n m : nat) {struct n} : nat := match n with @@ -649,17 +653,22 @@ the induction principle to easily reason about the function. *Limitations* -|term_0| must be built as a *pure pattern matching tree* (:g:`match … with`) +:token:`term` must be built as a *pure pattern matching tree* (:g:`match … with`) with applications only *at the end* of each branch. Function does not support partial application of the function being defined. Thus, the following example cannot be accepted due to the presence of partial application of :g:`wrong` in the body of :g:`wrong`: -.. coqtop:: all +.. coqtop:: none + + Require List. + Import List.ListNotations. + +.. coqtop:: all fail - Fail Function wrong (C:nat) : nat := - List.hd 0 (List.map wrong (C::nil)). + Function wrong (C:nat) : nat := + List.hd 0 (List.map wrong (C::nil)). For now, dependent cases are not treated for non structurally terminating functions. @@ -1406,7 +1415,7 @@ is needed. In this translation, names in the file system are called *physical* paths while |Coq| names are contrastingly called *logical* names. -A logical prefix Lib can be associated to a physical pathpath using +A logical prefix Lib can be associated with a physical path using the command line option ``-Q`` `path` ``Lib``. All subfolders of path are recursively associated to the logical path ``Lib`` extended with the corresponding suffix coming from the physical path. For instance, the @@ -1918,9 +1927,11 @@ Renaming implicit arguments This command is used to redefine the names of implicit arguments. -With the assert flag, ``Arguments`` can be used to assert that a given -object has the expected number of arguments and that these arguments -are named as expected. +.. cmd:: Arguments @qualid {* @name} : assert + :name: Arguments (assert) + + This command is used to assert that a given object has the expected + number of arguments and that these arguments are named as expected. .. example:: (continued) @@ -2400,7 +2411,7 @@ by means of the interactive proof engine. .. _primitive-integers: Primitive Integers --------------------------------- +------------------ The language of terms features 63-bit machine integers as values. The type of such a value is *axiomatized*; it is declared through the following sentence @@ -2453,6 +2464,55 @@ wrapped into the :g:`Uint63.of_int` (resp. :g:`Uint63.of_int64`) constructor on 64-bit (resp. 32-bit) platforms. Currently, this cannot be customized (see the function :g:`Uint63.compile` from the kernel). +.. _primitive-floats: + +Primitive Floats +---------------- + +The language of terms features Binary64 floating-point numbers as values. +The type of such a value is *axiomatized*; it is declared through the +following sentence (excerpt from the :g:`PrimFloat` module): + +.. coqdoc:: + + Primitive float := #float64_type. + +This type is equipped with a few operators, that must be similarly declared. +For instance, the product of two primitive floats can be computed using the +:g:`PrimFloat.mul` function, declared and specified as follows: + +.. coqdoc:: + + Primitive mul := #float64_mul. + Notation "x * y" := (mul x y) : float_scope. + + Axiom mul_spec : forall x y, Prim2SF (x * y)%float = SF64mul (Prim2SF x) (Prim2SF y). + +where :g:`Prim2SF` is defined in the :g:`FloatOps` module. + +The set of such operators is described in section :ref:`floats_library`. + +These primitive declarations are regular axioms. As such, they must be trusted, and are listed by the +:g:`Print Assumptions` command. + +The reduction machines (:tacn:`vm_compute`, :tacn:`native_compute`) implement +dedicated, efficient rules to reduce the applications of these primitive +operations, using the floating-point processor operators that are assumed +to comply with the IEEE 754 standard for floating-point arithmetic. + +The extraction of these primitives can be customized similarly to the extraction +of regular axioms (see :ref:`extraction`). Nonetheless, the :g:`ExtrOCamlFloats` +module can be used when extracting to OCaml: it maps the Coq primitives to types +and functions of a :g:`Float64` module. Said OCaml module is not produced by +extraction. Instead, it has to be provided by the user (if they want to compile +or execute the extracted code). For instance, an implementation of this module +can be taken from the kernel of Coq. + +Literal values (of type :g:`Float64.t`) are extracted to literal OCaml +values (of type :g:`float`) written in hexadecimal notation and +wrapped into the :g:`Float64.of_float` constructor, e.g.: +:g:`Float64.of_float (0x1p+0)`. + Bidirectionality hints ---------------------- diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 91dfa34494..dd65d4aeb3 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -111,7 +111,7 @@ Other tokens tokens defined at any given time can vary because the :cmd:`Notation` command can define new tokens. A :cmd:`Require` command may load more notation definitions, while the end of a :cmd:`Section` may remove notations. Some notations - are defined in the basic library (see :ref:`thecoqlibrary`) and are normallly + are defined in the basic library (see :ref:`thecoqlibrary`) and are normally loaded automatically at startup time. Here are the character sequences that Coq directly defines as tokens @@ -395,7 +395,7 @@ stands for :n:`let @ident := fun {+ @binder} => @term in @term’`. Definition by case analysis --------------------------- -Objects of inductive types can be destructurated by a case-analysis +Objects of inductive types can be destructured by a case-analysis construction called *pattern matching* expression. A pattern matching expression is used to analyze the structure of an inductive object and to apply specific treatments accordingly. @@ -572,7 +572,7 @@ The Vernacular assertion : `assertion_keyword` `ident` [`binders`] : `term` . assertion_keyword : Theorem | Lemma : Remark | Fact - : Corollary | Proposition + : Corollary | Property | Proposition : Definition | Example proof : Proof . … Qed . : Proof . … Defined . @@ -778,7 +778,8 @@ Simple inductive types The types of the constructors have to satisfy a *positivity condition* (see Section :ref:`positivity`). This condition ensures the soundness of - the inductive definition. + the inductive definition. The positivity checking can be disabled using + the option :flag:`Positivity Checking` (see :ref:`controlling-typing-flags`). .. exn:: The conclusion of @type is not valid; it must be built from @ident. @@ -1555,6 +1556,11 @@ the following attributes names are recognized: now foo. Abort. +.. warn:: Unsupported attribute + + This warning is an error by default. It is caused by using a + command with some attribute it does not understand. + .. [1] This is similar to the expression “*entry* :math:`\{` sep *entry* :math:`\}`” in standard BNF, or “*entry* :math:`(` sep *entry* diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 48d5f4075e..70259ff565 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -184,6 +184,13 @@ and ``coqtop``, unless stated otherwise: :-verbose: Output the content of the input file as it is compiled. This option is available for ``coqc`` only; it is the counterpart of -compile-verbose. +:-vos: Indicate |Coq| to skip the processing of opaque proofs + (i.e., proofs ending with ``Qed`` or ``Admitted``), output a ``.vos`` files + instead of a ``.vo`` file, and to load ``.vos`` files instead of ``.vo`` files + when interpreting ``Require`` commands. +:-vok: Indicate |Coq| to check a file completely, to load ``.vos`` files instead + of ``.vo`` files when interpreting ``Require`` commands, and to output an empty + ``.vok`` files upon success instead of writing a ``.vo`` file. :-w (all|none|w₁,…,wₙ): Configure the display of warnings. This option expects all, none or a comma-separated list of warning names or categories (see Section :ref:`controlling-display`). @@ -245,6 +252,119 @@ and ``coqtop``, unless stated otherwise: currently associated color and exit. :-h, --help: Print a short usage and exit. + + +Compiled interfaces (produced using ``-vos``) +---------------------------------------------- + +Compiled interfaces help saving time while developing Coq formalizations, +by compiling the formal statements exported by a library independently of +the proofs that it contains. + + .. warning:: + + Compiled interfaces should only be used for development purposes. + At the end of the day, one still needs to proof check all files + by producing standard ``.vo`` files. (Technically, when using ``-vos``, + fewer universe constraints are collected.) + Moreover, this feature is still experimental, it may be subject to + change without prior notice. + +**Principle.** + +The compilation using ``coqc -vos foo.v`` produces a file called ``foo.vos``, +which is similar to ``foo.vo`` except that all opaque proofs are skipped in +the compilation process. + +The compilation using ``coqc -vok foo.v`` checks that the file ``foo.v`` +correctly compiles, including all its opaque proofs. If the compilation +succeeds, then the output is a file called ``foo.vok``, with empty contents. +This file is only a placeholder indicating that ``foo.v`` has been successfully +compiled. (This placeholder is useful for build systems such as ``make``.) + +When compiling a file ``bar.v`` that depends on ``foo.v`` (for example via +a ``Require Foo.`` command), if the compilation command is ``coqc -vos bar.v`` +or ``coqc -vok bar.v``, then the file ``foo.vos`` gets loaded (instead of +``foo.vo``). A special case is if file ``foo.vos`` exists and has empty +contents, and ``foo.vo`` exists, then ``foo.vo`` is loaded. + +Appart from the aforementioned case where ``foo.vo`` can be loaded in place +of ``foo.vos``, in general the ``.vos`` and ``.vok`` files live totally +independently from the ``.vo`` files. + +**Dependencies generated by ``coq_makefile``.** + +The files ``foo.vos`` and ``foo.vok`` both depend on ``foo.v``. + +Furthermore, if a file ``foo.v`` requires ``bar.v``, then ``foo.vos`` +and ``foo.vok`` also depend on ``bar.vos``. + +Note, however, that ``foo.vok`` does not depend on ``bar.vok``. +Hence, as detailed further, parallel compilation of proofs is possible. + +In addition, ``coq_makefile`` generates for a file ``foo.v`` a target +``foo.required_vos`` which depends on the list of ``.vos`` files that +``foo.vos`` depends upon (excluding ``foo.vos`` itself). As explained +next, the purpose of this target is to be able to request the minimal +working state for editing interactively the file ``foo.v``. + +**Typical compilation of a set of file using a build system.** + +Assume a file ``foo.v`` that depends on two files ``f1.v`` and ``f2.v``. The +command ``make foo.required_vos`` will compile ``f1.v`` and ``f2.v`` using +the option ``-vos`` to skip the proofs, producing ``f1.vos`` and ``f2.vos``. +At this point, one is ready to work interactively on the file ``foo.v``, even +though it was never needed to compile the proofs involved in the files ``f1.v`` +and ``f2.v``. + +Assume a set of files ``f1.v ... fn.v`` with linear dependencies. The command +``make vos`` enables compiling the statements (i.e. excluding the proofs) in all +the files. Next, ``make -j vok`` enables compiling all the proofs in parallel. +Thus, calling ``make -j vok`` directly enables taking advantage of a maximal +amount of parallelism during the compilation of the set of files. + +Note that this comes at the cost of parsing and typechecking all definitions +twice, once for the ``.vos`` file and once for the ``.vok`` file. However, if +files contain nontrivial proofs, or if the files have many linear chains of +dependencies, or if one has many cores available, compilation should be faster +overall. + +**Need for ``Proof using``** + +When a theorem is part of a section, typechecking the statement of this theorem +might be insufficient for deducing the type of this statement as of at the end +of the section. Indeed, the proof of the theorem could make use of section +variables or section hypotheses that are not mentioned in the statement of the +theorem. + +For this reason, proofs inside section should begin with :cmd:`Proof using` +instead of :cmd:`Proof`, where after the ``using`` clause one should provide +the list of the names of the section variables that are required for the proof +but are not involved in the typechecking of the statement. Note that it is safe +to write ``Proof using.`` instead of ``Proof.`` also for proofs that are not +within a section. + +.. warn:: You should use the “Proof using [...].” syntax instead of “Proof.” to enable skipping this proof which is located inside a section. Give as argument to “Proof using” the list of section variables that are not needed to typecheck the statement but that are required by the proof. + + If |Coq| is invoked using the ``-vos`` option, whenever it finds the + command ``Proof.`` inside a section, it will compile the proof, that is, + refuse to skip it, and it will raise a warning. To disable the warning, one + may pass the flag ``-w -proof-without-using-in-section``. + +**Interaction with standard compilation** + +When compiling a file ``foo.v`` using ``coqc`` in the standard way (i.e., without +``-vos`` nor ``-vok``), an empty file ``foo.vos`` is created in addition to the +regular output file ``foo.vo``. If ``coqc`` is subsequently invoked on some other +file ``bar.v`` using option ``-vos`` or ``-vok``, and that ``bar.v`` requires +``foo.v``, if |Coq| finds an empty file ``foo.vos``, then it will load +``foo.vo`` instead of ``foo.vos``. + +The purpose of this feature is to allow users to benefit from the ``-vos`` +option even if they depend on libraries that were compiled in the traditional +manner (i.e., never compiled using the ``-vos`` option). + + Compiled libraries checker (coqchk) ---------------------------------------- diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index 7d6171285e..b1f392c337 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -179,10 +179,13 @@ compilation, printing, web browsing. In the browser command, you may use `%s` to denote the URL to open, for example: `firefox -remote "OpenURL(%s)"`. -Notice that these settings are saved in the file `.coqiderc` of your -home directory. +Notice that these settings are saved in the file ``coqiderc`` in the +``coq`` subdirectory of the user configuration directory which +is the value of ``$XDG_CONFIG_HOME`` if this environment variable is +set and which otherwise is ``$HOME/.config/``. -A Gtk2 accelerator keymap is saved under the name `.coqide.keys`. It +A GTK+ accelerator keymap is saved under the name ``coqide.keys`` in +the same ``coq`` subdirectory of the user configuration directory. It is not recommended to edit this file manually: to modify a given menu shortcut, go to the corresponding menu item without releasing the mouse button, press the key you want for the new shortcut, and release @@ -259,8 +262,9 @@ Adding custom bindings ~~~~~~~~~~~~~~~~~~~~~~ To extend the default set of bindings, create a file named ``coqide.bindings`` -and place it in the same folder as ``coqide.keys``. On Linux, this would be -the folder ``~/.config/coq``. The file `coqide.bindings` should contain one +and place it in the same folder as ``coqide.keys``. This would be +the folder ``$XDG_CONFIG_HOME/coq``, defaulting to ``~/.config/coq`` +if ``XDG_CONFIG_HOME`` is unset. The file `coqide.bindings` should contain one binding per line, in the form ``\key value``, followed by an optional priority integer. (The key and value should not contain any space character.) diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 554f6bf230..e5edd08995 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -62,7 +62,7 @@ A simple example of a ``_CoqProject`` file follows: theories/foo.v theories/bar.v -I src/ - src/baz.ml4 + src/baz.mlg src/bazaux.ml src/qux_plugin.mlpack @@ -111,7 +111,7 @@ decide how to build them. In particular: + |Coq| files must use the ``.v`` extension + |OCaml| files must use the ``.ml`` or ``.mli`` extension + |OCaml| files that require pre processing for syntax - extensions (like ``VERNAC EXTEND``) must use the ``.ml4`` extension + extensions (like ``VERNAC EXTEND``) must use the ``.mlg`` extension + In order to generate a plugin one has to list all |OCaml| modules (i.e. ``Baz`` for ``baz.ml``) in a ``.mlpack`` file (or ``.mllib`` file). @@ -359,7 +359,7 @@ line timing data: pass ``TIMING=before`` or ``TIMING=after`` rather than ``TIMING=1``. .. note:: - The sorting used here is the same as in the ``print-pretty-timed -diff`` target. + The sorting used here is the same as in the ``print-pretty-timed-diff`` target. .. note:: This target requires python to build the table. @@ -522,10 +522,7 @@ of your project. (flags :standard -warn-error -3-9-27-32-33-50) (libraries coq.plugins.cc coq.plugins.extraction)) - (rule - (targets g_equations.ml) - (deps (:pp-file g_equations.mlg)) - (action (run coqpp %{pp-file}))) + (coq.pp (modules g_equations)) And a Coq-specific part that depends on it via the ``libraries`` field: diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 362c3da6cb..6efc634087 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -368,7 +368,7 @@ We can check if a tactic made progress with: :name: progress :n:`@ltac_expr` is evaluated to v which must be a tactic value. The tactic value ``v`` - is applied to each focued subgoal independently. If the application of ``v`` + is applied to each focused subgoal independently. If the application of ``v`` to one of the focused subgoal produced subgoals equal to the initial goals (up to syntactical equality), then an error of level 0 is raised. @@ -516,7 +516,9 @@ Coq provides a derived tactic to check that a tactic *fails*: .. tacn:: assert_fails @ltac_expr :name: assert_fails - This behaves like :n:`tryif @ltac_expr then fail 0 tac "succeeds" else idtac`. + This behaves like :tacn:`idtac` if :n:`@ltac_expr` fails, and + behaves like :n:`fail 0 @ltac_expr "succeeds"` if :n:`@ltac_expr` + has at least one success. Checking the success ~~~~~~~~~~~~~~~~~~~~ @@ -528,7 +530,7 @@ success: :name: assert_succeeds This behaves like - :n:`tryif (assert_fails tac) then fail 0 tac "fails" else idtac`. + :n:`tryif (assert_fails @ltac_expr) then fail 0 @ltac_expr "fails" else idtac`. Solving ~~~~~~~ diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index c545287fdd..cfdc70d50e 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -427,6 +427,8 @@ In general, quotations can be introduced in terms using the following syntax, wh .. prodn:: ltac2_term += @ident : ( @quotentry ) +.. _ltac2_built-in-quotations: + Built-in quotations +++++++++++++++++++ @@ -439,10 +441,11 @@ The current implementation recognizes the following built-in quotations: 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 +- ``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``. + ``Std.reference``. There shall be no white space between the ampersand + symbol (``&``) and the identifier (:n:`@ident`). The following syntactic sugar is provided for two common cases. @@ -560,6 +563,20 @@ for it. - `&x` as a Coq constr expression expands to `ltac2:(Control.refine (fun () => hyp @x))`. +In the special case where Ltac2 antiquotations appear inside a Coq term +notation, the notation variables are systematically bound in the body +of the tactic expression with type `Ltac2.Init.preterm`. Such a type represents +untyped syntactic Coq expressions, which can by typed in the +current context using the `Ltac2.Constr.pretype` function. + +.. example:: + + The following notation is essentially the identity. + + .. coqtop:: in + + Notation "[ x ]" := ltac2:(let x := Ltac2.Constr.pretype x in exact $x) (only parsing). + Dynamic semantics ***************** @@ -850,6 +867,9 @@ 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`. +.. productionlist:: coq + ltac2_term : ltac1 : ( `ltac_expr` ) + Ltac1 **cannot** implicitly access variables from the Ltac2 scope, but this can be done with an explicit annotation on the :n:`ltac1` quotation. @@ -887,10 +907,19 @@ 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, one 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. +.. productionlist:: coq + ltac_expr : ltac2 : ( `ltac2_term` ) + : ltac2 : ( `ident` ... `ident` |- `ltac2_term` ) + +The typing rules are dual, that is, the optional identifiers are bound +with type `Ltac2.Ltac1.t` in the Ltac2 expression, which is expected to have +type unit. The value returned by this quotation is an Ltac1 function with the +same arity as the number of bound variables. + +Note that when no variables are bound, the inner tactic expression is evaluated +eagerly, if one wants to use it as an argument to a Ltac1 function, one 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 @@ -899,11 +928,17 @@ and won't print anything. .. coqtop:: all - Ltac mytac tac := idtac "wow"; tac. + Ltac mytac tac := idtac "I am being evaluated"; tac. Goal True. Proof. + (* Doesn't print anything *) Fail mytac ltac2:(fail). + (* Prints and fails *) + Fail mytac ltac:(idtac; ltac2:(fail)). + +In any case, the value returned by the fully applied quotation is an +unspecified dummy Ltac1 closure and should not be further used. Transition from Ltac1 --------------------- diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 03b30d5d97..00f8269dc3 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -535,16 +535,20 @@ Requesting information eexists ?[n]. Show n. - .. cmdv:: Show Proof + .. cmdv:: Show Proof {? Diffs {? removed } } :name: Show Proof - It displays the proof term generated by the tactics - that have been applied. If the proof is not completed, this term - contain holes, which correspond to the sub-terms which are still to be - constructed. These holes appear as a question mark indexed by an - integer, and applied to the list of variables in the context, since it - may depend on them. The types obtained by abstracting away the context - from the type of each placeholder are also printed. + Displays the proof term generated by the tactics + that have been applied so far. If the proof is incomplete, the term + will contain holes, which correspond to subterms which are still to be + constructed. Each hole is an existential variable, which appears as a + question mark followed by an identifier. + + Experimental: Specifying “Diffs” highlights the difference between the + current and previous proof step. By default, the command shows the + output once with additions highlighted. Including “removed” shows + the output twice: once showing removals and once showing additions. + It does not examine the :opt:`Diffs` option. See :ref:`showing_diffs`. .. cmdv:: Show Conjectures :name: Show Conjectures @@ -574,9 +578,8 @@ Requesting information .. cmdv:: Show Existentials :name: Show Existentials - It displays the set of all uninstantiated - existential variables in the current proof tree, along with the type - and the context of each variable. + Displays all open goals / existential variables in the current proof + along with the type and the context of each variable. .. cmdv:: Show Match @ident @@ -627,8 +630,11 @@ Showing differences between proof steps --------------------------------------- -Coq can automatically highlight the differences between successive proof steps and between -values in some error messages. +Coq can automatically highlight the differences between successive proof steps +and between values in some error messages. Also, as an experimental feature, +Coq can also highlight differences between proof steps shown in the :cmd:`Show Proof` +command, but only, for now, when using coqtop and Proof General. + For example, the following screenshots of CoqIDE and coqtop show the application of the same :tacn:`intros` tactic. The tactic creates two new hypotheses, highlighted in green. The conclusion is entirely in pale green because although it’s changed, no tokens were added diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index e70f9d7716..04d0503ff4 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -514,7 +514,7 @@ is a valid tactic expression. The pose tactic is also improved for the local definition of higher order terms. Local definitions of functions can use the same syntax as global ones. -For example, the tactic :tacn:`pose <pose (ssreflect)>` supoprts parameters: +For example, the tactic :tacn:`pose <pose (ssreflect)>` supports parameters: .. example:: @@ -684,7 +684,7 @@ conditions: + If this head is a projection of a canonical structure, then canonical structure equations are used for the matching. + If the head of term is *not* a constant, the subterm should have the - same structure (λ abstraction,let…in structure …). + same structure (λ abstraction, let…in structure …). + If the head of :token:`term` is a hole, the subterm should have at least as many arguments as :token:`term`. @@ -1151,7 +1151,7 @@ is basically equivalent to move: a H1 H2; tactic => a H1 H2. -with two differences: the in tactical will preserve the body of a ifa +with two differences: the in tactical will preserve the body of an if a is a defined constant, and if the ``*`` is omitted it will use a temporary abbreviation to hide the statement of the goal from ``tactic``. @@ -1706,7 +1706,7 @@ Intro patterns execution of tactic should thus generate exactly m subgoals, unless the ``[…]`` :token:`i_pattern` comes after an initial ``//`` or ``//=`` :token:`s_item` that closes some of the goals produced by ``tactic``, in - which case exactly m subgoals should remain after thes- item, or we have + which case exactly m subgoals should remain after the :token:`s_item`, or we have the trivial branching :token:`i_pattern` [], which always does nothing, regardless of the number of remaining subgoals. ``[`` :token:`i_item` * ``| … |`` :token:`i_item` * ``]`` @@ -2240,8 +2240,8 @@ then the tactic tactic ; last k [ tactic1 |…| tacticm ] || tacticn. -where natural denotes the integer k as above, applies tactic1 to the n -−k + 1-th goal, … tacticm to the n −k + 2 − m-th goal and tactic n +where natural denotes the integer :math:`k` as above, applies tactic1 to the +:math:`n−k+1`\-th goal, … tacticm to the :math:`n−k+2`\-th goal and tacticn to the others. .. example:: @@ -2631,7 +2631,7 @@ The :token:`i_item` and :token:`s_item` can be used to interpret the asserted hypothesis with views (see section :ref:`views_and_reflection_ssr`) or simplify the resulting goals. -The ``have`` tactic also supports a ``suff`` modifier which allows for +The :tacn:`have` tactic also supports a ``suff`` modifier which allows for asserting that a given statement implies the current goal without copying the goal itself. @@ -2651,7 +2651,7 @@ compatible with the presence of a list of binders. Generating let in context entries with have ``````````````````````````````````````````` -Since |SSR| 1.5 the ``have`` tactic supports a “transparent” modifier +Since |SSR| 1.5 the :tacn:`have` tactic supports a “transparent” modifier to generate let in context entries: the ``@`` symbol in front of the context entry name. @@ -2670,7 +2670,7 @@ context entry name. Lemma test n m (H : m + 1 < n) : True. have @i : 'I_n by apply: (Sub m); omega. -Note that the sub-term produced by ``omega`` is in general huge and +Note that the subterm produced by :tacn:`omega` is in general huge and uninteresting, and hence one may want to hide it. For this purpose the ``[: name ]`` intro pattern and the tactic ``abstract`` (see :ref:`abstract_ssr`) are provided. @@ -2782,7 +2782,7 @@ The ``have`` and ``suff`` tactics are equivalent and have the same syntax but: -+ the order of the generated subgoals is inversed ++ the order of the generated subgoals is inverted + the optional clear item is still performed in the *second* branch. This means that the tactic: @@ -4593,7 +4593,7 @@ The ``elim/`` tactic distinguishes two cases: passed to the eliminator as the last argument (``x`` in ``foo_ind``) and ``en−1 … e1`` are used as patterns to select in the goal the occurrences that will be bound by the predicate ``P``, thus it must be possible to unify - the sub-term of the goal matched by ``en−1`` with ``pm`` , the one matched + the subterm of the goal matched by ``en−1`` with ``pm`` , the one matched by ``en−2`` with ``pm−1`` and so on. :regular eliminator: in all the other cases. Here it must be possible to unify the term matched by ``en`` with ``pm`` , the one matched by @@ -5461,7 +5461,7 @@ equivalences are indeed taken into account, otherwise only single name of an open module. This command returns the list of lemmas: + whose *conclusion* contains a subterm matching the optional first - pattern. A - reverses the test, producing the list of lemmas whose + pattern. A ``-`` reverses the test, producing the list of lemmas whose conclusion does not contain any subterm matching the pattern; + whose name contains the given string. A ``-`` prefix reverses the test, producing the list of lemmas whose name does not contain the string. A diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index fa6d62ffa2..78753fc053 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -157,10 +157,10 @@ The :n:`eqn:` construct in various tactics uses :n:`@naming_intropattern`. Use these elementary patterns to specify a name: -* :n:`@ident` - use the specified name -* :n:`?` - let Coq choose a name -* :n:`?@ident` - generate a name that begins with :n:`@ident` -* :n:`_` - discard the matched part (unless it is required for another +* :n:`@ident` — use the specified name +* :n:`?` — let Coq choose a name +* :n:`?@ident` — generate a name that begins with :n:`@ident` +* :n:`_` — discard the matched part (unless it is required for another hypothesis) * if a disjunction pattern omits a name, such as :g:`[|H2]`, Coq will choose a name @@ -186,7 +186,7 @@ use the :tacn:`split` tactic to replace the current goal with subgoals :g:`A` an For a goal :g:`A \/ B`, use :tacn:`left` to replace the current goal with :g:`A`, or :tacn:`right` to replace the current goal with :g:`B`. -* :n:`( {+, @simple_intropattern}` ) - matches +* :n:`( {+, @simple_intropattern}` ) — matches a product over an inductive type with a :ref:`single constructor <intropattern_cons_note>`. If the number of patterns @@ -196,7 +196,7 @@ For a goal :g:`A \/ B`, use :tacn:`left` to replace the current goal with :g:`A` If the number of patterns equals the number of constructor arguments plus the number of :n:`let-ins`, the patterns are applied to the arguments and :n:`let-in` variables. -* :n:`( {+& @simple_intropattern} )` - matches a right-hand nested term that consists +* :n:`( {+& @simple_intropattern} )` — matches a right-hand nested term that consists of one or more nested binary inductive types such as :g:`a1 OP1 a2 OP2 ...` (where the :g:`OPn` are right-associative). (If the :g:`OPn` are left-associative, additional parentheses will be needed to make the @@ -207,15 +207,15 @@ For a goal :g:`A \/ B`, use :tacn:`left` to replace the current goal with :g:`A` :ref:`single constructor with two parameters <intropattern_cons_note>`. :ref:`Example <intropattern_ampersand_ex>` -* :n:`[ {+| @intropattern_list} ]` - splits an inductive type that has +* :n:`[ {+| @intropattern_list} ]` — splits an inductive type that has :ref:`multiple constructors <intropattern_cons_note>` such as :n:`A \/ B` into multiple subgoals. The number of :token:`intropattern_list` must be the same as the number of constructors for the matched part. -* :n:`[ {+ @intropattern} ]` - splits an inductive type that has a +* :n:`[ {+ @intropattern} ]` — splits an inductive type that has a :ref:`single constructor with multiple parameters <intropattern_cons_note>` such as :n:`A /\ B` into multiple hypotheses. Use :n:`[H1 [H2 H3]]` to match :g:`A /\ B /\ C`. -* :n:`[]` - splits an inductive type: If the inductive +* :n:`[]` — splits an inductive type: If the inductive type has multiple constructors, such as :n:`A \/ B`, create one subgoal for each constructor. If the inductive type has a single constructor with multiple parameters, such as :n:`A /\ B`, split it into multiple hypotheses. @@ -224,14 +224,14 @@ For a goal :g:`A \/ B`, use :tacn:`left` to replace the current goal with :g:`A` These patterns can be used when the hypothesis is an equality: -* :n:`->` - replaces the right-hand side of the hypothesis with the left-hand +* :n:`->` — replaces the right-hand side of the hypothesis with the left-hand side of the hypothesis in the conclusion of the goal; the hypothesis is cleared; if the left-hand side of the hypothesis is a variable, it is substituted everywhere in the context and the variable is removed. :ref:`Example <intropattern_rarrow_ex>` -* :n:`<-` - similar to :n:`->`, but replaces the left-hand side of the hypothesis +* :n:`<-` — similar to :n:`->`, but replaces the left-hand side of the hypothesis with the right-hand side of the hypothesis. -* :n:`[= {*, @intropattern} ]` - If the product is over an equality type, +* :n:`[= {*, @intropattern} ]` — If the product is over an equality type, applies either :tacn:`injection` or :tacn:`discriminate`. If :tacn:`injection` is applicable, the intropattern is used on the hypotheses generated by :tacn:`injection`. If the @@ -241,16 +241,16 @@ These patterns can be used when the hypothesis is an equality: **Other patterns** -* :n:`*` - introduces one or more quantified variables from the result +* :n:`*` — introduces one or more quantified variables from the result until there are no more quantified variables. :ref:`Example <intropattern_star_ex>` -* :n:`**` - introduces one or more quantified variables or hypotheses from the result until there are +* :n:`**` — introduces one or more quantified variables or hypotheses from the result until there are no more quantified variables or implications (:g:`->`). :g:`intros **` is equivalent to :g:`intros`. :ref:`Example <intropattern_2stars_ex>` -* :n:`@simple_intropattern_closed {* % @term}` - first applies each of the terms +* :n:`@simple_intropattern_closed {* % @term}` — first applies each of the terms with the :tacn:`apply ... in` tactic on the hypothesis to be introduced, then it uses :n:`@simple_intropattern_closed`. :ref:`Example <intropattern_injection_ex>` @@ -1409,7 +1409,7 @@ Controlling the proof flow While the different variants of :tacn:`assert` expect that no existential variables are generated by the tactic, :tacn:`eassert` removes this constraint. - This allows not to specify the asserted statement completeley before starting + This lets you avoid specifying the asserted statement completely before starting to prove it. .. tacv:: pose proof @term {? as @simple_intropattern} @@ -1555,8 +1555,8 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`. :name: instantiate The instantiate tactic refines (see :tacn:`refine`) an existential variable - :n:`@ident` with the term :n:`@term`. It is equivalent to only [ident]: - :n:`refine @term` (preferred alternative). + :n:`@ident` with the term :n:`@term`. It is equivalent to + :n:`only [ident]: refine @term` (preferred alternative). .. note:: To be able to refer to an existential variable by name, the user must have given the name explicitly (see :ref:`Existential-Variables`). @@ -2008,7 +2008,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) .. coqtop:: reset all - Lemma le_minus : forall n:nat, n < 1 -> n = 0. + Lemma lt_1_r : forall n:nat, n < 1 -> n = 0. intros n H ; induction H. Here we did not get any information on the indexes to help fulfill @@ -2020,7 +2020,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) .. coqtop:: reset all Require Import Coq.Program.Equality. - Lemma le_minus : forall n:nat, n < 1 -> n = 0. + Lemma lt_1_r : forall n:nat, n < 1 -> n = 0. intros n H ; dependent induction H. The subgoal is cleaned up as the tactic tries to automatically @@ -2691,7 +2691,7 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. This tactic applies to any goal. The type of :token:`term` must have the form - ``forall (x``:sub:`1` ``:A``:sub:`1` ``) ... (x``:sub:`n` ``:A``:sub:`n` ``). eq term``:sub:`1` ``term``:sub:`2` ``.`` + ``forall (x``:sub:`1` ``:A``:sub:`1` ``) ... (x``:sub:`n` ``:A``:sub:`n` ``), eq term``:sub:`1` ``term``:sub:`2` ``.`` where :g:`eq` is the Leibniz equality or a registered setoid equality. @@ -3005,7 +3005,7 @@ the conversion in hypotheses :n:`{+ @ident}`. flags are either ``beta``, ``delta``, ``match``, ``fix``, ``cofix``, ``iota`` or ``zeta``. The ``iota`` flag is a shorthand for ``match``, ``fix`` and ``cofix``. The ``delta`` flag itself can be refined into - :n:`delta {+ @qualid}` or :n:`delta -{+ @qualid}`, restricting in the first + :n:`delta [ {+ @qualid} ]` or :n:`delta - [ {+ @qualid} ]`, restricting in the first case the constants to unfold to the constants listed, and restricting in the second case the constant to unfold to all but the ones explicitly mentioned. Notice that the ``delta`` flag does not apply to variables bound by a let-in @@ -3049,18 +3049,18 @@ the conversion in hypotheses :n:`{+ @ident}`. This is a synonym for ``lazy beta delta iota zeta``. -.. tacv:: compute {+ @qualid} - cbv {+ @qualid} +.. tacv:: compute [ {+ @qualid} ] + cbv [ {+ @qualid} ] These are synonyms of :n:`cbv beta delta {+ @qualid} iota zeta`. -.. tacv:: compute -{+ @qualid} - cbv -{+ @qualid} +.. tacv:: compute - [ {+ @qualid} ] + cbv - [ {+ @qualid} ] These are synonyms of :n:`cbv beta delta -{+ @qualid} iota zeta`. -.. tacv:: lazy {+ @qualid} - lazy -{+ @qualid} +.. tacv:: lazy [ {+ @qualid} ] + lazy - [ {+ @qualid} ] These are respectively synonyms of :n:`lazy beta delta {+ @qualid} iota zeta` and :n:`lazy beta delta -{+ @qualid} iota zeta`. @@ -3071,7 +3071,7 @@ the conversion in hypotheses :n:`{+ @ident}`. This tactic evaluates the goal using the optimized call-by-value evaluation bytecode-based virtual machine described in :cite:`CompiledStrongReduction`. This algorithm is dramatically more efficient than the algorithm used for the - ``cbv`` tactic, but it cannot be fine-tuned. It is specially interesting for + :tacn:`cbv` tactic, but it cannot be fine-tuned. It is especially interesting for full evaluation of algebraic objects. This includes the case of reflection-based tactics. @@ -3080,14 +3080,14 @@ the conversion in hypotheses :n:`{+ @ident}`. This tactic evaluates the goal by compilation to OCaml as described in :cite:`FullReduction`. If Coq is running in native code, it can be - typically two to five times faster than ``vm_compute``. Note however that the + typically two to five times faster than :tacn:`vm_compute`. Note however that the compilation cost is higher, so it is worth using only for intensive computations. .. flag:: NativeCompute Profiling On Linux, if you have the ``perf`` profiler installed, this option makes - it possible to profile ``native_compute`` evaluations. + it possible to profile :tacn:`native_compute` evaluations. .. opt:: NativeCompute Profile Filename @string :name: NativeCompute Profile Filename @@ -3097,7 +3097,7 @@ the conversion in hypotheses :n:`{+ @ident}`. will contain extra characters to avoid overwriting an existing file; that filename is reported to the user. That means you can individually profile multiple uses of - ``native_compute`` in a script. From the Linux command line, run ``perf report`` + :tacn:`native_compute` in a script. From the Linux command line, run ``perf report`` on the profile file to see the results. Consult the ``perf`` documentation for more details. @@ -3153,14 +3153,15 @@ the conversion in hypotheses :n:`{+ @ident}`. use the name of the constant the (co)fixpoint comes from instead of the (co)fixpoint definition in recursive calls. - The ``cbn`` tactic is claimed to be a more principled, faster and more - predictable replacement for ``simpl``. + The :tacn:`cbn` tactic is claimed to be a more principled, faster and more + predictable replacement for :tacn:`simpl`. - The ``cbn`` tactic accepts the same flags as ``cbv`` and ``lazy``. The - behavior of both ``simpl`` and ``cbn`` can be tuned using the - Arguments vernacular command as follows: + The :tacn:`cbn` tactic accepts the same flags as :tacn:`cbv` and + :tacn:`lazy`. The behavior of both :tacn:`simpl` and :tacn:`cbn` + can be tuned using the Arguments vernacular command as follows: - + A constant can be marked to be never unfolded by ``cbn`` or ``simpl``: + + A constant can be marked to be never unfolded by :tacn:`cbn` or + :tacn:`simpl`: .. example:: @@ -3169,7 +3170,7 @@ the conversion in hypotheses :n:`{+ @ident}`. Arguments minus n m : simpl never. After that command an expression like :g:`(minus (S x) y)` is left - untouched by the tactics ``cbn`` and ``simpl``. + untouched by the tactics :tacn:`cbn` and :tacn:`simpl`. + A constant can be marked to be unfolded only if applied to enough arguments. The number of arguments required can be specified using the @@ -3184,7 +3185,7 @@ the conversion in hypotheses :n:`{+ @ident}`. Notation "f \o g" := (fcomp f g) (at level 50). After that command the expression :g:`(f \o g)` is left untouched by - ``simpl`` while :g:`((f \o g) t)` is reduced to :g:`(f (g t))`. + :tacn:`simpl` while :g:`((f \o g) t)` is reduced to :g:`(f (g t))`. The same mechanism can be used to make a constant volatile, i.e. always unfolded. @@ -3206,7 +3207,7 @@ the conversion in hypotheses :n:`{+ @ident}`. Arguments minus !n !m. After that command, the expression :g:`(minus (S x) y)` is left untouched - by ``simpl``, while :g:`(minus (S x) (S y))` is reduced to :g:`(minus x y)`. + by :tacn:`simpl`, while :g:`(minus (S x) (S y))` is reduced to :g:`(minus x y)`. + A special heuristic to determine if a constant has to be unfolded can be activated with the following command: @@ -3222,25 +3223,25 @@ the conversion in hypotheses :n:`{+ @ident}`. :g:`(minus (S (S x)) (S y))` is simplified to :g:`(minus (S x) y)` even if an extra simplification is possible. - In detail, the tactic ``simpl`` first applies :math:`\beta`:math:`\iota`-reduction. Then, it - expands transparent constants and tries to reduce further using :math:`\beta`:math:`\iota`- - reduction. But, when no :math:`\iota` rule is applied after unfolding then - :math:`\delta`-reductions are not applied. For instance trying to use ``simpl`` on + In detail, the tactic :tacn:`simpl` first applies :math:`\beta`:math:`\iota`-reduction. Then, it + expands transparent constants and tries to reduce further using :math:`\beta`:math:`\iota`-reduction. + But, when no :math:`\iota` rule is applied after unfolding then + :math:`\delta`-reductions are not applied. For instance trying to use :tacn:`simpl` on :g:`(plus n O) = n` changes nothing. Notice that only transparent constants whose name can be reused in the - recursive calls are possibly unfolded by ``simpl``. For instance a + recursive calls are possibly unfolded by :tacn:`simpl`. For instance a constant defined by :g:`plus' := plus` is possibly unfolded and reused in the recursive calls, but a constant such as :g:`succ := plus (S O)` is - never unfolded. This is the main difference between ``simpl`` and ``cbn``. - The tactic ``cbn`` reduces whenever it will be able to reuse it or not: + never unfolded. This is the main difference between :tacn:`simpl` and :tacn:`cbn`. + The tactic :tacn:`cbn` reduces whenever it will be able to reuse it or not: :g:`succ t` is reduced to :g:`S t`. -.. tacv:: cbn {+ @qualid} - cbn -{+ @qualid} +.. tacv:: cbn [ {+ @qualid} ] + cbn - [ {+ @qualid} ] - These are respectively synonyms of :n:`cbn beta delta {+ @qualid} iota zeta` - and :n:`cbn beta delta -{+ @qualid} iota zeta` (see :tacn:`cbn`). + These are respectively synonyms of :n:`cbn beta delta [ {+ @qualid} ] iota zeta` + and :n:`cbn beta delta - [ {+ @qualid} ] iota zeta` (see :tacn:`cbn`). .. tacv:: simpl @pattern @@ -3249,7 +3250,7 @@ the conversion in hypotheses :n:`{+ @ident}`. .. tacv:: simpl @pattern at {+ @num} - This applies ``simpl`` only to the :n:`{+ @num}` occurrences of the subterms + This applies :tacn:`simpl` only to the :n:`{+ @num}` occurrences of the subterms matching :n:`@pattern` in the current goal. .. exn:: Too few occurrences. @@ -3265,7 +3266,7 @@ the conversion in hypotheses :n:`{+ @ident}`. .. tacv:: simpl @qualid at {+ @num} simpl @string at {+ @num} - This applies ``simpl`` only to the :n:`{+ @num}` applicative subterms whose + This applies :tacn:`simpl` only to the :n:`{+ @num}` applicative subterms whose head occurrence is :n:`@qualid` (or :n:`@string`). .. flag:: Debug RAKAM @@ -3960,6 +3961,9 @@ At Coq startup, only the core database is nonempty and can be used. :fset: internal database for the implementation of the ``FSets`` library. +:ordered_type: lemmas about ordered types (as defined in the legacy ``OrderedType`` module), + mainly used in the ``FSets`` and ``FMaps`` libraries. + You are advised not to put your own hints in the core database, but use one or several databases specific to your development. @@ -4001,8 +4005,8 @@ use one or several databases specific to your development. This vernacular command adds the terms :n:`{+ @term}` (their types must be equalities) in the rewriting bases :n:`{+ @ident}` with the default orientation - (left to right). Notice that the rewriting bases are distinct from the ``auto`` - hint bases and thatauto does not take them into account. + (left to right). Notice that the rewriting bases are distinct from the :tacn:`auto` + hint bases and that :tacn:`auto` does not take them into account. This command is synchronous with the section mechanism (see :ref:`section-mechanism`): when closing a section, all aliases created by ``Hint Rewrite`` in that @@ -4549,7 +4553,7 @@ Inversion .. tacv:: functional inversion @num - This does the same thing as :n:`intros until @num` folowed by + This does the same thing as :n:`intros until @num` followed by :n:`functional inversion @ident` where :token:`ident` is the identifier for the last introduced hypothesis. @@ -4565,8 +4569,8 @@ Inversion Classical tactics ----------------- -In order to ease the proving process, when the Classical module is -loaded. A few more tactics are available. Make sure to load the module +In order to ease the proving process, when the ``Classical`` module is +loaded, a few more tactics are available. Make sure to load the module using the ``Require Import`` command. .. tacn:: classical_left @@ -4623,7 +4627,7 @@ Automating The tactic :tacn:`omega`, due to Pierre Crégut, is an automatic decision procedure for Presburger arithmetic. It solves quantifier-free - formulas built with `~`, `\/`, `/\`, `->` on top of equalities, + formulas built with `~`, `\\/`, `/\\`, `->` on top of equalities, inequalities and disequalities on both the type :g:`nat` of natural numbers and :g:`Z` of binary integers. This tactic must be loaded by the command ``Require Import Omega``. See the additional documentation about omega diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 774732825a..843459b723 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -627,6 +627,7 @@ file is a particular case of module called *library file*. as ``Export``. .. cmdv:: From @dirpath Require @qualid + :name: From ... Require ... This command acts as :cmd:`Require`, but picks any library whose absolute name is of the form :n:`@dirpath.@dirpath’.@qualid` @@ -1011,8 +1012,9 @@ Controlling display .. flag:: Printing Dependent Evars Line - This option controls the printing of the “(dependent evars: …)” line when - ``-emacs`` is passed. + This option controls the printing of the “(dependent evars: …)” information + after each tactic. The information is used by the Prooftree tool in Proof + General. (https://askra.de/software/prooftree) .. _vernac-controlling-the-reduction-strategies: @@ -1204,6 +1206,79 @@ Controlling the locality of commands occurs in a section. The :cmd:`Set` and :cmd:`Unset` commands belong to this category. +.. _controlling-typing-flags: + +Controlling Typing Flags +---------------------------- + +.. flag:: Guard Checking + + This option can be used to enable/disable the guard checking of + fixpoints. Warning: this can break the consistency of the system, use at your + own risk. Decreasing argument can still be specified: the decrease is not checked + anymore but it still affects the reduction of the term. Unchecked fixpoints are + printed by :cmd:`Print Assumptions`. + +.. flag:: Positivity Checking + + This option can be used to enable/disable the positivity checking of inductive + types and the productivity checking of coinductive types. Warning: this can + break the consistency of the system, use at your own risk. Unchecked + (co)inductive types are printed by :cmd:`Print Assumptions`. + +.. flag:: Universe Checking + + This option can be used to enable/disable the checking of universes, providing a + form of "type in type". Warning: this breaks the consistency of the system, use + at your own risk. Constants relying on "type in type" are printed by + :cmd:`Print Assumptions`. It has the same effect as `-type-in-type` command line + argument (see :ref:`command-line-options`). + +.. cmd:: Print Typing Flags + + Print the status of the three typing flags: guard checking, positivity checking + and universe checking. + +.. example:: + + .. coqtop:: all reset + + Unset Guard Checking. + + Print Typing Flags. + + Fixpoint f (n : nat) : False + := f n. + + Fixpoint ackermann (m n : nat) {struct m} : nat := + match m with + | 0 => S n + | S m => + match n with + | 0 => ackermann m 1 + | S n => ackermann m (ackermann (S m) n) + end + end. + + Print Assumptions ackermann. + + Note that the proper way to define the Ackermann function is to use + an inner fixpoint: + + .. coqtop:: all reset + + Fixpoint ack m := + fix ackm n := + match m with + | 0 => S n + | S m' => + match n with + | 0 => ack m' 1 + | S n' => ack m' (ackm n') + end + end. + + .. _internal-registration-commands: Internal registration commands diff --git a/doc/sphinx/refman-preamble.rst b/doc/sphinx/refman-preamble.rst index c662028773..de95eda989 100644 --- a/doc/sphinx/refman-preamble.rst +++ b/doc/sphinx/refman-preamble.rst @@ -70,7 +70,11 @@ .. |p_i| replace:: `p`\ :math:`_{i}` .. |p_n| replace:: `p`\ :math:`_{n}` .. |Program| replace:: :strong:`Program` +.. |Prop| replace:: :math:`\Prop` +.. |SProp| replace:: :math:`\SProp` +.. |Set| replace:: :math:`\Set` .. |SSR| replace:: :smallcaps:`SSReflect` +.. |Type| replace:: :math:`\Type` .. |t_1| replace:: `t`\ :math:`_{1}` .. |t_i| replace:: `t`\ :math:`_{i}` .. |t_m| replace:: `t`\ :math:`_{m}` diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index fd315c097d..02910e603a 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -267,31 +267,30 @@ The second, more powerful control on printing is by using the format A *format* is an extension of the string denoting the notation with the possible following elements delimited by single quotes: -- extra spaces are translated into simple spaces +- tokens of the form ``'/ '`` are translated into breaking points. If + there is a line break, indents the number of spaces appearing after the + “``/``” (no indentation in the example) -- tokens of the form ``'/ '`` are translated into breaking point, in - case a line break occurs, an indentation of the number of spaces after - the “ ``/``” is applied (2 spaces in the given example) - -- token of the form ``'//'`` force writing on a new line +- tokens of the form ``'//'`` force writing on a new line - well-bracketed pairs of tokens of the form ``'[ '`` and ``']'`` are - translated into printing boxes; in case a line break occurs, an extra - indentation of the number of spaces given after the “ ``[``” is applied - (4 spaces in the example) + translated into printing boxes; if there is a line break, an extra + indentation of the number of spaces after the “``[``” is applied - well-bracketed pairs of tokens of the form ``'[hv '`` and ``']'`` are translated into horizontal-or-else-vertical printing boxes; if the content of the box does not fit on a single line, then every breaking - point forces a newline and an extra indentation of the number of - spaces given after the “ ``[``” is applied at the beginning of each - newline (3 spaces in the example) + point forces a new line and an extra indentation of the number of + spaces after the “``[hv``” is applied at the beginning of each new line - well-bracketed pairs of tokens of the form ``'[v '`` and ``']'`` are translated into vertical printing boxes; every breaking point forces a - newline, even if the line is large enough to display the whole content - of the box, and an extra indentation of the number of spaces given - after the “``[``” is applied at the beginning of each newline + new line, even if the line is large enough to display the whole content + of the box, and an extra indentation of the number of spaces + after the “``[v``” is applied at the beginning of each new line (3 spaces + in the example) + +- extra spaces in other tokens are preserved in the output Notations disappear when a section is closed. No typing of the denoted expression is performed at definition time. Type checking is done only @@ -592,7 +591,7 @@ placeholder being the nesting point. In the innermost occurrence of the nested iterating pattern, the second placeholder is finally filled with the terminating expression. -In the example above, the iterator :math:`φ([~]_E , [~]_I)` is :math:`cons [~]_E [~]_I` +In the example above, the iterator :math:`φ([~]_E , [~]_I)` is :math:`cons [~]_E\, [~]_I` and the terminating expression is ``nil``. Here are other examples: .. coqtop:: in @@ -751,12 +750,12 @@ level is otherwise given explicitly by using the syntax Levels are cumulative: a notation at level ``n`` of which the left end is a term shall use rules at level less than ``n`` to parse this -sub-term. More precisely, it shall use rules at level strictly less +subterm. More precisely, it shall use rules at level strictly less than ``n`` if the rule is declared with ``right associativity`` and rules at level less or equal than ``n`` if the rule is declared with ``left associativity``. Similarly, a notation at level ``n`` of which the right end is a term shall use by default rules at level strictly -less than ``n`` to parse this sub-term if the rule is declared left +less than ``n`` to parse this subterm if the rule is declared left associative and rules at level less or equal than ``n`` if the rule is declared right associative. This is what happens for instance in the rule @@ -1443,8 +1442,8 @@ Numeral notations of the resulting term will be refreshed. Note that only fully-reduced ground terms (terms containing only - function application, constructors, inductive type families, and - primitive integers) will be considered for printing. + function application, constructors, inductive type families, + sorts, and primitive integers) will be considered for printing. .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (warning after @num). @@ -1593,8 +1592,8 @@ String notations of the resulting term will be refreshed. Note that only fully-reduced ground terms (terms containing only - function application, constructors, inductive type families, and - primitive integers) will be considered for printing. + function application, constructors, inductive type families, + sorts, and primitive integers) will be considered for printing. .. exn:: Cannot interpret this string as a value of type @type diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index 6699252cee..a2bc90ffc0 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -13,6 +13,7 @@ plugins/extraction/ExtrHaskellZNum.v plugins/extraction/ExtrOcamlBasic.v plugins/extraction/ExtrOcamlBigIntConv.v plugins/extraction/ExtrOCamlInt63.v +plugins/extraction/ExtrOCamlFloats.v plugins/extraction/ExtrOcamlIntConv.v plugins/extraction/ExtrOcamlNatBigInt.v plugins/extraction/ExtrOcamlNatInt.v @@ -42,6 +43,11 @@ plugins/micromega/Tauto.v plugins/micromega/VarMap.v plugins/micromega/ZCoeff.v plugins/micromega/ZMicromega.v +plugins/micromega/ZifyInst.v +plugins/micromega/ZifyBool.v +plugins/micromega/ZifyComparison.v +plugins/micromega/ZifyClasses.v +plugins/micromega/Zify.v plugins/nsatz/Nsatz.v plugins/omega/Omega.v plugins/omega/OmegaLemmas.v diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 2673d8db82..851510b465 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -68,6 +68,7 @@ through the <tt>Require Import</tt> command.</p> theories/Logic/WKL.v theories/Logic/FinFun.v theories/Logic/PropFacts.v + theories/Logic/HLevels.v </dd> <dt> <b>Structures</b>: @@ -327,6 +328,19 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/Integer/Binary/ZBinary.v theories/Numbers/Integer/NatPairs/ZNatPairs.v </dd> + + <dt> <b> Floats</b>: + Floating-point arithmetic + </dt> + <dd> + theories/Floats/FloatClass.v + theories/Floats/PrimFloat.v + theories/Floats/SpecFloat.v + theories/Floats/FloatOps.v + theories/Floats/FloatAxioms.v + theories/Floats/FloatLemmas.v + (theories/Floats/Floats.v) + </dd> </dl> </dd> @@ -514,9 +528,13 @@ through the <tt>Require Import</tt> command.</p> </dt> <dd> theories/Reals/Rdefinitions.v + theories/Reals/ConstructiveReals.v + theories/Reals/ConstructiveRealsMorphisms.v theories/Reals/ConstructiveCauchyReals.v + theories/Reals/ConstructiveCauchyRealsMult.v + theories/Reals/ClassicalDedekindReals.v theories/Reals/Raxioms.v - theories/Reals/ConstructiveRIneq.v + theories/Reals/ConstructiveRealsLUB.v theories/Reals/RIneq.v theories/Reals/DiscrR.v theories/Reals/ROrderedType.v @@ -624,5 +642,6 @@ through the <tt>Require Import</tt> command.</p> theories/Compat/Coq88.v theories/Compat/Coq89.v theories/Compat/Coq810.v + theories/Compat/Coq811.v </dd> </dl> |