diff options
Diffstat (limited to 'doc')
19 files changed, 437 insertions, 355 deletions
diff --git a/doc/changelog/02-specification-language/10167-orpat-mixfix.rst b/doc/changelog/02-specification-language/10167-orpat-mixfix.rst new file mode 100644 index 0000000000..e3c3923348 --- /dev/null +++ b/doc/changelog/02-specification-language/10167-orpat-mixfix.rst @@ -0,0 +1,12 @@ +- Require parentheses around nested disjunctive patterns, so that pattern and + term syntax are consistent; match branch patterns no longer require + parentheses for notation at level 100 or more. Incompatibilities: + + + in :g:`match p with (_, (0|1)) => ...` parentheses may no longer be + omitted around :n:`0|1`. + + notation :g:`(p | q)` now potentially clashes with core pattern syntax, + and should be avoided. ``-w disj-pattern-notation`` flags such :cmd:`Notation`. + + see :ref:`extendedpatternmatching` for details + (`#10167 <https://github.com/coq/coq/pull/10167>`_, + by Georges Gonthier). diff --git a/doc/changelog/04-tactics/09288-injection-as.rst b/doc/changelog/04-tactics/09288-injection-as.rst new file mode 100644 index 0000000000..6a74551f06 --- /dev/null +++ b/doc/changelog/04-tactics/09288-injection-as.rst @@ -0,0 +1,4 @@ +- Documented syntax :n:`injection @term as [= {+ @intropattern} ]` as + an alternative to :n:`injection @term as {+ @simple_intropattern}` using + the standard :n:`@injection_intropattern` syntax (`#09288 + <https://github.com/coq/coq/pull/09288>`_, by Hugo Herbelin). diff --git a/doc/plugin_tutorial/tuto1/src/simple_print.ml b/doc/plugin_tutorial/tuto1/src/simple_print.ml index cfc38ff9c9..22a0163fbb 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_print.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_print.ml @@ -11,7 +11,7 @@ let simple_body_access gref = failwith "constructors are not covered in this example" | Globnames.ConstRef cst -> let cb = Environ.lookup_constant cst (Global.env()) in - match Global.body_of_constant_body cb with + match Global.body_of_constant_body Library.indirect_accessor cb with | Some(e, _) -> e | None -> failwith "This term has no value" diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst index e882ce6e88..b568160356 100644 --- a/doc/sphinx/addendum/extended-pattern-matching.rst +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -21,10 +21,10 @@ type is considered to be a variable. A variable name cannot occur more than once in a given pattern. It is recommended to start variable names by a lowercase letter. -If a pattern has the form ``(c x)`` where ``c`` is a constructor symbol and x +If a pattern has the form ``c x`` where ``c`` is a constructor symbol and x is a linear vector of (distinct) variables, it is called *simple*: it is the kind of pattern recognized by the basic version of match. On -the opposite, if it is a variable ``x`` or has the form ``(c p)`` with ``p`` not +the opposite, if it is a variable ``x`` or has the form ``c p`` with ``p`` not only made of variables, the pattern is called *nested*. A variable pattern matches any value, and the identifier is bound to @@ -216,7 +216,8 @@ Here is an example: end. -Here is another example using disjunctive subpatterns. +Nested disjunctive patterns are allowed, inside parentheses, with the +notation :n:`({+| @pattern})`, as in: .. coqtop:: in diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index 68f6d4008a..e58049b8d0 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -528,7 +528,7 @@ pass additional arguments such as ``using relation``. .. tacv:: setoid_reflexivity setoid_symmetry {? in @ident} setoid_transitivity - setoid_rewrite {? @orientation} @term {? at @occs} {? in @ident} + setoid_rewrite {? @orientation} @term {? at @occurrences} {? in @ident} setoid_replace @term with @term {? using relation @term} {? in @ident} {? by @tactic} :name: setoid_reflexivity; setoid_symmetry; setoid_transitivity; setoid_rewrite; setoid_replace @@ -567,13 +567,13 @@ Printing relations and morphisms Deprecated syntax and backward incompatibilities ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: Add Setoid @A @Aeq @ST as @ident +.. cmd:: Add Setoid @qualid__1 @qualid__2 @qualid__3 as @ident This command for declaring setoids and morphisms is also accepted due to backward compatibility reasons. - Here ``Aeq`` is a congruence relation without parameters, ``A`` is its carrier - and ``ST`` is an object of type (``Setoid_Theory A Aeq``) (i.e. a record + Here :n:`@qualid__2` is a congruence relation without parameters, :n:`@qualid__1` is its carrier + and :n:`@qualid__3` is an object of type (:n:`Setoid_Theory @qualid__1 @qualid__2`) (i.e. a record packing together the reflexivity, symmetry and transitivity lemmas). Notice that the syntax is not completely backward compatible since the identifier was not required. @@ -708,91 +708,65 @@ Definitions The generalized rewriting tactic is based on a set of strategies that can be combined to obtain custom rewriting procedures. Its set of strategies is based on Elan’s rewriting strategies :cite:`Luttik97specificationof`. Rewriting -strategies are applied using the tactic ``rewrite_strat s`` where ``s`` is a +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:: rewriting - s, t, u : `strategy` - : `lemma` - : `lemma_right_to_left` - : `failure` - : `identity` - : `reflexivity` - : `progress` - : `failure_catch` - : `composition` - : `left_biased_choice` - : `iteration_one_or_more` - : `iteration_zero_or_more` - : `one_subterm` - : `all_subterms` - : `innermost_first` - : `outermost_first` - : `bottom_up` - : `top_down` - : `apply_hint` - : `any_of_the_terms` - : `apply_reduction` - : `fold_expression` - -.. productionlist:: rewriting - strategy : ( `s` ) - lemma : `c` - lemma_right_to_left : <- `c` - failure : fail - identity : id - reflexivity : refl - progress : progress `s` - failure_catch : try `s` - composition : `s` ; `u` - left_biased_choice : choice `s` `t` - iteration_one_or_more : repeat `s` - iteration_zero_or_more : any `s` - one_subterm : subterm `s` - all_subterms : subterms `s` - innermost_first : innermost `s` - outermost_first : outermost `s` - bottom_up : bottomup `s` - top_down : topdown `s` - apply_hint : hints `hintdb` - any_of_the_terms : terms (`c`)+ - apply_reduction : eval `redexpr` - fold_expression : fold `c` - +.. 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 `redexpr` (apply reduction) + : fold `term` (unify) + : ( `strategy` ) Actually a few of these are defined in term of the others using a primitive fixpoint operator: -.. productionlist:: rewriting - try `s` : choice `s` `id` - any `s` : fix `u`. try (`s` ; `u`) - repeat `s` : `s` ; any `s` - bottomup s : fix `bu`. (choice (progress (subterms bu)) s) ; try bu - topdown s : fix `td`. (choice s (progress (subterms td))) ; try td - innermost s : fix `i`. (choice (subterm i) s) - outermost s : fix `o`. (choice s (subterm o)) +- :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))` The basic control strategy semantics are straightforward: strategies are applied to subterms of the term to rewrite, starting from the root of the term. The lemma strategies unify the left-hand-side of the lemma with the current subterm and on success rewrite it to the right- hand-side. Composition can be used to continue rewriting on the -current subterm. The fail strategy always fails while the identity +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 strategy and fails if no +``progress`` tests progress of the argument :token:`strategy` 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 +``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 strategy ``s`` to +The ``subterm`` and ``subterms`` strategies apply their argument :token:`strategy` to respectively one or all subterms of the current term under consideration, left-to-right. ``subterm`` stops at the first subterm for -which ``s`` made progress. The composite strategies ``innermost`` and ``outermost`` +which :token:`strategy` made progress. The composite strategies ``innermost`` and ``outermost`` perform a single innermost or outermost rewrite using their argument -strategy. Their counterparts ``bottomup`` and ``topdown`` perform as many +:token:`strategy`. Their counterparts ``bottomup`` and ``topdown`` perform as many rewritings as possible, starting from the bottom or the top of the term. @@ -802,15 +776,15 @@ lemmas at the current subterm. The ``terms`` strategy takes the lemma names directly as arguments. The ``eval`` strategy expects a reduction expression (see :ref:`performingcomputations`) and succeeds if it reduces the subterm under consideration. The ``fold`` strategy takes -a term ``c`` and tries to *unify* it to the current subterm, converting it to ``c`` -on success, it is stronger than the tactic ``fold``. +a :token:`term` and tries to *unify* it to the current subterm, converting it to :token:`term` +on success. It is stronger than the tactic ``fold``. Usage ~~~~~ -.. tacn:: rewrite_strat @s {? in @ident } +.. tacn:: rewrite_strat @strategy {? in @ident } :name: rewrite_strat Rewrite using the strategy s in hypothesis ident or the conclusion. diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 22ddcae584..45c74ab02a 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -299,9 +299,9 @@ optional tactic is replaced by the default one if not specified. Displays all remaining obligations. -.. cmd:: Obligation num {? of @ident} +.. cmd:: Obligation @num {? of @ident} - Start the proof of obligation num. + Start the proof of obligation :token:`num`. .. cmd:: Next Obligation {? of @ident} diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index 3b350d5dc0..3f4d5cc784 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -310,10 +310,10 @@ The syntax for adding a new ring is .. productionlist:: coq ring_mod : abstract | decidable `term` | morphism `term` : setoid `term` `term` - : constants [`ltac`] - : preprocess [`ltac`] - : postprocess [`ltac`] - : power_tac `term` [`ltac`] + : constants [ `tactic` ] + : preprocess [ `tactic` ] + : postprocess [ `tactic` ] + : power_tac `term` [ `tactic` ] : sign `term` : div `term` @@ -341,31 +341,31 @@ The syntax for adding a new ring is This modifier needs not be used if the setoid and morphisms have been declared. - constants [ :n:`@ltac` ] - specifies a tactic expression :n:`@ltac` that, given a + constants [ :n:`@tactic` ] + specifies a tactic expression :n:`@tactic` 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:`@ltac` ] - specifies a tactic :n:`@ltac` that is applied as a + preprocess [ :n:`@tactic` ] + specifies a tactic :n:`@tactic` 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:`@ltac` ] - specifies a tactic :n:`@ltac` that is applied as a final + postprocess [ :n:`@tactic` ] + specifies a tactic :n:`@tactic` 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:`@ltac` ] + power_tac :n:`@term` [ :n:`@tactic` ] 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 the specification of a power function (term has to be a proof of - ``Ring_theory.power_theory``) and :n:`@ltac` specifies a tactic expression + ``Ring_theory.power_theory``) and :n:`@tactic` specifies a tactic expression that, given a term, “abstracts” it into an object of type |N| whose interpretation via ``Cp_phi`` (the evaluation function of power coefficient) is the original term, or returns ``InitialRing.NotConstant`` diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 1aa2111816..395b5ce2d3 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -366,24 +366,32 @@ The syntax has been extended to allow users to explicitly bind names to universes and explicitly instantiate polymorphic definitions. .. cmd:: Universe @ident + Polymorphic Universe @ident 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 + command supports the ``Polymorphic`` flag only in sections, meaning the universe quantification will be discharged on each section definition independently. One cannot mix polymorphic and monomorphic declarations in the same section. -.. cmd:: Constraint @ident @ord @ident +.. cmd:: Constraint @universe_constraint + Polymorphic Constraint @universe_constraint - This command declares a new constraint between named universes. The - order relation :n:`@ord` can be one of :math:`<`, :math:`≤` or :math:`=`. If consistent, the constraint - is then enforced in the global environment. Like ``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. + This command declares a new constraint between named universes. + + .. productionlist:: coq + universe_constraint : `qualid` < `qualid` + : `qualid` <= `qualid` + : `qualid` = `qualid` + + 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. .. exn:: Undeclared universe @ident. :undocumented: diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 701c62cdce..db4ebd5e38 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -656,8 +656,8 @@ changes: attribute. - Removed deprecated commands ``Arguments Scope`` and ``Implicit - Arguments`` in favor of :cmd:`Arguments`, with the help of Jasper - Hugunin. + Arguments`` in favor of :cmd:`Arguments (scopes)` and + :cmd:`Arguments (implicits)`, with the help of Jasper Hugunin. - New flag :flag:`Uniform Inductive Parameters` by Jasper Hugunin to avoid repeating uniform parameters in constructor declarations. diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index ec3343dac6..53309cd313 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -181,7 +181,21 @@ suppress_warnings = ["misc.highlighting_failure"] todo_include_todos = False # Extra warnings, including undefined references -nitpicky = False +nitpicky = True + +nitpick_ignore = [ ('token', token) for token in [ + 'tactic', + # 142 occurrences currently sort of defined in the ltac chapter, + # but is it the right place? + 'module', + 'redexpr', + 'modpath', + 'dirpath', + 'collection', + 'term_pattern', + 'term_pattern_string', + 'command', + 'symbol' ]] # -- Options for HTML output ---------------------------------------------- diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index c48964d66c..c1af4d067f 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -603,11 +603,16 @@ The following experimental command is available when the ``FunInd`` library has The meaning of this declaration is to define a function ident, similarly to ``Fixpoint``. Like in ``Fixpoint``, the decreasing argument must be given (unless the function is not recursive), but it might not - necessarily be *structurally* decreasing. The point of the {} annotation + necessarily be *structurally* decreasing. The point of the :n:`{ @decrease_annot }` annotation is to name the decreasing argument *and* to describe which kind of decreasing criteria must be used to ensure termination of recursive calls. + .. productionlist:: + decrease_annot : struct `ident` + : measure `term` `ident` + : wf `term` `ident` + The ``Function`` construction also enjoys the ``with`` extension to define mutually recursive definitions. However, this feature does not work for non structurally recursive functions. @@ -616,31 +621,33 @@ 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. -Remark: To obtain the right principle, it is better to put rigid -parameters of the function as first arguments. For example it is -better to define plus like this: +.. note:: -.. coqtop:: reset none + To obtain the right principle, it is better to put rigid + parameters of the function as first arguments. For example it is + better to define plus like this: - Require Import FunInd. + .. coqtop:: reset none -.. coqtop:: all + Require Import FunInd. - Function plus (m n : nat) {struct n} : nat := - match n with - | 0 => m - | S p => S (plus m p) - end. + .. coqtop:: all -than like this: + Function plus (m n : nat) {struct n} : nat := + match n with + | 0 => m + | S p => S (plus m p) + end. -.. coqtop:: reset all + than like this: - Function plus (n m : nat) {struct n} : nat := - match n with - | 0 => m - | S p => S (plus p m) - end. + .. coqtop:: reset all + + Function plus (n m : nat) {struct n} : nat := + match n with + | 0 => m + | S p => S (plus p m) + end. *Limitations* @@ -710,7 +717,7 @@ used by ``Function``. A more precise description is given below. with :cmd:`Fixpoint`. Moreover the following are defined: + The same objects as above; - + The fixpoint equation of :token:`ident`: :n:`@ident_equation`. + + 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 @@ -1662,6 +1669,7 @@ Declaring Implicit Arguments of :token:`qualid`. .. cmd:: Arguments @qualid : clear implicits + :name: Arguments (clear implicits) This command clears implicit arguments. @@ -1738,6 +1746,7 @@ 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. @@ -1907,7 +1916,8 @@ This syntax extension is given in the following grammar: Renaming implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: Arguments @qualid {* @name} : @rename +.. cmd:: Arguments @qualid {* @name} : rename + :name: Arguments (rename) This command is used to redefine the names of implicit arguments. @@ -2293,7 +2303,7 @@ Printing universes 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(@names) +.. cmdv:: Print Universes Subgraph({+ @qualid }) :name: Print Universes Subgraph Prints the graph restricted to the requested names (adjusting diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 8acbcbec8f..ebaa6fde66 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -185,8 +185,7 @@ is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`. : `qualid` : _ : `num` - : ( `or_pattern` , … , `or_pattern` ) - or_pattern : `pattern` | … | `pattern` + : ( `pattern` | … | `pattern` ) Types diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index fed7111628..c48dd5b99e 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -32,22 +32,25 @@ The syntax of the tactic language is given below. See Chapter :ref:`gallinaspecificationlanguage` for a description of the BNF metasyntax used in these grammar rules. Various already defined entries will be used in this chapter: entries :token:`natural`, :token:`integer`, :token:`ident`, -:token:`qualid`, :token:`term`, :token:`cpattern` and :token:`atomic_tactic` +:token:`qualid`, :token:`term`, :token:`cpattern` and :token:`tactic` represent respectively the natural and integer numbers, the authorized identificators and qualified names, Coq terms and patterns and all the atomic -tactics described in Chapter :ref:`tactics`. The syntax of :token:`cpattern` is +tactics described in Chapter :ref:`tactics`. + +The syntax of :production:`cpattern` is the same as that of terms, but it is extended with pattern matching metavariables. In :token:`cpattern`, a pattern matching metavariable is -represented with the syntax :g:`?id` where :g:`id` is an :token:`ident`. The +represented with the syntax :n:`?@ident`. The notation :g:`_` can also be used to denote metavariable whose instance is -irrelevant. In the notation :g:`?id`, the identifier allows us to keep +irrelevant. In the notation :n:`?@ident`, the identifier allows us to keep instantiations and to make constraints whereas :g:`_` shows that we are not interested in what will be matched. On the right hand side of pattern matching clauses, the named metavariables are used without the question mark prefix. There is also a special notation for second-order pattern matching problems: in an -applicative pattern of the form :g:`@?id id1 … idn`, the variable id matches any -complex expression with (possible) dependencies in the variables :g:`id1 … idn` -and returns a functional term of the form :g:`fun id1 … idn => term`. +applicative pattern of the form :n:`%@?@ident @ident__1 … @ident__n`, +the variable :token:`ident` matches any complex expression with (possible) +dependencies in the variables :n:`@ident__i` and returns a functional term +of the form :n:`fun @ident__1 … ident__n => @term`. The main entry of the grammar is :n:`@expr`. This language is used in proof mode but it can also be used in toplevel definitions as shown below. @@ -121,6 +124,7 @@ mode but it can also be used in toplevel definitions as shown below. : solve [ `expr` | ... | `expr` ] : idtac [ `message_token` ... `message_token`] : fail [`natural`] [`message_token` ... `message_token`] + : gfail [`natural`] [`message_token` ... `message_token`] : fresh [ `component` … `component` ] : context `ident` [`term`] : eval `redexpr` in `term` @@ -132,7 +136,7 @@ mode but it can also be used in toplevel definitions as shown below. : guard `test` : assert_fails `tacexpr3` : assert_succeeds `tacexpr3` - : `atomic_tactic` + : `tactic` : `qualid` `tacarg` ... `tacarg` : `atom` atom : `qualid` @@ -582,11 +586,11 @@ Failing the call to :n:`fail @num` is not enclosed in a :n:`+` command, respecting the algebraic identity. - .. tacv:: fail {* message_token} + .. tacv:: fail {* @message_token} The given tokens are used for printing the failure message. - .. tacv:: fail @num {* message_token} + .. tacv:: fail @num {* @message_token} This is a combination of the previous variants. @@ -597,8 +601,8 @@ Failing Similarly, ``gfail`` fails even when used after ``all:`` and there are no goals left. See the example for clarification. - .. tacv:: gfail {* message_token} - gfail @num {* message_token} + .. tacv:: gfail {* @message_token} + gfail @num {* @message_token} These variants fail with an error message or an error level even if there are no goals left. Be careful however if Coq terms have to be @@ -964,7 +968,7 @@ system decide a name with the intro tactic is not so good since it is very awkward to retrieve the name the system gave. The following expression returns an identifier: -.. tacn:: fresh {* component} +.. tacn:: fresh {* @component} It evaluates to an identifier unbound in the goal. This fresh identifier is obtained by concatenating the value of the :n:`@component`\ s (each of them diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index aa603fc966..5f2e911ff9 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -124,13 +124,13 @@ Type declarations One can define new types by the following commands. -.. cmd:: Ltac2 Type @ltac2_typeparams @lident +.. cmd:: Ltac2 Type {? @ltac2_typeparams } @lident :name: Ltac2 Type This command defines an abstract type. It has no use for the end user and is dedicated to types representing data coming from the OCaml world. -.. cmdv:: Ltac2 Type {? rec} @ltac2_typeparams @lident := @ltac2_typedef +.. cmdv:: Ltac2 Type {? rec} {? @ltac2_typeparams } @lident := @ltac2_typedef This command defines a type with a manifest. There are four possible kinds of such definitions: alias, variant, record and open variant types. @@ -154,7 +154,7 @@ One can define new types by the following commands. Records are product types with named fields and eliminated by projection. Likewise they can be recursive if the `rec` flag is set. - .. cmdv:: Ltac2 Type @ltac2_typeparams @ltac2_qualid := [ @ltac2_constructordef ] + .. cmdv:: Ltac2 Type {? @ltac2_typeparams } @ltac2_qualid ::= [ @ltac2_constructordef ] Open variants are a special kind of variant types whose constructors are not statically defined, but can instead be extended dynamically. A typical example @@ -179,7 +179,7 @@ constructions from ML. : let `ltac2_var` := `ltac2_term` in `ltac2_term` : let rec `ltac2_var` := `ltac2_term` in `ltac2_term` : match `ltac2_term` with `ltac2_branch` ... `ltac2_branch` end - : `int` + : `integer` : `string` : `ltac2_term` ; `ltac2_term` : [| `ltac2_term` ; ... ; `ltac2_term` |] @@ -619,7 +619,7 @@ calls to term matching functions from the `Pattern` module. Internally, it is implemented thanks to a specific scope accepting the :n:`@constrmatching` syntax. Variables from the :n:`@constrpattern` are statically bound in the body of the branch, to -values of type `constr` for the variables from the :n:`@constr` pattern and to a +values of type `constr` for the variables from the :n:`@term` pattern and to a value of type `Pattern.context` for the variable :n:`@lident`. Note that unlike Ltac, only lowercase identifiers are valid as Ltac2 @@ -686,20 +686,22 @@ The following scopes are built-in. - :n:`list0(@ltac2_scope)`: - + if :n:`@ltac2_scope` parses :production:`entry`, parses :n:`(@entry__0, ..., @entry__n)` and produces - :n:`[@entry__0; ...; @entry__n]`. + + if :n:`@ltac2_scope` parses :n:`@quotentry`, + then it parses :n:`(@quotentry__0, ..., @quotentry__n)` and produces + :n:`[@quotentry__0; ...; @quotentry__n]`. - :n:`list0(@ltac2_scope, sep = @string__sep)`: - + if :n:`@ltac2_scope` parses :n:`@entry`, parses :n:`(@entry__0 @string__sep ... @string__sep @entry__n)` - and produces :n:`[@entry__0; ...; @entry__n]`. + + if :n:`@ltac2_scope` parses :n:`@quotentry`, + then it parses :n:`(@quotentry__0 @string__sep ... @string__sep @quotentry__n)` + and produce :n:`[@quotentry__0; ...; @quotentry__n]`. -- :n:`list1`: same as :n:`list0` (with or without separator) but parses :n:`{+ @entry}` instead - of :n:`{* @entry}`. +- :n:`list1`: same as :n:`list0` (with or without separator) but parses :n:`{+ @quotentry}` instead + of :n:`{* @quotentry}`. - :n:`opt(@ltac2_scope)` - + if :n:`@ltac2_scope` parses :n:`@entry`, parses :n:`{? @entry}` and produces either :n:`None` or + + if :n:`@ltac2_scope` parses :n:`@quotentry`, parses :n:`{? @quotentry}` and produces either :n:`None` or :n:`Some x` where :n:`x` is the parsed expression. - :n:`self`: diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 4a2f9c0db3..3f966755ca 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -175,12 +175,12 @@ list of assertion commands is given in :ref:`Assertions`. The command Use all section variables except the list of :token:`ident`. - .. cmdv:: Proof using @collection1 + @collection2 + .. cmdv:: Proof using @collection__1 + @collection__2 Use section variables from the union of both collections. See :ref:`nameaset` to know how to form a named collection. - .. cmdv:: Proof using @collection1 - @collection2 + .. cmdv:: Proof using @collection__1 - @collection__2 Use section variables which are in the first collection but not in the second one. @@ -202,10 +202,10 @@ Proof using options The following options modify the behavior of ``Proof using``. -.. opt:: Default Proof Using "@expression" +.. opt:: Default Proof Using "@collection" :name: Default Proof Using - Use :n:`@expression` as the default ``Proof using`` value. E.g. ``Set Default + Use :n:`@collection` as the default ``Proof using`` value. E.g. ``Set Default Proof Using "a b"`` will complete all ``Proof`` commands not followed by a ``using`` part with ``using a b``. @@ -220,7 +220,7 @@ The following options modify the behavior of ``Proof using``. Name a set of section hypotheses for ``Proof using`` ```````````````````````````````````````````````````` -.. cmd:: Collection @ident := @expression +.. cmd:: Collection @ident := @collection This can be used to name a set of section hypotheses, with the purpose of making ``Proof using`` annotations more diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index b19b0742c1..cc4976587d 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -455,7 +455,7 @@ the latter can be replaced by the open syntax ``of term`` or following extension of the binder syntax: .. prodn:: - binder += & @term | of @term + binder += {| & @term | of @term } Caveat: ``& T`` and ``of T`` abbreviations have to appear at the end of a binder list. For instance, the usual two-constructor polymorphic @@ -1340,7 +1340,7 @@ The general syntax of the discharging tactical ``:`` is: :undocumented: .. prodn:: - d_item ::= {? @occ_switch %| @clear_switch } @term + d_item ::= {? {| @occ_switch | @clear_switch } } @term .. prodn:: clear_switch ::= { {+ @ident } } @@ -1499,7 +1499,7 @@ side of an equation. The abstract tactic ``````````````````` -.. tacn:: abstract: {+ d_item} +.. tacn:: abstract: {+ @d_item} :name: abstract (ssreflect) This tactic assigns an abstract constant previously introduced with the @@ -1556,19 +1556,19 @@ whose general syntax is :undocumented: .. prodn:: - i_item ::= @i_pattern %| @s_item %| @clear_switch %| @i_view %| @i_block + i_item ::= {| @i_pattern | @s_item | @clear_switch | @i_view | @i_block } .. prodn:: - s_item ::= /= %| // %| //= + s_item ::= {| /= | // | //= } .. prodn:: - i_view ::= {? %{%} } /@term %| /ltac:( @tactic ) + i_view ::= {? %{%} } {| /@term | /ltac:( @tactic ) } .. prodn:: - i_pattern ::= @ident %| > %| _ %| ? %| * %| + %| {? @occ_switch } -> %| {? @occ_switch }<- %| [ {?| @i_item } ] %| - %| [: {+ @ident } ] + i_pattern ::= {| @ident | > | _ | ? | * | + | {? @occ_switch } {| -> | <- } | [ {?| @i_item } ] | - | [: {+ @ident } ] } .. prodn:: - i_block ::= [^ @ident ] %| [^~ @ident ] %| [^~ @num ] + i_block ::= {| [^ @ident ] | [^~ {| @ident | @num } ] } The ``=>`` tactical first executes :token:`tactic`, then the :token:`i_item`\s, left to right. An :token:`s_item` specifies a @@ -2390,7 +2390,7 @@ of a local definition during the generalization phase, the name of the local definition must be written between parentheses, like in ``rewrite H in H1 (def_n) H2.`` -.. tacv:: @tactic in {+ @clear_switch | {? @ } @ident | ( @ident ) | ( {? @ } @ident := @c_pattern ) } {? * } +.. tacv:: @tactic in {+ {| @clear_switch | {? @}@ident | ( @ident ) | ( {? @}@ident := @c_pattern ) } } {? * } This is the most general form of the ``in`` tactical. In its simplest form the last option lets one rename hypotheses that @@ -2492,7 +2492,7 @@ tactic: The behavior of the defective have tactic makes it possible to generalize it in the following general construction: -.. tacn:: have {* @i_item } {? @i_pattern } {? @s_item | {+ @ssr_binder } } {? : @term } {? := @term | by @tactic } +.. tacn:: have {* @i_item } {? @i_pattern } {? {| @s_item | {+ @ssr_binder } } } {? : @term } {? {| := @term | by @tactic } } :undocumented: Open syntax is supported for both :token:`term`. For the description @@ -2920,7 +2920,7 @@ Advanced generalization The complete syntax for the items on the left hand side of the ``/`` separator is the following one: -.. tacv:: wlog … : {? @clear_switch | {? @ } @ident | ( {? @ } @ident := @c_pattern) } / @term +.. tacv:: wlog … : {? {| @clear_switch | {? @}@ident | ( {? @}@ident := @c_pattern) } } / @term :undocumented: Clear operations are intertwined with generalization operations. This @@ -3020,13 +3020,13 @@ A rewrite step :token:`rstep` has the general form: rstep ::= {? @r_prefix } @r_item .. prodn:: - r_prefix ::= {? - } {? @mult } {? @occ_switch %| @clear_switch } {? [ @r_pattern ] } + r_prefix ::= {? - } {? @mult } {? {| @occ_switch | @clear_switch } } {? [ @r_pattern ] } .. prodn:: - r_pattern ::= @term %| in {? @ident in } @term %| %( @term in %| @term as %) @ident in @term + r_pattern ::= {| @term | in {? @ident in } @term | {| @term in | @term as } @ident in @term } .. prodn:: - r_item ::= {? / } @term %| @s_item + r_item ::= {| {? / } @term | @s_item } An :token:`r_prefix` contains annotations to qualify where and how the rewrite operation should be performed: @@ -3478,7 +3478,7 @@ efficient ones, e.g. for the purpose of a correctness proof. Wildcards vs abstractions ````````````````````````` -The rewrite tactic supports :token:`r_items` containing holes. For example, in +The rewrite tactic supports :token:`r_item`\s containing holes. For example, in the tactic ``rewrite (_ : _ * 0 = 0).`` the term ``_ * 0 = 0`` is interpreted as ``forall n : nat, n * 0 = 0.`` Anyway this tactic is *not* equivalent to @@ -3702,7 +3702,7 @@ The under tactic The convenience :tacn:`under` tactic supports the following syntax: -.. tacn:: under {? @r_prefix } @term {? => {+ @i_item}} {? do ( @tactic | [ {*| @tactic } ] ) } +.. tacn:: under {? @r_prefix } @term {? => {+ @i_item}} {? do {| @tactic | [ {*| @tactic } ] } } :name: under Operate under the context proved to be extensional by @@ -3753,7 +3753,7 @@ involves the following steps: 3. If so :tacn:`under` puts these n goals in head normal form (using the defective form of the tactic :tacn:`move`), then executes - the corresponding intro pattern :n:`@ipat__i` in each goal. + the corresponding intro pattern :n:`@i_pattern__i` in each goal. 4. Then :tacn:`under` checks that the first n subgoals are (quantified) equalities or double implications between a @@ -3802,11 +3802,11 @@ One-liner mode The Ltac expression: -:n:`under @term => [ @i_item__1 | … | @i_item__n ] do [ @tac__1 | … | @tac__n ].` +:n:`under @term => [ @i_item__1 | … | @i_item__n ] do [ @tactic__1 | … | @tactic__n ].` can be seen as a shorter form for the following expression: -:n:`(under @term) => [ @i_item__1 | … | @i_item__n | ]; [ @tac__1; over | … | @tac__n; over | cbv beta iota ].` +:n:`(under @term) => [ @i_item__1 | … | @i_item__n | ]; [ @tactic__1; over | … | @tactic__n; over | cbv beta iota ].` Notes: @@ -3819,14 +3819,14 @@ Notes: involving the `bigop` theory from the Mathematical Components library. + If there is only one tactic, the brackets can be omitted, e.g.: - :n:`under @term => i do @tac.` and that shorter form should be + :n:`under @term => i do @tactic.` and that shorter form should be preferred. + If the ``do`` clause is provided and the intro pattern is omitted, then the default :token:`i_item` ``*`` is applied to each branch. E.g., the Ltac expression: - :n:`under @term do [ @tac__1 | … | @tac__n ]` is equivalent to: - :n:`under @term => [ * | … | * ] do [ @tac__1 | … | @tac__n ]` + :n:`under @term do [ @tactic__1 | … | @tactic__n ]` is equivalent to: + :n:`under @term => [ * | … | * ] do [ @tactic__1 | … | @tactic__n ]` (and it can be noted here that the :tacn:`under` tactic performs a ``move.`` before processing the intro patterns ``=> [ * | … | * ]``). @@ -4237,7 +4237,7 @@ selecting a specific redex and has been described in the previous sections. We have seen so far that the possibility of selecting a redex using a term with holes is already a powerful means of redex selection. Similarly, any terms provided by the user in the more -complex forms of :token:`c_patterns` +complex forms of :token:`c_pattern`\s presented in the tables above can contain holes. @@ -5167,7 +5167,7 @@ Interpreting assumptions The general form of an assumption view tactic is: -.. tacv:: [move | case] / @term +.. tacv:: {| move | case } / @term :undocumented: The term , called the *view lemma* can be: @@ -5514,7 +5514,7 @@ Parameters |SSR| tactics .. prodn:: - d_tactic ::= elim %| case %| congr %| apply %| exact %| move + d_tactic ::= {| elim | case | congr | apply | exact | move } Notation scope @@ -5526,7 +5526,7 @@ Module name Natural number -.. prodn:: natural ::= @num %| @ident +.. prodn:: natural ::= {| @num | @ident } where :token:`ident` is an Ltac variable denoting a standard |Coq| numeral (should not be the name of a tactic which can be followed by a @@ -5535,7 +5535,7 @@ bracket ``[``, like ``do``, ``have``,…) Items and switches ~~~~~~~~~~~~~~~~~~ -.. prodn:: ssr_binder ::= @ident %| ( @ident {? : @term } ) +.. prodn:: ssr_binder ::= {| @ident | ( @ident {? : @term } ) } binder see :ref:`abbreviations_ssr`. @@ -5543,33 +5543,33 @@ binder see :ref:`abbreviations_ssr`. clear switch see :ref:`discharge_ssr` -.. prodn:: c_pattern ::= {? @term in %| @term as } @ident in @term +.. prodn:: c_pattern ::= {? {| @term in | @term as } } @ident in @term context pattern see :ref:`contextual_patterns_ssr` -.. prodn:: d_item ::= {? @occ_switch %| @clear_switch } {? @term %| ( @c_pattern ) } +.. prodn:: d_item ::= {? {| @occ_switch | @clear_switch } } {? {| @term | ( @c_pattern ) } } discharge item see :ref:`discharge_ssr` -.. prodn:: gen_item ::= {? @ } @ident %| ( @ident ) %| ( {? @ } @ident := @c_pattern ) +.. prodn:: gen_item ::= {| {? @ } @ident | ( @ident ) | ( {? @ } @ident := @c_pattern ) } generalization item see :ref:`structure_ssr` -.. prodn:: i_pattern ::= @ident %| > %| _ %| ? %| * %| + %| {? @occ_switch } -> %| {? @occ_switch } <- %| [ {?| @i_item } ] %| - %| [: {+ @ident } ] +.. prodn:: i_pattern ::= {| @ident | > | _ | ? | * | + | {? @occ_switch } {| -> | <- } | [ {?| @i_item } ] | - | [: {+ @ident } ] } intro pattern :ref:`introduction_ssr` -.. prodn:: i_item ::= @clear_switch %| @s_item %| @i_pattern %| @i_view %| @i_block +.. prodn:: i_item ::= {| @clear_switch | @s_item | @i_pattern | @i_view | @i_block } view :ref:`introduction_ssr` .. prodn:: - i_view ::= {? %{%} } /@term %| /ltac:( @tactic ) + i_view ::= {? %{%} } {| /@term | /ltac:( @tactic ) } intro block :ref:`introduction_ssr` .. prodn:: - i_block ::= [^ @ident ] %| [^~ @ident ] %| [^~ @num ] + i_block ::= {| [^ @ident ] | [^~ {| @ident | @num } ] } intro item see :ref:`introduction_ssr` @@ -5577,7 +5577,7 @@ intro item see :ref:`introduction_ssr` multiplier see :ref:`iteration_ssr` -.. prodn:: occ_switch ::= { {? + %| - } {* @num } } +.. prodn:: occ_switch ::= { {? {| + | - } } {* @num } } occur. switch see :ref:`occurrence_selection_ssr` @@ -5585,19 +5585,19 @@ occur. switch see :ref:`occurrence_selection_ssr` multiplier see :ref:`iteration_ssr` -.. prodn:: mult_mark ::= ? %| ! +.. prodn:: mult_mark ::= {| ? | ! } multiplier mark see :ref:`iteration_ssr` -.. prodn:: r_item ::= {? / } @term %| @s_item +.. prodn:: r_item ::= {| {? / } @term | @s_item } rewrite item see :ref:`rewriting_ssr` -.. prodn:: r_prefix ::= {? - } {? @int_mult } {? @occ_switch %| @clear_switch } {? [ @r_pattern ] } +.. prodn:: r_prefix ::= {? - } {? @int_mult } {? {| @occ_switch | @clear_switch } } {? [ @r_pattern ] } rewrite prefix see :ref:`rewriting_ssr` -.. prodn:: r_pattern ::= @term %| @c_pattern %| in {? @ident in } @term +.. prodn:: r_pattern ::= {| @term | @c_pattern | in {? @ident in } @term } rewrite pattern see :ref:`rewriting_ssr` @@ -5605,7 +5605,7 @@ rewrite pattern see :ref:`rewriting_ssr` rewrite step see :ref:`rewriting_ssr` -.. prodn:: s_item ::= /= %| // %| //= +.. prodn:: s_item ::= {| /= | // | //= } simplify switch see :ref:`introduction_ssr` @@ -5640,7 +5640,7 @@ respectively. rewrite (see :ref:`rewriting_ssr`) -.. tacn:: under {? @r_prefix } @term {? => {+ @i_item}} {? do ( @tactic | [ {*| @tactic } ] )} +.. tacn:: under {? @r_prefix } @term {? => {+ @i_item}} {? do {| @tactic | [ {*| @tactic } ] } } under (see :ref:`under_ssr`) @@ -5648,8 +5648,8 @@ respectively. over (see :ref:`over_ssr`) -.. tacn:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @ssr_binder } } {? : @term } := @term - have {* @i_item } {? @i_pattern } {? @s_item %| {+ @ssr_binder } } : @term {? by @tactic } +.. tacn:: have {* @i_item } {? @i_pattern } {? {| @s_item | {+ @ssr_binder } } } {? : @term } := @term + have {* @i_item } {? @i_pattern } {? {| @s_item | {+ @ssr_binder } } } : @term {? by @tactic } have suff {? @clear_switch } {? @i_pattern } {? : @term } := @term have suff {? @clear_switch } {? @i_pattern } : @term {? by @tactic } gen have {? @ident , } {? @i_pattern } : {+ @gen_item } / @term {? by @tactic } @@ -5658,7 +5658,7 @@ respectively. forward chaining (see :ref:`structure_ssr`) -.. tacn:: wlog {? suff } {? @i_item } : {* @gen_item %| @clear_switch } / @term +.. tacn:: wlog {? suff } {? @i_item } : {* {| @gen_item | @clear_switch } } / @term specializing (see :ref:`structure_ssr`) @@ -5710,7 +5710,7 @@ discharge :ref:`discharge_ssr` introduction see :ref:`introduction_ssr` -.. prodn:: tactic += @tactic in {+ @gen_item %| @clear_switch } {? * } +.. prodn:: tactic += @tactic in {+ {| @gen_item | @clear_switch } } {? * } localization see :ref:`localization_ssr` diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 2ee23df019..fa6d62ffa2 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -131,16 +131,17 @@ include :tacn:`assert`, :tacn:`intros` and :tacn:`destruct`. simple_intropattern_closed : `naming_intropattern` : _ : `or_and_intropattern` - : `equality_intropattern` + : `rewriting_intropattern` + : `injection_intropattern` naming_intropattern : `ident` : ? : ?`ident` or_and_intropattern : [ `intropattern_list` | ... | `intropattern_list` ] : ( `simple_intropattern` , ... , `simple_intropattern` ) : ( `simple_intropattern` & ... & `simple_intropattern` ) - equality_intropattern : -> + rewriting_intropattern : -> : <- - : [= `intropattern_list` ] + injection_intropattern : [= `intropattern_list` ] or_and_intropattern_loc : `or_and_intropattern` : `ident` @@ -462,7 +463,7 @@ Occurrence sets and occurrence clauses An occurrence clause is a modifier to some tactics that obeys the following syntax: - .. productionlist:: sentence + .. productionlist:: coq occurrence_clause : in `goal_occurrences` goal_occurrences : [`ident` [`at_occurrences`], ... , `ident` [`at_occurrences`] [|- [* [`at_occurrences`]]]] : * |- [* [`at_occurrences`]] @@ -2127,7 +2128,7 @@ and an explanation of the underlying technique. :name: discriminate This tactic proves any goal from an assumption stating that two - structurally different :n:`@terms` of an inductive set are equal. For + structurally different :n:`@term`\s of an inductive set are equal. For example, from :g:`(S (S O))=(S O)` we can derive by absurdity any proposition. @@ -2285,6 +2286,18 @@ and an explanation of the underlying technique. to the number of new equalities. The original equality is erased if it corresponds to a hypothesis. + .. tacv:: injection @term {? with @bindings_list} as @injection_intropattern + injection @num as @injection_intropattern + injection as @injection_intropattern + einjection @term {? with @bindings_list} as @injection_intropattern + einjection @num as @injection_intropattern + einjection as @injection_intropattern + + These are equivalent to the previous variants but using instead the + syntax :token:`injection_intropattern` which :tacn:`intros` + uses. In particular :n:`as [= {+ @simple_intropattern}]` behaves + the same as :n:`as {+ @simple_intropattern}`. + .. flag:: Structural Injection This option ensure that :n:`injection @term` erases the original hypothesis @@ -2294,7 +2307,7 @@ and an explanation of the underlying technique. .. flag:: Keep Proof Equalities - By default, :tacn:`injection` only creates new equalities between :n:`@terms` + By default, :tacn:`injection` only creates new equalities between :n:`@term`\s whose type is in sort :g:`Type` or :g:`Set`, thus implementing a special behavior for objects that are proofs of a statement in :g:`Prop`. This option controls this behavior. @@ -2703,42 +2716,42 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. Uses the equality :n:`@term`:sub:`1` :n:`= @term` :sub:`2` from right to left - .. tacv:: rewrite @term in clause + .. tacv:: rewrite @term in @goal_occurrences - Analogous to :n:`rewrite @term` but rewriting is done following clause - (similarly to :ref:`performing computations <performingcomputations>`). For instance: + Analogous to :n:`rewrite @term` but rewriting is done following + the clause :token:`goal_occurrences`. For instance: - + :n:`rewrite H in H`:sub:`1` will rewrite `H` in the hypothesis - `H`:sub:`1` instead of the current goal. - + :n:`rewrite H in H`:sub:`1` :g:`at 1, H`:sub:`2` :g:`at - 2 |- *` means - :n:`rewrite H; rewrite H in H`:sub:`1` :g:`at 1; rewrite H in H`:sub:`2` :g:`at - 2.` + + :n:`rewrite H in H'` will rewrite `H` in the hypothesis + ``H'`` instead of the current goal. + + :n:`rewrite H in H' at 1, H'' at - 2 |- *` means + :n:`rewrite H; rewrite H in H' at 1; rewrite H in H'' at - 2.` In particular a failure will happen if any of these three simpler tactics fails. - + :n:`rewrite H in * |-` will do :n:`rewrite H in H`:sub:`i` for all hypotheses - :g:`H`:sub:`i` different from :g:`H`. + + :n:`rewrite H in * |-` will do :n:`rewrite H in H'` for all hypotheses + :g:`H'` different from :g:`H`. A success will happen as soon as at least one of these simpler tactics succeeds. + :n:`rewrite H in *` is a combination of :n:`rewrite H` and :n:`rewrite H in * |-` that succeeds if at least one of these two tactics succeeds. Orientation :g:`->` or :g:`<-` can be inserted before the :token:`term` to rewrite. - .. tacv:: rewrite @term at occurrences + .. tacv:: rewrite @term at @occurrences - Rewrite only the given occurrences of :token:`term`. Occurrences are + Rewrite only the given :token:`occurrences` of :token:`term`. Occurrences are specified from left to right as for pattern (:tacn:`pattern`). The rewrite is always performed using setoid rewriting, even for Leibniz’s equality, so one has to ``Import Setoid`` to use this variant. - .. tacv:: rewrite @term by tactic + .. tacv:: rewrite @term by @tactic Use tactic to completely solve the side-conditions arising from the :tacn:`rewrite`. - .. tacv:: rewrite {+, @term} + .. tacv:: rewrite {+, @orientation @term} {? in @ident } Is equivalent to the `n` successive tactics :n:`{+; rewrite @term}`, each one - working on the first subgoal generated by the previous one. Orientation - :g:`->` or :g:`<-` can be inserted before each :token:`term` to rewrite. One + working on the first subgoal generated by the previous one. An :production:`orientation` + ``->`` or ``<-`` can be inserted before each :token:`term` to rewrite. One unique clause can be added at the end after the keyword in; it will then affect all rewrite operations. @@ -2799,13 +2812,14 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has the form :n:`@term’ = @term` - .. tacv:: replace @term {? with @term} in clause {? by @tactic} - replace -> @term in clause - replace <- @term in clause + .. tacv:: replace @term {? with @term} in @goal_occurrences {? by @tactic} + replace -> @term in @goal_occurrences + replace <- @term in @goal_occurrences - Acts as before but the replacements take place in the specified clause (see - :ref:`performingcomputations`) and not only in the conclusion of the goal. The - clause argument must not contain any ``type of`` nor ``value of``. + Acts as before but the replacements take place in the specified clauses + (:token:`goal_occurrences`) (see :ref:`performingcomputations`) and not + only in the conclusion of the goal. The clause argument must not contain + any ``type of`` nor ``value of``. .. tacv:: cutrewrite <- (@term = @term’) :name: cutrewrite @@ -2893,7 +2907,7 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. This applies :n:`stepl @term` then applies :token:`tactic` to the second goal. - .. tacv:: stepr @term stepr @term by tactic + .. tacv:: stepr @term by @tactic :name: stepr This behaves as :tacn:`stepl` but on the right-hand-side of the binary @@ -3064,7 +3078,7 @@ the conversion in hypotheses :n:`{+ @ident}`. .. tacv:: native_compute :name: native_compute - This tactic evaluates the goal by compilation to Objective Caml as described + This tactic evaluates the goal by compilation to OCaml as described in :cite:`FullReduction`. If Coq is running in native code, it can be typically two to five times faster than ``vm_compute``. Note however that the compilation cost is higher, so it is worth using only for intensive @@ -3159,7 +3173,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` vernacular command. + ``/`` symbol in the argument list of the :cmd:`Arguments <Arguments (implicits)>` vernacular command. .. example:: @@ -3230,8 +3244,8 @@ the conversion in hypotheses :n:`{+ @ident}`. .. tacv:: simpl @pattern - This applies ``simpl`` only to the subterms matching :n:`@pattern` in the - current goal. + This applies :tacn:`simpl` only to the subterms matching + :n:`@pattern` in the current goal. .. tacv:: simpl @pattern at {+ @num} @@ -3264,50 +3278,77 @@ the conversion in hypotheses :n:`{+ @ident}`. This tactic applies to any goal. The argument qualid must denote a defined transparent constant or local definition (see - :ref:`gallina-definitions` and :ref:`vernac-controlling-the-reduction-strategies`). The tactic - ``unfold`` applies the :math:`\delta` rule to each occurrence of the constant to which - :n:`@qualid` refers in the current goal and then replaces it with its - :math:`\beta`:math:`\iota`-normal form. + :ref:`gallina-definitions` and + :ref:`vernac-controlling-the-reduction-strategies`). The tactic + :tacn:`unfold` applies the :math:`\delta` rule to each occurrence of + the constant to which :n:`@qualid` refers in the current goal and + then replaces it with its :math:`\beta`:math:`\iota`-normal form. -.. exn:: @qualid does not denote an evaluable constant. - :undocumented: + .. exn:: @qualid does not denote an evaluable constant. -.. tacv:: unfold @qualid in @ident + This error is frequent when trying to unfold something that has + defined as an inductive type (or constructor) and not as a + definition. - Replaces :n:`@qualid` in hypothesis :n:`@ident` with its definition - and replaces the hypothesis with its :math:`\beta`:math:`\iota` normal form. + .. example:: -.. tacv:: unfold {+, @qualid} + .. coqtop:: abort all fail - Replaces *simultaneously* :n:`{+, @qualid}` with their definitions and - replaces the current goal with its :math:`\beta`:math:`\iota` normal form. + Goal 0 <= 1. + unfold le. -.. tacv:: unfold {+, @qualid at {+, @num }} + This error can also be raised if you are trying to unfold + something that has been marked as opaque. - The lists :n:`{+, @num}` specify the occurrences of :n:`@qualid` to be - unfolded. Occurrences are located from left to right. + .. example:: - .. exn:: Bad occurrence number of @qualid. - :undocumented: + .. coqtop:: abort all fail - .. exn:: @qualid does not occur. - :undocumented: + Opaque Nat.add. + Goal 1 + 0 = 1. + unfold Nat.add. + + .. tacv:: unfold @qualid in @goal_occurrences -.. tacv:: unfold @string + Replaces :n:`@qualid` in hypothesis (or hypotheses) designated + by :token:`goal_occurrences` with its definition and replaces + the hypothesis with its :math:`\beta`:math:`\iota` normal form. - If :n:`@string` denotes the discriminating symbol of a notation (e.g. "+") or - an expression defining a notation (e.g. `"_ + _"`), and this notation refers to an unfoldable constant, then the - tactic unfolds it. + .. tacv:: unfold {+, @qualid} -.. tacv:: unfold @string%key + Replaces :n:`{+, @qualid}` with their definitions and replaces + the current goal with its :math:`\beta`:math:`\iota` normal + form. - This is variant of :n:`unfold @string` where :n:`@string` gets its - interpretation from the scope bound to the delimiting key :n:`key` - instead of its default interpretation (see :ref:`Localinterpretationrulesfornotations`). -.. tacv:: unfold {+, qualid_or_string at {+, @num}} + .. tacv:: unfold {+, @qualid at @occurrences } - This is the most general form, where :n:`qualid_or_string` is either a - :n:`@qualid` or a :n:`@string` referring to a notation. + The list :token:`occurrences` specify the occurrences of + :n:`@qualid` to be unfolded. Occurrences are located from left + to right. + + .. exn:: Bad occurrence number of @qualid. + :undocumented: + + .. exn:: @qualid does not occur. + :undocumented: + + .. tacv:: unfold @string + + If :n:`@string` denotes the discriminating symbol of a notation + (e.g. "+") or an expression defining a notation (e.g. `"_ + + _"`), and this notation denotes an application whose head symbol + is an unfoldable constant, then the tactic unfolds it. + + .. tacv:: unfold @string%@ident + + This is variant of :n:`unfold @string` where :n:`@string` gets + its interpretation from the scope bound to the delimiting key + :token:`ident` instead of its default interpretation (see + :ref:`Localinterpretationrulesfornotations`). + + .. tacv:: unfold {+, {| @qualid | @string{? %@ident } } {? at @occurrences } } {? in @goal_occurrences } + + This is the most general form. .. tacn:: fold @term :name: fold @@ -3382,14 +3423,13 @@ the conversion in hypotheses :n:`{+ @ident}`. Conversion tactics applied to hypotheses ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. tacn:: conv_tactic in {+, @ident} +.. tacn:: @tactic in {+, @ident} - Applies the conversion tactic :n:`conv_tactic` to the hypotheses - :n:`{+ @ident}`. The tactic :n:`conv_tactic` is any of the conversion tactics - listed in this section. + Applies :token:`tactic` (any of the conversion tactics listed in this + section) to the hypotheses :n:`{+ @ident}`. - If :n:`@ident` is a local definition, then :n:`@ident` can be replaced by - (type of :n:`@ident`) to address not the body but the type of the local + If :token:`ident` is a local definition, then :token:`ident` can be replaced by + :n:`type of @ident` to address not the body but the type of the local definition. Example: :n:`unfold not in (type of H1) (type of H3)`. @@ -3447,9 +3487,9 @@ Automation :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` for the list of pre-defined databases and the way to create or extend a database. - .. tacv:: auto using {+ @ident__i} {? with {+ @ident } } + .. tacv:: auto using {+ @qualid__i} {? with {+ @ident } } - Uses lemmas :n:`@ident__i` in addition to hints. If :n:`@ident` is an + Uses lemmas :n:`@qualid__i` in addition to hints. If :n:`@qualid` is an inductive type, it is the collection of its constructors which are added as hints. @@ -3457,8 +3497,8 @@ Automation The hints passed through the `using` clause are used in the same way as if they were passed through a hint database. Consequently, - they use a weaker version of :tacn:`apply` and :n:`auto using @ident` - may fail where :n:`apply @ident` succeeds. + they use a weaker version of :tacn:`apply` and :n:`auto using @qualid` + may fail where :n:`apply @qualid` succeeds. Given that this can be seen as counter-intuitive, it could be useful to have an option to use full-blown :tacn:`apply` for lemmas passed @@ -3476,7 +3516,7 @@ Automation Behaves like :tacn:`auto` but shows the tactics it tries to solve the goal, including failing paths. - .. tacv:: {? info_}auto {? @num} {? using {+ @lemma}} {? with {+ @ident}} + .. tacv:: {? info_}auto {? @num} {? using {+ @qualid}} {? with {+ @ident}} This is the most general form, combining the various options. @@ -3489,10 +3529,10 @@ Automation .. tacv:: trivial with {+ @ident} trivial with * - trivial using {+ @lemma} + trivial using {+ @qualid} debug trivial info_trivial - {? info_}trivial {? using {+ @lemma}} {? with {+ @ident}} + {? info_}trivial {? using {+ @qualid}} {? with {+ @ident}} :name: _; _; _; debug trivial; info_trivial; _ :undocumented: @@ -3531,7 +3571,7 @@ Automation Note that ``ex_intro`` should be declared as a hint. - .. tacv:: {? info_}eauto {? @num} {? using {+ @lemma}} {? with {+ @ident}} + .. tacv:: {? info_}eauto {? @num} {? using {+ @qualid}} {? with {+ @ident}} The various options for :tacn:`eauto` are the same as for :tacn:`auto`. @@ -3550,9 +3590,9 @@ Automation This tactic unfolds constants that were declared through a :cmd:`Hint Unfold` in the given databases. -.. tacv:: autounfold with {+ @ident} in clause +.. tacv:: autounfold with {+ @ident} in @goal_occurrences - Performs the unfolding in the given clause. + Performs the unfolding in the given clause (:token:`goal_occurrences`). .. tacv:: autounfold with * @@ -3592,10 +3632,9 @@ Automation Performs all the rewritings in hypothesis :n:`@qualid` applying :n:`@tactic` to the main subgoal after each rewriting step. -.. tacv:: autorewrite with {+ @ident} in @clause +.. tacv:: autorewrite with {+ @ident} in @goal_occurrences - Performs all the rewriting in the clause :n:`@clause`. The clause argument - must not contain any ``type of`` nor ``value of``. + Performs all the rewriting in the clause :n:`@goal_occurrences`. .. seealso:: @@ -3666,10 +3705,11 @@ automatically created. from the order in which they were inserted, making this implementation observationally different from the legacy one. -The general command to add a hint to some databases :n:`{+ @ident}` is - .. cmd:: Hint @hint_definition : {+ @ident} + The general command to add a hint to some databases :n:`{+ @ident}`. + The various possible :production:`hint_definition`\s are given below. + .. cmdv:: Hint @hint_definition No database name is given: the hint is registered in the ``core`` database. @@ -3718,7 +3758,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is before, the tactic actually used is a restricted version of :tacn:`apply`). - .. cmdv:: Resolve <- @term + .. cmdv:: Hint Resolve <- @term Adds the right-to-left implication of an equivalence as a hint. @@ -3738,7 +3778,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is .. exn:: @term cannot be used as a hint :undocumented: - .. cmdv:: Immediate {+ @term} : @ident + .. cmdv:: Hint Immediate {+ @term} : @ident Adds each :n:`Hint Immediate @term`. @@ -3981,7 +4021,7 @@ use one or several databases specific to your development. Adds the rewriting rules :n:`{+ @term}` with a right-to-left orientation in the bases :n:`{+ @ident}`. -.. cmd:: Hint Rewrite {+ @term} using tactic : {+ @ident} +.. cmd:: Hint Rewrite {+ @term} using @tactic : {+ @ident} When the rewriting rules :n:`{+ @term}` in :n:`{+ @ident}` will be used, the tactic ``tactic`` will be applied to the generated subgoals, the main subgoal @@ -4202,7 +4242,7 @@ some incompatibilities. Adds lemmas from :tacn:`auto` hint bases :n:`{+ @ident}` to the proof-search environment. -.. tacv:: firstorder tactic using {+ @qualid} with {+ @ident} +.. tacv:: firstorder @tactic using {+ @qualid} with {+ @ident} This combines the effects of the different variants of :tacn:`firstorder`. @@ -4243,10 +4283,10 @@ some incompatibilities. congruence. Qed. -.. tacv:: congruence n +.. tacv:: congruence @num - Tries to add at most `n` instances of hypotheses stating quantified equalities - to the problem in order to solve it. A bigger value of `n` does not make + Tries to add at most :token:`num` instances of hypotheses stating quantified equalities + to the problem in order to solve it. A bigger value of :token:`num` does not make success slower, only failure. You might consider adding some lemmas as hypotheses using assert in order for :tacn:`congruence` to use them. @@ -4556,14 +4596,14 @@ Automating .. _btauto_grammar: .. productionlist:: sentence - t : `x` - : true - : false - : orb `t` `t` - : andb `t` `t` - : xorb `t` `t` - : negb `t` - : if `t` then `t` else `t` + btauto_term : `ident` + : true + : false + : orb `btauto_term` `btauto_term` + : andb `btauto_term` `btauto_term` + : xorb `btauto_term` `btauto_term` + : negb `btauto_term` + : if `btauto_term` then `btauto_term` else `btauto_term` Whenever the formula supplied is not a tautology, it also provides a counter-example. diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 26dc4e02cf..5f3e82938d 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -189,18 +189,13 @@ Requests to the environment This command displays the type of :n:`@term`. When called in proof mode, the term is checked in the local context of the current subgoal. - - .. TODO : selector is not a syntax entry - .. cmdv:: @selector: Check @term This variant specifies on which subgoal to perform typing (see Section :ref:`invocation-of-tactics`). -.. TODO : convtactic is not a syntax entry - -.. cmd:: Eval @convtactic in @term +.. cmd:: Eval @redexpr in @term This command performs the specified reduction on :n:`@term`, and displays the resulting term with its type. The term to be reduced may depend on @@ -264,11 +259,11 @@ Requests to the environment main symbol as in `"+"` or by its notation’s string as in `"_ + _"` or `"_ 'U' _"`, see Section :ref:`notations`), the command works like ``Search`` :n:`@qualid`. - .. cmdv:: Search @string%@key + .. cmdv:: Search @string%@ident The string string must be a notation or the main symbol of a notation which is then interpreted in the scope bound to - the delimiting key :n:`@key` (see Section :ref:`LocalInterpretationRulesForNotations`). + the delimiting key :token:`ident` (see Section :ref:`LocalInterpretationRulesForNotations`). .. cmdv:: Search @term_pattern @@ -1132,6 +1127,8 @@ described first. with lower level is expanded first. In case of a tie, the second one (appearing in the cast type) is expanded. + .. prodn:: level ::= {| opaque | @num | expand } + Levels can be one of the following (higher to lower): + ``opaque`` : level of opaque constants. They cannot be expanded by @@ -1167,19 +1164,19 @@ described first. Print all the currently non-transparent strategies. -.. cmd:: Declare Reduction @ident := @convtactic +.. cmd:: Declare Reduction @ident := @redexpr This command allows giving a short name to a reduction expression, for - instance lazy beta delta [foo bar]. This short name can then be used + instance ``lazy beta delta [foo bar]``. This short name can then be used in :n:`Eval @ident in` or ``eval`` directives. This command accepts the - Local modifier, for discarding this reduction name at the end of the - file or module. For the moment the name cannot be qualified. In + ``Local`` modifier, for discarding this reduction name at the end of the + file or module. For the moment, the name is not qualified. In particular declaring the same name in several modules or in several - functor applications will be refused if these declarations are not + functor applications will be rejected if these declarations are not local. The name :n:`@ident` cannot be used directly as an Ltac tactic, but - nothing prevents the user to also perform a - :n:`Ltac @ident := @convtactic`. + nothing prevents the user from also performing a + :n:`Ltac @ident := @redexpr`. .. seealso:: :ref:`performingcomputations` @@ -1208,7 +1205,7 @@ Controlling the locality of commands 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 sections and current module if the command occurs in a section. As an example, - the :cmd:`Arguments`, :cmd:`Ltac` or :cmd:`Notation` commands belong + the :cmd:`Arguments <Arguments (implicits)>`, :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 applicable to them. diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 6da42f4a48..9b381cb9de 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -109,7 +109,7 @@ the associativity of disjunction and conjunction, so let us apply for instance a right associativity (which is the choice of Coq). Precedence levels and associativity rules of notations have to be -given between parentheses in a list of modifiers that the :cmd:`Notation` +given between parentheses in a list of :token:`modifiers` that the :cmd:`Notation` command understands. Here is how the previous examples refine. .. coqtop:: in @@ -249,7 +249,7 @@ bar of the notation. Check (sig (fun x : nat => x=x)). The second, more powerful control on printing is by using the format -modifier. Here is an example +:token:`modifier`. Here is an example .. coqtop:: all @@ -298,8 +298,8 @@ expression is performed at definition time. Type checking is done only at the time of use of the notation. .. note:: Sometimes, a notation is expected only for the parser. To do - so, the option ``only parsing`` is allowed in the list of modifiers - of :cmd:`Notation`. Conversely, the ``only printing`` modifier can be + so, the option ``only parsing`` is allowed in the list of :token:`modifiers` + of :cmd:`Notation`. Conversely, the ``only printing`` :token:`modifier` can be used to declare that a notation should only be used for printing and should not declare a parsing rule. In particular, such notations do not modify the parser. @@ -310,11 +310,11 @@ The Infix command The :cmd:`Infix` command is a shortening for declaring notations of infix symbols. -.. cmd:: Infix "@symbol" := @term ({+, @modifier}). +.. cmd:: Infix "@symbol" := @term {? (@modifiers) }. This command is equivalent to - :n:`Notation "x @symbol y" := (@term x y) ({+, @modifier}).` + :n:`Notation "x @symbol y" := (@term x y) {? (@modifiers) }.` where ``x`` and ``y`` are fresh names. Here is an example. @@ -437,7 +437,7 @@ application of the notation: Check sigma z : nat, z = 0. -Notice the modifier ``x ident`` in the declaration of the +Notice the :token:`modifier` ``x ident`` in the declaration of the notation. It tells to parse :g:`x` as a single identifier. Binders bound in the notation and parsed as patterns @@ -457,7 +457,7 @@ binder. Here is an example: Check subset '(x,y), x+y=0. -The modifier ``p pattern`` in the declaration of the notation tells to parse +The :token:`modifier` ``p pattern`` in the declaration of the notation tells to parse :g:`p` as a pattern. Note that a single variable is both an identifier and a pattern, so, e.g., the following also works: @@ -467,7 +467,7 @@ pattern, so, e.g., the following also works: If one wants to prevent such a notation to be used for printing when the pattern is reduced to a single identifier, one has to use instead -the modifier ``p strict pattern``. For parsing, however, a +the :token:`modifier` ``p strict pattern``. For parsing, however, a ``strict pattern`` will continue to include the case of a variable. Here is an example showing the difference: @@ -507,7 +507,7 @@ that ``x`` is parsed as a term at level 99 (as done in the notation for :g:`sumbool`), but that this term has actually to be an identifier. The notation :g:`{ x | P }` is already defined in the standard -library with the ``as ident`` modifier. We cannot redefine it but +library with the ``as ident`` :token:`modifier`. We cannot redefine it but one can define an alternative notation, say :g:`{ p such that P }`, using instead ``as pattern``. @@ -527,7 +527,7 @@ is just an identifier, one could have said ``p at level 99 as strict pattern``. Note also that in the absence of a ``as ident``, ``as strict pattern`` or -``as pattern`` modifiers, the default is to consider sub-expressions occurring +``as pattern`` :token:`modifier`\s, the default is to consider sub-expressions occurring in binding position and parsed as terms to be ``as ident``. .. _NotationsWithBinders: @@ -628,7 +628,7 @@ except that in the iterator position of the binding variable of a ``fun`` or a ``forall``. To specify that the part “``x .. y``” of the notation parses a sequence of -binders, ``x`` and ``y`` must be marked as ``binder`` in the list of modifiers +binders, ``x`` and ``y`` must be marked as ``binder`` in the list of :token:`modifiers` of the notation. The binders of the parsed sequence are used to fill the occurrences of the first placeholder of the iterating pattern which is repeatedly nested as many times as the number of binders generated. If ever the @@ -678,7 +678,7 @@ Predefined entries ~~~~~~~~~~~~~~~~~~ By default, sub-expressions are parsed as terms and the corresponding -grammar entry is called :n:`@constr`. However, one may sometimes want +grammar entry is called ``constr``. However, one may sometimes want to restrict the syntax of terms in a notation. For instance, the following notation will accept to parse only global reference in position of :g:`x`: @@ -866,16 +866,17 @@ notations are given below. The optional :production:`scope` is described in :ref:`Scopes`. .. productionlist:: coq - notation : [Local] Notation `string` := `term` [`modifiers`] [: `scope`]. - : [Local] Infix `string` := `qualid` [`modifiers`] [: `scope`]. - : [Local] Reserved Notation `string` [`modifiers`] . + 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 `cofix_body` [`decl_notation`] with … with `cofix_body` [`decl_notation`]. : [Local] Declare Custom Entry `ident`. decl_notation : [where `string` := `term` [: `scope`] and … and `string` := `term` [: `scope`]]. - modifiers : at level `num` + modifiers : `modifier`, … , `modifier` + modifier : at level `num` : in custom `ident` : in custom `ident` at level `num` : `ident` , … , `ident` at level `num` [`binderinterp`] @@ -924,6 +925,17 @@ notations are given below. The optional :production:`scope` is described in given to some notation, say ``"{ y } & { z }"`` in fact applies to the underlying ``"{ x }"``\-free rule which is ``"y & z"``). +.. note:: Notations such as ``"( p | q )"`` (or starting with ``"( x | "``, + more generally) are deprecated as they conflict with the syntax for + nested disjunctive patterns (see :ref:`extendedpatternmatching`), + and are not honored in pattern expressions. + + .. warn:: Use of @string Notation is deprecated as it is inconsistent with pattern syntax. + + This warning is disabled by default to avoid spurious diagnostics + due to legacy notation in the Coq standard library. + It can be turned on with the ``-w disj-pattern-notation`` flag. + Persistence of notations ++++++++++++++++++++++++ @@ -1032,11 +1044,11 @@ Local opening of an interpretation scope +++++++++++++++++++++++++++++++++++++++++ It is possible to locally extend the interpretation scope stack using the syntax -:g:`(term)%key` (or simply :g:`term%key` for atomic terms), where key is a +:n:`(@term)%@ident` (or simply :n:`@term%@ident` for atomic terms), where :token:`ident` is a special identifier called *delimiting key* and bound to a given scope. In such a situation, the term term, and all its subterms, are -interpreted in the scope stack extended with the scope bound tokey. +interpreted in the scope stack extended with the scope bound to :token:`ident`. .. cmd:: Delimit Scope @scope with @ident @@ -1051,15 +1063,15 @@ interpreted in the scope stack extended with the scope bound tokey. Binding arguments of a constant to an interpretation scope +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ -.. cmd:: Arguments @qualid {+ @name%@scope} +.. cmd:: Arguments @qualid {+ @name%@ident} :name: Arguments (scopes) It is possible to set in advance that some arguments of a given constant have to be interpreted in a given scope. The command is - :n:`Arguments @qualid {+ @name%@scope}` where the list is a prefix of the - arguments of ``qualid`` eventually annotated with their ``scope``. Grouping + :n:`Arguments @qualid {+ @name%@ident}` where the list is a prefix of the + arguments of ``qualid`` optionally annotated with their scope :token:`ident`. Grouping round parentheses can be used to decorate multiple arguments with the same - scope. ``scope`` can be either a scope name or its delimiting key. For + scope. :token:`ident` can be either a scope name or its delimiting key. For example the following command puts the first two arguments of :g:`plus_fct` in the scope delimited by the key ``F`` (``Rfun_scope``) and the last argument in the scope delimited by the key ``R`` (``R_scope``). @@ -1070,13 +1082,13 @@ Binding arguments of a constant to an interpretation scope The ``Arguments`` command accepts scopes decoration to all grouping parentheses. In the following example arguments A and B are marked as - maximally inserted implicit arguments and are put into the type_scope scope. + maximally inserted implicit arguments and are put into the ``type_scope`` scope. .. coqdoc:: Arguments respectful {A B}%type (R R')%signature _ _. - When interpreting a term, if some of the arguments of qualid are built + When interpreting a term, if some of the arguments of :token:`qualid` are built from a notation, then this notation is interpreted in the scope stack extended by the scope bound (if any) to this argument. The effect of the scope is limited to the argument itself. It does not propagate to @@ -1088,21 +1100,21 @@ Binding arguments of a constant to an interpretation scope This command can be used to clear argument scopes of :token:`qualid`. - .. cmdv:: Arguments @qualid {+ @name%scope} : extra scopes + .. cmdv:: Arguments @qualid {+ @name%@ident} : extra scopes Defines extra argument scopes, to be used in case of coercion to ``Funclass`` (see the :ref:`implicitcoercions` chapter) or with a computed type. - .. cmdv:: Global Arguments @qualid {+ @name%@scope} + .. cmdv:: Global Arguments @qualid {+ @name%@ident} - This behaves like :n:`Arguments qualid {+ @name%@scope}` but survives when a + This behaves like :n:`Arguments qualid {+ @name%@ident}` but survives when a section is closed instead of stopping working at section closing. Without the ``Global`` modifier, the effect of the command stops when the section it belongs to ends. - .. cmdv:: Local Arguments @qualid {+ @name%@scope} + .. cmdv:: Local Arguments @qualid {+ @name%@ident} - This behaves like :n:`Arguments @qualid {+ @name%@scope}` but does not + This behaves like :n:`Arguments @qualid {+ @name%@ident}` but does not survive modules and files. Without the ``Local`` modifier, the effect of the command is visible from within other modules or files. @@ -1141,10 +1153,10 @@ Binding types of arguments to an interpretation scope 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 - to this type. When a scope ``scope`` is bound to a type ``type``, any new function - defined later on gets its arguments of type ``type`` interpreted by default in - scope scope (this default behavior can however be overwritten by explicitly - using the command :cmd:`Arguments`). + to this type. When a scope :token:`scope` is bound to a type :token:`type`, any function + gets its arguments of type :token:`type` interpreted by default in scope :token:`scope` + (this default behavior can however be overwritten by explicitly using the + command :cmd:`Arguments <Arguments (scopes)>`). Whether the argument of a function has some type ``type`` is determined statically. For instance, if ``f`` is a polymorphic function of type @@ -1172,6 +1184,11 @@ Binding types of arguments to an interpretation scope Check (fun x y1 y2 z t => P _ (x + t) ((f _ (y1 + y2) + z))). + .. note:: When active, a bound scope has effect on all defined functions + (even if they are defined after the :cmd:`Bind Scope` directive), except + if argument scopes were assigned explicitly using the + :cmd:`Arguments <Arguments (scopes)>` command. + .. note:: The scopes ``type_scope`` and ``function_scope`` also have a local effect on interpretation. See the next section. @@ -1657,15 +1674,15 @@ Tactic notations allow to customize the syntax of tactics. They have the followi tacn : Tactic Notation [`tactic_level`] [`prod_item` … `prod_item`] := `tactic`. prod_item : `string` | `tactic_argument_type`(`ident`) tactic_level : (at level `num`) - tactic_argument_type : `ident` | `simple_intropattern` | `reference` - : `hyp` | `hyp_list` | `ne_hyp_list` - : `constr` | `uconstr` | `constr_list` | `ne_constr_list` - : `integer` | `integer_list` | `ne_integer_list` - : `int_or_var` | `int_or_var_list` | `ne_int_or_var_list` - : `tactic` | `tactic0` | `tactic1` | `tactic2` | `tactic3` - : `tactic4` | `tactic5` - -.. cmd:: Tactic Notation {? (at level @level)} {+ @prod_item} := @tactic. + tactic_argument_type : ident | simple_intropattern | reference + : hyp | hyp_list | ne_hyp_list + : constr | uconstr | constr_list | ne_constr_list + : integer | integer_list | ne_integer_list + : int_or_var | int_or_var_list | ne_int_or_var_list + : tactic | tactic0 | tactic1 | tactic2 | tactic3 + : tactic4 | tactic5 + +.. cmd:: Tactic Notation {? (at level @num)} {+ @prod_item} := @tactic. A tactic notation extends the parser and pretty-printer of tactics with a new rule made of the list of production items. It then evaluates into the |