diff options
Diffstat (limited to 'doc')
32 files changed, 557 insertions, 133 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/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/06-ssreflect/10022-ssr-under-setoid.rst b/doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst new file mode 100644 index 0000000000..5e005742fd --- /dev/null +++ b/doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst @@ -0,0 +1,28 @@ +- Generalize tactics :tacn:`under` and :tacn:`over` for any registered + relation. More precisely, assume the given context lemma has type + `forall f1 f2, .. -> (forall i, R1 (f1 i) (f2 i)) -> R2 f1 f2`. The + first step performed by :tacn:`under` (since Coq 8.10) amounts to + calling the tactic :tacn:`rewrite <rewrite (ssreflect)>`, which + itself relies on :tacn:`setoid_rewrite` if need be. So this step was + already compatible with a double implication or setoid equality for + the conclusion head symbol `R2`. But a further step consists in + tagging the generated subgoal `R1 (f1 i) (?f2 i)` to protect it from + unwanted evar instantiation, and get `Under_rel _ R1 (f1 i) (?f2 i)` + that is displayed as ``'Under[ f1 i ]``. In Coq 8.10, this second + (convenience) step was only performed when `R1` was Leibniz' `eq` or + `iff`. Now, it is also performed for any relation `R1` which has a + ``RewriteRelation`` instance (a `RelationClasses.Reflexive` instance + being also needed so :tacn:`over` can discharge the ``'Under[ _ ]`` + goal by instantiating the hidden evar.) Also, it is now possible to + manipulate `Under_rel _ R1 (f1 i) (?f2 i)` subgoals directly if `R1` + is a `PreOrder` relation or so, thanks to extra instances proving + that `Under_rel` preserves the properties of the `R1` relation. + These two features generalizing support for setoid-like relations is + enabled as soon as we do both ``Require Import ssreflect.`` and + ``Require Setoid.`` Finally, a rewrite rule ``UnderE`` has been + added if one wants to "unprotect" the evar, and instantiate it + manually with another rule than reflexivity (i.e., without using the + :tacn:`over` tactic nor the ``over`` rewrite rule). See also Section + :ref:`under_ssr` (`#10022 <https://github.com/coq/coq/pull/10022>`_, + by Erik Martin-Dorel, with suggestions and review by Enrico Tassi + and Cyril Cohen). 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/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index 3dc8707a34..9f92fc4c56 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -127,20 +127,21 @@ Concerning Haskell, type-preserving optimizations are less useful because of laziness. We still make some optimizations, for example in order to produce more readable code. -The type-preserving optimizations are controlled by the following |Coq| options: +The type-preserving optimizations are controlled by the following |Coq| flags +and commands: .. flag:: Extraction Optimize Default is on. This controls all type-preserving optimizations made on the ML terms (mostly reduction of dummy beta/iota redexes, but also - simplifications on Cases, etc). Turn this option off if you want a + simplifications on Cases, etc). Turn this flag off if you want a ML term as close as possible to the Coq term. .. flag:: Extraction Conservative Types Default is off. This controls the non type-preserving optimizations made on ML terms (which try to avoid function abstraction of dummy - types). Turn this option on to make sure that ``e:t`` + types). Turn this flag on to make sure that ``e:t`` implies that ``e':t'`` where ``e'`` and ``t'`` are the extracted code of ``e`` and ``t`` respectively. @@ -150,7 +151,7 @@ The type-preserving optimizations are controlled by the following |Coq| options: produces a singleton type (i.e. a type with only one constructor, and only one argument to this constructor), the inductive structure is removed and this type is seen as an alias to the inner type. - The typical example is ``sig``. This option allows disabling this + The typical example is ``sig``. This flag allows disabling this optimization when one wishes to preserve the inductive structure of types. .. flag:: Extraction AutoInline @@ -159,7 +160,7 @@ The type-preserving optimizations are controlled by the following |Coq| options: some defined constants, according to some heuristics like size of bodies, uselessness of some arguments, etc. Those heuristics are not always perfect; if you want to disable - this feature, turn this option off. + this feature, turn this flag off. .. cmd:: Extraction Inline {+ @qualid } @@ -223,11 +224,11 @@ principles of extraction (logical parts and types). When an actual extraction takes place, an error is normally raised if the :cmd:`Extraction Implicit` declarations cannot be honored, that is if any of the implicit arguments still occurs in the final code. -This behavior can be relaxed via the following option: +This behavior can be relaxed via the following flag: .. flag:: Extraction SafeImplicits - Default is on. When this option is off, a warning is emitted + Default is on. When this flag is off, a warning is emitted instead of an error if some implicit arguments still occur in the final code of an extraction. This way, the extracted code may be obtained nonetheless and reviewed manually to locate the source of the issue diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index 2ea0861e47..93a1be027c 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -714,8 +714,10 @@ Definitions The generalized rewriting tactic is based on a set of strategies that can be combined to obtain custom rewriting procedures. Its set of strategies is based -on Elan’s rewriting strategies :cite:`Luttik97specificationof`. Rewriting -strategies are applied using the tactic :n:`rewrite_strat @strategy` where :token:`strategy` is a +on the programmable rewriting strategies with generic traversals by Visser et al. +:cite:`Luttik97specificationof` :cite:`Visser98`, which formed the core of +the Stratego transformation language :cite:`Visser01`. Rewriting strategies +are applied using the tactic :n:`rewrite_strat @strategy` where :token:`strategy` is a strategy expression. Strategies are defined inductively as described by the following grammar: diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index 7fee62179b..c3b197288f 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -274,7 +274,7 @@ Activating the Printing of Coercions .. flag:: Printing Coercions - When on, this option forces all the coercions to be printed. + When on, this flag forces all the coercions to be printed. By default, coercions are not printed. .. table:: Printing Coercion @qualid diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index 4a691bde3a..cc19c8b6a9 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -31,21 +31,21 @@ tactics for solving arithmetic goals over :math:`\mathbb{Q}`, .. flag:: Simplex - This option (set by default) instructs the decision procedures to + This flag (set by default) instructs the decision procedures to use the Simplex method for solving linear goals. If it is not set, the decision procedures are using Fourier elimination. .. flag:: Lia Cache - This option (set by default) instructs :tacn:`lia` to cache its results in the file `.lia.cache` + This flag (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` + This flag (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` + This flag (set by default) instructs :tacn:`nra` to cache its results in the file `.nra.cache` The tactics solve propositional formulas parameterized by atomic diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst index b008508bbc..650a444a16 100644 --- a/doc/sphinx/addendum/omega.rst +++ b/doc/sphinx/addendum/omega.rst @@ -119,21 +119,21 @@ Options .. deprecated:: 8.5 - This deprecated option (on by default) is for compatibility with Coq pre 8.5. It + This deprecated flag (on by default) is for compatibility with Coq pre 8.5. It resets internal name counters to make executions of :tacn:`omega` independent. .. flag:: Omega UseLocalDefs - This option (on by default) allows :tacn:`omega` to use the bodies of local + This flag (on by default) allows :tacn:`omega` to use the bodies of local variables. .. flag:: Omega System - This option (off by default) activate the printing of debug information + This flag (off by default) activate the printing of debug information .. flag:: Omega Action - This option (off by default) activate the printing of debug information + This flag (off by default) activate the printing of debug information Technical data -------------- diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst index cdb7ea834f..35729d852d 100644 --- a/doc/sphinx/addendum/parallel-proof-processing.rst +++ b/doc/sphinx/addendum/parallel-proof-processing.rst @@ -58,7 +58,7 @@ variables used. Automatic suggestion of proof annotations ````````````````````````````````````````` -The flag :flag:`Suggest Proof Using` makes |Coq| suggest, when a ``Qed`` +The :flag:`Suggest Proof Using` flag makes |Coq| suggest, when a ``Qed`` command is processed, a correct proof annotation. It is up to the user to modify the proof script accordingly. diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 45c74ab02a..a17dca1693 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -78,7 +78,7 @@ operation (see :ref:`extendedpatternmatching`). also works with the previous mechanism. -There are options to control the generation of equalities and +There are flags to control the generation of equalities and coercions. .. flag:: Program Cases @@ -86,13 +86,13 @@ coercions. This controls the special treatment of pattern matching generating equalities and disequalities when using |Program| (it is on by default). All pattern-matches and let-patterns are handled using the standard algorithm - of |Coq| (see :ref:`extendedpatternmatching`) when this option is + of |Coq| (see :ref:`extendedpatternmatching`) when this flag is deactivated. .. flag:: Program Generalized Coercion This controls the coercion of general inductive types when using |Program| - (the option is on by default). Coercion of subset types and pairs is still + (the flag is on by default). Coercion of subset types and pairs is still active in this case. .. flag:: Program Mode @@ -341,9 +341,9 @@ optional tactic is replaced by the default one if not specified. .. flag:: Shrink Obligations - *Deprecated since 8.7* + .. deprecated:: 8.7 - This option (on by default) controls whether obligations should have + This flag (on by default) controls whether obligations should have their context minimized to the set of variables used in the proof of the obligation, to avoid unnecessary dependencies. diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst index 9a9ec78edc..9acdd18b89 100644 --- a/doc/sphinx/addendum/sprop.rst +++ b/doc/sphinx/addendum/sprop.rst @@ -9,9 +9,11 @@ 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). Using :math:`\SProp` may be prevented -by passing ``-disallow-sprop`` to the |Coq| program or using -:flag:`Allow StrictProp`. +known as strict propositions) as described in +:cite:`Gilbert:POPL2019`. + +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 diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index db3e20a9c6..1bbf988505 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -560,8 +560,8 @@ Settings Determines how much information is shown for typeclass resolution steps during search. 1 is the default level. 2 shows additional information such as tried tactics and shelving - of goals. Setting this option to 1 or 2 turns on :flag:`Typeclasses Debug`; setting this - option to 0 turns that option off. + of goals. Setting this option to 1 or 2 turns on the :flag:`Typeclasses Debug` flag; setting this + option to 0 turns that flag off. Typeclasses eauto `:=` ~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 905068e316..7adb25cbd6 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -129,12 +129,12 @@ Polymorphic, Monomorphic .. flag:: Universe Polymorphism - Once enabled, this option will implicitly prepend ``Polymorphic`` to any + Once enabled, this flag will implicitly prepend ``Polymorphic`` to any definition of the user. .. cmd:: Monomorphic @definition - When the :flag:`Universe Polymorphism` option is set, to make a definition + When the :flag:`Universe Polymorphism` flag is set, to make a definition producing global universe constraints, one can use the ``Monomorphic`` prefix. Many other commands support the ``Polymorphic`` flag, including: @@ -162,8 +162,8 @@ declared cumulative using the :g:`Cumulative` prefix. Declares the inductive as cumulative -Alternatively, there is a flag :flag:`Polymorphic Inductive -Cumulativity` which when set, makes all subsequent *polymorphic* +Alternatively, there is a :flag:`Polymorphic Inductive +Cumulativity` flag which when set, makes all subsequent *polymorphic* inductive definitions cumulative. When set, inductive types and the like can be enforced to be non-cumulative using the :g:`NonCumulative` prefix. @@ -174,7 +174,7 @@ prefix. .. flag:: Polymorphic Inductive Cumulativity - When this option is on, it sets all following polymorphic inductive + When this flag is on, it sets all following polymorphic inductive types as cumulative (it is off by default). Consider the examples below. @@ -222,8 +222,8 @@ Cumulative inductive types, coinductive types, variants and records only make sense when they are universe polymorphic. Therefore, an error is issued whenever the user uses the :g:`Cumulative` or :g:`NonCumulative` prefix in a monomorphic context. -Notice that this is not the case for the option :flag:`Polymorphic Inductive Cumulativity`. -That is, this option, when set, makes all subsequent *polymorphic* +Notice that this is not the case for the :flag:`Polymorphic Inductive Cumulativity` flag. +That is, this flag, when set, makes all subsequent *polymorphic* inductive declarations cumulative (unless, of course the :g:`NonCumulative` prefix is used) but has no effect on *monomorphic* inductive declarations. @@ -439,7 +439,7 @@ underscore or by omitting the annotation to a polymorphic definition. .. flag:: Strict Universe Declaration - Turning this option off allows one to freely use + Turning this flag off allows one to freely use identifiers for universes without declaring them first, with the semantics that the first use declares it. In this mode, the universe names are not associated with the definition or proof once it has been @@ -447,7 +447,7 @@ underscore or by omitting the annotation to a polymorphic definition. .. flag:: Private Polymorphic Universes - This option, on by default, removes universes which appear only in + This flag, on by default, removes universes which appear only in the body of an opaque polymorphic definition from the definition's universe arguments. As such, no value needs to be provided for these universes when instantiating the definition. Universe @@ -480,7 +480,7 @@ underscore or by omitting the annotation to a polymorphic definition. About foo. To recover the same behaviour with regard to universes as - :g:`Defined`, the option :flag:`Private Polymorphic Universes` may + :g:`Defined`, the :flag:`Private Polymorphic Universes` flag may be unset: .. coqtop:: all diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib index 85b02013d8..db089df395 100644 --- a/doc/sphinx/biblio.bib +++ b/doc/sphinx/biblio.bib @@ -222,6 +222,25 @@ s}, year = {1890} } +@article{Gilbert:POPL2019, + author = {Gilbert, Ga\"{e}tan and Cockx, Jesper and Sozeau, Matthieu and Tabareau, Nicolas}, + title = {{Definitional Proof Irrelevance Without K}}, + journal = {Proc. ACM Program. Lang.}, + issue_date = {January 2019}, + volume = {3}, + number = {POPL}, + year = {2019}, + issn = {2475-1421}, + pages = {3:1--3:28}, + articleno = {3}, + numpages = {28}, + url = {http://doi.acm.org/10.1145/3290316}, + acmid = {3290316}, + publisher = {ACM}, + address = {New York, NY, USA}, + keywords = {proof assistants, proof irrelevance, type theory}, +} + @InProceedings{Gim94, author = {E. Gim\'enez}, booktitle = {Types'94 : Types for Proofs and Programs}, @@ -340,6 +359,27 @@ s}, year = {1997} } +@inproceedings{Visser98, + author = {Eelco Visser and + Zine{-}El{-}Abidine Benaissa and + Andrew P. Tolmach}, + title = {Building Program Optimizers with Rewriting Strategies}, + booktitle = {ICFP}, + pages = {13--26}, + year = {1998}, +} + +@inproceedings{Visser01, + author = {Eelco Visser}, + title = {Stratego: {A} Language for Program Transformation Based on Rewriting + Strategies}, + booktitle = {RTA}, + pages = {357--362}, + year = {2001}, + series = {LNCS}, + volume = {2051}, +} + @InProceedings{DBLP:conf/types/McBride00, author = {Conor McBride}, title = {Elimination with a Motive}, diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 6410620b40..54aeed428f 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -49,7 +49,8 @@ The sort :math:`\SProp` is like :math:`\Prop` but the propositions in equal). Objects of type :math:`\SProp` are called strict propositions. :math:`\SProp` is rejected except when using the compiler option ``-allow-sprop``. See :ref:`sprop` for information about using -:math:`\SProp`. +:math:`\SProp`, and :cite:`Gilbert:POPL2019` for meta theoretical +considerations. The sort :math:`\Set` intends to be the type of small sets. This includes data types such as booleans and naturals, but also products, subsets, and @@ -1195,7 +1196,7 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or .. flag:: Auto Template Polymorphism - This option, enabled by default, makes every inductive type declared + This flag, enabled by default, makes every inductive type declared at level :math:`\Type` (without annotations or hiding it behind a definition) template polymorphic if possible. @@ -1224,7 +1225,7 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or .. flag:: Template Check - Unsetting option :flag:`Template Check` disables the check of + This flag is on by default. Turning it off 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 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 f477bf239d..a047bab421 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -188,7 +188,7 @@ other arguments are the parameters of the inductive type. .. note:: Induction schemes are automatically generated for inductive records. Automatic generation of induction schemes for non-recursive records defined with the ``Record`` keyword can be activated with the - ``Nonrecursive Elimination Schemes`` option (see :ref:`proofschemes-induction-principles`). + :flag:`Nonrecursive Elimination Schemes` flag (see :ref:`proofschemes-induction-principles`). .. note:: ``Structure`` is a synonym of the keyword ``Record``. @@ -243,14 +243,14 @@ Primitive Projections .. flag:: Printing Primitive Projection Parameters - This compatibility option reconstructs internally omitted parameters at + This compatibility flag reconstructs internally omitted parameters at printing time (even though they are absent in the actual AST manipulated by the kernel). Primitive Record Types ++++++++++++++++++++++ -When the :flag:`Primitive Projections` option is on, definitions of +When the :flag:`Primitive Projections` flag is on, definitions of record types change meaning. When a type is declared with primitive projections, its :g:`match` construct is disabled (see :ref:`primitive_projections` though). To eliminate the (co-)inductive type, one must use its defined primitive projections. @@ -302,7 +302,7 @@ an object of the record type as arguments, and whose body is an application of the unfolded primitive projection of the same name. These constants are used when elaborating partial applications of the projection. One can distinguish them from applications of the primitive -projection if the :flag:`Printing Primitive Projection Parameters` option +projection if the :flag:`Printing Primitive Projection Parameters` flag is off: For a primitive projection application, parameters are printed as underscores while for the compatibility projections they are printed as usual. @@ -481,7 +481,7 @@ Printing nested patterns pattern matching into a single pattern matching over a nested pattern. - When this option is on (default), |Coq|’s printer tries to do such + When this flag is on (default), |Coq|’s printer tries to do such limited re-factorization. Turning it off tells |Coq| to print only simple pattern matching problems in the same way as the |Coq| kernel handles them. @@ -494,7 +494,7 @@ Factorization of clauses with same right-hand side When several patterns share the same right-hand side, it is additionally possible to share the clauses using disjunctive patterns. Assuming that the - printing matching mode is on, this option (on by default) tells |Coq|'s + printing matching mode is on, this flag (on by default) tells |Coq|'s printer to try to do this kind of factorization. Use of a default clause @@ -505,7 +505,7 @@ Use of a default clause When several patterns share the same right-hand side which do not depend on the arguments of the patterns, yet an extra factorization is possible: the disjunction of patterns can be replaced with a `_` default clause. Assuming that - the printing matching mode and the factorization mode are on, this option (on by + the printing matching mode and the factorization mode are on, this flag (on by default) tells |Coq|'s printer to use a default clause when relevant. Printing of wildcard patterns @@ -514,7 +514,7 @@ Printing of wildcard patterns .. flag:: Printing Wildcard Some variables in a pattern may not occur in the right-hand side of - the pattern matching clause. When this option is on (default), the + the pattern matching clause. When this flag is on (default), the variables having no occurrences in the right-hand side of the pattern matching clause are just printed using the wildcard symbol “_”. @@ -527,7 +527,7 @@ Printing of the elimination predicate In most of the cases, the type of the result of a matched term is mechanically synthesizable. Especially, if the result type does not - depend of the matched term. When this option is on (default), + depend of the matched term. When this flag is on (default), the result type is not printed when |Coq| knows that it can re- synthesize it. @@ -562,7 +562,7 @@ which types are written this way: ``if`` … ``then`` … ``else`` …. Use the :cmd:`Add @table` and :cmd:`Remove @table` commands to update this set. -This example emphasizes what the printing options offer. +This example emphasizes what the printing settings offer. .. example:: @@ -1311,7 +1311,7 @@ component is equal ``nat`` and hence ``M1.T`` as specified. .. flag:: Short Module Printing - This option (off by default) disables the printing of the types of fields, + This flag (off by default) disables the printing of the types of fields, leaving only their names, for the commands :cmd:`Print Module` and :cmd:`Print Module Type`. @@ -1584,7 +1584,7 @@ says that the implicit argument is maximally inserted. Each implicit argument can be declared to have to be inserted maximally or non maximally. This can be governed argument per argument by the command -:cmd:`Arguments (implicits)` or globally by the :flag:`Maximal Implicit Insertion` option. +:cmd:`Arguments (implicits)` or globally by the :flag:`Maximal Implicit Insertion` flag. .. seealso:: :ref:`displaying-implicit-args`. @@ -1757,7 +1757,7 @@ Automatic declaration of implicit arguments This command tells |Coq| to automatically detect what are the implicit arguments of a defined object. - The auto-detection is governed by options telling if strict, + The auto-detection is governed by flags telling if strict, contextual, or reversible-pattern implicit arguments must be considered or not (see :ref:`controlling-strict-implicit-args`, :ref:`controlling-strict-implicit-args`, :ref:`controlling-rev-pattern-implicit-args`, and also :ref:`controlling-insertion-implicit-args`). @@ -1827,9 +1827,9 @@ Mode for automatic declaration of implicit arguments .. flag:: Implicit Arguments - This option (off by default) allows to systematically declare implicit + This flag (off by default) allows to systematically declare implicit the arguments detectable as such. Auto-detection of implicit arguments is - governed by options controlling whether strict and contextual implicit + governed by flags controlling whether strict and contextual implicit arguments have to be considered or not. .. _controlling-strict-implicit-args: @@ -1844,11 +1844,11 @@ Controlling strict implicit arguments arguments plus, for historical reasons, a small subset of the non-strict implicit arguments. To relax this constraint and to set implicit all non strict implicit arguments by default, you can turn this - option off. + flag off. .. flag:: Strongly Strict Implicit - Use this option (off by default) to capture exactly the strict implicit + Use this flag (off by default) to capture exactly the strict implicit arguments and no more than the strict implicit arguments. .. _controlling-contextual-implicit-args: @@ -1859,7 +1859,7 @@ Controlling contextual implicit arguments .. flag:: Contextual Implicit By default, |Coq| does not automatically set implicit the contextual - implicit arguments. You can turn this option on to tell |Coq| to also + implicit arguments. You can turn this flag on to tell |Coq| to also infer contextual implicit argument. .. _controlling-rev-pattern-implicit-args: @@ -1870,7 +1870,7 @@ Controlling reversible-pattern implicit arguments .. flag:: Reversible Pattern Implicit By default, |Coq| does not automatically set implicit the reversible-pattern - implicit arguments. You can turn this option on to tell |Coq| to also infer + implicit arguments. You can turn this flag on to tell |Coq| to also infer reversible-pattern implicit argument. .. _controlling-insertion-implicit-args: @@ -1880,7 +1880,7 @@ Controlling the insertion of implicit arguments not followed by explicit argumen .. flag:: Maximal Implicit Insertion - Assuming the implicit argument mode is on, this option (off by default) + Assuming the implicit argument mode is on, this flag (off by default) declares implicit arguments to be automatically inserted when a function is partially applied and the next argument of the function is an implicit one. @@ -1927,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) @@ -1960,7 +1962,7 @@ Explicit displaying of implicit arguments for pretty-printing .. flag:: Printing Implicit By default, the basic pretty-printing rules hide the inferable implicit - arguments of an application. Turn this option on to force printing all + arguments of an application. Turn this flag on to force printing all implicit arguments. .. flag:: Printing Implicit Defensive @@ -1968,7 +1970,7 @@ Explicit displaying of implicit arguments for pretty-printing By default, the basic pretty-printing rules display the implicit arguments that are not detected as strict implicit arguments. This “defensive” mode can quickly make the display cumbersome so this can - be deactivated by turning this option off. + be deactivated by turning this flag off. .. seealso:: :flag:`Printing All`. @@ -1997,7 +1999,7 @@ Deactivation of implicit arguments for parsing .. flag:: Parsing Explicit - Turning this option on (it is off by default) deactivates the use of implicit arguments. + Turning this flag on (it is off by default) deactivates the use of implicit arguments. In this case, all arguments of constants, inductive types, constructors, etc, including the arguments declared as implicit, have @@ -2269,11 +2271,11 @@ Printing constructions in full Coercions, implicit arguments, the type of pattern matching, but also notations (see :ref:`syntaxextensionsandinterpretationscopes`) can obfuscate the behavior of some tactics (typically the tactics applying to occurrences of subterms are - sensitive to the implicit arguments). Turning this option on + sensitive to the implicit arguments). Turning this flag on deactivates all high-level printing features such as coercions, implicit arguments, returned type of pattern matching, notations and various syntactic sugar for pattern matching or record projections. - Otherwise said, :flag:`Printing All` includes the effects of the options + Otherwise said, :flag:`Printing All` includes the effects of the flags :flag:`Printing Implicit`, :flag:`Printing Coercions`, :flag:`Printing Synth`, :flag:`Printing Projections`, and :flag:`Printing Notations`. To reactivate the high-level printing features, use the command ``Unset Printing All``. @@ -2285,8 +2287,8 @@ Printing universes .. flag:: Printing Universes - Turn this option on to activate the display of the actual level of each - occurrence of :g:`Type`. See :ref:`Sorts` for details. This wizard option, in + Turn this flag on to activate the display of the actual level of each + occurrence of :g:`Type`. See :ref:`Sorts` for details. This wizard flag, in combination with :flag:`Printing All` can help to diagnose failures to unify terms apparently identical but internally different in the Calculus of Inductive Constructions. @@ -2297,7 +2299,7 @@ Printing universes This command can be used to print the constraints on the internal level of the occurrences of :math:`\Type` (see :ref:`Sorts`). - If the optional ``Sorted`` option is given, each universe will be made + If the ``Sorted`` keyword is present, each universe will be made equivalent to a numbered label reflecting its level (with a linear ordering) in the universe hierarchy. @@ -2355,7 +2357,7 @@ outside of its context of definition, its instance, written under the form :n:`{ {*; @ident := @term} }` is appending to its name, indicating how the variables of its defining context are instantiated. The variables of the context of the existential variables which are -instantiated by themselves are not written, unless the flag :flag:`Printing Existential Instances` +instantiated by themselves are not written, unless the :flag:`Printing Existential Instances` flag is on (see Section :ref:`explicit-display-existentials`), and this is why an existential variable used in the same context as its context of definition is written with no instance. @@ -2379,7 +2381,7 @@ Explicit displaying of existential instances for pretty-printing .. flag:: Printing Existential Instances - This option (off by default) activates the full display of how the + This flag (off by default) activates the full display of how the context of an existential variable is instantiated at each of the occurrences of the existential variable. @@ -2409,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 @@ -2462,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 ae9d284661..f667dd94b0 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -779,7 +779,7 @@ 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 positivity checking can be disabled using - the option :flag:`Positivity Checking` (see :ref:`controlling-typing-flags`). + the :flag:`Positivity Checking` flag (see :ref:`controlling-typing-flags`). .. exn:: The conclusion of @type is not valid; it must be built from @ident. @@ -956,7 +956,7 @@ Parameterized inductive types .. flag:: Uniform Inductive Parameters - When this option is set (it is off by default), + When this flag is set (it is off by default), inductive definitions are abstracted over their parameters before type checking constructors, allowing to write: @@ -991,7 +991,7 @@ Variants The :cmd:`Variant` command is identical to the :cmd:`Inductive` command, except that it disallows recursive definition of types (for instance, lists cannot be defined using :cmd:`Variant`). No induction scheme is generated for - this variant, unless option :flag:`Nonrecursive Elimination Schemes` is on. + this variant, unless the :flag:`Nonrecursive Elimination Schemes` flag is on. .. exn:: The @num th argument of @ident must be @ident in @type. :undocumented: @@ -1393,11 +1393,11 @@ Chapter :ref:`Tactics`. The basic assertion command is: The name you provided is already defined. You have then to choose another name. - .. exn:: Nested proofs are not allowed unless you turn option Nested Proofs Allowed on. + .. exn:: Nested proofs are not allowed unless you turn the :flag:`Nested Proofs Allowed` flag on. You are asserting a new statement while already being in proof editing mode. This feature, called nested proofs, is disabled by default. - To activate it, turn option :flag:`Nested Proofs Allowed` on. + To activate it, turn the :flag:`Nested Proofs Allowed` flag on. .. cmdv:: Lemma @ident {? @binders } : @type Remark @ident {? @binders } : @type @@ -1470,8 +1470,8 @@ using the keyword :cmd:`Qed`. .. note:: - #. Several statements can be simultaneously asserted provided option - :flag:`Nested Proofs Allowed` was turned on. + #. Several statements can be simultaneously asserted provided the + :flag:`Nested Proofs Allowed` flag was turned on. #. Not only other assertions but any vernacular command can be given while in the process of proving a given assertion. In this case, the @@ -1556,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..97e7af8cb4 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -36,7 +36,7 @@ toplevel with the command ``Coqloop.loop();;``. .. flag:: Coqtop Exit On Error - This option, off by default, causes coqtop to exit with status code + This flag, off by default, causes coqtop to exit with status code ``1`` if a command produces an error instead of recovering from it. Batch compilation (coqc) @@ -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`). @@ -212,7 +219,7 @@ and ``coqtop``, unless stated otherwise: .. warning:: This makes the logic inconsistent. :-mangle-names *ident*: *Experimental.* Do not depend on this option. Replace Coq's auto-generated name scheme with names of the form *ident0*, *ident1*, - etc. Within Coq, the flag :flag:`Mangle Names` turns this behavior on, + etc. Within Coq, the :flag:`Mangle Names` flag turns this behavior on, and the :opt:`Mangle Names Prefix` option sets the prefix to use. This feature is intended to be used as a linter for developments that want to be robust to changes in the auto-generated name scheme. The options are provided to @@ -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/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 6efc634087..e37f300915 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -860,8 +860,8 @@ We can carry out pattern matching on terms with: If the evaluation of the right-hand-side of a valid match fails, the next matching subterm is tried. If no further subterm matches, the next clause is tried. Matching subterms are considered top-bottom and from left to - right (with respect to the raw printing obtained by setting option - :flag:`Printing All`). + right (with respect to the raw printing obtained by setting the + :flag:`Printing All` flag). .. example:: @@ -1642,7 +1642,7 @@ Interactive debugger .. flag:: Ltac Debug - This option governs the step-by-step debugger that comes with the |Ltac| interpreter. + This flag governs the step-by-step debugger that comes with the |Ltac| interpreter. When the debugger is activated, it stops at every step of the evaluation of the current |Ltac| expression and prints information on what it is doing. @@ -1666,13 +1666,13 @@ following: .. exn:: Debug mode not available in the IDE :undocumented: -A non-interactive mode for the debugger is available via the option: +A non-interactive mode for the debugger is available via the flag: .. flag:: Ltac Batch Debug - This option has the effect of presenting a newline at every prompt, when + This flag has the effect of presenting a newline at every prompt, when the debugger is on. The debug log thus created, which does not require - user input to generate when this option is set, can then be run through + user input to generate when this flag is set, can then be run through external tools such as diff. Profiling |Ltac| tactics @@ -1691,7 +1691,7 @@ performance issue. .. flag:: Ltac Profiling - This option enables and disables the profiler. + This flag enables and disables the profiler. .. cmd:: Show Ltac Profile @@ -1775,7 +1775,7 @@ performance issue. benchmarking purposes. You can also pass the ``-profile-ltac`` command line option to ``coqc``, which -turns the :flag:`Ltac Profiling` option on at the beginning of each document, +turns the :flag:`Ltac Profiling` flag on at the beginning of each document, and performs a :cmd:`Show Ltac Profile` at the end. .. warning:: diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 18d2c79461..cfdc70d50e 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -563,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 ***************** diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 00f8269dc3..6884b6e998 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -804,7 +804,7 @@ Controlling the effect of proof editing commands .. flag:: Nested Proofs Allowed - When turned on (it is off by default), this option enables support for nested + When turned on (it is off by default), this flag enables support for nested proofs: a new assertion command can be inserted before the current proof is finished, in which case Coq will temporarily switch to the proof of this *nested lemma*. When the proof of the nested lemma is finished (with :cmd:`Qed` diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 75897fec45..4c697be963 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -2764,7 +2764,7 @@ typeclass inference. .. flag:: SsrHave NoTCResolution - This option restores the behavior of |SSR| 1.4 and below (never resolve typeclasses). + This flag restores the behavior of |SSR| 1.4 and below (never resolve typeclasses). Variants: the suff and wlog tactics ``````````````````````````````````` @@ -3756,8 +3756,11 @@ involves the following steps: the corresponding intro pattern :n:`@i_pattern__i` in each goal. 4. Then :tacn:`under` checks that the first n subgoals - are (quantified) equalities or double implications between a - term and an evar (e.g. ``m - m = ?F2 m`` in the running example). + are (quantified) Leibniz equalities, double implications or + registered relations (w.r.t. Class ``RewriteRelation``) between a + term and an evar, e.g. ``m - m = ?F2 m`` in the running example. + (This support for setoid-like relations is enabled as soon as we do + both ``Require Import ssreflect.`` and ``Require Setoid.``) 5. If so :tacn:`under` protects these n goals against an accidental instantiation of the evar. @@ -3769,7 +3772,10 @@ involves the following steps: by using a regular :tacn:`rewrite` tactic. 7. Interactive editing of the first n goals has to be signalled by - using the :tacn:`over` tactic or rewrite rule (see below). + using the :tacn:`over` tactic or rewrite rule (see below), which + requires that the underlying relation is reflexive. (The running + example deals with Leibniz equality, but ``PreOrder`` relations are + also supported, for example.) 8. Finally, a post-processing step is performed in the main goal to keep the name(s) for the bound variables chosen by the user in @@ -3795,6 +3801,10 @@ displayed as ``'Under[ … ]``): This is a variant of :tacn:`over` in order to close ``'Under[ … ]`` goals, relying on the ``over`` rewrite rule. +Note that a rewrite rule ``UnderE`` is available as well, if one wants +to "unprotect" the evar, without closing the goal automatically (e.g., +to instantiate it manually with another rule than reflexivity). + .. _under_one_liner: One-liner mode diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 78753fc053..ad7f9af0f9 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -261,7 +261,7 @@ These patterns can be used when the hypothesis is an equality: conjunctive pattern that doesn't give enough simple patterns to match all the arguments in the constructor. If set (the default), |Coq| generates additional names to match the number of arguments. - Unsetting the option will put the additional hypotheses in the goal instead, behavior that is more + Unsetting the flag will put the additional hypotheses in the goal instead, behavior that is more similar to |SSR|'s intro patterns. .. deprecated:: 8.10 @@ -477,7 +477,7 @@ that occurrences have to be selected in the hypotheses named :token:`ident`. If no numbers are given for hypothesis :token:`ident`, then all the occurrences of :token:`term` in the hypothesis are selected. If numbers are given, they refer to occurrences of :token:`term` when the term is printed -using option :flag:`Printing All`, counting from left to right. In particular, +using the :flag:`Printing All` flag, counting from left to right. In particular, occurrences of :token:`term` in implicit arguments (see :ref:`ImplicitArguments`) or coercions (see :ref:`Coercions`) are counted. @@ -804,11 +804,11 @@ Applying theorems component of the tuple matches the goal, it excludes components whose statement would result in applying an universal lemma of the form ``forall A, ... -> A``. Excluding this kind of lemma can be avoided by - setting the following option: + setting the following flag: .. flag:: Universal Lemma Under Conjunction - This option, which preserves compatibility with versions of Coq prior to + This flag, which preserves compatibility with versions of Coq prior to 8.4 is also available for :n:`apply @term in @ident` (see :tacn:`apply ... in`). .. tacn:: apply @term in @ident @@ -1527,7 +1527,7 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`. This is equivalent to :n:`generalize @term` but it generalizes only over the specified occurrences of :n:`@term` (counting from left to right on the - expression printed using option :flag:`Printing All`). + expression printed using the :flag:`Printing All` flag). .. tacv:: generalize @term as @ident @@ -2300,16 +2300,16 @@ and an explanation of the underlying technique. .. flag:: Structural Injection - This option ensure that :n:`injection @term` erases the original hypothesis + This flag ensures that :n:`injection @term` erases the original hypothesis and leaves the generated equalities in the context rather than putting them as antecedents of the current goal, as if giving :n:`injection @term as` - (with an empty list of names). This option is off by default. + (with an empty list of names). This flag is off by default. .. flag:: Keep Proof Equalities By default, :tacn:`injection` only creates new equalities between :n:`@term`\s whose type is in sort :g:`Type` or :g:`Set`, thus implementing a special - behavior for objects that are proofs of a statement in :g:`Prop`. This option + behavior for objects that are proofs of a statement in :g:`Prop`. This flag controls this behavior. .. tacn:: inversion @ident @@ -2862,26 +2862,26 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. .. flag:: Regular Subst Tactic - This option controls the behavior of :tacn:`subst`. When it is + This flag controls the behavior of :tacn:`subst`. When it is activated (it is by default), :tacn:`subst` also deals with the following corner cases: + A context with ordered hypotheses :n:`@ident`:sub:`1` :n:`= @ident`:sub:`2` and :n:`@ident`:sub:`1` :n:`= t`, or :n:`t′ = @ident`:sub:`1`` with `t′` not a variable, and no other hypotheses of the form :n:`@ident`:sub:`2` :n:`= u` - or :n:`u = @ident`:sub:`2`; without the option, a second call to + or :n:`u = @ident`:sub:`2`; without the flag, a second call to subst would be necessary to replace :n:`@ident`:sub:`2` by `t` or `t′` respectively. - + The presence of a recursive equation which without the option would + + The presence of a recursive equation which without the flag would be a cause of failure of :tacn:`subst`. + A context with cyclic dependencies as with hypotheses :n:`@ident`:sub:`1` :n:`= f @ident`:sub:`2` and :n:`@ident`:sub:`2` :n:`= g @ident`:sub:`1` which without the - option would be a cause of failure of :tacn:`subst`. + flag would be a cause of failure of :tacn:`subst`. Additionally, it prevents a local definition such as :n:`@ident := t` to be unfolded which otherwise it would exceptionally unfold in configurations containing hypotheses of the form :n:`@ident = u`, or :n:`u′ = @ident` with `u′` not a variable. Finally, it preserves the initial order of - hypotheses, which without the option it may break. + hypotheses, which without the flag it may break. default. @@ -3086,7 +3086,7 @@ the conversion in hypotheses :n:`{+ @ident}`. .. flag:: NativeCompute Profiling - On Linux, if you have the ``perf`` profiler installed, this option makes + On Linux, if you have the ``perf`` profiler installed, this flag makes it possible to profile :tacn:`native_compute` evaluations. .. opt:: NativeCompute Profile Filename @string @@ -3103,7 +3103,7 @@ the conversion in hypotheses :n:`{+ @ident}`. .. flag:: Debug Cbv - This option makes :tacn:`cbv` (and its derivative :tacn:`compute`) print + This flag makes :tacn:`cbv` (and its derivative :tacn:`compute`) print information about the constants it encounters and the unfolding decisions it makes. @@ -3271,7 +3271,7 @@ the conversion in hypotheses :n:`{+ @ident}`. .. flag:: Debug RAKAM - This option makes :tacn:`cbn` print various debugging information. + This flag makes :tacn:`cbn` print various debugging information. ``RAKAM`` is the Refolding Algebraic Krivine Abstract Machine. .. tacn:: unfold @qualid @@ -3548,7 +3548,7 @@ Automation Info Trivial Debug Trivial - These options enable printing of informative or debug information for + These flags enable printing of informative or debug information for the :tacn:`auto` and :tacn:`trivial` tactics. .. tacn:: eauto @@ -3576,7 +3576,7 @@ Automation The various options for :tacn:`eauto` are the same as for :tacn:`auto`. - :tacn:`eauto` also obeys the following options: + :tacn:`eauto` also obeys the following flags: .. flag:: Info Eauto Debug Eauto @@ -3720,7 +3720,7 @@ automatically created. .. cmdv:: Local Hint @hint_definition : {+ @ident} This is used to declare hints that must not be exported to the other modules - that require and import the current module. Inside a section, the option + that require and import the current module. Inside a section, the flag Local is useless since hints do not survive anyway to the closure of sections. @@ -4196,7 +4196,7 @@ some incompatibilities. .. flag:: Intuition Negation Unfolding Controls whether :tacn:`intuition` unfolds inner negations which do not need - to be unfolded. This option is on by default. + to be unfolded. This flag is on by default. .. tacn:: rtauto :name: rtauto @@ -4316,7 +4316,7 @@ some incompatibilities. .. flag:: Congruence Verbose - This option makes :tacn:`congruence` print debug information. + This flag makes :tacn:`congruence` print debug information. Checking properties of terms diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 843459b723..e87b76b4ab 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -962,7 +962,7 @@ Controlling display .. flag:: Silent - This option controls the normal displaying. + This flag controls the normal displaying. .. opt:: Warnings "{+, {? {| - | + } } @ident }" :name: Warnings @@ -977,7 +977,7 @@ Controlling display .. flag:: Search Output Name Only - This option restricts the output of search commands to identifier names; + This flag restricts the output of search commands to identifier names; turning it on causes invocations of :cmd:`Search`, :cmd:`SearchHead`, :cmd:`SearchPattern`, :cmd:`SearchRewrite` etc. to omit types from their output, printing only identifiers. @@ -998,7 +998,7 @@ Controlling display .. flag:: Printing Compact Contexts - This option controls the compact display mode for goals contexts. When on, + This flag controls the compact display mode for goals contexts. When on, the printer tries to reduce the vertical size of goals contexts by putting several variables (even if of different types) on the same line provided it does not exceed the printing width (see :opt:`Printing Width`). At the time @@ -1006,13 +1006,13 @@ Controlling display .. flag:: Printing Unfocused - This option controls whether unfocused goals are displayed. Such goals are + This flag controls whether unfocused goals are displayed. Such goals are created by focusing other goals with bullets (see :ref:`bullets` or :ref:`curly braces <curly-braces>`). It is off by default. .. flag:: Printing Dependent Evars Line - This option controls the printing of the “(dependent evars: …)” information + This flag 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) @@ -1213,7 +1213,7 @@ Controlling Typing Flags .. flag:: Guard Checking - This option can be used to enable/disable the guard checking of + This flag 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 @@ -1221,14 +1221,14 @@ Controlling Typing Flags .. flag:: Positivity Checking - This option can be used to enable/disable the positivity checking of inductive + This flag 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 + This flag 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 diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index 3a12ee288a..5b0b3c51b0 100644 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ b/doc/sphinx/user-extensions/proof-schemes.rst @@ -128,7 +128,7 @@ Automatic declaration of schemes .. warning:: - You have to be careful with this option since Coq may now reject well-defined + You have to be careful with these flags since Coq may now reject well-defined inductive types because it cannot compute a Boolean equality for them. .. flag:: Rewriting Schemes diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index a28ce600ca..02910e603a 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1442,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). @@ -1592,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 bb6df87970..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 @@ -82,3 +83,5 @@ plugins/setoid_ring/Rings_Q.v plugins/setoid_ring/Rings_R.v plugins/setoid_ring/Rings_Z.v plugins/setoid_ring/ZArithRing.v +plugins/ssr/ssrunder.v +plugins/ssr/ssrsetoid.v diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index f0ada745e7..851510b465 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -328,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> @@ -607,6 +620,7 @@ through the <tt>Require Import</tt> command.</p> </dt> <dd> plugins/ssrmatching/ssrmatching.v + plugins/ssr/ssrclasses.v plugins/ssr/ssreflect.v plugins/ssr/ssrbool.v plugins/ssr/ssrfun.v |