diff options
Diffstat (limited to 'doc/sphinx')
29 files changed, 1511 insertions, 309 deletions
diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst index b568160356..45b3f6f161 100644 --- a/doc/sphinx/addendum/extended-pattern-matching.rst +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -192,7 +192,7 @@ Disjunctive patterns -------------------- Multiple patterns that share the same right-hand-side can be -factorized using the notation :n:`{+| @mult_pattern}`. For +factorized using the notation :n:`{+| @patterns_comma}`. For instance, :g:`max` can be rewritten as follows: .. coqtop:: in reset diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index 3dc8707a34..7136cc28d1 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 @@ -282,7 +283,7 @@ Notice that in the case of type scheme axiom (i.e. whose type is an arity, that is a sequence of product finished by a sort), then some type variables have to be given (as quoted strings). The syntax is then: -.. cmdv:: Extract Constant @qualid @string ... @string => @string +.. cmdv:: Extract Constant @qualid {+ @string } => @string :undocumented: The number of type variables is checked by the system. For example: @@ -529,7 +530,7 @@ A detailed example: Euclidean division ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The file ``Euclid`` contains the proof of Euclidean division. -The natural numbers used here are unary, represented by the type``nat``, +The natural numbers used here are unary, represented by the type ``nat``, which is defined by two constructors ``O`` and ``S``. This module contains a theorem ``eucl_dev``, whose type is:: diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index 2ea0861e47..9f5741f72a 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -9,7 +9,7 @@ This chapter presents the extension of several equality related tactics to work over user-defined structures (called setoids) that are equipped with ad-hoc equivalence relations meant to behave as equalities. Actually, the tactics have also been generalized to -relations weaker then equivalences (e.g. rewriting systems). The +relations weaker than equivalences (e.g. rewriting systems). The toolbox also extends the automatic rewriting capabilities of the system, allowing the specification of custom strategies for rewriting. @@ -117,7 +117,7 @@ parameters is any term :math:`f \, t_1 \ldots t_n`. .. example:: Morphisms Continuing the previous example, let ``union: forall (A : Type), list A -> list A -> list A`` - perform the union of two sets by appending one list to the other. ``union` is a binary + perform the union of two sets by appending one list to the other. ``union`` is a binary morphism parametric over ``A`` that respects the relation instance ``(set_eq A)``. The latter condition is proved by showing: @@ -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: @@ -739,7 +741,7 @@ following grammar: : topdown `strategy` (top-down) : hints `ident` (apply hints from hint database) : terms `term` ... `term` (any of the terms) - : eval `redexpr` (apply reduction) + : eval `red_expr` (apply reduction) : fold `term` (unify) : ( `strategy` ) diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index 7fee62179b..19b33f0d90 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -165,6 +165,12 @@ Declaring Coercions convertible with existing ones when they have coercions that don't satisfy the uniform inheritance condition. + .. warn:: ... is not definitionally an identity function. + + If a coercion path has the same source and target class, that is said to be + circular. When a new circular coercion path is not convertible with the + identity function, it will be reported as ambiguous. + .. cmdv:: Local Coercion @qualid : @class >-> @class Declares the construction denoted by :token:`qualid` as a coercion local to @@ -274,7 +280,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..57a2254100 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -47,9 +47,22 @@ Leibniz equality on some type. An example implementation is: | tt, tt => eq_refl tt end }. -Using :cmd:`Program Instance`, if one does not give all the members in -the Instance declaration, Coq generates obligations for the remaining -fields, e.g.: +Using the attribute ``refine``, if the term is not sufficient to +finish the definition (e.g. due to a missing field or non-inferable +hole) it must be finished in proof mode. If it is sufficient a trivial +proof mode with no open goals is started. + +.. coqtop:: in + + #[refine] Instance unit_EqDec' : EqDec unit := { eqb x y := true }. + Proof. intros [] [];reflexivity. Defined. + +Note that if you finish the proof with :cmd:`Qed` the entire instance +will be opaque, including the fields given in the initial term. + +Alternatively, in :flag:`Program Mode` if one does not give all the +members in the Instance declaration, Coq generates obligations for the +remaining fields, e.g.: .. coqtop:: in @@ -560,8 +573,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..3d73f9bd6e 100644 --- a/doc/sphinx/biblio.bib +++ b/doc/sphinx/biblio.bib @@ -192,7 +192,7 @@ s}, @InProceedings{Del00, author = {Delahaye, D.}, - title = {A {T}actic {L}anguage for the {S}ystem {{\sf Coq}}}, + title = {A {T}actic {L}anguage for the {S}ystem {Coq}}, booktitle = {Proceedings of Logic for Programming and Automated Reasoning (LPAR), Reunion Island}, publisher = SV, @@ -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/changes.rst b/doc/sphinx/changes.rst index 80a24b997c..1d0c937792 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -6,6 +6,512 @@ Recent changes .. include:: ../unreleased.rst +Version 8.11 +------------ + +Summary of changes +~~~~~~~~~~~~~~~~~~ + +The main changes brought by |Coq| version 8.11 are: + +- `Ltac2`__, a new tactic language for writing more robust larger scale + tactics, with built-in support for datatypes and the multi-goal tactic monad. +- `Primitive floats`__ are integrated in terms and follow the binary64 format + of the IEEE 754 standard, as specified in the `Coq.Float.Floats` library. +- `Cleanups`__ of the section mechanism, delayed proofs and further + restrictions of template polymorphism to fix soundness issues related to + universes. +- New `unsafe flags`__ to disable locally guard, positivity and universe + checking. Reliance on these flags is always printed by + :g:`Print Assumptions`. +- `Fixed bugs`__ of :g:`Export` and :g:`Import` that can have a + significant impact on user developments (**common source of + incompatibility!**). +- New interactive development method based on `vos` `interface files`__, + allowing to work on a file without recompiling the proof parts of their + dependencies. +- New :g:`Arguments` annotation for `bidirectional type inference`__ + configuration for reference (e.g. constants, inductive) applications. +- New `refine attribute`__ for :cmd:`Instance` can be used instead of + the removed ``Refine Instance Mode``. +- Generalization of the :g:`under` and :g:`over` tactics__ of SSReflect to + arbitrary relations. +- `Revision`__ of the :g:`Coq.Reals` library, its axiomatisation and + instances of the constructive and classical real numbers. + +__ 811Ltac2_ +__ 811PrimitiveFloats_ +__ 811Sections_ +__ 811UnsafeFlags_ +__ 811ExportBug_ +__ 811vos_ +__ 811BidirArguments_ +__ 811RefineInstance_ +__ 811SSRUnderOver_ +__ 811Reals_ + +The ``dev/doc/critical-bugs`` file documents the known critical bugs of |Coq| +and affected releases. See the `Changes in 8.11+beta1`_ section for the +detailed list of changes, including potentially breaking changes marked with +**Changed**. + +Maxime Dénès, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Michael +Soegtrop, Théo Zimmermann worked on maintaining and improving the +continuous integration system and package building infrastructure. + +Coq's documentation is available at https://coq.github.io/doc/V8.11+beta1/api (documentation of +the ML API), https://coq.github.io/doc/V8.11+beta1/refman (reference +manual), and https://coq.github.io/doc/V8.11+beta1/stdlib (documentation of +the standard library). + +The OPAM repository for |Coq| packages has been maintained by +Karl Palmskog, Matthieu Sozeau, Enrico Tassi 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 Michael D. Adams, Guillaume +Allais, Helge Bahmann, Langston Barrett, Guillaume Bertholon, Frédéric +Besson, Simon Boulier, Michele Caci, Tej Chajed, Arthur Charguéraud, +Cyril Cohen, Frédéric Dabrowski, Arthur Azevedo de Amorim, Maxime +Dénès, Nikita Eshkeev, Jim Fehrle, Emilio Jesús Gallego Arias, +Paolo G. Giarrusso, Gaëtan Gilbert, Georges Gonthier, Jason Gross, +Samuel Gruetter, Armaël Guéneau, Hugo Herbelin, Florent Hivert, Jasper +Hugunin, Shachar Itzhaky, Jan-Oliver Kaiser, Robbert Krebbers, Vincent +Laporte, Olivier Laurent, Samuel Lelièvre, Nicholas Lewycky, Yishuai +Li, Jose Fernando Lopez Fernandez, Andreas Lynge, Kenji Maillard, Erik +Martin-Dorel, Guillaume Melquiond, Alexandre Moine, Oliver Nash, +Wojciech Nawrocki, Antonio Nikishaev, Pierre-Marie Pédrot, Clément +Pit-Claudel, Lars Rasmusson, Robert Rand, Talia Ringer, JP Rodi, +Pierre Roux, Kazuhiko Sakaguchi, Vincent Semeria, Michael Soegtrop, +Matthieu Sozeau, spanjel, Claude Stolze, Enrico Tassi, Laurent Théry, +James R. Wilcox, Xia Li-yao, Théo Zimmermann + +Many power users helped to improve the design of the new features via +the issue and pull request system, the |Coq| development mailing list, +the coq-club@inria.fr mailing list or the `Discourse forum +<https://coq.discourse.group/>`_. It would be impossible to mention +exhaustively the names of everybody who to some extent influenced the +development. + +Version 8.11 is the sixth release of |Coq| developed on a time-based +development cycle. Its development spanned 3 months from the release of +|Coq| 8.10. Pierre-Marie Pédrot is the release manager and maintainer of this +release, assisted by Matthieu Sozeau. This release is the result of 2000+ +commits and 300+ PRs merged, closing 75+ issues. + +| Paris, November 2019, +| Matthieu Sozeau for the |Coq| development team +| + + +Changes in 8.11+beta1 +~~~~~~~~~~~~~~~~~~~~~ + +**Kernel** + + .. _811PrimitiveFloats: + +- **Added:** + A built-in support of floating-point arithmetic, 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). +- **Changed:** + Internal definitions generated by :tacn:`abstract`\-like tactics are now inlined + inside universe :cmd:`Qed`\-terminated polymorphic definitions, similarly to what + happens for their monomorphic counterparts, + (`#10439 <https://github.com/coq/coq/pull/10439>`_, by Pierre-Marie Pédrot). + + .. _811Sections: + +- **Fixed:** + 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). +- **Changed:** + 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). + +**Specification language, type inference** + + .. _811BidirArguments: + +- **Added:** + Annotation in `Arguments` for bidirectionality hints: it is now possible + to tell type inference to use type information from the context once the `n` + first arguments of an application are known. The syntax is: + `Arguments foo x y & z`. See :cmd:`Arguments (bidirectionality hints)` + (`#10049 <https://github.com/coq/coq/pull/10049>`_, by Maxime Dénès with + help from Enrico Tassi). +- **Added:** + Record fields can be annotated to prevent them from being used as canonical projections; + see :ref:`canonicalstructures` for details + (`#10076 <https://github.com/coq/coq/pull/10076>`_, + by Vincent Laporte). +- **Changed:** + Require parentheses around nested disjunctive patterns, so that pattern and + term syntax are consistent; match branch patterns no longer require + parentheses for notation at level 100 or more. + + .. warning:: Incompatibilities + + + In :g:`match p with (_, (0|1)) => ...` parentheses may no longer be + omitted around :n:`0|1`. + + Notation :g:`(p | q)` now potentially clashes with core pattern syntax, + and should be avoided. ``-w disj-pattern-notation`` flags such :cmd:`Notation`. + + See :ref:`extendedpatternmatching` for details + (`#10167 <https://github.com/coq/coq/pull/10167>`_, + by Georges Gonthier). +- **Changed:** + :cmd:`Function` always opens a proof when used with a ``measure`` or ``wf`` + annotation, see :ref:`advanced-recursive-functions` for the updated + documentation (`#10215 <https://github.com/coq/coq/pull/10215>`_, + by Enrico Tassi). +- **Changed:** + The legacy command :cmd:`Add Morphism` always opens a proof and cannot be used + inside a module type. In order to declare a module type parameter that + happens to be a morphism, use :cmd:`Declare Morphism`. See + :ref:`deprecated_syntax_for_generalized_rewriting` for the updated + documentation (`#10215 <https://github.com/coq/coq/pull/10215>`_, + by Enrico Tassi). +- **Changed:** + The universe polymorphism setting now applies from the opening of a section. + In particular, it is not possible anymore to mix polymorphic and monomorphic + definitions in a section when there are no variables nor universe constraints + defined in this section. This makes the behaviour consistent with the + documentation. (`#10441 <https://github.com/coq/coq/pull/10441>`_, + by Pierre-Marie Pédrot) +- **Added:** + The :cmd:`Section` vernacular command now accepts the "universes" attribute. In + addition to setting the section universe polymorphism, it also locally sets + the universe polymorphic option inside the section. + (`#10441 <https://github.com/coq/coq/pull/10441>`_, by Pierre-Marie Pédrot) +- **Fixed:** + ``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). +- **Changed:** + Output of the :cmd:`Print` and :cmd:`About` commands. + 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). + + .. _811RefineInstance: + +- **Added:** ``#[refine]`` attribute for :cmd:`Instance`, a more + predictable version of the old ``Refine Instance Mode`` which + unconditionally opens a proof (`#10996 + <https://github.com/coq/coq/pull/10996>`_, by Gaëtan Gilbert). +- **Changed:** + 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). +- **Fixed:** Bugs sometimes preventing to define valid (co)fixpoints with implicit arguments + in the presence of local definitions, see `#3282 <https://github.com/coq/coq/issues/3282>`_ + (`#11132 <https://github.com/coq/coq/pull/11132>`_, by Hugo Herbelin). + + .. example:: + + The following features an implicit argument after a local + definition. It was wrongly rejected. + + .. coqtop:: in + + Definition f := fix f (o := true) {n : nat} m {struct m} := + match m with 0 => 0 | S m' => f (n:=n+1) m' end. + +**Notations** + +- **Added:** + 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). +- **Added:** + The :cmd:`Notation` and :cmd:`Infix` commands now support the `deprecated` + attribute + (`#10180 <https://github.com/coq/coq/pull/10180>`_, by Maxime Dénès). +- **Deprecated:** + The former `compat` annotation for notations is + deprecated, and its semantics changed. It is now made equivalent to using + a `deprecated` attribute, and is no longer connected with the `-compat` + command-line flag + (`#10180 <https://github.com/coq/coq/pull/10180>`_, by Maxime Dénès). +- **Changed:** + 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). + +**Tactics** + +- **Added:** + Syntax :n:`injection @term as [= {+ @intropattern} ]` as + an alternative to :n:`injection @term as {+ @simple_intropattern}` using + the standard :n:`@injection_intropattern` syntax (`#9288 + <https://github.com/coq/coq/pull/9288>`_, by Hugo Herbelin). +- **Changed:** + 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). +- **Changed:** + The goal selector tactical ``only`` now checks that the goal range + it is given is valid instead of ignoring goals out of the focus + range (`#10318 <https://github.com/coq/coq/pull/10318>`_, by Gaëtan + Gilbert). +- **Added:** + Flags :flag:`Lia Cache`, :flag:`Nia Cache` and :flag:`Nra Cache`. + (`#10765 <https://github.com/coq/coq/pull/10765>`_, by Frédéric Besson, + see `#10772 <https://github.com/coq/coq/issues/10772>`_ for use case). +- **Added:** + The :tacn:`zify` tactic is now aware of `Z.to_N`. + (`#10774 <https://github.com/coq/coq/pull/10774>`_, grants + `#9162 <https://github.com/coq/coq/issues/9162>`_, by Kazuhiko Sakaguchi). +- **Changed:** + 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). +- **Fixed:** + 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). + +**Tactic language** + + .. _811Ltac2: + +- **Added:** + Ltac2, a new version of the tactic language Ltac, that doesn't + preserve backward compatibility, has been integrated in the main Coq + distribution. It is still experimental, but we already recommend + users of advanced Ltac to start using it and report bugs or request + enhancements. See its documentation in the :ref:`dedicated chapter + <ltac2>` (`#10002 <https://github.com/coq/coq/pull/10002>`_, plugin + authored by Pierre-Marie Pédrot, with contributions by various + users, integration by Maxime Dénès, help on integrating / improving + the documentation by Théo Zimmermann and Jim Fehrle). +- **Added:** + Ltac2 tactic notations with “constr” arguments can specify the + interpretation scope for these arguments; + see :ref:`ltac2_notations` for details + (`#10289 <https://github.com/coq/coq/pull/10289>`_, + by Vincent Laporte). +- **Changed:** + White spaces are forbidden in the :n:`&@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). + +**SSReflect** + + .. _811SSRUnderOver: + +- **Added:** + 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). +- **Added:** + 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). +- **Added:** Lemma :g:`inj_compr` to :g:`ssr.ssrfun` + (`#11136 <https://github.com/coq/coq/pull/11136>`_, by Cyril Cohen). + +**Commands and options** + +- **Removed:** + Deprecated flag `Refine Instance Mode` + (`#9530 <https://github.com/coq/coq/pull/9530>`_, fixes + `#3632 <https://github.com/coq/coq/issues/3632>`_, `#3890 + <https://github.com/coq/coq/issues/3890>`_ and `#4638 + <https://github.com/coq/coq/issues/4638>`_ + by Maxime Dénès, review by Gaëtan Gilbert). +- **Removed:** + Undocumented :n:`Instance : !@type` syntax + (`#10185 <https://github.com/coq/coq/pull/10185>`_, by Gaëtan Gilbert). +- **Removed:** + Deprecated ``Show Script`` command + (`#10277 <https://github.com/coq/coq/pull/10277>`_, by Gaëtan Gilbert). + + .. _811UnsafeFlags: + +- **Added:** + 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). + + .. _811ExportBug: + +- **Fixed:** + Two bugs in :cmd:`Export`. This can have an impact on the behavior of the + :cmd:`Import` command on libraries. `Import A` when `A` imports `B` which exports + `C` was importing `C`, whereas :cmd:`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). + + .. warning:: + + This is a common source of incompatibilities in projects + migrating to Coq 8.11. + +- **Changed:** + 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). +- **Added:** + 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). +- **Removed:** Legacy commands ``AddPath``, ``AddRecPath``, and ``DelPath`` + which were undocumented, broken variants of :cmd:`Add LoadPath`, + :cmd:`Add Rec LoadPath`, and :cmd:`Remove LoadPath` + (`#11187 <https://github.com/coq/coq/pull/11187>`_, + by Maxime Dénès and Théo Zimmermann). + +**Tools** + + .. _811vos: + +- **Added:** + `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). +- **Added:** + Command-line options `-require-import`, `-require-export`, + `-require-import-from` and `-require-export-from`, as well as their + shorthand, `-ri`, `-re`, `-refrom` and -`rifrom`. Deprecate + confusing command line option `-require` + (`#10245 <https://github.com/coq/coq/pull/10245>`_ + by Hugo Herbelin, review by Emilio Gallego). +- **Changed:** + 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). +- **Fixed:** ``coq_makefile`` now supports environment variable ``COQBIN`` with + no ending ``/`` character (`#11068 + <https://github.com/coq/coq/pull/11068>`_, by Gaëtan Gilbert). + +**Standard library** + +- **Changed:** + Moved the :tacn:`auto` hints of the `OrderedType` module into a new `ordered_type` + database + (`#9772 <https://github.com/coq/coq/pull/9772>`_, + by Vincent Laporte). +- **Removed:** + Deprecated modules `Coq.ZArith.Zlogarithm` and `Coq.ZArith.Zsqrt_compat` + (`#9881 <https://github.com/coq/coq/pull/9811>`_, + by Vincent Laporte). + + .. _811Reals: + +- **Added:** + Module `Reals.ConstructiveCauchyReals` defines constructive real numbers + by Cauchy sequences of rational numbers + (`#10445 <https://github.com/coq/coq/pull/10445>`_, by Vincent Semeria, + with the help and review of Guillaume Melquiond and Bas Spitters). +- **Added:** + New module `Reals.ClassicalDedekindReals` defines Dedekind real + numbers as boolean-valued 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` now corresponds to these Dedekind reals, + hidden behind an opaque module, which significantly reduces the + number of axioms needed (see `Reals.Rdefinitions` and + `Reals.Raxioms`), while preserving backward compatibility. + Classical Dedekind reals are a quotient of constructive reals, which + allows to transport many constructive proofs to the classical case + (`#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). +- **Added:** + New lemmas on :g:`combine`, :g:`filter`, :g:`nodup`, :g:`nth`, and + :g:`nth_error` functions on lists + (`#10651 <https://github.com/coq/coq/pull/10651>`_, and + `#10731 <https://github.com/coq/coq/pull/10731>`_, by Oliver Nash). +- **Changed:** + The lemma :g:`filter_app` was moved to the :g:`List` module + (`#10651 <https://github.com/coq/coq/pull/10651>`_, by Oliver Nash). +- **Added:** + Standard equivalence between weak excluded-middle and the + classical instance of De Morgan's law, in module :g:`ClassicalFacts` + (`#10895 <https://github.com/coq/coq/pull/10895>`_, by Hugo Herbelin). + +**Infrastructure and dependencies** + +- **Changed:** + Coq now officially supports OCaml 4.08. + See `INSTALL` file for details + (`#10471 <https://github.com/coq/coq/pull/10471>`_, + by Emilio Jesús Gallego Arias). + Version 8.10 ------------ @@ -568,7 +1074,7 @@ Other changes in 8.10+beta1 - The prelude used to be automatically Exported and is now only Imported. This should be relevant only when importing files which don't use `-noinit` into files which do - (`#9013 <https://github.com/coq/coq/pull/9013>`_, by Gaëtan Gilert). + (`#9013 <https://github.com/coq/coq/pull/9013>`_, by Gaëtan Gilbert). - Added `Coq.Structures.OrderedTypeEx.String_as_OT` to make strings an ordered type, using lexical order @@ -765,6 +1271,51 @@ A few bug fixes and documentation improvements, in particular: fixes `#4741 <https://github.com/coq/coq/issues/4741>`_, by Helge Bahmann). +Changes in 8.10.2 +~~~~~~~~~~~~~~~~~ + +**Kernel** + +- Fixed a critical bug of template polymorphism and nonlinear universes + (`#11128 <https://github.com/coq/coq/pull/11128>`_, + fixes `#11039 <https://github.com/coq/coq/issues/11039>`_, + by Gaëtan Gilbert). + +- Fixed an anomaly “Uncaught exception Constr.DestKO” on :g:`Inductive` + (`#11052 <https://github.com/coq/coq/pull/11052>`_, + fixes `#11048 <https://github.com/coq/coq/issues/11048>`_, + by Gaëtan Gilbert). + +- Fixed an anomaly “not enough abstractions in fix body” + (`#11014 <https://github.com/coq/coq/pull/11014>`_, + fixes `#8459 <https://github.com/coq/coq/issues/8459>`_, + by Gaëtan Gilbert). + +**Notations** + +- Fixed an 8.10 regression related to the printing of coercions associated to notations + (`#11090 <https://github.com/coq/coq/pull/11090>`_, + fixes `#11033 <https://github.com/coq/coq/issues/11033>`_, by Hugo Herbelin). + +**CoqIDE** + +- Fixed uneven dimensions of CoqIDE panels when window has been resized + (`#11070 <https://github.com/coq/coq/pull/11070>`_, + fixes 8.10-regression `#10956 <https://github.com/coq/coq/issues/10956>`_, + by Guillaume Melquiond). + +- Do not include final stops in queries + (`#11069 <https://github.com/coq/coq/pull/11069>`_, + fixes 8.10-regression `#11058 <https://github.com/coq/coq/issues/11058>`_, + by Guillaume Melquiond). + +**Infrastructure and dependencies** + +- Enable building of executables when they are running + (`#11000 <https://github.com/coq/coq/pull/11000>`_, + fixes 8.9-regression `#10728 <https://github.com/coq/coq/issues/10728>`_, + by Gaëtan Gilbert). + Version 8.9 ----------- diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 867a19efe5..f1dd7479c5 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -183,18 +183,17 @@ todo_include_todos = False nitpicky = True nitpick_ignore = [ ('token', token) for token in [ - 'tactic', - # 142 occurrences currently sort of defined in the ltac chapter, - # but is it the right place? - 'module', - 'redexpr', - 'modpath', - 'dirpath', 'collection', + 'command', + 'dirpath', + 'modpath', + 'module', + 'red_expr', + 'symbol', + 'tactic', 'term_pattern', 'term_pattern_string', - 'command', - 'symbol' ]] +]] # -- Options for HTML output ---------------------------------------------- diff --git a/doc/sphinx/dune b/doc/sphinx/dune index 353d58c676..b788fbbeed 100644 --- a/doc/sphinx/dune +++ b/doc/sphinx/dune @@ -1,8 +1,10 @@ (dirs :standard _static) -(rule (targets README.gen.rst) +(rule + (targets README.gen.rst) (deps (source_tree ../tools/coqrst) README.template.rst) (action (run ../tools/coqrst/regen_readme.py %{targets}))) -(alias (name refman-html) - (action (diff README.rst README.gen.rst))) +(rule + (alias refman-html) + (action (diff README.rst README.gen.rst))) diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index bcdf3277ad..1424b4f3e1 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -60,7 +60,7 @@ Nonetheless, the manual has some structure that is explained below. of the formalism. Chapter :ref:`themodulesystem` describes the module system. -- The second part describes the proof engine. It is divided in six +- The second part describes the proof engine. It is divided into several chapters. Chapter :ref:`vernacularcommands` presents all commands (we call them *vernacular commands*) that are not directly related to interactive proving: requests to the environment, complete or partial @@ -68,8 +68,10 @@ Nonetheless, the manual has some structure that is explained below. proofs, do multiple proofs in parallel is explained in Chapter :ref:`proofhandling`. In Chapter :ref:`tactics`, all commands that realize one or more steps of the proof are presented: we call them - *tactics*. The language to combine these tactics into complex proof - strategies is given in Chapter :ref:`ltac`. Examples of tactics + *tactics*. The legacy language to combine these tactics into complex proof + strategies is given in Chapter :ref:`ltac`. The currently experimental + language that will eventually replace Ltac is presented in + Chapter :ref:`ltac2`. Examples of tactics are described in Chapter :ref:`detailedexamplesoftactics`. Finally, the |SSR| proof language is presented in Chapter :ref:`thessreflectprooflanguage`. diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index c08a9ed0e6..4beaff70f5 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 @@ -1046,6 +1047,67 @@ between universes for inductive types in the Type hierarchy. exT_intro : forall X:Type, P X -> exType P. +.. example:: Negative occurrence (first example) + + The following inductive definition is rejected because it does not + satisfy the positivity condition: + + .. coqtop:: all + + Fail Inductive I : Prop := not_I_I (not_I : I -> False) : I. + + 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): + + .. coqtop:: none + + Unset Positivity Checking. + Inductive I : Prop := not_I_I (not_I : I -> False) : I. + Set Positivity Checking. + + .. coqtop:: all + + Definition I_not_I : I -> ~ I := fun i => + match i with not_I_I not_I => not_I end. + + .. coqtop:: in + + 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: @@ -1134,11 +1196,12 @@ 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. - This can be prevented using the ``notemplate`` attribute. + This can be prevented using the ``universes(notemplate)`` + attribute. .. warn:: Automatically declaring @ident as template polymorphic. @@ -1146,9 +1209,9 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or 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. + An inductive type can be forced to be template polymorphic using + the ``universes(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. @@ -1159,11 +1222,11 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or 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. + cause an error when using the ``universes(template)`` attribute. .. 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..a8d6d2632b 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -79,14 +79,6 @@ To build an object of type :token:`ident`, one should provide the constructor Definition half := mkRat true 1 2 (O_S 1) one_two_irred. Check half. -.. FIXME: move this to the main grammar in the spec chapter - -.. _record-named-fields-grammar: - - .. productionlist:: - record_term : {| [`field_def` ; … ; `field_def`] |} - field_def : `ident` [`binders`] := `term` - Alternatively, the following syntax allows creating objects by using named fields, as shown in this grammar. The fields do not have to be in any particular order, nor do they have to be all present if the missing ones can be inferred or prompted for @@ -163,10 +155,11 @@ available: .. _record_projections_grammar: - .. productionlist:: terms - projection : `term` `.` ( `qualid` ) - : `term` `.` ( `qualid` `arg` … `arg` ) - : `term` `.` ( @`qualid` `term` … `term` ) + .. insertgram term_projection term_projection + + .. productionlist:: coq + term_projection : `term0` .( `qualid` `args_opt` ) + : `term0` .( @ `qualid` `term1_list_opt` ) Syntax of Record projections @@ -188,7 +181,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 +236,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 +295,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 +474,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 +487,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 +498,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 +507,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 +520,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 +555,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:: @@ -591,7 +584,7 @@ Advanced recursive functions The following experimental command is available when the ``FunInd`` library has been loaded via ``Require Import FunInd``: -.. cmd:: Function @ident {* @binder} { @decrease_annot } : @type := @term +.. cmd:: Function @ident {* @binder} { @fixannot } : @type := @term This command can be seen as a generalization of ``Fixpoint``. It is actually a wrapper for several ways of defining a function *and other useful related @@ -600,16 +593,11 @@ The following experimental command is available when the ``FunInd`` library has The meaning of this declaration is to define a function ident, similarly to ``Fixpoint``. Like in ``Fixpoint``, the decreasing argument must be given (unless the function is not recursive), but it might not - necessarily be *structurally* decreasing. The point of the :n:`{ @decrease_annot }` annotation + necessarily be *structurally* decreasing. The point of the :n:`{ @fixannot }` annotation is to name the decreasing argument *and* to describe which kind of decreasing criteria must be used to ensure termination of recursive calls. - .. productionlist:: - decrease_annot : struct `ident` - : measure `term` `ident` - : wf `term` `ident` - The ``Function`` construction also enjoys the ``with`` extension to define mutually recursive definitions. However, this feature does not work for non structurally recursive functions. @@ -874,7 +862,7 @@ Sections create local contexts which can be shared across multiple definitions. :name: Let Fixpoint :undocumented: - .. cmdv:: Let CoFixpoint @ident @cofix_body {* with @cofix_body} + .. cmdv:: Let CoFixpoint @ident @fix_body {* with @fix_body} :name: Let CoFixpoint :undocumented: @@ -1311,7 +1299,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 +1572,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 +1745,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 +1815,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 +1832,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 +1847,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 +1858,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 +1868,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 +1915,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 +1950,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 +1958,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 +1987,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 @@ -2013,10 +2003,11 @@ applied to an unknown structure instance (an implicit argument) and a value. The complete documentation of canonical structures can be found in :ref:`canonicalstructures`; here only a simple example is given. -.. cmd:: Canonical {? Structure } @qualid +.. cmd:: {? Local | #[local] } Canonical {? Structure } @qualid This command declares :token:`qualid` as a canonical instance of a - structure (a record). + structure (a record). When the :g:`#[local]` attribute is given the effect + stops at the end of the :g:`Section` containig it. Assume that :token:`qualid` denotes an object ``(Build_struct`` |c_1| … |c_n| ``)`` in the structure :g:`struct` of which the fields are |x_1|, …, |x_n|. @@ -2079,16 +2070,18 @@ in :ref:`canonicalstructures`; here only a simple example is given. See :ref:`canonicalstructures` for a more realistic example. - .. cmdv:: Canonical {? Structure } @ident {? : @type } := @term + .. cmdv:: {? Local | #[local] } Canonical {? Structure } @ident {? : @type } := @term This is equivalent to a regular definition of :token:`ident` followed by the declaration :n:`Canonical @ident`. -.. cmd:: Print Canonical Projections +.. cmd:: Print Canonical Projections {* @ident} This displays the list of global names that are components of some canonical structure. For each of them, the canonical structure of - which it is a projection is indicated. + which it is a projection is indicated. If constants are given as + its arguments, only the unification rules that involve or are + synthesized from simultaneously all given constants will be shown. .. example:: @@ -2098,10 +2091,15 @@ in :ref:`canonicalstructures`; here only a simple example is given. Print Canonical Projections. + .. coqtop:: all + + Print Canonical Projections nat. + .. note:: - The last line would not show up if the corresponding projection (namely - :g:`Prf_equiv`) were annotated as not canonical, as described above. + The last line in the first example would not show up if the + corresponding projection (namely :g:`Prf_equiv`) were annotated as not + canonical, as described above. Implicit types of variables ~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2269,11 +2267,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 +2283,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 +2295,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. @@ -2321,6 +2319,18 @@ Printing universes Existential variables --------------------- +.. insertgram term_evar evar_binding + +.. productionlist:: coq + term_evar : ?[ `ident` ] + : ?[ ?`ident` ] + : ?`ident` `evar_bindings_opt` + evar_bindings_opt : @{ `evar_bindings_semi` } + : `empty` + evar_bindings_semi : `evar_bindings_semi` ; `evar_binding` + : `evar_binding` + evar_binding : `ident` := `term` + |Coq| terms can include existential variables which represents unknown subterms to eventually be replaced by actual subterms. @@ -2355,7 +2365,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 +2389,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 +2419,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 +2472,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..3cc101d06b 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -52,7 +52,7 @@ Comments They can contain any character. However, embedded :token:`string` literals must be correctly closed. Comments are treated as blanks. -Identifiers and field identifiers +Identifiers Identifiers, written :token:`ident`, are sequences of letters, digits, ``_`` and ``'``, that do not start with a digit or ``'``. That is, they are recognized by the following grammar (except that the string ``_`` is reserved; @@ -60,7 +60,6 @@ Identifiers and field identifiers .. productionlist:: coq ident : `first_letter`[`subsequent_letter`…`subsequent_letter`] - field : .`ident` first_letter : a..z ∣ A..Z ∣ _ ∣ `unicode_letter` subsequent_letter : `first_letter` ∣ 0..9 ∣ ' ∣ `unicode_id_part` @@ -71,10 +70,6 @@ Identifiers and field identifiers symbols and non-breaking space. :production:`unicode_id_part` non-exhaustively includes symbols for prime letters and subscripts. - Field identifiers, written :token:`field`, are identifiers prefixed by - `.` (dot) with no blank between the dot and the identifier. They are used in - the syntax of qualified identifiers. - Numerals Numerals are sequences of digits with an optional fractional part and exponent, optionally preceded by a minus sign. :token:`int` is an integer; @@ -144,62 +139,50 @@ presentation of Cic is given in Chapter :ref:`calculusofinductiveconstructions`. are given in Chapter :ref:`extensionsofgallina`. How to customize the syntax is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`. -.. productionlist:: coq - term : forall `binders` , `term` - : fun `binders` => `term` - : fix `fix_bodies` - : cofix `cofix_bodies` - : let `ident` [`binders`] [: `term`] := `term` in `term` - : let fix `fix_body` in `term` - : let cofix `cofix_body` in `term` - : let ( [`name` , … , `name`] ) [`dep_ret_type`] := `term` in `term` - : let ' `pattern` [in `term`] := `term` [`return_type`] in `term` - : if `term` [`dep_ret_type`] then `term` else `term` - : `term` : `term` - : `term` <: `term` - : `term` :> - : `term` -> `term` - : `term` `arg` … `arg` - : @ `qualid` [`term` … `term`] - : `term` % `ident` - : match `match_item` , … , `match_item` [`return_type`] with - : [[|] `equation` | … | `equation`] end - : `qualid` - : `sort` - : `num` - : _ - : ( `term` ) - arg : `term` - : ( `ident` := `term` ) - binders : `binder` … `binder` - binder : `name` - : ( `name` … `name` : `term` ) - : ( `name` [: `term`] := `term` ) - : ' `pattern` - name : `ident` | _ - qualid : `ident` | `qualid` `field` - sort : SProp | Prop | Set | Type - fix_bodies : `fix_body` - : `fix_body` with `fix_body` with … with `fix_body` for `ident` - cofix_bodies : `cofix_body` - : `cofix_body` with `cofix_body` with … with `cofix_body` for `ident` - fix_body : `ident` `binders` [`annotation`] [: `term`] := `term` - cofix_body : `ident` [`binders`] [: `term`] := `term` - annotation : { struct `ident` } - match_item : `term` [as `name`] [in `qualid` [`pattern` … `pattern`]] - dep_ret_type : [as `name`] `return_type` - return_type : return `term` - equation : `mult_pattern` | … | `mult_pattern` => `term` - mult_pattern : `pattern` , … , `pattern` - pattern : `qualid` `pattern` … `pattern` - : @ `qualid` `pattern` … `pattern` - : `pattern` as `ident` - : `pattern` % `ident` - : `qualid` - : _ - : `num` - : ( `pattern` | … | `pattern` ) +.. insertgram term binders_opt +.. productionlist:: coq + term : forall `open_binders` , `term` + : fun `open_binders` => `term` + : `term_let` + : if `term` `as_return_type_opt` then `term` else `term` + : `term_fix` + : `term100` + term100 : `term_cast` + : `term10` + term10 : `term1` `args` + : @ `qualid` `universe_annot_opt` `term1_list_opt` + : `term1` + args : `args` `arg` + : `arg` + arg : ( `ident` := `term` ) + : `term1` + term1_list_opt : `term1_list_opt` `term1` + : `empty` + empty : + term1 : `term_projection` + : `term0` % `ident` + : `term0` + args_opt : `args` + : `empty` + term0 : `qualid` `universe_annot_opt` + : `sort` + : `numeral` + : `string` + : _ + : `term_evar` + : `term_match` + : ( `term` ) + : {| `fields_def` |} + : `{ `term` } + : `( `term` ) + : ltac : ( `ltac_expr` ) + fields_def : `field_def` ; `fields_def` + : `field_def` + : `empty` + field_def : `qualid` `binders_opt` := `term` + binders_opt : `binders` + : `empty` Types ----- @@ -213,6 +196,13 @@ of types inside the syntactic class :token:`term`. Qualified identifiers and simple identifiers -------------------------------------------- +.. insertgram qualid field + +.. productionlist:: coq + qualid : `qualid` `field` + : `ident` + field : .`ident` + *Qualified identifiers* (:token:`qualid`) denote *global constants* (definitions, lemmas, theorems, remarks or facts), *global variables* (parameters or axioms), *inductive types* or *constructors of inductive @@ -220,11 +210,15 @@ types*. *Simple identifiers* (or shortly :token:`ident`) are a syntactic subset of qualified identifiers. Identifiers may also denote *local variables*, while qualified identifiers do not. -Numerals --------- +Field identifiers, written :token:`field`, are identifiers prefixed by +`.` (dot) with no blank between the dot and the identifier. + -Numerals have no definite semantics in the calculus. They are mere -notations that can be bound to objects through the notation mechanism +Numerals and strings +-------------------- + +Numerals and strings have no predefined semantics in the calculus. They are +merely notations that can be bound to objects through the notation mechanism (see Chapter :ref:`syntaxextensionsandinterpretationscopes` for details). Initially, numerals are bound to Peano’s representation of natural numbers (see :ref:`datatypes`). @@ -243,6 +237,35 @@ numbers (see :ref:`datatypes`). Sorts ----- +.. insertgram sort universe_level + +.. productionlist:: coq + sort : Set + : Prop + : SProp + : Type + : Type @{ _ } + : Type @{ `universe` } + universe : max ( `universe_exprs_comma` ) + : `universe_expr` + universe_exprs_comma : `universe_exprs_comma` , `universe_expr` + : `universe_expr` + universe_expr : `universe_name` `universe_increment_opt` + universe_name : `qualid` + : Set + : Prop + universe_increment_opt : + `num` + : `empty` + universe_annot_opt : @{ `universe_levels_opt` } + : `empty` + universe_levels_opt : `universe_levels_opt` `universe_level` + : `empty` + universe_level : Set + : Prop + : Type + : _ + : `qualid` + There are four sorts :g:`SProp`, :g:`Prop`, :g:`Set` and :g:`Type`. - :g:`SProp` is the universe of *definitionally irrelevant @@ -266,6 +289,35 @@ More on sorts can be found in Section :ref:`sorts`. Binders ------- +.. insertgram open_binders exclam_opt + +.. productionlist:: coq + open_binders : `names` : `term` + : `binders` + names : `names` `name` + : `name` + name : _ + : `ident` + binders : `binders` `binder` + : `binder` + binder : `name` + : ( `names` : `term` ) + : ( `name` `colon_term_opt` := `term` ) + : { `name` } + : { `names` `colon_term_opt` } + : `( `typeclass_constraints_comma` ) + : `{ `typeclass_constraints_comma` } + : ' `pattern0` + : ( `name` : `term` | `term` ) + typeclass_constraints_comma : `typeclass_constraints_comma` , `typeclass_constraint` + : `typeclass_constraint` + typeclass_constraint : `exclam_opt` `term` + : { `name` } : `exclam_opt` `term` + : `name` : `exclam_opt` `term` + exclam_opt : ! + : `empty` + + Various constructions such as :g:`fun`, :g:`forall`, :g:`fix` and :g:`cofix` *bind* variables. A binding is represented by an identifier. If the binding variable is not used in the expression, the identifier can be replaced by the @@ -291,8 +343,8 @@ the case of a single sequence of bindings sharing the same type (e.g.: .. index:: fun ... => ... -Abstractions ------------- +Abstractions: fun +----------------- The expression :n:`fun @ident : @type => @term` defines the *abstraction* of the variable :token:`ident`, of type :token:`type`, over the term @@ -313,8 +365,8 @@ Section :ref:`let-in`). .. index:: forall -Products --------- +Products: forall +---------------- The expression :n:`forall @ident : @type, @term` denotes the *product* of the variable :token:`ident` of type :token:`type`, over the term :token:`term`. @@ -359,6 +411,14 @@ Section :ref:`explicit-applications`). Type cast --------- +.. insertgram term_cast term_cast + +.. productionlist:: coq + term_cast : `term10` <: `term` + : `term10` <<: `term` + : `term10` : `term` + : `term10` :> + The expression :n:`@term : @type` is a type cast expression. It enforces the type of :token:`term` to be :token:`type`. @@ -384,6 +444,22 @@ guess the missing piece of information. Let-in definitions ------------------ +.. insertgram term_let names_comma + +.. productionlist:: coq + term_let : let `name` `colon_term_opt` := `term` in `term` + : let `name` `binders` `colon_term_opt` := `term` in `term` + : let `single_fix` in `term` + : let `names_tuple` `as_return_type_opt` := `term` in `term` + : let ' `pattern` := `term` `return_type_opt` in `term` + : let ' `pattern` in `pattern` := `term` `return_type` in `term` + colon_term_opt : : `term` + : `empty` + names_tuple : ( `names_comma` ) + : () + names_comma : `names_comma` , `name` + : `name` + :n:`let @ident := @term in @term’` denotes the local binding of :token:`term` to the variable :token:`ident` in :token:`term`’. There is a syntactic sugar for let-in @@ -392,8 +468,60 @@ stands for :n:`let @ident := fun {+ @binder} => @term in @term’`. .. index:: match ... with ... -Definition by case analysis ---------------------------- +Definition by cases: match +-------------------------- + +.. insertgram term_match record_pattern + +.. productionlist:: coq + term_match : match `case_items_comma` `return_type_opt` with `or_opt` `eqns_or_opt` end + case_items_comma : `case_items_comma` , `case_item` + : `case_item` + return_type_opt : `return_type` + : `empty` + as_return_type_opt : `as_name_opt` `return_type` + : `empty` + return_type : return `term100` + case_item : `term100` `as_name_opt` `in_opt` + as_name_opt : as `name` + : `empty` + in_opt : in `pattern` + : `empty` + or_opt : | + : `empty` + eqns_or_opt : `eqns_or` + : `empty` + eqns_or : `eqns_or` | `eqn` + : `eqn` + eqn : `patterns_comma_list_or` => `term` + patterns_comma_list_or : `patterns_comma_list_or` | `patterns_comma` + : `patterns_comma` + patterns_comma : `patterns_comma` , `pattern` + : `pattern` + pattern : `pattern10` : `term` + : `pattern10` + pattern10 : `pattern1` as `name` + : `pattern1_list` + : @ `qualid` `pattern1_list_opt` + : `pattern1` + pattern1_list : `pattern1_list` `pattern1` + : `pattern1` + pattern1_list_opt : `pattern1_list` + : `empty` + pattern1 : `pattern0` % `ident` + : `pattern0` + pattern0 : `qualid` + : {| `record_patterns_opt` |} + : _ + : ( `patterns_or` ) + : `numeral` + : `string` + patterns_or : `patterns_or` | `pattern` + : `pattern` + record_patterns_opt : `record_patterns_opt` ; `record_pattern` + : `record_pattern` + : `empty` + record_pattern : `qualid` := `pattern` Objects of inductive types can be destructured by a case-analysis construction called *pattern matching* expression. A pattern matching @@ -403,11 +531,11 @@ to apply specific treatments accordingly. This paragraph describes the basic form of pattern matching. See Section :ref:`Mult-match` and Chapter :ref:`extendedpatternmatching` for the description of the general form. The basic form of pattern matching is characterized -by a single :token:`match_item` expression, a :token:`mult_pattern` restricted to a +by a single :token:`case_item` expression, a :token:`patterns_comma` restricted to a single :token:`pattern` and :token:`pattern` restricted to the form :n:`@qualid {* @ident}`. -The expression match ":token:`term`:math:`_0` :token:`return_type` with +The expression match ":token:`term`:math:`_0` :token:`return_type_opt` with :token:`pattern`:math:`_1` => :token:`term`:math:`_1` :math:`|` … :math:`|` :token:`pattern`:math:`_n` => :token:`term`:math:`_n` end" denotes a *pattern matching* over the term :token:`term`:math:`_0` (expected to be @@ -417,10 +545,10 @@ expression. Each of :token:`pattern`:math:`_i` has a form :token:`qualid` :token:`ident` where :token:`qualid` must denote a constructor. There should be exactly one branch for every constructor of :math:`I`. -The :token:`return_type` expresses the type returned by the whole match +The :token:`return_type_opt` expresses the type returned by the whole match expression. There are several cases. In the *non dependent* case, all -branches have the same type, and the :token:`return_type` is the common type of -branches. In this case, :token:`return_type` can usually be omitted as it can be +branches have the same type, and the :token:`return_type_opt` is the common type of +branches. In this case, :token:`return_type_opt` can usually be omitted as it can be inferred from the type of the branches [2]_. In the *dependent* case, there are three subcases. In the first subcase, @@ -520,8 +648,30 @@ Sections :ref:`if-then-else` and :ref:`irrefutable-patterns`). single: fix single: cofix -Recursive functions -------------------- +Recursive and co-recursive functions: fix and cofix +--------------------------------------------------- + +.. insertgram term_fix term1_extended_opt + +.. productionlist:: coq + term_fix : `single_fix` + : `single_fix` with `fix_bodies` for `ident` + single_fix : fix `fix_body` + : cofix `fix_body` + fix_bodies : `fix_bodies` with `fix_body` + : `fix_body` + fix_body : `ident` `binders_opt` `fixannot_opt` `colon_term_opt` := `term` + fixannot_opt : `fixannot` + : `empty` + fixannot : { struct `ident` } + : { wf `term1_extended` `ident` } + : { measure `term1_extended` `ident_opt` `term1_extended_opt` } + term1_extended : `term1` + : @ `qualid` `universe_annot_opt` + ident_opt : `ident` + : `empty` + term1_extended_opt : `term1_extended` + : `empty` The expression “``fix`` :token:`ident`:math:`_1` :token:`binder`:math:`_1` ``:`` :token:`type`:math:`_1` ``:=`` :token:`term`:math:`_1` ``with … with`` @@ -547,6 +697,8 @@ syntax: :n:`let fix @ident @binders := @term in` stands for The Vernacular ============== +.. insertgramXX vernac ident_opt2 + .. productionlist:: coq decorated-sentence : [ `decoration` … `decoration` ] `sentence` sentence : `assumption` @@ -568,7 +720,7 @@ The Vernacular ind_body : `ident` [`binders`] : `term` := : [[|] `ident` [`binders`] [:`term`] | … | `ident` [`binders`] [:`term`]] fixpoint : Fixpoint `fix_body` with … with `fix_body` . - : CoFixpoint `cofix_body` with … with `cofix_body` . + : CoFixpoint `fix_body` with … with `fix_body` . assertion : `assertion_keyword` `ident` [`binders`] : `term` . assertion_keyword : Theorem | Lemma : Remark | Fact @@ -779,7 +931,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 +1108,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 +1143,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 +1545,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 +1622,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 @@ -1503,19 +1655,20 @@ Each attribute has a name (an identifier) and may have a value. A value is either a :token:`string` (in which case it is specified with an equal ``=`` sign), or a list of attributes, enclosed within brackets. -Currently, -the following attributes names are recognized: +Some attributes are specific to a command, and so are described with +that command. Currently, the following attributes are recognized by a +variety of commands: -``monomorphic``, ``polymorphic`` - Take no value, analogous to the ``Monomorphic`` and ``Polymorphic`` flags - (see :ref:`polymorphicuniverses`). +``universes(monomorphic)``, ``universes(polymorphic)`` + Equivalent to the ``Monomorphic`` and + ``Polymorphic`` flags (see :ref:`polymorphicuniverses`). ``program`` - Takes no value, analogous to the ``Program`` flag + Takes no value, equivalent to the ``Program`` flag (see :ref:`programs`). ``global``, ``local`` - Take no value, analogous to the ``Global`` and ``Local`` flags + Take no value, equivalent to the ``Global`` and ``Local`` flags (see :ref:`controlling-locality-of-commands`). ``deprecated`` @@ -1556,6 +1709,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..d4a61425e1 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,127 @@ 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``. + +.. warning:: + + When writing a custom build system, be aware that ``coqdep`` only + produces dependencies related to ``.vos`` and ``.vok`` if the + ``-vos`` command line flag is passed. This is to maintain + compatibility with dune (see `ocaml/dune#2642 on github + <https://github.com/ocaml/dune/issues/2842>`_). + +**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`` and an empty file ``foo.vok`` +are 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 79eddbd3b5..b2b426ada5 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -127,7 +127,7 @@ mode but it can also be used in toplevel definitions as shown below. : gfail [`natural`] [`message_token` ... `message_token`] : fresh [ `component` … `component` ] : context `ident` [`term`] - : eval `redexpr` in `term` + : eval `red_expr` in `term` : type of `term` : constr : `term` : uconstr : `term` @@ -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 ~~~~~~~ @@ -858,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:: @@ -984,9 +986,9 @@ Computing in a constr Evaluation of a term can be performed with: -.. tacn:: eval @redexpr in @term +.. tacn:: eval @red_expr in @term - where :n:`@redexpr` is a reduction tactic among :tacn:`red`, :tacn:`hnf`, + where :n:`@red_expr` is a reduction tactic among :tacn:`red`, :tacn:`hnf`, :tacn:`compute`, :tacn:`simpl`, :tacn:`cbv`, :tacn:`lazy`, :tacn:`unfold`, :tacn:`fold`, :tacn:`pattern`. @@ -1640,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. @@ -1664,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 @@ -1689,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 @@ -1773,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..dd80b29bda 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -1,12 +1,12 @@ .. _ltac2: +Ltac2 +===== + .. coqtop:: none From Ltac2 Require Import Ltac2. -Ltac2 -===== - The Ltac tactic language is probably one of the ingredients of the success of Coq, yet it is at the same time its Achilles' heel. Indeed, Ltac: @@ -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 57a54bc0ad..6884b6e998 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -535,7 +535,7 @@ Requesting information eexists ?[n]. Show n. - .. cmdv:: Show Proof + .. cmdv:: Show Proof {? Diffs {? removed } } :name: Show Proof Displays the proof term generated by the tactics @@ -544,6 +544,12 @@ Requesting information 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 @@ -624,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 @@ -795,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..853ddfd6dc 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1513,7 +1513,7 @@ In a goal like the following:: ============= m < 5 + n -The tactic ``abstract: abs n`` first generalizes the goal with respect ton +The tactic :g:`abstract: abs n` first generalizes the goal with respect to :g:`n` (that is not visible to the abstract constant abs) and then assigns abs. The resulting goal is:: @@ -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 @@ -4061,6 +4071,7 @@ which the function is supplied: :name: congr This tactic: + + checks that the goal is a Leibniz equality; + matches both sides of this equality with “term applied to some arguments”, inferring the right number of arguments from the goal and the type of term. This may expand some definitions or fixpoints; + generates the subgoals corresponding to pairwise equalities of the arguments present in the goal. @@ -4208,7 +4219,7 @@ in the second column. ``ident`` in all the occurrences of ``term2`` * - ``term1 as ident in term2`` - ``term 1`` - - in all the subterms identified by ``ident` + - in all the subterms identified by ``ident`` in all the occurrences of ``term2[term 1 /ident]`` The rewrite tactic supports two more patterns obtained prefixing the @@ -5013,7 +5024,7 @@ mechanism: Coercion is_true (b : bool) := b = true. This allows any boolean formula ``b`` to be used in a context where |Coq| -would expect a proposition, e.g., after ``Lemma … : ``. It is then +would expect a proposition, e.g., after ``Lemma … :``. It is then interpreted as ``(is_true b)``, i.e., the proposition ``b = true``. Coercions are elided by the pretty-printer, so they are essentially transparent to the user. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 78753fc053..53cfb973d4 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. @@ -555,12 +555,14 @@ Applying theorems This tactic applies to any goal. It behaves like :tacn:`exact` with a big difference: the user can leave some holes (denoted by ``_`` or :n:`(_ : @type)`) in the term. :tacn:`refine` will generate as many - subgoals as there are holes in the term. The type of holes must be either - synthesized by the system or declared by an explicit cast + subgoals as there are remaining holes in the elaborated term. The type + of holes must be either synthesized by the system or declared by an explicit cast like ``(_ : nat -> Prop)``. Any subgoal that occurs in other subgoals is automatically shelved, as if calling - :tacn:`shelve_unifiable`. This low-level tactic can be - useful to advanced users. + :tacn:`shelve_unifiable`. The produced subgoals (shelved or not) + are *not* candidates for typeclass resolution, even if they have a type-class + type as conclusion, letting the user control when and how typeclass resolution + is launched on them. This low-level tactic can be useful to advanced users. .. example:: @@ -611,8 +613,9 @@ Applying theorems .. tacv:: simple notypeclasses refine @term :name: simple notypeclasses refine - This tactic behaves like :tacn:`simple refine` except it performs type checking - without resolution of typeclasses. + This tactic behaves like the combination of :tacn:`simple refine` and + :tacn:`notypeclasses refine`: it performs type checking without resolution of + typeclasses, does not perform beta reductions or shelve the subgoals. .. flag:: Debug Unification @@ -685,6 +688,28 @@ Applying theorems instantiate (see :ref:`Existential-Variables`). The instantiation is intended to be found later in the proof. + .. tacv:: rapply @term + :name: rapply + + The tactic :tacn:`rapply` behaves like :tacn:`eapply` but it + uses the proof engine of :tacn:`refine` for dealing with + existential variables, holes, and conversion problems. This may + result in slightly different behavior regarding which conversion + problems are solvable. However, like :tacn:`apply` but unlike + :tacn:`eapply`, :tacn:`rapply` will fail if there are any holes + which remain in :n:`@term` itself after typechecking and + typeclass resolution but before unification with the goal. More + technically, :n:`@term` is first parsed as a + :production:`constr` rather than as a :production:`uconstr` or + :production:`open_constr` before being applied to the goal. Note + that :tacn:`rapply` prefers to instantiate as many hypotheses of + :n:`@term` as possible. As a result, if it is possible to apply + :n:`@term` to arbitrarily many arguments without getting a type + error, :tacn:`rapply` will loop. + + Note that you need to :n:`Require Import Coq.Program.Tactics` to + make use of :tacn:`rapply`. + .. tacv:: simple apply @term. This behaves like :tacn:`apply` but it reasons modulo conversion only on subterms @@ -804,11 +829,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 +1552,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 +2325,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 @@ -2824,11 +2849,15 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. .. tacv:: cutrewrite <- (@term = @term’) :name: cutrewrite - This tactic is deprecated. It can be replaced by :n:`enough (@term = @term’) as <-`. + .. deprecated:: 8.5 + + This tactic can be replaced by :n:`enough (@term = @term’) as <-`. .. tacv:: cutrewrite -> (@term = @term’) - This tactic is deprecated. It can be replaced by :n:`enough (@term = @term’) as ->`. + .. deprecated:: 8.5 + + This tactic can be replaced by :n:`enough (@term = @term’) as ->`. .. tacn:: subst @ident @@ -2862,26 +2891,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 +3115,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 +3132,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 +3300,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 @@ -3281,11 +3310,13 @@ the conversion in hypotheses :n:`{+ @ident}`. defined transparent constant or local definition (see :ref:`gallina-definitions` and :ref:`vernac-controlling-the-reduction-strategies`). The tactic - :tacn:`unfold` applies the :math:`\delta` rule to each occurrence of - the constant to which :n:`@qualid` refers in the current goal and - then replaces it with its :math:`\beta`:math:`\iota`-normal form. + :tacn:`unfold` applies the :math:`\delta` rule to each occurrence + of the constant to which :n:`@qualid` refers in the current goal + and then replaces it with its :math:`\beta\iota\zeta`-normal form. + Use the general reduction tactics if you want to avoid this final + reduction, for instance :n:`cbv delta [@qualid]`. - .. exn:: @qualid does not denote an evaluable constant. + .. exn:: Cannot coerce @qualid to an evaluable reference. This error is frequent when trying to unfold something that has defined as an inductive type (or constructor) and not as a @@ -3548,7 +3579,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 +3607,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 +3751,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 +4227,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 @@ -4237,7 +4268,13 @@ some incompatibilities. .. tacv:: firstorder using {+ @qualid} - Adds lemmas :n:`{+ @qualid}` to the proof-search environment. If :n:`@qualid` + .. deprecated:: 8.3 + + Use the syntax below instead (with commas). + +.. tacv:: firstorder using {+, @qualid} + + Adds lemmas :n:`{+, @qualid}` to the proof-search environment. If :n:`@qualid` refers to an inductive type, it is the collection of its constructors which are added to the proof-search environment. @@ -4246,7 +4283,7 @@ some incompatibilities. Adds lemmas from :tacn:`auto` hint bases :n:`{+ @ident}` to the proof-search environment. -.. tacv:: firstorder @tactic using {+ @qualid} with {+ @ident} +.. tacv:: firstorder @tactic using {+, @qualid} with {+ @ident} This combines the effects of the different variants of :tacn:`firstorder`. @@ -4316,7 +4353,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 @@ -4887,6 +4924,8 @@ Performance-oriented tactic variants .. tacv:: convert_concl_no_check @term :name: convert_concl_no_check + .. deprecated:: 8.11 + Deprecated old name for :tacn:`change_no_check`. Does not support any of its variants. diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 843459b723..89b24ea8a3 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -195,7 +195,7 @@ Requests to the environment (see Section :ref:`invocation-of-tactics`). -.. cmd:: Eval @redexpr in @term +.. cmd:: Eval @red_expr in @term This command performs the specified reduction on :n:`@term`, and displays the resulting term with its type. The term to be reduced may depend on @@ -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) @@ -1146,7 +1146,7 @@ described first. Print all the currently non-transparent strategies. -.. cmd:: Declare Reduction @ident := @redexpr +.. cmd:: Declare Reduction @ident := @red_expr This command allows giving a short name to a reduction expression, for instance ``lazy beta delta [foo bar]``. This short name can then be used @@ -1158,7 +1158,7 @@ described first. functor applications will be rejected if these declarations are not local. The name :n:`@ident` cannot be used directly as an Ltac tactic, but nothing prevents the user from also performing a - :n:`Ltac @ident := @redexpr`. + :n:`Ltac @ident := @red_expr`. .. seealso:: :ref:`performingcomputations` @@ -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..dbe714c388 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -871,7 +871,7 @@ notations are given below. The optional :production:`scope` is described in : Inductive `ind_body` [`decl_notation`] with … with `ind_body` [`decl_notation`]. : CoInductive `ind_body` [`decl_notation`] with … with `ind_body` [`decl_notation`]. : Fixpoint `fix_body` [`decl_notation`] with … with `fix_body` [`decl_notation`]. - : CoFixpoint `cofix_body` [`decl_notation`] with … with `cofix_body` [`decl_notation`]. + : CoFixpoint `fix_body` [`decl_notation`] with … with `fix_body` [`decl_notation`]. : [Local] Declare Custom Entry `ident`. decl_notation : [where `string` := `term` [: `scope`] and … and `string` := `term` [: `scope`]]. modifiers : `modifier`, … , `modifier` @@ -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 |