path: root/doc/sphinx/proofs/writing-proofs/rewriting.rst

=================================
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 @goal_occurrences

      In the presence of :n:`with`, this applies :tacn:`change` to the
      occurrences specified by :n:`@goal_occurrences`. In the
      absence of :n:`with`, :n:`@goal_occurrences` is expected to
      only list hypotheses (and optionally the conclusion) without
      specifying occurrences (i.e. no :n:`at` clause).

   .. 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 ::= @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)`.