diff options
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 18 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 20 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 208 |
4 files changed, 34 insertions, 216 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 013ff0a83f..b1759bf71b 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -1564,9 +1564,9 @@ Computing in a term: eval Evaluation of a term can be performed with: -.. tacn:: eval @red_expr in @term +:n:`eval @red_expr in @term` - :tacn:`eval` is a :token:`value_tactic`. +See :tacn:`eval`. :tacn:`eval` is a :token:`value_tactic`. Getting the type of a term ~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 1bb4216e4f..9f3f0ef3d5 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -1299,7 +1299,7 @@ Two examples of syntax differences: to add the necessary notation. - The built-in `simpl` tactic in Ltac1 supports the use of scope keys in delta flags, e.g. :n:`simpl ["+"%nat]` which is not accepted by Ltac2. This is because Ltac2 uses a different - definition for :token:`delta_flag`; compare it to :token:`ltac2_delta_flag`. This also affects + definition for :token:`delta_reductions`; compare it to :token:`ltac2_delta_reductions`. This also affects :tacn:`compute`. Ltac1 tactics are not automatically available in Ltac2. (Note that some of the tactics described @@ -1461,9 +1461,9 @@ Other nonterminals that have syntactic classes are listed here. - :token:`ltac2_bindings` - :token:`bindings` - * - :n:`strategy` - - :token:`ltac2_strategy_flag` - - :token:`strategy_flag` + * - :n:`reductions` + - :token:`ltac2_reductions` + - :token:`reductions` * - :n:`reference` - :token:`refglobal` @@ -1571,19 +1571,19 @@ Here is the syntax for the :n:`q_*` nonterminals: | @natural | @lident -.. insertprodn ltac2_strategy_flag ltac2_delta_flag +.. insertprodn ltac2_reductions ltac2_delta_reductions .. prodn:: - ltac2_strategy_flag ::= {+ @ltac2_red_flag } - | {? @ltac2_delta_flag } + ltac2_reductions ::= {+ @ltac2_red_flag } + | {? @ltac2_delta_reductions } ltac2_red_flag ::= beta | iota | match | fix | cofix | zeta - | delta {? @ltac2_delta_flag } - ltac2_delta_flag ::= {? - } [ {+ @refglobal } ] + | delta {? @ltac2_delta_reductions } + ltac2_delta_reductions ::= {? - } [ {+ @refglobal } ] .. insertprodn refglobal refglobal diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 665bae7077..fad02b2645 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -479,6 +479,7 @@ one or more of its hypotheses. .. prodn:: occurrences ::= at @occs_nums | in @goal_occurrences + simple_occurrences ::= @occurrences occs_nums ::= {? - } {+ @nat_or_var } nat_or_var ::= {| @natural | @ident } goal_occurrences ::= {+, @hyp_occs } {? %|- {? @concl_occs } } @@ -496,6 +497,10 @@ one or more of its hypotheses. the conclusion of the goal. The second form can select occurrences in the goal conclusion and in one or more hypotheses. + :n:`@simple_occurrences` + A semantically restricted form of :n:`@occurrences` that doesn't allow the + `at` clause anywhere within it. + :n:`{? - } {+ @nat_or_var }` Selects the specified occurrences within a single goal or hypothesis. Occurrences are numbered starting with 1 following a depth-first traversal @@ -675,10 +680,10 @@ Applying theorems :tacn:`notypeclasses refine`: it performs type checking without resolution of typeclasses, does not perform beta reductions or shelve the subgoals. - .. flag:: Debug Unification - - Enables printing traces of unification steps used during - elaboration/typechecking and the :tacn:`refine` tactic. + :opt:`Debug` ``"unification"`` enables printing traces of + unification steps used during elaboration/typechecking and the + :tacn:`refine` tactic. ``"ho-unification"`` prints information + about higher order heuristics. .. tacn:: apply @term :name: apply @@ -1040,10 +1045,9 @@ Applying theorems when the instantiation of a variable cannot be found (cf. :tacn:`eapply` and :tacn:`apply`). -.. flag:: Debug Tactic Unification - - Enables printing traces of unification steps in tactic unification. - Tactic unification is used in tactics such as :tacn:`apply` and :tacn:`rewrite`. +:opt:`Debug` ``"tactic-unification"`` enables printing traces of +unification steps in tactic unification. Tactic unification is used in +tactics such as :tacn:`apply` and :tacn:`rewrite`. .. _managingthelocalcontext: diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 8d1817b61f..22e4350c38 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -65,6 +65,9 @@ If no selector is provided, the command applies to the current goal. If no proof is open, then the command only applies to accessible objects. (see Section :ref:`invocation-of-tactics`). +:cmd:`Eval` and :cmd:`Compute` are also :token:`query_command`\s, which are +described elsewhere + .. cmd:: About @reference {? @univ_name_list } Displays information about the :n:`@reference` object, which, @@ -80,22 +83,6 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`). Displays the type of :n:`@term`. When called in proof mode, the term is checked in the local context of the selected goal. -.. cmd:: Eval @red_expr in @term - - Performs the specified reduction on :n:`@term` and displays - the resulting term with its type. If a proof is open, :n:`@term` - may reference hypotheses of the selected goal. - - .. seealso:: Section :ref:`performingcomputations`. - - -.. cmd:: Compute @term - - Evaluates :n:`@term` using the bytecode-based virtual machine. - It is a shortcut for :cmd:`Eval` :n:`vm_compute in @term`. - - .. seealso:: Section :ref:`performingcomputations`. - .. cmd:: Search {+ @search_query } {? {| inside | outside } {+ @qualid } } This command can be used to filter the goal and the global context @@ -865,6 +852,14 @@ Controlling display interpreted from left to right, so in case of an overlap, the flags on the right have higher priority, meaning that `A,-A` is equivalent to `-A`. +.. opt:: Debug "{+, {? - } @ident }" + + Configures the display of debug messages. Each :n:`@ident` enables debug messages + for that component, while :n:`-@ident` disables messages for the component. + ``all`` activates or deactivates all other components. ``backtrace`` controls printing of + error backtraces. + + :cmd:`Test` `Debug` displays the list of components and their enabled/disabled state. .. opt:: Printing Width @natural This command sets which left-aligned part of the width of the screen is used @@ -928,187 +923,6 @@ Printing constructions in full .. see a contrived example here: https://github.com/coq/coq/pull/11718#discussion_r415481854 -.. _vernac-controlling-the-reduction-strategies: - -Controlling the reduction strategies and the conversion algorithm ----------------------------------------------------------------------- - - -Coq provides reduction strategies that the tactics can invoke and two -different algorithms to check the convertibility of types. The first -conversion algorithm lazily compares applicative terms while the other -is a brute-force but efficient algorithm that first normalizes the -terms before comparing them. The second algorithm is based on a -bytecode representation of terms similar to the bytecode -representation used in the ZINC virtual machine :cite:`Leroy90`. It is -especially useful for intensive computation of algebraic values, such -as numbers, and for reflection-based tactics. The commands to fine- -tune the reduction strategies and the lazy conversion algorithm are -described first. - -.. cmd:: Opaque {+ @reference } - - This command accepts the :attr:`global` attribute. By default, the scope - of :cmd:`Opaque` is limited to the current section or module. - - This command has an effect on unfoldable constants, i.e. on constants - defined by :cmd:`Definition` or :cmd:`Let` (with an explicit body), or by a command - associated with a definition such as :cmd:`Fixpoint`, etc, - or by a proof ended by :cmd:`Defined`. The command tells not to unfold the - constants in the :n:`@reference` sequence in tactics using δ-conversion (unfolding - a constant is replacing it by its definition). - - :cmd:`Opaque` has also an effect on the conversion algorithm of Coq, telling - it to delay the unfolding of a constant as much as possible when Coq - has to check the conversion (see Section :ref:`conversion-rules`) of two distinct - applied constants. - -.. cmd:: Transparent {+ @reference } - - This command accepts the :attr:`global` attribute. By default, the scope - of :cmd:`Transparent` is limited to the current section or module. - - This command is the converse of :cmd:`Opaque` and it applies on unfoldable - constants to restore their unfoldability after an Opaque command. - - Note in particular that constants defined by a proof ended by Qed are - not unfoldable and Transparent has no effect on them. This is to keep - with the usual mathematical practice of *proof irrelevance*: what - matters in a mathematical development is the sequence of lemma - statements, not their actual proofs. This distinguishes lemmas from - the usual defined constants, whose actual values are of course - relevant in general. - - .. exn:: The reference @qualid was not found in the current environment. - - There is no constant named :n:`@qualid` in the environment. - -.. seealso:: :ref:`performingcomputations` and :ref:`proof-editing-mode` - -.. _vernac-strategy: - -.. cmd:: Strategy {+ @strategy_level [ {+ @reference } ] } - - .. insertprodn strategy_level strategy_level_or_var - - .. prodn:: - strategy_level ::= opaque - | @integer - | expand - | transparent - strategy_level_or_var ::= @strategy_level - | @ident - - This command accepts the :attr:`local` attribute, which limits its effect - to the current section or module, in which case the section and module - behavior is the same as :cmd:`Opaque` and :cmd:`Transparent` (without :attr:`global`). - - This command generalizes the behavior of the :cmd:`Opaque` and :cmd:`Transparent` - commands. It is used to fine-tune the strategy for unfolding - constants, both at the tactic level and at the kernel level. This - command associates a :n:`@strategy_level` with the qualified names in the :n:`@reference` - sequence. Whenever two - expressions with two distinct head constants are compared (for - instance, this comparison can be triggered by a type cast), the one - with lower level is expanded first. In case of a tie, the second one - (appearing in the cast type) is expanded. - - Levels can be one of the following (higher to lower): - - + ``opaque`` : level of opaque constants. They cannot be expanded by - tactics (behaves like +∞, see next item). - + :n:`@integer` : levels indexed by an integer. Level 0 corresponds to the - default behavior, which corresponds to transparent constants. This - level can also be referred to as ``transparent``. Negative levels - correspond to constants to be expanded before normal transparent - constants, while positive levels correspond to constants to be - expanded after normal transparent constants. - + ``expand`` : level of constants that should be expanded first (behaves - like −∞) - + ``transparent`` : Equivalent to level 0 - -.. cmd:: Print Strategy @reference - - This command prints the strategy currently associated with :n:`@reference`. It - fails if :n:`@reference` is not an unfoldable reference, that is, neither a - variable nor a constant. - - .. exn:: The reference is not unfoldable. - :undocumented: - -.. cmd:: Print Strategies - - Print all the currently non-transparent strategies. - - -.. cmd:: Declare Reduction @ident := @red_expr - - Declares a short name for the reduction expression :n:`@red_expr`, for - instance ``lazy beta delta [foo bar]``. This short name can then be used - in :n:`Eval @ident in` or ``eval`` constructs. This command - accepts the :attr:`local` attribute, which indicates that the reduction - will be discarded at the end of the - file or module. The name is not qualified. In - particular declaring the same name in several modules or in several - 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 from also performing a - :n:`Ltac @ident := @red_expr`. - - .. seealso:: :ref:`performingcomputations` - - -.. _controlling-locality-of-commands: - -Controlling the locality of commands ------------------------------------------ - -.. attr:: global - local - - Some commands support a :attr:`local` or :attr:`global` attribute - to control the scope of their effect. There is also a legacy (and - much more commonly used) syntax using the ``Local`` or ``Global`` - prefixes (see :n:`@legacy_attr`). There are four kinds of - commands: - - + Commands whose default is to extend their effect both outside the - section and the module or library file they occur in. For these - commands, the :attr:`local` attribute limits the effect of the command to the - current section or module it occurs in. As an example, the :cmd:`Coercion` - and :cmd:`Strategy` commands belong to this category. - + Commands whose default behavior is to stop their effect at the end - of the section they occur in but to extend their effect outside the module or - library file they occur in. For these commands, the :attr:`local` attribute limits the - effect of the command to the current module if the command does not occur in a - section and the :attr:`global` attribute extends the effect outside the current - sections and current module if the command occurs in a section. As an example, - the :cmd:`Arguments`, :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 :attr:`global` attribute is not - applicable to them. - + Commands whose default behavior is to stop their effect at the end - of the section or module they occur in. For these commands, the :attr:`global` - attribute extends their effect outside the sections and modules they - occur in. The :cmd:`Transparent` and :cmd:`Opaque` commands - belong to this category. - + Commands whose default behavior is to extend their effect outside - sections but not outside modules when they occur in a section and to - extend their effect outside the module or library file they occur in - when no section contains them. For these commands, the :attr:`local` attribute - limits the effect to the current section or module while the :attr:`global` - attribute extends the effect outside the module even when the command - occurs in a section. The :cmd:`Set` and :cmd:`Unset` commands belong to this - category. - -.. attr:: export - - Some commands support an :attr:`export` attribute. The effect of - the attribute is to make the effect of the command available when - the module containing it is imported. It is supported in - particular by the :ref:`Hint <creating_hints>`, :cmd:`Set` and :cmd:`Unset` - commands. - .. _controlling-typing-flags: Controlling Typing Flags |