diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/README.rst | 22 | ||||
| -rw-r--r-- | doc/sphinx/_static/coqnotations.sty | 17 | ||||
| -rw-r--r-- | doc/sphinx/_static/notations.css | 54 | ||||
| -rw-r--r-- | doc/sphinx/addendum/extended-pattern-matching.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/addendum/implicit-coercions.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/dune | 8 | ||||
| -rw-r--r-- | doc/sphinx/introduction.rst | 8 | ||||
| -rw-r--r-- | doc/sphinx/language/coq-library.rst | 63 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 83 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 442 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 37 |
12 files changed, 382 insertions, 366 deletions
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index 549598b187..a34b2d5195 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -143,22 +143,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/_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..3806ba6ee6 100644 --- a/doc/sphinx/_static/notations.css +++ b/doc/sphinx/_static/notations.css @@ -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/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst index 45b3f6f161..15f42591ce 100644 --- a/doc/sphinx/addendum/extended-pattern-matching.rst +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -192,7 +192,7 @@ Disjunctive patterns -------------------- Multiple patterns that share the same right-hand-side can be -factorized using the notation :n:`{+| @patterns_comma}`. For +factorized using the notation :n:`{+| {+, @pattern } }`. For instance, :g:`max` can be rewritten as follows: .. coqtop:: in reset diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index c3b197288f..19b33f0d90 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -165,6 +165,12 @@ Declaring Coercions convertible with existing ones when they have coercions that don't satisfy the uniform inheritance condition. + .. warn:: ... is not definitionally an identity function. + + If a coercion path has the same source and target class, that is said to be + circular. When a new circular coercion path is not convertible with the + identity function, it will be reported as ambiguous. + .. cmdv:: Local Coercion @qualid : @class >-> @class Declares the construction denoted by :token:`qualid` as a coercion local to diff --git a/doc/sphinx/dune b/doc/sphinx/dune index 353d58c676..b788fbbeed 100644 --- a/doc/sphinx/dune +++ b/doc/sphinx/dune @@ -1,8 +1,10 @@ (dirs :standard _static) -(rule (targets README.gen.rst) +(rule + (targets README.gen.rst) (deps (source_tree ../tools/coqrst) README.template.rst) (action (run ../tools/coqrst/regen_readme.py %{targets}))) -(alias (name refman-html) - (action (diff README.rst README.gen.rst))) +(rule + (alias refman-html) + (action (diff README.rst README.gen.rst))) diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index bcdf3277ad..1424b4f3e1 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -60,7 +60,7 @@ Nonetheless, the manual has some structure that is explained below. of the formalism. Chapter :ref:`themodulesystem` describes the module system. -- The second part describes the proof engine. It is divided in six +- The second part describes the proof engine. It is divided into several chapters. Chapter :ref:`vernacularcommands` presents all commands (we call them *vernacular commands*) that are not directly related to interactive proving: requests to the environment, complete or partial @@ -68,8 +68,10 @@ Nonetheless, the manual has some structure that is explained below. proofs, do multiple proofs in parallel is explained in Chapter :ref:`proofhandling`. In Chapter :ref:`tactics`, all commands that realize one or more steps of the proof are presented: we call them - *tactics*. The language to combine these tactics into complex proof - strategies is given in Chapter :ref:`ltac`. Examples of tactics + *tactics*. The legacy language to combine these tactics into complex proof + strategies is given in Chapter :ref:`ltac`. The currently experimental + language that will eventually replace Ltac is presented in + Chapter :ref:`ltac2`. Examples of tactics are described in Chapter :ref:`detailedexamplesoftactics`. Finally, the |SSR| proof language is presented in Chapter :ref:`thessreflectprooflanguage`. diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index cad5e4e67e..80f209fcf1 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -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/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index ae0afc7819..78428be18f 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -155,19 +155,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. @@ -1878,27 +1878,16 @@ Controlling the insertion of implicit arguments not followed by explicit argumen 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: +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`. -.. _explicit_app_grammar: - - .. productionlist:: explicit_apps - term : @ `qualid` `term` … `term` - : @ `qualid` - : `qualid` `argument` … `argument` - argument : `term` - : (`ident` := `term`) - - Syntax for explicitly giving implicit arguments - -.. example:: (continued) +.. example:: Syntax for explicitly giving implicit arguments (continued) .. coqtop:: all @@ -2003,10 +1992,11 @@ applied to an unknown structure instance (an implicit argument) and a value. The complete documentation of canonical structures can be found in :ref:`canonicalstructures`; here only a simple example is given. -.. cmd:: Canonical {? Structure } @qualid +.. cmd:: {? Local | #[local] } Canonical {? Structure } @qualid This command declares :token:`qualid` as a canonical instance of a - structure (a record). + structure (a record). When the :g:`#[local]` attribute is given the effect + stops at the end of the :g:`Section` containig it. Assume that :token:`qualid` denotes an object ``(Build_struct`` |c_1| … |c_n| ``)`` in the structure :g:`struct` of which the fields are |x_1|, …, |x_n|. @@ -2069,16 +2059,18 @@ in :ref:`canonicalstructures`; here only a simple example is given. See :ref:`canonicalstructures` for a more realistic example. - .. cmdv:: Canonical {? Structure } @ident {? : @type } := @term + .. cmdv:: {? Local | #[local] } Canonical {? Structure } @ident {? : @type } := @term This is equivalent to a regular definition of :token:`ident` followed by the declaration :n:`Canonical @ident`. -.. cmd:: Print Canonical Projections +.. cmd:: Print Canonical Projections {* @ident} This displays the list of global names that are components of some canonical structure. For each of them, the canonical structure of - which it is a projection is indicated. + which it is a projection is indicated. If constants are given as + its arguments, only the unification rules that involve or are + synthesized from simultaneously all given constants will be shown. .. example:: @@ -2088,10 +2080,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 ~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2311,17 +2308,13 @@ Printing universes Existential variables --------------------- -.. insertgram term_evar evar_binding - -.. productionlist:: coq - term_evar : ?[ `ident` ] - : ?[ ?`ident` ] - : ?`ident` `evar_bindings_opt` - evar_bindings_opt : @{ `evar_bindings_semi` } - : `empty` - evar_bindings_semi : `evar_bindings_semi` ; `evar_binding` - : `evar_binding` - evar_binding : `ident` := `term` +.. insertprodn term_evar evar_binding + +.. prodn:: + term_evar ::= ?[ @ident ] + | ?[ ?@ident ] + | ?@ident {? @%{ {+; @evar_binding } %} } + evar_binding ::= @ident := @term |Coq| terms can include existential variables which represents unknown subterms to eventually be replaced by actual subterms. diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 3cc101d06b..f82282911f 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: @@ -58,10 +58,12 @@ Identifiers 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, @@ -77,13 +79,13 @@ Numerals 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 @@ -139,50 +141,39 @@ 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 + 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 Types ----- @@ -196,12 +187,11 @@ of types inside the syntactic class :token:`term`. 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* (definitions, lemmas, theorems, remarks or facts), *global variables* @@ -210,7 +200,7 @@ types*. *Simple identifiers* (or shortly :token:`ident`) are a syntactic subset of qualified identifiers. Identifiers may also denote *local variables*, while qualified identifiers do not. -Field identifiers, written :token:`field`, are identifiers prefixed by +Field identifiers, written :token:`field_ident`, are identifiers prefixed by `.` (dot) with no blank between the dot and the identifier. @@ -237,34 +227,27 @@ 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_annot + +.. 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 + universe_level ::= Set + | Prop + | Type + | _ + | @qualid + univ_annot ::= @%{ {* @universe_level } %} There are four sorts :g:`SProp`, :g:`Prop`, :g:`Set` and :g:`Type`. @@ -272,12 +255,12 @@ 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`. + themselves are typing the proofs. We denote propositions by :token:`form`. This constitutes a semantic subclass of the syntactic class :token:`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 + specifications by :token:`specif`. This constitutes a semantic subclass of the syntactic class :token:`term`. - :g:`Type` is the type of sorts. @@ -289,34 +272,24 @@ 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 typeclass_constraint + +.. prodn:: + open_binders ::= {+ @name } : @term + | {+ @binder } + name ::= _ + | @ident + binder ::= @name + | ( {+ @name } : @term ) + | ( @name {? : @term } := @term ) + | %{ {+ @name } {? : @term } %} + | `( {+, @typeclass_constraint } ) + | `%{ {+, @typeclass_constraint } %} + | ' @pattern0 + | ( @name : @term %| @term ) + typeclass_constraint ::= {? ! } @term + | %{ @name %} : {? ! } @term + | @name : {? ! } @term 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 @@ -411,13 +384,13 @@ 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`. @@ -444,21 +417,14 @@ guess the missing piece of information. Let-in definitions ------------------ -.. insertgram term_let names_comma +.. insertprodn term_let term_let -.. 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` +.. prodn:: + term_let ::= let @name {? : @term } := @term in @term + | let @name {+ @binder } {? : @term } := @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 @@ -471,57 +437,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 +465,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 +by a single :token:`case_item` expression, an :token:`eqn` restricted to a single :token:`pattern` and :token:`pattern` restricted to the form :n:`@qualid {* @ident}`. -The expression match ":token:`term`:math:`_0` :token:`return_type_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 :token:`ident` is dependent in the return type. For instance, in the following example: .. coqtop:: in @@ -604,19 +537,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; +- :token:`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,27 +584,18 @@ Sections :ref:`if-then-else` and :ref:`irrefutable-patterns`). Recursive and co-recursive functions: fix and cofix --------------------------------------------------- -.. insertgram term_fix term1_extended_opt +.. insertprodn term_fix term1_extended + +.. prodn:: + term_fix ::= let fix @fix_body in @term + | fix @fix_body {? {+ with @fix_body } for @ident } + fix_body ::= @ident {* @binder } {? @fixannot } {? : @term } := @term + fixannot ::= %{ struct @ident %} + | %{ wf @term1_extended @ident %} + | %{ measure @term1_extended {? @ident } {? @term1_extended } %} + term1_extended ::= @term1 + | @ @qualid {? @univ_annot } -.. 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`` @@ -681,6 +605,17 @@ The expression “``fix`` :token:`ident`:math:`_1` :token:`binder`:math:`_1` ``: 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 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. + +.. 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 } {? : @term } := @term + 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 @@ -688,10 +623,6 @@ The expression “``cofix`` :token:`ident`:math:`_1` :token:`binder`:math:`_1` ` 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. -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. - .. _vernacular: The Vernacular @@ -715,6 +646,8 @@ The Vernacular : ( `ident` … `ident` : `term` ) … ( `ident` … `ident` : `term` ) definition : [Local] Definition `ident` [`binders`] [: `term`] := `term` . : Let `ident` [`binders`] [: `term`] := `term` . + binders : binders binder + : binder inductive : Inductive `ind_body` with … with `ind_body` . : CoInductive `ind_body` with … with `ind_body` . ind_body : `ident` [`binders`] : `term` := @@ -1545,7 +1478,7 @@ Chapter :ref:`Tactics`. The basic assertion command is: The name you provided is already defined. You have then to choose another name. - .. exn:: Nested proofs are not allowed unless you turn the :flag:`Nested Proofs Allowed` flag on. + .. exn:: Nested proofs are not allowed unless you turn the 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. @@ -1715,10 +1648,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/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index cfdc70d50e..dd80b29bda 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -1,12 +1,12 @@ .. _ltac2: +Ltac2 +===== + .. coqtop:: none From Ltac2 Require Import Ltac2. -Ltac2 -===== - The Ltac tactic language is probably one of the ingredients of the success of Coq, yet it is at the same time its Achilles' heel. Indeed, Ltac: diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 81e50c0834..53cfb973d4 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -555,12 +555,14 @@ Applying theorems This tactic applies to any goal. It behaves like :tacn:`exact` with a big difference: the user can leave some holes (denoted by ``_`` or :n:`(_ : @type)`) in the term. :tacn:`refine` will generate as many - subgoals as there are holes in the term. The type of holes must be either - synthesized by the system or declared by an explicit cast + subgoals as there are remaining holes in the elaborated term. The type + of holes must be either synthesized by the system or declared by an explicit cast like ``(_ : nat -> Prop)``. Any subgoal that occurs in other subgoals is automatically shelved, as if calling - :tacn:`shelve_unifiable`. This low-level tactic can be - useful to advanced users. + :tacn:`shelve_unifiable`. The produced subgoals (shelved or not) + are *not* candidates for typeclass resolution, even if they have a type-class + type as conclusion, letting the user control when and how typeclass resolution + is launched on them. This low-level tactic can be useful to advanced users. .. example:: @@ -611,8 +613,9 @@ Applying theorems .. tacv:: simple notypeclasses refine @term :name: simple notypeclasses refine - This tactic behaves like :tacn:`simple refine` except it performs type checking - without resolution of typeclasses. + This tactic behaves like the combination of :tacn:`simple refine` and + :tacn:`notypeclasses refine`: it performs type checking without resolution of + typeclasses, does not perform beta reductions or shelve the subgoals. .. flag:: Debug Unification @@ -685,6 +688,28 @@ Applying theorems instantiate (see :ref:`Existential-Variables`). The instantiation is intended to be found later in the proof. + .. tacv:: rapply @term + :name: rapply + + The tactic :tacn:`rapply` behaves like :tacn:`eapply` but it + uses the proof engine of :tacn:`refine` for dealing with + existential variables, holes, and conversion problems. This may + result in slightly different behavior regarding which conversion + problems are solvable. However, like :tacn:`apply` but unlike + :tacn:`eapply`, :tacn:`rapply` will fail if there are any holes + which remain in :n:`@term` itself after typechecking and + typeclass resolution but before unification with the goal. More + technically, :n:`@term` is first parsed as a + :production:`constr` rather than as a :production:`uconstr` or + :production:`open_constr` before being applied to the goal. Note + that :tacn:`rapply` prefers to instantiate as many hypotheses of + :n:`@term` as possible. As a result, if it is possible to apply + :n:`@term` to arbitrarily many arguments without getting a type + error, :tacn:`rapply` will loop. + + Note that you need to :n:`Require Import Coq.Program.Tactics` to + make use of :tacn:`rapply`. + .. tacv:: simple apply @term. This behaves like :tacn:`apply` but it reasons modulo conversion only on subterms |