\[\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}\]

Term rewriting and simplification¶

Rewriting expressions¶

These tactics use the equality eq:forall A:Type, A->A->Prop defined in file Logic.v (see Logic). The notation for eq T t u is simply t=u dropping the implicit type of t and u.

Tactic rewrite term¶

This tactic applies to any goal. The type of term must have the form

forall (x₁ :A₁ ) ... (x_n :A_n ), eq term₁ term₂ .

where eq is the Leibniz equality or a registered setoid equality.

Then rewrite term finds the first subterm matching term₁ in the goal, resulting in instances term₁' and term₂' and then replaces every occurrence of term₁' by term₂'. Hence, some of the variables x_i are solved by unification, and some of the types A₁, ..., A_n become new subgoals.

Error The term provided does not end with an equation.¶

Error Tactic generated a subgoal identical to the original goal. This happens if term does not occur in the goal.¶

Variant rewrite -> term: Is equivalent to rewrite term

Variant rewrite <- term: Uses the equality term₁ = term ₂ from right to left

Variant rewrite term in goal_occurrences

Analogous to rewrite term but rewriting is done following the clause goal_occurrences. For instance:

rewrite H in H' will rewrite H in the hypothesis H' instead of the current goal.
rewrite H in H' at 1, H'' at - 2 |- * means 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.
rewrite H in * |- will do rewrite H in H' for all hypotheses H' different from H. A success will happen as soon as at least one of these simpler tactics succeeds.
rewrite H in * is a combination of rewrite H and rewrite H in * |- that succeeds if at least one of these two tactics succeeds.

Orientation -> or <- can be inserted before the term to rewrite.

Variant rewrite term at occurrences: Rewrite only the given occurrences of term. Occurrences are specified from left to right as for pattern (pattern). The rewrite is always performed using setoid rewriting, even for Leibniz’s equality, so one has to Import Setoid to use this variant.

Variant rewrite term by tactic: Use tactic to completely solve the side-conditions arising from the rewrite.

Variant rewrite orientation term+, in ident?: Is equivalent to the n successive tactics rewrite term+;, each one working on the first subgoal generated by the previous one. An orientation -> or <- can be inserted before each 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 term to rewrite can be immediately prefixed by one of the following modifiers:

? : the tactic rewrite ?term performs the rewrite of term as many times as possible (perhaps zero time). This form never fails.
natural? : works similarly, except that it will do at most natural rewrites.
! : works as ?, except that at least one rewrite should succeed, otherwise the tactic fails.
natural! (or simply natural) : precisely natural rewrites of term will be done, leading to failure if these natural rewrites are not possible.

Variant erewrite term¶: This tactic works as rewrite term but turning unresolved bindings into existential variables, if any, instead of failing. It has the same variants as rewrite has.

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 replace term with term’¶

This tactic applies to any goal. It replaces all free occurrences of term in the current goal with term’ and generates an equality 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 cut term = term’; [intro H_n ; rewrite <- H_n ; clear H_n|| assumption || symmetry; try assumption].

Error Terms do not have convertible types.¶

Variant replace term with term’ by tactic: This acts as replace term with term’ but applies tactic to solve the generated subgoal term = term’.

Variant replace term: Replaces term with term’ using the first assumption whose type has the form term = term’ or term’ = term.

Variant replace -> term: Replaces term with term’ using the first assumption whose type has the form term = term’

Variant replace <- term: Replaces term with term’ using the first assumption whose type has the form term’ = term

Variant replace term with term? in goal_occurrences by tactic?
Variant replace -> term in goal_occurrences
Variant replace <- term in goal_occurrences: Acts as before but the replacements take place in the specified clauses (goal_occurrences) (see Performing computations) and not only in the conclusion of the goal. The clause argument must not contain any type of nor value of.

Variant cutrewrite <-->? (term₁ = term₂) in ident?¶: Deprecated since version 8.5: Use replace instead.

Tactic subst ident¶

This tactic applies to a goal that has ident in its context and (at least) one hypothesis, say H, of type ident = t or t = ident with ident not occurring in t. Then it replaces ident by t everywhere in the goal (in the hypotheses and in the conclusion) and clears ident and H from the context.

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

If 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 ident = t or t = ident, the first one is used.
If H is itself dependent in the goal, it is replaced by the proof of reflexivity of equality.

Variant subst ident+: This is equivalent to subst ident₁; ...; subst ident_n.

Variant subst: This applies subst repeatedly from top to bottom to all hypotheses of the context for which an equality of the form ident = t or t = ident or ident := t exists, with ident not occurring in t and ident not a section variable with indirect dependencies in the goal.

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_1` 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 to be 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. default.

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

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

Tactic stepl term¶

This tactic is for chaining rewriting steps. It assumes a goal of 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 term then replaces the goal by R term term and adds a new goal stating eq term term.

Command Declare Left Step term¶: Adds 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).

Variant stepl term by tactic: This applies stepl term then applies tactic to the second goal.

Variant stepr term by tactic¶: This behaves as stepl but on the right-hand-side of the binary relation. Lemmas are expected to be of the form forall x y z, R x y -> eq y z -> R x z.

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

Tactic change term¶

This tactic applies to any goal. It implements the rule Conv given in Subtyping rules. change U replaces the current goal T with U providing that U is well-formed and that T and U are convertible.

Error Not convertible.¶

Variant change term with term’: This replaces the occurrences of term by term’ in the current goal. The term term and term’ must be convertible.

Variant change term at natural+ with term’

This replaces the occurrences numbered natural+ of term by term’ in the current goal. The terms term and term’ must be convertible.

Error Too few occurrences.¶

Variant change term at natural+? with term? in goal_occurrences: In the presence of with, this applies change to the occurrences specified by goal_occurrences. In the absence of with, goal_occurrences is expected to only list hypotheses (and optionally the conclusion) without specifying occurrences (i.e. no at clause).

Variant now_show term: This is a synonym of change term. It can be used to make some proof steps explicit when refactoring a proof script to make it readable.

Performing computations¶

red_expr

::=

red

|

hnf

|

simpl delta_flag? reference_occspattern_occs?

|

cbv strategy_flag?

|

cbn strategy_flag?

|

lazy strategy_flag?

|

compute delta_flag?

|

vm_compute reference_occspattern_occs?

|

native_compute reference_occspattern_occs?

|

unfold reference_occs+,

|

fold one_term+

|

pattern pattern_occs+,

|

ident

delta_flag

::=

-? [ reference+ ]

::=

|

::=

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

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 Not reducible.¶

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 is claimed 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.384 secs (0.172u,0.212s) (successful) 1 subgoal H : id (fact 8) = fact 8 ============================ True
Time assert (id (fact 9) = fact 9) by reflexivity.: Finished transaction in 1.391 secs (1.386u,0.005s) (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.002 secs (0.002u,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.005 secs (0.001u,0.003s) (successful) 1 subgoal H : id (fact 100) = fact 100 ============================ True
exact I.: No more subgoals.
Time Defined.: Finished transaction in 0.002 secs (0.u,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¶

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