diff options
Diffstat (limited to 'doc/sphinx')
56 files changed, 2934 insertions, 2306 deletions
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index 549598b187..0802b5d0b4 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -3,8 +3,8 @@ ============================= .. - README.rst is auto-generated from README.template.rst and the coqrst docs; - use ``doc/tools/coqrst/regen_readme.py`` to rebuild it. + README.rst is auto-generated from README.template.rst and the coqrst/*.py files + (in particular coqdomain.py). Use ``doc/tools/coqrst/regen_readme.py`` to rebuild it. Coq's reference manual is written in `reStructuredText <http://www.sphinx-doc.org/en/master/usage/restructuredtext/basics.html>`_ (“reST”), and compiled with `Sphinx <http://www.sphinx-doc.org/en/master/>`_. @@ -34,14 +34,14 @@ Names (link targets) are auto-generated for most simple objects, though they can Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms). Undocumented objects should have the ``:undocumented:`` flag instead, as shown above. When multiple objects have a single description, they can be grouped into a single object, like this (semicolons can be used to separate the names of the objects; names starting with ``_`` will be omitted from the indexes):: - .. cmdv:: Lemma @ident {? @binders} : @type - Remark @ident {? @binders} : @type - Fact @ident {? @binders} : @type - Corollary @ident {? @binders} : @type - Proposition @ident {? @binders} : @type + .. cmdv:: Lemma @ident {* @binder } : @type + Remark @ident {* @binder } : @type + Fact @ident {* @binder } : @type + Corollary @ident {* @binder } : @type + Proposition @ident {* @binder } : @type :name: Lemma; Remark; Fact; Corollary; Proposition - These commands are all synonyms of :n:`Theorem @ident {? @binders } : type`. + These commands are all synonyms of :n:`Theorem @ident {* @binder } : type`. Notations --------- @@ -89,10 +89,15 @@ Objects Here is the list of all objects of the Coq domain (The symbol :black_nib: indicates an object whose signature can be written using the notations DSL): +``.. attr::`` :black_nib: An attribute. + Example:: + + .. attr:: local + ``.. cmd::`` :black_nib: A Coq command. Example:: - .. cmd:: Infix "@symbol" := @term ({+, @modifier}). + .. cmd:: Infix @string := @one_term {? ( {+, @syntax_modifier } ) } {? : @ident } This command is equivalent to :n:`…`. @@ -143,22 +148,24 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica application of a tactic. ``.. prodn::`` A grammar production. - This is useful if you intend to document individual grammar productions. - Otherwise, use Sphinx's `production lists + Use ``.. prodn`` to document grammar productions instead of Sphinx + `production lists <http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_. - Unlike ``.. productionlist``\ s, this directive accepts notation syntax. - - - Usage:: - - .. prodn:: token += production - .. prodn:: token ::= production + prodn displays multiple productions together with alignment similar to ``.. productionlist``, + however unlike ``.. productionlist``\ s, this directive accepts notation syntax. Example:: - .. prodn:: term += let: @pattern := @term in @term .. prodn:: occ_switch ::= { {? {| + | - } } {* @num } } + term += let: @pattern := @term in @term + | second_production + + The first line defines "occ_switch", which must be unique in the document. The second + references and expands the definition of "term", whose main definition is elsewhere + in the document. The third form is for continuing the + definition of a nonterminal when it has multiple productions. It leaves the first + column in the output blank. ``.. table::`` :black_nib: A Coq table, i.e. a setting that is a set of values. Example:: diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst index 51d5174567..5762967c36 100644 --- a/doc/sphinx/README.template.rst +++ b/doc/sphinx/README.template.rst @@ -3,8 +3,8 @@ ============================= .. - README.rst is auto-generated from README.template.rst and the coqrst docs; - use ``doc/tools/coqrst/regen_readme.py`` to rebuild it. + README.rst is auto-generated from README.template.rst and the coqrst/*.py files + (in particular coqdomain.py). Use ``doc/tools/coqrst/regen_readme.py`` to rebuild it. Coq's reference manual is written in `reStructuredText <http://www.sphinx-doc.org/en/master/usage/restructuredtext/basics.html>`_ (“reST”), and compiled with `Sphinx <http://www.sphinx-doc.org/en/master/>`_. @@ -34,14 +34,14 @@ Names (link targets) are auto-generated for most simple objects, though they can Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms). Undocumented objects should have the ``:undocumented:`` flag instead, as shown above. When multiple objects have a single description, they can be grouped into a single object, like this (semicolons can be used to separate the names of the objects; names starting with ``_`` will be omitted from the indexes):: - .. cmdv:: Lemma @ident {? @binders} : @type - Remark @ident {? @binders} : @type - Fact @ident {? @binders} : @type - Corollary @ident {? @binders} : @type - Proposition @ident {? @binders} : @type + .. cmdv:: Lemma @ident {* @binder } : @type + Remark @ident {* @binder } : @type + Fact @ident {* @binder } : @type + Corollary @ident {* @binder } : @type + Proposition @ident {* @binder } : @type :name: Lemma; Remark; Fact; Corollary; Proposition - These commands are all synonyms of :n:`Theorem @ident {? @binders } : type`. + These commands are all synonyms of :n:`Theorem @ident {* @binder } : type`. Notations --------- diff --git a/doc/sphinx/_static/ansi-dark.css b/doc/sphinx/_static/ansi-dark.css index bbace7c553..f02f522bdd 100644 --- a/doc/sphinx/_static/ansi-dark.css +++ b/doc/sphinx/_static/ansi-dark.css @@ -1,7 +1,7 @@ /************************************************************************/ /* * The Coq Proof Assistant / The Coq Development Team */ -/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */ -/* <O___,, * (see CREDITS file for the list of authors) */ +/* v * Copyright INRIA, CNRS and contributors */ +/* <O___,, * (see version control and CREDITS file for authors & dates) */ /* \VV/ **************************************************************/ /* // * This file is distributed under the terms of the */ /* * GNU Lesser General Public License Version 2.1 */ diff --git a/doc/sphinx/_static/ansi.css b/doc/sphinx/_static/ansi.css index b3b5341166..2a618f68d2 100644 --- a/doc/sphinx/_static/ansi.css +++ b/doc/sphinx/_static/ansi.css @@ -1,7 +1,7 @@ /************************************************************************/ /* * The Coq Proof Assistant / The Coq Development Team */ -/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */ -/* <O___,, * (see CREDITS file for the list of authors) */ +/* v * Copyright INRIA, CNRS and contributors */ +/* <O___,, * (see version control and CREDITS file for authors & dates) */ /* \VV/ **************************************************************/ /* // * This file is distributed under the terms of the */ /* * GNU Lesser General Public License Version 2.1 */ diff --git a/doc/sphinx/_static/coqdoc.css b/doc/sphinx/_static/coqdoc.css index 7a3d59d4c0..32cb0a7a15 100644 --- a/doc/sphinx/_static/coqdoc.css +++ b/doc/sphinx/_static/coqdoc.css @@ -1,7 +1,7 @@ /************************************************************************/ /* * The Coq Proof Assistant / The Coq Development Team */ -/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */ -/* <O___,, * (see CREDITS file for the list of authors) */ +/* v * Copyright INRIA, CNRS and contributors */ +/* <O___,, * (see version control and CREDITS file for authors & dates) */ /* \VV/ **************************************************************/ /* // * This file is distributed under the terms of the */ /* * GNU Lesser General Public License Version 2.1 */ diff --git a/doc/sphinx/_static/coqnotations.sty b/doc/sphinx/_static/coqnotations.sty index 3548b8754c..3dfe4db439 100644 --- a/doc/sphinx/_static/coqnotations.sty +++ b/doc/sphinx/_static/coqnotations.sty @@ -67,11 +67,26 @@ \newcssclass{notation-sup}{\nsup{#1}} \newcssclass{notation-sub}{\nsub{#1}} -\newcssclass{notation}{\nnotation{#1}} +\newcssclass{notation}{\nnotation{\textbf{#1}}} \newcssclass{repeat}{\nrepeat{#1}} \newcssclass{repeat-wrapper}{\nwrapper{#1}} +\newcssclass{repeat-wrapper-with-sub}{\nwrapper{#1}} \newcssclass{hole}{\nhole{#1}} \newcssclass{alternative}{\nalternative{\nbox{#1}}{0pt}} \newcssclass{alternative-block}{#1} \newcssclass{repeated-alternative}{\nalternative{#1}{\nboxsep}} \newcssclass{alternative-separator}{\quad\naltsep{}\quad} +\newcssclass{prodn-table}{% + \begin{savenotes} + \sphinxattablestart + \begin{tabulary}{\linewidth}[t]{lLL} + #1 + \end{tabulary} + \par + \sphinxattableend + \end{savenotes}} +% latex puts targets 1 line below where they should be; prodn-target corrects for this +\newcssclass{prodn-target}{\raisebox{\dimexpr \nscriptsize \relax}{#1}} +\newcssclass{prodn-cell-nonterminal}{#1 &} +\newcssclass{prodn-cell-op}{#1 &} +\newcssclass{prodn-cell-production}{#1\\} diff --git a/doc/sphinx/_static/notations.css b/doc/sphinx/_static/notations.css index 4a5fa0b328..733a73bd21 100644 --- a/doc/sphinx/_static/notations.css +++ b/doc/sphinx/_static/notations.css @@ -1,7 +1,7 @@ /************************************************************************/ /* * The Coq Proof Assistant / The Coq Development Team */ -/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */ -/* <O___,, * (see CREDITS file for the list of authors) */ +/* v * Copyright INRIA, CNRS and contributors */ +/* <O___,, * (see version control and CREDITS file for authors & dates) */ /* \VV/ **************************************************************/ /* // * This file is distributed under the terms of the */ /* * GNU Lesser General Public License Version 2.1 */ @@ -10,6 +10,7 @@ .notation { /* font-family: "Ubuntu Mono", "Consolas", monospace; */ white-space: pre-wrap; + font-weight: bold; } .notation .notation-sup { @@ -85,7 +86,8 @@ padding-right: 0.6em; /* Space for the left half of the sub- and sup-scripts */ } -.notation .repeat-wrapper { +.notation .repeat-wrapper, +.notation .repeat-wrapper-with-sub { display: inline-block; position: relative; margin-right: 0.4em; /* Space for the right half of the sub- and sup-scripts */ @@ -165,10 +167,52 @@ /* Overrides */ /*************/ -.rst-content table.docutils td, .rst-content table.docutils th { - padding: 8px; /* Reduce horizontal padding */ - border-left: none; - border-right: none; +.prodn-table { + display: table; + margin: 1.5em 0px; + vertical-align: baseline; + font-weight: bold; +} + +.prodn-column-group { + display: table-column-group; +} + +.prodn-column { + display: table-column; +} + +.prodn-row-group { + display: table-row-group; +} + +.prodn-row { + display: table-row; +} + +.prodn-cell-nonterminal, +.prodn-cell-op, +.prodn-cell-production +{ + display: table-cell; +} + +.prodn-cell-nonterminal { + padding-right: 0.49em; +} + +.prodn-cell-op { + padding-right: 0.90em; + font-weight: normal; +} + +.prodn-table .notation > .repeat-wrapper { + margin-top: 0.28em; +} + +.prodn-table .notation > .repeat-wrapper-with-sub { + margin-top: 0.28em; + margin-bottom: 0.28em; } /* We can't display nested blocks otherwise */ diff --git a/doc/sphinx/_static/notations.js b/doc/sphinx/_static/notations.js index 63112312d0..d2eee1f5fa 100644 --- a/doc/sphinx/_static/notations.js +++ b/doc/sphinx/_static/notations.js @@ -1,7 +1,7 @@ /************************************************************************/ /* * The Coq Proof Assistant / The Coq Development Team */ -/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */ -/* <O___,, * (see CREDITS file for the list of authors) */ +/* v * Copyright INRIA, CNRS and contributors */ +/* <O___,, * (see version control and CREDITS file for authors & dates) */ /* \VV/ **************************************************************/ /* // * This file is distributed under the terms of the */ /* * GNU Lesser General Public License Version 2.1 */ diff --git a/doc/sphinx/_static/pre-text.css b/doc/sphinx/_static/pre-text.css index 9d133fb1aa..aa4180d246 100644 --- a/doc/sphinx/_static/pre-text.css +++ b/doc/sphinx/_static/pre-text.css @@ -1,7 +1,7 @@ /************************************************************************/ /* * The Coq Proof Assistant / The Coq Development Team */ -/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */ -/* <O___,, * (see CREDITS file for the list of authors) */ +/* v * Copyright INRIA, CNRS and contributors */ +/* <O___,, * (see version control and CREDITS file for authors & dates) */ /* \VV/ **************************************************************/ /* // * This file is distributed under the terms of the */ /* * GNU Lesser General Public License Version 2.1 */ diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst index 45b3f6f161..8ec51e45ba 100644 --- a/doc/sphinx/addendum/extended-pattern-matching.rst +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -5,8 +5,6 @@ Extended pattern matching :Authors: Cristina Cornes and Hugo Herbelin -.. TODO links to figures - This section describes the full form of pattern matching in |Coq| terms. .. |rhs| replace:: right hand sides @@ -14,7 +12,7 @@ This section describes the full form of pattern matching in |Coq| terms. Patterns -------- -The full syntax of match is presented in Figures 1.1 and 1.2. +The full syntax of :g:`match` is presented in section :ref:`term`. Identifiers in patterns are either constructor names or variables. Any identifier that is not the constructor of an inductive or co-inductive type is considered to be a variable. A variable name cannot occur more @@ -192,7 +190,7 @@ Disjunctive patterns -------------------- Multiple patterns that share the same right-hand-side can be -factorized using the notation :n:`{+| @patterns_comma}`. For +factorized using the notation :n:`{+| {+, @pattern } }`. For instance, :g:`max` can be rewritten as follows: .. coqtop:: in reset @@ -496,9 +494,8 @@ We can use multiple patterns to write the proof of the lemma In the example of :g:`dec`, the first match is dependent while the second is not. -The user can also use match in combination with the tactic :tacn:`refine` (see -Section 8.2.3) to build incomplete proofs beginning with a match -construction. +The user can also use match in combination with the tactic :tacn:`refine` +to build incomplete proofs beginning with a :g:`match` construction. Pattern-matching on inductive objects involving local definitions diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index 7136cc28d1..41b726b069 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -1,7 +1,7 @@ .. _extraction: -Extraction of programs in |OCaml| and Haskell -============================================= +Program extraction +================== :Authors: Jean-Christophe Filliâtre and Pierre Letouzey @@ -313,14 +313,21 @@ The system also provides a mechanism to specify ML terms for inductive types and constructors. For instance, the user may want to use the ML native boolean type instead of the |Coq| one. The syntax is the following: -.. cmd:: Extract Inductive @qualid => @string [ {+ @string } ] +.. cmd:: Extract Inductive @qualid => @string__1 [ {+ @string } ] Give an ML extraction for the given inductive type. You must specify - extractions for the type itself (first :token:`string`) and all its - constructors (all the :token:`string` between square brackets). In this form, + extractions for the type itself (:n:`@string__1`) and all its + constructors (all the :n:`@string` between square brackets). In this form, the ML extraction must be an ML inductive datatype, and the native pattern matching of the language will be used. + When :n:`@string__1` matches the name of the type of characters or strings + (``char`` and ``string`` for OCaml, ``Prelude.Char`` and ``Prelude.String`` + for Haskell), extraction of literals is handled in a specialized way, so as + to generate literals in the target language. This feature requires the type + designated by :n:`@qualid` to be registered as the standard char or string type, + using the :cmd:`Register` command. + .. cmdv:: Extract Inductive @qualid => @string [ {+ @string } ] @string Same as before, with a final extra :token:`string` that indicates how to diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index 9f5741f72a..315c9d4a80 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -170,7 +170,7 @@ compatibility constraints. Adding new relations and morphisms ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: Add Parametric Relation @binders : (A t1 ... tn) (Aeq t′1 ... t′m) {? reflexivity proved by @term} {? symmetry proved by @term} {? transitivity proved by @term} as @ident +.. cmd:: Add Parametric Relation {* @binder } : (A t1 ... tn) (Aeq t′1 ... t′m) {? reflexivity proved by @term} {? symmetry proved by @term} {? transitivity proved by @term} as @ident This command declares a parametric relation :g:`Aeq: forall (y1 : β1 ... ym : βm)`, :g:`relation (A t1 ... tn)` over :g:`(A : αi -> ... αn -> Type)`. @@ -219,7 +219,7 @@ replace terms with related ones only in contexts that are syntactic compositions of parametric morphism instances declared with the following command. -.. cmd:: Add Parametric Morphism @binders : (@ident {+ @term__1}) with signature @term__2 as @ident +.. cmd:: Add Parametric Morphism {* @binder } : (@ident {+ @term__1}) with signature @term__2 as @ident This command declares a parametric morphism :n:`@ident {+ @term__1}` of signature :n:`@term__2`. The final identifier :token:`ident` gives a unique @@ -713,48 +713,119 @@ 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 +combined to create custom rewriting procedures. Its set of strategies is based 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: - -.. productionlist:: coq - strategy : `qualid` (lemma, left to right) - : <- `qualid` (lemma, right to left) - : fail (failure) - : id (identity) - : refl (reflexivity) - : progress `strategy` (progress) - : try `strategy` (try catch) - : `strategy` ; `strategy` (composition) - : choice `strategy` `strategy` (left_biased_choice) - : repeat `strategy` (one or more) - : any `strategy` (zero or more) - : subterm `strategy` (one subterm) - : subterms `strategy` (all subterms) - : innermost `strategy` (innermost first) - : outermost `strategy` (outermost first) - : bottomup `strategy` (bottom-up) - : topdown `strategy` (top-down) - : hints `ident` (apply hints from hint database) - : terms `term` ... `term` (any of the terms) - : eval `red_expr` (apply reduction) - : fold `term` (unify) - : ( `strategy` ) - -Actually a few of these are defined in term of the others using a +are applied using the tactic :n:`rewrite_strat @rewstrategy`. + +.. insertprodn rewstrategy rewstrategy + +.. prodn:: + rewstrategy ::= @one_term + | <- @one_term + | fail + | id + | refl + | progress @rewstrategy + | try @rewstrategy + | @rewstrategy ; @rewstrategy + | choice @rewstrategy @rewstrategy + | repeat @rewstrategy + | any @rewstrategy + | subterm @rewstrategy + | subterms @rewstrategy + | innermost @rewstrategy + | outermost @rewstrategy + | bottomup @rewstrategy + | topdown @rewstrategy + | hints @ident + | terms {* @one_term } + | eval @red_expr + | fold @one_term + | ( @rewstrategy ) + | old_hints @ident + +:n:`@one_term` + lemma, left to right + +:n:`<- @one_term` + lemma, right to left + +:n:`fail` + failure + +:n:`id` + identity + +:n:`refl` + reflexivity + +:n:`progress @rewstrategy` + progress + +:n:`try @rewstrategy` + try catch + +:n:`@rewstrategy ; @rewstrategy` + composition + +:n:`choice @rewstrategy @rewstrategy` + left_biased_choice + +:n:`repeat @rewstrategy` + one or more + +:n:`any @rewstrategy` + zero or more + +:n:`subterm @rewstrategy` + one subterm + +:n:`subterms @rewstrategy` + all subterms + +:n:`innermost @rewstrategy` + innermost first + +:n:`outermost @rewstrategy` + outermost first + +:n:`bottomup @rewstrategy` + bottom-up + +:n:`topdown @rewstrategy` + top-down + +:n:`hints @ident` + apply hints from hint database + +:n:`terms {* @one_term }` + any of the terms + +:n:`eval @red_expr` + apply reduction + +:n:`fold @term` + unify + +:n:`( @rewstrategy )` + to be documented + +:n:`old_hints @ident` + to be documented + + +A few of these are defined in terms of the others using a primitive fixpoint operator: -- :n:`try @strategy := choice @strategy id` -- :n:`any @strategy := fix @ident. try (@strategy ; @ident)` -- :n:`repeat @strategy := @strategy; any @strategy` -- :n:`bottomup @strategy := fix @ident. (choice (progress (subterms @ident)) @strategy) ; try @ident` -- :n:`topdown @strategy := fix @ident. (choice @strategy (progress (subterms @ident))) ; try @ident` -- :n:`innermost @strategy := fix @ident. (choice (subterm @ident) @strategy)` -- :n:`outermost @strategy := fix @ident. (choice @strategy (subterm @ident))` +- :n:`try @rewstrategy := choice @rewstrategy id` +- :n:`any @rewstrategy := fix @ident. try (@rewstrategy ; @ident)` +- :n:`repeat @rewstrategy := @rewstrategy; any @rewstrategy` +- :n:`bottomup @rewstrategy := fix @ident. (choice (progress (subterms @ident)) @rewstrategy) ; try @ident` +- :n:`topdown @rewstrategy := fix @ident. (choice @rewstrategy (progress (subterms @ident))) ; try @ident` +- :n:`innermost @rewstrategy := fix @ident. (choice (subterm @ident) @rewstrategy)` +- :n:`outermost @rewstrategy := fix @ident. (choice @rewstrategy (subterm @ident))` The basic control strategy semantics are straightforward: strategies are applied to subterms of the term to rewrite, starting from the root @@ -764,18 +835,18 @@ hand-side. Composition can be used to continue rewriting on the current subterm. The ``fail`` strategy always fails while the identity strategy succeeds without making progress. The reflexivity strategy succeeds, making progress using a reflexivity proof of rewriting. -``progress`` tests progress of the argument :token:`strategy` and fails if no +``progress`` tests progress of the argument :n:`@rewstrategy` and fails if no progress was made, while ``try`` always succeeds, catching failures. ``choice`` is left-biased: it will launch the first strategy and fall back on the second one in case of failure. One can iterate a strategy at least 1 time using ``repeat`` and at least 0 times using ``any``. -The ``subterm`` and ``subterms`` strategies apply their argument :token:`strategy` to +The ``subterm`` and ``subterms`` strategies apply their argument :n:`@rewstrategy` to respectively one or all subterms of the current term under consideration, left-to-right. ``subterm`` stops at the first subterm for -which :token:`strategy` made progress. The composite strategies ``innermost`` and ``outermost`` +which :n:`@rewstrategy` made progress. The composite strategies ``innermost`` and ``outermost`` perform a single innermost or outermost rewrite using their argument -:token:`strategy`. Their counterparts ``bottomup`` and ``topdown`` perform as many +:n:`@rewstrategy`. Their counterparts ``bottomup`` and ``topdown`` perform as many rewritings as possible, starting from the bottom or the top of the term. @@ -793,7 +864,7 @@ Usage ~~~~~ -.. tacn:: rewrite_strat @strategy {? in @ident } +.. tacn:: rewrite_strat @rewstrategy {? in @ident } :name: rewrite_strat Rewrite using the strategy s in hypothesis ident or the conclusion. diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index 19b33f0d90..1f33775a01 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -37,12 +37,13 @@ In addition to these user-defined classes, we have two built-in classes: * ``Funclass``, the class of functions; its objects are all the terms with a functional type, i.e. of form :g:`forall x:A,B`. -Formally, the syntax of classes is defined as: + .. insertprodn class class + + .. prodn:: + class ::= Funclass + | Sortclass + | @smart_qualid -.. productionlist:: - class: `qualid` - : Sortclass - : Funclass Coercions @@ -186,43 +187,12 @@ Declaring Coercions This defines :token:`ident` just like :n:`Let @ident := @term {? @type }`, and then declares :token:`ident` as a coercion between it source and its target. -Assumptions can be declared as coercions at declaration time. -This extends the grammar of assumptions from -Figure :ref:`vernacular` as follows: - -.. - FIXME: - \comindex{Variable \mbox{\rm (and coercions)}} - \comindex{Axiom \mbox{\rm (and coercions)}} - \comindex{Parameter \mbox{\rm (and coercions)}} - \comindex{Hypothesis \mbox{\rm (and coercions)}} - -.. productionlist:: - assumption : `assumption_keyword` `assums` . - assums : `simple_assums` - : (`simple_assums`) ... (`simple_assums`) - simple_assums : `ident` ... `ident` :[>] `term` - -If the extra ``>`` is present before the type of some assumptions, these -assumptions are declared as coercions. - -Similarly, constructors of inductive types can be declared as coercions at -definition time of the inductive type. This extends and modifies the -grammar of inductive types from Figure :ref:`vernacular` as follows: +Some objects can be declared as coercions when they are defined. +This applies to :ref:`assumptions<gallina-assumptions>` and +constructors of :ref:`inductive types and record fields<gallina-inductive-definitions>`. +Use :n:`:>` instead of :n:`:` before the +:n:`@type` of the assumption to do so. See :n:`@of_type`. -.. - FIXME: - \comindex{Inductive \mbox{\rm (and coercions)}} - \comindex{CoInductive \mbox{\rm (and coercions)}} - -.. productionlist:: - inductive : Inductive `ind_body` with ... with `ind_body` - : CoInductive `ind_body` with ... with `ind_body` - ind_body : `ident` [ `binders` ] : `term` := [[|] `constructor` | ... | `constructor` ] - constructor : `ident` [ `binders` ] [:[>] `term` ] - -Especially, if the extra ``>`` is present in a constructor -declaration, this constructor is declared as a coercion. .. cmd:: Identity Coercion @ident : @class >-> @class @@ -240,7 +210,7 @@ declaration, this constructor is declared as a coercion. Same as :cmd:`Identity Coercion` but locally to the current section. - .. cmdv:: SubClass @ident := @type + .. cmd:: SubClass @ident_decl @def_body :name: SubClass If :n:`@type` is a class :n:`@ident'` applied to some arguments then @@ -251,7 +221,7 @@ declaration, this constructor is declared as a coercion. :n:`Definition @ident := @type.` :n:`Identity Coercion Id_@ident_@ident' : @ident >-> @ident'`. - .. cmdv:: Local SubClass @ident := @type + .. cmdv:: Local SubClass @ident_decl @def_body Same as before but locally to the current section. @@ -299,7 +269,7 @@ Classes as Records We allow the definition of *Structures with Inheritance* (or classes as records) by extending the existing :cmd:`Record` macro. Its new syntax is: -.. cmdv:: Record {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } } +.. cmdv:: {| Record | Structure } {? >} @ident {* @binder } : @sort := {? @ident} { {+; @ident :{? >} @term } } The first identifier :token:`ident` is the name of the defined record and :token:`sort` is its type. The optional identifier after ``:=`` is the name @@ -315,12 +285,6 @@ by extending the existing :cmd:`Record` macro. Its new syntax is: (this may fail if the uniform inheritance condition is not satisfied). -.. cmdv:: Structure {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } } - :name: Structure - - This is a synonym of :cmd:`Record`. - - Coercions and Sections ---------------------- diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index cc19c8b6a9..f706633da9 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -35,6 +35,17 @@ tactics for solving arithmetic goals over :math:`\mathbb{Q}`, use the Simplex method for solving linear goals. If it is not set, the decision procedures are using Fourier elimination. +.. opt:: Dump Arith + + This option (unset by default) may be set to a file path where + debug info will be written. + +.. cmd:: Show Lia Profile + + This command prints some statistics about the amount of pivoting + operations needed by :tacn:`lia` and may be useful to detect + inefficiencies (only meaningful if flag :flag:`Simplex` is set). + .. flag:: Lia Cache This flag (set by default) instructs :tacn:`lia` to cache its results in the file `.lia.cache` diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst index db8c09d88f..0e8660cb0e 100644 --- a/doc/sphinx/addendum/miscellaneous-extensions.rst +++ b/doc/sphinx/addendum/miscellaneous-extensions.rst @@ -1,10 +1,5 @@ -.. _miscellaneousextensions: - -Miscellaneous extensions -======================== - Program derivation ------------------- +================== |Coq| comes with an extension called ``Derive``, which supports program derivation. Typically in the style of Bird and Meertens or derivations diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst index 650a444a16..daca43e65e 100644 --- a/doc/sphinx/addendum/omega.rst +++ b/doc/sphinx/addendum/omega.rst @@ -5,6 +5,27 @@ Omega: a solver for quantifier-free problems in Presburger Arithmetic :Author: Pierre Crégut +.. warning:: + + The :tacn:`omega` tactic is about to be deprecated in favor of the + :tacn:`lia` tactic. The goal is to consolidate the arithmetic + solving capabilities of Coq into a single engine; moreover, + :tacn:`lia` is in general more powerful than :tacn:`omega` (it is a + complete Presburger arithmetic solver while :tacn:`omega` was known + to be incomplete). + + Work is in progress to make sure that there are no regressions + (including no performance regression) when switching from + :tacn:`omega` to :tacn:`lia` in existing projects. However, we + already recommend using :tacn:`lia` in new or refactored proof + scripts. We also ask that you report (in our `bug tracker + <https://github.com/coq/coq/issues>`_) any issue you encounter, + especially if the issue was not present in :tacn:`omega`. + + Note that replacing :tacn:`omega` with :tacn:`lia` can break + non-robust proof scripts which rely on incompleteness bugs of + :tacn:`omega` (e.g. using the pattern :g:`; try omega`). + Description of ``omega`` ------------------------ diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst index 35729d852d..7a50748c51 100644 --- a/doc/sphinx/addendum/parallel-proof-processing.rst +++ b/doc/sphinx/addendum/parallel-proof-processing.rst @@ -154,6 +154,18 @@ to a worker process. The threshold can be configured with Batch mode --------------- + .. warning:: + + The ``-vio`` flag is subsumed, for most practical usage, by the + the more recent ``-vos`` flag. See :ref:`compiled-interfaces`. + + .. warning:: + + When working with ``.vio`` files, do not use the ``-vos`` option at + the same time, otherwise stale files might get loaded when executing + a ``Require``. Indeed, the loading of a nonempty ``.vos`` file is + assigned higher priority than the loading of a ``.vio`` file. + When |Coq| is used as a batch compiler by running ``coqc``, it produces a ``.vo`` file for each ``.v`` file. A ``.vo`` file contains, among other things, theorem statements and proofs. Hence to produce a .vo |Coq| @@ -161,10 +173,10 @@ need to process all the proofs of the ``.v`` file. The asynchronous processing of proofs can decouple the generation of a compiled file (like the ``.vo`` one) that can be loaded by ``Require`` from the -generation and checking of the proof objects. The ``-quick`` flag can be +generation and checking of the proof objects. The ``-vio`` flag can be passed to ``coqc`` to produce, quickly, ``.vio`` files. Alternatively, when using a Makefile produced by ``coq_makefile``, -the ``quick`` target can be used to compile all files using the ``-quick`` flag. +the ``vio`` target can be used to compile all files using the ``-vio`` flag. A ``.vio`` file can be loaded using ``Require`` exactly as a ``.vo`` file but proofs will not be available (the Print command produces an error). @@ -173,7 +185,7 @@ inconsistencies might go unnoticed. A ``.vio`` file does not contain proof objects, but proof tasks, i.e. what a worker process can transform into a proof object. -Compiling a set of files with the ``-quick`` flag allows one to work, +Compiling a set of files with the ``-vio`` flag allows one to work, interactively, on any file without waiting for all the proofs to be checked. diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index a17dca1693..5cffe9e435 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -98,10 +98,17 @@ coercions. .. flag:: Program Mode Enables the program mode, in which 1) typechecking allows subset coercions and - 2) the elaboration of pattern matching of :cmd:`Program Fixpoint` and - :cmd:`Program Definition` act - like Program Fixpoint/Definition, generating obligations if there are - unresolved holes after typechecking. + 2) the elaboration of pattern matching of :cmd:`Fixpoint` and + :cmd:`Definition` act as if the :attr:`program` attribute had been + used, generating obligations if there are unresolved holes after + typechecking. + +.. attr:: program + + This attribute allows to use the Program mode on a specific + definition. An alternative syntax is to use the legacy ``Program`` + prefix (cf. :n:`@legacy_attr`) as documented in the rest of this + chapter. .. _syntactic_control: @@ -155,7 +162,7 @@ Program Definition This command types the value term in Russell and generates proof obligations. Once solved using the commands shown below, it binds the - final |Coq| term to the name ``ident`` in the environment. + final |Coq| term to the name :n:`@ident` in the environment. .. exn:: @ident already exists. :name: @ident already exists. (Program Definition) @@ -163,22 +170,22 @@ Program Definition .. cmdv:: Program Definition @ident : @type := @term - It interprets the type ``type``, potentially generating proof + It interprets the type :n:`@type`, potentially generating proof obligations to be resolved. Once done with them, we have a |Coq| - type |type_0|. It then elaborates the preterm ``term`` into a |Coq| - term |term_0|, checking that the type of |term_0| is coercible to - |type_0|, and registers ``ident`` as being of type |type_0| once the - set of obligations generated during the interpretation of |term_0| + type :n:`@type__0`. It then elaborates the preterm :n:`@term` into a |Coq| + term :n:`@term__0`, checking that the type of :n:`@term__0` is coercible to + :n:`@type__0`, and registers :n:`@ident` as being of type :n:`@type__0` once the + set of obligations generated during the interpretation of :n:`@term__0` and the aforementioned coercion derivation are solved. .. exn:: In environment … the term: @term does not have type @type. Actually, it has type ... :undocumented: - .. cmdv:: Program Definition @ident @binders : @type := @term + .. cmdv:: Program Definition @ident {* @binder } : @type := @term This is equivalent to: - :g:`Program Definition ident : forall binders, type := fun binders => term`. + :n:`Program Definition @ident : forall {* @binder }, @type := fun {* @binder } => @term`. .. TODO refer to production in alias @@ -189,7 +196,7 @@ Program Definition Program Fixpoint ~~~~~~~~~~~~~~~~ -.. cmd:: Program Fixpoint @ident @binders {? {@order}} : @type := @term +.. cmd:: Program Fixpoint @ident {* @binder } {? {@order}} : @type := @term The optional order annotation follows the grammar: diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index 1098aa75da..2a321b5cbf 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -1,8 +1,12 @@ +.. |bdi| replace:: :math:`\beta\delta\iota` .. |ra| replace:: :math:`\rightarrow_{\beta\delta\iota}` .. |la| replace:: :math:`\leftarrow_{\beta\delta\iota}` .. |eq| replace:: `=`:sub:`(by the main correctness theorem)` .. |re| replace:: ``(PEeval`` `v` `ap`\ ``)`` .. |le| replace:: ``(Pphi_dev`` `v` ``(norm`` `ap`\ ``))`` +.. |N| replace:: ``N`` +.. |nat| replace:: ``nat`` +.. |Z| replace:: ``Z`` .. _theringandfieldtacticfamilies: @@ -300,70 +304,79 @@ following property: The syntax for adding a new ring is -.. cmd:: Add Ring @ident : @term {? ( @ring_mod {* , @ring_mod } )} - - The :token:`ident` is not relevant. It is used just for error messages. The - :token:`term` is a proof that the ring signature satisfies the (semi-)ring +.. cmd:: Add Ring @ident : @one_term {? ( {+, @ring_mod } ) } + + .. insertprodn ring_mod ring_mod + + .. prodn:: + ring_mod ::= decidable @one_term + | abstract + | morphism @one_term + | constants [ @ltac_expr ] + | preprocess [ @ltac_expr ] + | postprocess [ @ltac_expr ] + | setoid @one_term @one_term + | sign @one_term + | power @one_term [ {+ @qualid } ] + | power_tac @one_term [ @ltac_expr ] + | div @one_term + | closed [ {+ @qualid } ] + + The :n:`@ident` is used only for error messages. The + :n:`@one_term` is a proof that the ring signature satisfies the (semi-)ring axioms. The optional list of modifiers is used to tailor the behavior - of the tactic. The following list describes their syntax and effects: - - .. productionlist:: coq - ring_mod : abstract | decidable `term` | morphism `term` - : setoid `term` `term` - : constants [ `tactic` ] - : preprocess [ `tactic` ] - : postprocess [ `tactic` ] - : power_tac `term` [ `tactic` ] - : sign `term` - : div `term` - - abstract + of the tactic. Here are their effects: + + :n:`abstract` declares the ring as abstract. This is the default. - decidable :n:`@term` + :n:`decidable @one_term` declares the ring as computational. The expression - :n:`@term` is the correctness proof of an equality test ``?=!`` + :n:`@one_term` is the correctness proof of an equality test ``?=!`` (which should be evaluable). Its type should be of the form ``forall x y, x ?=! y = true → x == y``. - morphism :n:`@term` + :n:`morphism @one_term` declares the ring as a customized one. The expression - :n:`@term` is a proof that there exists a morphism between a set of + :n:`@one_term` is a proof that there exists a morphism between a set of coefficient and the ring carrier (see ``Ring_theory.ring_morph`` and ``Ring_theory.semi_morph``). - setoid :n:`@term` :n:`@term` + :n:`setoid @one_term @one_term` forces the use of given setoid. The first - :n:`@term` is a proof that the equality is indeed a setoid (see - ``Setoid.Setoid_Theory``), and the second :n:`@term` a proof that the + :n:`@one_term` is a proof that the equality is indeed a setoid (see + ``Setoid.Setoid_Theory``), and the second a proof that the ring operations are morphisms (see ``Ring_theory.ring_eq_ext`` and ``Ring_theory.sring_eq_ext``). This modifier needs not be used if the setoid and morphisms have been declared. - constants [ :n:`@tactic` ] - specifies a tactic expression :n:`@tactic` that, given a + :n:`constants [ @ltac_expr ]` + specifies a tactic expression :n:`@ltac_expr` that, given a term, returns either an object of the coefficient set that is mapped to the expression via the morphism, or returns ``InitialRing.NotConstant``. The default behavior is to map only 0 and 1 to their counterpart in the coefficient set. This is generally not desirable for non trivial computational rings. - preprocess [ :n:`@tactic` ] - specifies a tactic :n:`@tactic` that is applied as a + :n:`preprocess [ @ltac_expr ]` + specifies a tactic :n:`@ltac_expr` that is applied as a preliminary step for :tacn:`ring` and :tacn:`ring_simplify`. It can be used to transform a goal so that it is better recognized. For instance, ``S n`` can be changed to ``plus 1 n``. - postprocess [ :n:`@tactic` ] - specifies a tactic :n:`@tactic` that is applied as a final + :n:`postprocess [ @ltac_expr ]` + specifies a tactic :n:`@ltac_expr` that is applied as a final step for :tacn:`ring_simplify`. For instance, it can be used to undo modifications of the preprocessor. - power_tac :n:`@term` [ :n:`@tactic` ] + :n:`power @one_term [ {+ @qualid } ]` + to be documented + + :n:`power_tac @one_term @ltac_expr ]` allows :tacn:`ring` and :tacn:`ring_simplify` to recognize power expressions with a constant positive integer exponent (example: - :math:`x^2` ). The term :n:`@term` is a proof that a given power function satisfies + :math:`x^2` ). The term :n:`@one_term` is a proof that a given power function satisfies the specification of a power function (term has to be a proof of ``Ring_theory.power_theory``) and :n:`@tactic` specifies a tactic expression that, given a term, “abstracts” it into an object of type |N| whose @@ -374,22 +387,25 @@ The syntax for adding a new ring is and ``plugins/setoid_ring/RealField.v`` for examples. By default the tactic does not recognize power expressions as ring expressions. - sign :n:`@term` + :n:`sign @one_term` allows :tacn:`ring_simplify` to use a minus operation when outputting its normal form, i.e writing ``x − y`` instead of ``x + (− y)``. The term :token:`term` is a proof that a given sign function indicates expressions that are signed (:token:`term` has to be a proof of ``Ring_theory.get_sign``). See ``plugins/setoid_ring/InitialRing.v`` for examples of sign function. - div :n:`@term` + :n:`div @one_term` allows :tacn:`ring` and :tacn:`ring_simplify` to use monomials with - coefficients other than 1 in the rewriting. The term :n:`@term` is a proof + coefficients other than 1 in the rewriting. The term :n:`@one_term` is a proof that a given division function satisfies the specification of an - euclidean division function (:n:`@term` has to be a proof of + euclidean division function (:n:`@one_term` has to be a proof of ``Ring_theory.div_theory``). For example, this function is called when trying to rewrite :math:`7x` by :math:`2x = z` to tell that :math:`7 = 3 \times 2 + 1`. See ``plugins/setoid_ring/InitialRing.v`` for examples of div function. + :n:`closed [ {+ @qualid } ]` + to be documented + Error messages: .. exn:: Bad ring structure. @@ -653,24 +669,27 @@ zero for the correctness of the algorithm. The syntax for adding a new field is -.. cmd:: Add Field @ident : @term {? ( @field_mod {* , @field_mod } )} +.. cmd:: Add Field @ident : @one_term {? ( {+, @field_mod } ) } - The :n:`@ident` is not relevant. It is used just for error - messages. :n:`@term` is a proof that the field signature satisfies the + .. insertprodn field_mod field_mod + + .. prodn:: + field_mod ::= @ring_mod + | completeness @one_term + + The :n:`@ident` is used only for error + messages. :n:`@one_term` is a proof that the field signature satisfies the (semi-)field axioms. The optional list of modifiers is used to tailor the behavior of the tactic. - .. productionlist:: coq - field_mod : `ring_mod` | completeness `term` - Since field tactics are built upon ``ring`` - tactics, all modifiers of the ``Add Ring`` apply. There is only one + tactics, all modifiers of :cmd:`Add Ring` apply. There is only one specific modifier: - completeness :n:`@term` + completeness :n:`@one_term` allows the field tactic to prove automatically that the image of nonzero coefficients are mapped to nonzero - elements of the field. :n:`@term` is a proof of + elements of the field. :n:`@one_term` is a proof of :g:`forall x y, [x] == [y] -> x ?=! y = true`, which is the completeness of equality on coefficients w.r.t. the field equality. diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 57a2254100..bd4c276571 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -47,7 +47,7 @@ Leibniz equality on some type. An example implementation is: | tt, tt => eq_refl tt end }. -Using the attribute ``refine``, if the term is not sufficient to +Using the :attr:`refine` attribute, 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. @@ -77,9 +77,9 @@ remaining fields, e.g.: Defined. One has to take care that the transparency of every field is -determined by the transparency of the :cmd:`Instance` proof. One can use -alternatively the :cmd:`Program Instance` variant which has richer facilities -for dealing with obligations. +determined by the transparency of the :cmd:`Instance` proof. One can +use alternatively the :attr:`program` attribute to get richer +facilities for dealing with obligations. Binding classes @@ -174,7 +174,7 @@ For example: .. coqtop:: in - Global Program Instance option_eqb : EqDec (option A) := + #[ global, program ] Instance option_eqb : EqDec (option A) := { eqb x y := match x, y with | Some x, Some y => eqb x y | None, None => true @@ -188,7 +188,7 @@ For example: About option_eqb. -Here the :cmd:`Global` modifier redeclares the instance at the end of the +Here the :attr:`global` attribute redeclares the instance at the end of the section, once it has been generalized by the context variables it uses. @@ -295,14 +295,20 @@ the Existing Instance command to achieve the same effect. Summary of the commands ----------------------- -.. cmd:: Class @ident {? @binders} : {? @sort} := {? @ident} { {+; @ident :{? >} @term } } +.. cmd:: Class @inductive_definition {* with @inductive_definition } The :cmd:`Class` command is used to declare a typeclass with parameters :token:`binders` and fields the declared record fields. + Like any command declaring a record, this command supports the + :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`, + :attr:`universes(template)`, :attr:`universes(notemplate)`, + :attr:`universes(cumulative)`, :attr:`universes(noncumulative)` and + :attr:`private(matching)` attributes. + .. _singleton-class: - .. cmdv:: Class @ident {? @binders} : {? @sort} := @ident : @term + .. cmdv:: Class @ident {* @binder } : {? @sort} := @ident : @term This variant declares a *singleton* class with a single method. This singleton class is a so-called definitional class, represented simply @@ -324,7 +330,7 @@ Summary of the commands This command has no effect when used on a typeclass. -.. cmd:: Instance @ident {? @binders} : @term__0 {+ @term} {? | @num} := { {*; @field_def} } +.. cmd:: Instance @ident {* @binder } : @term__0 {+ @term} {? | @num} := { {*; @field_def} } This command is used to declare a typeclass instance named :token:`ident` of the class :n:`@term__0` with parameters :token:`term` and @@ -337,25 +343,31 @@ Summary of the commands :tacn:`auto` hints. If the priority :token:`num` is not specified, it defaults to the number of non-dependent binders of the instance. - .. cmdv:: Instance @ident {? @binders} : forall {? @binders}, @term__0 {+ @term} {? | @num } := @term + This command supports the :attr:`global` attribute that can be + used on instances declared in a section so that their + generalization is automatically redeclared after the section is + closed. - This syntax is used for declaration of singleton class instances or - for directly giving an explicit term of type :n:`forall @binders, @term__0 - {+ @term}`. One need not even mention the unique field name for - singleton classes. + Like :cmd:`Definition`, it also supports the :attr:`program` + attribute to switch the type checking to `Program` (chapter + :ref:`programs`) and use the obligation mechanism to manage missing + fields. - .. cmdv:: Global Instance - :name: Global Instance + Finally, it supports the lighter :attr:`refine` attribute: - One can use the :cmd:`Global` modifier on instances declared in a - section so that their generalization is automatically redeclared - after the section is closed. + .. attr:: refine - .. cmdv:: Program Instance - :name: Program Instance + This attribute can be used to leave holes or not provide all + fields in the definition of an instance and open the tactic mode + to fill them. It works exactly as if no body had been given and + the :tacn:`refine` tactic has been used first. - Switches the type checking to `Program` (chapter :ref:`programs`) and - uses the obligation mechanism to manage missing fields. + .. cmdv:: Instance @ident {* @binder } : forall {* @binder }, @term__0 {+ @term} {? | @num } := @term + + This syntax is used for declaration of singleton class instances or + for directly giving an explicit term of type :n:`forall {* @binder }, @term__0 + {+ @term}`. One need not even mention the unique field name for + singleton classes. .. cmdv:: Declare Instance :name: Declare Instance @@ -381,8 +393,10 @@ few other commands related to typeclasses. .. tacn:: typeclasses eauto :name: typeclasses eauto - This tactic uses a different resolution engine than :tacn:`eauto` and - :tacn:`auto`. The main differences are the following: + This proof search tactic implements the resolution engine that is run + implicitly during type-checking. This tactic uses a different resolution + engine than :tacn:`eauto` and :tacn:`auto`. The main differences are the + following: + Contrary to :tacn:`eauto` and :tacn:`auto`, the resolution is done entirely in the new proof engine (as of Coq 8.6), meaning that backtracking is @@ -418,6 +432,17 @@ few other commands related to typeclasses. resolution with the local hypotheses use full conversion during unification. + + The mode hints (see :cmd:`Hint Mode`) associated to a class are + taken into account by :tacn:`typeclasses eauto`. When a goal + does not match any of the declared modes for its head (if any), + instead of failing like :tacn:`eauto`, the goal is suspended and + resolution proceeds on the remaining goals. + If after one run of resolution, there remains suspended goals, + resolution is launched against on them, until it reaches a fixed + point when the set of remaining suspended goals does not change. + Using `solve [typeclasses eauto]` can be used to ensure that + no suspended goals remain. + + When considering local hypotheses, we use the union of all the modes declared in the given databases. diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 7adb25cbd6..a08495badd 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -122,60 +122,92 @@ in a universe strictly higher than :g:`Set`. Polymorphic, Monomorphic ------------------------- -.. cmd:: Polymorphic @definition +.. attr:: universes(polymorphic) - As shown in the examples, polymorphic definitions and inductives can be - declared using the ``Polymorphic`` prefix. + This attribute can be used to declare universe polymorphic + definitions and inductive types. There is also a legacy syntax + using the ``Polymorphic`` prefix (see :n:`@legacy_attr`) which, as + shown in the examples, is more commonly used. .. flag:: Universe Polymorphism - Once enabled, this flag will implicitly prepend ``Polymorphic`` to any - definition of the user. + This flag is off by default. When it is on, new declarations are + polymorphic unless the :attr:`universes(monomorphic)` attribute is + used. -.. cmd:: Monomorphic @definition +.. attr:: universes(monomorphic) - When the :flag:`Universe Polymorphism` flag is set, to make a definition - producing global universe constraints, one can use the ``Monomorphic`` prefix. + This attribute can be used to declare universe monomorphic + definitions and inductive types (i.e. global universe constraints + are produced), even when the :flag:`Universe Polymorphism` flag is + on. There is also a legacy syntax using the ``Monomorphic`` prefix + (see :n:`@legacy_attr`). -Many other commands support the ``Polymorphic`` flag, including: +Many other commands can be used to declare universe polymorphic or +monomorphic constants depending on whether the :flag:`Universe +Polymorphism` flag is on or the :attr:`universes(polymorphic)` or +:attr:`universes(monomorphic)` attributes are used: -.. TODO add links on each of these? +- :cmd:`Lemma`, :cmd:`Axiom`, etc. can be used to declare universe + polymorphic constants. -- ``Lemma``, ``Axiom``, and all the other “definition” keywords support - polymorphism. +- Using the :attr:`universes(polymorphic)` attribute with the + :cmd:`Section` command will locally set the polymorphism flag inside + the section. -- :cmd:`Section` will locally set the polymorphism flag inside the section. +- :cmd:`Variable`, :cmd:`Context`, :cmd:`Universe` and + :cmd:`Constraint` in a section support polymorphism. See + :ref:`universe-polymorphism-in-sections` for more details. -- ``Variables``, ``Context``, ``Universe`` and ``Constraint`` in a section support - polymorphism. See :ref:`universe-polymorphism-in-sections` for more details. +- Using the :attr:`universes(polymorphic)` attribute with the + :cmd:`Hint Resolve` or :cmd:`Hint Rewrite` commands will make + :tacn:`auto` / :tacn:`rewrite` use the hint polymorphically, not at + a single instance. -- :cmd:`Hint Resolve` and :cmd:`Hint Rewrite` will use the auto/rewrite hint - polymorphically, not at a single instance. +.. _cumulative: Cumulative, NonCumulative ------------------------- -Polymorphic inductive types, coinductive types, variants and records can be -declared cumulative using the :g:`Cumulative` prefix. +.. attr:: universes(cumulative) -.. cmd:: Cumulative @inductive + Polymorphic inductive types, coinductive types, variants and + records can be declared cumulative using this attribute or the + legacy ``Cumulative`` prefix (see :n:`@legacy_attr`) which, as + shown in the examples, is more commonly used. - Declares the inductive as cumulative + This means that two instances of the same inductive type (family) + are convertible based on the universe variances; they do not need + to be equal. -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. + .. exn:: The cumulative and noncumulative attributes can only be used in a polymorphic context. -.. cmd:: NonCumulative @inductive + Using this attribute requires being in a polymorphic context, + i.e. either having the :flag:`Universe Polymorphism` flag on, or + having used the :attr:`universes(polymorphic)` attribute as + well. - Declares the inductive as non-cumulative + .. note:: + + ``#[ universes(polymorphic), universes(cumulative) ]`` can be + abbreviated into ``#[ universes(polymorphic, cumulative) ]``. .. flag:: Polymorphic Inductive Cumulativity - When this flag is on, it sets all following polymorphic inductive - types as cumulative (it is off by default). + When this flag is on (it is off by default), it makes all + subsequent *polymorphic* inductive definitions cumulative, unless + the :attr:`universes(noncumulative)` attribute is used. It has no + effect on *monomorphic* inductive definitions. + +.. attr:: universes(noncumulative) + + Declares the inductive type as non-cumulative even if the + :flag:`Polymorphic Inductive Cumulativity` flag is on. There is + also a legacy syntax using the ``NonCumulative`` prefix (see + :n:`@legacy_attr`). + + This means that two instances of the same inductive type (family) + are convertible only if all the universes are equal. Consider the examples below. @@ -218,34 +250,10 @@ The following is an example of a record with non-trivial subtyping relation: E[Γ] ⊢ \mathsf{packType}@\{i\} =_{βδιζη} \mathsf{packType}@\{j\}~\mbox{ whenever }~i ≤ j -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 :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. - -Consider the following examples. - -.. coqtop:: all reset - - Fail Monomorphic Cumulative Inductive Unit := unit. - -.. coqtop:: all reset - - Fail Monomorphic NonCumulative Inductive Unit := unit. - -.. coqtop:: all reset - - Set Polymorphic Inductive Cumulativity. - Inductive Unit := unit. - An example of a proof using cumulativity ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. coqtop:: in +.. coqtop:: in reset Set Universe Polymorphism. Set Polymorphic Inductive Cumulativity. @@ -366,25 +374,25 @@ to universes and explicitly instantiate polymorphic definitions. In the monorphic case, this command declares a new global universe named :g:`ident`, which can be referred to using its qualified name as well. Global universe names live in a separate namespace. The - command supports the ``Polymorphic`` flag only in sections, meaning the - universe quantification will be discharged on each section definition + command supports the :attr:`universes(polymorphic)` attribute (or + the ``Polymorphic`` prefix) only in sections, meaning the universe + quantification will be discharged on each section definition independently. -.. cmd:: Constraint @universe_constraint - Polymorphic Constraint @universe_constraint + .. exn:: Polymorphic universes can only be declared inside sections, use Monomorphic Universe instead. + :undocumented: - This command declares a new constraint between named universes. +.. cmd:: Constraint @univ_constraint + Polymorphic Constraint @univ_constraint - .. productionlist:: coq - universe_constraint : `qualid` < `qualid` - : `qualid` <= `qualid` - : `qualid` = `qualid` + This command declares a new constraint between named universes. If consistent, the constraint is then enforced in the global environment. Like :cmd:`Universe`, it can be used with the - ``Polymorphic`` prefix in sections only to declare constraints - discharged at section closing time. One cannot declare a global - constraint on polymorphic universes. + :attr:`universes(polymorphic)` attribute (or the ``Polymorphic`` + prefix) in sections only to declare constraints discharged at + section closing time. One cannot declare a global constraint on + polymorphic universes. .. exn:: Undeclared universe @ident. :undocumented: @@ -392,6 +400,9 @@ to universes and explicitly instantiate polymorphic definitions. .. exn:: Universe inconsistency. :undocumented: + .. exn:: Polymorphic universe constraints can only be declared inside sections, use Monomorphic Constraint instead + :undocumented: + Polymorphic definitions ~~~~~~~~~~~~~~~~~~~~~~~ @@ -529,8 +540,8 @@ sections, except in the following ways: Polymorphic Universe i. Fail Constraint i = i. - This includes constraints implictly declared by commands such as - :cmd:`Variable`, which may as a such need to be used with universe + This includes constraints implicitly declared by commands such as + :cmd:`Variable`, which may need to be used with universe polymorphism activated (locally by attribute or globally by option): .. coqtop:: all diff --git a/doc/sphinx/appendix/history-and-changes/index.rst b/doc/sphinx/appendix/history-and-changes/index.rst new file mode 100644 index 0000000000..50ffec8e3f --- /dev/null +++ b/doc/sphinx/appendix/history-and-changes/index.rst @@ -0,0 +1,21 @@ +.. _history-and-changes: + +========================== +History and recent changes +========================== + +This chapter is divided in two parts. The first one is about the +:ref:`early history of Coq <history>` and is presented in +chronological order. The second one provides :ref:`release notes +about recent versions of Coq <changes>` and is presented in reverse +chronological order. When updating your copy of Coq to a new version +(especially a new major version), it is strongly recommended that you +read the corresponding release notes. They may contain advice that +will help you understand the differences with the previous version and +upgrade your projects. + +.. toctree:: + :maxdepth: 1 + + ../../history + ../../changes diff --git a/doc/sphinx/appendix/indexes/index.rst b/doc/sphinx/appendix/indexes/index.rst new file mode 100644 index 0000000000..a5032ff822 --- /dev/null +++ b/doc/sphinx/appendix/indexes/index.rst @@ -0,0 +1,24 @@ +:orphan: + +.. _indexes: + +======== +Indexes +======== + +We provide various specialized indexes that are helpful to quickly +find what you are looking for. + +.. toctree:: + + ../../genindex + ../../coq-cmdindex + ../../coq-tacindex + ../../coq-optindex + ../../coq-exnindex + +For reference, here are direct links to the documentation of: + +- :ref:`flags, options and tables <flags-options-tables>`; +- controlling the display of warning messages with the :opt:`Warnings` + option. diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 1d0c937792..5ca0d8b81f 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -1,8 +1,10 @@ +.. _changes: + -------------- Recent changes -------------- -.. ifconfig:: not coq_config.is_a_released_version +.. ifconfig:: not is_a_released_version .. include:: ../unreleased.rst @@ -50,23 +52,28 @@ __ 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**. +Additionally, while the :tacn:`omega` tactic is not yet deprecated in +this version of Coq, it should soon be the case and we already +recommend users to switch to :tacn:`lia` in new proof scripts (see +also the warning message in the :ref:`corresponding chapter <omega>`). -Maxime Dénès, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Michael -Soegtrop, Théo Zimmermann worked on maintaining and improving the -continuous integration system and package building infrastructure. +The ``dev/doc/critical-bugs`` file documents the known critical bugs +of |Coq| and affected releases. See the `Changes in 8.11+beta1`_ +section and following sections for the detailed list of changes, +including potentially breaking changes marked with **Changed**. -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 +Coq's documentation is available at https://coq.github.io/doc/v8.11/api (documentation of +the ML API), https://coq.github.io/doc/v8.11/refman (reference +manual), and https://coq.github.io/doc/v8.11/stdlib (documentation of the standard library). +Maxime Dénès, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Michael +Soegtrop and Théo Zimmermann worked on maintaining and improving the +continuous integration system and package building infrastructure. + The OPAM repository for |Coq| packages has been maintained by -Karl Palmskog, Matthieu Sozeau, Enrico Tassi with contributions -from many users. A list of packages is available at +Guillaume Claret, Karl Palmskog, Matthieu Sozeau and 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 @@ -153,7 +160,7 @@ Changes in 8.11+beta1 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)` + `Arguments foo x y & z`. See :ref:`bidirectionality_hints` (`#10049 <https://github.com/coq/coq/pull/10049>`_, by Maxime Dénès with help from Enrico Tassi). - **Added:** @@ -209,13 +216,13 @@ Changes in 8.11+beta1 - **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 + :cmd:`Arguments` 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 +- **Added:** :attr:`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). @@ -350,11 +357,8 @@ Changes in 8.11+beta1 `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 + goal by instantiating the hidden evar.) + This feature 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 @@ -512,6 +516,133 @@ Changes in 8.11+beta1 (`#10471 <https://github.com/coq/coq/pull/10471>`_, by Emilio Jesús Gallego Arias). +Changes in 8.11.0 +~~~~~~~~~~~~~~~~~ + +**Kernel** + +- **Changed:** the native compilation (:tacn:`native_compute`) now + creates a directory to contain temporary files instead of putting + them in the root of the system temporary directory (`#11081 + <https://github.com/coq/coq/pull/11081>`_, by Gaëtan Gilbert). +- **Fixed:** `#11360 <https://github.com/issues/11360>`_. + Broken section closing when a template polymorphic inductive type depends on + a section variable through its parameters (`#11361 + <https://github.com/coq/coq/pull/11361>`_, by Gaëtan Gilbert). +- **Fixed:** The type of :g:`Set+1` would be computed to be itself, + leading to a proof of False (`#11422 + <https://github.com/coq/coq/pull/11422>`_, by Gaëtan Gilbert). + +**Specification language, type inference** + +- **Changed:** Heuristics for universe minimization to :g:`Set`: only + minimize flexible universes (`#10657 <https://github.com/coq/coq/pull/10657>`_, + by Gaëtan Gilbert with help from Maxime Dénès and Matthieu Sozeau). +- **Fixed:** + A dependency was missing when looking for default clauses in the + algorithm for printing pattern matching clauses (`#11233 + <https://github.com/coq/coq/pull/11233>`_, by Hugo Herbelin, fixing + `#11231 <https://github.com/coq/coq/pull/11231>`_, reported by Barry + Jay). + +**Notations** + +- **Fixed:** + :cmd:`Print Visibility` was failing in the presence of only-printing notations + (`#11276 <https://github.com/coq/coq/pull/11276>`_, + by Hugo Herbelin, fixing `#10750 <https://github.com/coq/coq/pull/10750>`_). +- **Fixed:** + Recursive notations with custom entries were incorrectly parsing `constr` + instead of custom grammars (`#11311 <https://github.com/coq/coq/pull/11311>`_ + by Maxime Dénès, fixes `#9532 <https://github.com/coq/coq/pull/9532>`_, + `#9490 <https://github.com/coq/coq/pull/9490>`_). + +**Tactics** + +- **Changed:** + The tactics :tacn:`eapply`, :tacn:`refine` and variants no + longer allow shelved goals to be solved by typeclass resolution + (`#10762 <https://github.com/coq/coq/pull/10762>`_, by Matthieu Sozeau). +- **Fixed:** The optional string argument to :tacn:`time` is now + properly quoted under :cmd:`Print Ltac` (`#11203 + <https://github.com/coq/coq/pull/11203>`_, fixes `#10971 + <https://github.com/coq/coq/issues/10971>`_, by Jason Gross) +- **Fixed:** + Efficiency regression of :tacn:`lia` introduced in 8.10 + by PR `#9725 <https://github.com/coq/coq/pull/9725>`_ + (`#11263 <https://github.com/coq/coq/pull/11263>`_, + fixes `#11063 <https://github.com/coq/coq/issues/11063>`_, + and `#11242 <https://github.com/coq/coq/issues/11242>`_, + and `#11270 <https://github.com/coq/coq/issues/11270>`_, by Frédéric Besson). +- **Deprecated:** + The undocumented ``omega with`` tactic variant has been deprecated. + Using :tacn:`lia` is the recommended replacement, though the old semantics + of ``omega with *`` can be recovered with ``zify; omega`` + (`#11337 <https://github.com/coq/coq/pull/11337>`_, + by Emilio Jesus Gallego Arias). +- **Fixed** + For compatibility reasons, in 8.11, :tacn:`zify` does not support :g:`Z.pow_pos` by default. + It can be enabled by explicitly loading the module :g:`ZifyPow` + (`#11430 <https://github.com/coq/coq/pull/11430>`_ by Frédéric Besson + fixes `#11191 <https://github.com/coq/coq/issues/11191>`_). + +**Tactic language** + +- **Fixed:** + Syntax of tactic `cofix ... with ...` was broken since Coq 8.10 + (`#11241 <https://github.com/coq/coq/pull/11241>`_, + by Hugo Herbelin). + +**Commands and options** + +- **Deprecated:** The `-load-ml-source` and `-load-ml-object` command + line options have been deprecated; their use was very limited, you + can achieve the same by adding object files in the linking step or + by using a plugin (`#11428 + <https://github.com/coq/coq/pull/11428>`_, by Emilio Jesus Gallego + Arias). + +**Tools** + +- **Fixed:** + ``coqtop --version`` was broken when called in the middle of an installation process + (`#11255 <https://github.com/coq/coq/pull/11255>`_, by Hugo Herbelin, fixing + `#11254 <https://github.com/coq/coq/pull/11254>`_). +- **Deprecated:** The ``-quick`` command is renamed to ``-vio``, for + consistency with the new ``-vos`` and ``-vok`` flags. Usage of + ``-quick`` is now deprecated (`#11280 + <https://github.com/coq/coq/pull/11280>`_, by Arthur Charguéraud). +- **Fixed:** + ``coq_makefile`` does not break when using the ``CAMLPKGS`` variable + together with an unpacked (``mllib``) plugin (`#11357 + <https://github.com/coq/coq/pull/11357>`_, by Gaëtan Gilbert). +- **Fixed:** + ``coqdoc`` with option ``-g`` (Gallina only) now correctly prints + commands with attributes (`#11394 <https://github.com/coq/coq/pull/11394>`_, + fixes `#11353 <https://github.com/coq/coq/issues/11353>`_, + by Karl Palmskog). + +**CoqIDE** + +- **Changed:** CoqIDE now uses the GtkSourceView native implementation + of the autocomplete mechanism (`#11400 + <https://github.com/coq/coq/pull/11400>`_, by Pierre-Marie Pédrot). + +**Standard library** + +- **Removed:** Export of module :g:`RList` in :g:`Ranalysis` and + :g:`Ranalysis_reg`. Module :g:`RList` is still there but must be + imported explicitly where required (`#11396 + <https://github.com/coq/coq/pull/11396>`_, by Michael Soegtrop). + +**Infrastructure and dependencies** + +- **Added:** + Build date can now be overridden by setting the `SOURCE_DATE_EPOCH` + environment variable + (`#11227 <https://github.com/coq/coq/pull/11227>`_, + by Bernhard M. Wiedemann). + Version 8.10 ------------ @@ -554,7 +685,7 @@ reference manual. Here are the most important user-visible changes: - Universes: - - Added :cmd:`Print Universes Subgraph` variant of :cmd:`Print Universes`. + - Added Subgraph variant to :cmd:`Print Universes`. Try for instance :g:`Print Universes Subgraph(sigT2.u1 sigT_of_sigT2.u1 projT3_eq.u1).` (`#8451 <https://github.com/coq/coq/pull/8451>`_, by Gaëtan Gilbert). @@ -1185,7 +1316,7 @@ Changes in 8.10+beta3 rules governing template-polymorphic types. To help users incrementally fix this issue, a command line option - `-no-template-check` and a global flag :flag:`Template Check` are + `-no-template-check` and a global flag ``Template Check`` are available to selectively disable the new check. Use at your own risk. (`#9918 <https://github.com/coq/coq/pull/9918>`_, by Matthieu Sozeau @@ -1377,7 +1508,7 @@ changes: - Removed deprecated commands ``Arguments Scope`` and ``Implicit Arguments`` in favor of :cmd:`Arguments (scopes)` and - :cmd:`Arguments (implicits)`, with the help of Jasper Hugunin. + :cmd:`Arguments`, with the help of Jasper Hugunin. - New flag :flag:`Uniform Inductive Parameters` by Jasper Hugunin to avoid repeating uniform parameters in constructor declarations. @@ -4584,7 +4715,7 @@ Specification language Module system -- Include Type is now deprecated since Include now accept both modules and +- Include Type is now deprecated since Include now accepts both modules and module types. - Declare ML Module supports Local option. - The sharing between non-logical object and the management of the diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index f1dd7479c5..2ed9ec21b3 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -1,8 +1,8 @@ #!/usr/bin/env python3 ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## -## v # INRIA, CNRS and contributors - Copyright 1999-2019 ## -## <O___,, # (see CREDITS file for the list of authors) ## +## v # Copyright INRIA, CNRS and contributors ## +## <O___,, # (see version control and CREDITS file for authors & dates) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## ## # GNU Lesser General Public License Version 2.1 ## @@ -46,7 +46,7 @@ with open("refman-preamble.rst") as s: # -- General configuration ------------------------------------------------ # If your documentation needs a minimal Sphinx version, state it here. -needs_sphinx = '1.7.8' +needs_sphinx = '1.8.0' # Add any Sphinx extension module names here, as strings. They can be # extensions coming with Sphinx (named 'sphinx.ext.*') or your custom @@ -100,7 +100,7 @@ def copy_formatspecific_files(app): def setup(app): app.connect('builder-inited', copy_formatspecific_files) - app.add_config_value('coq_config', coq_config, 'env') + app.add_config_value('is_a_released_version', coq_config.is_a_released_version, 'env') # The master toctree document. # We create this file in `copy_master_doc` above. @@ -108,7 +108,7 @@ master_doc = "index" # General information about the project. project = 'Coq' -copyright = '1999-2019, Inria, CNRS and contributors' +copyright = '1999-2020, Inria, CNRS and contributors' author = 'The Coq Development Team' # The version info for the project you're documenting, acts as replacement for @@ -183,16 +183,18 @@ todo_include_todos = False nitpicky = True nitpick_ignore = [ ('token', token) for token in [ + 'assums', + 'binders', 'collection', - 'command', 'dirpath', + 'ind_body', 'modpath', 'module', - 'red_expr', + 'simple_tactic', 'symbol', - 'tactic', 'term_pattern', 'term_pattern_string', + 'toplevel_selector', ]] # -- Options for HTML output ---------------------------------------------- diff --git a/doc/sphinx/coq-cmdindex.rst b/doc/sphinx/coq-cmdindex.rst index fd0b342ae4..18d2e379ac 100644 --- a/doc/sphinx/coq-cmdindex.rst +++ b/doc/sphinx/coq-cmdindex.rst @@ -2,6 +2,8 @@ .. hack to get index in TOC +.. _command_index: + ----------------- Command index ----------------- diff --git a/doc/sphinx/coq-tacindex.rst b/doc/sphinx/coq-tacindex.rst index 31b2f7f8cb..cddcdf83e8 100644 --- a/doc/sphinx/coq-tacindex.rst +++ b/doc/sphinx/coq-tacindex.rst @@ -2,6 +2,8 @@ .. hack to get index in TOC +.. _tactic_index: + ------------- Tactic index ------------- diff --git a/doc/sphinx/coqdoc.css b/doc/sphinx/coqdoc.css index 2ac2af1c13..a325a33842 100644 --- a/doc/sphinx/coqdoc.css +++ b/doc/sphinx/coqdoc.css @@ -1,7 +1,7 @@ /************************************************************************/ /* * The Coq Proof Assistant / The Coq Development Team */ -/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */ -/* <O___,, * (see CREDITS file for the list of authors) */ +/* v * Copyright INRIA, CNRS and contributors */ +/* <O___,, * (see version control and CREDITS file for authors & dates) */ /* \VV/ **************************************************************/ /* // * This file is distributed under the terms of the */ /* * GNU Lesser General Public License Version 2.1 */ diff --git a/doc/sphinx/genindex.rst b/doc/sphinx/genindex.rst index 29f792b3aa..e3a27fd7c4 100644 --- a/doc/sphinx/genindex.rst +++ b/doc/sphinx/genindex.rst @@ -2,6 +2,6 @@ .. hack to get index in TOC ------ -Index ------ +------------- +General index +------------- diff --git a/doc/sphinx/history.rst b/doc/sphinx/history.rst index c4a48d6985..153dc1f368 100644 --- a/doc/sphinx/history.rst +++ b/doc/sphinx/history.rst @@ -1,3 +1,5 @@ +.. _history: + -------------------- Early history of Coq -------------------- diff --git a/doc/sphinx/index.html.rst b/doc/sphinx/index.html.rst index 0a20d1c47b..6069ed42fe 100644 --- a/doc/sphinx/index.html.rst +++ b/doc/sphinx/index.html.rst @@ -8,84 +8,37 @@ Contents -------- .. toctree:: - :caption: Indexes - - genindex - coq-cmdindex - coq-tacindex - coq-optindex - coq-exnindex - -.. No entries yet - * :index:`thmindex` - -.. toctree:: - :caption: Preamble self - history - changes .. toctree:: - :caption: The language + :caption: Specification language - language/gallina-specification-language - language/gallina-extensions - language/coq-library - language/cic - language/module-system + language/core/index + language/extensions/index .. toctree:: - :caption: The proof engine + :caption: Proofs - proof-engine/vernacular-commands - proof-engine/proof-handling - proof-engine/tactics - proof-engine/ltac - proof-engine/ltac2 - proof-engine/detailed-tactic-examples - proof-engine/ssreflect-proof-language + proofs/writing-proofs/index + proofs/automatic-tactics/index + proofs/creating-tactics/index .. toctree:: - :caption: User extensions + :caption: Using Coq - user-extensions/syntax-extensions - user-extensions/proof-schemes + using/libraries/index + using/tools/index .. toctree:: - :caption: Practical tools + :caption: Appendix - practical-tools/coq-commands - practical-tools/utilities - practical-tools/coqide - -.. toctree:: - :caption: Addendum - - addendum/extended-pattern-matching - addendum/implicit-coercions - addendum/canonical-structures - addendum/type-classes - addendum/omega - addendum/micromega - addendum/extraction - addendum/program - addendum/ring - addendum/nsatz - addendum/generalized-rewriting - addendum/parallel-proof-processing - addendum/miscellaneous-extensions - addendum/universe-polymorphism - addendum/sprop + appendix/history-and-changes/index + appendix/indexes/index + zebibliography -.. toctree:: - :caption: Reference +.. No entries yet + * :index:`thmindex` - zebibliography .. include:: license.rst - -.. [#PG] Proof-General is available at https://proofgeneral.github.io/. - Optionally, you can enhance it with the minor mode - Company-Coq :cite:`Pit16` - (see https://github.com/cpitclaudel/company-coq). diff --git a/doc/sphinx/index.latex.rst b/doc/sphinx/index.latex.rst index 5562736997..62d9525194 100644 --- a/doc/sphinx/index.latex.rst +++ b/doc/sphinx/index.latex.rst @@ -10,81 +10,39 @@ Introduction .. include:: license.rst -.. [#PG] Proof-General is available at https://proofgeneral.github.io/. - Optionally, you can enhance it with the minor mode - Company-Coq :cite:`Pit16` - (see https://github.com/cpitclaudel/company-coq). - -.. include:: history.rst - -.. include:: changes.rst - ------------- -The language ------------- +---------------------- +Specification language +---------------------- .. toctree:: - language/gallina-specification-language - language/gallina-extensions - language/coq-library - language/cic - language/module-system + language/core/index + language/extensions/index ----------------- -The proof engine ----------------- +------ +Proofs +------ .. toctree:: - proof-engine/vernacular-commands - proof-engine/proof-handling - proof-engine/tactics - proof-engine/ltac - proof-engine/ltac2 - proof-engine/detailed-tactic-examples - proof-engine/ssreflect-proof-language + proofs/writing-proofs/index + proofs/automatic-tactics/index + proofs/creating-tactics/index ---------------- -User extensions ---------------- +--------- +Using Coq +--------- .. toctree:: - user-extensions/syntax-extensions - user-extensions/proof-schemes - ---------------- -Practical tools ---------------- - -.. toctree:: - - practical-tools/coq-commands - practical-tools/utilities - practical-tools/coqide + using/libraries/index + using/tools/index -------- -Addendum +Appendix -------- .. toctree:: - addendum/extended-pattern-matching - addendum/implicit-coercions - addendum/canonical-structures - addendum/type-classes - addendum/omega - addendum/micromega - addendum/extraction - addendum/program - addendum/ring - addendum/nsatz - addendum/generalized-rewriting - addendum/parallel-proof-processing - addendum/miscellaneous-extensions - addendum/universe-polymorphism - addendum/sprop - -.. toctree:: + appendix/history-and-changes/index zebibliography diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index bcdf3277ad..b059fb4069 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -1,105 +1,68 @@ -This document is the Reference Manual of the |Coq| proof assistant. -To start using Coq, it is advised to first read a tutorial. -Links to several tutorials can be found at -https://coq.inria.fr/documentation and -https://github.com/coq/coq/wiki#coq-tutorials - -The |Coq| system is designed to develop mathematical proofs, and -especially to write formal specifications, programs and to verify that -programs are correct with respect to their specifications. It provides a -specification language named |Gallina|. Terms of |Gallina| can represent -programs as well as properties of these programs and proofs of these -properties. Using the so-called *Curry-Howard isomorphism*, programs, -properties and proofs are formalized in the same language called -*Calculus of Inductive Constructions*, that is a -:math:`\lambda`-calculus with a rich type system. All logical judgments -in |Coq| are typing judgments. The very heart of the |Coq| system is the -type checking algorithm that checks the correctness of proofs, in other -words that checks that a program complies to its specification. |Coq| also -provides an interactive proof assistant to build proofs using specific -programs called *tactics*. - -All services of the |Coq| proof assistant are accessible by interpretation -of a command language called *the vernacular*. - -Coq has an interactive mode in which commands are interpreted as the -user types them in from the keyboard and a compiled mode where commands -are processed from a file. - -- In interactive mode, users can develop their theories and proofs step by - step, and query the system for available theorems and definitions. The - interactive mode is generally run with the help of an IDE, such - as CoqIDE, documented in :ref:`coqintegrateddevelopmentenvironment`, - Emacs with Proof-General :cite:`Asp00` [#PG]_, - or jsCoq to run Coq in your browser (see https://github.com/ejgallego/jscoq). - The `coqtop` read-eval-print-loop can also be used directly, for debugging - purposes. - -- The compiled mode acts as a proof checker taking a file containing a - whole development in order to ensure its correctness. Moreover, - |Coq|’s compiler provides an output file containing a compact - representation of its input. The compiled mode is run with the `coqc` - command. - -.. seealso:: :ref:`thecoqcommands`. - -How to read this book ---------------------- - -This is a Reference Manual, so it is not intended for continuous reading. -We recommend using the various indexes to quickly locate the documentation -you are looking for. There is a global index, and a number of specific indexes -for tactics, vernacular commands, and error messages and warnings. -Nonetheless, the manual has some structure that is explained below. - -- The first part describes the specification language, |Gallina|. - Chapters :ref:`gallinaspecificationlanguage` and :ref:`extensionsofgallina` describe the concrete - syntax as well as the meaning of programs, theorems and proofs in the - Calculus of Inductive Constructions. Chapter :ref:`thecoqlibrary` describes the - standard library of |Coq|. Chapter :ref:`calculusofinductiveconstructions` is a mathematical description - of the formalism. Chapter :ref:`themodulesystem` describes the module - system. - -- The second part describes the proof engine. It is divided in six - 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 - evaluation, loading and compiling files. How to start and stop - 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 - are described in Chapter :ref:`detailedexamplesoftactics`. - Finally, the |SSR| proof language is presented in - Chapter :ref:`thessreflectprooflanguage`. - -- The third part describes how to extend the syntax of |Coq| in - Chapter :ref:`syntaxextensionsandinterpretationscopes` and how to define - new induction principles in Chapter :ref:`proofschemes`. - -- In the fourth part more practical tools are documented. First in - Chapter :ref:`thecoqcommands`, the usage of `coqc` (batch mode) and - `coqtop` (interactive mode) with their options is described. Then, - in Chapter :ref:`utilities`, various utilities that come with the - |Coq| distribution are presented. Finally, Chapter :ref:`coqintegrateddevelopmentenvironment` - describes CoqIDE. - -- The fifth part documents a number of advanced features, including coercions, - canonical structures, typeclasses, program extraction, and specialized - solvers and tactics. See the table of contents for a complete list. - -List of additional documentation --------------------------------- - -This manual does not contain all the documentation the user may need -about |Coq|. Various informations can be found in the following documents: - -Installation - A text file `INSTALL` that comes with the sources explains how to - install |Coq|. - -The |Coq| standard library - A commented version of sources of the |Coq| standard library - (including only the specifications, the proofs are removed) is - available at https://coq.inria.fr/stdlib/. +This is the reference manual of |Coq|. Coq is an interactive theorem +prover. It lets you formalize mathematical concepts and then helps +you interactively generate machine-checked proofs of theorems. +Machine checking gives users much more confidence that the proofs are +correct compared to human-generated and -checked proofs. Coq has been +used in a number of flagship verification projects, including the +`CompCert verified C compiler <http://compcert.inria.fr/>`_, and has +served to verify the proof of the `four color theorem +<https://github.com/math-comp/fourcolor>`_ (among many other +mathematical formalizations). + +Users generate proofs by entering a series of tactics that constitute +steps in the proof. There are many built-in tactics, some of which +are elementary, while others implement complex decision procedures +(such as :tacn:`lia`, a decision procedure for linear integer +arithmetic). :ref:`Ltac <ltac>` and its planned replacement, +:ref:`Ltac2 <ltac2>`, provide languages to define new tactics by +combining existing tactics with looping and conditional constructs. +These permit automation of large parts of proofs and sometimes entire +proofs. Furthermore, users can add novel tactics or functionality by +creating Coq plugins using OCaml. + +The Coq kernel, a small part of Coq, does the final verification that +the tactic-generated proof is valid. Usually the tactic-generated +proof is indeed correct, but delegating proof verification to the +kernel means that even if a tactic is buggy, it won't be able to +introduce an incorrect proof into the system. + +Finally, Coq also supports extraction of verified programs to +programming languages such as OCaml and Haskell. This provides a way +of executing Coq code efficiently and can be used to create verified +software libraries. + +To learn Coq, beginners are advised to first start with a tutorial / +book. Several such tutorials / books are listed at +https://coq.inria.fr/documentation. + +This manual is organized in three main parts, plus an appendix: + +- **The first part presents the specification language of Coq**, that + allows to define programs and state mathematical theorems. + :ref:`core-language` presents the language that the kernel of Coq + understands. :ref:`extensions` presents the richer language, with + notations, implicits, etc. that a user can use and which is + translated down to the language of the kernel by means of an + "elaboration process". + +- **The second part presents the interactive proof mode**, the central + feature of Coq. :ref:`writing-proofs` introduces this interactive + proof mode and the available proof languages. + :ref:`automatic-tactics` presents some more advanced tactics, while + :ref:`writing-tactics` is about the languages that allow a user to + combine tactics together and develop new ones. + +- **The third part shows how to use Coq in practice.** + :ref:`libraries` presents some of the essential reusable blocks from + the ecosystem and some particularly important extensions such as the + program extraction mechanism. :ref:`tools` documents important + tools that a user needs to build a Coq project. + +- In the appendix, :ref:`history-and-changes` presents the history of + Coq and changes in recent releases. This is an important reference + if you upgrade the version of Coq that you use. The various + :ref:`indexes <indexes>` are very useful to **quickly browse the + manual and find what you are looking for.** They are often the main + entry point to the manual. + +The full table of contents is presented below: diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 4beaff70f5..09a3897a06 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -47,8 +47,7 @@ provable. An object of type :math:`\Prop` is called a proposition. The sort :math:`\SProp` is like :math:`\Prop` but the propositions in :math:`\SProp` are known to have irrelevant proofs (all proofs are 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 +See :ref:`sprop` for information about using :math:`\SProp`, and :cite:`Gilbert:POPL2019` for meta theoretical considerations. @@ -1200,45 +1199,47 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or at level :math:`\Type` (without annotations or hiding it behind a definition) template polymorphic if possible. - This can be prevented using the ``universes(notemplate)`` + This can be prevented using the :attr:`universes(notemplate)` attribute. + Template polymorphism and full universe polymorphism (see Chapter + :ref:`polymorphicuniverses`) are incompatible, so if the latter is + enabled (through the :flag:`Universe Polymorphism` flag or the + :attr:`universes(polymorphic)` attribute) it will prevail over + automatic template polymorphism. + .. warn:: Automatically declaring @ident as template polymorphic. - Warning ``auto-template`` can be used to find which types are - implicitly declared template polymorphic by :flag:`Auto Template - Polymorphism`. + Warning ``auto-template`` can be used (it is off by default) to + find which types are implicitly declared template polymorphic by + :flag:`Auto Template Polymorphism`. An inductive type can be forced to be template polymorphic using - the ``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. - - This error is raised when the `#[universes(template)]` attribute is - on but the inductive cannot be made polymorphic on any universe or be - inferred to live in :math:`\Prop` or :math:`\Set`. - - Template polymorphism and universe polymorphism (see Chapter - :ref:`polymorphicuniverses`) are incompatible, so if the later is - enabled it will prevail over automatic template polymorphism and - cause an error when using the ``universes(template)`` attribute. - -.. flag:: Template Check - - 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 - code from Coq versions < 8.10 which did not implement this check. - The `Coq89.v` compatibility file sets this flag globally. A global - ``-no-template-check`` command line option is also available. Use at - your own risk. Use of this flag is recorded in the typing flags - associated to a definition but is *not* supported by the |Coq| - checker (`coqchk`). It will appear in :g:`Print Assumptions` and - :g:`About @ident` output involving inductive declarations that were - (potentially unsoundly) assumed to be template polymorphic. + the :attr:`universes(template)` attribute: in this case, the + warning is not emitted. + +.. attr:: universes(template) + + This attribute can be used to explicitly declare an inductive type + as template polymorphic, whether the :flag:`Auto Template + Polymorphism` flag is on or off. + + .. exn:: template and polymorphism not compatible + + This attribute cannot be used in a full universe polymorphic + context, i.e. if the :flag:`Universe Polymorphism` flag is on or + if the :attr:`universes(polymorphic)` attribute is used. + + .. exn:: Ill-formed template inductive declaration: not polymorphic on any universe. + + The attribute was used but the inductive definition does not + satisfy the criterion to be template polymorphic. + +.. attr:: universes(notemplate) + This attribute can be used to prevent an inductive type to be + template polymorphic, even if the :flag:`Auto Template + Polymorphism` flag is on. In practice, the rule **Ind-Family** is used by |Coq| only when all the inductive types of the inductive definition are declared with an arity diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index cad5e4e67e..39f2ccec29 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -23,7 +23,7 @@ These libraries and developments are available for download at http://coq.inria.fr (see :ref:`userscontributions`). This chapter briefly reviews the |Coq| libraries whose contents can -also be browsed at http://coq.inria.fr/stdlib. +also be browsed at http://coq.inria.fr/stdlib/. @@ -95,25 +95,23 @@ Logic The basic library of |Coq| comes with the definitions of standard (intuitionistic) logical connectives (they are defined as inductive constructions). They are equipped with an appealing syntax enriching the -subclass :token:`form` of the syntactic class :token:`term`. The syntax of -:token:`form` is shown below: - -.. /!\ Please keep the blanks in the lines below, experimentally they produce - a nice last column. Or even better, find a proper way to do this! - -.. productionlist:: - form : True (True) - : False (False) - : ~ `form` (not) - : `form` /\ `form` (and) - : `form` \/ `form` (or) - : `form` -> `form` (primitive implication) - : `form` <-> `form` (iff) - : forall `ident` : `type`, `form` (primitive for all) - : exists `ident` [: `specif`], `form` (ex) - : exists2 `ident` [: `specif`], `form` & `form` (ex2) - : `term` = `term` (eq) - : `term` = `term` :> `specif` (eq) +subclass :token:`form` of the syntactic class :token:`term`. The constructs +for :production:`form` are: + +============================================== ======= +True True +False False +:n:`~ @form` not +:n:`@form /\ @form` and +:n:`@form \/ @form` or +:n:`@form -> @form` primitive implication +:n:`@form <-> @form` iff +:n:`forall @ident : @type, @form` primitive for all +:n:`exists @ident {? @specif}, @form` ex +:n:`exists2 @ident {? @specif}, @form & @form` ex2 +:n:`@term = @term` eq +:n:`@term = @term :> @specif` eq +============================================== ======= .. note:: @@ -281,19 +279,20 @@ In the basic library, we find in ``Datatypes.v`` the definition of the basic data-types of programming, defined as inductive constructions over the sort ``Set``. Some of them come with a special syntax shown below (this syntax table is common with -the next section :ref:`specification`): - -.. productionlist:: - specif : `specif` * `specif` (prod) - : `specif` + `specif` (sum) - : `specif` + { `specif` } (sumor) - : { `specif` } + { `specif` } (sumbool) - : { `ident` : `specif` | `form` } (sig) - : { `ident` : `specif` | `form` & `form` } (sig2) - : { `ident` : `specif` & `specif` } (sigT) - : { `ident` : `specif` & `specif` & `specif` } (sigT2) - term : (`term`, `term`) (pair) - +the next section :ref:`specification`). The constructs for :production:`specif` are: + +============================================= ======= +:n:`@specif * @specif` prod +:n:`@specif + @specif` sum +:n:`@specif + { @specif }` sumor +:n:`{ @specif } + { @specif }` sumbool +:n:`{ @ident : @specif | @form }` sig +:n:`{ @ident : @specif | @form & @form }` sig2 +:n:`{ @ident : @specif & @specif }` sigT +:n:`{ @ident : @specif & @specif & @specif }` sigT2 +============================================= ======= + +The notation for pairs (elements of type prod) is: :n:`(@term, @term)` Programming +++++++++++ diff --git a/doc/sphinx/language/core/index.rst b/doc/sphinx/language/core/index.rst new file mode 100644 index 0000000000..07dcfff444 --- /dev/null +++ b/doc/sphinx/language/core/index.rst @@ -0,0 +1,37 @@ +.. _core-language: + +============= +Core language +============= + +At the heart of the Coq proof assistant is the Coq kernel. While +users have access to a language with many convenient features such as +notations, implicit arguments, etc. (that are presented in the +:ref:`next chapter <extensions>`), such complex terms get translated +down to a core language (the Calculus of Inductive Constructions) that +the kernel understands, and which we present here. Furthermore, while +users can build proofs interactively using tactics (see Chapter +:ref:`writing-proofs`), the role of these tactics is to incrementally +build a "proof term" which the kernel will verify. More precisely, a +proof term is a term of the Calculus of Inductive Constructions whose +type corresponds to a theorem statement. The kernel is a type checker +which verifies that terms have their expected type. + +This separation between the kernel on the one hand and the elaboration +engine and tactics on the other hand follows what is known as the "de +Bruijn criterion" (keeping a small and well delimited trusted code +base within a proof assistant which can be much more complex). This +separation makes it possible to reduce the trust in the whole system +to trusting a smaller, critical component: the kernel. In particular, +users may rely on external plugins that provide advanced and complex +tactics without fear of these tactics being buggy, because the kernel +will have to check their output. + +.. toctree:: + :maxdepth: 1 + + ../gallina-specification-language + ../cic + ../../addendum/universe-polymorphism + ../../addendum/sprop + ../module-system diff --git a/doc/sphinx/language/extensions/index.rst b/doc/sphinx/language/extensions/index.rst new file mode 100644 index 0000000000..f22927d627 --- /dev/null +++ b/doc/sphinx/language/extensions/index.rst @@ -0,0 +1,26 @@ +.. _extensions: + +=================== +Language extensions +=================== + +Elaboration extends the language accepted by the Coq kernel to make it +easier to use. For example, this lets the user omit most type +annotations because they can be inferred, call functions with implicit +arguments which will be inferred as well, extend the syntax with +notations, factorize branches when pattern-matching, etc. In this +chapter, we present these language extensions and we give some +explanations on how this language is translated down to the core +language presented in the :ref:`previous chapter <core-language>`. + +.. toctree:: + :maxdepth: 1 + + ../gallina-extensions + ../../addendum/extended-pattern-matching + ../../user-extensions/syntax-extensions + ../../addendum/implicit-coercions + ../../addendum/type-classes + ../../addendum/canonical-structures + ../../addendum/program + ../../proof-engine/vernacular-commands diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 8caa289a47..18b05e47d3 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -20,26 +20,43 @@ expressions. In this sense, the :cmd:`Record` construction allows defining .. _record_grammar: - .. productionlist:: sentence - record : `record_keyword` `record_body` with … with `record_body` - record_keyword : Record | Inductive | CoInductive - record_body : `ident` [ `binders` ] [: `sort` ] := [ `ident` ] { [ `field` ; … ; `field` ] }. - field : `ident` [ `binders` ] : `type` [ where `notation` ] - : `ident` [ `binders` ] [: `type` ] := `term` - -.. cmd:: Record @ident @binders {? : @sort} := {? @ident} { {*; @ident @binders : @type } } - - The first identifier :token:`ident` is the name of the defined record and :token:`sort` is its - type. The optional identifier following ``:=`` is the name of its constructor. If it is omitted, - the default name :n:`Build_@ident`, where :token:`ident` is the record name, is used. If :token:`sort` is - omitted, the default sort is :math:`\Type`. The identifiers inside the brackets are the names of - fields. For a given field :token:`ident`, its type is :n:`forall @binders, @type`. - Remark that the type of a particular identifier may depend on a previously-given identifier. Thus the - order of the fields is important. Finally, :token:`binders` are parameters of the record. +.. cmd:: {| Record | Structure } @record_definition {* with @record_definition } + :name: Record; Structure + + .. insertprodn record_definition field_body + + .. prodn:: + record_definition ::= {? > } @ident_decl {* @binder } {? : @type } {? @ident } %{ {*; @record_field } %} {? @decl_notations } + record_field ::= {* #[ {*, @attr } ] } @name {? @field_body } {? %| @num } {? @decl_notations } + field_body ::= {* @binder } @of_type + | {* @binder } @of_type := @term + | {* @binder } := @term + + Each :n:`@record_definition` defines a record named by :n:`@ident_decl`. + The constructor name is given by :n:`@ident`. + If the constructor name is not specified, then the default name :n:`Build_@ident` is used, + where :n:`@ident` is the record name. + + If :n:`@type` is + omitted, the default type is :math:`\Type`. The identifiers inside the brackets are the field names. + The type of each field :n:`@ident` is :n:`forall {* @binder }, @type`. + Notice that the type of an identifier can depend on a previously-given identifier. Thus the + order of the fields is important. :n:`@binder` parameters may be applied to the record as a whole + or to individual fields. + + Notations can be attached to fields using the :n:`@decl_notations` annotation. + + :cmd:`Record` and :cmd:`Structure` are synonyms. + + This command supports the :attr:`universes(polymorphic)`, + :attr:`universes(monomorphic)`, :attr:`universes(template)`, + :attr:`universes(notemplate)`, :attr:`universes(cumulative)`, + :attr:`universes(noncumulative)` and :attr:`private(matching)` + attributes. More generally, a record may have explicitly defined (a.k.a. manifest) fields. For instance, we might have: -:n:`Record @ident @binders : @sort := { @ident__1 : @type__1 ; @ident__2 := @term__2 ; @ident__3 : @type__3 }`. +:n:`Record @ident {* @binder } : @sort := { @ident__1 : @type__1 ; @ident__2 := @term__2 ; @ident__3 : @type__3 }`. in which case the correctness of :n:`@type__3` may rely on the instance :n:`@term__2` of :n:`@ident__2` and :n:`@term__2` may in turn depend on :n:`@ident__1`. .. example:: @@ -62,7 +79,7 @@ in which case the correctness of :n:`@type__3` may rely on the instance :n:`@ter Let us now see the work done by the ``Record`` macro. First the macro generates a variant type definition with just one constructor: -:n:`Variant @ident {? @binders } : @sort := @ident__0 {? @binders }`. +:n:`Variant @ident {* @binder } : @sort := @ident__0 {* @binder }`. To build an object of type :token:`ident`, one should provide the constructor :n:`@ident__0` with the appropriate number of terms filling the fields of the record. @@ -155,19 +172,19 @@ available: .. _record_projections_grammar: - .. insertgram term_projection term_projection + .. insertprodn term_projection term_projection - .. productionlist:: coq - term_projection : `term0` .( `qualid` `args_opt` ) - : `term0` .( @ `qualid` `term1_list_opt` ) + .. prodn:: + term_projection ::= @term0 .( @qualid {* @arg } ) + | @term0 .( @ @qualid {* @term1 } ) Syntax of Record projections The corresponding grammar rules are given in the preceding grammar. When :token:`qualid` -denotes a projection, the syntax :n:`@term.(@qualid)` is equivalent to :n:`@qualid @term`, -the syntax :n:`@term.(@qualid {+ @arg })` to :n:`@qualid {+ @arg } @term`. -and the syntax :n:`@term.(@@qualid {+ @term })` to :n:`@@qualid {+ @term } @term`. -In each case, :token:`term` is the object projected and the +denotes a projection, the syntax :n:`@term0.(@qualid)` is equivalent to :n:`@qualid @term0`, +the syntax :n:`@term0.(@qualid {+ @arg })` to :n:`@qualid {+ @arg } @term0`. +and the syntax :n:`@term0.(@@qualid {+ @term0 })` to :n:`@@qualid {+ @term0 } @term0`. +In each case, :token:`term0` is the object projected and the other arguments are the parameters of the inductive type. @@ -183,8 +200,6 @@ other arguments are the parameters of the inductive type. defined with the ``Record`` keyword can be activated with the :flag:`Nonrecursive Elimination Schemes` flag (see :ref:`proofschemes-induction-principles`). -.. note:: ``Structure`` is a synonym of the keyword ``Record``. - .. warn:: @ident cannot be defined. It can happen that the definition of a projection is impossible. @@ -346,16 +361,12 @@ can be alternatively written Definition not (b:bool) := if b then false else true. -More generally, for an inductive type with constructors |C_1| and |C_2|, -we have the following equivalence +More generally, for an inductive type with constructors :n:`@ident__1` +and :n:`@ident__2`, the following terms are equal: -:: +:n:`if @term__0 {? {? as @name } return @term } then @term__1 else @term__2` - if term [dep_ret_type] then term₁ else term₂ ≡ - match term [dep_ret_type] with - | C₁ _ … _ => term₁ - | C₂ _ … _ => term₂ - end +:n:`match @term__0 {? {? as @name } return @term } with | @ident__1 {* _ } => @term__1 | @ident__2 {* _ } => @term__2 end` .. example:: @@ -383,11 +394,13 @@ constructions. There are two variants of them. First destructuring let syntax ++++++++++++++++++++++++++++++ -The expression :g:`let (`\ |ident_1|:g:`, … ,` |ident_n|\ :g:`) :=` |term_0|\ :g:`in` |term_1| performs -case analysis on |term_0| which must be in an inductive type with one -constructor having itself :math:`n` arguments. Variables |ident_1| … |ident_n| are -bound to the :math:`n` arguments of the constructor in expression |term_1|. For -instance, the definition +The expression :n:`let ( {*, @ident__i } ) := @term__0 in @term__1` +performs case analysis on :n:`@term__0` whose type must be an +inductive type with exactly one constructor. The number of variables +:n:`@ident__i` must correspond to the number of arguments of this +contrustor. Then, in :n:`@term__1`, these variables are bound to the +arguments of the constructor in :n:`@term__0`. For instance, the +definition .. coqtop:: reset all @@ -402,7 +415,7 @@ can be alternatively written Definition fst (A B:Set) (p:A * B) := let (x, _) := p in x. Notice that reduction is different from regular :g:`let … in …` -construction since it happens only if |term_0| is in constructor form. +construction since it happens only if :n:`@term__0` is in constructor form. Otherwise, the reduction is blocked. The pretty-printing of a definition by matching on a irrefutable @@ -582,29 +595,82 @@ This example emphasizes what the printing settings offer. Advanced recursive functions ---------------------------- -The following experimental command is available when the ``FunInd`` library has been loaded via ``Require Import FunInd``: +The following command is available when the ``FunInd`` library has been loaded via ``Require Import FunInd``: -.. cmd:: Function @ident {* @binder} { @fixannot } : @type := @term +.. cmd:: Function @fix_definition {* with @fix_definition } - 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 - objects*, namely: an induction principle that reflects the recursive + This command is a generalization of :cmd:`Fixpoint`. It is a wrapper + for several ways of defining a function *and* other useful related + objects, namely: an induction principle that reflects the recursive structure of the function (see :tacn:`function induction`) and its fixpoint equality. - The meaning of this declaration is to define a function ident, - similarly to ``Fixpoint``. Like in ``Fixpoint``, the decreasing argument must + This defines a function similar to those defined by :cmd:`Fixpoint`. + As in :cmd:`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:`{ @fixannot }` annotation - is to name the decreasing argument *and* to describe which kind of - decreasing criteria must be used to ensure termination of recursive + necessarily be *structurally* decreasing. Use the :n:`@fixannot` clause + to name the decreasing argument *and* to describe which kind of + decreasing criteria to use to ensure termination of recursive calls. -The ``Function`` construction also enjoys the ``with`` extension to define -mutually recursive definitions. However, this feature does not work -for non structurally recursive functions. - -See the documentation of functional induction (:tacn:`function induction`) -and ``Functional Scheme`` (:ref:`functional-scheme`) for how to use -the induction principle to easily reason about the function. + :cmd:`Function` also supports the :n:`with` clause to create + mutually recursive definitions, however this feature is limited + to structurally recursive functions (i.e. when :n:`@fixannot` is a :n:`struct` + clause). + + See :tacn:`function induction` and :cmd:`Functional Scheme` for how to use + the induction principle to reason easily about the function. + + The form of the :n:`@fixannot` clause determines which definition mechanism :cmd:`Function` uses. + (Note that references to :n:`ident` below refer to the name of the function being defined.): + + * If :n:`@fixannot` is not specified, :cmd:`Function` + defines the nonrecursive function :token:`ident` as if it was declared with + :cmd:`Definition`. In addition, the following are defined: + + + :token:`ident`\ ``_rect``, :token:`ident`\ ``_rec`` and :token:`ident`\ ``_ind``, + which reflect the pattern matching structure of :token:`term` (see :cmd:`Inductive`); + + The inductive :n:`R_@ident` corresponding to the graph of :token:`ident` (silently); + + :token:`ident`\ ``_complete`` and :token:`ident`\ ``_correct`` which + are inversion information linking the function and its graph. + + * If :n:`{ struct ... }` is specified, :cmd:`Function` + defines the structural recursive function :token:`ident` as if it was declared + with :cmd:`Fixpoint`. In addition, the following are defined: + + + The same objects as above; + + The fixpoint equation of :token:`ident`: :n:`@ident`\ ``_equation``. + + * If :n:`{ measure ... }` or :n:`{ wf ... }` are specified, :cmd:`Function` + defines a recursive function by well-founded recursion. The module ``Recdef`` + of the standard library must be loaded for this feature. + + + :n:`{measure @one_term__1 {? @ident } {? @one_term__2 } }`\: where :n:`@ident` is the decreasing argument + and :n:`@one_term__1` is a function from the type of :n:`@ident` to :g:`nat` for which + the decreasing argument decreases (for the :g:`lt` order on :g:`nat`) + for each recursive call of the function. The parameters of the function are + bound in :n:`@one_term__1`. + + :n:`{wf @one_term @ident }`\: where :n:`@ident` is the decreasing argument and + :n:`@one_term` is an ordering relation on the type of :n:`@ident` (i.e. of type + `T`\ :math:`_{\sf ident}` → `T`\ :math:`_{\sf ident}` → ``Prop``) for which the decreasing argument + decreases for each recursive call of the function. The order must be well-founded. + The parameters of the function are bound in :n:`@one_term`. + + If the clause is ``measure`` or ``wf``, the user is left with some proof + obligations that will be used to define the function. These proofs + are: proofs that each recursive call is actually decreasing with + respect to the given criteria, and (if the criteria is `wf`) a proof + that the ordering relation is well-founded. Once proof obligations are + discharged, the following objects are defined: + + + The same objects as with the ``struct`` clause; + + The lemma :n:`@ident`\ ``_tcc`` which collects all proof obligations in one + property; + + The lemmas :n:`@ident`\ ``_terminate`` and :n:`@ident`\ ``_F`` which will be inlined + during extraction of :n:`@ident`. + + The way this recursive function is defined is the subject of several + papers by Yves Bertot and Antonia Balaa on the one hand, and Gilles + Barthe, Julien Forest, David Pichardie, and Vlad Rusu on the other + hand. .. note:: @@ -644,7 +710,7 @@ the induction principle to easily reason about the function. :token:`term` must be built as a *pure pattern matching tree* (:g:`match … with`) with applications only *at the end* of each branch. -Function does not support partial application of the function being +:cmd:`Function` does not support partial application of the function being defined. Thus, the following example cannot be accepted due to the presence of partial application of :g:`wrong` in the body of :g:`wrong`: @@ -677,7 +743,7 @@ terminating functions. will not be generated. This error happens generally when: - the definition uses pattern matching on dependent types, - which ``Function`` cannot deal with yet. + which :cmd:`Function` cannot deal with yet. - the definition is not a *pattern matching tree* as explained above. .. warn:: Cannot define principle(s) for @ident. @@ -691,65 +757,6 @@ terminating functions. .. seealso:: :ref:`functional-scheme` and :tacn:`function induction` -Depending on the ``{…}`` annotation, different definition mechanisms are -used by ``Function``. A more precise description is given below. - -.. cmdv:: Function @ident {* @binder } : @type := @term - - Defines the not recursive function :token:`ident` as if declared with - :cmd:`Definition`. Moreover the following are defined: - - + :token:`ident`\ ``_rect``, :token:`ident`\ ``_rec`` and :token:`ident`\ ``_ind``, - which reflect the pattern matching structure of :token:`term` (see :cmd:`Inductive`); - + The inductive :n:`R_@ident` corresponding to the graph of :token:`ident` (silently); - + :token:`ident`\ ``_complete`` and :token:`ident`\ ``_correct`` which - are inversion information linking the function and its graph. - -.. cmdv:: Function @ident {* @binder } { struct @ident } : @type := @term - - Defines the structural recursive function :token:`ident` as if declared - with :cmd:`Fixpoint`. Moreover the following are defined: - - + The same objects as above; - + The fixpoint equation of :token:`ident`: :token:`ident`\ ``_equation``. - -.. cmdv:: Function @ident {* @binder } { measure @term @ident } : @type := @term - Function @ident {* @binder } { wf @term @ident } : @type := @term - - Defines a recursive function by well-founded recursion. The module ``Recdef`` - of the standard library must be loaded for this feature. The ``{}`` - annotation is mandatory and must be one of the following: - - + :n:`{measure @term @ident }` with :token:`ident` being the decreasing argument - and :token:`term` being a function from type of :token:`ident` to :g:`nat` for which - value on the decreasing argument decreases (for the :g:`lt` order on :g:`nat`) - at each recursive call of :token:`term`. Parameters of the function are - bound in :token:`term`; - + :n:`{wf @term @ident }` with :token:`ident` being the decreasing argument and - :token:`term` an ordering relation on the type of :token:`ident` (i.e. of type - `T`\ :math:`_{\sf ident}` → `T`\ :math:`_{\sf ident}` → ``Prop``) for which the decreasing argument - decreases at each recursive call of :token:`term`. The order must be well-founded. - Parameters of the function are bound in :token:`term`. - - If the annotation is ``measure`` or ``fw``, the user is left with some proof - obligations that will be used to define the function. These proofs - are: proofs that each recursive call is actually decreasing with - respect to the given criteria, and (if the criteria is `wf`) a proof - that the ordering relation is well-founded. Once proof obligations are - discharged, the following objects are defined: - - + The same objects as with the struct; - + The lemma `ident`\ :math:`_{\sf tcc}` which collects all proof obligations in one - property; - + The lemmas `ident`\ :math:`_{\sf terminate}` and `ident`\ :math:`_{\sf F}` which is needed to be inlined - during extraction of ident. - - The way this recursive function is defined is the subject of several - papers by Yves Bertot and Antonia Balaa on the one hand, and Gilles - Barthe, Julien Forest, David Pichardie, and Vlad Rusu on the other - hand. Remark: Proof obligations are presented as several subgoals - belonging to a Lemma `ident`\ :math:`_{\sf tcc}`. - .. _section-mechanism: Section mechanism @@ -804,69 +811,44 @@ Sections create local contexts which can be shared across multiple definitions. .. cmd:: End @ident - This command closes the section named :token:`ident`. After closing of the - section, the local declarations (variables and local definitions, see :cmd:`Variable`) get + This command closes the section or module named :token:`ident`. + See :ref:`Terminating an interactive module or module type definition<terminating_module>` + for a description of its use with modules. + + After closing the + section, the local declarations (variables and local definitions, see :cmd:`Variable`) are *discharged*, meaning that they stop being visible and that all global objects defined in the section are generalized with respect to the variables and local definitions they each depended on in the section. - .. exn:: This is not the last opened section. + .. exn:: There is nothing to end. :undocumented: + .. exn:: Last block to end has name @ident. + :undocumented: + .. note:: Most commands, like :cmd:`Hint`, :cmd:`Notation`, option management, … which appear inside a section are canceled when the section is closed. -.. cmd:: Variable @ident : @type - - This command links :token:`type` to the name :token:`ident` in the context of - the current section. When the current section is closed, name :token:`ident` - will be unknown and every object using this variable will be explicitly - parameterized (the variable is *discharged*). - - .. exn:: @ident already exists. - :name: @ident already exists. (Variable) - :undocumented: - - .. cmdv:: Variable {+ @ident } : @type - - Links :token:`type` to each :token:`ident`. +.. cmd:: Let @ident @def_body + Let Fixpoint @fix_definition {* with @fix_definition } + Let CoFixpoint @cofix_definition {* with @cofix_definition } + :name: Let; Let Fixpoint; Let CoFixpoint - .. cmdv:: Variable {+ ( {+ @ident } : @type ) } + These commands behave like :cmd:`Definition`, :cmd:`Fixpoint` and :cmd:`CoFixpoint`, except that + the declared constant is local to the current section. + When the section is closed, all persistent + definitions and theorems within it that depend on the constant + will be wrapped with a :n:`@term_let` with the same declaration. - Declare one or more variables with various types. + As for :cmd:`Definition`, :cmd:`Fixpoint` and :cmd:`CoFixpoint`, + if :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. + This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic. + In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant + for which the computational behavior is relevant. See :ref:`proof-editing-mode`. - .. cmdv:: Variables {+ ( {+ @ident } : @type) } - Hypothesis {+ ( {+ @ident } : @type) } - Hypotheses {+ ( {+ @ident } : @type) } - :name: Variables; Hypothesis; Hypotheses - - These variants are synonyms of :n:`Variable {+ ( {+ @ident } : @type) }`. - -.. cmd:: Let @ident := @term - - This command binds the value :token:`term` to the name :token:`ident` in the - environment of the current section. The name :token:`ident` is accessible - only within the current section. When the section is closed, all persistent - definitions and theorems within it and depending on :token:`ident` - will be prefixed by the let-in definition :n:`let @ident := @term in`. - - .. exn:: @ident already exists. - :name: @ident already exists. (Let) - :undocumented: - - .. cmdv:: Let @ident {? @binders } {? : @type } := @term - :undocumented: - - .. cmdv:: Let Fixpoint @ident @fix_body {* with @fix_body} - :name: Let Fixpoint - :undocumented: - - .. cmdv:: Let CoFixpoint @ident @fix_body {* with @fix_body} - :name: Let CoFixpoint - :undocumented: - -.. cmd:: Context @binders +.. cmd:: Context {+ @binder } Declare variables in the context of the current section, like :cmd:`Variable`, but also allowing implicit variables, :ref:`implicit-generalization`, and @@ -886,255 +868,297 @@ Module system The module system provides a way of packaging related elements together, as well as a means of massive abstraction. - .. productionlist:: modules - module_type : `qualid` - : `module_type` with Definition `qualid` := `term` - : `module_type` with Module `qualid` := `qualid` - : `qualid` `qualid` … `qualid` - : !`qualid` `qualid` … `qualid` - module_binding : ( [Import|Export] `ident` … `ident` : `module_type` ) - module_bindings : `module_binding` … `module_binding` - module_expression : `qualid` … `qualid` - : !`qualid` … `qualid` - Syntax of modules +.. cmd:: Module {? {| Import | Export } } @ident {* @module_binder } {? @of_module_type } {? := {+<+ @module_expr_inl } } -In the syntax of module application, the ! prefix indicates that any -`Inline` directive in the type of the functor arguments will be ignored -(see the :cmd:`Module Type` command below). + .. insertprodn module_binder module_expr_inl + .. prodn:: + module_binder ::= ( {? {| Import | Export } } {+ @ident } : @module_type_inl ) + module_type_inl ::= ! @module_type + | @module_type {? @functor_app_annot } + functor_app_annot ::= [ inline at level @num ] + | [ no inline ] + module_type ::= @qualid + | ( @module_type ) + | @module_type @module_expr_atom + | @module_type with @with_declaration + with_declaration ::= Definition @qualid {? @univ_decl } := @term + | Module @qualid := @qualid + module_expr_atom ::= @qualid + | ( {+ @module_expr_atom } ) + of_module_type ::= : @module_type_inl + | {* <: @module_type_inl } + module_expr_inl ::= ! {+ @module_expr_atom } + | {+ @module_expr_atom } {? @functor_app_annot } -.. cmd:: Module @ident + Defines a module named :token:`ident`. See the examples :ref:`here<module_examples>`. - This command is used to start an interactive module named :token:`ident`. + The :n:`Import` and :n:`Export` flags specify whether the module should be automatically + imported or exported. -.. cmdv:: Module @ident {* @module_binding} + Specifying :n:`{* @module_binder }` starts a functor with + parameters given by the :n:`@module_binder`\s. (A *functor* is a function + from modules to modules.) - Starts an interactive functor with - parameters given by module_bindings. + .. todo: would like to find a better term than "interactive", not very descriptive -.. cmdv:: Module @ident : @module_type + :n:`@of_module_type` specifies the module type. :n:`{+ <: @module_type_inl }` + starts a module that satisfies each :n:`@module_type_inl`. - Starts an interactive module specifying its module type. + :n:`:= {+<+ @module_expr_inl }` specifies the body of a module or functor + definition. If it's not specified, then the module is defined *interactively*, + meaning that the module is defined as a series of commands terminated with :cmd:`End` + instead of in a single :cmd:`Module` command. + Interactively defining the :n:`@module_expr_inl`\s in a series of + :cmd:`Include` commands is equivalent to giving them all in a single + non-interactive :cmd:`Module` command. -.. cmdv:: Module @ident {* @module_binding} : @module_type + The ! prefix indicates that any assumption command (such as :cmd:`Axiom`) with an :n:`Inline` clause + in the type of the functor arguments will be ignored. - Starts an interactive functor with parameters given by the list of - :token:`module_bindings`, and output module type :token:`module_type`. + .. todo: What is an Inline directive? sb command but still unclear. Maybe referring to the + "inline" in functor_app_annot? or assumption_token Inline assum_list? -.. cmdv:: Module @ident <: {+<: @module_type } +.. cmd:: Module Type @ident {* @module_binder } {* <: @module_type_inl } {? := {+<+ @module_type_inl } } - Starts an interactive module satisfying each :token:`module_type`. + Defines a module type named :n:`@ident`. See the example :ref:`here<example_def_simple_module_type>`. - .. cmdv:: Module @ident {* @module_binding} <: {+<: @module_type }. + Specifying :n:`{* @module_binder }` starts a functor type with + parameters given by the :n:`@module_binder`\s. - Starts an interactive functor with parameters given by the list of - :token:`module_binding`. The output module type - is verified against each :token:`module_type`. + :n:`:= {+<+ @module_type_inl }` specifies the body of a module or functor type + definition. If it's not specified, then the module type is defined *interactively*, + meaning that the module type is defined as a series of commands terminated with :cmd:`End` + instead of in a single :cmd:`Module Type` command. + Interactively defining the :n:`@module_type_inl`\s in a series of + :cmd:`Include` commands is equivalent to giving them all in a single + non-interactive :cmd:`Module Type` command. -.. cmdv:: Module {| Import | Export } +.. _terminating_module: - Behaves like :cmd:`Module`, but automatically imports or exports the module. +**Terminating an interactive module or module type definition** -Reserved commands inside an interactive module -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Interactive modules are terminated with the :cmd:`End` command, which +is also used to terminate :ref:`Sections<section-mechanism>`. +:n:`End @ident` closes the interactive module or module type :token:`ident`. +If the module type was given, the command verifies that the content of the module +matches the module type. If the module is not a +functor, its components (constants, inductive types, submodules etc.) +are now available through the dot notation. -.. cmd:: Include @module +.. exn:: No such label @ident. + :undocumented: - Includes the content of module in the current - interactive module. Here module can be a module expression or a module - type expression. If module is a high-order module or module type - expression then the system tries to instantiate module by the current - interactive module. +.. exn:: Signature components for label @ident do not match. + :undocumented: -.. cmd:: Include {+<+ @module} +.. exn:: The field @ident is missing in @qualid. + :undocumented: - is a shortcut for the commands :n:`Include @module` for each :token:`module`. +.. |br| raw:: html -.. cmd:: End @ident + <br> - This command closes the interactive module :token:`ident`. If the module type - was given the content of the module is matched against it and an error - is signaled if the matching fails. If the module is basic (is not a - functor) its components (constants, inductive types, submodules etc.) - are now available through the dot notation. +.. note:: - .. exn:: No such label @ident. - :undocumented: + #. Interactive modules and module types can be nested. + #. Interactive modules and module types can't be defined inside of :ref:`sections<section-mechanism>`. + Sections can be defined inside of interactive modules and module types. + #. Hints and notations (:cmd:`Hint` and :cmd:`Notation` commands) can also appear inside interactive + modules and module types. Note that with module definitions like: - .. exn:: Signature components for label @ident do not match. - :undocumented: + :n:`Module @ident__1 : @module_type := @ident__2.` - .. exn:: This is not the last opened module. - :undocumented: + or -.. cmd:: Module @ident := @module_expression + :n:`Module @ident__1 : @module_type.` |br| + :n:`Include @ident__2.` |br| + :n:`End @ident__1.` - This command defines the module identifier :token:`ident` to be equal - to :token:`module_expression`. + hints and the like valid for :n:`@ident__1` are the ones defined in :n:`@module_type` + rather then those defined in :n:`@ident__2` (or the module body). + #. Within an interactive module type definition, the :cmd:`Parameter` command declares a + constant instead of definining a new axiom (which it does when not in a module type definition). + #. Assumptions such as :cmd:`Axiom` that include the :n:`Inline` clause will be automatically + expanded when the functor is applied, except when the function application is prefixed by ``!``. - .. cmdv:: Module @ident {* @module_binding} := @module_expression +.. cmd:: Include @module_type_inl {* <+ @module_expr_inl } - Defines a functor with parameters given by the list of :token:`module_binding` and body :token:`module_expression`. + Includes the content of module(s) in the current + interactive module. Here :n:`@module_type_inl` can be a module expression or a module + type expression. If it is a high-order module or module type + expression then the system tries to instantiate :n:`@module_type_inl` with the current + interactive module. - .. cmdv:: Module @ident {* @module_binding} : @module_type := @module_expression + Including multiple modules is a single :cmd:`Include` is equivalent to including each module + in a separate :cmd:`Include` command. - Defines a functor with parameters given by the list of :token:`module_binding` (possibly none), and output module type :token:`module_type`, - with body :token:`module_expression`. +.. cmd:: Include Type {+<+ @module_type_inl } - .. cmdv:: Module @ident {* @module_binding} <: {+<: @module_type} := @module_expression + .. deprecated:: 8.3 - Defines a functor with parameters given by module_bindings (possibly none) with body :token:`module_expression`. - The body is checked against each :n:`@module_type__i`. + Use :cmd:`Include` instead. - .. cmdv:: Module @ident {* @module_binding} := {+<+ @module_expression} +.. cmd:: Declare Module {? {| Import | Export } } @ident {* @module_binder } : @module_type_inl - is equivalent to an interactive module where each :token:`module_expression` is included. + Declares a module :token:`ident` of type :token:`module_type_inl`. -.. cmd:: Module Type @ident + If :n:`@module_binder`\s are specified, declares a functor with parameters given by the list of + :token:`module_binder`\s. - This command is used to start an interactive module type :token:`ident`. +.. cmd:: Import {+ @qualid } - .. cmdv:: Module Type @ident {* @module_binding} + If :token:`qualid` denotes a valid basic module (i.e. its module type is a + signature), makes its components available by their short names. - Starts an interactive functor type with parameters given by :token:`module_bindings`. + .. example:: + .. coqtop:: reset in -Reserved commands inside an interactive module type: -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + Module Mod. + Definition T:=nat. + Check T. + End Mod. + Check Mod.T. -.. cmd:: Include @module + .. coqtop:: all - Same as ``Include`` inside a module. + Fail Check T. + Import Mod. + Check T. -.. cmd:: Include {+<+ @module} + Some features defined in modules are activated only when a module is + imported. This is for instance the case of notations (see :ref:`Notations`). - This is a shortcut for the command :n:`Include @module` for each :token:`module`. + Declarations made with the :attr:`local` attribute are never imported by the :cmd:`Import` + command. Such declarations are only accessible through their fully + qualified name. -.. cmd:: @assumption_keyword Inline @assums - :name: Inline + .. example:: - The instance of this assumption will be automatically expanded at functor application, except when - this functor application is prefixed by a ``!`` annotation. + .. coqtop:: in -.. cmd:: End @ident + Module A. + Module B. + Local Definition T := nat. + End B. + End A. + Import A. - This command closes the interactive module type :token:`ident`. + .. coqtop:: all fail - .. exn:: This is not the last opened module type. - :undocumented: + Check B.T. -.. cmd:: Module Type @ident := @module_type +.. cmd:: Export {+ @qualid } + :name: Export - Defines a module type :token:`ident` equal to :token:`module_type`. + Similar to :cmd:`Import`, except that when the module containing this command + is imported, the :n:`{+ @qualid }` are imported as well. - .. cmdv:: Module Type @ident {* @module_binding} := @module_type + .. exn:: @qualid is not a module. + :undocumented: - Defines a functor type :token:`ident` specifying functors taking arguments :token:`module_bindings` and - returning :token:`module_type`. + .. warn:: Trying to mask the absolute name @qualid! + :undocumented: - .. cmdv:: Module Type @ident {* @module_binding} := {+<+ @module_type } +.. cmd:: Print Module @qualid - is equivalent to an interactive module type were each :token:`module_type` is included. + Prints the module type and (optionally) the body of the module :n:`@qualid`. -.. cmd:: Declare Module @ident : @module_type +.. cmd:: Print Module Type @qualid - Declares a module :token:`ident` of type :token:`module_type`. + Prints the module type corresponding to :n:`@qualid`. - .. cmdv:: Declare Module @ident {* @module_binding} : @module_type +.. flag:: Short Module Printing - Declares a functor with parameters given by the list of :token:`module_binding` and output module type - :token:`module_type`. + 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`. -.. example:: +.. _module_examples: - Let us define a simple module. +Examples +~~~~~~~~ - .. coqtop:: all +.. example:: Defining a simple module interactively - Module M. + .. coqtop:: in + Module M. Definition T := nat. - Definition x := 0. - Definition y : bool. + .. coqtop:: all + Definition y : bool. exact true. - Defined. + .. coqtop:: in + Defined. End M. -Inside a module one can define constants, prove theorems and do any -other things that can be done in the toplevel. Components of a closed +Inside a module one can define constants, prove theorems and do anything +else that can be done in the toplevel. Components of a closed module can be accessed using the dot notation: .. coqtop:: all Print M.x. -A simple module type: - -.. coqtop:: all - - Module Type SIG. - - Parameter T : Set. - - Parameter x : T. - - End SIG. - -Now we can create a new module from M, giving it a less precise -specification: the y component is dropped as well as the body of x. +.. _example_def_simple_module_type: -.. coqtop:: all - - Module N : SIG with Definition T := nat := M. - - Print N.T. - - Print N.x. - - Fail Print N.y. +.. example:: Defining a simple module type interactively -.. reset to remove N (undo in last coqtop block doesn't seem to do that), invisibly redefine M, SIG -.. coqtop:: none reset - - Module M. - - Definition T := nat. + .. coqtop:: in - Definition x := 0. + Module Type SIG. + Parameter T : Set. + Parameter x : T. + End SIG. - Definition y : bool. +.. _example_filter_module: - exact true. +.. example:: Creating a new module that omits some items from an existing module - Defined. + Since :n:`SIG`, the type of the new module :n:`N`, doesn't define :n:`y` or + give the body of :n:`x`, which are not included in :n:`N`. - End M. + .. coqtop:: all - Module Type SIG. + Module N : SIG with Definition T := nat := M. + Print N.T. + Print N.x. + Fail Print N.y. - Parameter T : Set. + .. reset to remove N (undo in last coqtop block doesn't seem to do that), invisibly redefine M, SIG + .. coqtop:: none reset - Parameter x : T. + Module M. + Definition T := nat. + Definition x := 0. + Definition y : bool. + exact true. + Defined. + End M. - End SIG. + Module Type SIG. + Parameter T : Set. + Parameter x : T. + End SIG. -The definition of :g:`N` using the module type expression :g:`SIG` with +The following definition of :g:`N` using the module type expression :g:`SIG` with :g:`Definition T := nat` is equivalent to the following one: -.. coqtop:: all +.. todo: what is other definition referred to above? + "Module N' : SIG with Definition T := nat. End N`." is not it. - Module Type SIG'. +.. coqtop:: in + Module Type SIG'. Definition T : Set := nat. - Parameter x : T. - End SIG'. Module N : SIG' := M. @@ -1143,165 +1167,58 @@ If we just want to be sure that our implementation satisfies a given module type without restricting the interface, we can use a transparent constraint -.. coqtop:: all +.. coqtop:: in Module P <: SIG := M. - Print P.y. - -Now let us create a functor, i.e. a parametric module - .. coqtop:: all - Module Two (X Y: SIG). - - Definition T := (X.T * Y.T)%type. - - Definition x := (X.x, Y.x). - - End Two. - -and apply it to our modules and do some computations: - -.. coqtop:: all - - Module Q := Two M N. - - Eval compute in (fst Q.x + snd Q.x). - -In the end, let us define a module type with two sub-modules, sharing -some of the fields and give one of its possible implementations: - -.. coqtop:: all + Print P.y. - Module Type SIG2. +.. example:: Creating a functor (a module with parameters) - Declare Module M1 : SIG. + .. coqtop:: in - Module M2 <: SIG. + Module Two (X Y: SIG). + Definition T := (X.T * Y.T)%type. + Definition x := (X.x, Y.x). + End Two. - Definition T := M1.T. + and apply it to our modules and do some computations: - Parameter x : T. + .. coqtop:: in - End M2. - End SIG2. + Module Q := Two M N. - Module Mod <: SIG2. + .. coqtop:: all - Module M1. + Eval compute in (fst Q.x + snd Q.x). - Definition T := nat. +.. example:: A module type with two sub-modules, sharing some fields - Definition x := 1. + .. coqtop:: in - End M1. + Module Type SIG2. + Declare Module M1 : SIG. + Module M2 <: SIG. + Definition T := M1.T. + Parameter x : T. + End M2. + End SIG2. - Module M2 := M. + .. coqtop:: in - End Mod. + Module Mod <: SIG2. + Module M1. + Definition T := nat. + Definition x := 1. + End M1. + Module M2 := M. + End Mod. Notice that ``M`` is a correct body for the component ``M2`` since its ``T`` -component is equal ``nat`` and hence ``M1.T`` as specified. - -.. note:: - - #. Modules and module types can be nested components of each other. - #. One can have sections inside a module or a module type, but not a - module or a module type inside a section. - #. Commands like :cmd:`Hint` or :cmd:`Notation` can also appear inside modules and - module types. Note that in case of a module definition like: - - :: - - Module N : SIG := M. - - or:: - - Module N : SIG. … End N. - - hints and the like valid for ``N`` are not those defined in ``M`` - (or the module body) but the ones defined in ``SIG``. - - -.. _import_qualid: - -.. cmd:: Import @qualid - - If :token:`qualid` denotes a valid basic module (i.e. its module type is a - signature), makes its components available by their short names. - - .. example:: - - .. coqtop:: reset all - - Module Mod. - - Definition T:=nat. - - Check T. - - End Mod. - - Check Mod.T. - - Fail Check T. - - Import Mod. - - Check T. - - Some features defined in modules are activated only when a module is - imported. This is for instance the case of notations (see :ref:`Notations`). - - Declarations made with the ``Local`` flag are never imported by the :cmd:`Import` - command. Such declarations are only accessible through their fully - qualified name. - - .. example:: - - .. coqtop:: all - - Module A. - - Module B. - - Local Definition T := nat. - - End B. - - End A. - - Import A. - - Fail Check B.T. - - .. cmdv:: Export @qualid - :name: Export - - When the module containing the command ``Export`` qualid - is imported, qualid is imported as well. - - .. exn:: @qualid is not a module. - :undocumented: - - .. warn:: Trying to mask the absolute name @qualid! - :undocumented: - -.. cmd:: Print Module @ident - - Prints the module type and (optionally) the body of the module :token:`ident`. - -.. cmd:: Print Module Type @ident - - Prints the module type corresponding to :token:`ident`. - -.. flag:: Short Module Printing - - 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`. +component is ``nat`` as specified for ``M1.T``. Libraries and qualified names --------------------------------- @@ -1364,7 +1281,7 @@ also each time a new declaration is added to the context. An absolute name is called visible from a given short or partially qualified name when this latter name is enough to denote it. This means that the short or partially qualified name is mapped to the absolute name in -|Coq| name table. Definitions flagged as Local are only accessible with +|Coq| name table. Definitions with the :attr:`local` attribute are only accessible with their fully qualified name (see :ref:`gallina-definitions`). It may happen that a visible name is hidden by the short name or a @@ -1431,7 +1348,7 @@ with the same physical-to-logical translation and with an empty logical prefix. The command line option ``-R`` is a variant of ``-Q`` which has the strictly same behavior regarding loadpaths, but which also makes the corresponding ``.vo`` files available through their short names in a way -not unlike the ``Import`` command (see :ref:`here <import_qualid>`). For instance, ``-R path Lib`` +similar to the :cmd:`Import` command. For instance, ``-R path Lib`` associates to the file ``/path/fOO/Bar/File.vo`` the logical name ``Lib.fOO.Bar.File``, but allows this file to be accessed through the short names ``fOO.Bar.File,Bar.File`` and ``File``. If several files with @@ -1570,11 +1487,26 @@ inserted. In the second case, the function is considered to be implicitly applied to the implicit arguments it is waiting for: one 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` flag. +Each implicit argument can be declared to be inserted maximally or non +maximally. In Coq, maximally-inserted implicit arguments are written between curly braces +"{ }" and non-maximally-inserted implicit arguments are written in square brackets "[ ]". + +.. seealso:: :flag:`Maximal Implicit Insertion` + +Trailing Implicit Arguments ++++++++++++++++++++++++++++ -.. seealso:: :ref:`displaying-implicit-args`. +An implicit argument is considered trailing when all following arguments are declared +implicit. Trailing implicit arguments cannot be declared non maximally inserted, +otherwise they would never be inserted. + +.. exn:: Argument @name is a trailing implicit, so it can't be declared non maximal. Please use %{ %} instead of [ ]. + + For instance: + + .. coqtop:: all fail + + Fail Definition double [n] := n + n. Casual use of implicit arguments @@ -1605,10 +1537,16 @@ this, *a priori* and *a posteriori*. Implicit Argument Binders +++++++++++++++++++++++++ +.. insertprodn implicit_binders implicit_binders + +.. prodn:: + implicit_binders ::= %{ {+ @name } {? : @type } %} + | [ {+ @name } {? : @type } ] + In the first setting, one wants to explicitly give the implicit arguments of a declared object as part of its definition. To do this, one has to surround the bindings of implicit arguments by curly -braces: +braces or square braces: .. coqtop:: all @@ -1624,13 +1562,24 @@ absent in every situation but still be able to specify it if needed: Goal forall A, compose id id = id (A:=A). +For non maximally inserted implicit arguments, use square brackets: + +.. coqtop:: all + + Fixpoint map [A B : Type] (f : A -> B) (l : list A) : list B := + match l with + | nil => nil + | cons a t => cons (f a) (map f t) + end. + + Print Implicit map. The syntax is supported in all top-level definitions: :cmd:`Definition`, :cmd:`Fixpoint`, :cmd:`Lemma` and so on. For (co-)inductive datatype declarations, the semantics are the following: an inductive parameter declared as an implicit argument need not be repeated in the inductive -definition but will become implicit for the constructors of the -inductive only, not the inductive type itself. For example: +definition and will become implicit for the inductive type and the constructors. +For example: .. coqtop:: all @@ -1643,54 +1592,123 @@ inductive only, not the inductive type itself. For example: One can always specify the parameter if it is not uniform using the usual implicit arguments disambiguation syntax. +The syntax is also supported in internal binders. For instance, in the +following kinds of expressions, the type of each declaration present +in :token:`binders` can be bracketed to mark the declaration as +implicit: +:n:`fun (@ident:forall {* @binder }, @type) => @term`, +:n:`forall (@ident:forall {* @binder }, @type), @type`, +:n:`let @ident {* @binder } := @term in @term`, +:n:`fix @ident {* @binder } := @term in @term` and +:n:`cofix @ident {* @binder } := @term in @term`. +Here is an example: -Declaring Implicit Arguments -++++++++++++++++++++++++++++ +.. coqtop:: all + Axiom Ax : + forall (f:forall {A} (a:A), A * A), + let g {A} (x y:A) := (x,y) in + f 0 = g 0 0. +.. warn:: Ignoring implicit binder declaration in unexpected position -.. cmd:: Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } } - :name: Arguments (implicits) + This is triggered when setting an argument implicit in an + expression which does not correspond to the type of an assumption + or to the body of a definition. Here is an example: - This command is used to set implicit arguments *a posteriori*, - where the list of possibly bracketed :token:`ident` is a prefix of the list of - arguments of :token:`qualid` where the ones to be declared implicit are - surrounded by square brackets and the ones to be declared as maximally - inserted implicits are surrounded by curly braces. + .. coqtop:: all warn - After the above declaration is issued, implicit arguments can just - (and have to) be skipped in any expression involving an application - of :token:`qualid`. + Definition f := forall {y}, y = 0. -.. cmd:: Arguments @qualid : clear implicits - :name: Arguments (clear implicits) +.. warn:: Making shadowed name of implicit argument accessible by position - This command clears implicit arguments. + This is triggered when two variables of same name are set implicit + in the same block of binders, in which case the first occurrence is + considered to be unnamed. Here is an example: -.. cmdv:: Global Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } } + .. coqtop:: all warn - This command is used to recompute the implicit arguments of - :token:`qualid` after ending of the current section if any, enforcing the - implicit arguments known from inside the section to be the ones - declared by the command. + Check let g {x:nat} (H:x=x) {x} (H:x=x) := x in 0. -.. cmdv:: Local Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } } - When in a module, tell not to activate the - implicit arguments of :token:`qualid` declared by this command to contexts that - require the module. +Declaring Implicit Arguments +++++++++++++++++++++++++++++ -.. cmdv:: {? {| Global | Local } } Arguments @qualid {*, {+ {| [ @ident ] | { @ident } | @ident } } } - For names of constants, inductive types, - constructors, lemmas which can only be applied to a fixed number of - arguments (this excludes for instance constants whose type is - polymorphic), multiple implicit arguments declarations can be given. - Depending on the number of arguments qualid is applied to in practice, - the longest applicable list of implicit arguments is used to select - which implicit arguments are inserted. For printing, the omitted - arguments are the ones of the longest list of implicit arguments of - the sequence. + +.. cmd:: Arguments @smart_qualid {* @argument_spec_block } {* , {* @more_implicits_block } } {? : {+, @arguments_modifier } } + :name: Arguments + + .. insertprodn smart_qualid arguments_modifier + + .. prodn:: + smart_qualid ::= @qualid + | @by_notation + by_notation ::= @string {? % @ident } + argument_spec_block ::= @argument_spec + | / + | & + | ( {+ @argument_spec } ) {? % @ident } + | [ {+ @argument_spec } ] {? % @ident } + | %{ {+ @argument_spec } %} {? % @ident } + argument_spec ::= {? ! } @name {? % @ident } + more_implicits_block ::= @name + | [ {+ @name } ] + | %{ {+ @name } %} + arguments_modifier ::= simpl nomatch + | simpl never + | default implicits + | clear bidirectionality hint + | clear implicits + | clear scopes + | clear scopes and implicits + | clear implicits and scopes + | rename + | assert + | extra scopes + + This command sets implicit arguments *a posteriori*, + where the list of :n:`@name`\s is a prefix of the list of + arguments of :n:`@smart_qualid`. Arguments in square + brackets are declared as implicit and arguments in curly brackets are declared as + maximally inserted. + + After the command is issued, implicit arguments can and must be + omitted in any expression that applies :token:`qualid`. + + This command supports the :attr:`local` and :attr:`global` attributes. + Default behavior is to limit the effect to the current section but also to + extend their effect outside the current module or library file. + Applying :attr:`local` limits the effect of the command to the current module if + it's not in a section. Applying :attr:`global` within a section extends the + effect outside the current sections and current module if the command occurs. + + A command containing :n:`@argument_spec_block & @argument_spec_block` + provides :ref:`bidirectionality_hints`. + + Use the :n:`@more_implicits_block` to specify multiple implicit arguments declarations + for names of constants, inductive types, constructors and lemmas that can only be + applied to a fixed number of arguments (excluding, for instance, + constants whose type is polymorphic). + The longest applicable list of implicit arguments will be used to select which + implicit arguments are inserted. + For printing, the omitted arguments are the ones of the longest list of implicit + arguments of the sequence. See the example :ref:`here<example_more_implicits>`. + + The :n:`@arguments_modifier` values have various effects: + + * :n:`clear implicits` - clears implicit arguments + * :n:`default implicits` - automatically determine the implicit arguments of the object. + See :ref:`auto_decl_implicit_args`. + * :n:`rename` - rename implicit arguments for the object + * :n:`assert` - assert that the object has the expected number of arguments with the + expected names. See the example here: :ref:`renaming_implicit_arguments`. + +.. exn:: The / modifier may only occur once. + :undocumented: + +.. exn:: The & modifier may only occur once. + :undocumented: .. example:: @@ -1720,48 +1738,34 @@ Declaring Implicit Arguments Check (fun l:list (list nat) => map length l). - Arguments map [A B] f l, [A] B f l, A B f l. +.. _example_more_implicits: - Check (fun l => map length l = map (list nat) nat length l). +.. example:: Multiple implicit arguments with :n:`@more_implicits_block` -.. note:: - To know which are the implicit arguments of an object, use the - command :cmd:`Print Implicit` (see :ref:`displaying-implicit-args`). + .. coqtop:: all -.. warn:: Argument number @num is a trailing implicit so must be maximal. + Arguments map [A B] f l, [A] B f l, A B f l. - For instance in + Check (fun l => map length l = map (list nat) nat length l). - .. coqtop:: all warn +.. note:: + Use the :cmd:`Print Implicit` command to see the implicit arguments + of an object (see :ref:`displaying-implicit-args`). - Arguments prod _ [_]. +.. _auto_decl_implicit_args: Automatic declaration of implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: Arguments @qualid : default implicits - :name: Arguments (default implicits) - - This command tells |Coq| to automatically detect what are the implicit arguments of a - defined object. + The :n:`default implicits @arguments_modifier` clause tells |Coq| to automatically determine the + implicit arguments of the object. - The auto-detection is governed by flags telling if strict, + Auto-detection is governed by flags specifying whether 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`). - - .. cmdv:: Global Arguments @qualid : default implicits - - Tell to recompute the - implicit arguments of qualid after ending of the current section if - any. + considered or not (see :ref:`controlling-strict-implicit-args`, :ref:`controlling-contextual-implicit-args`, + :ref:`controlling-rev-pattern-implicit-args` and also :ref:`controlling-insertion-implicit-args`). - .. cmdv:: Local Arguments @qualid : default implicits - - When in a module, tell not to activate the implicit arguments of :token:`qualid` computed by this - declaration to contexts that requires the module. - -.. example:: +.. example:: Default implicits .. coqtop:: reset all @@ -1811,7 +1815,7 @@ appear strictly in the body of the type, they are implicit. Mode for automatic declaration of implicit arguments -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +++++++++++++++++++++++++++++++++++++++++++++++++++++ .. flag:: Implicit Arguments @@ -1823,7 +1827,7 @@ Mode for automatic declaration of implicit arguments .. _controlling-strict-implicit-args: Controlling strict implicit arguments -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ++++++++++++++++++++++++++++++++++++++ .. flag:: Strict Implicit @@ -1842,7 +1846,7 @@ Controlling strict implicit arguments .. _controlling-contextual-implicit-args: Controlling contextual implicit arguments -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ++++++++++++++++++++++++++++++++++++++++++ .. flag:: Contextual Implicit @@ -1853,7 +1857,7 @@ Controlling contextual implicit arguments .. _controlling-rev-pattern-implicit-args: Controlling reversible-pattern implicit arguments -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ++++++++++++++++++++++++++++++++++++++++++++++++++ .. flag:: Reversible Pattern Implicit @@ -1864,7 +1868,7 @@ Controlling reversible-pattern implicit arguments .. _controlling-insertion-implicit-args: Controlling the insertion of implicit arguments not followed by explicit arguments -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ .. flag:: Maximal Implicit Insertion @@ -1873,32 +1877,43 @@ Controlling the insertion of implicit arguments not followed by explicit argumen function is partially applied and the next argument of the function is an implicit one. +Combining manual declaration and automatic declaration +++++++++++++++++++++++++++++++++++++++++++++++++++++++ + +When some arguments are manually specified implicit with binders in a definition +and the automatic declaration mode in on, the manual implicit arguments are added to the +automatically declared ones. + +In that case, and when the flag :flag:`Maximal Implicit Insertion` is set to off, +some trailing implicit arguments can be inferred to be non maximally inserted. In +this case, they are converted to maximally inserted ones. + +.. example:: + + .. coqtop:: all + + Set Implicit Arguments. + Axiom eq0_le0 : forall (n : nat) (x : n = 0), n <= 0. + Print Implicit eq0_le0. + Axiom eq0_le0' : forall (n : nat) {x : n = 0}, n <= 0. + Print Implicit eq0_le0'. + + .. _explicit-applications: Explicit applications ~~~~~~~~~~~~~~~~~~~~~ -In presence of non-strict or contextual argument, or in presence of +In presence of non-strict or contextual arguments, or in presence of partial applications, the synthesis of implicit arguments may fail, so -one may have to give explicitly certain implicit arguments of an -application. The syntax for this is :n:`(@ident := @term)` where :token:`ident` is the -name of the implicit argument and term is its corresponding explicit -term. Alternatively, one can locally deactivate the hiding of implicit -arguments of a function by using the notation :n:`@qualid {+ @term }`. -This syntax extension is given in the following grammar: - -.. _explicit_app_grammar: - - .. productionlist:: explicit_apps - term : @ `qualid` `term` … `term` - : @ `qualid` - : `qualid` `argument` … `argument` - argument : `term` - : (`ident` := `term`) - - Syntax for explicitly giving implicit arguments +one may have to explicitly give certain implicit arguments of an +application. Use the :n:`(@ident := @term)` form of :token:`arg` to do so, +where :token:`ident` is the name of the implicit argument and :token:`term` +is its corresponding explicit term. Alternatively, one can deactivate +the hiding of implicit arguments for a single function application using the +:n:`@ @qualid {? @univ_annot } {* @term1 }` form of :token:`term10`. -.. example:: (continued) +.. example:: Syntax for explicitly giving implicit arguments (continued) .. coqtop:: all @@ -1907,21 +1922,12 @@ This syntax extension is given in the following grammar: Check (p (x:=a) (y:=b) r1 (z:=c) r2). +.. _renaming_implicit_arguments: + Renaming implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: Arguments @qualid {* @name} : rename - :name: Arguments (rename) - - This command is used to redefine the names of implicit arguments. - -.. 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) +.. example:: (continued) Renaming implicit arguments .. coqtop:: all @@ -1935,27 +1941,27 @@ Renaming implicit arguments .. _displaying-implicit-args: -Displaying what the implicit arguments are -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Displaying implicit arguments +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: Print Implicit @qualid +.. cmd:: Print Implicit @smart_qualid - Use this command to display the implicit arguments associated to an object, - and to know if each of them is to be used maximally or not. + Displays the implicit arguments associated with an object, + identifying which arguments are applied maximally or not. -Explicit displaying of implicit arguments for pretty-printing -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Displaying implicit arguments when pretty-printing +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. flag:: Printing Implicit - By default, the basic pretty-printing rules hide the inferable implicit + By default, the basic pretty-printing rules hide the inferrable implicit arguments of an application. Turn this flag on to force printing all implicit arguments. .. flag:: Printing Implicit Defensive - By default, the basic pretty-printing rules display the implicit + By default, the basic pretty-printing rules display 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 flag off. @@ -1994,6 +2000,8 @@ Deactivation of implicit arguments for parsing to be given as if no arguments were implicit. By symmetry, this also affects printing. +.. _canonical-structure-declaration: + Canonical structures ~~~~~~~~~~~~~~~~~~~~ @@ -2003,11 +2011,19 @@ 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:: {? Local | #[local] } Canonical {? Structure } @qualid +.. cmd:: Canonical {? Structure } @smart_qualid + Canonical {? Structure } @ident_decl @def_body + :name: Canonical Structure; _ + + The first form of this command declares an existing :n:`@smart_qualid` as a + canonical instance of a structure (a record). + + The second form defines a new constant as if the :cmd:`Definition` command + had been used, then declares it as a canonical instance as if the first + form had been used on the defined object. - This command declares :token:`qualid` as a canonical instance of a - structure (a record). When the :g:`#[local]` attribute is given the effect - stops at the end of the :g:`Section` containig it. + This command supports the :attr:`local` attribute. When used, the + structure is canonical only within the :cmd:`Section` containing 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|. @@ -2055,9 +2071,12 @@ in :ref:`canonicalstructures`; here only a simple example is given. If a same field occurs in several canonical structures, then only the structure declared first as canonical is considered. - .. note:: - To prevent a field from being involved in the inference of canonical instances, - its declaration can be annotated with the :g:`#[canonical(false)]` attribute. + .. attr:: canonical(false) + + To prevent a field from being involved in the inference of + canonical instances, its declaration can be annotated with the + :attr:`canonical(false)` attribute (cf. the syntax of + :n:`@record_field`). .. example:: @@ -2070,16 +2089,19 @@ in :ref:`canonicalstructures`; here only a simple example is given. See :ref:`canonicalstructures` for a more realistic example. - .. cmdv:: {? Local | #[local] } Canonical {? Structure } @ident {? : @type } := @term +.. attr:: canonical - This is equivalent to a regular definition of :token:`ident` followed by the - declaration :n:`Canonical @ident`. + This attribute can decorate a :cmd:`Definition` or :cmd:`Let` command. + It is equivalent to having a :cmd:`Canonical Structure` declaration just + after the command. -.. cmd:: Print Canonical Projections +.. cmd:: Print Canonical Projections {* @smart_qualid } 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:: @@ -2089,10 +2111,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 ~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2101,13 +2128,21 @@ It is possible to bind variable names to a given type (e.g. in a development using arithmetic, it may be convenient to bind the names :g:`n` or :g:`m` to the type :g:`nat` of natural numbers). -.. cmd:: Implicit Types {+ @ident } : @type +.. cmd:: Implicit {| Type | Types } @reserv_list + :name: Implicit Type; Implicit Types + + .. insertprodn reserv_list simple_reserv + + .. prodn:: + reserv_list ::= {+ ( @simple_reserv ) } + | @simple_reserv + simple_reserv ::= {+ @ident } : @type - The effect of the command is to automatically set the type of bound + Sets the type of bound variables starting with :token:`ident` (either :token:`ident` itself or :token:`ident` followed by one or more single quotes, underscore or - digits) to be :token:`type` (unless the bound variable is already declared - with an explicit type in which case, this latter type is considered). + digits) to :token:`type` (unless the bound variable is already declared + with an explicit type, in which case, that type will be used). .. example:: @@ -2123,13 +2158,12 @@ or :g:`m` to the type :g:`nat` of natural numbers). Lemma cons_inj_bool : forall (m n:bool) l, n :: l = m :: l -> n = m. Abort. -.. cmdv:: Implicit Type @ident : @type - - This is useful for declaring the implicit type of a single variable. - -.. cmdv:: Implicit Types {+ ( {+ @ident } : @type ) } +.. flag:: Printing Use Implicit Types - Adds blocks of implicit types with different specifications. + By default, the type of bound variables is not printed when + the variable name is associated to an implicit type which matches the + actual type of the variable. This feature can be deactivated by + turning this flag off. .. _implicit-generalization: @@ -2137,20 +2171,35 @@ Implicit generalization ~~~~~~~~~~~~~~~~~~~~~~~ .. index:: `{ } +.. index:: `[ ] .. index:: `( ) .. index:: `{! } +.. index:: `[! ] .. index:: `(! ) +.. insertprodn generalizing_binder typeclass_constraint + +.. prodn:: + generalizing_binder ::= `( {+, @typeclass_constraint } ) + | `%{ {+, @typeclass_constraint } %} + | `[ {+, @typeclass_constraint } ] + typeclass_constraint ::= {? ! } @term + | %{ @name %} : {? ! } @term + | @name : {? ! } @term + + Implicit generalization is an automatic elaboration of a statement with free variables into a closed statement where these variables are -quantified explicitly. +quantified explicitly. Use the :cmd:`Generalizable` command to designate +which variables should be generalized. It is activated for a binder by prefixing a \`, and for terms by -surrounding it with \`{ } or \`( ). +surrounding it with \`{ }, or \`[ ] or \`( ). Terms surrounded by \`{ } introduce their free variables as maximally -inserted implicit arguments, and terms surrounded by \`( ) introduce -them as explicit arguments. +inserted implicit arguments, terms surrounded by \`[ ] introduce them as +non maximally inserted implicit arguments and terms surrounded by \`( ) +introduce them as explicit arguments. Generalizing binders always introduce their free variables as maximally inserted implicit arguments. The binder itself introduces @@ -2204,31 +2253,26 @@ Multiple binders can be merged using ``,`` as a separator: Check (forall `{Commutative A, Hnat : !Commutative nat}, True). -One can control the set of generalizable identifiers with -the ``Generalizable`` vernacular command to avoid unexpected -generalizations when mistyping identifiers. There are several commands -that specify which variables should be generalizable. - -.. cmd:: Generalizable All Variables +.. cmd:: Generalizable {| {| Variable | Variables } {+ @ident } | All Variables | No Variables } - All variables are candidate for - generalization if they appear free in the context under a - generalization delimiter. This may result in confusing errors in case - of typos. In such cases, the context will probably contain some - unexpected generalized variable. - -.. cmd:: Generalizable No Variables + Controls the set of generalizable identifiers. By default, no variables are + generalizable. - Disable implicit generalization entirely. This is the default behavior. + This command supports the :attr:`global` attribute. -.. cmd:: Generalizable {| Variable | Variables } {+ @ident } + The :n:`{| Variable | Variables } {+ @ident }` form allows generalization of only the given :n:`@ident`\s. + Using this command multiple times adds to the allowed identifiers. The other forms clear + the list of :n:`@ident`\s. - Allow generalization of the given identifiers only. Calling this command multiple times - adds to the allowed identifiers. + The :n:`All Variables` form generalizes all free variables in + the context that appear under a + generalization delimiter. This may result in confusing errors in case + of typos. In such cases, the context will probably contain some + unexpected generalized variables. -.. cmd:: Global Generalizable + The :n:`No Variables` form disables implicit generalization entirely. This is + the default behavior (before any :cmd:`Generalizable` command has been entered). - Allows exporting the choice of generalizable variables. .. _Coercions: @@ -2240,7 +2284,7 @@ which they reside into another one. A *class* is either a sort (denoted by the keyword ``Sortclass``), a product type (denoted by the keyword ``Funclass``), or a type constructor (denoted by its name), e.g. an inductive type or any constant with a type of the form -``forall (`` |x_1| : |A_1| ) … ``(``\ |x_n| : |A_n|\ ``)``, `s` where `s` is a sort. +:n:`forall {+ @binder }, @sort`. Then the user is able to apply an object that is not a function, but can be coerced to a function, and more generally to consider that a @@ -2282,47 +2326,36 @@ Printing universes terms apparently identical but internally different in the Calculus of Inductive Constructions. -.. cmd:: Print {? Sorted} Universes +.. cmd:: Print {? Sorted } Universes {? Subgraph ( {* @qualid } ) } {? @string } :name: Print 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 ``Sorted`` keyword is present, each universe will be made + The :n:`Subgraph` clause limits the printed graph to the requested names (adjusting + constraints to preserve the implied transitive constraints between + kept universes). + + The :n:`Sorted` clause makes each universe equivalent to a numbered label reflecting its level (with a linear ordering) in the universe hierarchy. - .. cmdv:: Print {? Sorted} Universes @string - - This variant accepts an optional output filename. - - If :token:`string` ends in ``.dot`` or ``.gv``, the constraints are printed in the DOT - language, and can be processed by Graphviz tools. The format is - unspecified if `string` doesn’t end in ``.dot`` or ``.gv``. - -.. cmdv:: Print Universes Subgraph({+ @qualid }) - :name: Print Universes Subgraph - - Prints the graph restricted to the requested names (adjusting - constraints to preserve the implied transitive constraints between - kept universes). + :n:`@string` is an optional output filename. + If :n:`@string` ends in ``.dot`` or ``.gv``, the constraints are printed in the DOT + language, and can be processed by Graphviz tools. The format is + unspecified if `string` doesn’t end in ``.dot`` or ``.gv``. .. _existential-variables: Existential variables --------------------- -.. insertgram term_evar evar_binding +.. insertprodn term_evar term_evar -.. 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` +.. prodn:: + term_evar ::= ?[ @ident ] + | ?[ ?@ident ] + | ?@ident {? @%{ {+; @ident := @term } %} } |Coq| terms can include existential variables which represents unknown subterms to eventually be replaced by actual subterms. @@ -2514,6 +2547,8 @@ 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: + Bidirectionality hints ---------------------- @@ -2524,15 +2559,14 @@ Bidirectionality hints make it possible to specify that after type-checking the first arguments of an application, typing information should be propagated from the context to help inferring the types of the remaining arguments. -.. cmd:: Arguments @qualid {* @ident__1 } & {* @ident__2} - :name: Arguments (bidirectionality hints) - - This commands tells the typechecking algorithm, when type-checking - applications of :n:`@qualid`, to first type-check the arguments in - :n:`@ident__1` and then propagate information from the typing context to - type-check the remaining arguments (in :n:`@ident__2`). +An :cmd:`Arguments` command containing :n:`@argument_spec_block__1 & @argument_spec_block__2` +provides :ref:`bidirectionality_hints`. +It tells the typechecking algorithm, when type-checking +applications of :n:`@qualid`, to first type-check the arguments in +:n:`@argument_spec_block__1` and then propagate information from the typing context to +type-check the remaining arguments (in :n:`@argument_spec_block__2`). -.. example:: +.. example:: Bidirectionality hints In a context where a coercion was declared from ``bool`` to ``nat``: @@ -2555,3 +2589,8 @@ the context to help inferring the types of the remaining arguments. Arguments ex_intro _ _ & _ _. Check (ex_intro _ true _ : exists n : nat, n > 0). + +Coq will attempt to produce a term which uses the arguments you +provided, but in some cases involving Program mode the arguments after +the bidirectionality starts may be replaced by convertible but +syntactically different terms. diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 3cc101d06b..f4592f8f37 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -16,27 +16,27 @@ In Coq, logical objects are typed to ensure their logical correctness. The rules implemented by the typing algorithm are described in Chapter :ref:`calculusofinductiveconstructions`. -About the grammars in the manual -================================ +.. About the grammars in the manual + ================================ -Grammars are presented in Backus-Naur form (BNF). Terminal symbols are -set in black ``typewriter font``. In addition, there are special notations for -regular expressions. + Grammars are presented in Backus-Naur form (BNF). Terminal symbols are + set in black ``typewriter font``. In addition, there are special notations for + regular expressions. -An expression enclosed in square brackets ``[…]`` means at most one -occurrence of this expression (this corresponds to an optional -component). + An expression enclosed in square brackets ``[…]`` means at most one + occurrence of this expression (this corresponds to an optional + component). -The notation “``entry sep … sep entry``” stands for a non empty sequence -of expressions parsed by entry and separated by the literal “``sep``” [1]_. + The notation “``entry sep … sep entry``” stands for a non empty sequence + of expressions parsed by entry and separated by the literal “``sep``” [1]_. -Similarly, the notation “``entry … entry``” stands for a non empty -sequence of expressions parsed by the “``entry``” entry, without any -separator between. + Similarly, the notation “``entry … entry``” stands for a non empty + sequence of expressions parsed by the “``entry``” entry, without any + separator between. -At the end, the notation “``[entry sep … sep entry]``” stands for a -possibly empty sequence of expressions parsed by the “``entry``” entry, -separated by the literal “``sep``”. + At the end, the notation “``[entry sep … sep entry]``” stands for a + possibly empty sequence of expressions parsed by the “``entry``” entry, + separated by the literal “``sep``”. .. _lexical-conventions: @@ -49,19 +49,21 @@ Blanks Comments Comments are enclosed between ``(*`` and ``*)``. They can be nested. - They can contain any character. However, embedded :token:`string` literals must be + They can contain any character. However, embedded :n:`@string` literals must be correctly closed. Comments are treated as blanks. Identifiers - Identifiers, written :token:`ident`, are sequences of letters, digits, ``_`` and + Identifiers, written :n:`@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; it is not a valid identifier): - .. productionlist:: coq - ident : `first_letter`[`subsequent_letter`…`subsequent_letter`] - first_letter : a..z ∣ A..Z ∣ _ ∣ `unicode_letter` - subsequent_letter : `first_letter` ∣ 0..9 ∣ ' ∣ `unicode_id_part` + .. insertprodn ident subsequent_letter + + .. prodn:: + ident ::= @first_letter {* @subsequent_letter } + first_letter ::= {| a .. z | A .. Z | _ | @unicode_letter } + subsequent_letter ::= {| @first_letter | @digit | ' | @unicode_id_part } All characters are meaningful. In particular, identifiers are case-sensitive. :production:`unicode_letter` non-exhaustively includes Latin, @@ -72,18 +74,18 @@ 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; - a numeral without fractional or exponent parts. :token:`num` is a non-negative + and exponent, optionally preceded by a minus sign. :n:`@int` is an integer; + a numeral without fractional or exponent parts. :n:`@num` is a non-negative integer. Underscores embedded in the digits are ignored, for example ``1_000_000`` is the same as ``1000000``. - .. productionlist:: coq - numeral : `num`[. `num`][`exp`[`sign`]`num`] - int : [-]`num` - num : `digit`…`digit` - digit : 0..9 - exp : e | E - sign : + | - + .. insertprodn numeral digit + + .. prodn:: + numeral ::= {+ @digit } {? . {+ @digit } } {? {| e | E } {? {| + | - } } {+ @digit } } + int ::= {? - } {+ @digit } + num ::= {+ @digit } + digit ::= 0 .. 9 Strings Strings begin and end with ``"`` (double quote). Use ``""`` to represent @@ -115,7 +117,7 @@ Other tokens ! #[ % & ' ( () (bfs) (dfs) ) * ** + , - -> . .( .. ... / : ::= := :> :>> ; < <+ <- <: - <<: <= = => > >-> >= ? @ @{ [ [= ] _ _eqn + <<: <= = => > >-> >= ? @ @{ [ [= ] _ `( `{ { {| | |- || } When multiple tokens match the beginning of a sequence of characters, @@ -139,78 +141,82 @@ 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`. -.. 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` +.. insertprodn term field_def + +.. prodn:: + term ::= forall @open_binders , @term + | fun @open_binders => @term + | @term_let + | if @term {? {? as @name } return @term100 } then @term else @term + | @term_fix + | @term_cofix + | @term100 + term100 ::= @term_cast + | @term10 + term10 ::= @term1 {+ @arg } + | @ @qualid {? @univ_annot } {* @term1 } + | @term1 + arg ::= ( @ident := @term ) + | @term1 + one_term ::= @term1 + | @ @qualid {? @univ_annot } + term1 ::= @term_projection + | @term0 % @ident + | @term0 + term0 ::= @qualid {? @univ_annot } + | @sort + | @numeral + | @string + | _ + | @term_evar + | @term_match + | ( @term ) + | %{%| {* @field_def } %|%} + | `%{ @term %} + | `( @term ) + | ltac : ( @ltac_expr ) + field_def ::= @qualid {* @binder } := @term + +.. note:: + + Many commands and tactics use :n:`@one_term` rather than :n:`@term`. + The former need to be enclosed in parentheses unless they're very + simple, such as a single identifier. This avoids confusing a space-separated + list of terms with a :n:`@term1` applied to a list of arguments. + +.. _types: Types ----- -Coq terms are typed. Coq types are recognized by the same syntactic -class as :token:`term`. We denote by :production:`type` the semantic subclass -of types inside the syntactic class :token:`term`. +.. prodn:: + type ::= @term + +:n:`@type`\s are a subset of :n:`@term`\s; not every :n:`@term` is a :n:`@type`. +Every term has an associated type, which +can be determined by applying the :ref:`typing-rules`. Distinct terms +may share the same type, for example 0 and 1 are both of type `nat`, the +natural numbers. .. _gallina-identifiers: Qualified identifiers and simple identifiers -------------------------------------------- -.. insertgram qualid field +.. insertprodn qualid field_ident -.. productionlist:: coq - qualid : `qualid` `field` - : `ident` - field : .`ident` +.. prodn:: + qualid ::= @ident {* @field_ident } + field_ident ::= .@ident -*Qualified identifiers* (:token:`qualid`) denote *global constants* +*Qualified identifiers* (:n:`@qualid`) denote *global constants* (definitions, lemmas, theorems, remarks or facts), *global variables* (parameters or axioms), *inductive types* or *constructors of inductive -types*. *Simple identifiers* (or shortly :token:`ident`) are a syntactic subset +types*. *Simple identifiers* (or shortly :n:`@ident`) are a syntactic subset of qualified identifiers. Identifiers may also denote *local variables*, while qualified identifiers do not. -Field identifiers, written :token:`field`, are identifiers prefixed by +Field identifiers, written :n:`@field_ident`, are identifiers prefixed by `.` (dot) with no blank between the dot and the identifier. @@ -225,7 +231,7 @@ numbers (see :ref:`datatypes`). .. note:: - Negative integers are not at the same level as :token:`num`, for this + Negative integers are not at the same level as :n:`@num`, for this would make precedence unnatural. .. index:: @@ -237,34 +243,29 @@ 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` +.. insertprodn sort univ_constraint + +.. prodn:: + sort ::= Set + | Prop + | SProp + | Type + | Type @%{ _ %} + | Type @%{ @universe %} + universe ::= max ( {+, @universe_expr } ) + | @universe_expr + universe_expr ::= @universe_name {? + @num } + universe_name ::= @qualid + | Set + | Prop + univ_annot ::= @%{ {* @universe_level } %} + universe_level ::= Set + | Prop + | Type + | _ + | @qualid + univ_decl ::= @%{ {* @ident } {? + } {? %| {*, @univ_constraint } {? + } } %} + univ_constraint ::= @universe_name {| < | = | <= } @universe_name There are four sorts :g:`SProp`, :g:`Prop`, :g:`Set` and :g:`Type`. @@ -272,13 +273,13 @@ There are four sorts :g:`SProp`, :g:`Prop`, :g:`Set` and :g:`Type`. propositions* (also called *strict propositions*). - :g:`Prop` is the universe of *logical propositions*. The logical propositions - themselves are typing the proofs. We denote propositions by :production:`form`. - This constitutes a semantic subclass of the syntactic class :token:`term`. + themselves are typing the proofs. We denote propositions by :n:`@form`. + This constitutes a semantic subclass of the syntactic class :n:`@term`. - :g:`Set` is the universe of *program types* or *specifications*. The specifications themselves are typing the programs. We denote - specifications by :production:`specif`. This constitutes a semantic subclass of - the syntactic class :token:`term`. + specifications by :n:`@specif`. This constitutes a semantic subclass of + the syntactic class :n:`@term`. - :g:`Type` is the type of sorts. @@ -289,34 +290,20 @@ 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` - +.. insertprodn open_binders binder + +.. prodn:: + open_binders ::= {+ @name } : @term + | {+ @binder } + name ::= _ + | @ident + binder ::= @name + | ( {+ @name } : @type ) + | ( @name {? : @type } := @term ) + | @implicit_binders + | @generalizing_binder + | ( @name : @type %| @term ) + | ' @pattern0 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 @@ -328,14 +315,14 @@ a notation for a sequence of binding variables sharing the same type: binder can also be any pattern prefixed by a quote, e.g. :g:`'(x,y)`. Some constructions allow the binding of a variable to value. This is -called a “let-binder”. The entry :token:`binder` of the grammar accepts +called a “let-binder”. The entry :n:`@binder` of the grammar accepts either an assumption binder as defined above or a let-binder. The notation in the latter case is :n:`(@ident := @term)`. In a let-binder, only one variable can be introduced at the same time. It is also possible to give the type of the variable as follows: :n:`(@ident : @type := @term)`. -Lists of :token:`binder` are allowed. In the case of :g:`fun` and :g:`forall`, +Lists of :n:`@binder`\s are allowed. In the case of :g:`fun` and :g:`forall`, it is intended that at least one binder of the list is an assumption otherwise fun and forall gets identical. Moreover, parentheses can be omitted in the case of a single sequence of bindings sharing the same type (e.g.: @@ -347,18 +334,15 @@ Abstractions: fun ----------------- The expression :n:`fun @ident : @type => @term` defines the -*abstraction* of the variable :token:`ident`, of type :token:`type`, over the term -:token:`term`. It denotes a function of the variable :token:`ident` that evaluates to -the expression :token:`term` (e.g. :g:`fun x : A => x` denotes the identity +*abstraction* of the variable :n:`@ident`, of type :n:`@type`, over the term +:n:`@term`. It denotes a function of the variable :n:`@ident` that evaluates to +the expression :n:`@term` (e.g. :g:`fun x : A => x` denotes the identity function on type :g:`A`). The keyword :g:`fun` can be followed by several binders as given in Section :ref:`binders`. Functions over several variables are equivalent to an iteration of one-variable functions. For instance the expression -“fun :token:`ident`\ :math:`_{1}` … :token:`ident`\ :math:`_{n}` -: :token:`type` => :token:`term`” -denotes the same function as “ fun :token:`ident`\ -:math:`_{1}` : :token:`type` => … -fun :token:`ident`\ :math:`_{n}` : :token:`type` => :token:`term`”. If +:n:`fun {+ @ident__i } : @type => @term` +denotes the same function as :n:`{+ fun @ident__i : @type => } @term`. If a let-binder occurs in the list of binders, it is expanded to a let-in definition (see Section :ref:`let-in`). @@ -369,12 +353,12 @@ 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`. +*product* of the variable :n:`@ident` of type :n:`@type`, over the term :n:`@term`. As for abstractions, :g:`forall` is followed by a binder list, and products over several variables are equivalent to an iteration of one-variable -products. Note that :token:`term` is intended to be a type. +products. Note that :n:`@term` is intended to be a type. -If the variable :token:`ident` occurs in :token:`term`, the product is called +If the variable :n:`@ident` occurs in :n:`@term`, the product is called *dependent product*. The intention behind a dependent product :g:`forall x : A, B` is twofold. It denotes either the universal quantification of the variable :g:`x` of type :g:`A` @@ -389,15 +373,14 @@ the propositional implication and function types. Applications ------------ -The expression :token:`term`\ :math:`_0` :token:`term`\ :math:`_1` denotes the -application of :token:`term`\ :math:`_0` to :token:`term`\ :math:`_1`. +The expression :n:`@term__fun @term` denotes the application of +:n:`@term__fun` (which is expected to have a function type) to +:token:`term`. -The expression :token:`term`\ :math:`_0` :token:`term`\ :math:`_1` ... -:token:`term`\ :math:`_n` denotes the application of the term -:token:`term`\ :math:`_0` to the arguments :token:`term`\ :math:`_1` ... then -:token:`term`\ :math:`_n`. It is equivalent to ( … ( :token:`term`\ :math:`_0` -:token:`term`\ :math:`_1` ) … ) :token:`term`\ :math:`_n` : associativity is to the -left. +The expression :n:`@term__fun {+ @term__i }` denotes the application +of the term :n:`@term__fun` to the arguments :n:`@term__i`. It is +equivalent to :n:`( … ( @term__fun @term__1 ) … ) @term__n`: +associativity is to the left. The notation :n:`(@ident := @term)` for arguments is used for making explicit the value of implicit arguments (see @@ -411,22 +394,22 @@ Section :ref:`explicit-applications`). Type cast --------- -.. insertgram term_cast term_cast +.. insertprodn term_cast term_cast -.. productionlist:: coq - term_cast : `term10` <: `term` - : `term10` <<: `term` - : `term10` : `term` - : `term10` :> +.. prodn:: + 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`. +the type of :n:`@term` to be :n:`@type`. :n:`@term <: @type` locally sets up the virtual machine for checking that -:token:`term` has type :token:`type`. +:n:`@term` has type :n:`@type`. -:n:`@term <<: @type` uses native compilation for checking that :token:`term` -has type :token:`type`. +:n:`@term <<: @type` uses native compilation for checking that :n:`@term` +has type :n:`@type`. .. index:: _ @@ -444,25 +427,18 @@ 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` +.. insertprodn term_let term_let + +.. prodn:: + term_let ::= let @name {? : @type } := @term in @term + | let @name {+ @binder } {? : @type } := @term in @term + | let ( {*, @name } ) {? {? as @name } return @term100 } := @term in @term + | let ' @pattern := @term {? return @term100 } in @term + | let ' @pattern in @pattern := @term return @term100 in @term :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 +denotes the local binding of :n:`@term` to the variable +:n:`@ident` in :n:`@term`’. There is a syntactic sugar for let-in definition of functions: :n:`let @ident {+ @binder} := @term in @term’` stands for :n:`let @ident := fun {+ @binder} => @term in @term’`. @@ -471,57 +447,25 @@ stands for :n:`let @ident := fun {+ @binder} => @term in @term’`. 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` +.. insertprodn term_match pattern0 + +.. prodn:: + term_match ::= match {+, @case_item } {? return @term100 } with {? %| } {*| @eqn } end + case_item ::= @term100 {? as @name } {? in @pattern } + eqn ::= {+| {+, @pattern } } => @term + pattern ::= @pattern10 : @term + | @pattern10 + pattern10 ::= @pattern1 as @name + | @pattern1 {* @pattern1 } + | @ @qualid {* @pattern1 } + pattern1 ::= @pattern0 % @ident + | @pattern0 + pattern0 ::= @qualid + | %{%| {* @qualid := @pattern } %|%} + | _ + | ( {+| @pattern } ) + | @numeral + | @string Objects of inductive types can be destructured by a case-analysis construction called *pattern matching* expression. A pattern matching @@ -531,31 +475,30 @@ 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:`case_item` expression, a :token:`patterns_comma` restricted to a -single :token:`pattern` and :token:`pattern` restricted to the form +by a single :n:`@case_item` expression, an :n:`@eqn` restricted to a +single :n:`@pattern` and :n:`@pattern` restricted to the form :n:`@qualid {* @ident}`. -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 -of an inductive type :math:`I`). The terms :token:`term`:math:`_1`\ …\ -:token:`term`:math:`_n` are the *branches* of the pattern matching -expression. Each of :token:`pattern`:math:`_i` has a form :token:`qualid` -:token:`ident` where :token:`qualid` must denote a constructor. There should be +The expression +:n:`match @term {? return @term100 } with {+| @pattern__i => @term__i } end` denotes a +*pattern matching* over the term :n:`@term` (expected to be +of an inductive type :math:`I`). The :n:`@term__i` +are the *branches* of the pattern matching +expression. Each :n:`@pattern__i` has the form :n:`@qualid @ident` +where :n:`@qualid` must denote a constructor. There should be exactly one branch for every constructor of :math:`I`. -The :token:`return_type_opt` expresses the type returned by the whole match +The :n:`return @term100` clause gives 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_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]_. +branches have the same type, and the :n:`return @term100` specifies that type. +In this case, :n:`return @term100` can usually be omitted as it can be +inferred from the type of the branches [1]_. In the *dependent* case, there are three subcases. In the first subcase, the type in each branch may depend on the exact value being matched in the branch. In this case, the whole pattern matching itself depends on the term being matched. This dependency of the term being matched in the -return type is expressed with an “as :token:`ident`” clause where :token:`ident` +return type is expressed with an :n:`@ident` clause where :n:`@ident` is dependent in the return type. For instance, in the following example: .. coqtop:: in @@ -604,19 +547,19 @@ type of each branch can depend on the type dependencies specific to the branch and the whole pattern matching expression has a type determined by the specific dependencies in the type of the term being matched. This dependency of the return type in the annotations of the inductive type -is expressed using a “:g:`in` :math:`I` :g:`_ … _` :token:`pattern`:math:`_1` … -:token:`pattern`:math:`_n`” clause, where +is expressed with a clause in the form +:n:`in @qualid {+ _ } {+ @pattern }`, where -- :math:`I` is the inductive type of the term being matched; +- :n:`@qualid` is the inductive type of the term being matched; -- the :g:`_` are matching the parameters of the inductive type: the +- the holes :n:`_` match the parameters of the inductive type: the return type is not dependent on them. -- the :token:`pattern`:math:`_i` are matching the annotations of the +- each :n:`@pattern` matches the annotations of the inductive type: the return type is dependent on them -- in the basic case which we describe below, each :token:`pattern`:math:`_i` - is a name :token:`ident`:math:`_i`; see :ref:`match-in-patterns` for the +- in the basic case which we describe below, each :n:`@pattern` + is a name :n:`@ident`; see :ref:`match-in-patterns` for the general case For instance, in the following example: @@ -651,105 +594,70 @@ Sections :ref:`if-then-else` and :ref:`irrefutable-patterns`). 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`` -:token:`ident`:math:`_n` :token:`binder`:math:`_n` : :token:`type`:math:`_n` -``:=`` :token:`term`:math:`_n` ``for`` :token:`ident`:math:`_i`” denotes the +.. insertprodn term_fix fixannot + +.. prodn:: + term_fix ::= let fix @fix_body in @term + | fix @fix_body {? {+ with @fix_body } for @ident } + fix_body ::= @ident {* @binder } {? @fixannot } {? : @type } := @term + fixannot ::= %{ struct @ident %} + | %{ wf @one_term @ident %} + | %{ measure @one_term {? @ident } {? @one_term } %} + + +The expression ":n:`fix @ident__1 @binder__1 : @type__1 := @term__1 with … with @ident__n @binder__n : @type__n := @term__n for @ident__i`" denotes the :math:`i`-th component of a block of functions defined by mutual structural recursion. It is the local counterpart of the :cmd:`Fixpoint` command. When -:math:`n=1`, the “``for`` :token:`ident`:math:`_i`” clause is omitted. - -The expression “``cofix`` :token:`ident`:math:`_1` :token:`binder`:math:`_1` ``:`` -:token:`type`:math:`_1` ``with … with`` :token:`ident`:math:`_n` :token:`binder`:math:`_n` -: :token:`type`:math:`_n` ``for`` :token:`ident`:math:`_i`” denotes the -:math:`i`-th component of a block of terms defined by a mutual guarded -co-recursion. It is the local counterpart of the :cmd:`CoFixpoint` command. When -:math:`n=1`, the “``for`` :token:`ident`:math:`_i`” clause is omitted. +:math:`n=1`, the ":n:`for @ident__i`" clause is omitted. The association of a single fixpoint and a local definition have a special -syntax: :n:`let fix @ident @binders := @term in` stands for -:n:`let @ident := fix @ident @binders := @term in`. The same applies for co-fixpoints. +syntax: :n:`let fix @ident {* @binder } := @term in` stands for +:n:`let @ident := fix @ident {* @binder } := @term in`. The same applies for co-fixpoints. + +Some options of :n:`@fixannot` are only supported in specific constructs. :n:`fix` and :n:`let fix` +only support the :n:`struct` option, while :n:`wf` and :n:`measure` are only supported in +commands such as :cmd:`Function` and :cmd:`Program Fixpoint`. + +.. insertprodn term_cofix cofix_body + +.. prodn:: + term_cofix ::= let cofix @cofix_body in @term + | cofix @cofix_body {? {+ with @cofix_body } for @ident } + cofix_body ::= @ident {* @binder } {? : @type } := @term + +The expression +":n:`cofix @ident__1 @binder__1 : @type__1 with … with @ident__n @binder__n : @type__n for @ident__i`" +denotes the :math:`i`-th component of a block of terms defined by a mutual guarded +co-recursion. It is the local counterpart of the :cmd:`CoFixpoint` command. When +:math:`n=1`, the ":n:`for @ident__i`" clause is omitted. .. _vernacular: The Vernacular ============== -.. insertgramXX vernac ident_opt2 - -.. productionlist:: coq - decorated-sentence : [ `decoration` … `decoration` ] `sentence` - sentence : `assumption` - : `definition` - : `inductive` - : `fixpoint` - : `assertion` `proof` - assumption : `assumption_keyword` `assums`. - assumption_keyword : Axiom | Conjecture - : Parameter | Parameters - : Variable | Variables - : Hypothesis | Hypotheses - assums : `ident` … `ident` : `term` - : ( `ident` … `ident` : `term` ) … ( `ident` … `ident` : `term` ) - definition : [Local] Definition `ident` [`binders`] [: `term`] := `term` . - : Let `ident` [`binders`] [: `term`] := `term` . - inductive : Inductive `ind_body` with … with `ind_body` . - : CoInductive `ind_body` with … with `ind_body` . - ind_body : `ident` [`binders`] : `term` := - : [[|] `ident` [`binders`] [:`term`] | … | `ident` [`binders`] [:`term`]] - fixpoint : Fixpoint `fix_body` with … with `fix_body` . - : CoFixpoint `fix_body` with … with `fix_body` . - assertion : `assertion_keyword` `ident` [`binders`] : `term` . - assertion_keyword : Theorem | Lemma - : Remark | Fact - : Corollary | Property | Proposition - : Definition | Example - proof : Proof . … Qed . - : Proof . … Defined . - : Proof . … Admitted . - decoration : #[ `attributes` ] - attributes : [`attribute`, … , `attribute`] - attribute : `ident` - : `ident` = `string` - : `ident` ( `attributes` ) - -.. todo:: This use of … in this grammar is inconsistent - What about removing the proof part of this grammar from this chapter - and putting it somewhere where top-level tactics can be described as well? - See also #7583. - -This grammar describes *The Vernacular* which is the language of -commands of Gallina. A sentence of the vernacular language, like in -many natural languages, begins with a capital letter and ends with a -dot. - -Sentences may be *decorated* with so-called *attributes*, -which are described in the corresponding section (:ref:`gallina-attributes`). - -The different kinds of command are described hereafter. They all suppose -that the terms occurring in the sentences are well-typed. +.. insertprodn vernacular vernacular + +.. prodn:: + vernacular ::= {* {? @all_attrs } {| @command | @ltac_expr } . } + +The top-level input to |Coq| is a series of :production:`command`\s and :production:`tactic`\s, +each terminated with a period +and optionally decorated with :ref:`gallina-attributes`. :n:`@ltac_expr` syntax supports both simple +and compound tactics. For example: ``split`` is a simple tactic while ``split; auto`` combines two +simple tactics. + +Tactics specify how to transform the current proof state as a step in creating a proof. They +are syntactically valid only when |Coq| is in proof mode, such as after a :cmd:`Theorem` command +and before any subsequent proof-terminating command such as :cmd:`Qed`. See :ref:`proofhandling` for more +on proof mode. + +By convention, command names begin with uppercase letters, while +tactic names begin with lowercase letters. Commands appear in the +HTML documentation in blue boxes after the label "Command". In the pdf, they appear +after the boldface label "Command:". Commands are listed in the :ref:`command_index`. + +Similarly, tactics appear after the label "Tactic". Tactics are listed in the :ref:`tactic_index`. .. _gallina-assumptions: @@ -757,73 +665,70 @@ Assumptions ----------- Assumptions extend the environment with axioms, parameters, hypotheses -or variables. An assumption binds an :token:`ident` to a :token:`type`. It is accepted -by Coq if and only if this :token:`type` is a correct type in the environment -preexisting the declaration and if :token:`ident` was not previously defined in -the same module. This :token:`type` is considered to be the type (or -specification, or statement) assumed by :token:`ident` and we say that :token:`ident` -has type :token:`type`. +or variables. An assumption binds an :n:`@ident` to a :n:`@type`. It is accepted +by Coq if and only if this :n:`@type` is a correct type in the environment +preexisting the declaration and if :n:`@ident` was not previously defined in +the same module. This :n:`@type` is considered to be the type (or +specification, or statement) assumed by :n:`@ident` and we say that :n:`@ident` +has type :n:`@type`. .. _Axiom: -.. cmd:: Parameter @ident : @type - - This command links :token:`type` to the name :token:`ident` as its specification in - the global context. The fact asserted by :token:`type` is thus assumed as a - postulate. - - .. exn:: @ident already exists. - :name: @ident already exists. (Axiom) - :undocumented: +.. cmd:: @assumption_token {? Inline {? ( @num ) } } {| {+ ( @assumpt ) } | @assumpt } + :name: Axiom; Axioms; Conjecture; Conjectures; Hypothesis; Hypotheses; Parameter; Parameters; Variable; Variables - .. cmdv:: Parameter {+ @ident } : @type + .. insertprodn assumption_token of_type - Adds several parameters with specification :token:`type`. + .. prodn:: + assumption_token ::= {| Axiom | Axioms } + | {| Conjecture | Conjectures } + | {| Parameter | Parameters } + | {| Hypothesis | Hypotheses } + | {| Variable | Variables } + assumpt ::= {+ @ident_decl } @of_type + ident_decl ::= @ident {? @univ_decl } + of_type ::= {| : | :> | :>> } @type - .. cmdv:: Parameter {+ ( {+ @ident } : @type ) } + These commands bind one or more :n:`@ident`\(s) to specified :n:`@type`\(s) as their specifications in + the global context. The fact asserted by the :n:`@type` (or, equivalently, the existence + of an object of this type) is accepted as a postulate. - Adds blocks of parameters with different specifications. + :cmd:`Axiom`, :cmd:`Conjecture`, :cmd:`Parameter` and their plural forms + are equivalent. They can take the :attr:`local` attribute (see :ref:`gallina-attributes`), + which makes the defined :n:`@ident`\s accessible by :cmd:`Import` and its variants + only through their fully qualified names. - .. cmdv:: Local Parameter {+ ( {+ @ident } : @type ) } - :name: Local Parameter + Similarly, :cmd:`Hypothesis`, :cmd:`Variable` and their plural forms are equivalent. Outside + of a section, these are equivalent to :n:`Local Parameter`. Inside a section, the + :n:`@ident`\s defined are only accessible within the section. When the current section + is closed, the :n:`@ident`\(s) become undefined and every object depending on them will be explicitly + parameterized (i.e., the variables are *discharged*). See Section :ref:`section-mechanism`. - Such parameters are never made accessible through their unqualified name by - :cmd:`Import` and its variants. You have to explicitly give their fully - qualified name to refer to them. + The :n:`Inline` clause is only relevant inside functors. See :cmd:`Module`. - .. cmdv:: {? Local } Parameters {+ ( {+ @ident } : @type ) } - {? Local } Axiom {+ ( {+ @ident } : @type ) } - {? Local } Axioms {+ ( {+ @ident } : @type ) } - {? Local } Conjecture {+ ( {+ @ident } : @type ) } - {? Local } Conjectures {+ ( {+ @ident } : @type ) } - :name: Parameters; Axiom; Axioms; Conjecture; Conjectures +.. example:: Simple assumptions - These variants are synonyms of :n:`{? Local } Parameter {+ ( {+ @ident } : @type ) }`. + .. coqtop:: reset in - .. cmdv:: Variable {+ ( {+ @ident } : @type ) } - Variables {+ ( {+ @ident } : @type ) } - Hypothesis {+ ( {+ @ident } : @type ) } - Hypotheses {+ ( {+ @ident } : @type ) } - :name: Variable (outside a section); Variables (outside a section); Hypothesis (outside a section); Hypotheses (outside a section) + Parameter X Y : Set. + Parameter (R : X -> Y -> Prop) (S : Y -> X -> Prop). + Axiom R_S_inv : forall x y, R x y <-> S y x. - Outside of any section, these variants are synonyms of - :n:`Local Parameter {+ ( {+ @ident } : @type ) }`. - For their meaning inside a section, see :cmd:`Variable` in - :ref:`section-mechanism`. +.. exn:: @ident already exists. + :name: @ident already exists. (Axiom) + :undocumented: - .. warn:: @ident is declared as a local axiom [local-declaration,scope] +.. warn:: @ident is declared as a local axiom [local-declaration,scope] - Warning generated when using :cmd:`Variable` instead of - :cmd:`Local Parameter`. + Warning generated when using :cmd:`Variable` or its equivalent + instead of :n:`Local Parameter` or its equivalent. .. note:: - It is advised to use the commands :cmd:`Axiom`, :cmd:`Conjecture` and + We advise using the commands :cmd:`Axiom`, :cmd:`Conjecture` and :cmd:`Hypothesis` (and their plural forms) for logical postulates (i.e. when - the assertion :token:`type` is of sort :g:`Prop`), and to use the commands + the assertion :n:`@type` is of sort :g:`Prop`), and to use the commands :cmd:`Parameter` and :cmd:`Variable` (and their plural forms) in other cases - (corresponding to the declaration of an abstract mathematical entity). - -.. seealso:: Section :ref:`section-mechanism`. + (corresponding to the declaration of an abstract object of the given type). .. _gallina-definitions: @@ -846,85 +751,94 @@ type which is the type of its body. A formal presentation of constants and environments is given in Section :ref:`typing-rules`. -.. cmd:: Definition @ident := @term - - This command binds :token:`term` to the name :token:`ident` in the environment, - provided that :token:`term` is well-typed. +.. cmd:: {| Definition | Example } @ident_decl @def_body + :name: Definition; Example - .. exn:: @ident already exists. - :name: @ident already exists. (Definition) - :undocumented: + .. insertprodn def_body def_body - .. cmdv:: Definition @ident : @type := @term + .. prodn:: + def_body ::= {* @binder } {? : @type } := {? @reduce } @term + | {* @binder } : @type - This variant checks that the type of :token:`term` is definitionally equal to - :token:`type`, and registers :token:`ident` as being of type - :token:`type`, and bound to value :token:`term`. + These commands bind :n:`@term` to the name :n:`@ident` in the environment, + provided that :n:`@term` is well-typed. They can take the :attr:`local` attribute (see :ref:`gallina-attributes`), + which makes the defined :n:`@ident` accessible by :cmd:`Import` and its variants + only through their fully qualified names. + If :n:`@reduce` is present then :n:`@ident` is bound to the result of the specified + computation on :n:`@term`. - .. exn:: The term @term has type @type while it is expected to have type @type'. - :undocumented: + These commands also support the :attr:`universes(polymorphic)`, + :attr:`universes(monomorphic)`, :attr:`program` and + :attr:`canonical` attributes. - .. cmdv:: Definition @ident @binders {? : @type } := @term + If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. + This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic. + In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant + for which the computational behavior is relevant. See :ref:`proof-editing-mode`. - This is equivalent to - :n:`Definition @ident : forall @binders, @type := fun @binders => @term`. + The form :n:`Definition @ident : @type := @term` checks that the type of :n:`@term` + is definitionally equal to :n:`@type`, and registers :n:`@ident` as being of type + :n:`@type`, and bound to value :n:`@term`. - .. cmdv:: Local Definition @ident {? @binders } {? : @type } := @term - :name: Local Definition + The form :n:`Definition @ident {* @binder } : @type := @term` is equivalent to + :n:`Definition @ident : forall {* @binder }, @type := fun {* @binder } => @term`. - Such definitions are never made accessible through their - unqualified name by :cmd:`Import` and its variants. - You have to explicitly give their fully qualified name to refer to them. - - .. cmdv:: {? Local } Example @ident {? @binders } {? : @type } := @term - :name: Example - - This is equivalent to :cmd:`Definition`. - - .. cmdv:: Let @ident := @term - :name: Let (outside a section) - - Outside of any section, this variant is a synonym of - :n:`Local Definition @ident := @term`. - For its meaning inside a section, see :cmd:`Let` in - :ref:`section-mechanism`. - - .. warn:: @ident is declared as a local definition [local-declaration,scope] + .. seealso:: :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`. - Warning generated when using :cmd:`Let` instead of - :cmd:`Local Definition`. + .. exn:: @ident already exists. + :name: @ident already exists. (Definition) + :undocumented: -.. seealso:: Section :ref:`section-mechanism`, commands :cmd:`Opaque`, - :cmd:`Transparent`, and tactic :tacn:`unfold`. + .. exn:: The term @term has type @type while it is expected to have type @type'. + :undocumented: .. _gallina-inductive-definitions: -Inductive definitions ---------------------- - -We gradually explain simple inductive types, simple annotated inductive -types, simple parametric inductive types, mutually inductive types. We -explain also co-inductive types. - -Simple inductive types -~~~~~~~~~~~~~~~~~~~~~~ +Inductive types +--------------- -.. cmd:: Inductive @ident : {? @sort } := {? | } @ident : @type {* | @ident : @type } - - This command defines a simple inductive type and its constructors. - The first :token:`ident` is the name of the inductively defined type - and :token:`sort` is the universe where it lives. The next :token:`ident`\s - are the names of its constructors and :token:`type` their respective types. - Depending on the universe where the inductive type :token:`ident` lives - (e.g. its type :token:`sort`), Coq provides a number of destructors. - Destructors are named :token:`ident`\ ``_sind``,:token:`ident`\ ``_ind``, - :token:`ident`\ ``_rec`` or :token:`ident`\ ``_rect`` which respectively - correspond to elimination principles on :g:`SProp`, :g:`Prop`, :g:`Set` and :g:`Type`. - The type of the destructors expresses structural induction/recursion - principles over objects of type :token:`ident`. - The constant :token:`ident`\ ``_ind`` is always provided, - whereas :token:`ident`\ ``_rec`` and :token:`ident`\ ``_rect`` can be - impossible to derive (for example, when :token:`ident` is a proposition). +.. cmd:: Inductive @inductive_definition {* with @inductive_definition } + + .. insertprodn inductive_definition constructor + + .. prodn:: + inductive_definition ::= {? > } @ident_decl {* @binder } {? %| {* @binder } } {? : @type } {? := {? @constructors_or_record } } {? @decl_notations } + constructors_or_record ::= {? %| } {+| @constructor } + | {? @ident } %{ {*; @record_field } %} + constructor ::= @ident {* @binder } {? @of_type } + + This command defines one or more + inductive types and its constructors. Coq generates destructors + depending on the universe that the inductive type belongs to. + + The destructors are named :n:`@ident`\ ``_rect``, :n:`@ident`\ ``_ind``, + :n:`@ident`\ ``_rec`` and :n:`@ident`\ ``_sind``, which + respectively correspond to elimination principles on :g:`Type`, :g:`Prop`, + :g:`Set` and :g:`SProp`. The type of the destructors + expresses structural induction/recursion principles over objects of + type :n:`@ident`. The constant :n:`@ident`\ ``_ind`` is always + generated, whereas :n:`@ident`\ ``_rec`` and :n:`@ident`\ ``_rect`` + may be impossible to derive (for example, when :n:`@ident` is a + proposition). + + This command supports the :attr:`universes(polymorphic)`, + :attr:`universes(monomorphic)`, :attr:`universes(template)`, + :attr:`universes(notemplate)`, :attr:`universes(cumulative)`, + :attr:`universes(noncumulative)` and :attr:`private(matching)` + attributes. + + Mutually inductive types can be defined by including multiple :n:`@inductive_definition`\s. + The :n:`@ident`\s are simultaneously added to the environment before the types of constructors are checked. + Each :n:`@ident` can be used independently thereafter. + See :ref:`mutually_inductive_types`. + + If the entire inductive definition is parameterized with :n:`@binder`\s, the parameters correspond + to a local context in which the entire set of inductive declarations is interpreted. + For this reason, the parameters must be strictly the same for each inductive type. + See :ref:`parametrized-inductive-types`. + + Constructor :n:`@ident`\s can come with :n:`@binder`\s, in which case + the actual type of the constructor is :n:`forall {* @binder }, @type`. .. exn:: Non strictly positive occurrence of @ident in @type. @@ -936,66 +850,71 @@ Simple inductive types .. exn:: The conclusion of @type is not valid; it must be built from @ident. The conclusion of the type of the constructors must be the inductive type - :token:`ident` being defined (or :token:`ident` applied to arguments in + :n:`@ident` being defined (or :n:`@ident` applied to arguments in the case of annotated inductive types — cf. next section). - .. example:: +The following subsections show examples of simple inductive types, +simple annotated inductive types, simple parametric inductive types, +mutually inductive types and private (matching) inductive types. - The set of natural numbers is defined as: +.. _simple-inductive-types: - .. coqtop:: all +Simple inductive types +~~~~~~~~~~~~~~~~~~~~~~ + +A simple inductive type belongs to a universe that is a simple :n:`@sort`. - Inductive nat : Set := - | O : nat - | S : nat -> nat. +.. example:: - The type nat is defined as the least :g:`Set` containing :g:`O` and closed by - the :g:`S` constructor. The names :g:`nat`, :g:`O` and :g:`S` are added to the - environment. + The set of natural numbers is defined as: - Now let us have a look at the elimination principles. They are three of them: - :g:`nat_ind`, :g:`nat_rec` and :g:`nat_rect`. The type of :g:`nat_ind` is: + .. coqtop:: reset all - .. coqtop:: all + Inductive nat : Set := + | O : nat + | S : nat -> nat. - Check nat_ind. + The type nat is defined as the least :g:`Set` containing :g:`O` and closed by + the :g:`S` constructor. The names :g:`nat`, :g:`O` and :g:`S` are added to the + environment. - This is the well known structural induction principle over natural - numbers, i.e. the second-order form of Peano’s induction principle. It - allows proving some universal property of natural numbers (:g:`forall - n:nat, P n`) by induction on :g:`n`. + This definition generates four elimination principles: + :g:`nat_rect`, :g:`nat_ind`, :g:`nat_rec` and :g:`nat_sind`. The type of :g:`nat_ind` is: - The types of :g:`nat_rec` and :g:`nat_rect` are similar, except that they pertain - to :g:`(P:nat->Set)` and :g:`(P:nat->Type)` respectively. They correspond to - primitive induction principles (allowing dependent types) respectively - over sorts ``Set`` and ``Type``. + .. coqtop:: all - .. cmdv:: Inductive @ident {? : @sort } := {? | } {*| @ident {? @binders } {? : @type } } + Check nat_ind. - Constructors :token:`ident`\s can come with :token:`binders` in which case, - the actual type of the constructor is :n:`forall @binders, @type`. + This is the well known structural induction principle over natural + numbers, i.e. the second-order form of Peano’s induction principle. It + allows proving universal properties of natural numbers (:g:`forall + n:nat, P n`) by induction on :g:`n`. - In the case where inductive types have no annotations (next section - gives an example of such annotations), a constructor can be defined - by only giving the type of its arguments. + The types of :g:`nat_rect`, :g:`nat_rec` and :g:`nat_sind` are similar, except that they + apply to, respectively, :g:`(P:nat->Type)`, :g:`(P:nat->Set)` and :g:`(P:nat->SProp)`. They correspond to + primitive induction principles (allowing dependent types) respectively + over sorts ```Type``, ``Set`` and ``SProp``. - .. example:: +In the case where inductive types don't have annotations (the next section +gives an example of annotations), a constructor can be defined +by giving the type of its arguments alone. - .. coqtop:: none +.. example:: - Reset nat. + .. coqtop:: reset none - .. coqtop:: in + Reset nat. - Inductive nat : Set := O | S (_:nat). + .. coqtop:: in + Inductive nat : Set := O | S (_:nat). Simple annotated inductive types ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -In an annotated inductive types, the universe where the inductive type -is defined is no longer a simple sort, but what is called an arity, -which is a type whose conclusion is a sort. +In annotated inductive types, the universe where the inductive type +is defined is no longer a simple :n:`@sort`, but what is called an arity, +which is a type whose conclusion is a :n:`@sort`. .. example:: @@ -1008,72 +927,74 @@ which is a type whose conclusion is a sort. | even_0 : even O | even_SS : forall n:nat, even n -> even (S (S n)). - The type :g:`nat->Prop` means that even is a unary predicate (inductively + The type :g:`nat->Prop` means that :g:`even` is a unary predicate (inductively defined) over natural numbers. The type of its two constructors are the - defining clauses of the predicate even. The type of :g:`even_ind` is: + defining clauses of the predicate :g:`even`. The type of :g:`even_ind` is: .. coqtop:: all Check even_ind. - From a mathematical point of view it asserts that the natural numbers satisfying - the predicate even are exactly in the smallest set of naturals satisfying the + From a mathematical point of view, this asserts that the natural numbers satisfying + the predicate :g:`even` are exactly in the smallest set of naturals satisfying the clauses :g:`even_0` or :g:`even_SS`. This is why, when we want to prove any predicate :g:`P` over elements of :g:`even`, it is enough to prove it for :g:`O` and to prove that if any natural number :g:`n` satisfies :g:`P` its double - successor :g:`(S (S n))` satisfies also :g:`P`. This is indeed analogous to the + successor :g:`(S (S n))` satisfies also :g:`P`. This is analogous to the structural induction principle we got for :g:`nat`. +.. _parametrized-inductive-types: + Parameterized inductive types ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. cmdv:: Inductive @ident @binders {? : @type } := {? | } @ident : @type {* | @ident : @type} +In the previous example, each constructor introduces a different +instance of the predicate :g:`even`. In some cases, all the constructors +introduce the same generic instance of the inductive definition, in +which case, instead of an annotation, we use a context of parameters +which are :n:`@binder`\s shared by all the constructors of the definition. - In the previous example, each constructor introduces a different - instance of the predicate :g:`even`. In some cases, all the constructors - introduce the same generic instance of the inductive definition, in - which case, instead of an annotation, we use a context of parameters - which are :token:`binders` shared by all the constructors of the definition. +Parameters differ from inductive type annotations in that the +conclusion of each type of constructor invokes the inductive type with +the same parameter values of its specification. - Parameters differ from inductive type annotations in the fact that the - conclusion of each type of constructor invoke the inductive type with - the same values of parameters as its specification. +.. example:: - .. example:: + A typical example is the definition of polymorphic lists: - A typical example is the definition of polymorphic lists: + .. coqtop:: all - .. coqtop:: in + Inductive list (A:Set) : Set := + | nil : list A + | cons : A -> list A -> list A. - Inductive list (A:Set) : Set := - | nil : list A - | cons : A -> list A -> list A. + In the type of :g:`nil` and :g:`cons`, we write ":g:`list A`" and not + just ":g:`list`". The constructors :g:`nil` and :g:`cons` have these types: - In the type of :g:`nil` and :g:`cons`, we write :g:`(list A)` and not - just :g:`list`. The constructors :g:`nil` and :g:`cons` will have respectively - types: + .. coqtop:: all - .. coqtop:: all + Check nil. + Check cons. - Check nil. - Check cons. + Observe that the destructors are also quantified with :g:`(A:Set)`, for example: - Types of destructors are also quantified with :g:`(A:Set)`. + .. coqtop:: all + + Check list_ind. - Once again, it is possible to specify only the type of the arguments - of the constructors, and to omit the type of the conclusion: + Once again, the types of the constructor arguments and of the conclusion can be omitted: - .. coqtop:: none + .. coqtop:: none - Reset list. + Reset list. - .. coqtop:: in + .. coqtop:: in - Inductive list (A:Set) : Set := nil | cons (_:A) (_:list A). + Inductive list (A:Set) : Set := nil | cons (_:A) (_:list A). .. note:: - + It is possible in the type of a constructor, to - invoke recursively the inductive definition on an argument which is not + + The constructor type can + recursively invoke the inductive definition on an argument which is not the parameter itself. One can define : @@ -1088,7 +1009,9 @@ Parameterized inductive types .. coqtop:: all reset - Inductive list2 (A:Set) : Set := nil2 | cons2 (_:A) (_:list2 (A*A)). + Inductive list2 (A:Set) : Set := + | nil2 + | cons2 (_:A) (_:list2 (A*A)). But the following definition will give an error: @@ -1132,45 +1055,31 @@ Parameterized inductive types | cons3 : A -> list3 -> list3. End list3. -.. seealso:: - Section :ref:`inductive-definitions` and the :tacn:`induction` tactic. + For finer control, you can use a ``|`` between the uniform and + the non-uniform parameters: -Variants -~~~~~~~~ + .. coqtop:: in reset -.. cmd:: Variant @ident @binders {? : @type } := {? | } @ident : @type {* | @ident : @type} + Inductive Acc {A:Type} (R:A->A->Prop) | (x:A) : Prop + := Acc_in : (forall y, R y x -> Acc y) -> Acc x. - 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 the :flag:`Nonrecursive Elimination Schemes` flag is on. + The flag can then be seen as deciding whether the ``|`` is at the + beginning (when the flag is unset) or at the end (when it is set) + of the parameters when not explicitly given. - .. exn:: The @num th argument of @ident must be @ident in @type. - :undocumented: +.. seealso:: + Section :ref:`inductive-definitions` and the :tacn:`induction` tactic. + +.. _mutually_inductive_types: Mutually defined inductive types ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. cmdv:: Inductive @ident {? : @type } := {? | } {*| @ident : @type } {* with {? | } {*| @ident {? : @type } } } - - This variant allows defining a block of mutually inductive types. - It has the same semantics as the above :cmd:`Inductive` definition for each - :token:`ident`. All :token:`ident` are simultaneously added to the environment. - Then well-typing of constructors can be checked. Each one of the :token:`ident` - can be used on its own. - - .. cmdv:: Inductive @ident @binders {? : @type } := {? | } {*| @ident : @type } {* with {? | } {*| @ident @binders {? : @type } } } +.. example:: Mutually defined inductive types - In this variant, the inductive definitions are parameterized - with :token:`binders`. However, parameters correspond to a local context - in which the whole set of inductive declarations is done. For this - reason, the parameters must be strictly the same for each inductive types. - -.. example:: - - The typical example of a mutual inductive data type is the one for trees and - forests. We assume given two types :g:`A` and :g:`B` as variables. It can - be declared the following way. + A typical example of mutually inductive data types is trees and + forests. We assume two types :g:`A` and :g:`B` that are given as variables. The types can + be declared like this: .. coqtop:: in @@ -1182,13 +1091,10 @@ Mutually defined inductive types | leaf : B -> forest | cons : tree -> forest -> forest. - This declaration generates automatically six induction principles. They are - respectively called :g:`tree_rec`, :g:`tree_ind`, :g:`tree_rect`, - :g:`forest_rec`, :g:`forest_ind`, :g:`forest_rect`. These ones are not the most - general ones but are just the induction principles corresponding to each - inductive part seen as a single inductive definition. + This declaration automatically generates eight induction principles. They are not the most + general principles, but they correspond to each inductive part seen as a single inductive definition. - To illustrate this point on our example, we give the types of :g:`tree_rec` + To illustrate this point on our example, here are the types of :g:`tree_rec` and :g:`forest_rec`. .. coqtop:: all @@ -1199,7 +1105,7 @@ Mutually defined inductive types Assume we want to parameterize our mutual inductive definitions with the two type variables :g:`A` and :g:`B`, the declaration should be - done the following way: + done as follows: .. coqdoc:: @@ -1218,10 +1124,59 @@ Mutually defined inductive types A generic command :cmd:`Scheme` is useful to build automatically various mutual induction principles. +Private (matching) inductive types +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. attr:: private(matching) + + This attribute can be used to forbid the use of the :g:`match` + construct on objects of this inductive type outside of the module + where it is defined. There is also a legacy syntax using the + ``Private`` prefix (cf. :n:`@legacy_attr`). + + The main use case of private (matching) inductive types is to emulate + quotient types / higher-order inductive types in projects such as + the `HoTT library <https://github.com/HoTT/HoTT>`_. + +.. example:: + + .. coqtop:: all + + Module Foo. + #[ private(matching) ] Inductive my_nat := my_O : my_nat | my_S : my_nat -> my_nat. + Check (fun x : my_nat => match x with my_O => true | my_S _ => false end). + End Foo. + Import Foo. + Fail Check (fun x : my_nat => match x with my_O => true | my_S _ => false end). + +Variants +~~~~~~~~ + +.. cmd:: Variant @variant_definition {* with @variant_definition } + + .. insertprodn variant_definition variant_definition + + .. prodn:: + variant_definition ::= @ident_decl {* @binder } {? %| {* @binder } } {? : @type } := {? %| } {+| @constructor } {? @decl_notations } + + The :cmd:`Variant` command is similar 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 the :flag:`Nonrecursive Elimination Schemes` flag is on. + + This command supports the :attr:`universes(polymorphic)`, + :attr:`universes(monomorphic)`, :attr:`universes(template)`, + :attr:`universes(notemplate)`, :attr:`universes(cumulative)`, + :attr:`universes(noncumulative)` and :attr:`private(matching)` + attributes. + + .. exn:: The @num th argument of @ident must be @ident in @type. + :undocumented: + .. _coinductive-types: Co-inductive types -~~~~~~~~~~~~~~~~~~ +------------------ The objects of an inductive type are well-founded with respect to the constructors of the type. In other words, such objects contain only a @@ -1231,7 +1186,7 @@ constructors. Infinite objects are introduced by a non-ending (but effective) process of construction, defined in terms of the constructors of the type. -.. cmd:: CoInductive @ident @binders {? : @type } := {? | } @ident : @type {* | @ident : @type} +.. cmd:: CoInductive @inductive_definition {* with @inductive_definition } This command introduces a co-inductive type. The syntax of the command is the same as the command :cmd:`Inductive`. @@ -1239,10 +1194,16 @@ of the type. type, since such principles only make sense for inductive types. For co-inductive types, the only elimination principle is case analysis. + This command supports the :attr:`universes(polymorphic)`, + :attr:`universes(monomorphic)`, :attr:`universes(template)`, + :attr:`universes(notemplate)`, :attr:`universes(cumulative)`, + :attr:`universes(noncumulative)` and :attr:`private(matching)` + attributes. + .. example:: - An example of a co-inductive type is the type of infinite sequences of - natural numbers, usually called streams. + The type of infinite sequences of natural numbers, usually called streams, + is an example of a co-inductive type. .. coqtop:: in @@ -1256,13 +1217,12 @@ of the type. Definition hd (x:Stream) := let (a,s) := x in a. Definition tl (x:Stream) := let (a,s) := x in s. -Definition of co-inductive predicates and blocks of mutually +Definitions of co-inductive predicates and blocks of mutually co-inductive definitions are also allowed. .. example:: - An example of a co-inductive predicate is the extensional equality on - streams: + The extensional equality on streams is an example of a co-inductive type: .. coqtop:: in @@ -1276,7 +1236,7 @@ co-inductive definitions are also allowed. objects in Section :ref:`cofixpoint`. Caveat -++++++ +~~~~~~ The ability to define co-inductive types by constructors, hereafter called *positive co-inductive types*, is known to break subject reduction. The story is @@ -1344,27 +1304,44 @@ constructions. .. _Fixpoint: -.. cmd:: Fixpoint @ident @binders {? {struct @ident} } {? : @type } := @term +.. cmd:: Fixpoint @fix_definition {* with @fix_definition } + + .. insertprodn fix_definition fix_definition + + .. prodn:: + fix_definition ::= @ident_decl {* @binder } {? @fixannot } {? : @type } {? := @term } {? @decl_notations } This command allows defining functions by pattern matching over inductive objects using a fixed point construction. The meaning of this declaration is - to define :token:`ident` a recursive function with arguments specified by - the :token:`binders` such that :token:`ident` applied to arguments - corresponding to these :token:`binders` has type :token:`type`, and is - equivalent to the expression :token:`term`. The type of :token:`ident` is - consequently :n:`forall @binders, @type` and its value is equivalent - to :n:`fun @binders => @term`. - - To be accepted, a :cmd:`Fixpoint` definition has to satisfy some syntactical + to define :n:`@ident` as a recursive function with arguments specified by + the :n:`@binder`\s such that :n:`@ident` applied to arguments + corresponding to these :n:`@binder`\s has type :n:`@type`, and is + equivalent to the expression :n:`@term`. The type of :n:`@ident` is + consequently :n:`forall {* @binder }, @type` and its value is equivalent + to :n:`fun {* @binder } => @term`. + + To be accepted, a :cmd:`Fixpoint` definition has to satisfy syntactical constraints on a special argument called the decreasing argument. They are needed to ensure that the :cmd:`Fixpoint` definition always terminates. - The point of the :n:`{struct @ident}` annotation is to let the user tell the - system which argument decreases along the recursive calls. + The point of the :n:`{struct @ident}` annotation (see :n:`@fixannot`) is to + let the user tell the system which argument decreases along the recursive calls. - The :n:`{struct @ident}` annotation may be left implicit, in this case the - system tries successively arguments from left to right until it finds one + The :n:`{struct @ident}` annotation may be left implicit, in which case the + system successively tries arguments from left to right until it finds one that satisfies the decreasing condition. + :cmd:`Fixpoint` without the :attr:`program` attribute does not support the + :n:`wf` or :n:`measure` clauses of :n:`@fixannot`. + + The :n:`with` clause allows simultaneously defining several mutual fixpoints. + It is especially useful when defining functions over mutually defined + inductive types. Example: :ref:`Mutual Fixpoints<example_mutual_fixpoints>`. + + If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. + This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic. + In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant + for which the computational behavior is relevant. See :ref:`proof-editing-mode`. + .. note:: + Some fixpoints may have several arguments that fit as decreasing @@ -1445,35 +1422,35 @@ constructions. end end. +.. _example_mutual_fixpoints: - .. cmdv:: Fixpoint @ident @binders {? {struct @ident} } {? : @type } := @term {* with @ident @binders {? : @type } := @term } - - This variant allows defining simultaneously several mutual fixpoints. - It is especially useful when defining functions over mutually defined - inductive types. - - .. example:: + .. example:: Mutual fixpoints - The size of trees and forests can be defined the following way: + The size of trees and forests can be defined the following way: - .. coqtop:: all + .. coqtop:: all - Fixpoint tree_size (t:tree) : nat := - match t with - | node a f => S (forest_size f) - end - with forest_size (f:forest) : nat := - match f with - | leaf b => 1 - | cons t f' => (tree_size t + forest_size f') - end. + Fixpoint tree_size (t:tree) : nat := + match t with + | node a f => S (forest_size f) + end + with forest_size (f:forest) : nat := + match f with + | leaf b => 1 + | cons t f' => (tree_size t + forest_size f') + end. .. _cofixpoint: Definitions of recursive objects in co-inductive types ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: CoFixpoint @ident {? @binders } {? : @type } := @term +.. cmd:: CoFixpoint @cofix_definition {* with @cofix_definition } + + .. insertprodn cofix_definition cofix_definition + + .. prodn:: + cofix_definition ::= @ident_decl {* @binder } {? : @type } {? := @term } {? @decl_notations } This command introduces a method for constructing an infinite object of a coinductive type. For example, the stream containing all natural numbers can @@ -1485,7 +1462,7 @@ Definitions of recursive objects in co-inductive types CoFixpoint from (n:nat) : Stream := Seq n (from (S n)). - Oppositely to recursive ones, there is no decreasing argument in a + Unlike recursive definitions, there is no decreasing argument in a co-recursive definition. To be admissible, a method of construction must provide at least one extra constructor of the infinite object for each iteration. A syntactical guard condition is imposed on co-recursive @@ -1514,10 +1491,58 @@ Definitions of recursive objects in co-inductive types Eval compute in (hd (from 0)). Eval compute in (tl (from 0)). - .. cmdv:: CoFixpoint @ident {? @binders } {? : @type } := @term {* with @ident {? @binders } : {? @type } := @term } + As in the :cmd:`Fixpoint` command, the :n:`with` clause allows simultaneously + defining several mutual cofixpoints. + + If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. + This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic. + In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant + for which the computational behavior is relevant. See :ref:`proof-editing-mode`. - As in the :cmd:`Fixpoint` command, it is possible to introduce a block of - mutually dependent methods. +.. _Computations: + +Computations +------------ + +.. insertprodn reduce pattern_occ + +.. prodn:: + reduce ::= Eval @red_expr in + red_expr ::= red + | hnf + | simpl {? @delta_flag } {? @ref_or_pattern_occ } + | cbv {? @strategy_flag } + | cbn {? @strategy_flag } + | lazy {? @strategy_flag } + | compute {? @delta_flag } + | vm_compute {? @ref_or_pattern_occ } + | native_compute {? @ref_or_pattern_occ } + | unfold {+, @unfold_occ } + | fold {+ @one_term } + | pattern {+, @pattern_occ } + | @ident + delta_flag ::= {? - } [ {+ @smart_qualid } ] + strategy_flag ::= {+ @red_flags } + | @delta_flag + red_flags ::= beta + | iota + | match + | fix + | cofix + | zeta + | delta {? @delta_flag } + ref_or_pattern_occ ::= @smart_qualid {? at @occs_nums } + | @one_term {? at @occs_nums } + occs_nums ::= {+ {| @num | @ident } } + | - {| @num | @ident } {* @int_or_var } + int_or_var ::= @int + | @ident + unfold_occ ::= @smart_qualid {? at @occs_nums } + pattern_occ ::= @one_term {? at @occs_nums } + +See :ref:`Conversion-rules`. + +.. todo:: Add text here .. _Assertions: @@ -1529,40 +1554,26 @@ inhabitant of the type) is interactively built using tactics. The interactive proof mode is described in Chapter :ref:`proofhandling` and the tactics in Chapter :ref:`Tactics`. The basic assertion command is: -.. cmd:: Theorem @ident {? @binders } : @type +.. cmd:: @thm_token @ident_decl {* @binder } : @type {* with @ident_decl {* @binder } : @type } + :name: Theorem; Lemma; Fact; Remark; Corollary; Proposition; Property - After the statement is asserted, Coq needs a proof. Once a proof of - :token:`type` under the assumptions represented by :token:`binders` is given and - validated, the proof is generalized into a proof of :n:`forall @binders, @type` and - the theorem is bound to the name :token:`ident` in the environment. + .. insertprodn thm_token thm_token - .. exn:: The term @term has type @type which should be Set, Prop or Type. - :undocumented: - - .. exn:: @ident already exists. - :name: @ident already exists. (Theorem) + .. prodn:: + thm_token ::= Theorem + | Lemma + | Fact + | Remark + | Corollary + | Proposition + | Property - The name you provided is already defined. You have then to choose - another name. - - .. 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 the :flag:`Nested Proofs Allowed` flag on. - - .. cmdv:: Lemma @ident {? @binders } : @type - Remark @ident {? @binders } : @type - Fact @ident {? @binders } : @type - Corollary @ident {? @binders } : @type - Proposition @ident {? @binders } : @type - :name: Lemma; Remark; Fact; Corollary; Proposition - - These commands are all synonyms of :n:`Theorem @ident {? @binders } : type`. - -.. cmdv:: Theorem @ident {? @binders } : @type {* with @ident {? @binders } : @type} + After the statement is asserted, Coq needs a proof. Once a proof of + :n:`@type` under the assumptions represented by :n:`@binder`\s is given and + validated, the proof is generalized into a proof of :n:`forall {* @binder }, @type` and + the theorem is bound to the name :n:`@ident` in the environment. - This command is useful for theorems that are proved by simultaneous induction + Forms using the :n:`with` clause are useful for theorems that are proved by simultaneous induction over a mutually inductive assumption, or that assert mutually dependent statements in some mutual co-inductive type. It is equivalent to :cmd:`Fixpoint` or :cmd:`CoFixpoint` but using tactics to build the proof of @@ -1579,46 +1590,29 @@ Chapter :ref:`Tactics`. The basic assertion command is: correct at some time of the interactive development of a proof, use the command :cmd:`Guarded`. - The command can be used also with :cmd:`Lemma`, :cmd:`Remark`, etc. instead of - :cmd:`Theorem`. - -.. cmdv:: Definition @ident {? @binders } : @type - - This allows defining a term of type :token:`type` using the proof editing - mode. It behaves as :cmd:`Theorem` but is intended to be used in conjunction with - :cmd:`Defined` in order to define a constant of which the computational - behavior is relevant. - - The command can be used also with :cmd:`Example` instead of :cmd:`Definition`. - - .. seealso:: :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`. - -.. cmdv:: Let @ident {? @binders } : @type - - Like :n:`Definition @ident {? @binders } : @type` except that the definition is - turned into a let-in definition generalized over the declarations depending - on it after closing the current section. + .. exn:: The term @term has type @type which should be Set, Prop or Type. + :undocumented: -.. cmdv:: Fixpoint @ident @binders : @type {* with @ident @binders : @type} + .. exn:: @ident already exists. + :name: @ident already exists. (Theorem) - This generalizes the syntax of :cmd:`Fixpoint` so that one or more bodies - can be defined interactively using the proof editing mode (when a - body is omitted, its type is mandatory in the syntax). When the block - of proofs is completed, it is intended to be ended by :cmd:`Defined`. + The name you provided is already defined. You have then to choose + another name. -.. cmdv:: CoFixpoint @ident {? @binders } : @type {* with @ident {? @binders } : @type} + .. exn:: Nested proofs are not allowed unless you turn the Nested Proofs Allowed flag on. - This generalizes the syntax of :cmd:`CoFixpoint` so that one or more bodies - can be defined interactively using the proof editing mode. + 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 the :flag:`Nested Proofs Allowed` flag on. -A proof starts by the keyword :cmd:`Proof`. Then Coq enters the proof editing mode -until the proof is completed. The proof editing mode essentially contains -tactics that are described in chapter :ref:`Tactics`. Besides tactics, there -are commands to manage the proof editing mode. They are described in Chapter +Proofs start with the keyword :cmd:`Proof`. Then Coq enters the proof editing mode +until the proof is completed. In proof editing mode, the user primarily enters +tactics, which are described in chapter :ref:`Tactics`. The user may also enter +commands to manage the proof editing mode. They are described in Chapter :ref:`proofhandling`. -When the proof is completed it should be validated and put in the environment -using the keyword :cmd:`Qed`. +When the proof is complete, use the :cmd:`Qed` command so the kernel verifies +the proof and adds it to the environment. .. note:: @@ -1647,67 +1641,71 @@ using the keyword :cmd:`Qed`. Attributes ----------- -Any vernacular command can be decorated with a list of attributes, enclosed -between ``#[`` (hash and opening square bracket) and ``]`` (closing square bracket) -and separated by commas ``,``. Multiple space-separated blocks may be provided. - -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. - -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: - -``universes(monomorphic)``, ``universes(polymorphic)`` - Equivalent to the ``Monomorphic`` and - ``Polymorphic`` flags (see :ref:`polymorphicuniverses`). - -``program`` - Takes no value, equivalent to the ``Program`` flag - (see :ref:`programs`). - -``global``, ``local`` - Take no value, equivalent to the ``Global`` and ``Local`` flags - (see :ref:`controlling-locality-of-commands`). - -``deprecated`` - Takes as value the optional attributes ``since`` and ``note``; - both have a string value. +.. insertprodn all_attrs legacy_attr + +.. prodn:: + all_attrs ::= {* #[ {*, @attr } ] } {* @legacy_attr } + attr ::= @ident {? @attr_value } + attr_value ::= = @string + | ( {*, @attr } ) + legacy_attr ::= {| Local | Global } + | {| Polymorphic | Monomorphic } + | {| Cumulative | NonCumulative } + | Private + | Program + +Attributes modify the behavior of a command or tactic. +Syntactically, most commands and tactics can be decorated with attributes, but +attributes not supported by the command or tactic will be flagged as errors. + +The order of top-level attributes doesn't affect their meaning. ``#[foo,bar]``, ``#[bar,foo]``, +``#[foo]#[bar]`` and ``#[bar]#[foo]`` are equivalent. + +The legacy attributes (:n:`@legacy_attr`) provide an older, alternate syntax +for certain attributes. They are equivalent to new attributes as follows: + +================ ================================ +Legacy attribute New attribute +================ ================================ +`Local` :attr:`local` +`Global` :attr:`global` +`Polymorphic` :attr:`universes(polymorphic)` +`Monomorphic` :attr:`universes(monomorphic)` +`Cumulative` :attr:`universes(cumulative)` +`NonCumulative` :attr:`universes(noncumulative)` +`Private` :attr:`private(matching)` +`Program` :attr:`program` +================ ================================ + +.. attr:: deprecated ( {? since = @string , } {? note = @string } ) + :name: deprecated + + At least one of :n:`since` or :n:`note` must be present. If both are present, + either one may appear first and they must be separated by a comma. This attribute is supported by the following commands: :cmd:`Ltac`, :cmd:`Tactic Notation`, :cmd:`Notation`, :cmd:`Infix`. It can trigger the following warnings: - .. warn:: Tactic @qualid is deprecated since @string. @string. - :undocumented: + .. warn:: Tactic @qualid is deprecated since @string__since. @string__note. + Tactic Notation @qualid is deprecated since @string__since. @string__note. + Notation @string is deprecated since @string__since. @string__note. - .. warn:: Tactic Notation @qualid is deprecated since @string. @string. - :undocumented: + :n:`@qualid` or :n:`@string` is the notation, :n:`@string__since` is the version number, + :n:`@string__note` is the note (usually explains the replacement). - .. warn:: Notation @string__1 is deprecated since @string__2. @string__3. + .. example:: - :n:`@string__1` is the actual notation, :n:`@string__2` is the version number, - :n:`@string__3` is the note. + .. coqtop:: all reset warn -.. example:: - - .. coqtop:: all reset warn - - From Coq Require Program. - #[program] Definition one : nat := S _. - Next Obligation. - exact O. - Defined. + #[deprecated(since="8.9.0", note="Use idtac instead.")] + Ltac foo := idtac. - #[deprecated(since="8.9.0", note="Use idtac instead.")] - Ltac foo := idtac. - - Goal True. - Proof. + Goal True. + Proof. now foo. - Abort. + Abort. .. warn:: Unsupported attribute @@ -1715,10 +1713,5 @@ variety of commands: 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* - :math:`)`\ \*” in the syntax of regular expressions. - -.. [2] Except if the inductive type is empty in which case there is no equation that can be used to infer the return type. diff --git a/doc/sphinx/license.rst b/doc/sphinx/license.rst index 55c6d988f0..35837f8407 100644 --- a/doc/sphinx/license.rst +++ b/doc/sphinx/license.rst @@ -1,7 +1,7 @@ -License -------- +.. note:: **License** -This material (the Coq Reference Manual) may be distributed only subject to the -terms and conditions set forth in the Open Publication License, v1.0 or later -(the latest version is presently available at -http://www.opencontent.org/openpub). Options A and B are not elected. + This material (the Coq Reference Manual) may be distributed only + subject to the terms and conditions set forth in the Open + Publication License, v1.0 or later (the latest version is presently + available at http://www.opencontent.org/openpub). Options A and B + are not elected. diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index d4a61425e1..aa4b6edd7d 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -157,8 +157,6 @@ and ``coqtop``, unless stated otherwise: loading the default resource file from the standard configuration directories. :-q: Do not to load the default resource file. -:-load-ml-source *file*: Load the OCaml source file *file*. -:-load-ml-object *file*: Load the OCaml object file *file*. :-l *file*, -load-vernac-source *file*: Load and execute the |Coq| script from *file.v*. :-lv *file*, -load-vernac-source-verbose *file*: Load and execute the @@ -229,7 +227,10 @@ and ``coqtop``, unless stated otherwise: type of the option. For flags ``Option Name`` is equivalent to ``Option Name=true``. For instance ``-set "Universe Polymorphism"`` will enable :flag:`Universe Polymorphism`. Note that the quotes are - shell syntax, Coq does not see them. + shell syntax, Coq does not see them. Flags are processed after initialization + of the document. This includes the `Prelude` if loaded and any libraries loaded + through the `-l`, `-lv`, `-r`, `-re`, `-ri`, `rfrom`, `-refrom` and `-rifrom` + options. :-unset *string*: As ``-set`` but used to disable options and flags. :-compat *version*: Attempt to maintain some backward-compatibility with a previous version. @@ -253,6 +254,7 @@ and ``coqtop``, unless stated otherwise: :-h, --help: Print a short usage and exit. +.. _compiled-interfaces: Compiled interfaces (produced using ``-vos``) ---------------------------------------------- diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index e5edd08995..e5ff26520a 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -255,14 +255,20 @@ file timing data: one, you can pass them via the variable ``TGTS``, e.g., ``make pretty-timed TGTS="a.vo b.vo"``. - .. :: + .. note:: This target requires ``python`` to build the table. .. note:: This target will *append* to the timing log; if you want a - fresh start, you must remove the ``filetime-of-build.log`` or + fresh start, you must remove the file ``time-of-build.log`` or ``run make cleanall``. + .. note:: + By default the table displays user times. If the build log + contains real times (which it does by default), passing + ``TIMING_REAL=1`` to ``make pretty-timed`` will use real times + rather than user times in the table. + .. example:: For example, the output of ``make pretty-timed`` may look like this: @@ -310,6 +316,15 @@ file timing data: (which are frequently noise); lexicographic sorting forces an order on files which take effectively no time to compile. + If you prefer a different sorting order, you can pass + ``TIMING_SORT_BY=absolute`` to sort by the total time taken, or + ``TIMING_SORT_BY=diff`` to sort by the signed difference in + time. + + .. note:: + Just like ``pretty-timed``, this table defaults to using user + times. Pass ``TIMING_REAL=1`` to ``make`` on the command line to show real times instead. + .. example:: For example, the output table from @@ -349,7 +364,7 @@ line timing data: :: - print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing + print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing this target will make a sorted table of the per-line timing differences between the timing logs in the ``BEFORE`` and ``AFTER`` files, display it, and @@ -364,6 +379,28 @@ line timing data: .. note:: This target requires python to build the table. + .. note:: + This target follows the same sorting order as the + ``print-pretty-timed-diff`` target, and supports the same + options for the ``TIMING_SORT_BY`` variable. + + .. note:: + By default, two lines are only considered the same if the + character offsets and initial code strings are identical. Passing + ``TIMING_FUZZ=N`` relaxes this constraint by allowing the + character locations to differ by up to ``N``, as long + as the total number of characters and initial code strings + continue to match. This is useful when there are small changes + to a file, and you want to match later lines that have not + changed even though the character offsets have changed. + + .. note:: + By default the table picks up real times, under the assumption + that when comparing line-by-line, the real time is a more + accurate representation as it includes disk time and time spent + in the native compiler. Passing ``TIMING_REAL=0`` to ``make`` + will use user times rather than real times in the table. + .. example:: For example, running ``print-pretty-single-time-diff`` might give a table like this: @@ -462,40 +499,81 @@ To build, say, two targets foo.vo and bar.vo in parallel one can use (``.PHONY`` or not) please use ``CoqMakefile.local``. +Precompiling for ``native_compute`` ++++++++++++++++++++++++++++++++++++ + +To compile files for ``native_compute``, one can use the +``-native-compiler yes`` option of |Coq|, for instance by putting the +following in a :ref:`coqmakefilelocal` file: + +:: + + COQEXTRAFLAGS += -native-compiler yes + +The generated ``CoqMakefile`` installation target will then take care +of installing the extra ``.coq-native`` directories. + +.. note:: + + As an alternative to modifying any file, one can set the + environment variable when calling ``make``: + + :: + + COQEXTRAFLAGS="-native-compiler yes" make + + This can be useful when files cannot be modified, for instance when + installing via OPAM a package built with ``coq_makefile``: + + :: + + COQEXTRAFLAGS="-native-compiler yes" opam install coq-package + +.. note:: + + This requires all dependencies to be themselves compiled with + ``-native-compiler yes``. Building a |Coq| project with Dune ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. note:: + Dune's Coq support is still experimental; we strongly recommend + using Dune 2.3 or later. + +.. note:: + The canonical documentation for the Coq Dune extension is maintained upstream; please refer to the `Dune manual - <https://dune.readthedocs.io/>`_ for up-to-date information. + <https://dune.readthedocs.io/>`_ for up-to-date information. This + documentation is up to date for Dune 2.3. Building a Coq project with Dune requires setting up a Dune project for your files. This involves adding a ``dune-project`` and -``pkg.opam`` file to the root (``pkg.opam`` can be empty), and then -providing ``dune`` files in the directories your ``.v`` files are -placed. For the experimental version "0.1" of the Coq Dune language, -|Coq| library stanzas look like: +``pkg.opam`` file to the root (``pkg.opam`` can be empty or generated +by Dune itself), and then providing ``dune`` files in the directories +your ``.v`` files are placed. For the experimental version "0.1" of +the Coq Dune language, |Coq| library stanzas look like: .. code:: scheme - (coqlib + (coq.theory (name <module_prefix>) - (public_name <package.lib_name>) + (package <opam_package>) (synopsis <text>) (modules <ordered_set_lang>) (libraries <ocaml_libraries>) (flags <coq_flags>)) This stanza will build all `.v` files in the given directory, wrapping -the library under ``<module_prefix>``. If you declare a -``<package.lib_name>`` a ``.install`` file for the library will be -generated; the optional ``<modules>`` field allows you to filter -the list of modules, and ``<libraries>`` allows to depend on ML -plugins. For the moment, Dune relies on Coq's standard mechanisms -(such as ``COQPATH``) to locate installed Coq libraries. +the library under ``<module_prefix>``. If you declare an +``<opam_package>``, an ``.install`` file for the library will be +generated; the optional ``(modules <ordered_set_lang>)`` field allows +you to filter the list of modules, and ``(libraries +<ocaml_libraries>)`` allows the Coq theory depend on ML plugins. For +the moment, Dune relies on Coq's standard mechanisms (such as +``COQPATH``) to locate installed Coq libraries. By default Dune will skip ``.v`` files present in subdirectories. In order to enable the usual recursive organization of Coq projects add @@ -528,9 +606,9 @@ of your project. .. code:: scheme - (coqlib + (coq.theory (name Equations) ; -R flag - (public_name equations.Equations) + (package equations) (synopsis "Equations Plugin") (libraries coq.plugins.extraction equations.plugin) (modules :standard \ IdDec NoCycle)) ; exclude some modules that don't build @@ -545,7 +623,7 @@ Computing Module dependencies In order to compute module dependencies (to be used by ``make`` or ``dune``), |Coq| provides the ``coqdep`` tool. -``coqdep`` computes inter-module dependencies for |Coq| and |OCaml| +``coqdep`` computes inter-module dependencies for |Coq| programs, and prints the dependencies on the standard output in a format readable by make. When a directory is given as argument, it is recursively looked at. @@ -554,11 +632,6 @@ Dependencies of |Coq| modules are computed by looking at ``Require`` commands (``Require``, ``Require Export``, ``Require Import``), but also at the command ``Declare ML Module``. -Dependencies of |OCaml| modules are computed by looking at -`open` commands and the dot notation *module.value*. However, this is -done approximately and you are advised to use ``ocamldep`` instead for the -|OCaml| module dependencies. - See the man page of ``coqdep`` for more details and options. Both Dune and ``coq_makefile`` use ``coqdep`` to compute the diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index cfdc70d50e..06106a6b4c 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -1,9 +1,5 @@ .. _ltac2: -.. coqtop:: none - - From Ltac2 Require Import Ltac2. - Ltac2 ===== @@ -88,6 +84,12 @@ which allows to ensure that Ltac2 satisfies the same equations as a generic ML with unspecified effects would do, e.g. function reduction is substitution by a value. +To import Ltac2, use the following command: + +.. coqtop:: in + + From Ltac2 Require Import Ltac2. + Type Syntax ~~~~~~~~~~~ @@ -907,9 +909,9 @@ Ltac2 from Ltac1 Same as above by switching Ltac1 by Ltac2 and using the `ltac2` quotation instead. -.. productionlist:: coq - ltac_expr : ltac2 : ( `ltac2_term` ) - : ltac2 : ( `ident` ... `ident` |- `ltac2_term` ) +.. prodn:: + ltac_expr += ltac2 : ( `ltac2_term` ) + | ltac2 : ( `ident` ... `ident` |- `ltac2_term` ) The typing rules are dual, that is, the optional identifiers are bound with type `Ltac2.Ltac1.t` in the Ltac2 expression, which is expected to have @@ -940,6 +942,13 @@ below will fail immediately and won't print anything. In any case, the value returned by the fully applied quotation is an unspecified dummy Ltac1 closure and should not be further used. +Switching between Ltac languages +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +We recommend using the :opt:`Default Proof Mode` option to switch between tactic +languages with a proof-based granularity. This allows to incrementally port +the proof scripts. + Transition from Ltac1 --------------------- diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 6884b6e998..03eebc32f9 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -80,20 +80,19 @@ list of assertion commands is given in :ref:`Assertions`. The command a while when the proof is large. In some exceptional cases one may even incur a memory overflow. - .. cmdv:: Defined - :name: Defined +.. cmd:: Defined - Same as :cmd:`Qed` but the proof is then declared transparent, which means - that its content can be explicitly used for type checking and that it can be - unfolded in conversion tactics (see :ref:`performingcomputations`, - :cmd:`Opaque`, :cmd:`Transparent`). + Same as :cmd:`Qed`, except the proof is made *transparent*, which means + that its content can be explicitly used for type checking and that it can be + unfolded in conversion tactics (see :ref:`performingcomputations`, + :cmd:`Opaque`, :cmd:`Transparent`). - .. cmdv:: Save @ident - :name: Save +.. cmd:: Save @ident + :name: Save - Forces the name of the original goal to be :token:`ident`. This - command (and the following ones) can only be used if the original goal - has been opened using the :cmd:`Goal` command. + Forces the name of the original goal to be :token:`ident`. This + command can only be used if the original goal + was opened using the :cmd:`Goal` command. .. cmd:: Admitted @@ -265,6 +264,35 @@ Name a set of section hypotheses for ``Proof using`` has remaining uninstantiated existential variables. It takes every uninstantiated existential variable and turns it into a goal. +Proof modes +``````````` + +When entering proof mode through commands such as :cmd:`Goal` and :cmd:`Proof`, +|Coq| picks by default the |Ltac| mode. Nonetheless, there exist other proof modes +shipped in the standard |Coq| installation, and furthermore some plugins define +their own proof modes. The default proof mode used when opening a proof can +be changed using the following option. + +.. opt:: Default Proof Mode @string + :name: Default Proof Mode + + Select the proof mode to use when starting a proof. Depending on the proof + mode, various syntactic constructs are allowed when writing an interactive + proof. The possible option values are listed below. + + - "Classic": this is the default. It activates the |Ltac| language to interact + with the proof, and also allows vernacular commands. + + - "Noedit": this proof mode only allows vernacular commands. No tactic + language is activated at all. This is the default when the prelude is not + loaded, e.g. through the `-noinit` option for `coqc`. + + - "Ltac2": this proof mode is made available when requiring the Ltac2 + library, and is set to be the default when it is imported. It allows + to use the Ltac2 language, as well as vernacular commands. + + - Some external plugins also define their own proof mode, which can be + activated via this command. Navigation in the proof tree -------------------------------- @@ -490,6 +518,13 @@ The following example script illustrates all these features: You just finished a goal focused by ``{``, you must unfocus it with ``}``. +Mandatory Bullets +````````````````` + +Using :opt:`Default Goal Selector` with the ``!`` selector forces +tactic scripts to keep focus to exactly one goal (e.g. using bullets) +or use explicit goal selectors. + Set Bullet Behavior ``````````````````` .. opt:: Bullet Behavior {| "None" | "Strict Subproofs" } diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 853ddfd6dc..90a991794f 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1702,7 +1702,7 @@ Intro patterns when it is the very *first* :token:`i_pattern` after tactic ``=>`` tactical *and* tactic is not a move, is a *branching*:token:`i_pattern`. It executes the sequence - :token:`i_item`:math:`_i` on the i-th subgoal produced by tactic. The + :n:`@i_item__i` on the i-th subgoal produced by tactic. The execution of tactic should thus generate exactly m subgoals, unless the ``[…]`` :token:`i_pattern` comes after an initial ``//`` or ``//=`` :token:`s_item` that closes some of the goals produced by ``tactic``, in @@ -2222,14 +2222,14 @@ tactics to *permute* the subgoals generated by a tactic. If :token:`num`\'s value is :math:`k`, this tactic rotates the :math:`n` subgoals :math:`G_1` , …, :math:`G_n` - in focus. The first subgoal becomes :math:`G_{n + 1 − k}` and the + in focus. Subgoal :math:`G_{n + 1 − k}` becomes the first, and the circular order of subgoals remains unchanged. .. tacn:: first @num last If :token:`num`\'s value is :math:`k`, this tactic rotates the :math:`n` subgoals :math:`G_1` , …, :math:`G_n` - in focus. The first subgoal becomes :math:`G_k` and the circular order + in focus. Subgoal :math:`G_{k + 1 \bmod n}` becomes the first, and the circular order of subgoals remains unchanged. Finally, the tactics ``last`` and ``first`` combine with the branching syntax diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 878118c48a..19573eee43 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -72,7 +72,7 @@ specified, the default selector is used. .. _bindingslist: Bindings list -~~~~~~~~~~~~~~~~~~~ +~~~~~~~~~~~~~ Tactics that take a term as an argument may also support a bindings list to instantiate some parameters of the term by name or position. @@ -275,7 +275,7 @@ These patterns can be used when the hypothesis is an equality: :n:`or` has multiple constructors (:n:`or_introl` and :n:`or_intror`), while :n:`and` has a single constructor (:n:`conj`) with multiple parameters (:n:`A` and :n:`B`). - These are defined in theories/Init/Logic.v. The "where" clauses define the + These are defined in ``theories/Init/Logic.v``. The "where" clauses define the infix notation for "or" and "and". .. coqdoc:: @@ -688,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 @@ -1259,16 +1281,16 @@ Managing the local context is an occurrence clause whose syntax and behavior are described in :ref:`goal occurrences <occurrencessets>`. - .. tacv:: set (@ident @binders := @term) {? in @goal_occurrences } + .. tacv:: set (@ident {* @binder } := @term) {? in @goal_occurrences } - This is equivalent to :n:`set (@ident := fun @binders => @term) {? in @goal_occurrences }`. + This is equivalent to :n:`set (@ident := fun {* @binder } => @term) {? in @goal_occurrences }`. .. tacv:: set @term {? in @goal_occurrences } This behaves as :n:`set (@ident := @term) {? in @goal_occurrences }` but :token:`ident` is generated by Coq. - .. tacv:: eset (@ident {? @binders } := @term) {? in @goal_occurrences } + .. tacv:: eset (@ident {* @binder } := @term) {? in @goal_occurrences } eset @term {? in @goal_occurrences } :name: eset; _ @@ -1304,16 +1326,16 @@ Managing the local context without performing any replacement in the goal or in the hypotheses. It is equivalent to :n:`set (@ident := @term) in |-`. - .. tacv:: pose (@ident @binders := @term) + .. tacv:: pose (@ident {* @binder } := @term) - This is equivalent to :n:`pose (@ident := fun @binders => @term)`. + This is equivalent to :n:`pose (@ident := fun {* @binder } => @term)`. .. tacv:: pose @term This behaves as :n:`pose (@ident := @term)` but :token:`ident` is generated by Coq. - .. tacv:: epose (@ident {? @binders} := @term) + .. tacv:: epose (@ident {* @binder } := @term) epose @term :name: epose; _ @@ -1430,6 +1452,19 @@ Controlling the proof flow While :tacn:`pose proof` expects that no existential variables are generated by the tactic, :tacn:`epose proof` removes this constraint. +.. tacv:: pose proof (@ident := @term) + + This is an alternative syntax for :n:`assert (@ident := @term)` and + :n:`pose proof @term as @ident`, following the model of :n:`pose + (@ident := @term)` but dropping the value of :token:`ident`. + +.. tacv:: epose proof (@ident := @term) + + This is an alternative syntax for :n:`eassert (@ident := @term)` + and :n:`epose proof @term as @ident`, following the model of + :n:`epose (@ident := @term)` but dropping the value of + :token:`ident`. + .. tacv:: enough (@ident : @type) :name: enough @@ -3091,6 +3126,12 @@ the conversion in hypotheses :n:`{+ @ident}`. compilation cost is higher, so it is worth using only for intensive computations. + .. flag:: NativeCompute Timing + + This flag causes all calls to the native compiler to print + timing information for the compilation, execution, and + reification phases of native compilation. + .. flag:: NativeCompute Profiling On Linux, if you have the ``perf`` profiler installed, this flag makes @@ -3181,7 +3222,7 @@ the conversion in hypotheses :n:`{+ @ident}`. + A constant can be marked to be unfolded only if applied to enough arguments. The number of arguments required can be specified using the - ``/`` symbol in the argument list of the :cmd:`Arguments <Arguments (implicits)>` vernacular command. + ``/`` symbol in the argument list of the :cmd:`Arguments` command. .. example:: @@ -3718,6 +3759,24 @@ automatically created. .. cmd:: Hint @hint_definition : {+ @ident} The general command to add a hint to some databases :n:`{+ @ident}`. + + This command supports the :attr:`local`, :attr:`global` and :attr:`export` + locality attributes. When no locality is explictly given, the + command is :attr:`local` inside a section and :attr:`global` otherwise. + + + :attr:`local` hints are never visible from other modules, even if they + require or import the current module. Inside a section, the :attr:`local` + attribute is useless since hints do not survive anyway to the closure of + sections. + + + :attr:`export` are visible from other modules when they import the current + module. Requiring it is not enough. This attribute is only effective for + the :cmd:`Hint Resolve`, :cmd:`Hint Immediate`, :cmd:`Hint Unfold` and + :cmd:`Hint Extern` variants of the command. + + + :attr:`global` hints are made available by merely requiring the current + module. + The various possible :production:`hint_definition`\s are given below. .. cmdv:: Hint @hint_definition @@ -3726,25 +3785,18 @@ automatically created. .. deprecated:: 8.10 - .. 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 flag - Local is useless since hints do not survive anyway to the closure of - sections. - - .. cmdv:: Hint Resolve @term {? | {? @num} {? @pattern}} : @ident + .. cmdv:: Hint Resolve @qualid {? | {? @num} {? @pattern}} : @ident :name: Hint Resolve - This command adds :n:`simple apply @term` to the hint list with the head - symbol of the type of :n:`@term`. The cost of that hint is the number of - subgoals generated by :n:`simple apply @term` or :n:`@num` if specified. The + This command adds :n:`simple apply @qualid` to the hint list with the head + symbol of the type of :n:`@qualid`. The cost of that hint is the number of + subgoals generated by :n:`simple apply @qualid` or :n:`@num` if specified. The associated :n:`@pattern` is inferred from the conclusion of the type of - :n:`@term` or the given :n:`@pattern` if specified. In case the inferred type - of :n:`@term` does not start with a product the tactic added in the hint list - is :n:`exact @term`. In case this type can however be reduced to a type - starting with a product, the tactic :n:`simple apply @term` is also stored in - the hints list. If the inferred type of :n:`@term` contains a dependent + :n:`@qualid` or the given :n:`@pattern` if specified. In case the inferred type + of :n:`@qualid` does not start with a product the tactic added in the hint list + is :n:`exact @qualid`. In case this type can however be reduced to a type + starting with a product, the tactic :n:`simple apply @qualid` is also stored in + the hints list. If the inferred type of :n:`@qualid` contains a dependent quantification on a variable which occurs only in the premisses of the type and not in its conclusion, no instance could be inferred for the variable by unification with the goal. In this case, the hint is added to the hint list @@ -3752,32 +3804,32 @@ automatically created. typical example of a hint that is used only by :tacn:`eauto` is a transitivity lemma. - .. exn:: @term cannot be used as a hint + .. exn:: @qualid cannot be used as a hint - The head symbol of the type of :n:`@term` is a bound variable + The head symbol of the type of :n:`@qualid` is a bound variable such that this tactic cannot be associated to a constant. - .. cmdv:: Hint Resolve {+ @term} : @ident + .. cmdv:: Hint Resolve {+ @qualid} : @ident - Adds each :n:`Hint Resolve @term`. + Adds each :n:`Hint Resolve @qualid`. - .. cmdv:: Hint Resolve -> @term : @ident + .. cmdv:: Hint Resolve -> @qualid : @ident Adds the left-to-right implication of an equivalence as a hint (informally - the hint will be used as :n:`apply <- @term`, although as mentioned + the hint will be used as :n:`apply <- @qualid`, although as mentioned before, the tactic actually used is a restricted version of :tacn:`apply`). - .. cmdv:: Hint Resolve <- @term + .. cmdv:: Hint Resolve <- @qualid Adds the right-to-left implication of an equivalence as a hint. - .. cmdv:: Hint Immediate @term : @ident + .. cmdv:: Hint Immediate @qualid : @ident :name: Hint Immediate - This command adds :n:`simple apply @term; trivial` to the hint list associated + This command adds :n:`simple apply @qualid; trivial` to the hint list associated with the head symbol of the type of :n:`@ident` in the given database. This - tactic will fail if all the subgoals generated by :n:`simple apply @term` are + tactic will fail if all the subgoals generated by :n:`simple apply @qualid` are not solved immediately by the :tacn:`trivial` tactic (which only tries tactics with cost 0).This command is useful for theorems such as the symmetry of equality or :g:`n+1=m+1 -> n=m` that we may like to introduce with a limited @@ -3785,12 +3837,12 @@ automatically created. never generates subgoals) is always 1, so that it is not used by :tacn:`trivial` itself. - .. exn:: @term cannot be used as a hint + .. exn:: @qualid cannot be used as a hint :undocumented: - .. cmdv:: Hint Immediate {+ @term} : @ident + .. cmdv:: Hint Immediate {+ @qualid} : @ident - Adds each :n:`Hint Immediate @term`. + Adds each :n:`Hint Immediate @qualid`. .. cmdv:: Hint Constructors @qualid : @ident :name: Hint Constructors @@ -4234,7 +4286,7 @@ some incompatibilities. :name: Firstorder Solver The default tactic used by :tacn:`firstorder` when no rule applies is - :g:`auto with *`, it can be reset locally or globally using this option. + :g:`auto with core`, it can be reset locally or globally using this option. .. cmd:: Print Firstorder Solver diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 89b24ea8a3..c33d62532e 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -91,34 +91,30 @@ and tables: Flags, options and tables are identified by a series of identifiers, each with an initial capital letter. -.. cmd:: {? {| Local | Global | Export } } Set @flag +.. cmd:: Set @flag :name: Set - Sets :token:`flag` on. Scoping qualifiers are - described :ref:`here <set_unset_scope_qualifiers>`. + Sets :token:`flag` on. -.. cmd:: {? {| Local | Global | Export } } Unset @flag +.. cmd:: Unset @flag :name: Unset - Sets :token:`flag` off. Scoping qualifiers are - described :ref:`here <set_unset_scope_qualifiers>`. + Sets :token:`flag` off. .. cmd:: Test @flag Prints the current value of :token:`flag`. -.. cmd:: {? {| Local | Global | Export } } Set @option {| @num | @string } +.. cmd:: Set @option {| @num | @string } :name: Set @option - Sets :token:`option` to the specified value. Scoping qualifiers are - described :ref:`here <set_unset_scope_qualifiers>`. + Sets :token:`option` to the specified value. -.. cmd:: {? {| Local | Global | Export } } Unset @option +.. cmd:: Unset @option :name: Unset @option - Sets :token:`option` to its default value. Scoping qualifiers are - described :ref:`here <set_unset_scope_qualifiers>`. + Sets :token:`option` to its default value. .. cmd:: Test @option @@ -157,27 +153,37 @@ capital letter. A synonym for :cmd:`Print Options`. -.. _set_unset_scope_qualifiers: +Locality attributes supported by :cmd:`Set` and :cmd:`Unset` +```````````````````````````````````````````````````````````` + +The :cmd:`Set` and :cmd:`Unset` commands support the :attr:`local`, +:attr:`global` and :attr:`export` locality attributes: + +* no attribute: the original setting is *not* restored at the end of + the current module or section. +* :attr:`local` (an alternative syntax is to use the ``Local`` + prefix): the setting is applied within the current module or + section. The original value of the setting is restored at the end + of the current module or section. +* :attr:`export` (an alternative syntax is to use the ``Export`` + prefix): similar to :attr:`local`, the original value of the setting + is restored at the end of the current module or section. In + addition, if the value is set in a module, then :cmd:`Import`\-ing + the module sets the option or flag. +* :attr:`global` (an alternative syntax is to use the ``Global`` + prefix): the original setting is *not* restored at the end of the + current module or section. In addition, if the value is set in a + file, then :cmd:`Require`\-ing the file sets the option. + +Newly opened modules and sections inherit the current settings. -Scope qualifiers for :cmd:`Set` and :cmd:`Unset` -````````````````````````````````````````````````` - -:n:`{? {| Local | Global | Export } }` - -Flag and option settings can be global in scope or local to nested scopes created by -:cmd:`Module` and :cmd:`Section` commands. There are four alternatives: - -* no qualifier: the original setting is *not* restored at the end of the current module or section. -* **Local**: the setting is applied within the current scope. The original value of the option - or flag is restored at the end of the current module or section. -* **Global**: similar to no qualifier, the original setting is *not* restored at the end of the current - module or section. In addition, if the value is set in a file, then :cmd:`Require`-ing - the file sets the option. -* **Export**: similar to **Local**, the original value of the option or flag is restored at the - end of the current module or section. In addition, if the value is set in a file, then :cmd:`Import`-ing - the file sets the option. +.. note:: -Newly opened scopes inherit the current settings. + The use of the :attr:`global` attribute with the :cmd:`Set` and + :cmd:`Unset` commands is discouraged. If your goal is to define + project-wide settings, you should rather use the command-line + arguments ``-set`` and ``-unset`` for setting flags and options + (cf. :ref:`command-line-options`). .. _requests-to-the-environment: @@ -602,11 +608,11 @@ file is a particular case of module called *library file*. This loads and declares the module :n:`@qualid` and its dependencies then imports the contents of :n:`@qualid` as described - :ref:`here <import_qualid>`. It does not import the modules on which - qualid depends unless these modules were themselves required in module + for :cmd:`Import`. It does not import the modules that + :n:`@qualid` depends on unless these modules were themselves required in module :n:`@qualid` - using :cmd:`Require Export`, as described below, or recursively required - through a sequence of :cmd:`Require Export`. If the module required has + using :cmd:`Require Export`, or recursively required + through a series of :cmd:`Require Export`. If the module required has already been loaded, :cmd:`Require Import` :n:`@qualid` simply imports it, as :cmd:`Import` :n:`@qualid` would. @@ -665,13 +671,9 @@ file is a particular case of module called *library file*. the time it was compiled. - .. exn:: Require is not allowed inside a module or a module type. + .. warn:: Require inside a module is deprecated and strongly discouraged. You can Require a module at toplevel and optionally Import it inside another one. - This command - is not allowed inside a module or a module type being defined. It is - meant to describe a dependency between compilation units. Note however - that the commands ``Import`` and ``Export`` alone can be used inside modules - (see Section :ref:`Import <import_qualid>`). + Note that the :cmd:`Import` and :cmd:`Export` commands can be used inside modules. .. seealso:: Chapter :ref:`thecoqcommands` @@ -745,11 +747,6 @@ the toplevel, and using them in source files is discouraged. :n:`-Q @string @dirpath`. It adds the physical directory string to the current |Coq| loadpath and maps it to the logical directory dirpath. - .. cmdv:: Add LoadPath @string - - Performs as :n:`Add LoadPath @string @dirpath` but - for the empty directory path. - .. cmd:: Add Rec LoadPath @string as @dirpath @@ -757,11 +754,6 @@ the toplevel, and using them in source files is discouraged. :n:`-R @string @dirpath`. It adds the physical directory string and all its subdirectories to the current |Coq| loadpath. - .. cmdv:: Add Rec LoadPath @string - - Works as :n:`Add Rec LoadPath @string as @dirpath` but for the empty - logical directory path. - .. cmd:: Remove LoadPath @string @@ -784,12 +776,6 @@ the toplevel, and using them in source files is discouraged. loadpath (see the command `Declare ML Module`` in Section :ref:`compiled-files`). -.. cmd:: Add Rec ML Path @string - - This command adds the directory :n:`@string` and all its subdirectories to - the current OCaml loadpath (see the command :cmd:`Declare ML Module`). - - .. cmd:: Print ML Path @string This command displays the current OCaml loadpath. This @@ -1168,44 +1154,52 @@ described first. Controlling the locality of commands ----------------------------------------- +.. attr:: global + local -.. cmd:: Local @command - Global @command - - Some commands support a Local or Global prefix modifier to control the - scope of their effect. There are four kinds of commands: - + Some commands support a :attr:`local` or :attr:`global` attribute + to control the scope of their effect. There is also a legacy (and + much more commonly used) syntax using the ``Local`` or ``Global`` + prefixes (see :n:`@legacy_attr`). There are four kinds of + commands: + Commands whose default is to extend their effect both outside the section and the module or library file they occur in. For these - commands, the Local modifier limits the effect of the command to the + commands, the :attr:`local` attribute limits the effect of the command to the current section or module it occurs in. As an example, the :cmd:`Coercion` and :cmd:`Strategy` commands belong to this category. + Commands whose default behavior is to stop their effect at the end of the section they occur in but to extend their effect outside the module or - library file they occur in. For these commands, the Local modifier limits the + library file they occur in. For these commands, the :attr:`local` attribute limits the effect of the command to the current module if the command does not occur in a - section and the Global modifier extends the effect outside the current + section and the :attr:`global` attribute extends the effect outside the current sections and current module if the command occurs in a section. As an example, - the :cmd:`Arguments <Arguments (implicits)>`, :cmd:`Ltac` or :cmd:`Notation` commands belong + the :cmd:`Arguments`, :cmd:`Ltac` or :cmd:`Notation` commands belong to this category. Notice that a subclass of these commands do not support - extension of their scope outside sections at all and the Global modifier is not + extension of their scope outside sections at all and the :attr:`global` attribute is not applicable to them. + Commands whose default behavior is to stop their effect at the end - of the section or module they occur in. For these commands, the ``Global`` - modifier extends their effect outside the sections and modules they - occur in. The :cmd:`Transparent` and :cmd:`Opaque` - (see Section :ref:`vernac-controlling-the-reduction-strategies`) commands + of the section or module they occur in. For these commands, the :attr:`global` + attribute extends their effect outside the sections and modules they + occur in. The :cmd:`Transparent` and :cmd:`Opaque` commands belong to this category. + Commands whose default behavior is to extend their effect outside sections but not outside modules when they occur in a section and to extend their effect outside the module or library file they occur in - when no section contains them.For these commands, the Local modifier - limits the effect to the current section or module while the Global - modifier extends the effect outside the module even when the command + when no section contains them. For these commands, the :attr:`local` attribute + limits the effect to the current section or module while the :attr:`global` + attribute extends the effect outside the module even when the command occurs in a section. The :cmd:`Set` and :cmd:`Unset` commands belong to this category. +.. attr:: export + + Some commands support an :attr:`export` attribute. The effect of + the attribute is to make the effect of the command available when + the module containing it is imported. It is supported in + particular by the :cmd:`Hint`, :cmd:`Set` and :cmd:`Unset` + commands. + .. _controlling-typing-flags: Controlling Typing Flags diff --git a/doc/sphinx/proofs/automatic-tactics/index.rst b/doc/sphinx/proofs/automatic-tactics/index.rst new file mode 100644 index 0000000000..a219770c69 --- /dev/null +++ b/doc/sphinx/proofs/automatic-tactics/index.rst @@ -0,0 +1,20 @@ +.. _automatic-tactics: + +===================================================== +Built-in decision procedures and programmable tactics +===================================================== + +Some tactics are largely automated and are able to solve complex +goals. This chapter presents both some decision procedures that can +be used to solve some specific categories of goals, and some +programmable tactics, that the user can instrument to handle some +complex goals in new domains. + +.. toctree:: + :maxdepth: 1 + + ../../addendum/omega + ../../addendum/micromega + ../../addendum/ring + ../../addendum/nsatz + ../../addendum/generalized-rewriting diff --git a/doc/sphinx/proofs/creating-tactics/index.rst b/doc/sphinx/proofs/creating-tactics/index.rst new file mode 100644 index 0000000000..1af1b0b726 --- /dev/null +++ b/doc/sphinx/proofs/creating-tactics/index.rst @@ -0,0 +1,34 @@ +.. _writing-tactics: + +==================== +Creating new tactics +==================== + +The languages presented in this chapter allow one to build complex +tactics by combining existing ones with constructs such as +conditionals and looping. While :ref:`Ltac <ltac>` was initially +thought of as a language for doing some basic combinations, it has +been used successfully to build highly complex tactics as well, but +this has also highlighted its limits and fragility. The experimental +language :ref:`Ltac2 <ltac2>` is a typed and more principled variant +which is more adapted to building complex tactics. + +There are other solutions beyond these two tactic languages to write +new tactics: + +- `Mtac2 <https://github.com/Mtac2/Mtac2>`_ is an external plugin + which provides another typed tactic language. While Ltac2 belongs + to the ML language family, Mtac2 reuses the language of Coq itself + as the language to build Coq tactics. + +- The most traditional way of building new complex tactics is to write + a Coq plugin in OCaml. Beware that this also requires much more + effort and commitment. A tutorial for writing Coq plugins is + available in the Coq repository in `doc/plugin_tutorial + <https://github.com/coq/coq/tree/master/doc/plugin_tutorial>`_. + +.. toctree:: + :maxdepth: 1 + + ../../proof-engine/ltac + ../../proof-engine/ltac2 diff --git a/doc/sphinx/proofs/writing-proofs/index.rst b/doc/sphinx/proofs/writing-proofs/index.rst new file mode 100644 index 0000000000..a279a5957f --- /dev/null +++ b/doc/sphinx/proofs/writing-proofs/index.rst @@ -0,0 +1,34 @@ +.. _writing-proofs: + +============== +Writing proofs +============== + +Coq is an interactive theorem prover, or proof assistant, which means +that proofs can be constructed interactively through a dialog between +the user and the assistant. The building blocks for this dialog are +tactics which the user will use to represent steps in the proof of a +theorem. + +Incomplete proofs have one or more open (unproven) sub-goals. Each +goal has its own context (a set of assumptions that can be used to +prove the goal). Tactics can transform goals and contexts. +Internally, the incomplete proof is represented as a partial proof +term, with holes for the unproven sub-goals. + +When a proof is complete, the user leaves the proof mode and defers +the verification of the resulting proof term to the :ref:`kernel +<core-language>`. + +This chapter is divided in several parts, describing the basic ideas +of the proof mode (during which tactics can be used), and several +flavors of tactics, including the SSReflect proof language. + +.. toctree:: + :maxdepth: 1 + + ../../proof-engine/proof-handling + ../../proof-engine/tactics + ../../proof-engine/ssreflect-proof-language + ../../proof-engine/detailed-tactic-examples + ../../user-extensions/proof-schemes diff --git a/doc/sphinx/refman-preamble.rst b/doc/sphinx/refman-preamble.rst index de95eda989..05e665a43b 100644 --- a/doc/sphinx/refman-preamble.rst +++ b/doc/sphinx/refman-preamble.rst @@ -11,60 +11,18 @@ .. role:: smallcaps -.. |A_1| replace:: `A`\ :math:`_{1}` -.. |A_n| replace:: `A`\ :math:`_{n}` -.. |arg_1| replace:: `arg`\ :math:`_{1}` -.. |arg_n| replace:: `arg`\ :math:`_{n}` -.. |bdi| replace:: :math:`\beta\delta\iota` -.. |binder_1| replace:: `binder`\ :math:`_{1}` -.. |binder_n| replace:: `binder`\ :math:`_{n}` -.. |binders_1| replace:: `binders`\ :math:`_{1}` -.. |binders_n| replace:: `binders`\ :math:`_{n}` -.. |C_1| replace:: `C`\ :math:`_{1}` .. |c_1| replace:: `c`\ :math:`_{1}` -.. |C_2| replace:: `C`\ :math:`_{2}` .. |c_i| replace:: `c`\ :math:`_{i}` .. |c_n| replace:: `c`\ :math:`_{n}` -.. |Cic| replace:: :smallcaps:`Cic` -.. |class_1| replace:: `class`\ :math:`_{1}` -.. |class_2| replace:: `class`\ :math:`_{2}` +.. |Cic| replace:: CIC .. |Coq| replace:: :smallcaps:`Coq` .. |CoqIDE| replace:: :smallcaps:`CoqIDE` .. |eq_beta_delta_iota_zeta| replace:: `=`\ :math:`_{\beta\delta\iota\zeta}` .. |Gallina| replace:: :smallcaps:`Gallina` -.. |ident_0| replace:: `ident`\ :math:`_{0}` -.. |ident_1,1| replace:: `ident`\ :math:`_{1,1}` -.. |ident_1,k_1| replace:: `ident`\ :math:`_{1,k_1}`) -.. |ident_1| replace:: `ident`\ :math:`_{1}` -.. |ident_2| replace:: `ident`\ :math:`_{2}` -.. |ident_3| replace:: `ident`\ :math:`_{3}` -.. |ident_i| replace:: `ident`\ :math:`_{i}` -.. |ident_j| replace:: `ident`\ :math:`_{j}` -.. |ident_k| replace:: `ident`\ :math:`_{k}` -.. |ident_n,1| replace:: `ident`\ :math:`_{n,1}` -.. |ident_n,k_n| replace:: `ident`\ :math:`_{n,k_n}` -.. |ident_n| replace:: `ident`\ :math:`_{n}` .. |Latex| replace:: :smallcaps:`LaTeX` .. |L_tac| replace:: `L`:sub:`tac` .. |Ltac| replace:: `L`:sub:`tac` .. |ML| replace:: :smallcaps:`ML` -.. |mod_0| replace:: `mod`\ :math:`_{0}` -.. |mod_1| replace:: `mod`\ :math:`_{1}` -.. |mod_2| replace:: `mod`\ :math:`_{1}` -.. |mod_n| replace:: `mod`\ :math:`_{n}` -.. |module_0| replace:: `module`\ :math:`_{0}` -.. |module_1| replace:: `module`\ :math:`_{1}` -.. |module_expression_0| replace:: `module_expression`\ :math:`_{0}` -.. |module_expression_1| replace:: `module_expression`\ :math:`_{1}` -.. |module_expression_i| replace:: `module_expression`\ :math:`_{i}` -.. |module_expression_n| replace:: `module_expression`\ :math:`_{n}` -.. |module_n| replace:: `module`\ :math:`_{n}` -.. |module_type_0| replace:: `module_type`\ :math:`_{0}` -.. |module_type_1| replace:: `module_type`\ :math:`_{1}` -.. |module_type_i| replace:: `module_type`\ :math:`_{i}` -.. |module_type_n| replace:: `module_type`\ :math:`_{n}` -.. |N| replace:: ``N`` -.. |nat| replace:: ``nat`` .. |OCaml| replace:: :smallcaps:`OCaml` .. |p_1| replace:: `p`\ :math:`_{1}` .. |p_i| replace:: `p`\ :math:`_{i}` @@ -79,24 +37,6 @@ .. |t_i| replace:: `t`\ :math:`_{i}` .. |t_m| replace:: `t`\ :math:`_{m}` .. |t_n| replace:: `t`\ :math:`_{n}` -.. |f_1| replace:: `f`\ :math:`_{1}` -.. |f_i| replace:: `f`\ :math:`_{i}` -.. |f_m| replace:: `f`\ :math:`_{m}` -.. |f_n| replace:: `f`\ :math:`_{n}` -.. |u_1| replace:: `u`\ :math:`_{1}` -.. |u_i| replace:: `u`\ :math:`_{i}` -.. |u_m| replace:: `u`\ :math:`_{m}` -.. |u_n| replace:: `u`\ :math:`_{n}` -.. |term_0| replace:: `term`\ :math:`_{0}` -.. |term_1| replace:: `term`\ :math:`_{1}` -.. |term_2| replace:: `term`\ :math:`_{2}` -.. |term_n| replace:: `term`\ :math:`_{n}` -.. |type_0| replace:: `type`\ :math:`_{0}` -.. |type_1| replace:: `type`\ :math:`_{1}` -.. |type_2| replace:: `type`\ :math:`_{2}` -.. |type_3| replace:: `type`\ :math:`_{3}` -.. |type_n| replace:: `type`\ :math:`_{n}` .. |x_1| replace:: `x`\ :math:`_{1}` .. |x_i| replace:: `x`\ :math:`_{i}` .. |x_n| replace:: `x`\ :math:`_{n}` -.. |Z| replace:: ``Z`` diff --git a/doc/sphinx/refman-preamble.sty b/doc/sphinx/refman-preamble.sty index 90a63a5a2d..629c30a793 100644 --- a/doc/sphinx/refman-preamble.sty +++ b/doc/sphinx/refman-preamble.sty @@ -1,32 +1,20 @@ -\newcommand{\alors}{\textsf{then}} -\newcommand{\alter}{\textsf{alter}} \newcommand{\as}{\kw{as}} \newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)} -\newcommand{\bool}{\textsf{bool}} \newcommand{\case}{\kw{case}} -\newcommand{\conc}{\textsf{conc}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} -\newcommand{\conshl}{\textsf{cons\_hl}} \newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} -\newcommand{\EqSt}{\textsf{EqSt}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} -\newcommand{\false}{\textsf{false}} -\newcommand{\filter}{\textsf{filter}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} -\newcommand{\from}{\textsf{from}} \newcommand{\Functor}{\kw{Functor}} -\newcommand{\haslength}{\textsf{has\_length}} -\newcommand{\hd}{\textsf{hd}} -\newcommand{\ident}{\textsf{ident}} \newcommand{\In}{\kw{in}} \newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} @@ -34,7 +22,6 @@ \newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} -\newcommand{\lb}{\lambda} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} @@ -45,7 +32,6 @@ \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} -\newcommand{\Nat}{\mathbb{N}} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} @@ -57,13 +43,10 @@ \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} -\newcommand{\Prod}{\textsf{prod}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} -\newcommand{\si}{\textsf{if}} -\newcommand{\sinon}{\textsf{else}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} @@ -71,9 +54,7 @@ \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} -\newcommand{\true}{\textsf{true}} \newcommand{\Type}{\textsf{Type}} -\newcommand{\unfold}{\textsf{unfold}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} @@ -88,4 +69,3 @@ \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} -\newcommand{\zeros}{\textsf{zeros}} diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index 5b0b3c51b0..34197c4fcf 100644 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ b/doc/sphinx/user-extensions/proof-schemes.rst @@ -337,31 +337,31 @@ Generation of inversion principles with ``Derive`` ``Inversion`` ----------------------------------------------------------------- .. cmd:: Derive Inversion @ident with @ident Sort @sort - Derive Inversion @ident with (forall @binders, @ident @term) Sort @sort + Derive Inversion @ident with (forall {* @binder }, @ident @term) Sort @sort This command generates an inversion principle for the :tacn:`inversion ... using ...` tactic. The first :token:`ident` is the name of the generated principle. The second :token:`ident` should be an inductive predicate, and :token:`binders` the variables occurring in the term :token:`term`. This command generates the inversion lemma for the sort - :token:`sort` corresponding to the instance :n:`forall @binders, @ident @term`. + :token:`sort` corresponding to the instance :n:`forall {* @binder }, @ident @term`. When applied, it is equivalent to having inverted the instance with the tactic :g:`inversion`. .. cmdv:: Derive Inversion_clear @ident with @ident Sort @sort - Derive Inversion_clear @ident with (forall @binders, @ident @term) Sort @sort + Derive Inversion_clear @ident with (forall {* @binder }, @ident @term) Sort @sort When applied, it is equivalent to having inverted the instance with the tactic inversion replaced by the tactic `inversion_clear`. .. cmdv:: Derive Dependent Inversion @ident with @ident Sort @sort - Derive Dependent Inversion @ident with (forall @binders, @ident @term) Sort @sort + Derive Dependent Inversion @ident with (forall {* @binder }, @ident @term) Sort @sort When applied, it is equivalent to having inverted the instance with the tactic `dependent inversion`. .. cmdv:: Derive Dependent Inversion_clear @ident with @ident Sort @sort - Derive Dependent Inversion_clear @ident with (forall @binders, @ident @term) Sort @sort + Derive Dependent Inversion_clear @ident with (forall {* @binder }, @ident @term) Sort @sort When applied, it is equivalent to having inverted the instance with the tactic `dependent inversion_clear`. diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index dbe714c388..669975ba7e 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -163,6 +163,10 @@ Grammar constr` is at level 100. To avoid ``x : A`` being parsed as a type cast, it is necessary to put ``x`` at a level below 100, typically 99. Hence, a correct definition is the following: +.. coqtop:: none + + Reset Initial. + .. coqtop:: all Notation "{ x : A | P }" := (sig A (fun x => P)) (x at level 99). @@ -306,10 +310,10 @@ at the time of use of the notation. The Infix command ~~~~~~~~~~~~~~~~~~ -The :cmd:`Infix` command is a shortening for declaring notations of infix +The :cmd:`Infix` command is a shortcut for declaring notations for infix symbols. -.. cmd:: Infix "@symbol" := @term {? (@modifiers) }. +.. cmd:: Infix @string := @term {? (@modifiers) } This command is equivalent to @@ -350,6 +354,11 @@ Reserving notations This command declares an infix parsing rule without giving its interpretation. + When a format is attached to a reserved notation, it is used by + default by all subsequent interpretations of the corresponding + notation. A specific interpretation can provide its own format + overriding the default format though. + Simultaneous definition of terms and notations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -357,7 +366,7 @@ Thanks to reserved notations, the inductive, co-inductive, record, recursive and corecursive definitions can benefit from customized notations. To do this, insert a ``where`` notation clause after the definition of the (co)inductive type or (co)recursive term (or after the definition of each of them in case of mutual -definitions). The exact syntax is given by :token:`decl_notation` for inductive, +definitions). The exact syntax is given by :n:`@decl_notation` for inductive, co-inductive, recursive and corecursive definitions and in :ref:`record-types` for records. Here are examples: @@ -387,6 +396,11 @@ Displaying information about notations Controls whether to use notations for printing terms wherever possible. Default is on. +.. flag:: Printing Parentheses + + If on, parentheses are printed even if implied by associativity and precedence + Default is off. + .. seealso:: :flag:`Printing All` @@ -408,6 +422,27 @@ identifiers or tokens starting with a single quote are dropped. Locate "exists". Locate "exists _ .. _ , _". +Inheritance of the properties of arguments of constants bound to a notation +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +If the right-hand side of a notation is a partially applied constant, +the notation inherits the implicit arguments (see +:ref:`ImplicitArguments`) and interpretation scopes (see +:ref:`Scopes`) of the constant. For instance: + +.. coqtop:: in reset + + Record R := {dom : Type; op : forall {A}, A -> dom}. + Notation "# x" := (@op x) (at level 8). + +.. coqtop:: all + + Check fun x:R => # x 3. + +As an exception, if the right-hand side is just of the form +:n:`@@qualid`, this conventionally stops the inheritance of implicit +arguments (but not of interpretation scopes). + Notations and binders ~~~~~~~~~~~~~~~~~~~~~ @@ -798,7 +833,13 @@ associated to the custom entry ``expr``. The level can be omitted, as in Notation "[ e ]" := e (e custom expr). -in which case Coq tries to infer it. +in which case Coq infer it. If the sub-expression is at a border of +the notation (as e.g. ``x`` and ``y`` in ``x + y``), the level is +determined by the associativity. If the sub-expression is not at the +border of the notation (as e.g. ``e`` in ``"[ e ]``), the level is +inferred to be the highest level used for the entry. In particular, +this level depends on the highest level existing in the entry at the +time of use of the notation. In the absence of an explicit entry for parsing or printing a sub-expression of a notation in a custom entry, the default is to @@ -868,12 +909,11 @@ notations are given below. The optional :production:`scope` is described in notation : [Local] Notation `string` := `term` [(`modifiers`)] [: `scope`]. : [Local] Infix `string` := `qualid` [(`modifiers`)] [: `scope`]. : [Local] Reserved Notation `string` [(`modifiers`)] . - : 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 `fix_body` [`decl_notation`] with … with `fix_body` [`decl_notation`]. + : Inductive `ind_body` [`decl_notations`] with … with `ind_body` [`decl_notations`]. + : CoInductive `ind_body` [`decl_notations`] with … with `ind_body` [`decl_notations`]. + : Fixpoint `fix_body` [`decl_notations`] with … with `fix_body` [`decl_notations`]. + : CoFixpoint `fix_body` [`decl_notations`] with … with `fix_body` [`decl_notations`]. : [Local] Declare Custom Entry `ident`. - decl_notation : [where `string` := `term` [: `scope`] and … and `string` := `term` [: `scope`]]. modifiers : `modifier`, … , `modifier` modifier : at level `num` : in custom `ident` @@ -903,6 +943,12 @@ notations are given below. The optional :production:`scope` is described in : as pattern : as strict pattern +.. insertprodn decl_notations decl_notation + +.. prodn:: + decl_notations ::= where @decl_notation {* and @decl_notation } + decl_notation ::= @string := @one_term {? ( only parsing ) } {? : @ident } + .. note:: No typing of the denoted expression is performed at definition time. Type checking is done only at the time of use of the notation. @@ -1148,7 +1194,7 @@ Binding arguments of a constant to an interpretation scope Binding types of arguments to an interpretation scope +++++++++++++++++++++++++++++++++++++++++++++++++++++ -.. cmd:: Bind Scope @scope with @qualid +.. cmd:: Bind Scope @ident with {+ @class } When an interpretation scope is naturally associated to a type (e.g. the scope of operations on the natural numbers), it may be convenient to bind it @@ -1400,6 +1446,12 @@ Abbreviations denoted expression is performed at definition time. Type checking is done only at the time of use of the abbreviation. + Like for notations, if the right-hand side of an abbreviation is a + partially applied constant, the abbreviation inherits the implicit + arguments and interpretation scopes of the constant. As an + exception, if the right-hand side is just of the form :n:`@@qualid`, + this conventionally stops the inheritance of implicit arguments. + .. _numeral-notations: Numeral notations diff --git a/doc/sphinx/using/libraries/index.rst b/doc/sphinx/using/libraries/index.rst new file mode 100644 index 0000000000..d0848e6c3f --- /dev/null +++ b/doc/sphinx/using/libraries/index.rst @@ -0,0 +1,24 @@ +.. _libraries: + +===================== +Libraries and plugins +===================== + +Coq is distributed with a standard library and a set of internal +plugins (most of which provide tactics that have already been +presented in :ref:`writing-proofs`). This chapter presents this +standard library and some of these internal plugins which provide +features that are not tactics. + +In addition, Coq has a rich ecosystem of external libraries and +plugins. These libraries and plugins can be browsed online through +the `Coq Package Index <https://coq.inria.fr/opam/www/>`_ and +installed with the `opam package manager +<https://coq.inria.fr/opam-using.html>`_. + +.. toctree:: + :maxdepth: 1 + + ../../language/coq-library + ../../addendum/extraction + ../../addendum/miscellaneous-extensions diff --git a/doc/sphinx/using/tools/index.rst b/doc/sphinx/using/tools/index.rst new file mode 100644 index 0000000000..4381c4d63d --- /dev/null +++ b/doc/sphinx/using/tools/index.rst @@ -0,0 +1,20 @@ +.. _tools: + +================================ +Command-line and graphical tools +================================ + +This chapter presents the command-line tools that users will need to +build their Coq project, the documentation of the CoqIDE standalone +user interface and the documentation of the parallel proof processing +feature that is supported by CoqIDE and several other user interfaces. +A list of available user interfaces to interact with Coq is available +on the `Coq website <https://coq.inria.fr/user-interfaces.html>`_. + +.. toctree:: + :maxdepth: 1 + + ../../practical-tools/coq-commands + ../../practical-tools/utilities + ../../practical-tools/coqide + ../../addendum/parallel-proof-processing |