def Lean.Parser.Tactic.Conv.conv.quot : ParserDescr

def Lean.Parser.Category.conv : Category

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.

def Lean.Parser.Tactic.Conv.convSeq1Indented : ParserDescr

def Lean.Parser.Tactic.Conv.convSeqBracketed : ParserDescr

def Lean.Parser.Tactic.Conv.convSeq : ParserDescr

def Lean.Parser.Tactic.Conv.occsWildcard : ParserDescr

The * occurrence list means to apply to all occurrences of the pattern.

def Lean.Parser.Tactic.Conv.occsIndexed : ParserDescr

A list 1 2 4 of occurrences means to apply to the first, second, and fourth occurrence of the pattern.

def Lean.Parser.Tactic.Conv.occs : ParserDescr

An occurrence specification, either * or a list of numbers. The default is [1].

def Lean.Parser.Tactic.Conv.withAnnotateState : ParserDescr

with_annotate_state stx t annotates the lexical range of stx : Syntax with the initial and final state of running tactic t.

def Lean.Parser.Tactic.Conv.skip : ParserDescr

skip does nothing.

def Lean.Parser.Tactic.Conv.cbv : ParserDescr

cbv performs simplification that closely mimics call-by-value evaluation. It reduces the target term by unfolding definitions using their defining equations and applying matcher equations. The unfolding is propositional, so cbv also works with functions defined via well-founded recursion or partial fixpoints.

The proofs produced by cbv only use the three standard axioms. In particular, they do not require trust in the correctness of the code generator.

This tactic is experimental and its behavior is likely to change in upcoming releases of Lean.

def Lean.Parser.Tactic.Conv.lhs : ParserDescr

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.

def Lean.Parser.Tactic.Conv.rhs : ParserDescr

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.

def Lean.Parser.Tactic.Conv.fun : ParserDescr

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.)

def Lean.Parser.Tactic.Conv.whnf : ParserDescr

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].

def Lean.Parser.Tactic.Conv.zeta : ParserDescr

Expands let-declarations and let-variables.

def Lean.Parser.Tactic.Conv.reduce : ParserDescr

Puts term in normal form, this tactic is meant for debugging purposes only.

def Lean.Parser.Tactic.Conv.congr : ParserDescr

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.

def Lean.Parser.Tactic.Conv.argArg : ParserDescr

def Lean.Parser.Tactic.Conv.arg : ParserDescr

• 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.

def Lean.Parser.Tactic.Conv.ext : ParserDescr

ext x traverses into a binder (a fun x => e or ∀ x, e expression) to target e, introducing name x in the process.

def Lean.Parser.Tactic.Conv.change : ParserDescr

change t' replaces the target t with t', assuming t and t' are definitionally equal.

def Lean.Parser.Tactic.Conv.delta : ParserDescr

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.

def Lean.Parser.Tactic.Conv.unfold : ParserDescr

• 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.

def Lean.Parser.Tactic.Conv.pattern : ParserDescr

• 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.

def Lean.Parser.Tactic.Conv.rewrite : ParserDescr

rw [thm] rewrites the target using thm. See the rw tactic for more information.

def Lean.Parser.Tactic.Conv.simp : ParserDescr

simp [thm] performs simplification using thm and marked @[simp] lemmas. See the simp tactic for more information.

def Lean.Parser.Tactic.Conv.simpTrace : ParserDescr

simp? takes the same arguments as simp, but reports an equivalent call to simp only that would be sufficient to close the goal. See the simp? tactic for more information.

def Lean.Parser.Tactic.Conv.dsimp : ParserDescr

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]

def Lean.Parser.Tactic.Conv.dsimpTrace : ParserDescr

simp? takes the same arguments as simp, but reports an equivalent call to simp only that would be sufficient to close the goal. See the simp? tactic for more information.

def Lean.Parser.Tactic.Conv.simpMatch : ParserDescr

simp_match simplifies match expressions. For example,

match [a, b] with
| [] => 0
| hd :: tl => hd

simplifies to a.

def Lean.Parser.Tactic.Conv.clear : ParserDescr

Removes one or more hypotheses from the local context.

def Lean.Parser.Tactic.Conv.nestedTacticCore : ParserDescr

Executes the given tactic block without converting conv goal into a regular goal.

def Lean.Parser.Tactic.Conv.nestedTactic : ParserDescr

Focuses, converts the conv goal ⊢ lhs into a regular goal ⊢ lhs = rhs, and then executes the given tactic block.

def Lean.Parser.Tactic.Conv.convTactic : ParserDescr

Executes the given conv block without converting regular goal into a conv goal.

def Lean.Parser.Tactic.Conv.nestedConv : ParserDescr

{ convs } runs the list of convs on the current target, and any subgoals that remain are trivially closed by skip.

def Lean.Parser.Tactic.Conv.paren : ParserDescr

(convs) runs the convs in sequence on the current list of targets. This is pure grouping with no added effects.

def Lean.Parser.Tactic.Conv.convRfl : ParserDescr

rfl closes one conv goal "trivially", by using reflexivity (that is, no rewriting).

def Lean.Parser.Tactic.Conv.convDone : ParserDescr

done succeeds iff there are no goals remaining.

def Lean.Parser.Tactic.Conv.convTrace_state : ParserDescr

trace_state prints the current goal state.

def Lean.Parser.Tactic.Conv.allGoals : ParserDescr

all_goals tac runs tac on each goal, concatenating the resulting goals, if any.

def Lean.Parser.Tactic.Conv.anyGoals : ParserDescr

any_goals tac applies the tactic tac to every goal, and succeeds if at least one application succeeds.

def Lean.Parser.Tactic.Conv.case : ParserDescr

• 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).

def Lean.Parser.Tactic.Conv.case' : ParserDescr

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.

def Lean.Parser.Tactic.Conv.«convNext__=>_» : ParserDescr

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.

def Lean.Parser.Tactic.Conv.focus : ParserDescr

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.

def Lean.Parser.Tactic.Conv.convConvSeq : ParserDescr

conv => cs runs cs in sequence on the target t, resulting in t', which becomes the new target subgoal.

def Lean.Parser.Tactic.Conv.«conv·._» : ParserDescr

· conv focuses on the main conv goal and tries to solve it using s.

def Lean.Parser.Tactic.Conv.failIfSuccess : ParserDescr

fail_if_success t fails if the tactic t succeeds.

def Lean.Parser.Tactic.Conv.convRw__ : ParserDescr

rw [rules] applies the given list of rewrite rules to the target. See the rw tactic for more information.

def Lean.Parser.Tactic.Conv.convErw__ : ParserDescr

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).

def Lean.Parser.Tactic.Conv.convArgs : ParserDescr

args traverses into all arguments. Synonym for congr.

def Lean.Parser.Tactic.Conv.convLeft : ParserDescr

left traverses into the left argument. Synonym for lhs.

def Lean.Parser.Tactic.Conv.convRight : ParserDescr

right traverses into the right argument. Synonym for rhs.

def Lean.Parser.Tactic.Conv.convIntro___ : ParserDescr

intro traverses into binders. Synonym for ext.

def Lean.Parser.Tactic.Conv.enterPattern : ParserDescr

def Lean.Parser.Tactic.Conv.enterArg : ParserDescr

def Lean.Parser.Tactic.Conv.enter : ParserDescr

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.
• enter [in e] (where e is a term) is equivalent to pattern e. Occurrences can be specified with enter [in (occs := ...) e]. For example, given the target f (g a (fun x => x b)), enter [1, 2, x, 1] will traverse to the subterm b.

def Lean.Parser.Tactic.Conv.convApply_ : ParserDescr

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.

def Lean.Parser.Tactic.Conv.first : ParserDescr

first | conv | ... runs each conv until one succeeds, or else fails.

def Lean.Parser.Tactic.Conv.convTry_ : ParserDescr

try tac runs tac and succeeds even if tac failed.

def Lean.Parser.Tactic.Conv.«conv_<;>_» : TrailingParserDescr

tac <;> tac' runs tac on the main goal and tac' on each produced goal, concatenating all goals produced by tac'.

def Lean.Parser.Tactic.Conv.convRepeat_ : ParserDescr

repeat convs runs the sequence convs repeatedly until it fails to apply.

def Lean.Parser.Tactic.Conv.extractLets : ParserDescr

Extracts let and have expressions from within the target expression. This is the conv mode version of the extract_lets tactic.

• extract_lets extracts all the lets from the target.
• extract_lets x y z extracts all the lets from the target and uses x, y, and z for the first names. Using _ for a name leaves it unnamed.

Limitation: the extracted local declarations do not persist outside of the conv goal. See also lift_lets, which does not extract lets as local declarations.

def Lean.Parser.Tactic.Conv.liftLets : ParserDescr

Lifts let and have expressions within the target expression as far out as possible. This is the conv mode version of the lift_lets tactic.

def Lean.Parser.Tactic.Conv.letToHave : ParserDescr

Transforms let expressions into have expressions within the target expression when possible. This is the conv mode version of the let_to_have tactic.

def Lean.Parser.Tactic.Conv.conv : ParserDescr

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).

def Lean.Parser.Tactic.Conv.normCast : ParserDescr

norm_cast tactic in conv mode.