conv
The conv, or conversion, tactic allows targeted rewriting within a goal.
The argument to conv is written in a separate language that interoperates with the main tactic language; it features commands to navigate to specific subterms within the goal along with commands that allow these subterms to be rewritten.
conv is useful when rewrites should only be applied in part of a goal (e.g. only on one side of an equality), rather than across the board, or when rewrites should be applied underneath a binder that prevents tactics like rw from accessing the term.
The conversion tactic language is very similar to the main tactic language: it uses the same proof states, tactics work primarily on the main goal and may either fail or succeed with a sequence of new goals, and macro expansion is interleaved with tactic execution.
Unlike the main tactic language, in which tactics are intended to eventually solve goals, the conv tactic is used to change a goal so that it becomes amenable to further processing in the main tactic language.
Goals that are intended to be rewritten with conv are shown with a vertical bar instead of a turnstile.
conv
conv => ... allows the user to perform targeted rewriting on a goal or hypothesis,
by focusing on particular subexpressions.
See https://lean-lang.org/theorem_proving_in_lean4/conv.html for more details.
Basic forms:
conv => cs will rewrite the goal with conv tactics cs.
conv at h => cs will rewrite hypothesis h.
conv in pat => cs will rewrite the first subexpression matching pat (see pattern).
conv
In this example, there are multiple instances of addition, and rw would by default rewrite the first instance that it encounters.
Using conv to navigate to the specific subterm before rewriting leaves rw no choice but to rewrite the correct term.
example (x y z : Nat) : x + (y + z) = (x + z) + y := x:Naty:Natz:Nat⊢ x + (y + z) = x + z + y
conv =>
x:Naty:Natz:Nat| x + (y + z)
x:Naty:Natz:Nat| y + z
rw [x:Naty:Natz:Nat| z + y]
All goals completed! 🐙
conv
In this example, addition occurs under binders, so rw can't be used.
However, after using conv to navigate to the function body, it succeeds.
The nested use of conv causes control to return to the current position in the term after performing further conversions on one of its subterms.
Because the goal is a reflexive equation after rewriting, conv automatically closes it.
example : (fun (x y z : Nat) => x + (y + z)) = (fun x y z => (z + x) + y) := ⊢ (fun x y z => x + (y + z)) = fun x y z => z + x + y
conv =>
| fun x y z => x + (y + z)
x:Naty:Natz:Nat| x + (y + z)
conv =>
x:Naty:Natz:Nat| y + z
rw [x:Naty:Natz:Nat| z + y]
rw [x:Naty:Natz:Nat| x + z + y]
x:Naty:Natz:Nat| x + z
rw [x:Naty:Natz:Nat| z + x]
first
first | conv | ... runs each conv until one succeeds, or else fails.
try
try tac runs tac and succeeds even if tac failed.
<;>
repeat
repeat convs runs the sequence convs repeatedly until it fails to apply.
skip
skip does nothing.
{ ... }
{ convs } runs the list of convs on the current target, and any subgoals that
remain are trivially closed by skip.
( ... )
(convs) runs the convs in sequence on the current list of targets.
This is pure grouping with no added effects.
done
done succeeds iff there are no goals remaining.
all_goals
all_goals tac runs tac on each goal, concatenating the resulting goals, if any.
any_goals
any_goals tac applies the tactic tac to every goal, and succeeds if at
least one application succeeds.
case ... => ...
case tag => tac focuses on the goal with case name tag and solves it using tac,
or else fails.
case tag x₁ ... xₙ => tac additionally renames the n most recent hypotheses
with inaccessible names to the given names.
case tag₁ | tag₂ => tac is equivalent to (case tag₁ => tac); (case tag₂ => tac).
case' ... => ...
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 tac failed.
Recall that case closes the goal using sorry when tac fails, and
the tactic execution is not interrupted.
next ... => ...
next => tac focuses on the next goal and solves it using tac, or else fails.
next x₁ ... xₙ => tac additionally renames the n most recent hypotheses with
inaccessible names to the given names.
focus
focus tac focuses on the main goal, suppressing all other goals, and runs tac on it.
Usually · tac, which enforces that the goal is closed by tac, should be preferred.
. ...
· conv focuses on the main conv goal and tries to solve it using s.
· ...
· conv focuses on the main conv goal and tries to solve it using s.
fail_if_success
fail_if_success t fails if the tactic t succeeds.
lhsTraverses into the left subterm of a binary operator.
In general, for an n-ary operator, it traverses into the second to last argument.
It is a synonym for arg -2.
rhsTraverses into the right subterm of a binary operator.
In general, for an n-ary operator, it traverses into the last argument.
It is a synonym for arg -1.
fun
Traverses into the function of a (unary) function application.
For example, | f a b turns into | f a. (Use arg 0 to traverse into f.)
congr
Performs one step of "congruence", which takes a term and produces
subgoals for all the function arguments. For example, if the target is f x y then
congr produces two subgoals, one for x and one for y.
arg [@]i
arg i traverses into the i'th argument of the target. For example if the
target is f a b c d then arg 1 traverses to a and arg 3 traverses to c.
The index may be negative; arg -1 traverses into the last argument,
arg -2 into the second-to-last argument, and so on.
arg @i is the same as arg i but it counts all arguments instead of just the
explicit arguments.
arg 0 traverses into the function. If the target is f a b c d, arg 0 traverses into f.
enter
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 arg i.
enter [@i] is equivalent to arg @i.
enter [x] (where x is 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 b.
pattern
pattern pat traverses to the first subterm of the target that matches pat.
pattern (occs := *) pat traverses to every subterm of the target that matches pat
which is not contained in another match of pat. It generates one subgoal for each matching
subterm.
pattern (occs := 1 2 4) pat matches occurrences 1, 2, 4 of pat and 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 := 2 returns | f a
occs := 2 3 returns | f a and | f b
occs := 1 3 is an error, because after skipping f b there is no third match.
ext
ext x traverses into a binder (a fun x => e or ∀ x, e expression)
to target e, introducing name x in the process.
args
args traverses into all arguments. Synonym for congr.
left
left traverses into the left argument. Synonym for lhs.
right
right traverses into the right argument. Synonym for rhs.
intro
intro traverses into binders. Synonym for ext.
whnf
Reduces the target to Weak Head Normal Form. This reduces definitions
in "head position" until a constructor is exposed. For example, List.map f [a, b, c]
weak head normalizes to f a :: List.map f [b, c].
reducePuts term in normal form, this tactic is meant for debugging purposes only.
zetaExpands let-declarations and let-variables.
delta
delta id1 id2 ... unfolds all occurrences of id1, id2, ... in the target.
Like the 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
unfold id unfolds all occurrences of definition id in the target.
unfold id1 id2 ... is equivalent to unfold id1; unfold id2; ....
Definitions can be either global or local definitions.
For non-recursive global definitions, this tactic is identical to delta.
For recursive global definitions, it uses the "unfolding lemma" id.eq_def,
which is generated for each recursive definition, to unfold according to the recursive definition given by the user.
Only one level of unfolding is performed, in contrast to simp only [id], which unfolds definition id recursively.
This is the conv version of the unfold tactic.
simp
simp [thm] performs simplification using thm and marked @[simp] lemmas.
See the simp tactic for more information.
dsimp
dsimp is the definitional simplifier in conv-mode. It differs from simp in that it only
applies theorems that hold by reflexivity.
Examples:
example (a : Nat): (0 + 0) = a - a := by
conv =>
lhs
dsimp
rw [← Nat.sub_self a]
simp_match
simp_match simplifies match expressions. For example,
match [a, b] with | [] => 0 | hd :: tl => hd
simplifies to a.
change
change t' replaces the target t with t',
assuming t and t' are definitionally equal.
rewrite
rw [thm] rewrites the target using thm. See the rw tactic for more information.
rw
rw [rules] applies the given list of rewrite rules to the target.
See the rw tactic for more information.
erw
erw [rules] is a shorthand for rw (transparency := .default) [rules].
This does rewriting up to unfolding of regular definitions (by comparison to regular rw
which only unfolds @[reducible] definitions).
apply
The apply thm conv tactic is the same as apply thm the tactic.
There are no restrictions on thm, but strange results may occur if thm
cannot be reasonably interpreted as proving one equality from a list of others.
conv'
Executes the given conv block without converting regular goal into a conv goal.
tactic
Focuses, converts the conv goal ⊢ lhs into a regular goal ⊢ lhs = rhs, and then executes the given tactic block.
tactic'
Executes the given tactic block without converting conv goal into a regular goal.
conv'
Executes the given conv block without converting regular goal into a conv goal.
conv => ...
conv => cs runs cs in sequence on the target t,
resulting in t', which becomes the new target subgoal.
trace_state
trace_state prints the current goal state.
rfl
rfl closes one conv goal "trivially", by using reflexivity
(that is, no rewriting).
norm_cast
norm_cast tactic in conv mode.