Introduction to the conversion mode tactic #
Inside a tactic block, one can use the
conv tactic to enter conversion
mode. This mode allows one to travel into subexpressions inside assumptions
and goals, even inside lambda functions and foralls, to apply targeted rewrites,
simplifications, and other tactics.
This is similar to the conversion tacticals (tactic combinators) found in other theorem provers like HOL4, HOL Light or Isabelle.
Basic navigation and rewriting #
As a first example, let us prove
example (a b c : ℕ) : a * (b * c) = a * (c * b) (examples in this file
are somewhat artificial since the
ring tactic from
Mathlib.Tactic.Ring could finish them immediately). The naive first attempt is
to enter tactic mode and try
rw [mul_comm]. But this transforms the goal
b * c * a = a * (c * b), after commuting the very first
multiplication appearing in the term. There are several ways to fix this
issue, and one way is to use a more precise tool: the
conversion mode. The following code block shows the current target after
each line. Note that the target is prefixed by
| where normal tactic mode
shows a goal prefixed by
⊢. Both cases are still called "goals" though.
example (a b c : ℕ) : a * (b * c) = a * (c * b) := by conv => -- `| a * (b * c) = a * (c * b)` lhs -- `| a * (b * c)` congr -- 2 goals : `| a` and `| b * c` rfl -- skip `| a` goal rw [mul_comm] -- `| c * b`
The above snippet show three navigation commands:
lhsnavigates to the left-hand side of a relation (here equality), there is also a
rhsnavigating to the right-hand side.
congrcreates as many targets as there are arguments to the current head function (here the head function is multiplication)
rflgoes to the next target
Once we arrive to the relevant target, we can use
rw as in normal tactic mode.
At the end,
conv will automatically use
rfl to skip the last remaining target.
The second main reason to use conversion mode is to rewrite subexpressions
involving bound variables ("rewrite under binders").
Suppose we want to prove
example : (fun x : ℕ => 0 + x) = (fun x => x).
The naive first attempt is to enter tactic mode and try
However, this fails with a frustrating
tactic 'rewrite' failed, did not find instance of the pattern in the target expression 0 + ?a ⊢ (fun x ↦ 0 + x) = fun x ↦ x
The solution is:
example : (fun x : ℕ => 0 + x) = (fun x => x) := by conv => -- | (fun x ↦ 0 + x) = fun x ↦ x lhs -- | fun x ↦ 0 + x ext x -- | 0 + x rw [zero_add] -- | x
ext is the navigation command entering inside the
fun binder (the
is optional). Note that this example is somewhat artificial, one could also do:
example : (fun x : ℕ => 0 + x) = (fun x => x) := by ext rw [zero_add]
All of this is also available for converting a hypothesis
H in the local context by
using the syntax
conv at H => ....
Here are a more ways to navigate expressions:
arg inavigates to the
ith explicit argument. It is like doing
congrand the appropriate number of
rfls for all but the
arg @inavigates to the
ith argument, counting both explicit and implicit arguments.
enter [...], where the
...consists of a list of arguments appropriate for
ext, and then runs the corresponding
extcommands. For example,
enter [1,@2,x,3]is the same as
arg 1; arg @2; ext x; arg 3.
Pattern matching #
Navigation using the above commands can be tedious. One can shortcut it using pattern matching as follows:
example (a b c : ℕ) : a * (b * c) = a * (c * b) := by conv in b * c => -- | b * c rw [mul_comm] -- | c * b
in clause is short for
example (a b c : ℕ) : a * (b * c) = a * (c * b) := by conv => -- | a * (b * c) = a * (c * b) pattern b * c -- | b * c rw [mul_comm] -- | c * b
As usual for
=> block tactics, the body can be placed on a single line with tactics
separated by semicolons. This yields a one-liner:
example (a b c : ℕ) : a * (b * c) = a * (c * b) := by conv in b * c => rw [mul_comm]
Of course placeholders are allowed:
example (a b c : ℕ) : a * (b * c) = a * (c * b) := by conv in _ * c => rw [mul_comm]
In all those cases, only the first match is affected.
One can also specify which occurences to convert using an
occs clause, which
creates goals for every matched occurrence. These can then all be handled at once
The following performs rewriting only for the second and third occurrences of
b * c:
example (b c : ℕ) : (b * c) * (b * c) * (b * c) = (b * c) * (c * b) * (c * b) := by conv in (occs := 2 3) b * c => all_goals rw [mul_comm]
This can also be done using
pattern and the
<;> combinator, where, like
in normal tactic mode,
t1 <;> t2 means to run
t1 and then run
t2 for every goal
produced by it.
example (b c : ℕ) : (b * c) * (b * c) * (b * c) = (b * c) * (c * b) * (c * b) := by conv => pattern (occs := 2 3) b * c <;> rw [mul_comm]
conv tactic supports nested
conv mode. This allows one to do a targeted rewrite
using the power of
conv mode and then return to the original position with the rewritten
example (a b : ℕ) : a * b * (a * b) = b * a * (a * b) := by conv => -- | a * b * (a * b) = b * a * (a * b) conv => pattern (occs := 2) a * b; rw [mul_comm] -- | a * b * (b * a) = b * a * (a * b) rw [mul_comm] -- | b * a * (a * b) = b * a * (a * b)
Other tactics inside conversion mode #
Besides rewriting using
rw, one can use
unfold, among others.
for a more in-depth overview.