\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)} \newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\Type}{\textsf{Type}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \end{split}\]

Reasoning with equalities¶

There are multiple notions of equality in Coq:

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:

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.
Setoid equality defines equality in terms of an equivalence relation. A setoid is a set that is equipped with an equivalence relation (see https://en.wikipedia.org/wiki/Setoid). These are needed to form a quotient set or 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.
Definitional equality is equality based on the 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 change X with Y, among many other advantages. "Convertible" is another way of saying that two terms are definitionally equal.

Rewriting with Leibniz and setoid equality¶

Tactic rewrite oriented_rewriter+, occurrences? by ltac_expr3?¶

oriented_rewriter::=-><-? natural? ?!? one_term_with_bindingsone_term_with_bindings::=>? one_term with bindings?

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

forall (x_i: A_i)+ ,? EQ term₁ term₂

where EQ is the Leibniz equality eq or a registered setoid equality. Note that eq term₁ term₂ is typically written with the infix notation term₁ = term₂. You must Require Setoid to use the tactic with a setoid equality or with setoid rewriting. In the general form, any binder may be used, not just (x_i: A_i).

rewrite one_term finds subterms matching term₁ in the goal, and replaces them with term₂ (or the reverse if <- is given). Some of the variables x_i are solved by unification, and some of the types A₁, ..., A_n may become new subgoals. rewrite won't find occurrences inside forall that refer to variables bound by the forall; use the more advanced setoid_rewrite if you want to find such occurrences.

oriented_rewriter+,

The oriented_rewriters are applied sequentially to the first goal generated by the previous oriented_rewriter. If any of them fail, the tactic fails.

-><-?

For -> (the default), term₁ is rewritten into term₂. For <-, term₂ is rewritten into term₁.

natural? ?!?

natural is the number of rewrites to perform. If ? is given, natural is the maximum number of rewrites to perform; otherwise natural is the exact number of rewrites to perform.

? (without natural) performs the rewrite as many times as possible (possibly zero times). This form never fails. ! (without 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. natural ! is equivalent to natural.

occurrences

If 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 at occs_nums is specified, rewriting is always done with setoid rewriting, even for Leibniz equality, which means that you must Require Setoid to use that form. However, note that rewrite (even when using setoid rewriting) and setoid_rewrite don't behave identically (as is noted above and below).

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, 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 one_term_with_bindings).

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

Require Import Arith.: [Loading ML file ring_plugin.cmxs ... done]

Lemma example x y : x + y = y + x.: 1 subgoal x, y : nat ============================ x + y = y + x

rewrite Nat.add_comm at 2.: Toplevel input, characters 0-25: > rewrite Nat.add_comm at 2. > ^^^^^^^^^^^^^^^^^^^^^^^^^ Error: Tactic failure: Nothing to rewrite.

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

rewrite Nat.add_comm with (m := x).: 1 subgoal x, y : nat ============================ x + y = x + y

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

Error Tactic failure: Setoid library not loaded.¶

Error Cannot find a relation to rewrite.¶

Error Tactic generated a subgoal identical to the original goal.¶

Error Found no subterm matching term in ident.¶
Error Found no subterm matching term in the current goal.¶: This happens if term does not occur in, respectively, the named hypothesis or the goal.

Tactic erewrite oriented_rewriter+, occurrences? by ltac_expr3?¶: Works like rewrite, but turns unresolved bindings, if any, into existential variables instead of failing. It has the same parameters as rewrite.

Flag Keyed Unification¶: Makes higher-order unification used by 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.

Tactic rewrite * -><-? one_term in ident? at rewrite_occs? by ltac_expr3?¶
Tactic rewrite * -><-? one_term at rewrite_occs in ident by ltac_expr3?¶

Tactic rewrite_db ident in ident?¶

Tactic replace one_term_from with one_term_to occurrences? by ltac_expr3?¶

Tactic replace -><-? one_term_from occurrences?¶

The first form replaces all free occurrences of one_term_from in the current goal with one_term_to and generates an equality 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.) 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 one_term_from with term_to using the first hypothesis whose type has the form one_term_from = term_to. If <- is given, the tactic uses the first hypothesis with the reverse form, i.e. term_to = one_term_from.

occurrences: The type of and value of forms are not supported. Note you must Require Setoid to use the at clause in occurrences.
by ltac_expr3: Applies the ltac_expr3 to solve the generated equality.

Error Terms do not have convertible types.¶

Tactic cutrewrite -><-? one_term in ident?¶: Where one_term is an equality.

Deprecated since version 8.5: Use replace instead.

Tactic substitute -><-? one_term with bindings?¶

Tactic subst ident*¶

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

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

If 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 subst. When it is activated (it is by default), subst also deals with the following corner cases:

A context with ordered hypotheses ident₁ = ident₂ and ident₁ = t, or t′ = ident₁ with t′ not a variable, and no other hypotheses of the form ident₂ = u or u = ident₂; without the flag, a second call to subst would be necessary to replace ident₂ by t or t′ respectively.
The presence of a recursive equation which without the flag would be a cause of failure of subst.
A context with cyclic dependencies as with hypotheses ident₁ = f ident₂ and ident₂ = g ident₁ which without the flag would be a cause of failure of subst.

Additionally, it prevents a local definition such as ident := t from being unfolded which otherwise it would exceptionally unfold in configurations containing hypotheses of the form ident = u, or u′ = ident with u′ not a variable. Finally, it preserves the initial order of hypotheses, which without the flag it may break.

Error Cannot find any non-recursive equality over ident.¶

Error Section variable ident occurs implicitly in global declaration qualid present in hypothesis ident.¶
Error 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 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.

Tactic simple subst¶

Tactic stepl one_term by ltac_expr?¶

For chaining rewriting steps. It assumes a goal in the form R term₁ term₂ where R is a binary relation and relies on a database of lemmas of the form forall x y z, R x y -> eq x z -> R z y where eq is typically a setoid equality. The application of stepl one_term then replaces the goal by R one_term term₂ and adds a new goal stating eq one_term term₁.

If ltac_expr is specified, it is applied to the side condition.

Command Declare Left Step one_term¶: Adds one_term to the database used by stepl.

This tactic is especially useful for parametric setoids which are not accepted as regular setoids for rewrite and setoid_replace (see Generalized rewriting).

Tactic stepr one_term by ltac_expr?¶: This behaves like stepl but on the right hand side of the binary relation. Lemmas are expected to be in the form forall x y z, R x y -> eq y z -> R x z.

Command Declare Right Step one_term¶: Adds term to the database used by stepr.

Rewriting with definitional equality¶

Tactic change one_term_from at occs_nums? with? one_term_to occurrences?¶

Replaces terms with other convertible terms. If one_term_from is not specified, then one_term_from replaces the conclusion and/or the specified hypotheses. If one_term_from is specified, the tactic replaces occurrences of one_term_to within the conclusion and/or the specified hypotheses.

one_term_from at occs_nums? with?: Replaces the occurrences of one_term_from specified by occs_nums with one_term_to, provided that the two one_terms are convertible. one_term_from may contain pattern variables such as ?x, whose value which will substituted for x in one_term_to, such as in change (f ?x ?y) with (g (x, y)) or change (fun x => ?f x) with f.
occurrences: If with is not specified, occurrences must only specify entire hypotheses and/or the goal; it must not include any at occs_nums clauses.

Error Not convertible.¶

Error Found an "at" clause without "with" clause¶

Tactic now_show one_term¶: A synonym for change one_term. It can be used to make some proof steps explicit when refactoring a proof script to make it readable.

Performing computations¶

This set of tactics implements different specialized usages of the tactic change.

All conversion tactics (including 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 set, rewrite, replace and 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 in ident+ performs the conversion in hypotheses ident+.

Tactic cbv strategy_flag?¶

Tactic lazy strategy_flag?¶

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 $\beta$ (reduction of functional application), $\delta$ (unfolding of transparent constants, see Controlling the reduction strategies and the conversion algorithm), $\iota$ (reduction of pattern matching over a constructed term, and unfolding of fix and cofix expressions) and $\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 delta [ qualid+ ] or 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 term itself (use here the zeta flag). In any cases, opaque constants are not unfolded (see Controlling the reduction strategies and the conversion algorithm).

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 x u1 ... un , or match x with ... end, or (fix f x {struct x} := ...) x, or is a constructed form (a $\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 exists x. P(x) reduce to a pair of a witness t, and a proof that t satisfies the predicate P. Most of the time, t may be computed without computing the proof of 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).

Variant compute¶
Variant cbv¶: These are synonyms for cbv beta delta iota zeta.

Variant lazy: This is a synonym for lazy beta delta iota zeta.

Variant compute [ qualid+ ]
Variant cbv [ qualid+ ]: These are synonyms of cbv beta delta qualid+ iota zeta.

Variant compute - [ qualid+ ]
Variant cbv - [ qualid+ ]: These are synonyms of cbv beta delta -qualid+ iota zeta.

Variant lazy [ qualid+ ]
Variant lazy - [ qualid+ ]: These are respectively synonyms of lazy beta delta qualid+ iota zeta and lazy beta delta -qualid+ iota zeta.

Variant vm_compute¶: This tactic evaluates the goal using the optimized call-by-value evaluation bytecode-based virtual machine described in [GregoireL02]. This algorithm is dramatically more efficient than the algorithm used for the 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.

Variant native_compute¶

This tactic evaluates the goal by compilation to OCaml as described in [BDenesGregoire11]. If Coq is running in native code, it can be typically two to five times faster than vm_compute. Note however that the compilation cost is higher, so it is worth using only for intensive computations. Depending on the configuration, this tactic can either default to vm_compute, recompile dependencies or fail due to some missing precompiled dependencies, see the native-compiler option 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 native_compute evaluations.

Option NativeCompute Profile Filename string¶: 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 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 cbv (and its derivative compute) print information about the constants it encounters and the unfolding decisions it makes.

Tactic red¶

This tactic applies to a goal that has the form:

forall (x:T1) ... (xk:Tk), T

with T $\beta$$\iota$$\zeta$-reducing to c t₁ ... t_n and c a constant. If c is transparent then it replaces c with its definition (say t) and then reduces (t t₁ ... t_n ) according to $\beta$$\iota$$\zeta$-reduction rules.

Error No head constant to reduce.¶

Tactic hnf¶

This tactic applies to any goal. It replaces the current goal with its head normal form according to the $\beta$$\delta$$\iota$$\zeta$-reduction rules, i.e. it reduces the head of the goal until it becomes a product or an irreducible term. All inner $\beta$$\iota$-redexes are also reduced. The behavior of both hnf can be tuned using the Arguments command.

Example: The term fun n : nat => S n + S n is not reduced by hnf.

Note

The $\delta$ rule only applies to transparent constants (see Controlling the reduction strategies and the conversion algorithm on transparency and opacity).

Tactic cbn¶

Tactic 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 $\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 cbn tactic was intended to be a more principled, faster and more predictable replacement for simpl.

The cbn tactic accepts the same flags as cbv and lazy. The behavior of both simpl and cbn can be tuned using the Arguments command.

Notice that only transparent constants whose name can be reused in the recursive calls are possibly unfolded by simpl. For instance a constant defined by plus' := plus is possibly unfolded and reused in the recursive calls, but a constant such as succ := plus (S O) is never unfolded. This is the main difference between simpl and cbn. The tactic cbn reduces whenever it will be able to reuse it or not: succ t is reduced to S t.

Variant cbn [ qualid+ ]
Variant cbn - [ qualid+ ]: These are respectively synonyms of cbn beta delta [ qualid+ ] iota zeta and cbn beta delta - [ qualid+ ] iota zeta (see cbn).

Variant simpl pattern: This applies simpl only to the subterms matching pattern in the current goal.

Variant simpl pattern at natural+

This applies simpl only to the natural+ occurrences of the subterms matching pattern in the current goal.

Error Too few occurrences.¶

Variant simpl qualid
Variant simpl string: This applies simpl only to the applicative subterms whose head occurrence is the unfoldable constant qualid (the constant can be referred to by its notation using string if such a notation exists).

Variant simpl qualid at natural+
Variant simpl string at natural+: This applies simpl only to the natural+ applicative subterms whose head occurrence is qualid (or string).

Flag Debug RAKAM¶: This flag makes cbn print various debugging information. RAKAM is the Refolding Algebraic Krivine Abstract Machine.

Tactic unfold qualid¶

This tactic applies to any goal. The argument qualid must denote a defined transparent constant or local definition (see Top-level definitions and Controlling the reduction strategies and the conversion algorithm). The tactic unfold applies the $\delta$ rule to each occurrence of the constant to which qualid refers in the current goal and then replaces it with its $\beta\iota\zeta$-normal form. Use the general reduction tactics if you want to avoid this final reduction, for instance cbv delta [qualid].

Error 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

Goal 0 <= 1.: 1 subgoal ============================ 0 <= 1
unfold le.: Toplevel input, characters 7-9: > unfold le. > ^^ Error: Cannot turn inductive le into an evaluable reference.

This error can also be raised if you are trying to unfold something that has been marked as opaque.

Example

Opaque Nat.add.
Goal 1 + 0 = 1.: 1 subgoal ============================ 1 + 0 = 1
unfold Nat.add.: Toplevel input, characters 0-14: > unfold Nat.add. > ^^^^^^^^^^^^^^ Error: Nat.add is opaque.

Variant unfold qualid in goal_occurrences: Replaces qualid in hypothesis (or hypotheses) designated by goal_occurrences with its definition and replaces the hypothesis with its $\beta$$\iota$ normal form.

Variant unfold qualid+,: Replaces qualid+, with their definitions and replaces the current goal with its $\beta$$\iota$ normal form.

Variant unfold qualid at occurrences+,

The list occurrences specify the occurrences of qualid to be unfolded. Occurrences are located from left to right.

Error Bad occurrence number of qualid.¶

Error qualid does not occur.¶

Variant unfold string: If 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.

Variant unfold string%ident: This is variant of unfold string where string gets its interpretation from the scope bound to the delimiting key ident instead of its default interpretation (see Local interpretation rules for notations).

Variant unfold qualidstring%ident? at occurrences?+, in goal_occurrences?: This is the most general form.

Tactic fold term¶

This tactic applies to any goal. The term term is reduced using the red tactic. Every occurrence of the resulting term in the goal is then replaced by 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 fold tactic won't do anything.

Example

Goal ~0=0.: 1 subgoal ============================ 0 <> 0
unfold not.: 1 subgoal ============================ 0 = 0 -> False
Fail progress fold not.: The command has indeed failed with message: Failed to progress.
pattern (0 = 0).: 1 subgoal ============================ (fun P : Prop => P -> False) (0 = 0)
fold not.: 1 subgoal ============================ 0 <> 0

Variant fold term+: Equivalent to fold term ; ... ; fold term.

Tactic pattern term¶

This command applies to any goal. The argument term must be a free subterm of the current goal. The command pattern performs $\beta$-expansion (the inverse of $\beta$-reduction) of the current goal (say T) by

replacing all occurrences of term in T with a fresh variable
abstracting this variable
applying the abstracted goal to term

For instance, if the current goal T is expressible as $\varphi$(t) where the notation captures all the instances of t in $\varphi$(t), then pattern t transforms it into (fun x:A => $\varphi$(x)) t. This tactic can be used, for instance, when the tactic apply fails on matching.

Variant pattern term at natural+: Only the occurrences natural+ of term are considered for $\beta$-expansion. Occurrences are located from left to right.

Variant pattern term at - natural+: All occurrences except the occurrences of indexes natural+ of term are considered for $\beta$-expansion. Occurrences are located from left to right.

Variant pattern term+,: Starting from a goal $\varphi$(t₁ ... t_m), the tactic pattern t₁, ..., t_m generates the equivalent goal (fun (x₁:A₁) ... (x_m :A_m ) =>$\varphi$(x₁ ... x_m )) t₁ ... t_m. If t_i occurs in one of the generated types A_j these occurrences will also be considered and possibly abstracted.

Variant pattern term at natural++,: This behaves as above but processing only the occurrences natural+ of term starting from term.

Variant pattern term at -? natural+,?+,: This is the most general syntax that combines the different variants.

Tactic with_strategy strategy_level_or_var [ reference+ ] ltac_expr3¶

Executes ltac_expr3, applying the alternate unfolding behavior that the Strategy command controls, but only for 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 simpl and cbn or to ensure that unfolding does not fail.

Example

Opaque id.
Goal id 10 = 10.: 1 subgoal ============================ id 10 = 10
Fail unfold id.: The command has indeed failed with message: id is opaque.
with_strategy transparent [id] unfold id.: 1 subgoal ============================ 10 = 10

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 Qed nor Defined, so this tactic is most useful either in combination with 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., unfold does not fail just because the user made a constant Opaque.

This can be illustrated with the following example involving the factorial function.

Fixpoint fact (n : nat) : nat := match n with | 0 => 1 | S n' => n * fact n' end.: fact is defined fact is recursively defined (guarded on 1st argument)

Suppose now that, for whatever reason, we want in general to unfold the id function very late during conversion:

Strategy 1000 [id].

If we try to prove id (fact n) = fact n by reflexivity, it will now take time proportional to $n!$, because Coq will keep unfolding fact and * and + before it unfolds id, resulting in a full computation of fact n (in unary, because we are using nat), which takes time $n!$. We can see this cross the relevant threshold at around $n = 9$:

Goal True.: 1 subgoal ============================ True
Time assert (id (fact 8) = fact 8) by reflexivity.: Finished transaction in 0.224 secs (0.157u,0.064s) (successful) 1 subgoal H : id (fact 8) = fact 8 ============================ True
Time assert (id (fact 9) = fact 9) by reflexivity.: Finished transaction in 1.026 secs (1.009u,0.s) (successful) 1 subgoal H : id (fact 8) = fact 8 H0 : id (fact 9) = fact 9 ============================ True

Note that behavior will be the same if you mark id as Opaque because while most reduction tactics refuse to unfold Opaque constants, conversion treats Opaque as merely a hint to unfold this constant last.

We can get around this issue by using with_strategy:

Goal True.: 1 subgoal ============================ True
Fail Timeout 1 assert (id (fact 100) = fact 100) by reflexivity.: The command has indeed failed with message: Timeout!
Time assert (id (fact 100) = fact 100) by with_strategy -1 [id] reflexivity.: Finished transaction in 0.001 secs (0.001u,0.s) (successful) 1 subgoal H : id (fact 100) = fact 100 ============================ True

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

exact I.: No more subgoals.
Timeout 1 Defined.: Toplevel input, characters 0-18: > Timeout 1 Defined. > ^^^^^^^^^^^^^^^^^^ Error: Timeout!

We can fix this issue by using abstract:

Goal True.: 1 subgoal ============================ True
Time assert (id (fact 100) = fact 100) by with_strategy -1 [id] abstract reflexivity.: Finished transaction in 0.003 secs (0.002u,0.s) (successful) 1 subgoal H : id (fact 100) = fact 100 ============================ True
exact I.: No more subgoals.
Time Defined.: Finished transaction in 0.001 secs (0.001u,0.s) (successful)

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 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 Qed and Defined without using abstract as an intermediary, this tactic does not play well with coqchk, even when used with abstract, due to the inability of tactics to persist information about conversion hints in the proof term. See #12200 for more details.

Conversion tactics applied to hypotheses¶

The form tactic in ident+, applies tactic (any of the conversion tactics listed in this section) to the hypotheses ident+.

If ident is a local definition, then ident can be replaced by type of ident to address not the body but the type of the local definition.

Example: unfold not in (type of H1) (type of H3).