Equations
- One or more equations did not get rendered due to their size.
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.
Equations
The *
occurrence list means to apply to all occurrences of the pattern.
A list 1 2 4
of occurrences means to apply to the first, second, and fourth
occurrence of the pattern.
An occurrence specification, either *
or a list of numbers. The default is [1]
.
with_annotate_state stx t
annotates the lexical range of stx : Syntax
with
the initial and final state of running tactic t
.
Equations
- One or more equations did not get rendered due to their size.
skip
does nothing.
Equations
- Lean.Parser.Tactic.Conv.skip = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.skip 1024 (Lean.ParserDescr.nonReservedSymbol "skip" false)
Traverses 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
.
Traverses 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
.
Equations
- Lean.Parser.Tactic.Conv.rhs = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.rhs 1024 (Lean.ParserDescr.nonReservedSymbol "rhs" false)
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
.)
Equations
- Lean.Parser.Tactic.Conv.fun = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.fun 1024 (Lean.ParserDescr.nonReservedSymbol "fun" false)
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]
.
Equations
- Lean.Parser.Tactic.Conv.whnf = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.whnf 1024 (Lean.ParserDescr.nonReservedSymbol "whnf" false)
Expands let-declarations and let-variables.
Equations
- Lean.Parser.Tactic.Conv.zeta = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.zeta 1024 (Lean.ParserDescr.nonReservedSymbol "zeta" false)
Puts term in normal form, this tactic is meant for debugging purposes only.
Equations
- Lean.Parser.Tactic.Conv.reduce = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.reduce 1024 (Lean.ParserDescr.nonReservedSymbol "reduce" false)
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
traverses into thei
'th argument of the target. For example if the target isf a b c d
thenarg 1
traverses toa
andarg 3
traverses toc
. 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 asarg i
but it counts all arguments instead of just the explicit arguments.arg 0
traverses into the function. If the target isf a b c d
,arg 0
traverses intof
.
Equations
- One or more equations did not get rendered due to their size.
change t'
replaces the target t
with t'
,
assuming t
and t'
are definitionally equal.
unfold id
unfolds all occurrences of definitionid
in the target.unfold id1 id2 ...
is equivalent tounfold 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.
Equations
- One or more equations did not get rendered due to their size.
pattern pat
traverses to the first subterm of the target that matchespat
.pattern (occs := *) pat
traverses to every subterm of the target that matchespat
which is not contained in another match ofpat
. It generates one subgoal for each matching subterm.pattern (occs := 1 2 4) pat
matches occurrences1, 2, 4
ofpat
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
(andoccs := *
) 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 skippingf b
there is no third match.
Equations
- One or more equations did not get rendered due to their size.
rw [thm]
rewrites the target using thm
. See the rw
tactic for more information.
simp_match
simplifies match expressions. For example,
match [a, b] with
| [] => 0
| hd :: tl => hd
simplifies to a
.
Executes the given tactic block without converting conv
goal into a regular goal.
Equations
- One or more equations did not get rendered due to their size.
Executes the given conv block without converting regular goal into a conv
goal.
Equations
- One or more equations did not get rendered due to their size.
{ convs }
runs the list of convs
on the current target, and any subgoals that
remain are trivially closed by skip
.
Equations
- Lean.Parser.Tactic.Conv.nestedConv = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.nestedConv 1022 Lean.Parser.Tactic.Conv.convSeqBracketed
(convs)
runs the convs
in sequence on the current list of targets.
This is pure grouping with no added effects.
Equations
- One or more equations did not get rendered due to their size.
rfl
closes one conv goal "trivially", by using reflexivity
(that is, no rewriting).
done
succeeds iff there are no goals remaining.
Equations
- Lean.Parser.Tactic.Conv.convDone = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.convDone 1024 (Lean.ParserDescr.nonReservedSymbol "done" false)
trace_state
prints the current goal state.
Equations
- Lean.Parser.Tactic.Conv.convTrace_state = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.convTrace_state 1024 (Lean.ParserDescr.nonReservedSymbol "trace_state" false)
all_goals tac
runs tac
on each goal, concatenating the resulting goals, if any.
Equations
- One or more equations did not get rendered due to their size.
any_goals tac
applies the tactic tac
to every goal, and succeeds if at
least one application succeeds.
case tag => tac
focuses on the goal with case nametag
and solves it usingtac
, or else fails.case tag x₁ ... xₙ => tac
additionally renames then
most recent hypotheses with inaccessible names to the given names.case tag₁ | tag₂ => tac
is equivalent to(case tag₁ => tac); (case tag₂ => tac)
.
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
- One or more equations did not get rendered due to their size.
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 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.
Equations
- One or more equations did not get rendered due to their size.
conv => cs
runs cs
in sequence on the target t
,
resulting in t'
, which becomes the new target subgoal.
Equations
- One or more equations did not get rendered due to their size.
· conv
focuses on the main conv goal and tries to solve it using s
.
Equations
- One or more equations did not get rendered due to their size.
fail_if_success t
fails if the tactic t
succeeds.
rw [rules]
applies the given list of rewrite rules to the target.
See the rw
tactic for more information.
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).
Equations
- One or more equations did not get rendered due to their size.
args
traverses into all arguments. Synonym for congr
.
Equations
- Lean.Parser.Tactic.Conv.convArgs = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.convArgs 1024 (Lean.ParserDescr.nonReservedSymbol "args" false)
left
traverses into the left argument. Synonym for lhs
.
Equations
- Lean.Parser.Tactic.Conv.convLeft = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.convLeft 1024 (Lean.ParserDescr.nonReservedSymbol "left" false)
right
traverses into the right argument. Synonym for rhs
.
intro
traverses into binders. Synonym for ext
.
Equations
- One or more equations did not get rendered due to their size.
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]
(wherex
is 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
.
Equations
- One or more equations did not get rendered due to their size.
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.
try tac
runs tac
and succeeds even if tac
failed.
repeat convs
runs the sequence convs
repeatedly until it fails to apply.
Equations
- One or more equations did not get rendered due to their size.
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: