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

=========================
Reasoning with equalities
=========================

There are multiple notions of :gdef:`equality` in Coq:

- :gdef:`Leibniz equality` is the standard
  way to define equality in Coq and the Calculus of Inductive Constructions,
  which is in terms of a binary relation, i.e. a binary function that returns
  a `Prop`.  The standard library
  defines `eq` similar to this:

   .. coqdoc::

      Inductive eq {A : Type} (x : A) : A -> Prop := eq_refl : eq x x.

  The notation `x = y` represents the term `eq x y`.  The notation `x = y :> A`
  gives the type of x and y explicitly.

- :gdef:`Setoid equality <setoid equality>` defines equality in terms of an equivalence
  relation.  A :gdef:`setoid` is a set that is equipped with an equivalence relation
  (see https://en.wikipedia.org/wiki/Setoid).  These are needed to form a :gdef:`quotient set`
  or :gdef:`quotient`
  (see https://en.wikipedia.org/wiki/Equivalence_Class).  In Coq, users generally work
  with setoids rather than constructing quotients, for which there is no specific support.

- :gdef:`Definitional equality <definitional equality>` is equality based on the
  :ref:`conversion rules <Conversion-rules>`, which Coq can determine automatically.
  When two terms are definitionally equal, Coq knows it can
  replace one with the other, such as with :tacn:`change` `X with Y`, among many
  other advantages.  ":term:`Convertible <convertible>`" is another way of saying that
  two terms are definitionally equal.

.. _rewritingexpressions:

Rewriting with Leibniz and setoid equality
------------------------------------------

.. tacn:: rewrite {+, @oriented_rewriter } {? @occurrences } {? by @ltac_expr3 }

   .. insertprodn oriented_rewriter one_term_with_bindings

   .. prodn::
      oriented_rewriter ::= {? {| -> | <- } } {? @natural } {? {| ? | ! } } @one_term_with_bindings
      one_term_with_bindings ::= {? > } @one_term {? with @bindings }

   Replaces subterms with other subterms that have been proven to be equal.
   The type of :n:`@one_term` must have the form:

      :n:`{? forall {+ (x__i: A__i) } , } EQ @term__1 @term__2`

   .. todo :term:`Leibniz equality` does not work with Sphinx 2.3.1. It does with Sphinx 3.0.3.

   where :g:`EQ` is the Leibniz equality `eq` or a registered :term:`setoid equality`.
   Note that :n:`eq @term__1 @term__2` is typically written with the infix notation
   :n:`@term__1 = @term__2`.  You must `Require Setoid` to use the tactic
   with a setoid equality or with :ref:`setoid rewriting <generalizedrewriting>`.
   In the general form, any :n:`@binder` may be used, not just :n:`(x__i: A__i)`.

   .. todo doublecheck the @binder comment is correct.

   :n:`rewrite @one_term` finds subterms matching :n:`@term__1` in the goal,
   and replaces them with :n:`@term__2` (or the reverse if `<-` is given).
   Some of the variables :g:`x`\ :sub:`i` are solved by unification,
   and some of the types :n:`A__1, ..., A__n` may become new
   subgoals.  :tacn:`rewrite` won't find occurrences inside `forall` that refer
   to variables bound by the `forall`; use the more advanced :tacn:`setoid_rewrite`
   if you want to find such occurrences.

   :n:`{+, @oriented_rewriter }`
     The :n:`@oriented_rewriter`\s are applied sequentially
     to the first goal generated by the previous :n:`@oriented_rewriter`.  If any of them fail,
     the tactic fails.

   :n:`{? {| -> | <- } }`
     For `->` (the default), :n:`@term__1` is rewritten
     into :n:`@term__2`.  For `<-`, :n:`@term__2` is rewritten into :n:`@term__1`.

   :n:`{? @natural } {? {| ? | ! } }`
     :n:`@natural` is the number of rewrites to perform.  If `?` is given, :n:`@natural`
     is the maximum number of rewrites to perform; otherwise :n:`@natural` is the exact number
     of rewrites to perform.

     `?` (without :n:`@natural`) performs the rewrite as many times as possible
     (possibly zero times).
     This form never fails.  `!` (without :n:`@natural`) performs the rewrite as many
     times as possible
     and at least once.  The tactic fails if the requested number of rewrites can't
     be performed.  :n:`@natural !` is equivalent to :n:`@natural`.

   :n:`@occurrences`
     If :n:`@occurrences` specifies multiple occurrences, the tactic succeeds if
     any of them can be rewritten.  If not specified, only the first occurrence
     in the conclusion is replaced.

     .. note::

        If :n:`at @occs_nums` is specified, rewriting is always done
        with :ref:`setoid rewriting <generalizedrewriting>`, even for
        Leibniz equality, which means that you must `Require
        Setoid` to use that form.  However, note that :tacn:`rewrite`
        (even when using setoid rewriting) and :tacn:`setoid_rewrite`
        don't behave identically (as is noted above and below).

   :n:`by @ltac_expr3`
     If specified, is used to resolve all side conditions generated by the tactic.

   .. note::

      For each selected hypothesis and/or the conclusion,
      :tacn:`rewrite` finds the first matching subterm in
      depth-first search order. Only subterms identical to
      that first matched subterm are rewritten.  If the `at` clause is specified,
      only these subterms are considered when counting occurrences.
      To select a different set of matching subterms, you can
      specify how some or all of the free variables are bound by
      using a `with` clause (see :n:`@one_term_with_bindings`).

      For instance, if we want to rewrite the right-hand side in the
      following goal, this will not work:

      .. coqtop:: none

         Require Import Arith.

      .. coqtop:: out

         Lemma example x y : x + y = y + x.

      .. coqtop:: all fail

         rewrite Nat.add_comm at 2.

      One can explicitly specify how some variables are bound to match
      a different subterm:

      .. coqtop:: all abort

         rewrite Nat.add_comm with (m := x).

      Note that the more advanced :tacn:`setoid_rewrite` tactic
      behaves differently, and thus the number of occurrences
      available to rewrite may differ between the two tactics.

   .. exn:: Tactic failure: Setoid library not loaded.
      :undocumented:

      .. todo You can use Typeclasses Debug to tell whether rewrite used
         setoid rewriting.  Example here: https://github.com/coq/coq/pull/13470#discussion_r539230973

   .. exn:: Cannot find a relation to rewrite.
      :undocumented:

   .. exn:: Tactic generated a subgoal identical to the original goal.
      :undocumented:

   .. exn:: Found no subterm matching @term in @ident.
            Found no subterm matching @term in the current goal.

      This happens if :n:`@term` does not occur in, respectively, the named hypothesis or the goal.

   .. tacn:: erewrite {+, @oriented_rewriter } {? @occurrences } {? by @ltac_expr3 }

      Works like :tacn:`rewrite`, but turns
      unresolved bindings, if any, into existential variables instead of
      failing. It has the same parameters as :tacn:`rewrite`.

   .. 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:: rewrite * {? {| -> | <- } } @one_term {? in @ident } {? at @rewrite_occs } {? by @ltac_expr3 }
          rewrite * {? {| -> | <- } } @one_term at @rewrite_occs in @ident {? by @ltac_expr3 }
   :name: rewrite *; _
   :undocumented:

.. tacn:: rewrite_db @ident {? in @ident }
   :undocumented:

.. tacn:: replace @one_term__from with @one_term__to {? @occurrences } {? by @ltac_expr3 }
          replace {? {| -> | <- } } @one_term__from {? @occurrences }
   :name: replace; _

   The first form replaces all free occurrences of :n:`@one_term__from`
   in the current goal with :n:`@one_term__to` and generates an equality
   :n:`@one_term__to = @one_term__from`
   as a subgoal. (Note the generated equality is reversed with respect
   to the order of the two terms in the tactic syntax; see
   issue `#13480 <https://github.com/coq/coq/issues/13480>`_.)
   This equality is automatically solved if it occurs among
   the hypotheses, or if its symmetric form occurs.

   The second form, with `->` or no arrow, replaces :n:`@one_term__from`
   with :n:`@term__to` using
   the first hypothesis whose type has the form :n:`@one_term__from = @term__to`.
   If `<-` is given, the tactic uses the first hypothesis with the reverse form,
   i.e. :n:`@term__to = @one_term__from`.

   :n:`@occurrences`
     The `type of` and `value of` forms are not supported.
     Note you must `Require Setoid` to use the `at` clause in :n:`@occurrences`.

   :n:`by @ltac_expr3`
     Applies the :n:`@ltac_expr3` to solve the generated equality.

   .. exn:: Terms do not have convertible types.
      :undocumented:

   .. tacn:: cutrewrite {? {| -> | <- } } @one_term {? in @ident }

      Where :n:`@one_term` is an equality.

      .. deprecated:: 8.5

         Use :tacn:`replace` instead.

.. tacn:: substitute {? {| -> | <- } } @one_term {? with @bindings }
   :undocumented:

.. tacn:: subst {* @ident }

   For each :n:`@ident`, in order, for which there is a hypothesis in the form
   :n:`@ident = @term` or :n:`@term = @ident`, replaces :n:`@ident` with :n:`@term`
   everywhere in the hypotheses and the conclusion and clears :n:`@ident` and the hypothesis
   from the context.  If there are multiple hypotheses that match the :n:`@ident`,
   the first one is used.  If no :n:`@ident` is given, replacement is done for all
   hypotheses in the appropriate form in top to bottom order.

   If :n:`@ident` is a local definition of the form :n:`@ident := @term`, it is also
   unfolded and cleared.

   If :n:`@ident` is a section variable it must have no
   indirect occurrences in the goal, i.e. no global declarations
   implicitly depending on the section variable may be present in the
   goal.

   .. note::
      If the hypothesis is itself dependent in the goal, it is replaced by the proof of
      reflexivity of equality.

   .. 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__1 = @ident__2`
        and :n:`@ident__1 = t`, or :n:`t′ = @ident__1` with `t′` not
        a variable, and no other hypotheses of the form :n:`@ident__2 = u`
        or :n:`u = @ident__2`; without the flag, a second call to
        subst would be necessary to replace :n:`@ident__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__1 = f @ident__2`
        and :n:`@ident__2 = g @ident__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` from being
      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.

   .. exn:: Cannot find any non-recursive equality over @ident.
      :undocumented:

   .. exn:: Section variable @ident occurs implicitly in global declaration @qualid present in hypothesis @ident.
            Section variable @ident occurs implicitly in global declaration @qualid present in the conclusion.

      Raised when the variable is a section variable with indirect
      dependencies in the goal.
      If :n:`@ident` is a section variable, it must not have any
      indirect occurrences in the goal, i.e. no global declarations
      implicitly depending on the section variable may be present in the
      goal.

.. tacn:: simple subst
   :undocumented:

.. tacn:: stepl @one_term {? by @ltac_expr }

   For chaining rewriting steps. It assumes a goal in the
   form :n:`R @term__1 @term__2` 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 @one_term`
   then replaces the goal by :n:`R @one_term @term__2` and adds a new goal stating
   :n:`eq @one_term @term__1`.

   If :n:`@ltac_expr` is specified, it is applied to the side condition.

   .. cmd:: Declare Left Step @one_term

      Adds :n:`@one_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`).

   .. tacn:: stepr @one_term {? by @ltac_expr }

      This behaves like :tacn:`stepl` but on the right hand side of the binary
      relation. Lemmas are expected to be in the form
      :g:`forall x y z, R x y -> eq y z -> R x z`.

   .. cmd:: Declare Right Step @one_term

       Adds :n:`@term` to the database used by :tacn:`stepr`.

Rewriting with definitional equality
------------------------------------

.. tacn:: change {? @one_term__from {? at @occs_nums } with } @one_term__to {? @occurrences }

   Replaces terms with other :term:`convertible` terms.
   If :n:`@one_term__from` is not specified, then :n:`@one_term__from` replaces the conclusion and/or
   the specified hypotheses.  If :n:`@one_term__from` is specified, the tactic replaces occurrences
   of :n:`@one_term__to` within the conclusion and/or the specified hypotheses.

   :n:`{? @one_term__from {? at @occs_nums } with }`
     Replaces the occurrences of :n:`@one_term__from` specified by :n:`@occs_nums`
     with :n:`@one_term__to`, provided that the two :n:`@one_term`\s are
     convertible.  :n:`@one_term__from` may contain pattern variables such as `?x`,
     whose value which will substituted for `x` in :n:`@one_term__to`, such as in
     `change (f ?x ?y) with (g (x, y))` or `change (fun x => ?f x) with f`.

     The `at ... with ...` form is deprecated in 8.14; use `with ... at ...` instead.
     For `at ... with ... in H |-`, use `with ... in H at ... |-`.

   :n:`@occurrences`
     If `with` is not specified, :n:`@occurrences` must only specify
     entire hypotheses and/or the goal; it must not include any
     :n:`at @occs_nums` clauses.

   .. exn:: Not convertible.
      :undocumented:

   .. exn:: Found an "at" clause without "with" clause
      :undocumented:

   .. tacn:: now_show @one_term

      A synonym for :n:`change @one_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>`

.. tacn:: change_no_check {? @one_term__from {? at @occs_nums } with } @one_term__to {? @occurrences }

   For advanced usage. Similar to :tacn:`change`, but as an optimization,
   it skips checking that :n:`@one_term__to` is convertible with the goal or
   :n:`@one_term__from`.

   Recall that the Coq kernel typechecks proofs again when they are concluded to
   ensure correctness. Hence, using :tacn:`change` checks convertibility twice
   overall, while :tacn:`change_no_check` can produce ill-typed terms,
   but checks convertibility only once.
   Hence, :tacn:`change_no_check` can be useful to speed up certain proof
   scripts, especially if one knows by construction that the argument is
   indeed convertible to the goal.

   In the following example, :tacn:`change_no_check` replaces :g:`False` with
   :g:`True`, but :cmd:`Qed` then rejects the proof, ensuring consistency.

   .. example::

      .. coqtop:: all abort fail

         Goal False.
           change_no_check True.
           exact I.
         Qed.

   .. example::

      .. coqtop:: all abort fail

         Goal True -> False.
           intro H.
           change_no_check False in H.
           exact H.
         Qed.

.. _performingcomputations:

Performing computations
---------------------------

.. insertprodn red_expr pattern_occs

.. prodn::
   red_expr ::= red
   | hnf
   | simpl {? @delta_flag } {? {| @reference_occs | @pattern_occs } }
   | cbv {? @strategy_flag }
   | cbn {? @strategy_flag }
   | lazy {? @strategy_flag }
   | compute {? @delta_flag }
   | vm_compute {? {| @reference_occs | @pattern_occs } }
   | native_compute {? {| @reference_occs | @pattern_occs } }
   | unfold {+, @reference_occs }
   | fold {+ @one_term }
   | pattern {+, @pattern_occs }
   | @ident
   delta_flag ::= {? - } [ {+ @reference } ]
   strategy_flag ::= {+ @red_flag }
   | @delta_flag
   red_flag ::= beta
   | iota
   | match
   | fix
   | cofix
   | zeta
   | delta {? @delta_flag }
   reference_occs ::= @reference {? at @occs_nums }
   pattern_occs ::= @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.

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. Depending on the configuration, this tactic can either default to
   :tacn:`vm_compute`, recompile dependencies or fail due to some missing
   precompiled dependencies,
   see :ref:`the native-compiler option <native-compiler-options>` for details.

   .. 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.

   :opt:`Debug` ``"Cbv"`` 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:: 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 was intended 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`).

:opt:`Debug` ``"RAKAM"`` 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
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

   The form :n:`@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)`.