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.
Instances For
The * occurrence list means to apply to all occurrences of the pattern.
Instances For
A list 1 2 4 of occurrences means to apply to the first, second, and fourth
occurrence of the pattern.
Instances For
An occurrence specification, either * or a list of numbers. The default is [1].
Instances For
with_annotate_state stx t annotates the lexical range of stx : Syntax with
the initial and final state of running tactic t.
Instances For
Traverses into the left subterm of a binary operator.
(In general, for an n-ary operator, it traverses into the second to last argument.)
Instances For
Traverses into the right subterm of a binary operator.
(In general, for an n-ary operator, it traverses into the last argument.)
Instances For
Expands let-declarations and let-variables.
Instances For
Puts term in normal form, this tactic is meant for debugging purposes only.
Instances For
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.
Instances For
ext x traverses into a binder (a fun x => e or ∀ x, e expression)
to target e, introducing name x in the process.
Instances For
change t' replaces the target t with t',
assuming t and t' are definitionally equal.
Instances For
unfold foounfolds all occurrences offooin the target.unfold id1 id2 ...is equivalent tounfold id1; unfold id2; .... Like theunfoldtactic, this uses equational lemmas for the chosen definition to rewrite the target. For recursive definitions, only one layer of unfolding is performed.
Instances For
pattern pattraverses to the first subterm of the target that matchespat.pattern (occs := *) pattraverses to every subterm of the target that matchespatwhich is not contained in another match ofpat. It generates one subgoal for each matching subterm.pattern (occs := 1 2 4) patmatches occurrences1, 2, 4ofpatand 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(andoccs := *) returns| f (f a)and| f boccs := 2returns| f aoccs := 2 3returns| f aand| f boccs := 1 3is an error, because after skippingf bthere is no third match.
Instances For
rw [thm] rewrites the target using thm. See the rw tactic for more information.
Instances For
simp_match simplifies match expressions. For example,
match [a, b] with
| [] => 0
| hd :: tl => hd
simplifies to a.
Instances For
Executes the given tactic block without converting conv goal into a regular goal.
Instances For
Executes the given conv block without converting regular goal into a conv goal.
Instances For
{ convs } runs the list of convs on the current target, and any subgoals that
remain are trivially closed by skip.
Instances For
(convs) runs the convs in sequence on the current list of targets.
This is pure grouping with no added effects.
Instances For
rfl closes one conv goal "trivially", by using reflexivity
(that is, no rewriting).
Instances For
done succeeds iff there are no goals remaining.
Instances For
trace_state prints the current goal state.
Instances For
all_goals tac runs tac on each goal, concatenating the resulting goals, if any.
Instances For
any_goals tac applies the tactic tac to every goal, and succeeds if at
least one application succeeds.
Instances For
case tag => tacfocuses on the goal with case nametagand solves it usingtac, or else fails.case tag x₁ ... xₙ => tacadditionally renames thenmost recent hypotheses with inaccessible names to the given names.case tag₁ | tag₂ => tacis equivalent to(case tag₁ => tac); (case tag₂ => tac).
Instances For
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.
Instances For
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.
Instances For
conv => cs runs cs in sequence on the target t,
resulting in t', which becomes the new target subgoal.
Instances For
· conv focuses on the main conv goal and tries to solve it using s.
Instances For
fail_if_success t fails if the tactic t succeeds.
Instances For
rw [rules] applies the given list of rewrite rules to the target.
See the rw tactic for more information.
Instances For
erw [rules] is a shorthand for rw (config := { transparency := .default }) [rules].
This does rewriting up to unfolding of regular definitions (by comparison to regular rw
which only unfolds @[reducible] definitions).
Instances For
args traverses into all arguments. Synonym for congr.
Instances For
left traverses into the left argument. Synonym for lhs.
Instances For
right traverses into the right argument. Synonym for rhs.
Instances For
intro traverses into binders. Synonym for ext.
Instances For
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 toarg i.enter [@i]is equivalent toarg @i.enter [x](wherexis an identifier) is equivalent toext x. For example, given the targetf (g a (fun x => x b)),enter [1, 2, x, 1]will traverse to the subtermb.
Instances For
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.
Instances For
try tac runs tac and succeeds even if tac failed.
Instances For
repeat convs runs the sequence convs repeatedly until it fails to apply.
Instances For
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.
Basic forms:
conv => cswill rewrite the goal with conv tacticscs.conv at h => cswill rewrite hypothesish.conv in pat => cswill rewrite the first subexpression matchingpat(seepattern).