diff options
Diffstat (limited to 'doc/sphinx/proof-engine/tactics.rst')
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 168 |
1 files changed, 97 insertions, 71 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index cdd23f4d06..67d32835f5 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -462,7 +462,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 +2127,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. @@ -2294,7 +2294,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. @@ -2705,8 +2705,8 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. .. 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'` will rewrite `H` in the hypothesis ``H'`` instead of the current goal. @@ -2724,7 +2724,7 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. .. 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. @@ -2734,11 +2734,11 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. 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,12 +2799,12 @@ 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 @goal_occurences {? by @tactic} - replace -> @term in @goal_occurences - replace <- @term in @goal_occurences + .. 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 clauses - (:token:`goal_occurences`) (see :ref:`performingcomputations`) and not + (: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``. @@ -3065,7 +3065,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 @@ -3231,8 +3231,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} @@ -3265,51 +3265,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 + + 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. + + .. tacv:: unfold {+, @qualid} -.. tacv:: unfold @string + Replaces :n:`{+, @qualid}` with their definitions and replaces + the current goal 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 at @occurrences } -.. tacv:: unfold @string%@ident + The list :token:`occurrences` specify the occurrences of + :n:`@qualid` to be unfolded. Occurrences are located from left + to right. - 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`). + .. 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 {+, @qualid_or_string at {+, @num}} + .. tacv:: unfold @string%@ident - This is the most general form, where :n:`qualid_or_string` is either a - :n:`@qualid` or a :n:`@string` referring to a notation. + 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 @@ -3448,9 +3474,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. @@ -3458,8 +3484,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 @@ -3477,7 +3503,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. @@ -3490,10 +3516,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: @@ -3532,7 +3558,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`. @@ -3551,9 +3577,9 @@ Automation This tactic unfolds constants that were declared through a :cmd:`Hint Unfold` in the given databases. -.. tacv:: autounfold with {+ @ident} in @goal_occurences +.. tacv:: autounfold with {+ @ident} in @goal_occurrences - Performs the unfolding in the given clause (:token:`goal_occurences`). + Performs the unfolding in the given clause (:token:`goal_occurrences`). .. tacv:: autounfold with * @@ -3593,10 +3619,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:: @@ -3667,10 +3692,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. @@ -3719,7 +3745,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is 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. @@ -3739,7 +3765,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`. @@ -4557,14 +4583,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. |