diff options
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 48 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 30 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 26 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 50 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 306 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 36 |
6 files changed, 244 insertions, 252 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index d8b2af092f..f18569c7fd 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -74,7 +74,7 @@ The constructs in :token:`ltac_expr` are :term:`left associative`. ltac_expr0 ::= ( @ltac_expr ) | [> @for_each_goal ] | @tactic_atom - tactic_atom ::= @int + tactic_atom ::= @integer | @qualid | () @@ -188,7 +188,7 @@ examining the part at the end under "Entry tactic:tactic_arg". - * - ``integer`` - - :token:`int` + - :token:`integer` - an integer - @@ -397,7 +397,7 @@ behavior.) `par` Applies :n:`@ltac_expr` to all focused goals in parallel. The number of workers can be controlled via the command line option - :n:`-async-proofs-tac-j @num` to specify the desired number of workers. + :n:`-async-proofs-tac-j @natural` to specify the desired number of workers. Limitations: ``par:`` only works on goals that don't contain existential variables. :n:`@ltac_expr` must either solve the goal completely or do nothing (i.e. it cannot make some progress). @@ -412,8 +412,8 @@ Selectors can also be used nested within a tactic expression with the .. prodn:: selector ::= {+, @range_selector } | [ @ident ] - range_selector ::= @num - @num - | @num + range_selector ::= @natural - @natural + | @natural Applies :token:`ltac_expr3` to the selected goals. @@ -426,10 +426,10 @@ Selectors can also be used nested within a tactic expression with the Limits the application of :token:`ltac_expr3` to the goal previously named :token:`ident` by the user (see :ref:`existential-variables`). - :n:`@num__1 - @num__2` - Selects the goals :n:`@num__1` through :n:`@num__2`, inclusive. + :n:`@natural__1 - @natural__2` + Selects the goals :n:`@natural__1` through :n:`@natural__2`, inclusive. - :n:`@num` + :n:`@natural` Selects a single goal. .. exn:: No such goal. @@ -876,7 +876,7 @@ Print/identity tactic: idtac ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. tacn:: idtac {* {| @ident | @string | @int } } +.. tacn:: idtac {* {| @ident | @string | @natural } } :name: idtac Leaves the proof unchanged and prints the given tokens. Strings and integers are printed @@ -888,7 +888,7 @@ Print/identity tactic: idtac Failing ~~~~~~~ -.. tacn:: {| fail | gfail } {? @int_or_var } {* {| @ident | @string | @int } } +.. tacn:: {| fail | gfail } {? @int_or_var } {* {| @ident | @string | @integer } } :name: fail; gfail :tacn:`fail` is the always-failing tactic: it does not solve any @@ -916,17 +916,17 @@ Failing (backtracking). If nonzero, the current :tacn:`match goal` block, :tacn:`try`, :tacn:`repeat`, or branching command is aborted and the level is decremented. In the case of :n:`+`, a nonzero level skips the first backtrack point, even if - the call to :tacn:`fail` :n:`@num` is not enclosed in a :n:`+` construct, + the call to :tacn:`fail` :n:`@natural` is not enclosed in a :n:`+` construct, respecting the algebraic identity. - :n:`{* {| @ident | @string | @int } }` + :n:`{* {| @ident | @string | @integer } }` The given tokens are used for printing the failure message. If :token:`ident` is an |Ltac| variable, its contents are printed; if not, it is an error. .. exn:: Tactic failure. :undocumented: - .. exn:: Tactic failure (level @num). + .. exn:: Tactic failure (level @natural). :undocumented: .. exn:: No such goal. @@ -976,7 +976,7 @@ amount of time: :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:`@num` seconds + ``v`` is applied normally, except that it is interrupted after :n:`@natural` seconds if it is still running. In this case the outcome is a failure. :tacn:`timeout` is an :token:`l3_tactic`. @@ -1675,8 +1675,8 @@ Proving a subgoal as a separate lemma: abstract Does a :tacn:`solve` :n:`[ @ltac_expr2 ]` and saves the subproof as an auxiliary lemma. if :n:`@ident__name` is specified, the lemma is saved with that name; otherwise - the lemma is saved with the name :n:`@ident`\ `_subproof`\ :n:`{? @num }` where - :token:`ident` is the name of the current goal (e.g. the theorem name) and :token:`num` + the lemma is saved with the name :n:`@ident`\ `_subproof`\ :n:`{? @natural }` where + :token:`ident` is the name of the current goal (e.g. the theorem name) and :token:`natural` is chosen to get a fresh name. If the proof is closed with :cmd:`Qed`, the auxiliary lemma is inlined in the final proof term. @@ -1709,7 +1709,7 @@ Proving a subgoal as a separate lemma: abstract .. tacn:: transparent_abstract @ltac_expr3 {? using @ident } Like :tacn:`abstract`, but save the subproof in a transparent lemma with a name in - the form :n:`@ident`\ :n:`_subterm`\ :n:`{? @num }`. + the form :n:`@ident`\ :n:`_subterm`\ :n:`{? @natural }`. .. warning:: @@ -2197,7 +2197,7 @@ Backtraces Tracing execution ~~~~~~~~~~~~~~~~~ -.. cmd:: Info @num @ltac_expr +.. cmd:: Info @natural @ltac_expr Applies :token:`ltac_expr` and prints a trace of the tactics that were successfully applied, discarding branches that failed. @@ -2205,7 +2205,7 @@ Tracing execution This command is valid only in proof mode. It accepts :ref:`goal-selectors`. - The number :n:`@num` is the unfolding level of tactics in the trace. At level + The number :n:`@natural` is the unfolding level of tactics in the trace. At level 0, the trace contains a sequence of tactics in the actual script, at level 1, the trace will be the concatenation of the traces of these tactics, etc… @@ -2237,12 +2237,12 @@ Tracing execution position in the script. In particular, the calls to idtac in branches which failed are not printed. - .. opt:: Info Level @num + .. opt:: Info Level @natural :name: Info Level This option is an alternative to the :cmd:`Info` command. - This will automatically print the same trace as :n:`Info @num` at each + This will automatically print the same trace as :n:`Info @natural` at each tactic call. The unfolding level can be overridden by a call to the :cmd:`Info` command. @@ -2302,11 +2302,11 @@ performance issue. This flag enables and disables the profiler. -.. cmd:: Show Ltac Profile {? {| CutOff @int | @string } } +.. cmd:: Show Ltac Profile {? {| CutOff @integer | @string } } Prints the profile. - :n:`CutOff @int` + :n:`CutOff @integer` By default, tactics that account for less than 2% of the total time are not displayed. `CutOff` lets you specify a different percentage. @@ -2373,7 +2373,7 @@ performance issue. Equivalent to the :cmd:`Reset Ltac Profile` command, which allows resetting the profile from tactic scripts for benchmarking purposes. -.. tacn:: show ltac profile {? {| cutoff @int | @string } } +.. tacn:: show ltac profile {? {| cutoff @integer | @string } } :name: show ltac profile Equivalent to the :cmd:`Show Ltac Profile` command, diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index b217448711..773e393eb6 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -283,7 +283,7 @@ There is dedicated syntax for list and array literals. | [ {*; @ltac2_expr5 } ] | %{ {? {+ @tac2rec_fieldexpr } {? ; } } %} | @ltac2_tactic_atom - ltac2_tactic_atom ::= @int + ltac2_tactic_atom ::= @integer | @string | @qualid | @ @ident @@ -1159,7 +1159,7 @@ Match on values Notations --------- -.. cmd:: Ltac2 Notation {+ @ltac2_scope } {? : @int } := @ltac2_expr +.. cmd:: Ltac2 Notation {+ @ltac2_scope } {? : @natural } := @ltac2_expr :name: Ltac2 Notation .. todo seems like name maybe should use lident rather than ident, considering: @@ -1177,7 +1177,7 @@ Notations :cmd:`Ltac2 Notation` provides a way to extend the syntax of Ltac2 tactics. The left-hand side (before the `:=`) defines the syntax to recognize and gives formal parameter - names for the syntactic values. :n:`@int` is the level of the notation. + names for the syntactic values. :n:`@integer` is the level of the notation. When the notation is used, the values are substituted into the right-hand side. The right-hand side is typechecked when the notation is used, not when it is defined. In the following example, `x` is the formal parameter name and @@ -1294,7 +1294,7 @@ workarounds through Ltac1 (described below). Two examples of syntax differences: -- There is no notation defined that's equivalent to :n:`intros until {| @ident | @num }`. There is, +- There is no notation defined that's equivalent to :n:`intros until {| @ident | @natural }`. There is, however, already an ``intros_until`` tactic function defined ``Std.v``, so it may be possible for a user 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]` @@ -1333,7 +1333,7 @@ Syntactic classes are described with a form of S-expression: .. prodn:: ltac2_scope ::= @string - | @int + | @integer | @name | @name ( {+, @ltac2_scope } ) @@ -1384,14 +1384,14 @@ table further down lists the classes that that are handled plainly. :n:`terminal(@string)` Accepts the specified string whether it's a keyword or not, returning a value of `()`. - :n:`tactic {? (@int) }` - Parses an :token:`ltac2_expr`. If :token:`int` is specified, the construct - parses a :n:`ltac2_expr@int`, for example `tactic(5)` parses :token:`ltac2_expr5`. + :n:`tactic {? (@integer) }` + Parses an :token:`ltac2_expr`. If :token:`integer` is specified, the construct + parses a :n:`ltac2_expr@integer`, for example `tactic(5)` parses :token:`ltac2_expr5`. `tactic(6)` parses :token:`ltac2_expr`. - :token:`int` must be in the range `0 .. 6`. + :token:`integer` must be in the range `0 .. 6`. - You can also use `tactic` to accept an :token:`int` or a :token:`string`, but there's - no syntactic class that accepts *only* an :token:`int` or a :token:`string`. + You can also use `tactic` to accept an :token:`integer` or a :token:`string`, but there's + no syntactic class that accepts *only* an :token:`integer` or a :token:`string`. .. todo this doesn't work as expected: "::" is in ltac2_expr1 Ltac2 Notation "ex4" x(tactic(0)) := x. @@ -1555,7 +1555,7 @@ Here is the syntax for the :n:`q_*` nonterminals: .. insertprodn ltac2_destruction_arg ltac2_constr_with_bindings .. prodn:: - ltac2_destruction_arg ::= @num + ltac2_destruction_arg ::= @natural | @lident | @ltac2_constr_with_bindings ltac2_constr_with_bindings ::= @term {? with @ltac2_bindings } @@ -1568,7 +1568,7 @@ Here is the syntax for the :n:`q_*` nonterminals: | {+ @term } ltac2_simple_binding ::= ( @qhyp := @term ) qhyp ::= $ @ident - | @num + | @natural | @lident .. insertprodn ltac2_strategy_flag ltac2_delta_flag @@ -1606,7 +1606,7 @@ Here is the syntax for the :n:`q_*` nonterminals: .. prodn:: q_occurrences ::= {? @ltac2_occs } ltac2_occs ::= at @ltac2_occs_nums - ltac2_occs_nums ::= {? - } {+ {| @num | $ @ident } } + ltac2_occs_nums ::= {? - } {+ {| @natural | $ @ident } } ltac2_concl_occ ::= * {? @ltac2_occs } ltac2_hypident_occ ::= @ltac2_hypident {? @ltac2_occs } ltac2_hypident ::= @ident_or_anti @@ -1630,7 +1630,7 @@ Here is the syntax for the :n:`q_*` nonterminals: .. prodn:: ltac2_oriented_rewriter ::= {| -> | <- } @ltac2_rewriter - ltac2_rewriter ::= {? @num } {? {| ? | ! } } @ltac2_constr_with_bindings + ltac2_rewriter ::= {? @natural } {? {| ? | ! } } @ltac2_constr_with_bindings .. insertprodn ltac2_for_each_goal ltac2_goal_tactics diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 55e4f26fe8..f90ebadb3a 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -259,9 +259,9 @@ Name a set of section hypotheses for ``Proof using`` -.. cmd:: Existential @num := @term +.. cmd:: Existential @natural := @term - This command instantiates an existential variable. :token:`num` is an index in + This command instantiates an existential variable. :token:`natural` is an index in the list of uninstantiated existential variables displayed by :cmd:`Show Existentials`. This command is intended to be used to instantiate existential @@ -313,9 +313,9 @@ Navigation in the proof tree This command cancels the effect of the last command. Thus, it backtracks one step. -.. cmdv:: Undo @num +.. cmdv:: Undo @natural - Repeats Undo :token:`num` times. + Repeats Undo :token:`natural` times. .. cmdv:: Restart :name: Restart @@ -336,9 +336,9 @@ Navigation in the proof tree Prefer the use of bullets or focusing brackets (see below). -.. cmdv:: Focus @num +.. cmdv:: Focus @natural - This focuses the attention on the :token:`num` th subgoal to prove. + This focuses the attention on the :token:`natural` th subgoal to prove. .. deprecated:: 8.8 @@ -373,9 +373,9 @@ Navigation in the proof tree together with a suggestion about the right bullet or ``}`` to unfocus it or focus the next one. - .. cmdv:: @num: %{ + .. cmdv:: @natural: %{ - This focuses on the :token:`num`\-th subgoal to prove. + This focuses on the :token:`natural`\-th subgoal to prove. .. cmdv:: [@ident]: %{ @@ -439,7 +439,7 @@ Navigation in the proof tree You are trying to use ``}`` but the current subproof has not been fully solved. - .. exn:: No such goal (@num). + .. exn:: No such goal (@natural). :undocumented: .. exn:: No such goal (@ident). @@ -559,9 +559,9 @@ Requesting information .. exn:: No focused proof. :undocumented: - .. cmdv:: Show @num + .. cmdv:: Show @natural - Displays only the :token:`num`\-th subgoal. + Displays only the :token:`natural`\-th subgoal. .. exn:: No such goal. :undocumented: @@ -649,7 +649,7 @@ Requesting information its normalized form at the current stage of the proof, useful for debugging universe inconsistencies. - .. cmdv:: Show Goal @num at @num + .. cmdv:: Show Goal @natural at @natural :name: Show Goal This command is only available in coqtop. Displays a goal at a @@ -838,7 +838,7 @@ Controlling the effect of proof editing commands ------------------------------------------------ -.. opt:: Hyps Limit @num +.. opt:: Hyps Limit @natural :name: Hyps Limit This option controls the maximum number of hypotheses displayed in goals diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 5a11b4f474..ca50a02562 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -617,7 +617,7 @@ Abbreviations selected occurrences of a term. .. prodn:: - occ_switch ::= { {? {| + | - } } {* @num } } + occ_switch ::= { {? {| + | - } } {* @natural } } where: @@ -1580,7 +1580,7 @@ whose general syntax is i_pattern ::= {| @ident | > | _ | ? | * | + | {? @occ_switch } {| -> | <- } | [ {?| @i_item } ] | - | [: {+ @ident } ] } .. prodn:: - i_block ::= {| [^ @ident ] | [^~ {| @ident | @num } ] } + i_block ::= {| [^ @ident ] | [^~ {| @ident | @natural } ] } The ``=>`` tactical first executes :token:`tactic`, then the :token:`i_item`\s, left to right. An :token:`s_item` specifies a @@ -1842,8 +1842,8 @@ Block introduction :n:`[^~ @ident ]` *block destructing* using :token:`ident` as a suffix. -:n:`[^~ @num ]` - *block destructing* using :token:`num` as a suffix. +:n:`[^~ @natural ]` + *block destructing* using :token:`natural` as a suffix. Only a :token:`s_item` is allowed between the elimination tactic and the block destructing. @@ -2236,17 +2236,17 @@ tactics to *permute* the subgoals generated by a tactic. These two equivalent tactics invert the order of the subgoals in focus. - .. tacv:: last @num first + .. tacv:: last @natural first - If :token:`num`\'s value is :math:`k`, + If :token:`natural`\'s value is :math:`k`, this tactic rotates the :math:`n` subgoals :math:`G_1` , …, :math:`G_n` in focus. Subgoal :math:`G_{n + 1 − k}` becomes the first, and the circular order of subgoals remains unchanged. - .. tacn:: first @num last + .. tacn:: first @natural last :name: first (ssreflect) - If :token:`num`\'s value is :math:`k`, + If :token:`natural`\'s value is :math:`k`, this tactic rotates the :math:`n` subgoals :math:`G_1` , …, :math:`G_n` in focus. Subgoal :math:`G_{k + 1 \bmod n}` becomes the first, and the circular order of subgoals remains unchanged. @@ -2319,7 +2319,7 @@ tactic should be repeated on the current subgoal. There are four kinds of multipliers: .. prodn:: - mult ::= {| @num ! | ! | @num ? | ? } + mult ::= {| @natural ! | ! | @natural ? | ? } Their meaning is: @@ -4086,7 +4086,7 @@ will generally fail to perform congruence simplification, even on rather simple cases. We therefore provide a more robust alternative in which the function is supplied: -.. tacn:: congr {? @num } @term +.. tacn:: congr {? @natural } @term :name: congr This tactic: @@ -4120,7 +4120,7 @@ which the function is supplied: Lemma test (x y z : nat) : x = y -> x = z. congr (_ = _). - The optional :token:`num` forces the number of arguments for which the + The optional :token:`natural` forces the number of arguments for which the tactic should generate equality proof obligations. This tactic supports equalities between applications with dependent @@ -5392,8 +5392,8 @@ In this context, the identity view can be used when no view has to be applied: Declaring new Hint Views ~~~~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: Hint View for move / @ident {? | @num } - Hint View for apply / @ident {? | @num } +.. cmd:: Hint View for move / @ident {? | @natural } + Hint View for apply / @ident {? | @natural } This command can be used to extend the database of hints for the view mechanism. @@ -5410,7 +5410,7 @@ Declaring new Hint Views views. The optional natural number is the number of implicit arguments to be considered for the declared hint view lemma. - .. cmdv:: Hint View for apply//@ident {? | @num } + .. cmdv:: Hint View for apply//@ident {? | @natural } This variant with a double slash ``//``, declares hint views for right hand sides of double views. @@ -5571,9 +5571,9 @@ Module name Natural number -.. prodn:: natural ::= {| @num | @ident } +.. prodn:: nat_or_ident ::= {| @natural | @ident } -where :token:`ident` is an Ltac variable denoting a standard |Coq| numeral +where :token:`ident` is an Ltac variable denoting a standard |Coq| number (should not be the name of a tactic which can be followed by a bracket ``[``, like ``do``, ``have``,…) @@ -5614,19 +5614,19 @@ view :ref:`introduction_ssr` intro block :ref:`introduction_ssr` .. prodn:: - i_block ::= {| [^ @ident ] | [^~ {| @ident | @num } ] } + i_block ::= {| [^ @ident ] | [^~ {| @ident | @natural } ] } intro item see :ref:`introduction_ssr` -.. prodn:: int_mult ::= {? @num } @mult_mark +.. prodn:: int_mult ::= {? @natural } @mult_mark multiplier see :ref:`iteration_ssr` -.. prodn:: occ_switch ::= { {? {| + | - } } {* @num } } +.. prodn:: occ_switch ::= { {? {| + | - } } {* @natural } } occur. switch see :ref:`occurrence_selection_ssr` -.. prodn:: mult ::= {? @num } @mult_mark +.. prodn:: mult ::= {? @natural } @mult_mark multiplier see :ref:`iteration_ssr` @@ -5741,7 +5741,7 @@ respectively. unlock (see :ref:`locking_ssr`) -.. tacn:: congr {? @num } @term +.. tacn:: congr {? @natural } @term congruence (see :ref:`congruence_ssr`) @@ -5765,11 +5765,11 @@ localization see :ref:`localization_ssr` iteration see :ref:`iteration_ssr` -.. prodn:: tactic += @tactic ; {| first | last } {? @num } {| @tactic | [ {+| @tactic } ] } +.. prodn:: tactic += @tactic ; {| first | last } {? @natural } {| @tactic | [ {+| @tactic } ] } selector see :ref:`selectors_ssr` -.. prodn:: tactic += @tactic ; {| first | last } {? @num } +.. prodn:: tactic += @tactic ; {| first | last } {? @natural } rotation see :ref:`selectors_ssr` @@ -5780,11 +5780,11 @@ closing see :ref:`terminators_ssr` Commands ~~~~~~~~ -.. cmd:: Hint View for {| move | apply } / @ident {? | @num } +.. cmd:: Hint View for {| move | apply } / @ident {? | @natural } view hint declaration (see :ref:`declaring_new_hints_ssr`) -.. cmd:: Hint View for apply // @ident {? @num } +.. cmd:: Hint View for apply // @ident {? @natural } right hand side double , view hint declaration (see :ref:`declaring_new_hints_ssr`) diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 2211a58e6e..e276a0edcb 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -59,9 +59,9 @@ specified, the default selector is used. .. _tactic_invocation_grammar: - .. productionlist:: sentence - tactic_invocation : `toplevel_selector` : `tactic`. - : `tactic`. + .. prodn:: + tactic_invocation ::= @toplevel_selector : @tactic. + | @tactic. .. todo: fully describe selectors. At the moment, ltac has a fairly complete description @@ -98,14 +98,14 @@ The general form of a term with a bindings list is .. _bindings_list_grammar: - .. productionlist:: bindings_list - ref : `ident` - : `num` - bindings_list : (`ref` := `term`) ... (`ref` := `term`) - : `term` ... `term` + .. prodn:: + ref ::= @ident + | @natural + bindings_list ::= {+ (@ref := @term) } + | {+ @term } + In a bindings list of the form :n:`{+ (@ref:= @term)}`, :n:`@ref` is either an - :n:`@ident` or a :n:`@num`. The references are determined according to the type of + :n:`@ident` or a :n:`@natural`. The references are determined according to the type of :n:`@term`. If :n:`@ref` is an identifier, this identifier has to be bound in the type of :n:`@term` and the binding provides the tactic with an instance for the parameter of this name. If :n:`@ref` is a number ``n``, it refers to @@ -137,30 +137,28 @@ introduced by tactics. They also let you split an introduced hypothesis into multiple hypotheses or subgoals. Common tactics that accept intro patterns include :tacn:`assert`, :tacn:`intros` and :tacn:`destruct`. -.. productionlist:: coq - intropattern_list : `intropattern` ... `intropattern` - : `empty` - empty : - intropattern : * - : ** - : `simple_intropattern` - simple_intropattern : `simple_intropattern_closed` [ % `term` ... % `term` ] - simple_intropattern_closed : `naming_intropattern` - : _ - : `or_and_intropattern` - : `rewriting_intropattern` - : `injection_intropattern` - naming_intropattern : `ident` - : ? - : ?`ident` - or_and_intropattern : [ `intropattern_list` | ... | `intropattern_list` ] - : ( `simple_intropattern` , ... , `simple_intropattern` ) - : ( `simple_intropattern` & ... & `simple_intropattern` ) - rewriting_intropattern : -> - : <- - injection_intropattern : [= `intropattern_list` ] - or_and_intropattern_loc : `or_and_intropattern` - : `ident` +.. prodn:: + intropattern_list ::= {* @intropattern } + intropattern ::= * + | ** + | @simple_intropattern + simple_intropattern ::= @simple_intropattern_closed {* % @term0 } + simple_intropattern_closed ::= @naming_intropattern + | _ + | @or_and_intropattern + | @rewriting_intropattern + | @injection_intropattern + naming_intropattern ::= @ident + | ? + | ?@ident + or_and_intropattern ::= [ {*| @intropattern_list } ] + | ( {*, @simple_intropattern } ) + | ( {*& @simple_intropattern } ) + rewriting_intropattern ::= -> + | <- + injection_intropattern ::= [= @intropattern_list ] + or_and_intropattern_loc ::= @or_and_intropattern + | ident Note that the intro pattern syntax varies between tactics. Most tactics use :n:`@simple_intropattern` in the grammar. @@ -480,13 +478,13 @@ Occurrence sets and occurrence clauses An occurrence clause is a modifier to some tactics that obeys the following syntax: - .. productionlist:: coq - occurrence_clause : in `goal_occurrences` - goal_occurrences : [`ident` [`at_occurrences`], ... , `ident` [`at_occurrences`] [|- [* [`at_occurrences`]]]] - : * |- [* [`at_occurrences`]] - : * - at_occurrences : at `occurrences` - occurrences : [-] `num` ... `num` + .. 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 @@ -734,12 +732,13 @@ Applying theorems does not succeed because it would require the conversion of ``id ?foo`` and :g:`O`. + .. _simple_apply_ex: .. example:: .. coqtop:: all Definition id (x : nat) := x. - Parameter H : forall y, id y = y. + Parameter H : forall x y, id x = y. Goal O = O. Fail simple apply H. @@ -909,13 +908,8 @@ Applying theorems .. 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. For instance, - if :g:`id := fun x:nat => x` and :g:`H: forall y, id y = y -> True` and - :g:`H0 : O = O` then :g:`simple apply H in H0` does not succeed because it - would require the conversion of :g:`id ?x` and :g:`O` where :g:`?x` is - an existential variable to instantiate. - Tactic :n:`simple apply @term in @ident` does not - either traverse tuples as :n:`apply @term in @ident` does. + 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_list}} in @ident {? as @simple_intropattern} {? simple} eapply {+, @term {? with @bindings_list}} in @ident {? as @simple_intropattern} @@ -923,11 +917,11 @@ Applying theorems This summarizes the different syntactic variants of :n:`apply @term in @ident` and :n:`eapply @term in @ident`. -.. tacn:: constructor @num +.. tacn:: constructor @natural :name: constructor This tactic applies to a goal such that its conclusion is an inductive - type (say :g:`I`). The argument :token:`num` must be less or equal to the + type (say :g:`I`). The argument :token:`natural` must be less or equal to the numbers of constructor(s) of :g:`I`. Let :n:`c__i` be the i-th constructor of :g:`I`, then :g:`constructor i` is equivalent to :n:`intros; apply c__i`. @@ -944,7 +938,7 @@ Applying theorems :g:`constructor n` where ``n`` is the number of constructors of the head of the goal. - .. tacv:: constructor @num with @bindings_list + .. tacv:: constructor @natural with @bindings_list Let ``c`` be the i-th constructor of :g:`I`, then :n:`constructor i with @bindings_list` is equivalent to @@ -1075,9 +1069,9 @@ Managing the local context .. exn:: No such hypothesis in current goal. :undocumented: - .. tacv:: intros until @num + .. tacv:: intros until @natural - This repeats :tacn:`intro` until the :token:`num`\-th non-dependent + This repeats :tacn:`intro` until the :token:`natural`\-th non-dependent product. .. example:: @@ -1093,7 +1087,7 @@ Managing the local context .. exn:: No such hypothesis in current goal. - This happens when :token:`num` is 0 or is greater than the number of + This happens when :token:`natural` is 0 or is greater than the number of non-dependent products of the goal. .. tacv:: intro {? @ident__1 } after @ident__2 @@ -1578,7 +1572,7 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`. This is equivalent to :n:`generalize @term; ... ; generalize @term`. Note that the sequence of term :sub:`i` 's are processed from n to 1. -.. tacv:: generalize @term at {+ @num} +.. tacv:: generalize @term at {+ @natural} This is equivalent to :n:`generalize @term` but it generalizes only over the specified occurrences of :n:`@term` (counting from left to right on the @@ -1589,7 +1583,7 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`. This is equivalent to :n:`generalize @term` but it uses :n:`@ident` to name the generalized hypothesis. -.. tacv:: generalize {+, @term at {+ @num} as @ident} +.. tacv:: generalize {+, @term at {+ @natural} as @ident} This is the most general form of :n:`generalize` that combines the previous behaviors. @@ -1621,16 +1615,16 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`. name the variable in the current goal and in the context of the existential variable. This can lead to surprising behaviors. -.. tacv:: instantiate (@num := @term) +.. tacv:: instantiate (@natural := @term) This variant allows to refer to an existential variable which was not named - by the user. The :n:`@num` argument is the position of the existential variable + by the user. The :n:`@natural` argument is the position of the existential variable from right to left in the goal. Because this variant is not robust to slight changes in the goal, its use is strongly discouraged. -.. tacv:: instantiate ( @num := @term ) in @ident - instantiate ( @num := @term ) in ( value of @ident ) - instantiate ( @num := @term ) in ( type of @ident ) +.. tacv:: instantiate ( @natural := @term ) in @ident + instantiate ( @natural := @term ) in ( value of @ident ) + instantiate ( @natural := @term ) in ( type of @ident ) These allow to refer respectively to existential variables occurring in a hypothesis or in the body or the type of a local definition. @@ -1730,13 +1724,13 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) of :tacn:`destruct`, it is erased (to avoid erasure, use parentheses, as in :n:`destruct (@ident)`). - .. tacv:: destruct @num + .. tacv:: destruct @natural - :n:`destruct @num` behaves as :n:`intros until @num` + :n:`destruct @natural` behaves as :n:`intros until @natural` followed by destruct applied to the last introduced hypothesis. .. note:: - For destruction of a numeral, use syntax :n:`destruct (@num)` (not + For destruction of a number, use syntax :n:`destruct (@natural)` (not very interesting anyway). .. tacv:: destruct @pattern @@ -1829,10 +1823,10 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) This tactic behaves as :n:`intros until @ident; case @ident` when :n:`@ident` is a quantified variable of the goal. -.. tacv:: simple destruct @num +.. tacv:: simple destruct @natural - This tactic behaves as :n:`intros until @num; case @ident` where :n:`@ident` - is the name given by :n:`intros until @num` to the :n:`@num` -th + This tactic behaves as :n:`intros until @natural; case @ident` where :n:`@ident` + is the name given by :n:`intros until @natural` to the :n:`@natural` -th non-dependent premise of the goal. .. tacv:: case_eq @term @@ -1863,12 +1857,12 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) @ident; induction @ident`. If :n:`@ident` is not anymore dependent in the goal after application of :n:`induction`, it is erased (to avoid erasure, use parentheses, as in :n:`induction (@ident)`). - + If :n:`@term` is a :n:`@num`, then :n:`induction @num` behaves as - :n:`intros until @num` followed by :n:`induction` applied to the last + + If :n:`@term` is a :n:`@natural`, then :n:`induction @natural` behaves as + :n:`intros until @natural` followed by :n:`induction` applied to the last introduced hypothesis. .. note:: - For simple induction on a numeral, use syntax induction (num) + For simple induction on a number, use syntax induction (number) (not very interesting anyway). + In case term is a hypothesis :n:`@ident` of the context, and :n:`@ident` @@ -2026,10 +2020,10 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) This tactic behaves as :n:`intros until @ident; elim @ident` when :n:`@ident` is a quantified variable of the goal. -.. tacv:: simple induction @num +.. tacv:: simple induction @natural - This tactic behaves as :n:`intros until @num; elim @ident` where :n:`@ident` - is the name given by :n:`intros until @num` to the :n:`@num`-th non-dependent + This tactic behaves as :n:`intros until @natural; elim @ident` where :n:`@ident` + is the name given by :n:`intros until @natural` to the :n:`@natural`-th non-dependent premise of the goal. .. tacn:: double induction @ident @ident @@ -2039,7 +2033,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) :n:`induction @ident; induction @ident` (or :n:`induction @ident ; destruct @ident` depending on the exact needs). -.. tacv:: double induction @num__1 @num__2 +.. tacv:: double induction @natural__1 @natural__2 This tactic is deprecated and should be replaced by :n:`induction num1; induction num3` where :n:`num3` is the result @@ -2148,9 +2142,9 @@ and an explanation of the underlying technique. .. exn:: Not a discriminable equality. :undocumented: -.. tacv:: discriminate @num +.. tacv:: discriminate @natural - This does the same thing as :n:`intros until @num` followed by + This does the same thing as :n:`intros until @natural` followed by :n:`discriminate @ident` where :n:`@ident` is the identifier for the last introduced hypothesis. @@ -2159,12 +2153,12 @@ and an explanation of the underlying technique. This does the same thing as :n:`discriminate @term` but using the given bindings to instantiate parameters or hypotheses of :n:`@term`. -.. tacv:: ediscriminate @num +.. tacv:: ediscriminate @natural ediscriminate @term {? with @bindings_list} :name: ediscriminate; _ This works the same as :tacn:`discriminate` but if the type of :token:`term`, or the - type of the hypothesis referred to by :token:`num`, has uninstantiated + type of the hypothesis referred to by :token:`natural`, has uninstantiated parameters, these parameters are left as existential variables. .. tacv:: discriminate @@ -2237,9 +2231,9 @@ and an explanation of the underlying technique. This error is given when one side of the equality is not a constructor. - .. tacv:: injection @num + .. tacv:: injection @natural - This does the same thing as :n:`intros until @num` followed by + This does the same thing as :n:`intros until @natural` followed by :n:`injection @ident` where :n:`@ident` is the identifier for the last introduced hypothesis. @@ -2248,12 +2242,12 @@ and an explanation of the underlying technique. This does the same as :n:`injection @term` but using the given bindings to instantiate parameters or hypotheses of :n:`@term`. - .. tacv:: einjection @num + .. tacv:: einjection @natural einjection @term {? with @bindings_list} :name: einjection; _ This works the same as :n:`injection` but if the type of :n:`@term`, or the - type of the hypothesis referred to by :n:`@num`, has uninstantiated + type of the hypothesis referred to by :n:`@natural`, has uninstantiated parameters, these parameters are left as existential variables. .. tacv:: injection @@ -2265,10 +2259,10 @@ and an explanation of the underlying technique. :undocumented: .. tacv:: injection @term {? with @bindings_list} as {+ @simple_intropattern} - injection @num as {+ @simple_intropattern} + injection @natural as {+ @simple_intropattern} injection as {+ @simple_intropattern} einjection @term {? with @bindings_list} as {+ @simple_intropattern} - einjection @num as {+ @simple_intropattern} + einjection @natural as {+ @simple_intropattern} einjection as {+ @simple_intropattern} These variants apply :n:`intros {+ @simple_intropattern}` after the call to @@ -2280,10 +2274,10 @@ and an explanation of the underlying technique. corresponds to a hypothesis. .. tacv:: injection @term {? with @bindings_list} as @injection_intropattern - injection @num as @injection_intropattern + injection @natural as @injection_intropattern injection as @injection_intropattern einjection @term {? with @bindings_list} as @injection_intropattern - einjection @num as @injection_intropattern + einjection @natural as @injection_intropattern einjection as @injection_intropattern These are equivalent to the previous variants but using instead the @@ -2332,9 +2326,9 @@ and an explanation of the underlying technique. :g:`Prop`). This behavior can be turned off by using the :flag:`Keep Proof Equalities` setting. -.. tacv:: inversion @num +.. tacv:: inversion @natural - This does the same thing as :n:`intros until @num` then :n:`inversion @ident` + This does the same thing as :n:`intros until @natural` then :n:`inversion @ident` where :n:`@ident` is the identifier for the last introduced hypothesis. .. tacv:: inversion_clear @ident @@ -2377,9 +2371,9 @@ and an explanation of the underlying technique. Goal forall l:list nat, contains0 (1 :: l) -> contains0 l. intros l H; inversion H as [ | l' p Hl' [Heqp Heql'] ]. -.. tacv:: inversion @num as @or_and_intropattern_loc +.. tacv:: inversion @natural as @or_and_intropattern_loc - This allows naming the hypotheses introduced by :n:`inversion @num` in the + This allows naming the hypotheses introduced by :n:`inversion @natural` in the context. .. tacv:: inversion_clear @ident as @or_and_intropattern_loc @@ -2627,7 +2621,7 @@ and an explanation of the underlying technique. .. seealso:: :tacn:`functional inversion` -.. tacn:: fix @ident @num +.. tacn:: fix @ident @natural :name: fix This tactic is a primitive tactic to start a proof by induction. In @@ -2635,11 +2629,11 @@ and an explanation of the underlying technique. as the ones described in :tacn:`induction`. In the syntax of the tactic, the identifier :n:`@ident` is the name given to - the induction hypothesis. The natural number :n:`@num` tells on which + the induction hypothesis. The natural number :n:`@natural` tells on which premise of the current goal the induction acts, starting from 1, counting both dependent and non dependent products, but skipping local definitions. Especially, the current lemma must be composed of at - least :n:`@num` products. + least :n:`@natural` products. Like in a fix expression, the induction hypotheses have to be used on structurally smaller arguments. The verification that inductive proof @@ -2648,7 +2642,7 @@ and an explanation of the underlying technique. is correct at some time of the interactive development of a proof, use the command ``Guarded`` (see Section :ref:`requestinginformation`). -.. tacv:: fix @ident @num with {+ (@ident {+ @binder} [{struct @ident}] : @type)} +.. tacv:: fix @ident @natural with {+ (@ident {+ @binder} [{struct @ident}] : @type)} This starts a proof by mutual induction. The statements to be simultaneously proved are respectively :g:`forall binder ... binder, type`. @@ -2758,11 +2752,11 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. + `?` : the tactic :n:`rewrite ?@term` performs the rewrite of :token:`term` as many times as possible (perhaps zero time). This form never fails. - + :n:`@num?` : works similarly, except that it will do at most :token:`num` rewrites. + + :n:`@natural?` : works similarly, except that it will do at most :token:`natural` rewrites. + `!` : works as `?`, except that at least one rewrite should succeed, otherwise the tactic fails. - + :n:`@num!` (or simply :n:`@num`) : precisely :token:`num` rewrites of :token:`term` will be done, - leading to failure if these :token:`num` rewrites are not possible. + + :n:`@natural!` (or simply :n:`@natural`) : precisely :token:`natural` rewrites of :token:`term` will be done, + leading to failure if these :token:`natural` rewrites are not possible. .. tacv:: erewrite @term :name: erewrite @@ -2939,15 +2933,15 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. This replaces the occurrences of :n:`@term` by :n:`@term’` in the current goal. The term :n:`@term` and :n:`@term’` must be convertible. - .. tacv:: change @term at {+ @num} with @term’ + .. tacv:: change @term at {+ @natural} with @term’ - This replaces the occurrences numbered :n:`{+ @num}` of :n:`@term` by :n:`@term’` + This replaces the occurrences numbered :n:`{+ @natural}` of :n:`@term` by :n:`@term’` in the current goal. The terms :n:`@term` and :n:`@term’` must be convertible. .. exn:: Too few occurrences. :undocumented: - .. tacv:: change @term {? {? at {+ @num}} with @term} in @ident + .. tacv:: change @term {? {? at {+ @natural}} with @term} in @ident This applies the :tacn:`change` tactic not to the goal but to the hypothesis :n:`@ident`. @@ -2992,9 +2986,9 @@ Performing computations | delta {? @delta_flag } ref_or_pattern_occ ::= @reference {? at @occs_nums } | @one_term {? at @occs_nums } - occs_nums ::= {+ {| @num | @ident } } - | - {| @num | @ident } {* @int_or_var } - int_or_var ::= @int + occs_nums ::= {+ {| @natural | @ident } } + | - {| @natural | @ident } {* @int_or_var } + int_or_var ::= @integer | @ident unfold_occ ::= @reference {? at @occs_nums } pattern_occ ::= @one_term {? at @occs_nums } @@ -3230,9 +3224,9 @@ the conversion in hypotheses :n:`{+ @ident}`. This applies :tacn:`simpl` only to the subterms matching :n:`@pattern` in the current goal. -.. tacv:: simpl @pattern at {+ @num} +.. tacv:: simpl @pattern at {+ @natural} - This applies :tacn:`simpl` only to the :n:`{+ @num}` occurrences of the subterms + This applies :tacn:`simpl` only to the :n:`{+ @natural}` occurrences of the subterms matching :n:`@pattern` in the current goal. .. exn:: Too few occurrences. @@ -3245,10 +3239,10 @@ the conversion in hypotheses :n:`{+ @ident}`. is the unfoldable constant :n:`@qualid` (the constant can be referred to by its notation using :n:`@string` if such a notation exists). -.. tacv:: simpl @qualid at {+ @num} - simpl @string at {+ @num} +.. tacv:: simpl @qualid at {+ @natural} + simpl @string at {+ @natural} - This applies :tacn:`simpl` only to the :n:`{+ @num}` applicative subterms whose + This applies :tacn:`simpl` only to the :n:`{+ @natural}` applicative subterms whose head occurrence is :n:`@qualid` (or :n:`@string`). .. flag:: Debug RAKAM @@ -3376,14 +3370,14 @@ the conversion in hypotheses :n:`{+ @ident}`. :g:`(fun x:A =>` :math:`\varphi`:g:`(x)) t`. This tactic can be used, for instance, when the tactic ``apply`` fails on matching. -.. tacv:: pattern @term at {+ @num} +.. tacv:: pattern @term at {+ @natural} - Only the occurrences :n:`{+ @num}` of :n:`@term` are considered for + Only the occurrences :n:`{+ @natural}` of :n:`@term` are considered for :math:`\beta`-expansion. Occurrences are located from left to right. -.. tacv:: pattern @term at - {+ @num} +.. tacv:: pattern @term at - {+ @natural} - All occurrences except the occurrences of indexes :n:`{+ @num }` + All occurrences except the occurrences of indexes :n:`{+ @natural }` of :n:`@term` are considered for :math:`\beta`-expansion. Occurrences are located from left to right. @@ -3396,12 +3390,12 @@ the conversion in hypotheses :n:`{+ @ident}`. If :g:`t`:sub:`i` occurs in one of the generated types :g:`A`:sub:`j` these occurrences will also be considered and possibly abstracted. -.. tacv:: pattern {+, @term at {+ @num}} +.. tacv:: pattern {+, @term at {+ @natural}} - This behaves as above but processing only the occurrences :n:`{+ @num}` of + This behaves as above but processing only the occurrences :n:`{+ @natural}` of :n:`@term` starting from :n:`@term`. -.. tacv:: pattern {+, @term {? at {? -} {+, @num}}} +.. tacv:: pattern {+, @term {? at {? -} {+, @natural}}} This is the most general syntax that combines the different variants. @@ -3558,9 +3552,9 @@ Automation :tacn:`simple apply` so it is expected that sometimes :tacn:`auto` will fail even if applying manually one of the hints would succeed. - .. tacv:: auto @num + .. tacv:: auto @natural - Forces the search depth to be :token:`num`. The maximal search depth + Forces the search depth to be :token:`natural`. The maximal search depth is 5 by default. .. tacv:: auto with {+ @ident} @@ -3611,7 +3605,7 @@ Automation Behaves like :tacn:`auto` but shows the tactics it tries to solve the goal, including failing paths. - .. tacv:: {? info_}auto {? @num} {? using {+ @qualid}} {? with {+ @ident}} + .. tacv:: {? info_}auto {? @natural} {? using {+ @qualid}} {? with {+ @ident}} This is the most general form, combining the various options. @@ -3666,7 +3660,7 @@ Automation Note that ``ex_intro`` should be declared as a hint. - .. tacv:: {? info_}eauto {? @num} {? using {+ @qualid}} {? with {+ @ident}} + .. tacv:: {? info_}eauto {? @natural} {? using {+ @qualid}} {? with {+ @ident}} The various options for :tacn:`eauto` are the same as for :tacn:`auto`. @@ -3829,12 +3823,12 @@ automatically created. .. deprecated:: 8.10 - .. cmdv:: Hint Resolve @qualid {? | {? @num} {? @pattern}} : @ident + .. cmdv:: Hint Resolve @qualid {? | {? @natural} {? @pattern}} : @ident :name: Hint Resolve This command adds :n:`simple apply @qualid` to the hint list with the head symbol of the type of :n:`@qualid`. The cost of that hint is the number of - subgoals generated by :n:`simple apply @qualid` or :n:`@num` if specified. The + subgoals generated by :n:`simple apply @qualid` or :n:`@natural` if specified. The associated :n:`@pattern` is inferred from the conclusion of the type of :n:`@qualid` or the given :n:`@pattern` if specified. In case the inferred type of :n:`@qualid` does not start with a product the tactic added in the hint list @@ -3932,7 +3926,7 @@ automatically created. overwriting the existing settings of opacity. It is advised to use this just after a :cmd:`Create HintDb` command. - .. cmdv:: Hint Extern @num {? @pattern} => @tactic : @ident + .. cmdv:: Hint Extern @natural {? @pattern} => @tactic : @ident :name: Hint Extern This hint type is to extend :tacn:`auto` with tactics other than :tacn:`apply` and @@ -3975,15 +3969,15 @@ automatically created. the following. Beware, there is no operator precedence during parsing, one can check with :cmd:`Print HintDb` to verify the current cut expression: - .. productionlist:: regexp - regexp : `ident` (hint or instance identifier) - : _ (any hint) - : `regexp` | `regexp` (disjunction) - : `regexp` `regexp` (sequence) - : `regexp` * (Kleene star) - : emp (empty) - : eps (epsilon) - : ( `regexp` ) + .. prodn:: + regexp ::= @ident (hint or instance identifier) + | _ (any hint) + | @regexp | @regexp (disjunction) + | @regexp @regexp (sequence) + | @regexp * (Kleene star) + | emp (empty) + | eps (epsilon) + | ( @regexp ) The `emp` regexp does not match any search path while `eps` matches the empty path. During proof search, the path of @@ -4361,7 +4355,7 @@ some incompatibilities. This combines the effects of the different variants of :tacn:`firstorder`. -.. opt:: Firstorder Depth @num +.. opt:: Firstorder Depth @natural :name: Firstorder Depth This option controls the proof-search depth bound. @@ -4398,10 +4392,10 @@ some incompatibilities. congruence. Qed. -.. tacv:: congruence @num +.. tacv:: congruence @natural - 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 + Tries to add at most :token:`natural` instances of hypotheses stating quantified equalities + to the problem in order to solve it. A bigger value of :token:`natural` 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. @@ -4600,9 +4594,9 @@ symbol :g:`=`. then :n:`simplify_eq @ident` first introduces the hypothesis in the local context using :n:`intros until @ident`. -.. tacv:: simplify_eq @num +.. tacv:: simplify_eq @natural - This does the same thing as :n:`intros until @num` then + This does the same thing as :n:`intros until @natural` then :n:`simplify_eq @ident` where :n:`@ident` is the identifier for the last introduced hypothesis. @@ -4611,12 +4605,12 @@ symbol :g:`=`. This does the same as :n:`simplify_eq @term` but using the given bindings to instantiate parameters or hypotheses of :n:`@term`. -.. tacv:: esimplify_eq @num +.. tacv:: esimplify_eq @natural esimplify_eq @term {? with @bindings_list} :name: esimplify_eq; _ This works the same as :tacn:`simplify_eq` but if the type of :n:`@term`, or the - type of the hypothesis referred to by :n:`@num`, has uninstantiated + type of the hypothesis referred to by :n:`@natural`, has uninstantiated parameters, these parameters are left as existential variables. .. tacv:: simplify_eq @@ -4672,17 +4666,15 @@ Automating tautologies. It solves goals of the form :g:`t = u` where `t` and `u` are constructed over the following grammar: - .. _btauto_grammar: - - .. productionlist:: sentence - 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` + .. prodn:: + 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. @@ -4741,12 +4733,12 @@ Non-logical tactics ------------------------ -.. tacn:: cycle @num +.. tacn:: cycle @integer :name: cycle - Reorders the selected goals so that the first :n:`@num` goals appear after the + Reorders the selected goals so that the first :n:`@integer` goals appear after the other selected goals. - If :n:`@num` is negative, it puts the last :n:`@num` goals at the + If :n:`@integer` is negative, it puts the last :n:`@integer` goals at the beginning of the list. The tactic is only useful with a goal selector, most commonly `all:`. Note that other selectors reorder goals; `1,3: cycle 1` is not equivalent @@ -4765,11 +4757,11 @@ Non-logical tactics all: cycle 2. all: cycle -3. -.. tacn:: swap @num @num +.. tacn:: swap @integer @integer :name: swap Exchanges the position of the specified goals. - Negative values for :n:`@num` indicate counting goals + Negative values for :n:`@integer` indicate counting goals backward from the end of the list of selected goals. Goals are indexed from 1. The tactic is only useful with a goal selector, most commonly `all:`. Note that other selectors reorder goals; `1,3: swap 1 3` is not equivalent @@ -4917,10 +4909,10 @@ Performance-oriented tactic variants .. tacv:: change_no_check @term with @term’ :undocumented: - .. tacv:: change_no_check @term at {+ @num} with @term’ + .. tacv:: change_no_check @term at {+ @natural} with @term’ :undocumented: - .. tacv:: change_no_check @term {? {? at {+ @num}} with @term} in @ident + .. tacv:: change_no_check @term {? {? at {+ @natural}} with @term} in @ident .. example:: diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 36ad4af837..6c07253bce 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -32,7 +32,7 @@ Displaying .. exn:: @qualid not a defined object. :undocumented: - .. exn:: Universe instance should have length @num. + .. exn:: Universe instance should have length @natural. :undocumented: .. exn:: This object does not support universe names. @@ -44,9 +44,9 @@ Displaying This command displays information about the current state of the environment, including sections and modules. -.. cmd:: Inspect @num +.. cmd:: Inspect @natural - This command displays the :n:`@num` last objects of the + This command displays the :n:`@natural` last objects of the current environment, including sections and modules. .. cmd:: Print Section @qualid @@ -60,7 +60,7 @@ Query commands -------------- Unlike other commands, :production:`query_command`\s may be prefixed with -a goal selector (:n:`@num:`) to specify which goal context it applies to. +a goal selector (:n:`@natural:`) to specify which goal context it applies to. 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`). @@ -757,10 +757,10 @@ interactively, they cannot be part of a vernacular file loaded via of the interactive session. -.. cmd:: Back {? @num } +.. cmd:: Back {? @natural } - Undoes all the effects of the last :n:`@num @sentence`\s. If - :n:`@num` is not specified, the command undoes one sentence. + Undoes all the effects of the last :n:`@natural @sentence`\s. If + :n:`@natural` is not specified, the command undoes one sentence. Sentences read from a `.v` file via a :cmd:`Load` are considered a single sentence. While :cmd:`Back` can undo tactics and commands executed within proof mode, once you exit proof mode, such as with :cmd:`Qed`, all @@ -772,14 +772,14 @@ interactively, they cannot be part of a vernacular file loaded via The user wants to undo more commands than available in the history. -.. cmd:: BackTo @num +.. cmd:: BackTo @natural - This command brings back the system to the state labeled :n:`@num`, + This command brings back the system to the state labeled :n:`@natural`, forgetting the effect of all commands executed after this state. The state label is an integer which grows after each successful command. It is displayed in the prompt when in -emacs mode. Just as :cmd:`Back` (see above), the :cmd:`BackTo` command now handles proof states. For that, it may - have to undo some extra commands and end on a state :n:`@num′ ≤ @num` if + have to undo some extra commands and end on a state :n:`@natural′ ≤ @natural` if necessary. .. _quitting-and-debugging: @@ -834,16 +834,16 @@ Quitting and debugging output to the file ":n:`@string`.out". -.. cmd:: Timeout @num @sentence +.. cmd:: Timeout @natural @sentence Executes :n:`@sentence`. If the operation - has not terminated after :n:`@num` seconds, then it is interrupted and an error message is + has not terminated after :n:`@natural` seconds, then it is interrupted and an error message is displayed. - .. opt:: Default Timeout @num + .. opt:: Default Timeout @natural :name: Default Timeout - If set, each :n:`@sentence` is treated as if it was prefixed with :cmd:`Timeout` :n:`@num`, + If set, each :n:`@sentence` is treated as if it was prefixed with :cmd:`Timeout` :n:`@natural`, except for :cmd:`Timeout` commands themselves. If unset, no timeout is applied. @@ -890,14 +890,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:: Printing Width @num +.. opt:: Printing Width @natural :name: Printing Width This command sets which left-aligned part of the width of the screen is used for display. At the time of writing this documentation, the default value is 78. -.. opt:: Printing Depth @num +.. opt:: Printing Depth @natural :name: Printing Depth This option controls the nesting depth of the formatter used for pretty- @@ -1028,7 +1028,7 @@ described first. .. prodn:: strategy_level ::= opaque - | @int + | @integer | expand | transparent strategy_level_or_var ::= @strategy_level @@ -1052,7 +1052,7 @@ described first. + ``opaque`` : level of opaque constants. They cannot be expanded by tactics (behaves like +∞, see next item). - + :n:`@int` : levels indexed by an integer. Level 0 corresponds to the + + :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 |