Guide: Conversion mode tactic #

This is a curated guide to point you toward how conv mode works and what tactics are available. It is not meant to be comprehensive, but rather a "cheat sheet." See also the conv introduction.

Syntax #

The syntax for the conv tactic is

"conv" ("at" ident)? ("in" ("(occs :=" ("*" <|> num+) ")")? term)? "=>" convSeq

where convSeq is any sequence of "conv tactics", which are tactics specifically written for conv mode.

The in clause is exactly the same as the arguments to the conv tactic pattern.

conv in ...pattArgs... =>

is short for

conv =>
  pattern ...patArgs...

Note that conv in (occs := 1 2 3) pat => ... starts with three goals (one for each occurrence), but conv in (occs := *) pat => ... starts with a single goal that converts in all occurrences simultaneously.

Mathlib also provides conv_lhs and conv_rhs variants to immediately apply either the lhs or rhs tactic.

What is conv mode? #

conv mode is essentially the normal tactic mode but with two differences.

  1. Only "conv tactics" can appear in the conv block. These are tactics with syntax in the conv category.

  2. The goals are all of the form ⊢ lhs = ?rhs with ?rhs a metavariable, but the goals are annotated in such a way that they display as | lhs.

Each conv tactic is aware that the goal is of this form, and in addition to solving for the goal like normal, they also solve for the ?rhs metavariable in some controlled way. For example, the rfl tactic uses rfl to solve the goal, which sets ?rhs := lhs. Other tactics, like congr, partially solve for ?rhs and create new goal metavariables for each unsolved-for hole.

Once all the tactics have had a chance to run, conv mode itself uses rfl to solve any remaining goals (note that in conv mode, every goal can be solved for by rfl!), and then it uses the resulting lhs = rhs proof to rewrite the goal in the surrounding normal tactic mode.

Conv tactics from Lean 4, Std4, and Mathlib4 #

Unless they're annotated with "Std4" or "Mathlib", the following tactics are defined in Lean 4 core.

Control #

Manipulation #

Reductions #

Debugging, for internal use, or otherwise technical #