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

2026年10月26日 17:39

🐺賢狼:

📖 Lean 4・Mathlib TIPS #002

`Nat` と `Int` — 引き算が変わると証明も変わる

本日は自然数 `ℕ` と整数 `ℤ` の違いを学ぶのじゃ。数学では同じ記号 $a-b$ を使うが、Lean では 型によって減算の性質が異なる。これは数論の形式化で重要な基礎知識じゃよ。

1. 自然数の減算は切り詰められる

自然数では負の数を表現できぬ。そのため、

$3-5=0$

となる。一方、整数では $3-5=-2$ じゃ。

import Mathlib

#eval (3 : ℕ) - 5   -- 0
#eval (3 : ℤ) - 5   -- -2

#check Nat.sub_add_cancel
#check Nat.add_sub_cancel
#check sub_add_cancel

`Nat.sub_add_cancel` は、自然数において

$b\le a\implies (a-b)+b=a$

を保証する補題じゃ。

2. 同じ等式を証明してみよう

import Mathlib

-- 自然数では大小関係が必要
example (a b : ℕ) (h : b ≤ a) :
    a - b + b = a := by
  exact Nat.sub_add_cancel h

-- 整数では無条件に成立
example (a b : ℤ) :
    a - b + b = a := by
  exact sub_add_cancel a b

整数では加法逆元が存在するため、

$a-b=a+(-b)$

と解釈できる。自然数には一般に加法逆元が存在しないので、同じ操作はできぬ。

3. 型クラスから理解する

`ℕ` は `Semiring` のインスタンスを持つが、`Ring` ではない。

`ℤ` は `Ring`、さらに `CommRing` のインスタンスを持つ。

import Mathlib

#synth Semiring ℕ
#synth CommSemiring ℕ
#synth Ring ℤ
#synth CommRing ℤ

`#synth` は指定した型クラスのインスタンスを Lean に探索させるコマンドじゃ。

`Ring ℕ` を要求すると失敗する。自然数には加法逆元がないからじゃな。

4. `omega` と `ring` の使い分け

import Mathlib

example (a b : ℕ) (h : b ≤ a) :
    a - b + b = a := by
  omega

example (a b : ℤ) :
    (a + b) * (a - b) = a^2 - b^2 := by
  ring

`omega` は自然数・整数の線形算術と大小関係を扱うのが得意。

`ring` は多項式の恒等式を正規化するのが得意じゃ。

ただし、`omega` は一般の変数同士の乗算を扱う万能な非線形算術ソルバーではない。

5. 本日の要点

自然数の減算には大小関係が関わり、整数の減算には加法逆元が関わる。

`Nat.sub_add_cancel` と `sub_add_cancel` の違いは、単なる補題名の違いではなく、背後にある代数構造の違いなのじゃ。

DkMath で自然数の差分や GN 多項式を扱う際にも、まず演算対象が `ℕ` なのか `ℤ` なのかを確認すると、証明戦略が立てやすくなるぞ。🐺

前回

2026/10/26 17:38　初稿

#LEAN #Lean4 #Mathlib #LEAN_TIPS