同値性のrwタクティクがわからない

３章の同値性まで読み進め中。現時点ではrwが一体なにをしているのか記述が浅くて理解できないので、AIに聞きながらconvというものを使って手作業で追いかけなおしてみる。
conv内部ではchangeで現在のフォーカスを明示的にソースに記録できるし、テストにもなる模様。

-- 3.1.5 同値性
namespace eq_rewrite
  example (f : ℕ → ℕ) (k : ℕ) (h₁ : f θ = θ) (h₂ : k = θ) : f k = θ := by
    show f k = θ
    rw [h₂]
    show f θ = θ
    rw [h₁]

  -- building a separate "tool" or fact (a₁) and then use that tool to finish
  -- the job.
  -- The main goal remains `f k = θ` until the very last line.
  example (f : ℕ → ℕ) (k : ℕ) (h₁ : f θ = θ) (h₂ : k = θ) : f k = θ := by
    have a₁ : f k = θ := by
      conv =>
        lhs
        change f k
        arg 1
        change k
        rw [h₂]
        change θ
      exact h₁
    show f k = θ
    exact a₁
    
  -- treating the main goal like a piece of clay, reshaping it until it becomes
  -- a trivial identity.
  -- The goal `f k = θ` is updated multiple times.
  example (f : ℕ → ℕ) (k : ℕ) (h₁ : f θ = θ) (h₂ : k = θ) : f k = θ := by
    show f k = θ
    conv =>
      -- When you enter conv mode, Lean shifts the focus. The pipe symbol in the
      -- InfoView indicates a congruence or focus state. It tells you:
      -- 1. Where you are: The expression to the right of the pipe is the specific
      --    part of the term you are currently targeting.
      -- 2. The Task: Your job isn't to "prove" this term is true, but to transform
      --    it into something else (usually to simplify it or prepare it for a
      --    specific rewrite).
      lhs
      change f k
      --^ The change tactic allows you to replace the term at the pipe with a
      --  definitionally equal term.
      arg 1
      change k
      rw [h₂]
      change θ
    show f θ = θ
    conv =>
      lhs
      change f θ
      rw [h₁]
      change θ

end eq_rewrite

TODO

読む: https://lean-lang.org/theorem_proving_in_lean4/The-Conversion-Tactic-Mode/

参考文献