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 defineseq
similar to this:Inductive eq {A : Type} (x : A) : A -> Prop := eq_refl : eq x x.The notation
x = y
represents the termeq x y
. The notationx = 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?
¶ Rewrites terms based on equalities. The type of
one_term
must have the form:where
EQ
is the Leibniz equalityeq
or a registered setoid equality. Note thateq term1 term2
is typically written with the infix notationterm1 = term2
. You mustRequire Setoid
to use the tactic with a setoid equality or with setoid rewriting. In the general form, anybinder
may be used, not just(xi: Ai)
.rewrite one_term
finds subterms matchingterm1
in the goal, and replaces them withterm2
(or the reverse if<-
is given). Some of the variablesx
i are solved by unification, and some of the typesA1, ..., An
may become new subgoals.rewrite
won't find occurrences insideforall
that refer to variables bound by theforall
; usesetoid_rewrite
if you want to find such occurrences.oriented_rewriter+,
The
oriented_rewriter
s are applied sequentially to the first goal generated by the previousoriented_rewriter
. If any of them fail, the tactic fails.-><-?
For
->
(the default),term1
is rewritten intoterm2
. For<-
,term2
is rewritten intoterm1
.natural? ?!?
natural
is the number of rewrites to perform. If?
is given,natural
is the maximum number of rewrites to perform; otherwisenatural
is the exact number of rewrites to perform.?
(withoutnatural
) performs the rewrite as many times as possible (possibly zero times). This form never fails.!
(withoutnatural
) 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 tonatural
.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.If
at occs_nums
is specified, rewriting is always done with setoid rewriting, even for Leibniz’s equality.by ltac_expr3
If specified, is used to resolve all side conditions generated by the tactic.
-
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 asrewrite
.
-
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
replace one_termfrom with one_termto occurrences? by ltac_expr3?
¶ -
Tactic
replace -><-? one_termfrom occurrences?
¶ The first form replaces all free occurrences of
one_termfrom
in the current goal withone_termto
and generates an equalityone_termto = one_termfrom
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, replacesone_termfrom
withtermto
using the first hypothesis whose type has the formone_termfrom = termto
. If<-
is given, the tactic uses the first hypothesis with the reverse form, i.e.termto = one_termfrom
.occurrences
The
type of
andvalue of
forms are not supported. Note you mustRequire Setoid
to use theat
clause inoccurrences
.by ltac_expr3
Applies the
ltac_expr3
to solve the generated equality.
-
Error
Terms do not have convertible types.
¶
-
Tactic
subst ident*
¶ For each
ident
, in order, for which there is a hypothesis in the formident = term
orterm = ident
, replacesident
withterm
everywhere in the hypotheses and the conclusion and clearsident
and the hypothesis from the context. If there are multiple hypotheses that match theident
, the first one is used. If noident
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 formident := 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
ident1 = ident2
andident1 = t
, ort′ = ident1
witht′
not a variable, and no other hypotheses of the formident2 = u
oru = ident2
; without the flag, a second call to subst would be necessary to replaceident2
byt
ort′
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
ident1 = f ident2
andident2 = g ident1
which without the flag would be a cause of failure ofsubst
.
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 formident = u
, oru′ = ident
withu′
not a variable. Finally, it preserves the initial order of hypotheses, which without the flag it may break.
-
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.
-
Flag
-
Tactic
simple subst
¶
-
Tactic
stepl one_term by ltac_expr?
¶ For chaining rewriting steps. It assumes a goal in the form
R term1 term2
whereR
is a binary relation and relies on a database of lemmas of the formforall x y z, R x y -> eq x z -> R z y
whereeq
is typically a setoid equality. The application ofstepl one_term
then replaces the goal byR one_term term2
and adds a new goal statingeq one_term term1
.If
ltac_expr
is specified, it is applied to the side condition.This tactic is especially useful for parametric setoids which are not accepted as regular setoids for
rewrite
andsetoid_replace
(see Generalized rewriting).
Rewriting with definitional equality¶
-
Tactic
change one_termfrom at occs_nums? with? one_termto occurrences?
¶ Replaces terms with other convertible terms. If
one_termfrom
is not specified, thenone_termfrom
replaces the conclusion and/or the specified hypotheses. Ifone_termfrom
is specified, the tactic replaces occurrences ofone_termto
within the conclusion and/or the specified hypotheses.one_termfrom at occs_nums? with?
Replaces the occurrences of
one_termfrom
specified byoccs_nums
withone_termto
, provided that the twoone_term
s are convertible.one_termfrom
may contain pattern variables such as?x
, whose value which will substituted forx
inone_termto
, such as inchange (f ?x ?y) with (g (x, y))
orchange (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 anyat 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.
See also
-
Tactic
change_no_check one_termfrom at occs_nums? with? one_termto occurrences?
¶ For advanced usage. Similar to
change
, but as an optimization, it skips checking thatone_termto
is convertible with the goal orone_termfrom
.Recall that the Coq kernel typechecks proofs again when they are concluded to ensure correctness. Hence, using
change
checks convertibility twice overall, whilechange_no_check
can produce ill-typed terms, but checks convertibility only once. Hence,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,
change_no_check
replacesFalse
withTrue
, butQed
then rejects the proof, ensuring consistency.Example
- Goal False.
- 1 subgoal ============================ False
- change_no_check True.
- 1 subgoal ============================ True
- exact I.
- No more subgoals.
- Qed.
- Toplevel input, characters 0-4: > Qed. > ^^^^ Error: The term "I" has type "True" while it is expected to have type "False".
Example
- Goal True -> False.
- 1 subgoal ============================ True -> False
- intro H.
- 1 subgoal H : True ============================ False
- change_no_check False in H.
- 1 subgoal H : False ============================ False
- exact H.
- No more subgoals.
- Qed.
- Toplevel input, characters 0-4: > Qed. > ^^^^ Error: The term "fun H : True => H" has type "True -> True" while it is expected to have type "True -> False".
-
Tactic
convert_concl_no_check one_term
¶ Deprecated since version 8.11.
Deprecated old name for
change_no_check
. Does not support any of its variants.
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
andcofix
expressions) and \(\zeta\) (contraction of local definitions), the flags are eitherbeta
,delta
,match
,fix
,cofix
,iota
orzeta
. Theiota
flag is a shorthand formatch
,fix
andcofix
. Thedelta
flag itself can be refined intodelta [ qualid+ ]
ordelta - [ 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 thedelta
flag does not apply to variables bound by a let-in construction inside theterm
itself (use here thezeta
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
, ormatch 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 propositionexists x. P(x)
reduce to a pair of a witnesst
, and a proof thatt
satisfies the predicateP
. Most of the time,t
may be computed without computing the proof ofP(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
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
andlazy 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 tovm_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 profilenative_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 ofnative_compute
in a script. From the Linux command line, runperf report
on the profile file to see the results. Consult theperf
documentation for more details.
-
Flag
-
Flag
Debug Cbv
¶ This flag makes
cbv
(and its derivativecompute
) 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 toc t
1... t
n andc
a constant. Ifc
is transparent then it replacesc
with its definition (sayt
) and then reduces(t t
1... 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 theArguments
command.Example: The term
fun n : nat => S n + S n
is not reduced byhnf
.
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 forsimpl
.The
cbn
tactic accepts the same flags ascbv
andlazy
. The behavior of bothsimpl
andcbn
can be tuned using theArguments
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 byplus' := plus
is possibly unfolded and reused in the recursive calls, but a constant such assucc := plus (S O)
is never unfolded. This is the main difference betweensimpl
andcbn
. The tacticcbn
reduces whenever it will be able to reuse it or not:succ t
is reduced toS t
.
-
Variant
cbn [ qualid+ ]
-
Variant
cbn - [ qualid+ ]
These are respectively synonyms of
cbn beta delta [ qualid+ ] iota zeta
andcbn beta delta - [ qualid+ ] iota zeta
(seecbn
).
-
Variant
simpl pattern at natural+
This applies
simpl
only to thenatural+
occurrences of the subterms matchingpattern
in the current goal.-
Error
Too few occurrences.
¶
-
Error
-
Variant
simpl qualid
-
Variant
simpl string
This applies
simpl
only to the applicative subterms whose head occurrence is the unfoldable constantqualid
(the constant can be referred to by its notation usingstring
if such a notation exists).
-
Variant
simpl qualid at natural+
-
Variant
simpl string at natural+
This applies
simpl
only to thenatural+
applicative subterms whose head occurrence isqualid
(orstring
).
-
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 whichqualid
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 instancecbv 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 bygoal_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 ofqualid
to be unfolded. Occurrences are located from left to right.
-
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
wherestring
gets its interpretation from the scope bound to the delimiting keyident
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.
-
Error
-
Tactic
fold term
¶ This tactic applies to any goal. The term
term
is reduced using thered
tactic. Every occurrence of the resultingterm
in the goal is then replaced byterm
. 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, thefold
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
-
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 (sayT
) byreplacing all occurrences of
term
inT
with a fresh variableabstracting 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 oft
in \(\varphi\)(t)
, thenpattern t
transforms it into(fun x:A =>
\(\varphi\)(x)) t
. This tactic can be used, for instance, when the tacticapply
fails on matching.
-
Variant
pattern term at natural+
Only the occurrences
natural+
ofterm
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+
ofterm
are considered for \(\beta\)-expansion. Occurrences are located from left to right.
-
Variant
pattern term+,
Starting from a goal \(\varphi\)
(t
1... t
m)
, the tacticpattern t
1, ..., t
m generates the equivalent goal(fun (x
1:A
1) ... (x
m:A
m) =>
\(\varphi\)(x
1... x
m)) t
1... t
m. Ift
i occurs in one of the generated typesA
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+
ofterm
starting fromterm
.
-
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 theStrategy
command controls, but only forltac_expr3
. This can be useful for guarding calls to reduction in tactic automation to ensure that certain constants are never unfolded by tactics likesimpl
andcbn
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
norDefined
, so this tactic is most useful either in combination withabstract
, 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 constantOpaque
.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
byreflexivity
, it will now take time proportional to \(n!\), because Coq will keep unfoldingfact
and*
and+
before it unfoldsid
, resulting in a full computation offact n
(in unary, because we are usingnat
), 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.231 secs (0.122u,0.106s) (successful) 1 subgoal H : id (fact 8) = fact 8 ============================ True
- Time assert (id (fact 9) = fact 9) by reflexivity.
- Finished transaction in 0.912 secs (0.894u,0.001s) (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
asOpaque
because while most reduction tactics refuse to unfoldOpaque
constants, conversion treatsOpaque
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.003u,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
andDefined
without usingabstract
as an intermediary, this tactic does not play well withcoqchk
, even when used withabstract
, 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 hypothesesident+
.If
ident
is a local definition, thenident
can be replaced bytype of ident
to address not the body but the type of the local definition.Example:
unfold not in (type of H1) (type of H3)
.