diff options
Diffstat (limited to 'doc/sphinx/proofs/writing-proofs/rewriting.rst')
| -rw-r--r-- | doc/sphinx/proofs/writing-proofs/rewriting.rst | 857 |
1 files changed, 857 insertions, 0 deletions
diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst new file mode 100644 index 0000000000..1358aad432 --- /dev/null +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -0,0 +1,857 @@ +================================= +Term rewriting and simplification +================================= + +.. _rewritingexpressions: + +Rewriting expressions +--------------------- + +These tactics use the equality :g:`eq:forall A:Type, A->A->Prop` defined in +file ``Logic.v`` (see :ref:`coq-library-logic`). The notation for :g:`eq T t u` is +simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. + +.. tacn:: rewrite @term + :name: rewrite + + This tactic applies to any goal. The type of :token:`term` must have the form + + ``forall (x``:sub:`1` ``:A``:sub:`1` ``) ... (x``:sub:`n` ``:A``:sub:`n` ``), eq term``:sub:`1` ``term``:sub:`2` ``.`` + + where :g:`eq` is the Leibniz equality or a registered setoid equality. + + Then :n:`rewrite @term` finds the first subterm matching `term`\ :sub:`1` in the goal, + resulting in instances `term`:sub:`1`' and `term`:sub:`2`' and then + replaces every occurrence of `term`:subscript:`1`' by `term`:subscript:`2`'. + Hence, some of the variables :g:`x`\ :sub:`i` are solved by unification, + and some of the types :g:`A`\ :sub:`1`:g:`, ..., A`\ :sub:`n` become new + subgoals. + + .. exn:: The @term provided does not end with an equation. + :undocumented: + + .. exn:: Tactic generated a subgoal identical to the original goal. This happens if @term does not occur in the goal. + :undocumented: + + .. tacv:: rewrite -> @term + + Is equivalent to :n:`rewrite @term` + + .. tacv:: rewrite <- @term + + Uses the equality :n:`@term`:sub:`1` :n:`= @term` :sub:`2` from right to left + + .. tacv:: rewrite @term in @goal_occurrences + + 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. + + :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'` 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 + + 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 + + Use tactic to completely solve the side-conditions arising from the + :tacn:`rewrite`. + + .. 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. 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. + + In all forms of rewrite described above, a :token:`term` to rewrite can be + immediately prefixed by one of the following modifiers: + + + `?` : the tactic :n:`rewrite ?@term` performs the rewrite of :token:`term` as many + times as possible (perhaps zero time). This form never fails. + + :n:`@natural?` : works similarly, except that it will do at most :token:`natural` rewrites. + + `!` : works as `?`, except that at least one rewrite should succeed, otherwise + the tactic fails. + + :n:`@natural!` (or simply :n:`@natural`) : precisely :token:`natural` rewrites of :token:`term` will be done, + leading to failure if these :token:`natural` rewrites are not possible. + + .. tacv:: erewrite @term + :name: erewrite + + This tactic works as :n:`rewrite @term` but turning + unresolved bindings into existential variables, if any, instead of + failing. It has the same variants as :tacn:`rewrite` has. + + .. flag:: Keyed Unification + + Makes higher-order unification used by :tacn:`rewrite` rely on a set of keys to drive + unification. The subterms, considered as rewriting candidates, must start with + the same key as the left- or right-hand side of the lemma given to rewrite, and the arguments + are then unified up to full reduction. + +.. tacn:: replace @term with @term’ + :name: replace + + This tactic applies to any goal. It replaces all free occurrences of :n:`@term` + in the current goal with :n:`@term’` and generates an equality :n:`@term = @term’` + as a subgoal. This equality is automatically solved if it occurs among + the assumptions, or if its symmetric form occurs. It is equivalent to + :n:`cut @term = @term’; [intro H`:sub:`n` :n:`; rewrite <- H`:sub:`n` :n:`; clear H`:sub:`n`:n:`|| assumption || symmetry; try assumption]`. + + .. exn:: Terms do not have convertible types. + :undocumented: + + .. tacv:: replace @term with @term’ by @tactic + + This acts as :n:`replace @term with @term’` but applies :token:`tactic` to solve the generated + subgoal :n:`@term = @term’`. + + .. tacv:: replace @term + + Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has + the form :n:`@term = @term’` or :n:`@term’ = @term`. + + .. tacv:: replace -> @term + + Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has + the form :n:`@term = @term’` + + .. tacv:: replace <- @term + + 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_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_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``. + +.. tacn:: subst @ident + :name: subst + + This tactic applies to a goal that has :n:`@ident` in its context and (at + least) one hypothesis, say :g:`H`, of type :n:`@ident = t` or :n:`t = @ident` + with :n:`@ident` not occurring in :g:`t`. Then it replaces :n:`@ident` by + :g:`t` everywhere in the goal (in the hypotheses and in the conclusion) and + clears :n:`@ident` and :g:`H` from the context. + + If :n:`@ident` is a local definition of the form :n:`@ident := t`, it is also + unfolded and cleared. + + If :n:`@ident` is a section variable it is expected to have no + indirect occurrences in the goal, i.e. that no global declarations + implicitly depending on the section variable must be present in the + goal. + + .. note:: + + When several hypotheses have the form :n:`@ident = t` or :n:`t = @ident`, the + first one is used. + + + If :g:`H` is itself dependent in the goal, it is replaced by the proof of + reflexivity of equality. + + .. tacv:: subst {+ @ident} + + This is equivalent to :n:`subst @ident`:sub:`1`:n:`; ...; subst @ident`:sub:`n`. + + .. tacv:: subst + + This applies :tacn:`subst` repeatedly from top to bottom to all hypotheses of the + context for which an equality of the form :n:`@ident = t` or :n:`t = @ident` + or :n:`@ident := t` exists, with :n:`@ident` not occurring in + ``t`` and :n:`@ident` not a section variable with indirect + dependencies in the goal. + + .. flag:: Regular Subst Tactic + + This flag controls the behavior of :tacn:`subst`. When it is + activated (it is by default), :tacn:`subst` also deals with the following corner cases: + + + A context with ordered hypotheses :n:`@ident`:sub:`1` :n:`= @ident`:sub:`2` + and :n:`@ident`:sub:`1` :n:`= t`, or :n:`t′ = @ident`:sub:`1`` with `t′` not + a variable, and no other hypotheses of the form :n:`@ident`:sub:`2` :n:`= u` + or :n:`u = @ident`:sub:`2`; without the flag, a second call to + subst would be necessary to replace :n:`@ident`:sub:`2` by `t` or + `t′` respectively. + + The presence of a recursive equation which without the flag would + be a cause of failure of :tacn:`subst`. + + A context with cyclic dependencies as with hypotheses :n:`@ident`:sub:`1` :n:`= f @ident`:sub:`2` + and :n:`@ident`:sub:`2` :n:`= g @ident`:sub:`1` which without the + flag would be a cause of failure of :tacn:`subst`. + + Additionally, it prevents a local definition such as :n:`@ident := t` to be + unfolded which otherwise it would exceptionally unfold in configurations + containing hypotheses of the form :n:`@ident = u`, or :n:`u′ = @ident` + with `u′` not a variable. Finally, it preserves the initial order of + hypotheses, which without the flag it may break. + default. + + .. exn:: Cannot find any non-recursive equality over :n:`@ident`. + :undocumented: + + .. exn:: Section variable :n:`@ident` occurs implicitly in global declaration :n:`@qualid` present in hypothesis :n:`@ident`. + Section variable :n:`@ident` occurs implicitly in global declaration :n:`@qualid` present in the conclusion. + + Raised when the variable is a section variable with indirect + dependencies in the goal. + + +.. tacn:: stepl @term + :name: stepl + + This tactic is for chaining rewriting steps. It assumes a goal of the + form :n:`R @term @term` where ``R`` is a binary relation and relies on a + database of lemmas of the form :g:`forall x y z, R x y -> eq x z -> R z y` + where `eq` is typically a setoid equality. The application of :n:`stepl @term` + then replaces the goal by :n:`R @term @term` and adds a new goal stating + :n:`eq @term @term`. + + .. cmd:: Declare Left Step @term + + Adds :n:`@term` to the database used by :tacn:`stepl`. + + This tactic is especially useful for parametric setoids which are not accepted + as regular setoids for :tacn:`rewrite` and :tacn:`setoid_replace` (see + :ref:`Generalizedrewriting`). + + .. tacv:: stepl @term by @tactic + + This applies :n:`stepl @term` then applies :token:`tactic` to the second goal. + + .. tacv:: stepr @term by @tactic + :name: stepr + + This behaves as :tacn:`stepl` but on the right-hand-side of the binary + relation. Lemmas are expected to be of the form + :g:`forall x y z, R x y -> eq y z -> R x z`. + + .. cmd:: Declare Right Step @term + + Adds :n:`@term` to the database used by :tacn:`stepr`. + + +.. tacn:: change @term + :name: change + + This tactic applies to any goal. It implements the rule ``Conv`` given in + :ref:`subtyping-rules`. :g:`change U` replaces the current goal `T` + with `U` providing that `U` is well-formed and that `T` and `U` are + convertible. + + .. exn:: Not convertible. + :undocumented: + + .. tacv:: change @term with @term’ + + This replaces the occurrences of :n:`@term` by :n:`@term’` in the current goal. + The term :n:`@term` and :n:`@term’` must be convertible. + + .. tacv:: change @term at {+ @natural} with @term’ + + This replaces the occurrences numbered :n:`{+ @natural}` of :n:`@term` by :n:`@term’` + in the current goal. The terms :n:`@term` and :n:`@term’` must be convertible. + + .. exn:: Too few occurrences. + :undocumented: + + .. tacv:: change @term {? {? at {+ @natural}} with @term} in @ident + + This applies the :tacn:`change` tactic not to the goal but to the hypothesis :n:`@ident`. + + .. tacv:: now_show @term + + This is a synonym of :n:`change @term`. It can be used to + make some proof steps explicit when refactoring a proof script + to make it readable. + + .. seealso:: :ref:`Performing computations <performingcomputations>` + +.. _performingcomputations: + +Performing computations +--------------------------- + +.. insertprodn red_expr pattern_occ + +.. prodn:: + red_expr ::= red + | hnf + | simpl {? @delta_flag } {? @ref_or_pattern_occ } + | cbv {? @strategy_flag } + | cbn {? @strategy_flag } + | lazy {? @strategy_flag } + | compute {? @delta_flag } + | vm_compute {? @ref_or_pattern_occ } + | native_compute {? @ref_or_pattern_occ } + | unfold {+, @unfold_occ } + | fold {+ @one_term } + | pattern {+, @pattern_occ } + | @ident + delta_flag ::= {? - } [ {+ @reference } ] + strategy_flag ::= {+ @red_flag } + | @delta_flag + red_flag ::= beta + | iota + | match + | fix + | cofix + | zeta + | delta {? @delta_flag } + ref_or_pattern_occ ::= @reference {? at @occs_nums } + | @one_term {? at @occs_nums } + occs_nums ::= {+ {| @natural | @ident } } + | - {| @natural | @ident } {* @int_or_var } + int_or_var ::= @integer + | @ident + unfold_occ ::= @reference {? at @occs_nums } + pattern_occ ::= @one_term {? at @occs_nums } + +This set of tactics implements different specialized usages of the +tactic :tacn:`change`. + +All conversion tactics (including :tacn:`change`) can be parameterized by the +parts of the goal where the conversion can occur. This is done using +*goal clauses* which consists in a list of hypotheses and, optionally, +of a reference to the conclusion of the goal. For defined hypothesis +it is possible to specify if the conversion should occur on the type +part, the body part or both (default). + +Goal clauses are written after a conversion tactic (tactics :tacn:`set`, +:tacn:`rewrite`, :tacn:`replace` and :tacn:`autorewrite` also use goal +clauses) and are introduced by the keyword `in`. If no goal clause is +provided, the default is to perform the conversion only in the +conclusion. + +The syntax and description of the various goal clauses is the +following: + ++ :n:`in {+ @ident} |-` only in hypotheses :n:`{+ @ident}` ++ :n:`in {+ @ident} |- *` in hypotheses :n:`{+ @ident}` and in the + conclusion ++ :n:`in * |-` in every hypothesis ++ :n:`in *` (equivalent to in :n:`* |- *`) everywhere ++ :n:`in (type of @ident) (value of @ident) ... |-` in type part of + :n:`@ident`, in the value part of :n:`@ident`, etc. + +For backward compatibility, the notation :n:`in {+ @ident}` performs +the conversion in hypotheses :n:`{+ @ident}`. + +.. tacn:: cbv {? @strategy_flag } + lazy {? @strategy_flag } + :name: cbv; lazy + + These parameterized reduction tactics apply to any goal and perform + the normalization of the goal according to the specified flags. In + correspondence with the kinds of reduction considered in |Coq| namely + :math:`\beta` (reduction of functional application), :math:`\delta` + (unfolding of transparent constants, see :ref:`vernac-controlling-the-reduction-strategies`), + :math:`\iota` (reduction of + pattern matching over a constructed term, and unfolding of :g:`fix` and + :g:`cofix` expressions) and :math:`\zeta` (contraction of local definitions), the + flags are either ``beta``, ``delta``, ``match``, ``fix``, ``cofix``, + ``iota`` or ``zeta``. The ``iota`` flag is a shorthand for ``match``, ``fix`` + and ``cofix``. The ``delta`` flag itself can be refined into + :n:`delta [ {+ @qualid} ]` or :n:`delta - [ {+ @qualid} ]`, restricting in the first + case the constants to unfold to the constants listed, and restricting in the + second case the constant to unfold to all but the ones explicitly mentioned. + Notice that the ``delta`` flag does not apply to variables bound by a let-in + construction inside the :n:`@term` itself (use here the ``zeta`` flag). In + any cases, opaque constants are not unfolded (see :ref:`vernac-controlling-the-reduction-strategies`). + + Normalization according to the flags is done by first evaluating the + head of the expression into a *weak-head* normal form, i.e. until the + evaluation is blocked by a variable (or an opaque constant, or an + axiom), as e.g. in :g:`x u1 ... un` , or :g:`match x with ... end`, or + :g:`(fix f x {struct x} := ...) x`, or is a constructed form (a + :math:`\lambda`-expression, a constructor, a cofixpoint, an inductive type, a + product type, a sort), or is a redex that the flags prevent to reduce. Once a + weak-head normal form is obtained, subterms are recursively reduced using the + same strategy. + + Reduction to weak-head normal form can be done using two strategies: + *lazy* (``lazy`` tactic), or *call-by-value* (``cbv`` tactic). The lazy + strategy is a call-by-need strategy, with sharing of reductions: the + arguments of a function call are weakly evaluated only when necessary, + and if an argument is used several times then it is weakly computed + only once. This reduction is efficient for reducing expressions with + dead code. For instance, the proofs of a proposition :g:`exists x. P(x)` + reduce to a pair of a witness :g:`t`, and a proof that :g:`t` satisfies the + predicate :g:`P`. Most of the time, :g:`t` may be computed without computing + the proof of :g:`P(t)`, thanks to the lazy strategy. + + The call-by-value strategy is the one used in ML languages: the + arguments of a function call are systematically weakly evaluated + first. Despite the lazy strategy always performs fewer reductions than + the call-by-value strategy, the latter is generally more efficient for + evaluating purely computational expressions (i.e. with little dead code). + +.. tacv:: compute + cbv + :name: compute; _ + + These are synonyms for ``cbv beta delta iota zeta``. + +.. tacv:: lazy + + This is a synonym for ``lazy beta delta iota zeta``. + +.. tacv:: compute [ {+ @qualid} ] + cbv [ {+ @qualid} ] + + These are synonyms of :n:`cbv beta delta {+ @qualid} iota zeta`. + +.. tacv:: compute - [ {+ @qualid} ] + cbv - [ {+ @qualid} ] + + These are synonyms of :n:`cbv beta delta -{+ @qualid} iota zeta`. + +.. tacv:: lazy [ {+ @qualid} ] + lazy - [ {+ @qualid} ] + + These are respectively synonyms of :n:`lazy beta delta {+ @qualid} iota zeta` + and :n:`lazy beta delta -{+ @qualid} iota zeta`. + +.. tacv:: vm_compute + :name: vm_compute + + This tactic evaluates the goal using the optimized call-by-value evaluation + bytecode-based virtual machine described in :cite:`CompiledStrongReduction`. + This algorithm is dramatically more efficient than the algorithm used for the + :tacn:`cbv` tactic, but it cannot be fine-tuned. It is especially interesting for + full evaluation of algebraic objects. This includes the case of + reflection-based tactics. + +.. tacv:: native_compute + :name: native_compute + + 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 :tacn:`vm_compute`. Note however that the + compilation cost is higher, so it is worth using only for intensive + computations. + + .. flag:: NativeCompute Timing + + This flag causes all calls to the native compiler to print + timing information for the conversion to native code, + compilation, execution, and reification phases of native + compilation. Timing is printed in units of seconds of + wall-clock time. + + .. flag:: NativeCompute Profiling + + On Linux, if you have the ``perf`` profiler installed, this flag makes + it possible to profile :tacn:`native_compute` evaluations. + + .. opt:: NativeCompute Profile Filename @string + :name: NativeCompute Profile Filename + + This option specifies the profile output; the default is + ``native_compute_profile.data``. The actual filename used + will contain extra characters to avoid overwriting an existing file; that + filename is reported to the user. + That means you can individually profile multiple uses of + :tacn:`native_compute` in a script. From the Linux command line, run ``perf report`` + on the profile file to see the results. Consult the ``perf`` documentation + for more details. + +.. flag:: Debug Cbv + + This flag makes :tacn:`cbv` (and its derivative :tacn:`compute`) print + information about the constants it encounters and the unfolding decisions it + makes. + +.. tacn:: red + :name: red + + This tactic applies to a goal that has the form:: + + forall (x:T1) ... (xk:Tk), T + + with :g:`T` :math:`\beta`:math:`\iota`:math:`\zeta`-reducing to :g:`c t`:sub:`1` :g:`... t`:sub:`n` and :g:`c` a + constant. If :g:`c` is transparent then it replaces :g:`c` with its + definition (say :g:`t`) and then reduces + :g:`(t t`:sub:`1` :g:`... t`:sub:`n` :g:`)` according to :math:`\beta`:math:`\iota`:math:`\zeta`-reduction rules. + +.. exn:: Not reducible. + :undocumented: + +.. exn:: No head constant to reduce. + :undocumented: + +.. tacn:: hnf + :name: hnf + + This tactic applies to any goal. It replaces the current goal with its + head normal form according to the :math:`\beta`:math:`\delta`:math:`\iota`:math:`\zeta`-reduction rules, i.e. it + reduces the head of the goal until it becomes a product or an + irreducible term. All inner :math:`\beta`:math:`\iota`-redexes are also reduced. + The behavior of both :tacn:`hnf` can be tuned using the :cmd:`Arguments` command. + + Example: The term :g:`fun n : nat => S n + S n` is not reduced by :n:`hnf`. + +.. note:: + The :math:`\delta` rule only applies to transparent constants (see :ref:`vernac-controlling-the-reduction-strategies` + on transparency and opacity). + +.. tacn:: cbn + simpl + :name: cbn; simpl + + These tactics apply to any goal. They try to reduce a term to + something still readable instead of fully normalizing it. They perform + a sort of strong normalization with two key differences: + + + They unfold a constant if and only if it leads to a :math:`\iota`-reduction, + i.e. reducing a match or unfolding a fixpoint. + + While reducing a constant unfolding to (co)fixpoints, the tactics + use the name of the constant the (co)fixpoint comes from instead of + the (co)fixpoint definition in recursive calls. + + The :tacn:`cbn` tactic is claimed to be a more principled, faster and more + predictable replacement for :tacn:`simpl`. + + The :tacn:`cbn` tactic accepts the same flags as :tacn:`cbv` and + :tacn:`lazy`. The behavior of both :tacn:`simpl` and :tacn:`cbn` + can be tuned using the :cmd:`Arguments` command. + + .. todo add "See <subsection about controlling the behavior of reduction strategies>" + to TBA section + + Notice that only transparent constants whose name can be reused in the + recursive calls are possibly unfolded by :tacn:`simpl`. For instance a + constant defined by :g:`plus' := plus` is possibly unfolded and reused in + the recursive calls, but a constant such as :g:`succ := plus (S O)` is + never unfolded. This is the main difference between :tacn:`simpl` and :tacn:`cbn`. + The tactic :tacn:`cbn` reduces whenever it will be able to reuse it or not: + :g:`succ t` is reduced to :g:`S t`. + +.. tacv:: cbn [ {+ @qualid} ] + cbn - [ {+ @qualid} ] + + These are respectively synonyms of :n:`cbn beta delta [ {+ @qualid} ] iota zeta` + and :n:`cbn beta delta - [ {+ @qualid} ] iota zeta` (see :tacn:`cbn`). + +.. tacv:: simpl @pattern + + This applies :tacn:`simpl` only to the subterms matching + :n:`@pattern` in the current goal. + +.. tacv:: simpl @pattern at {+ @natural} + + This applies :tacn:`simpl` only to the :n:`{+ @natural}` occurrences of the subterms + matching :n:`@pattern` in the current goal. + + .. exn:: Too few occurrences. + :undocumented: + +.. tacv:: simpl @qualid + simpl @string + + This applies :tacn:`simpl` only to the applicative subterms whose head occurrence + is the unfoldable constant :n:`@qualid` (the constant can be referred to by + its notation using :n:`@string` if such a notation exists). + +.. tacv:: simpl @qualid at {+ @natural} + simpl @string at {+ @natural} + + This applies :tacn:`simpl` only to the :n:`{+ @natural}` applicative subterms whose + head occurrence is :n:`@qualid` (or :n:`@string`). + +.. flag:: Debug RAKAM + + This flag makes :tacn:`cbn` print various debugging information. + ``RAKAM`` is the Refolding Algebraic Krivine Abstract Machine. + +.. tacn:: unfold @qualid + :name: unfold + + 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 + :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\iota\zeta`-normal form. + Use the general reduction tactics if you want to avoid this final + reduction, for instance :n:`cbv delta [@qualid]`. + + .. exn:: Cannot coerce @qualid to an evaluable reference. + + This error is frequent when trying to unfold something that has + defined as an inductive type (or constructor) and not as a + definition. + + .. example:: + + .. coqtop:: abort all fail + + Goal 0 <= 1. + unfold le. + + This error can also be raised if you are trying to unfold + something that has been marked as opaque. + + .. example:: + + .. coqtop:: abort all fail + + 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} + + Replaces :n:`{+, @qualid}` with their definitions and replaces + the current goal with its :math:`\beta`:math:`\iota` normal + form. + + .. tacv:: unfold {+, @qualid at @occurrences } + + 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 + + This tactic applies to any goal. The term :n:`@term` is reduced using the + :tacn:`red` tactic. Every occurrence of the resulting :n:`@term` in the goal is + then replaced by :n:`@term`. This tactic is particularly useful when a fixpoint + definition has been wrongfully unfolded, making the goal very hard to read. + On the other hand, when an unfolded function applied to its argument has been + reduced, the :tacn:`fold` tactic won't do anything. + + .. example:: + + .. coqtop:: all abort + + Goal ~0=0. + unfold not. + Fail progress fold not. + pattern (0 = 0). + fold not. + + .. tacv:: fold {+ @term} + + Equivalent to :n:`fold @term ; ... ; fold @term`. + +.. tacn:: pattern @term + :name: pattern + + This command applies to any goal. The argument :n:`@term` must be a free + subterm of the current goal. The command pattern performs :math:`\beta`-expansion + (the inverse of :math:`\beta`-reduction) of the current goal (say :g:`T`) by + + + replacing all occurrences of :n:`@term` in :g:`T` with a fresh variable + + abstracting this variable + + applying the abstracted goal to :n:`@term` + + For instance, if the current goal :g:`T` is expressible as + :math:`\varphi`:g:`(t)` where the notation captures all the instances of :g:`t` + in :math:`\varphi`:g:`(t)`, then :n:`pattern t` transforms it into + :g:`(fun x:A =>` :math:`\varphi`:g:`(x)) t`. This tactic can be used, for + instance, when the tactic ``apply`` fails on matching. + +.. tacv:: pattern @term at {+ @natural} + + Only the occurrences :n:`{+ @natural}` of :n:`@term` are considered for + :math:`\beta`-expansion. Occurrences are located from left to right. + +.. tacv:: pattern @term at - {+ @natural} + + All occurrences except the occurrences of indexes :n:`{+ @natural }` + of :n:`@term` are considered for :math:`\beta`-expansion. Occurrences are located from + left to right. + +.. tacv:: pattern {+, @term} + + Starting from a goal :math:`\varphi`:g:`(t`:sub:`1` :g:`... t`:sub:`m`:g:`)`, + the tactic :n:`pattern t`:sub:`1`:n:`, ..., t`:sub:`m` generates the + equivalent goal + :g:`(fun (x`:sub:`1`:g:`:A`:sub:`1`:g:`) ... (x`:sub:`m` :g:`:A`:sub:`m` :g:`) =>`:math:`\varphi`:g:`(x`:sub:`1` :g:`... x`:sub:`m` :g:`)) t`:sub:`1` :g:`... t`:sub:`m`. + If :g:`t`:sub:`i` occurs in one of the generated types :g:`A`:sub:`j` these + occurrences will also be considered and possibly abstracted. + +.. tacv:: pattern {+, @term at {+ @natural}} + + This behaves as above but processing only the occurrences :n:`{+ @natural}` of + :n:`@term` starting from :n:`@term`. + +.. tacv:: pattern {+, @term {? at {? -} {+, @natural}}} + + This is the most general syntax that combines the different variants. + +.. tacn:: with_strategy @strategy_level_or_var [ {+ @reference } ] @ltac_expr3 + :name: with_strategy + + Executes :token:`ltac_expr3`, applying the alternate unfolding + behavior that the :cmd:`Strategy` command controls, but only for + :token:`ltac_expr3`. This can be useful for guarding calls to + reduction in tactic automation to ensure that certain constants are + never unfolded by tactics like :tacn:`simpl` and :tacn:`cbn` or to + ensure that unfolding does not fail. + + .. example:: + + .. coqtop:: all reset abort + + Opaque id. + Goal id 10 = 10. + Fail unfold id. + with_strategy transparent [id] unfold id. + + .. warning:: + + Use this tactic with care, as effects do not persist past the + end of the proof script. Notably, this fine-tuning of the + conversion strategy is not in effect during :cmd:`Qed` nor + :cmd:`Defined`, so this tactic is most useful either in + combination with :tacn:`abstract`, which will check the proof + early while the fine-tuning is still in effect, or to guard + calls to conversion in tactic automation to ensure that, e.g., + :tacn:`unfold` does not fail just because the user made a + constant :cmd:`Opaque`. + + This can be illustrated with the following example involving the + factorial function. + + .. coqtop:: in reset + + Fixpoint fact (n : nat) : nat := + match n with + | 0 => 1 + | S n' => n * fact n' + end. + + Suppose now that, for whatever reason, we want in general to + unfold the :g:`id` function very late during conversion: + + .. coqtop:: in + + Strategy 1000 [id]. + + If we try to prove :g:`id (fact n) = fact n` by + :tacn:`reflexivity`, it will now take time proportional to + :math:`n!`, because |Coq| will keep unfolding :g:`fact` and + :g:`*` and :g:`+` before it unfolds :g:`id`, resulting in a full + computation of :g:`fact n` (in unary, because we are using + :g:`nat`), which takes time :math:`n!`. We can see this cross + the relevant threshold at around :math:`n = 9`: + + .. coqtop:: all abort + + Goal True. + Time assert (id (fact 8) = fact 8) by reflexivity. + Time assert (id (fact 9) = fact 9) by reflexivity. + + Note that behavior will be the same if you mark :g:`id` as + :g:`Opaque` because while most reduction tactics refuse to + unfold :g:`Opaque` constants, conversion treats :g:`Opaque` as + merely a hint to unfold this constant last. + + We can get around this issue by using :tacn:`with_strategy`: + + .. coqtop:: all + + Goal True. + Fail Timeout 1 assert (id (fact 100) = fact 100) by reflexivity. + Time assert (id (fact 100) = fact 100) by with_strategy -1 [id] reflexivity. + + However, when we go to close the proof, we will run into + trouble, because the reduction strategy changes are local to the + tactic passed to :tacn:`with_strategy`. + + .. coqtop:: all abort fail + + exact I. + Timeout 1 Defined. + + We can fix this issue by using :tacn:`abstract`: + + .. coqtop:: all + + Goal True. + Time assert (id (fact 100) = fact 100) by with_strategy -1 [id] abstract reflexivity. + exact I. + Time Defined. + + On small examples this sort of behavior doesn't matter, but + because |Coq| is a super-linear performance domain in so many + places, unless great care is taken, tactic automation using + :tacn:`with_strategy` may not be robustly performant when + scaling the size of the input. + + .. warning:: + + In much the same way this tactic does not play well with + :cmd:`Qed` and :cmd:`Defined` without using :tacn:`abstract` as + an intermediary, this tactic does not play well with ``coqchk``, + even when used with :tacn:`abstract`, due to the inability of + tactics to persist information about conversion hints in the + proof term. See `#12200 + <https://github.com/coq/coq/issues/12200>`_ for more details. + +Conversion tactics applied to hypotheses +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. tacn:: @tactic in {+, @ident} + + Applies :token:`tactic` (any of the conversion tactics listed in this + section) to the hypotheses :n:`{+ @ident}`. + + 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)`. |