# The conversion tactic mode #

Inside a tactic block, one can use the keyword `conv`

to enter conversion
mode. This mode allows to travel inside assumptions and goals, even
inside `λ`

binders in them, to apply rewriting or simplifying steps.

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
`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
into `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 mode
shows a goal prefixed by `⊢`

(these targets are still called "goals"
though).

```
example (a b c : ℕ) : a * (b * c) = a * (c * b) :=
begin
conv
begin -- | a * (b * c) = a * (c * b)
to_lhs, -- | a * (b * c)
congr, -- 2 goals : | a and | b * c
skip, -- | b * c
rw mul_comm, -- | c * b
end
end
```

The above snippet show three navigation commands:

`to_lhs`

navigates to the left hand side of a relation (here equality), there is also a`to_rhs`

navigating to the right hand side.`congr`

creates as many targets as there are arguments to the current head function (here the head function is multiplication)`skip`

goes to the next target

Once arrived at the relevant target, we can use `rw`

as in normal mode.
Note that Lean tries to solves the current goal if it became `x = x`

(in
the strict syntactical sense, definitional equality is not enough: one
needs to conclude by `refl`

or `trivial`

in this case).

The second main reason to use conversion mode is to rewrite under
binders. Suppose we want to prove `example (λ x : ℕ, 0+x) = (λ x, x)`

.
The naive first attempt is to enter tactic mode and try `rw zero_add`

.
But this fails with a frustrating

```
rewrite tactic failed, did not find
instance of the pattern in the target expression 0 + ?m_3
state:
⊢ (λ (x : ℕ), 0 + x) = λ (x : ℕ), x
```

The solution is:

```
example : (λ x : ℕ, 0 + x) = (λ x, x) :=
begin
conv
begin -- | (λ (x : ℕ), 0 + x) = λ (x : ℕ), x
to_lhs, -- | λ (x : ℕ), 0 + x
funext, -- | 0 + x
rw zero_add, -- | x
end
end
```

where `funext`

is the navigation command entering inside the `λ`

binder.
Note that this example is somewhat artificial, one could also do:

```
example : (λ x : ℕ, 0+x) = (λ x, x) :=
by funext ; rw zero_add
```

All this is also available to rewrite an hypothesis `H`

from the local context
using `conv at H`

.

## 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) :=
begin
conv in (b*c)
begin -- | b * c
rw mul_comm, -- | c * b
end
end
```

As usual, `begin`

and `end`

can be replaced by curly brackets to
delimit conversion mode and a single tactic invocation can be introduced
by `by`

to get the one liner:

```
example (a b c : ℕ) : a * (b * c) = a * (c * b) :=
by conv in (b*c) { rw mul_comm }
```

Beware that a well known bug makes Lean printing: "find converter failed, pattern was not found" when the tactics inside conversion mode fail, even if the pattern was actually found.

Of course wild-cards 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.
A more sophisticated version of pattern matching is available inside
conversion mode using the `for`

command. The following performs rewriting
only for the second and third occurrences of `b * c`

:

```
example (a b c : ℕ) : (b * c) * (b * c) * (b * c) = (b * c) * (c * b) * (c * b):=
by conv { for (b * c) [2, 3] { rw mul_comm } }
```

## Other tactics inside conversion mode #

Besides rewriting using `rw`

, one can use `simp`

, `dsimp`

, `change`

and `whnf`

.
`change`

is a useful tool -- it allows changing a term to something
definitionally equal, rather like the `show`

command in tactic mode.
The `whnf`

command means "reduces to weak head normal form" and will eventually
be explained in Programming in Lean section 8.4.

Extensions to `conv`

provided by mathlib, such as `ring`

and `norm_num`

, can be
found in the mathlib docs.