diff options
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 340 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 33 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 30 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 96 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 240 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 29 |
6 files changed, 403 insertions, 365 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index bbd7e0ba3d..46f9826e41 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -32,24 +32,27 @@ 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 +The main entry of the grammar is :n:`@ltac_expr`. This language is used in proof mode but it can also be used in toplevel definitions as shown below. .. note:: @@ -86,41 +89,42 @@ mode but it can also be used in toplevel definitions as shown below. :n:`((try (repeat (@tactic__1 || @tactic__2)); @tactic__3); [ {+| @tactic } ]); @tactic__4` .. productionlist:: coq - expr : `expr` ; `expr` - : [> `expr` | ... | `expr` ] - : `expr` ; [ `expr` | ... | `expr` ] - : `tacexpr3` - tacexpr3 : do (`natural` | `ident`) `tacexpr3` - : progress `tacexpr3` - : repeat `tacexpr3` - : try `tacexpr3` - : once `tacexpr3` - : exactly_once `tacexpr3` - : timeout (`natural` | `ident`) `tacexpr3` - : time [`string`] `tacexpr3` - : only `selector`: `tacexpr3` - : `tacexpr2` - tacexpr2 : `tacexpr1` || `tacexpr3` - : `tacexpr1` + `tacexpr3` - : tryif `tacexpr1` then `tacexpr1` else `tacexpr1` - : `tacexpr1` - tacexpr1 : fun `name` ... `name` => `atom` + ltac_expr : `ltac_expr` ; `ltac_expr` + : [> `ltac_expr` | ... | `ltac_expr` ] + : `ltac_expr` ; [ `ltac_expr` | ... | `ltac_expr` ] + : `ltac_expr3` + ltac_expr3 : do (`natural` | `ident`) `ltac_expr3` + : progress `ltac_expr3` + : repeat `ltac_expr3` + : try `ltac_expr3` + : once `ltac_expr3` + : exactly_once `ltac_expr3` + : timeout (`natural` | `ident`) `ltac_expr3` + : time [`string`] `ltac_expr3` + : only `selector`: `ltac_expr3` + : `ltac_expr2` + ltac_expr2 : `ltac_expr1` || `ltac_expr3` + : `ltac_expr1` + `ltac_expr3` + : tryif `ltac_expr1` then `ltac_expr1` else `ltac_expr1` + : `ltac_expr1` + ltac_expr1 : fun `name` ... `name` => `atom` : let [rec] `let_clause` with ... with `let_clause` in `atom` : match goal with `context_rule` | ... | `context_rule` end : match reverse goal with `context_rule` | ... | `context_rule` end - : match `expr` with `match_rule` | ... | `match_rule` end + : match `ltac_expr` with `match_rule` | ... | `match_rule` end : lazymatch goal with `context_rule` | ... | `context_rule` end : lazymatch reverse goal with `context_rule` | ... | `context_rule` end - : lazymatch `expr` with `match_rule` | ... | `match_rule` end + : lazymatch `ltac_expr` with `match_rule` | ... | `match_rule` end : multimatch goal with `context_rule` | ... | `context_rule` end : multimatch reverse goal with `context_rule` | ... | `context_rule` end - : multimatch `expr` with `match_rule` | ... | `match_rule` end + : multimatch `ltac_expr` with `match_rule` | ... | `match_rule` end : abstract `atom` : abstract `atom` using `ident` - : first [ `expr` | ... | `expr` ] - : solve [ `expr` | ... | `expr` ] + : first [ `ltac_expr` | ... | `ltac_expr` ] + : solve [ `ltac_expr` | ... | `ltac_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` @@ -130,31 +134,31 @@ mode but it can also be used in toplevel definitions as shown below. : type_term `term` : numgoals : guard `test` - : assert_fails `tacexpr3` - : assert_succeeds `tacexpr3` - : `atomic_tactic` + : assert_fails `ltac_expr3` + : assert_succeeds `ltac_expr3` + : `tactic` : `qualid` `tacarg` ... `tacarg` : `atom` atom : `qualid` : () : `integer` - : ( `expr` ) + : ( `ltac_expr` ) component : `string` | `qualid` message_token : `string` | `ident` | `integer` tacarg : `qualid` : () : ltac : `atom` : `term` - let_clause : `ident` [`name` ... `name`] := `expr` - context_rule : `context_hyp`, ..., `context_hyp` |- `cpattern` => `expr` - : `cpattern` => `expr` - : |- `cpattern` => `expr` - : _ => `expr` + let_clause : `ident` [`name` ... `name`] := `ltac_expr` + context_rule : `context_hyp`, ..., `context_hyp` |- `cpattern` => `ltac_expr` + : `cpattern` => `ltac_expr` + : |- `cpattern` => `ltac_expr` + : _ => `ltac_expr` context_hyp : `name` : `cpattern` : `name` := `cpattern` [: `cpattern`] - match_rule : `cpattern` => `expr` - : context [`ident`] [ `cpattern` ] => `expr` - : _ => `expr` + match_rule : `cpattern` => `ltac_expr` + : context [`ident`] [ `cpattern` ] => `ltac_expr` + : _ => `ltac_expr` test : `integer` = `integer` : `integer` (< | <= | > | >=) `integer` selector : [`ident`] @@ -167,8 +171,8 @@ mode but it can also be used in toplevel definitions as shown below. .. productionlist:: coq top : [Local] Ltac `ltac_def` with ... with `ltac_def` - ltac_def : `ident` [`ident` ... `ident`] := `expr` - : `qualid` [`ident` ... `ident`] ::= `expr` + ltac_def : `ident` [`ident` ... `ident`] := `ltac_expr` + : `qualid` [`ident` ... `ident`] ::= `ltac_expr` .. _ltac-semantics: @@ -193,12 +197,12 @@ Sequence A sequence is an expression of the following form: -.. tacn:: @expr__1 ; @expr__2 +.. tacn:: @ltac_expr__1 ; @ltac_expr__2 :name: ltac-seq - The expression :n:`@expr__1` is evaluated to :n:`v__1`, which must be + The expression :n:`@ltac_expr__1` is evaluated to :n:`v__1`, which must be a tactic value. The tactic :n:`v__1` is applied to the current goal, - possibly producing more goals. Then :n:`@expr__2` is evaluated to + possibly producing more goals. Then :n:`@ltac_expr__2` is evaluated to produce :n:`v__2`, which must be a tactic value. The tactic :n:`v__2` is applied to all the goals produced by the prior application. Sequence is associative. @@ -209,10 +213,10 @@ Local application of tactics Different tactics can be applied to the different goals using the following form: -.. tacn:: [> {*| @expr }] +.. tacn:: [> {*| @ltac_expr }] :name: [> ... | ... | ... ] (dispatch) - The expressions :n:`@expr__i` are evaluated to :n:`v__i`, for + The expressions :n:`@ltac_expr__i` are evaluated to :n:`v__i`, for i = 1, ..., n and all have to be tactics. The :n:`v__i` is applied to the i-th goal, for i = 1, ..., n. It fails if the number of focused goals is not exactly n. @@ -223,31 +227,31 @@ following form: were given. For instance, ``[> | auto]`` is a shortcut for ``[> idtac | auto ]``. - .. tacv:: [> {*| @expr__i} | @expr .. | {*| @expr__j}] + .. tacv:: [> {*| @ltac_expr__i} | @ltac_expr .. | {*| @ltac_expr__j}] - In this variant, :n:`@expr` is used for each goal coming after those - covered by the list of :n:`@expr__i` but before those covered by the - list of :n:`@expr__j`. + In this variant, :n:`@ltac_expr` is used for each goal coming after those + covered by the list of :n:`@ltac_expr__i` but before those covered by the + list of :n:`@ltac_expr__j`. - .. tacv:: [> {*| @expr} | .. | {*| @expr}] + .. tacv:: [> {*| @ltac_expr} | .. | {*| @ltac_expr}] In this variant, idtac is used for the goals not covered by the two lists of - :n:`@expr`. + :n:`@ltac_expr`. - .. tacv:: [> @expr .. ] + .. tacv:: [> @ltac_expr .. ] - In this variant, the tactic :n:`@expr` is applied independently to each of + In this variant, the tactic :n:`@ltac_expr` is applied independently to each of the goals, rather than globally. In particular, if there are no goals, the tactic is not run at all. A tactic which expects multiple goals, such as ``swap``, would act as if a single goal is focused. - .. tacv:: @expr__0 ; [{*| @expr__i}] + .. tacv:: @ltac_expr__0 ; [{*| @ltac_expr__i}] This variant of local tactic application is paired with a sequence. In this - variant, there must be as many :n:`@expr__i` as goals generated - by the application of :n:`@expr__0` to each of the individual goals + variant, there must be as many :n:`@ltac_expr__i` as goals generated + by the application of :n:`@ltac_expr__0` to each of the individual goals independently. All the above variants work in this form too. - Formally, :n:`@expr ; [ ... ]` is equivalent to :n:`[> @expr ; [> ... ] .. ]`. + Formally, :n:`@ltac_expr ; [ ... ]` is equivalent to :n:`[> @ltac_expr ; [> ... ] .. ]`. .. _goal-selectors: @@ -257,53 +261,53 @@ Goal selectors We can restrict the application of a tactic to a subset of the currently focused goals with: -.. tacn:: @toplevel_selector : @expr +.. tacn:: @toplevel_selector : @ltac_expr :name: ... : ... (goal selector) We can also use selectors as a tactical, which allows to use them nested in a tactic expression, by using the keyword ``only``: - .. tacv:: only @selector : @expr + .. tacv:: only @selector : @ltac_expr :name: only ... : ... - When selecting several goals, the tactic :token:`expr` is applied globally to all + When selecting several goals, the tactic :token:`ltac_expr` is applied globally to all selected goals. - .. tacv:: [@ident] : @expr + .. tacv:: [@ident] : @ltac_expr - In this variant, :token:`expr` is applied locally to a goal previously named + In this variant, :token:`ltac_expr` is applied locally to a goal previously named by the user (see :ref:`existential-variables`). - .. tacv:: @num : @expr + .. tacv:: @num : @ltac_expr - In this variant, :token:`expr` is applied locally to the :token:`num`-th goal. + In this variant, :token:`ltac_expr` is applied locally to the :token:`num`-th goal. - .. tacv:: {+, @num-@num} : @expr + .. tacv:: {+, @num-@num} : @ltac_expr - In this variant, :n:`@expr` is applied globally to the subset of goals + In this variant, :n:`@ltac_expr` is applied globally to the subset of goals described by the given ranges. You can write a single ``n`` as a shortcut for ``n-n`` when specifying multiple ranges. - .. tacv:: all: @expr + .. tacv:: all: @ltac_expr :name: all: ... - In this variant, :token:`expr` is applied to all focused goals. ``all:`` can only + In this variant, :token:`ltac_expr` is applied to all focused goals. ``all:`` can only be used at the toplevel of a tactic expression. - .. tacv:: !: @expr + .. tacv:: !: @ltac_expr - In this variant, if exactly one goal is focused, :token:`expr` is + In this variant, if exactly one goal is focused, :token:`ltac_expr` is applied to it. Otherwise the tactic fails. ``!:`` can only be used at the toplevel of a tactic expression. - .. tacv:: par: @expr + .. tacv:: par: @ltac_expr :name: par: ... - In this variant, :n:`@expr` is applied to all focused goals in parallel. + In this variant, :n:`@ltac_expr` is applied to all focused goals in parallel. The number of workers can be controlled via the command line option ``-async-proofs-tac-j`` taking as argument the desired number of workers. Limitations: ``par:`` only works on goals containing no existential - variables and :n:`@expr` must either solve the goal completely or do + variables and :n:`@ltac_expr` must either solve the goal completely or do nothing (i.e. it cannot make some progress). ``par:`` can only be used at the toplevel of a tactic expression. @@ -318,10 +322,10 @@ For loop There is a for loop that repeats a tactic :token:`num` times: -.. tacn:: do @num @expr +.. tacn:: do @num @ltac_expr :name: do - :n:`@expr` is evaluated to ``v`` which must be a tactic value. This tactic + :n:`@ltac_expr` is evaluated to ``v`` which must be a tactic value. This tactic value ``v`` is applied :token:`num` times. Supposing :token:`num` > 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 the num @@ -332,24 +336,24 @@ Repeat loop We have a repeat loop with: -.. tacn:: repeat @expr +.. tacn:: repeat @ltac_expr :name: repeat - :n:`@expr` is evaluated to ``v``. If ``v`` denotes a tactic, this tactic is + :n:`@ltac_expr` is evaluated to ``v``. If ``v`` denotes a tactic, this tactic is applied to each focused goal independently. If the application succeeds, the tactic is applied recursively to all the generated subgoals until it eventually fails. The recursion stops in a subgoal when the tactic has failed *to make - progress*. The tactic :n:`repeat @expr` itself never fails. + progress*. The tactic :n:`repeat @ltac_expr` itself never fails. Error catching ~~~~~~~~~~~~~~ We can catch the tactic errors with: -.. tacn:: try @expr +.. tacn:: try @ltac_expr :name: try - :n:`@expr` is evaluated to ``v`` which must be a tactic value. The tactic + :n:`@ltac_expr` is evaluated to ``v`` which must be a tactic value. The tactic value ``v`` is applied to each focused goal independently. If the application of ``v`` fails in a goal, it catches the error and leaves the goal unchanged. If the level of the exception is positive, then the exception is re-raised with its @@ -360,10 +364,10 @@ Detecting progress We can check if a tactic made progress with: -.. tacn:: progress @expr +.. tacn:: progress @ltac_expr :name: progress - :n:`@expr` is evaluated to v which must be a tactic value. The tactic value ``v`` + :n:`@ltac_expr` is evaluated to v which must be a tactic value. The tactic value ``v`` is applied to each focued subgoal independently. If the application of ``v`` to one of the focused subgoal produced subgoals equal to the initial goals (up to syntactical equality), then an error of level 0 is raised. @@ -376,19 +380,19 @@ Backtracking branching We can branch with the following structure: -.. tacn:: @expr__1 + @expr__2 +.. tacn:: @ltac_expr__1 + @ltac_expr__2 :name: + (backtracking branching) - :n:`@expr__1` and :n:`@expr__2` are evaluated respectively to :n:`v__1` and + :n:`@ltac_expr__1` and :n:`@ltac_expr__2` are evaluated respectively to :n:`v__1` and :n:`v__2` which must be tactic values. The tactic value :n:`v__1` is applied to each focused goal independently and if it fails or a later tactic fails, then the proof backtracks to the current goal and :n:`v__2` is applied. Tactics can be seen as having several successes. When a tactic fails it asks for more successes of the prior tactics. - :n:`@expr__1 + @expr__2` has all the successes of :n:`v__1` followed by all the + :n:`@ltac_expr__1 + @ltac_expr__2` has all the successes of :n:`v__1` followed by all the successes of :n:`v__2`. Algebraically, - :n:`(@expr__1 + @expr__2); @expr__3 = (@expr__1; @expr__3) + (@expr__2; @expr__3)`. + :n:`(@ltac_expr__1 + @ltac_expr__2); @ltac_expr__3 = (@ltac_expr__1; @ltac_expr__3) + (@ltac_expr__2; @ltac_expr__3)`. Branching is left-associative. @@ -399,22 +403,22 @@ Backtracking branching may be too expensive. In this case we may restrict to a local, left biased, branching and consider the first tactic to work (i.e. which does not fail) among a panel of tactics: -.. tacn:: first [{*| @expr}] +.. tacn:: first [{*| @ltac_expr}] :name: first - The :n:`@expr__i` are evaluated to :n:`v__i` and :n:`v__i` must be + The :n:`@ltac_expr__i` are evaluated to :n:`v__i` and :n:`v__i` must be tactic values for i = 1, ..., n. Supposing n > 1, - :n:`first [@expr__1 | ... | @expr__n]` applies :n:`v__1` in each + :n:`first [@ltac_expr__1 | ... | @ltac_expr__n]` applies :n:`v__1` in each focused goal independently and stops if it succeeds; otherwise it tries to apply :n:`v__2` and so on. It fails when there is no applicable tactic. In other words, - :n:`first [@expr__1 | ... | @expr__n]` behaves, in each goal, as the first + :n:`first [@ltac_expr__1 | ... | @ltac_expr__n]` behaves, in each goal, as the first :n:`v__i` to have *at least* one success. .. exn:: No applicable tactic. :undocumented: - .. tacv:: first @expr + .. tacv:: first @ltac_expr This is an |Ltac| alias that gives a primitive access to the first tactical as an |Ltac| definition without going through a parsing rule. It @@ -433,14 +437,14 @@ Left-biased branching Yet another way of branching without backtracking is the following structure: -.. tacn:: @expr__1 || @expr__2 +.. tacn:: @ltac_expr__1 || @ltac_expr__2 :name: || (left-biased branching) - :n:`@expr__1` and :n:`@expr__2` are evaluated respectively to :n:`v__1` and + :n:`@ltac_expr__1` and :n:`@ltac_expr__2` are evaluated respectively to :n:`v__1` and :n:`v__2` which must be tactic values. The tactic value :n:`v__1` is applied in each subgoal independently and if it fails *to progress* then - :n:`v__2` is applied. :n:`@expr__1 || @expr__2` is - equivalent to :n:`first [ progress @expr__1 | @expr__2 ]` (except that + :n:`v__2` is applied. :n:`@ltac_expr__1 || @ltac_expr__2` is + equivalent to :n:`first [ progress @ltac_expr__1 | @ltac_expr__2 ]` (except that if it fails, it fails like :n:`v__2`). Branching is left-associative. Generalized biased branching @@ -448,19 +452,19 @@ Generalized biased branching The tactic -.. tacn:: tryif @expr__1 then @expr__2 else @expr__3 +.. tacn:: tryif @ltac_expr__1 then @ltac_expr__2 else @ltac_expr__3 :name: tryif is a generalization of the biased-branching tactics above. The - expression :n:`@expr__1` is evaluated to :n:`v__1`, which is then + expression :n:`@ltac_expr__1` is evaluated to :n:`v__1`, which is then applied to each subgoal independently. For each goal where :n:`v__1` - succeeds at least once, :n:`@expr__2` is evaluated to :n:`v__2` which + succeeds at least once, :n:`@ltac_expr__2` is evaluated to :n:`v__2` which is then applied collectively to the generated subgoals. The :n:`v__2` tactic can trigger backtracking points in :n:`v__1`: where :n:`v__1` succeeds at least once, - :n:`tryif @expr__1 then @expr__2 else @expr__3` is equivalent to + :n:`tryif @ltac_expr__1 then @ltac_expr__2 else @ltac_expr__3` is equivalent to :n:`v__1; v__2`. In each of the goals where :n:`v__1` does not succeed at least - once, :n:`@expr__3` is evaluated in :n:`v__3` which is is then applied to the + once, :n:`@ltac_expr__3` is evaluated in :n:`v__3` which is is then applied to the goal. Soft cut @@ -469,13 +473,13 @@ Soft cut Another way of restricting backtracking is to restrict a tactic to a single success *a posteriori*: -.. tacn:: once @expr +.. tacn:: once @ltac_expr :name: once - :n:`@expr` is evaluated to ``v`` which must be a tactic value. The tactic value + :n:`@ltac_expr` is evaluated to ``v`` which must be a tactic value. The tactic value ``v`` is applied but only its first success is used. If ``v`` fails, - :n:`once @expr` fails like ``v``. If ``v`` has at least one success, - :n:`once @expr` succeeds once, but cannot produce more successes. + :n:`once @ltac_expr` fails like ``v``. If ``v`` has at least one success, + :n:`once @ltac_expr` succeeds once, but cannot produce more successes. Checking the successes ~~~~~~~~~~~~~~~~~~~~~~ @@ -483,14 +487,14 @@ Checking the successes Coq provides an experimental way to check that a tactic has *exactly one* success: -.. tacn:: exactly_once @expr +.. tacn:: exactly_once @ltac_expr :name: exactly_once - :n:`@expr` is evaluated to ``v`` which must be a tactic value. The tactic value + :n:`@ltac_expr` is evaluated to ``v`` which must be a tactic value. The tactic value ``v`` is applied if it has at most one success. If ``v`` fails, - :n:`exactly_once @expr` fails like ``v``. If ``v`` has a exactly one success, - :n:`exactly_once @expr` succeeds like ``v``. If ``v`` has two or more - successes, exactly_once expr fails. + :n:`exactly_once @ltac_expr` fails like ``v``. If ``v`` has a exactly one success, + :n:`exactly_once @ltac_expr` succeeds like ``v``. If ``v`` has two or more + successes, :n:`exactly_once @ltac_expr` fails. .. warning:: @@ -509,10 +513,10 @@ Checking the failure Coq provides a derived tactic to check that a tactic *fails*: -.. tacn:: assert_fails @expr +.. tacn:: assert_fails @ltac_expr :name: assert_fails - This behaves like :n:`tryif @expr then fail 0 tac "succeeds" else idtac`. + This behaves like :n:`tryif @ltac_expr then fail 0 tac "succeeds" else idtac`. Checking the success ~~~~~~~~~~~~~~~~~~~~ @@ -520,7 +524,7 @@ Checking the success Coq provides a derived tactic to check that a tactic has *at least one* success: -.. tacn:: assert_succeeds @expr +.. tacn:: assert_succeeds @ltac_expr :name: assert_succeeds This behaves like @@ -532,19 +536,19 @@ Solving We may consider the first to solve (i.e. which generates no subgoal) among a panel of tactics: -.. tacn:: solve [{*| @expr}] +.. tacn:: solve [{*| @ltac_expr}] :name: solve - The :n:`@expr__i` are evaluated to :n:`v__i` and :n:`v__i` must be + The :n:`@ltac_expr__i` are evaluated to :n:`v__i` and :n:`v__i` must be tactic values, for i = 1, ..., n. Supposing n > 1, - :n:`solve [@expr__1 | ... | @expr__n]` applies :n:`v__1` to + :n:`solve [@ltac_expr__1 | ... | @ltac_expr__n]` applies :n:`v__1` to each goal independently and stops if it succeeds; otherwise it tries to apply :n:`v__2` and so on. It fails if there is no solving tactic. .. exn:: Cannot solve the goal. :undocumented: - .. tacv:: solve @expr + .. tacv:: solve @ltac_expr This is an |Ltac| alias that gives a primitive access to the :n:`solve:` tactical. See the :n:`first` tactical for more information. @@ -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 @@ -647,10 +651,10 @@ Timeout We can force a tactic to stop if it has not finished after a certain amount of time: -.. tacn:: timeout @num @expr +.. tacn:: timeout @num @ltac_expr :name: timeout - :n:`@expr` is evaluated to ``v`` which must be a tactic value. The tactic value + :n:`@ltac_expr` 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 if it is still running. In this case the outcome is a failure. @@ -669,10 +673,10 @@ Timing a tactic A tactic execution can be timed: -.. tacn:: time @string @expr +.. tacn:: time @string @ltac_expr :name: time - evaluates :n:`@expr` and displays the running time of the tactic expression, whether it + evaluates :n:`@ltac_expr` and displays the running time of the tactic expression, whether it fails or succeeds. In case of several successes, the time for each successive run is displayed. Time is in seconds and is machine-dependent. The :n:`@string` argument is optional. When provided, it is used to identify this particular @@ -684,10 +688,10 @@ Timing a tactic that evaluates to a term Tactic expressions that produce terms can be timed with the experimental tactic -.. tacn:: time_constr @expr +.. tacn:: time_constr @ltac_expr :name: time_constr - which evaluates :n:`@expr ()` and displays the time the tactic expression + which evaluates :n:`@ltac_expr ()` and displays the time the tactic expression evaluated, assuming successful evaluation. Time is in seconds and is machine-dependent. @@ -708,7 +712,7 @@ tactic for printing. By copying the definition of :tacn:`time_constr` from the standard library, - users can achive support for a fixed pattern of nesting by passing + users can achieve support for a fixed pattern of nesting by passing different :token:`string` parameters to :tacn:`restart_timer` and :tacn:`finish_timing` at each level of nesting. @@ -735,12 +739,12 @@ Local definitions Local definitions can be done as follows: -.. tacn:: let @ident__1 := @expr__1 {* with @ident__i := @expr__i} in @expr +.. tacn:: let @ident__1 := @ltac_expr__1 {* with @ident__i := @ltac_expr__i} in @ltac_expr :name: let ... := ... - each :n:`@expr__i` is evaluated to :n:`v__i`, then, :n:`@expr` is evaluated + each :n:`@ltac_expr__i` is evaluated to :n:`v__i`, then, :n:`@ltac_expr` is evaluated by substituting :n:`v__i` to each occurrence of :n:`@ident__i`, for - i = 1, ..., n. There are no dependencies between the :n:`@expr__i` and the + i = 1, ..., n. There are no dependencies between the :n:`@ltac_expr__i` and the :n:`@ident__i`. Local definitions can be made recursive by using :n:`let rec` instead of :n:`let`. @@ -759,7 +763,7 @@ An application is an expression of the following form: The reference :n:`@qualid` must be bound to some defined tactic definition expecting at least as many arguments as the provided :n:`tacarg`. The - expressions :n:`@expr__i` are evaluated to :n:`v__i`, for i = 1, ..., n. + expressions :n:`@ltac_expr__i` are evaluated to :n:`v__i`, for i = 1, ..., n. .. what expressions ?? @@ -769,7 +773,7 @@ Function construction A parameterized tactic can be built anonymously (without resorting to local definitions) with: -.. tacn:: fun {+ @ident} => @expr +.. tacn:: fun {+ @ident} => @ltac_expr Indeed, local definitions of functions are a syntactic sugar for binding a :n:`fun` tactic to an identifier. @@ -779,9 +783,9 @@ Pattern matching on terms We can carry out pattern matching on terms with: -.. tacn:: match @expr with {+| @cpattern__i => @expr__i} end +.. tacn:: match @ltac_expr with {+| @cpattern__i => @ltac_expr__i} end - The expression :n:`@expr` is evaluated and should yield a term which is + The expression :n:`@ltac_expr` is evaluated and should yield a term which is matched against :n:`cpattern__1`. The matching is non-linear: if a metavariable occurs more than once, it should match the same expression every time. It is first-order except on the variables of the form :n:`@?id` @@ -795,20 +799,20 @@ We can carry out pattern matching on terms with: same types. This provides with a primitive form of matching under context which does not require manipulating a functional term. - If the matching with :n:`@cpattern__1` succeeds, then :n:`@expr__1` is + If the matching with :n:`@cpattern__1` succeeds, then :n:`@ltac_expr__1` is evaluated into some value by substituting the pattern matching - instantiations to the metavariables. If :n:`@expr__1` evaluates to a + instantiations to the metavariables. If :n:`@ltac_expr__1` evaluates to a tactic and the match expression is in position to be applied to a goal (e.g. it is not bound to a variable by a :n:`let in`), then this tactic is applied. If the tactic succeeds, the list of resulting subgoals is the - result of the match expression. If :n:`@expr__1` does not evaluate to a + result of the match expression. If :n:`@ltac_expr__1` does not evaluate to a tactic or if the match expression is not in position to be applied to a - goal, then the result of the evaluation of :n:`@expr__1` is the result + goal, then the result of the evaluation of :n:`@ltac_expr__1` is the result of the match expression. If the matching with :n:`@cpattern__1` fails, or if it succeeds but the - evaluation of :n:`@expr__1` fails, or if the evaluation of - :n:`@expr__1` succeeds but returns a tactic in execution position whose + evaluation of :n:`@ltac_expr__1` fails, or if the evaluation of + :n:`@ltac_expr__1` succeeds but returns a tactic in execution position whose execution fails, then :n:`cpattern__2` is used and so on. The pattern :n:`_` matches any term and shadows all remaining patterns if any. If all clauses fail (in particular, there is no pattern :n:`_`) then a @@ -824,9 +828,9 @@ We can carry out pattern matching on terms with: .. exn:: Argument of match does not evaluate to a term. - This happens when :n:`@expr` does not denote a term. + This happens when :n:`@ltac_expr` does not denote a term. - .. tacv:: multimatch @expr with {+| @cpattern__i => @expr__i} end + .. tacv:: multimatch @ltac_expr with {+| @cpattern__i => @ltac_expr__i} end Using multimatch instead of match will allow subsequent tactics to backtrack into a right-hand side tactic which has backtracking points @@ -835,7 +839,7 @@ We can carry out pattern matching on terms with: The syntax :n:`match …` is, in fact, a shorthand for :n:`once multimatch …`. - .. tacv:: lazymatch @expr with {+| @cpattern__i => @expr__i} end + .. tacv:: lazymatch @ltac_expr with {+| @cpattern__i => @ltac_expr__i} end Using lazymatch instead of match will perform the same pattern matching procedure but will commit to the first matching branch @@ -880,13 +884,13 @@ We can perform pattern matching on goals using the following expression: .. we should provide the full grammar here -.. tacn:: match goal with {+| {+, @context_hyp} |- @cpattern => @expr } | _ => @expr end +.. tacn:: match goal with {+| {+, @context_hyp} |- @cpattern => @ltac_expr } | _ => @ltac_expr end :name: match goal If each hypothesis pattern :n:`hyp`\ :sub:`1,i`, with i = 1, ..., m\ :sub:`1` is matched (non-linear first-order unification) by a hypothesis of the goal and if :n:`cpattern_1` is matched by the conclusion of the goal, - then :n:`@expr__1` is evaluated to :n:`v__1` by substituting the + then :n:`@ltac_expr__1` is evaluated to :n:`v__1` by substituting the pattern matching to the metavariables and the real hypothesis names bound to the possible hypothesis names occurring in the hypothesis patterns. If :n:`v__1` is a tactic value, then it is applied to the @@ -894,7 +898,7 @@ We can perform pattern matching on goals using the following expression: is tried with the same proof context pattern. If there is no other combination of hypotheses then the second proof context pattern is tried and so on. If the next to last proof context pattern fails then - the last :n:`@expr` is evaluated to :n:`v` and :n:`v` is + the last :n:`@ltac_expr` is evaluated to :n:`v` and :n:`v` is applied. Note also that matching against subterms (using the :n:`context @ident [ @cpattern ]`) is available and is also subject to yielding several matchings. @@ -918,7 +922,7 @@ We can perform pattern matching on goals using the following expression: first), but it possible to reverse this order (oldest first) with the :n:`match reverse goal with` variant. - .. tacv:: multimatch goal with {+| {+, @context_hyp} |- @cpattern => @expr } | _ => @expr end + .. tacv:: multimatch goal with {+| {+, @context_hyp} |- @cpattern => @ltac_expr } | _ => @ltac_expr end Using :n:`multimatch` instead of :n:`match` will allow subsequent tactics to backtrack into a right-hand side tactic which has backtracking points @@ -929,7 +933,7 @@ We can perform pattern matching on goals using the following expression: The syntax :n:`match [reverse] goal …` is, in fact, a shorthand for :n:`once multimatch [reverse] goal …`. - .. tacv:: lazymatch goal with {+| {+, @context_hyp} |- @cpattern => @expr } | _ => @expr end + .. tacv:: lazymatch goal with {+| {+, @context_hyp} |- @cpattern => @ltac_expr } | _ => @ltac_expr end Using lazymatch instead of match will perform the same pattern matching procedure but will commit to the first matching branch with the first @@ -944,11 +948,11 @@ Filling a term context The following expression is not a tactic in the sense that it does not produce subgoals but generates a term to be used in tactic expressions: -.. tacn:: context @ident [@expr] +.. tacn:: context @ident [@ltac_expr] :n:`@ident` must denote a context variable bound by a context pattern of a match expression. This expression evaluates replaces the hole of the - value of :n:`@ident` by the value of :n:`@expr`. + value of :n:`@ident` by the value of :n:`@ltac_expr`. .. exn:: Not a context variable. :undocumented: @@ -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 @@ -1068,10 +1072,10 @@ Testing boolean expressions Proving a subgoal as a separate lemma ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. tacn:: abstract @expr +.. tacn:: abstract @ltac_expr :name: abstract - From the outside, :n:`abstract @expr` is the same as :n:`solve @expr`. + From the outside, :n:`abstract @ltac_expr` is the same as :n:`solve @ltac_expr`. Internally it saves an auxiliary lemma called ``ident_subproofn`` where ``ident`` is the name of the current goal and ``n`` is chosen so that this is a fresh name. Such an auxiliary lemma is inlined in the final proof term. @@ -1094,7 +1098,7 @@ Proving a subgoal as a separate lemma if used as part of typeclass resolution, it may produce wrong terms when in universe polymorphic mode. - .. tacv:: abstract @expr using @ident + .. tacv:: abstract @ltac_expr using @ident Give explicitly the name of the auxiliary lemma. @@ -1103,7 +1107,7 @@ Proving a subgoal as a separate lemma Use this feature at your own risk; explicitly named and reused subterms don’t play well with asynchronous proofs. - .. tacv:: transparent_abstract @expr + .. tacv:: transparent_abstract @ltac_expr :name: transparent_abstract Save the subproof in a transparent lemma rather than an opaque one. @@ -1113,7 +1117,7 @@ Proving a subgoal as a separate lemma Use this feature at your own risk; building computationally relevant terms with tactics is fragile. - .. tacv:: transparent_abstract @expr using @ident + .. tacv:: transparent_abstract @ltac_expr using @ident Give explicitly the name of the auxiliary transparent lemma. @@ -1135,7 +1139,7 @@ Defining |Ltac| functions Basically, |Ltac| toplevel definitions are made as follows: -.. cmd:: {? Local} Ltac @ident {* @ident} := @expr +.. cmd:: {? Local} Ltac @ident {* @ident} := @ltac_expr :name: Ltac This defines a new |Ltac| function that can be used in any tactic @@ -1148,13 +1152,13 @@ Basically, |Ltac| toplevel definitions are made as follows: The preceding definition can equivalently be written: - :n:`Ltac @ident := fun {+ @ident} => @expr` + :n:`Ltac @ident := fun {+ @ident} => @ltac_expr` - .. cmdv:: Ltac @ident {* @ident} {* with @ident {* @ident}} := @expr + .. cmdv:: Ltac @ident {* @ident} {* with @ident {* @ident}} := @ltac_expr This syntax allows recursive and mutual recursive function definitions. - .. cmdv:: Ltac @qualid {* @ident} ::= @expr + .. cmdv:: Ltac @qualid {* @ident} ::= @ltac_expr This syntax *redefines* an existing user-defined tactic. @@ -1581,7 +1585,7 @@ Backtraces Info trace ~~~~~~~~~~ -.. cmd:: Info @num @expr +.. cmd:: Info @num @ltac_expr :name: Info This command can be used to print the trace of the path eventually taken by an @@ -1676,7 +1680,7 @@ It is possible to measure the time spent in invocations of primitive tactics as well as tactics defined in |Ltac| and their inner invocations. The primary use is the development of complex tactics, which can sometimes be so slow as to impede interactive usage. The -reasons for the performence degradation can be intricate, like a slowly +reasons for the performance degradation can be intricate, like a slowly performing |Ltac| match or a sub-tactic whose performance only degrades in certain situations. The profiler generates a call tree and indicates the time spent in a tactic depending on its calling context. Thus diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index aa603fc966..36eeff6192 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 @@ -655,6 +655,8 @@ this features has the same semantics as in Ltac1. In particular, a ``reverse`` flag can be specified to match hypotheses from the more recently introduced to the least recently introduced one. +.. _ltac2_notations: + Notations --------- @@ -679,6 +681,11 @@ The following scopes are built-in. + parses :n:`c = @term` and produces :n:`constr:(c)` + This scope can be parameterized by a list of delimiting keys of interpretation + scopes (as described in :ref:`LocalInterpretationRulesForNotations`), + describing how to interpret the parsed term. For instance, :n:`constr(A, B)` + parses :n:`c = @term` and produces :n:`constr:(c%A%B)`. + - :n:`ident`: + parses :n:`id = @ident` and produces :n:`ident:(id)` @@ -686,20 +693,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..0cff987a27 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 @@ -535,19 +535,6 @@ Requesting information eexists ?[n]. Show n. - .. cmdv:: Show Script - :name: Show Script - - Displays the whole list of tactics applied from the - beginning of the current proof. This tactics script may contain some - holes (subgoals not yet proved). They are printed under the form - - ``<Your Tactic Text here>``. - - .. deprecated:: 8.10 - - Please use a text editor. - .. cmdv:: Show Proof :name: Show Proof @@ -705,9 +692,10 @@ command in CoqIDE. You can change the background colors shown for diffs from th lets you control other attributes of the highlights, such as the foreground color, bold, italic, underline and strikeout. -Note: As of this writing (August 2018), Proof General will need minor changes -to be able to show diffs correctly. We hope it will support this feature soon. -See https://github.com/ProofGeneral/PG/issues/381 for the current status. +As of June 2019, Proof General can also display Coq-generated proof diffs automatically. +Please see the PG documentation section +"`Showing Proof Diffs" <https://proofgeneral.github.io/doc/master/userman/Coq-Proof-General#Showing-Proof-Diffs>`_) +for details. How diffs are calculated ```````````````````````` diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 75e019592f..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 @@ -853,7 +853,7 @@ An *occurrence switch* can be: algorithm in a local definition, instead of copying large terms by hand. -It is important to remember that matching *preceeds* occurrence +It is important to remember that matching *precedes* occurrence selection. .. example:: @@ -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 @@ -2455,7 +2455,7 @@ the holes are abstracted in term. Lemma test : True. have: _ * 0 = 0. - The invokation of ``have`` is equivalent to: + The invocation of ``have`` is equivalent to: .. coqtop:: reset none @@ -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. @@ -4927,7 +4927,7 @@ bookkeeping steps. apply/PQequiv. thus in this case, the tactic ``apply/PQequiv`` is equivalent to - ``apply: (iffRL (PQequiv _ _))``, where ``iffRL`` is tha analogue of + ``apply: (iffRL (PQequiv _ _))``, where ``iffRL`` is the analogue of ``iffRL`` for the converse implication. Any |SSR| term whose type coerces to a double implication can be @@ -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 4e47621938..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. @@ -3714,11 +3754,11 @@ The general command to add a hint to some databases :n:`{+ @ident}` is .. cmdv:: Hint Resolve -> @term : @ident Adds the left-to-right implication of an equivalence as a hint (informally - the hint will be used as :n:`apply <- @term`, although as mentionned + the hint will be used as :n:`apply <- @term`, although as mentioned 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`. @@ -3783,7 +3823,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is This sets the transparency flag used during unification of hints in the database for all constants or all variables, - overwritting the existing settings of opacity. It is advised + 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 @@ -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. |