diff options
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 122 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 2 |
4 files changed, 81 insertions, 50 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 2fc3c9f748..87a367fc93 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -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 4f01559cad..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 -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -An occurrence clause is a modifier to some tactics that obeys the -following syntax: - - .. 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`. +Occurrence clauses +~~~~~~~~~~~~~~~~~~ + +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. + + .. 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:: 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: |