conv モード

conv モードは，ゴール全体ではなく，式の特定の部分に入り込んで書き換えるためのモードです． 通常の rw はゴール全体から書き換え場所を探します． 一方，conv では「左辺に入る」「第 1 引数に入る」のように場所を指定してから書き換えます．

example (a b c : Nat) : (a + b) + c = (b + a) + c := by
  conv =>
    lhs
    rw [Nat.add_comm a b]

conv => の中では lhs や rhs を使って，左辺・右辺を選べます．

example (a b c : Nat) : (a + b) + c = (b + a) + c := by
  conv =>
    lhs
    arg 1
    rw [Nat.add_comm a b]

上の例では，左辺 (a + b) + c に入り，さらに第 1 引数 a + b に入ってから，そこだけを交換しています． arg 1 は関数適用や演算の第 1 引数へ移動する指示です．

example (a b c : Nat) : (a + b) + (c + 0) = (a + b) + c := by
  conv =>
    lhs
    arg 2
    rw [Nat.add_zero]

conv の中でも simp を使えます． 式の一部だけを簡約したいときに便利です．

example (a b : Nat) : (fun x : Nat => x + b) a = a + b := by
  conv =>
    lhs
    simp

conv は強力ですが，構文が細かく，証明が読みにくくなることもあります． まずは通常の rw や simp を試し，書き換える場所を厳密に指定したいときに conv を使うのがよいです．

演習

conv を使って，ゴールの一部だけを書き換えてください．

example (a b c : Nat) : (a + b) + c = (b + a) + c := by
  -- ヒント:
  --   conv =>
  --     lhs
  --     rw [Nat.add_comm a b]
  sorry