Module 6 · Lesson 2

conv — Targeted Rewriting

conv lets you navigate into subexpressions and rewrite precisely where you want, solving the "I can't rewrite the right occurrence" problem.

The Problem conv Solves

Standard rw rewrites all matching occurrences, or just the first one. When you need to rewrite a specific occurrence deep inside an expression,conv lets you navigate to exactly that spot.

lean

Try it

1-- Sometimes rw rewrites the wrong occurrence
2example (a b : Nat) : (a + b) * (a + b) = (b + a) * (a + b) := by
3  -- rw [Nat.add_comm]  -- Would rewrite both occurrences!
4  conv => 
5    lhs  -- focus on left-hand side
6    arg 1  -- first argument of *
7    rw [Nat.add_comm]
8  -- Now both sides are (b + a) * (a + b), and conv closes the goal with rfl

Key Takeaway

conv enters a "conversation mode" where you navigate to a subexpression and apply tactics to just that part.

Navigation Commands

Inside conv, you use navigation commands to "zoom in" on subexpressions. The main commands are lhs/rhsfor equation sides, arg n for function arguments, andext for going under binders.

lean

Try it

1-- lhs / rhs: go to left or right side of equation
2example (a b : Nat) : a + b = b + a := by
3  conv => 
4    lhs
5    rw [Nat.add_comm]
6
7-- arg n: go to nth argument (1-indexed)
8example (a b c : Nat) : (a + b) + c = (b + a) + c := by
9  conv =>
10    lhs
11    arg 1  -- go to (a + b)
12    rw [Nat.add_comm]
13
14-- ext: introduce binders (for under lambdas/foralls)
15example : (fun x : Nat => x + 0) = (fun x => x) := by
16  conv =>
17    lhs
18    ext x  -- introduce x
19    rw [Nat.add_zero]

Common conv Patterns

lean

Try it

1-- Rewrite inside a function argument
2example (xs : List Nat) : xs.map (· + 0) = xs.map id := by
3  conv =>
4    lhs
5    arg 1  -- the function argument
6    ext x
7    rw [Nat.add_zero]
8  simp [id]
9
10-- Rewrite one side of iff
11example (P Q : Prop) (h : P ↔ Q) : (P ∧ True) ↔ (Q ∧ True) := by
12  conv =>
13    lhs
14    arg 1
15    rw [h]
16
17-- Nested navigation
18example (a b c d : Nat) : ((a + b) + c) + d = ((b + a) + c) + d := by
19  conv =>
20    lhs
21    arg 1  -- (a + b) + c
22    arg 1  -- a + b
23    rw [Nat.add_comm]

Tactics Inside conv

lean

1-- rfl: close with reflexivity
2example (a : Nat) : a + 0 = a := by
3  conv => lhs; rw [Nat.add_zero]
4
5-- ring/omega inside conv
6example (a b : Nat) : (a + b) * 2 = 2 * (b + a) := by
7  conv => 
8    rhs
9    rw [Nat.add_comm]
10  ring
11
12-- simp at specific location
13example (xs : List Nat) : xs.reverse.reverse = xs := by
14  conv => lhs; simp

Deep Dive: conv Mode Navigation

Think of conv as zooming into your expression:

lean

1-- Expression: f (g (h x)) (k y)
2-- 
3-- conv =>
4--   arg 1     -- f (g (h x)) (k y) → g (h x)
5--   arg 1     -- g (h x) → h x
6--   arg 1     -- h x → x
7
8-- Other navigation:
9-- pattern e  -- go to subexpression matching pattern e
10-- enter [n]  -- same as arg n but for any position
11-- all        -- apply to all subexpressions

pattern Matching

lean

Try it

1-- Navigate by pattern matching
2example (a b c : Nat) : a + (b + c) = a + (c + b) := by
3  conv =>
4    lhs
5    pattern b + c  -- find and focus on b + c
6    rw [Nat.add_comm]
7
8-- Multiple patterns
9example (a b : Nat) : (a + 0) + (b + 0) = a + b := by
10  conv =>
11    lhs
12    pattern _ + 0
13    rw [Nat.add_zero]
14  -- Still have one more to do
15  conv =>
16    lhs
17    pattern _ + 0
18    rw [Nat.add_zero]

ℹ

Use pattern when the expression is complex and counting args would be error-prone.

Exercise: Rewrite One Occurrence

Use conv to rewrite just one occurrence of a + b.

lean

Try it

1example (a b : Nat) : (a + b) + (a + b) = (b + a) + (a + b) := by
2  conv =>
3    lhs
4    arg 1
5    rw [Nat.add_comm]
6  -- conv finishes with rfl, which closes the goal

conv with simp

lean

Try it

1-- simp only at specific positions
2example (xs : List Nat) (f : Nat → Nat) : 
3    (xs.map f).length = xs.length := by
4  conv => lhs; simp [List.length_map]
5
6-- Avoid unwanted simplification
7example (a b : Nat) : (a + b) * 1 = a + b := by
8  conv => 
9    lhs
10    arg 2  -- the 1
11    -- don't simp the whole thing, just verify * 1
12  simp [Nat.mul_one]

Changing Under Binders

lean

Try it

1-- ext to go under lambda
2example : (fun x : Nat => x * 2) = (fun x => 2 * x) := by
3  conv =>
4    lhs
5    ext x
6    rw [Nat.mul_comm]
7
8-- intro to go under forall
9example : (∀ x : Nat, x + 0 = x) ↔ (∀ x : Nat, x = x) := by
10  conv =>
11    lhs
12    intro x
13    rw [Nat.add_zero]

Examples

Specific Occurrence Rewrite

lean

1example (a b c : Nat) : a + b + c = c + b + a := by
2  conv =>
3    lhs
4    rw [Nat.add_assoc]
5    arg 2
6    rw [Nat.add_comm]
7  conv =>
8    lhs
9    rw [← Nat.add_assoc]
10    arg 1
11    rw [Nat.add_comm]
12  ring

Simplify Function Body

lean

1example (f : Nat → Nat) (h : ∀ n, f n = n + 1) : 
2    (fun x => f x + 1) = (fun x => x + 2) := by
3  conv =>
4    lhs
5    ext x
6    rw [h]
7  ring_nf

Rewrite in Hypothesis

lean

Try it

1example (a b : Nat) (h : a + b = 10) : b + a = 10 := by
2  conv at h =>
3    lhs
4    rw [Nat.add_comm]
5  exact h

calc Next: by_contra & by_cases