conv — Targeted Rewriting

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 goal is: (b + a) * (a + b) = (b + a) * (a + b)
9  rfl

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]

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]

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

1-- Navigate by pattern matching
2example (a b c : Nat) : a + (b + c) = a + (c + b) := by
3  conv =>
4    rhs
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]

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]

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-- Under forall
9example : (∀ x : Nat, x + 0 = x) ↔ (∀ x : Nat, x = x) := by
10  constructor
11  · intro h x
12    have := h x
13    simp at this
14    exact this
15  · intro _ x
16    simp

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

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

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