diff options
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 19 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 148 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 2 |
4 files changed, 101 insertions, 70 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 6464f085b8..87a367fc93 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -480,15 +480,15 @@ separately. They succeed only if there is a success for each goal. For example Do loop ~~~~~~~ -.. tacn:: do @int_or_var @ltac_expr3 +.. tacn:: do @nat_or_var @ltac_expr3 :name: do - The do loop repeats a tactic :token:`int_or_var` times: + The do loop repeats a tactic :token:`nat_or_var` times: - :n:`@ltac_expr` is evaluated to ``v`` which must be a tactic value. This tactic - value ``v`` is applied :token:`int_or_var` times. Supposing :token:`int_or_var` > 1, after the + :n:`@ltac_expr` is evaluated to ``v``, which must be a tactic value. This tactic + value ``v`` is applied :token:`nat_or_var` times. If :token:`nat_or_var` > 1, after the first application of ``v``, ``v`` is applied, at least once, to the generated - subgoals and so on. It fails if the application of ``v`` fails before :token:`int_or_var` + subgoals and so on. It fails if the application of ``v`` fails before :token:`nat_or_var` applications have been completed. :tacn:`do` is an :token:`l3_tactic`. @@ -973,11 +973,11 @@ Timeout We can force a tactic to stop if it has not finished after a certain amount of time: -.. tacn:: timeout @int_or_var @ltac_expr3 +.. tacn:: timeout @nat_or_var @ltac_expr3 :name: timeout :n:`@ltac_expr3` is evaluated to ``v`` which must be a tactic value. The tactic value - ``v`` is applied normally, except that it is interrupted after :n:`@natural` seconds + ``v`` is applied normally, except that it is interrupted after :n:`@nat_or_var` seconds if it is still running. In this case the outcome is a failure. :tacn:`timeout` is an :token:`l3_tactic`. @@ -1637,9 +1637,10 @@ Testing boolean expressions: guard .. tacn:: guard @int_or_var @comparison @int_or_var :name: guard - .. insertprodn comparison comparison + .. insertprodn int_or_var comparison .. prodn:: + int_or_var ::= {| @integer | @ident } comparison ::= = | < | <= @@ -1761,7 +1762,7 @@ Defining |Ltac| symbols "Ltac intros := idtac" seems like it redefines/hides an existing tactic, but in fact it creates a tactic which can only be called by its qualified name. This is true in - general of tactic notations. The only way to overwrite most + general of tactic notations. The only way to override most primitive tactics, and any user-defined tactic notation, is with another tactic notation. diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index a46f4fb894..375129c02d 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -1475,7 +1475,7 @@ Other nonterminals that have syntactic classes are listed here. * - :n:`clause` - :token:`ltac2_clause` - - :token:`clause_dft_concl` + - :token:`occurrences` * - :n:`occurrences` - :token:`q_occurrences` diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 26a56005c1..8f5c045929 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -466,52 +466,82 @@ Examples: .. _occurrencessets: -Occurrence sets and occurrence clauses -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Occurrence clauses +~~~~~~~~~~~~~~~~~~ -An occurrence clause is a modifier to some tactics that obeys the -following syntax: +An :gdef:`occurrence` is a subterm of a goal or hypothesis that +matches a pattern provided by a tactic. Occurrence clauses +select a subset of the ocurrences in a goal and/or in +one or more of its hypotheses. - .. prodn:: - occurrence_clause ::= in @goal_occurrences - goal_occurrences ::= {*, @ident {? @at_occurrences } } {? |- {? * {? @at_occurrences } } } - | * |- {? * {? @at_occurrences } } - | * - at_occurrences ::= at @occurrences - occurrences ::= {? - } {* @natural } - -The role of an occurrence clause is to select a set of occurrences of a term -in a goal. In the first case, the :n:`@ident {? at {* num}}` parts indicate -that occurrences have to be selected in the hypotheses named :token:`ident`. -If no numbers are given for hypothesis :token:`ident`, then all the -occurrences of :token:`term` in the hypothesis are selected. If numbers are -given, they refer to occurrences of :token:`term` when the term is printed -using the :flag:`Printing All` flag, counting from left to right. In particular, -occurrences of :token:`term` in implicit arguments -(see :ref:`ImplicitArguments`) or coercions (see :ref:`Coercions`) are -counted. - -If a minus sign is given between ``at`` and the list of occurrences, it -negates the condition so that the clause denotes all the occurrences -except the ones explicitly mentioned after the minus sign. - -As an exception to the left-to-right order, the occurrences in -the return subexpression of a match are considered *before* the -occurrences in the matched term. - -In the second case, the ``*`` on the left of ``|-`` means that all occurrences -of term are selected in every hypothesis. - -In the first and second case, if ``*`` is mentioned on the right of ``|-``, the -occurrences of the conclusion of the goal have to be selected. If some numbers -are given, then only the occurrences denoted by these numbers are selected. If -no numbers are given, all occurrences of :token:`term` in the goal are selected. - -Finally, the last notation is an abbreviation for ``* |- *``. Note also -that ``|-`` is optional in the first case when no ``*`` is given. - -Here are some tactics that understand occurrence clauses: :tacn:`set`, -:tacn:`remember`, :tacn:`induction`, :tacn:`destruct`. + .. insertprodn occurrences concl_occs + + .. prodn:: + occurrences ::= at @occs_nums + | in @goal_occurrences + occs_nums ::= {? - } {+ @nat_or_var } + nat_or_var ::= {| @natural | @ident } + goal_occurrences ::= {+, @hyp_occs } {? %|- {? @concl_occs } } + | * %|- {? @concl_occs } + | %|- {? @concl_occs } + | {? @concl_occs } + hyp_occs ::= @hypident {? at @occs_nums } + hypident ::= @ident + | ( type of @ident ) + | ( value of @ident ) + concl_occs ::= * {? at @occs_nums } + + :n:`@occurrences` + The first form of :token:`occurrences` selects occurrences in + the conclusion of the goal. The second form can select occurrences + in the goal conclusion and in one or more hypotheses. + + :n:`{? - } {+ @nat_or_var }` + Selects the specified occurrences within a single goal or hypothesis. + Occurrences are numbered from left to right starting with 1 when the + goal is printed with the :flag:`Printing All` flag. (In particular, occurrences + in :ref:`implicit arguments <ImplicitArguments>` and + :ref:`coercions <Coercions>` are counted but not shown by default.) + + Specifying `-` includes all occurrences *except* the ones listed. + + :n:`{*, @hyp_occs } {? %|- {? @concl_occs } }` + Selects occurrences in the specified hypotheses and the + specified occurrences in the conclusion. + + :n:`* %|- {? @concl_occs }` + Selects all occurrences in all hypotheses and the + specified occurrences in the conclusion. + + :n:`%|- {? @concl_occs }` + Selects the specified occurrences in the conclusion. + + :n:`@goal_occurrences ::= {? @concl_occs }` + Selects all occurrences in all hypotheses and in the specified occurrences + in the conclusion. + + :n:`@hypident {? at @occs_nums }` + Omiting :token:`occs_nums` selects all occurrences within the hypothesis. + + :n:`@hypident ::= @ident` + Selects the hypothesis named :token:`ident`. + + :n:`( type of @ident )` + Selects the type part of the named hypothesis (e.g. `: nat`). + + :n:`( value of @ident )` + Selects the value part of the named hypothesis (e.g. `:= 1`). + + :n:`@concl_occs ::= * {? at @occs_nums }` + Selects occurrences in the conclusion. '*' by itself selects all occurrences. + :n:`@occs_nums` selects the specified occurrences. + + Use `in *` to select all occurrences in all hypotheses and the conclusion, + which is equivalent to `in * |- *`. Use `* |-` to select all occurrences + in all hypotheses. + +Tactics that use occurrence clauses include :tacn:`set`, +:tacn:`remember`, :tacn:`induction` and :tacn:`destruct`. .. seealso:: @@ -878,38 +908,38 @@ Applying theorems This happens if the conclusion of :token:`ident` does not match any of the non-dependent premises of the type of :token:`term`. - .. tacv:: apply {+, @term} in @ident + .. tacv:: apply {+, @term} in {+, @ident} - This applies each :token:`term` in sequence in :token:`ident`. + This applies each :token:`term` in sequence in each hypothesis :token:`ident`. - .. tacv:: apply {+, @term with @bindings} in @ident + .. tacv:: apply {+, @term with @bindings} in {+, @ident} - This does the same but uses the bindings in each :n:`(@ident := @term)` to - instantiate the parameters of the corresponding type of :token:`term` - (see :ref:`bindings`). + This does the same but uses the bindings to instantiate + parameters of :token:`term` (see :ref:`bindings`). - .. tacv:: eapply {+, @term {? with @bindings } } in @ident + .. tacv:: eapply {+, @term {? with @bindings } } in {+, @ident} This works as :tacn:`apply … in` but turns unresolved bindings into existential variables, if any, instead of failing. - .. tacv:: apply {+, @term {? with @bindings } } in @ident as @simple_intropattern + .. tacv:: apply {+, @term {? with @bindings } } in {+, @ident {? as @simple_intropattern}} :name: apply … in … as - This works as :tacn:`apply … in` then applies the :token:`simple_intropattern` - to the hypothesis :token:`ident`. + This works as :tacn:`apply … in` but applying an associated + :token:`simple_intropattern` to each hypothesis :token:`ident` + that comes with such clause. - .. tacv:: simple apply @term in @ident + .. tacv:: simple apply @term in {+, @ident} This behaves like :tacn:`apply … in` but it reasons modulo conversion only on subterms that contain no variables to instantiate and does not traverse tuples. See :ref:`the corresponding example <simple_apply_ex>`. - .. tacv:: {? simple} apply {+, @term {? with @bindings}} in @ident {? as @simple_intropattern} - {? simple} eapply {+, @term {? with @bindings}} in @ident {? as @simple_intropattern} + .. tacv:: {? simple} apply {+, @term {? with @bindings}} in {+, @ident {? as @simple_intropattern}} + {? simple} eapply {+, @term {? with @bindings}} in {+, @ident {? as @simple_intropattern}} - This summarizes the different syntactic variants of :n:`apply @term in @ident` - and :n:`eapply @term in @ident`. + This summarizes the different syntactic variants of :n:`apply @term in {+, @ident}` + and :n:`eapply @term in {+, @ident}`. .. tacn:: constructor @natural :name: constructor diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 86d1d25745..e7db9cfaca 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1136,7 +1136,7 @@ Controlling the locality of commands Some commands support an :attr:`export` attribute. The effect of the attribute is to make the effect of the command available when the module containing it is imported. It is supported in - particular by the :cmd:`Hint`, :cmd:`Set` and :cmd:`Unset` + particular by the :ref:`Hint <creating_hints>`, :cmd:`Set` and :cmd:`Unset` commands. .. _controlling-typing-flags: |