conv is the syntax category for a "conv tactic", where "conv" is short
for conversion. A conv tactic is a program which receives a target, printed as
| a, and is tasked with coming up with some term
b and a proof of
a = b.
It is mainly used for doing targeted term transformations, for example rewriting
only on the left side of an equality.
arg itraverses into the
i'th argument of the target. For example if the target is
f a b c dthen
arg 1traverses to
arg 3traverses to
arg @iis the same as
arg ibut it counts all arguments instead of just the explicit arguments.
delta id1 id2 ... unfolds all occurrences of
id2, ... in the target.
delta tactic, this ignores any definitional equations and uses
primitive delta-reduction instead, which may result in leaking implementation details.
Users should prefer
unfold for unfolding definitions.
unfold foounfolds all occurrences of
fooin the target.
unfold id1 id2 ...is equivalent to
unfold id1; unfold id2; .... Like the
unfoldtactic, this uses equational lemmas for the chosen definition to rewrite the target. For recursive definitions, only one layer of unfolding is performed.
pattern pattraverses to the first subterm of the target that matches
pattern (occs := *) pattraverses to every subterm of the target that matches
patwhich is not contained in another match of
pat. It generates one subgoal for each matching subterm.
pattern (occs := 1 2 4) patmatches occurrences
1, 2, 4of
patand produces three subgoals. Occurrences are numbered left to right from the outside in.
Note that skipping an occurrence of
pat will traverse inside that subexpression, which means
it may find more matches and this can affect the numbering of subsequent pattern matches.
For example, if we are searching for
f _ in
f (f a) = f b:
occs := 1 2(and
occs := *) returns
| f (f a)and
| f b
occs := 2returns
| f a
occs := 2 3returns
| f aand
| f b
occs := 1 3is an error, because after skipping
f bthere is no third match.
case tag => tacfocuses on the goal with case name
tagand solves it using
tac, or else fails.
case tag x₁ ... xₙ => tacadditionally renames the
nmost recent hypotheses with inaccessible names to the given names.
case tag₁ | tag₂ => tacis equivalent to
(case tag₁ => tac); (case tag₂ => tac).
case' is similar to the
case tag => tac tactic, but does not ensure the goal
has been solved after applying
tac, nor admits the goal if
case closes the goal using
tac fails, and
the tactic execution is not interrupted.
enter [arg, ...] is a compact way to describe a path to a subterm.
It is a shorthand for other conv tactics as follows:
enter [i]is equivalent to
enter [@i]is equivalent to
xis an identifier) is equivalent to
ext x. For example, given the target
f (g a (fun x => x b)),
enter [1, 2, x, 1]will traverse to the subterm
conv => ... allows the user to perform targeted rewriting on a goal or hypothesis,
by focusing on particular subexpressions.
See https://leanprover.github.io/theorem_proving_in_lean4/conv.html for more details.
conv => cswill rewrite the goal with conv tactics
conv at h => cswill rewrite hypothesis
conv in pat => cswill rewrite the first subexpression matching