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

📖 Lean 4・Mathlib TIPS #001

加法の三法則と `rw` — 型クラスから補題を探す

本日は、Mathlib の代数操作の基本中の基本、 結合法則・交換法則・左交換法則 じゃ。

数学では当たり前の式変形も、Lean では対応する定理を指定して書き換える。その代表が `rw`（rewrite）じゃな。

1. 覚えておきたい補題

特に `add_left_comm` は便利じゃ。加法の交換と結合を一度に行える。

2. Lean で実験

import Mathlib.Algebra.Ring.Defs

#check add_assoc
#check add_comm
#check add_left_comm
#check mul_add
#check add_mul

example {R : Type*} [Semiring R]
    (a b c : R) :
    (a + b) + c = b + (a + c) := by
  rw [add_assoc]
  rw [add_left_comm]

最初の `rw` で

$$(a+b)+c \longrightarrow a+(b+c)$$

次の `rw` で

$$a+(b+c) \longrightarrow b+(a+c)$$

となり、左右が一致して証明完了じゃ。

3. `[Semiring R]` とは何か？

`R : Type*` は型を表す変数。

`[Semiring R]` は、型 `R` が半環の構造を持つという型クラスの仮定じゃ。

半環には加法の交換・結合、乗法の結合、分配法則、零元、単位元などが備わる。

したがって Lean は、`R` の具体的な正体を知らなくても、これらの補題を利用できる。

ただし注意！

`Semiring` は乗法の交換法則を保証しない。

`rw [mul_comm]` を使いたいなら、例えば `[CommSemiring R]` が必要じゃ。

4. よくある失敗

`rw [add_comm]` は、意図しない部分式を交換してしまうことがある。

そんなときは、

rw [add_comm a b]

と、対象を具体的に指定するのじゃ。

さらに `rw` は基本的に指定した向きへ書き換える。逆向きに使う場合は、

rw [← add_assoc]

とする。

5. 補題を自力で調べる

`#check add_assoc` は定理の型を表示する。

`#print Semiring` は型クラスの定義を調べる入口になる。

公式資料：Mathlib.Algebra.Ring.Defs

ここには `Semiring`、`Ring` などの構造と、その継承関係が記載されておる。

本日の要点： `rw` の補題を覚えるだけでなく、どの型クラスがその法則を保証しているのかを意識すること。

これが後々、自然数から一般の環へ証明を拡張する際の大きな武器になるのじゃよ！ 🐺

前回

2026/10/23 1:09　初稿

D.

#LEAN #Lean4 #Mathlib #LEAN_TIPS