Lean4: 000: 🐺賢狼のLean初級講座

第0回：`rw` の基本 — 結合法則と交換法則

Lean における `rw` は、等式による書き換え（rewrite）じゃ。

例えば、加法の結合法則は、

$$(a+b)+c=a+(b+c)$$

Mathlib では `add_assoc` という補題名で登録されておる。

import Mathlib

example (a b c : ℕ) :
    (a + b) + c = a + (b + c) := by
  rw [add_assoc]

example (a b : ℕ) :
    a + b = b + a := by
  rw [add_comm]

example (a b c : ℕ) :
    a * (b + c) = a * b + a * c := by
  rw [mul_add]

覚えておきたい基本補題

これらは同じ型クラス条件のもとでのみ使えるわけではない。例えば `mul_comm` は乗法が可換な場合に使えるが、一般の `Ring` の乗法は可換とは限らぬ。

逆方向への書き換え

rw [← add_assoc]

`←` を付けると、等式の右辺から左辺への書き換えになる。

また、

rw [add_comm a b]

のように引数を明示すれば、書き換え対象を絞り込める。

探索の小技

`#check` は型の表示、`#print` は宣言の詳細を調べるためのコマンドじゃ。

本日の要点： `rw` は計算を実行する命令ではなく、証明済みの等式を使って式を変形する操作なのじゃ。

そして、`add_assoc` などが使える理由は、対象の型に必要な代数構造のインスタンスが存在するためである。

ここが次回以降の `Semiring` や `Ring` の理解へつながるぞ。

参考：Mathematics in Lean — Basics

2026/10/21 12:21 初稿

D.

#LEAN #Lean4 #Mathlib #LEAN_TIPS

Appendix

Lean4Web