4.22 Rewriting with `conv`

The conv tactic provides fine-grained control over rewriting by allowing you to navigate inside an expression and apply transformations at a precise location. In Lean, conv is used when rw or simp either affect too much or fail to reach the intended subterm.

Basic structure

A conv block focuses on a specific part of the goal:

conv =>
  lhs
  rw [h]

This restricts rewriting to the left-hand side of the goal. Similarly:

conv =>
  rhs
  rw [h]

targets the right-hand side.

Navigating expressions

Inside conv, you can descend into subterms using congr, which mirrors the structure of the expression:

example (a b : Nat) (h : a = b) :
  (a + 1) * 2 = (b + 1) * 2 := by
  conv =>
    lhs
    congr
    rw [h]
  rfl

The congr step moves into the argument of multiplication, exposing a + 1.

You can apply multiple navigation steps:

conv =>
  lhs
  congr
  congr
  rw [h]

Each congr descends one level deeper.

Rewriting specific occurrences

When a term appears multiple times, conv allows you to rewrite only one occurrence:

example (a b : Nat) (h : a = b) :
  a + a = b + a := by
  conv =>
    lhs
    congr
    rw [h]
  rfl

Only the first a is rewritten.

Combining with simplification

You can use simp inside conv:

example (a : Nat) :
  (a + 0) + 1 = a + 1 := by
  conv =>
    lhs
    simp
  rfl

This simplifies a subexpression without affecting the rest of the goal.

Rewriting under binders

conv can reach inside binders without introducing variables:

example (a b : Nat) (h : a = b) :
  (fun x => x + a) = (fun x => x + b) := by
  conv =>
    lhs
    congr
    rw [h]
  rfl

This avoids explicit use of funext in simple cases, though extensionality is often clearer for function equality.

Working with nested structures

For deeply nested expressions, conv provides a path-based approach:

example (a b : Nat) (h : a = b) :
  ((a + 1) + 2) + 3 = ((b + 1) + 2) + 3 := by
  conv =>
    lhs
    congr
    congr
    rw [h]
  rfl

Each congr step moves inward.

Practical guidance

• Use conv when rw affects too many occurrences.
• Use conv when rewriting must target a deeply nested subterm.
• Keep navigation steps explicit and minimal.
• Prefer rw or simp for simple cases; reserve conv for precision work.
• Combine conv with simp for local normalization.

Summary

conv provides precise control over where rewriting occurs. It allows you to navigate expression structure and apply transformations exactly where needed. This is essential when dealing with complex terms where global rewriting is either too aggressive or insufficient.