Lean4: 「ゼロより大きい自然数はゼロでない」当たり前を数学証明的に書くとは？

Lean コードを読む

0 より大きい自然数は 0 ではないことを表す補題

lemma ne_zero_of_gt {n : ℕ} (hn : 0 < n) : n ≠ 0 := by
  intro h; rw [h] at hn; exact Nat.not_lt_zero 0 hn

• lemma := 補題

• ne := Not Equal

• zero := 0 is Zero

• of := 前置詞の「of」が名詞の前に置かれ、「〜の」「〜から」「〜の一部」といった意味で、所有、所属、構成、原因などを表す最も一般的な表現。つまり、このあとに続くものを指す。

• gt := Great ＜ ｛後に続くこっち側が大きいとする命名｝

• ここまでが補題である事と解りやすい命名

• {n : $${\N}$$} := 自然数 $${n}$$

• (hn : $${0 < n}$$) := Have $${0 < n}$$ n は ゼロよりも大きい事を条件指定して持ってるとする。

• `:` 記号までが前提

• $${n \ne 0}$$ := だから n はゼロじゃない。

• `:=` を定義する。

• by := それは、以下により証明する。

という感じで書かれる。始めての時は、これがさっぱり読めなかった。

#Lean の命名規約的な表現は、こういうのが多いので覚えていくしか無い。が、大体は $${\LaTeX}$$ 略記マクロなので数式を書いてる人にはそこそこ馴染み深い。

この自明な事なのに、複雑な記述構造を読む

#Lean4 #証明 に関係するコードを以下に抜き出した。

以下はコアライブラリのコード組み込まれている。

/--
Non-strict, or weak, inequality of natural numbers, usually accessed via the `≤` operator.
-/
protected inductive Nat.le (n : Nat) : Nat → Prop
  /-- Non-strict inequality is reflexive: `n ≤ n` -/
  | refl     : Nat.le n n
  /-- If `n ≤ m`, then `n ≤ m + 1`. -/
  | step {m} : Nat.le n m → Nat.le n (succ m)

instance instLENat : LE Nat where
  le := Nat.le

/--
Strict inequality of natural numbers, usually accessed via the `<` operator.

It is defined as `n < m = n + 1 ≤ m`.
-/
protected def Nat.lt (n m : Nat) : Prop :=
  Nat.le (succ n) m

instance instLTNat : LT Nat where
  lt := Nat.lt

theorem Nat.not_succ_le_zero : ∀ (n : Nat), LE.le (succ n) 0 → False
  | 0      => nofun
  | succ _ => nofun

theorem Nat.not_lt_zero (n : Nat) : Not (LT.lt n 0) :=
  not_succ_le_zero n

以下が、自分で書いた #命題 #補題
コアライブラリの Nat.not_lt_zero を利用して証明している。

/--
0 より大きい自然数は 0 ではないことを表す補題。

引数:
- `n : ℕ` — 自然数
- `hn : 0 < n` — `n` が正であるという仮定

説明:
`0 < n` という仮定から `n ≠ 0` を導く簡単な事実を記述する補題です。補題は証明や簡約（`simp`）に便利な形で利用されます。
-/
lemma ne_zero_of_gt {n : ℕ} (hn : 0 < n) : n ≠ 0 := by
  intro h; rw [h] at hn; exact Nat.not_lt_zero 0 hn

解説

lemma ne_zero_of_gt これを文系でも解る説明で教えて

うんうん、これは一見ちょっとまどろっこしく見えるけど、実は超基本的なことを形式的に書いてるだけだよ。文系の人にもわかるように、ふんわり優しく説明してみるね。

🍰 命題 ne_zero_of_gt の意味

lemma ne_zero_of_gt {n : ℕ} (hn : 0 < n) : n ≠ 0

これは自然数 n が「0より大きい（= 正の数）」なら、それは「0ではない」よね、ってだけの話。

🎓 たとえ話

🍎 リンゴの話でいうと：

「リンゴが1個以上あるなら、それは“ゼロ個ではない”よね？」

っていう、そりゃそうだろ的な当たり前のことを、数学的にちゃんと証明しましょう〜っていうのがこの補題。

🔬 Lean 的に何してる？

Lean は人間が「当たり前」と思うことも、ルールに基づいてキッチリ証明しないと納得してくれないの。

だからこの補題ではこうしてるよ：

lemma ne_zero_of_gt {n : ℕ} (hn : 0 < n) : n ≠ 0 := by
  intro h
  rw [h] at hn
  exact Nat.not_lt_zero 0 hn

🔍 一行ずつ解説：

1. intro h
   → 「じゃあ n = 0 だとして話を進めてみようか」って仮定する（背理法スタート）

2. rw [h] at hn
   → n を 0 だとすると、hn : 0 < n は 0 < 0 になる

3. exact Nat.not_lt_zero 0 hn
   → でも 0 < 0 は絶対に成り立たない（Nat.not_lt_zero という定理で証明済）
   → よって最初の仮定 n = 0 は間違い、つまり n ≠ 0

🧠 結論（要するに）

「正の自然数はゼロじゃない」って当たり前の話を、Lean 君にわかるように丁寧に分解して説明してるだけ！

この補題は、証明中で 0 < n っていう条件から n ≠ 0 を取り出すときに便利に使えるよ！

コアライブラリ theorem Nat.not_lt_zero からの読み解き。
Lean コード読解。どのように証明しているのか？

おっけー！じゃあ今度は、Nat.not_lt_zero が Lean のコアでどう定義・証明されているか を丁寧に読解していこう。

🎯 対象：Nat.not_lt_zero

theorem Nat.not_lt_zero (n : Nat) : ¬ (n < 0) :=
  Nat.not_succ_le_zero n

まずこれ、n < 0 は成り立たない（＝False）ことを言ってる。

そしてこの証明は、Nat.not_succ_le_zero n という定理に委ねているね。

🧩 Nat.not_succ_le_zero を見てみよう

theorem Nat.not_succ_le_zero : ∀ (n : Nat), LE.le (succ n) 0 → False
  | 0      => nofun
  | succ _ => nofun

定理名の意味：
succ n ≤ 0（n の次が 0 以下）なんてありえない！ってこと。

🔍 記号の整理

• succ n = n + 1

• LE.le は Nat.le、つまり ≤

なので、
n + 1 ≤ 0 なんてことはないよ！ という主張。

📚 Nat.le の定義（復習）

protected inductive Nat.le (n : Nat) : Nat → Prop
  | refl     : Nat.le n n
  | step {m} : Nat.le n m → Nat.le n (succ m)

n ≤ m を inductive に定義してる。

• refl（反射性）: n ≤ n

• step: n ≤ m なら n ≤ m + 1

つまり、n ≤ m は m を1ずつ増やしながら構成されるような定義。

🔍 Nat.not_succ_le_zero を精読！

theorem Nat.not_succ_le_zero : ∀ (n : Nat), Nat.le (succ n) 0 → False
  | 0      => nofun
  | succ _ => nofun

これは「どんな n でも、succ n ≤ 0 だったら False を返す」って形。

✅ なぜこれは正しいの？

• Nat.le (succ n) 0 を構成する方法が 存在しない から！

なぜなら：

• Nat.le の構成規則では、右側（m）が増えていく方向でしか作れない。

• でも succ n > 0 は必ず成り立つから、succ n ≤ 0 は 絶対に導出不可能！

だから Nat.le (succ n) 0 → False は 全体帰納法にすら入らず、直接 nofun（＝空の場合分け）で証明できる。

💥 nofun って何？

nofun は Lean における「不可能な場合分け」を処理するキーワード。
要するに、「この場合なんて来るわけないじゃん？」を明示的に表現してる。

この文脈では、succ n ≤ 0 を構成できる Nat.le のインスタンスは存在しないので、パターンマッチ不能。
よって nofun が使える。

🔁 まとめ：全体の流れ

1. Nat.lt n 0 は Nat.le (n + 1) 0 の別表記。

2. n + 1 ≤ 0 は 成り立ち得ない（Nat.le で構成不能）

3. よって Nat.lt n 0 は False

4. これを Nat.not_lt_zero が担っている。

5. その証明は Nat.not_succ_le_zero という空のパターンマッチで否定する定理を使ってる。

✏️ Lean 的な読みのコツ

• inductive 定義をしっかり理解すること（この場合 Nat.le）

• → False の証明には「構成不能性（空）」を活用する

• nofun は「該当パターンなし＝不可能性」の合図！

知ってしまえば納得のシンプルさだね！
他にも Lean の inductive 読解したい補題あったらどんどん持ってきて～！
📘💡

Nat.le, Nat.lt の定義構文の説明

いいねいいね、そこをしっかり押さえるのは Lean 証明の基本だから、
丁寧に見ていこう！

💡 まず最初に：Lean での順序関係定義

Lean（Core）では、自然数 ℕ 上の「小なり等しい」（≤）と「小なり」（<）は、論理構造から自分で定義しているの。

つまり：

• Nat.le は n ≤ m を「帰納的に」定義したもの

• Nat.lt はそれを使って「n < m := n+1 ≤ m」と定義したもの

🔸 Nat.le の定義構文

protected inductive Nat.le (n : Nat) : Nat → Prop
  | refl     : Nat.le n n
  | step {m} : Nat.le n m → Nat.le n (succ m)

🔍 解説：

これは inductive 型（帰納的な命題） の定義。

🔤 文法を分解すると：

パーツ と 意味

• inductive Nat.le (n : Nat) : Nat → Prop
  自然数 n を固定して、m : Nat に対して n ≤ m を命題として定義する。
  つまり Nat.le n m : Prop

• ` refl : Nat.le n n`

• ` step {m} : Nat.le n m → Nat.le n (succ m)`

🧠 これは何を言ってるの？

「n ≤ m」とは、m が n 以上であることを、n から m に向かって1つずつステップしていけるときに成り立つという構成的な定義！

つまり、例として：

• 2 ≤ 4 は
  2 ≤ 2 → 2 ≤ 3 → 2 ≤ 4 というステップを踏んで作れる。

🔹 Nat.lt の定義構文

protected def Nat.lt (n m : Nat) : Prop :=
  Nat.le (succ n) m

🔍 解説：

これは def による単なる定義の置き換え。

これは人間にもわかりやすい定義で、数学でもよくあるよね？

つまり：

• n < m を成立させたいなら、n + 1 ≤ m が証明できればOK。

• たとえば 2 < 5 は 3 ≤ 5 に帰着される。

🔧 まとめ：構文的ポイント

項目 → 構文・構造 → 解説

• inductive
  → 帰納的な命題（Prop）の定義 → データじゃなく「命題」を構築できる

• Nat.le n m : Prop
  →[$${n ≤ m}$$]である命題 → $${m}$$ に対して帰納的に構成される

• refl コンストラクタ
  → ベースケース $${n ≤ n}$$ → 自明な反射性

• step コンストラクタ
  → 帰納ステップ [$${n ≤ m → n ≤ m+1}$$] → 1つ上まで伸ばせる

• def による lt 定義
  →[$${n < m := n+1 ≤ m}$$] → 定義の糖衣。証明にもそのまま使える

💬 補足：Lean の流儀での構成的定義

Lean（というか type theory）では、「n ≤ m をどうやって構成（construct）するか」が大事なの。

この Nat.le の定義によって：

• 「本当に n ≤ m が成り立つなら、その構築手順（証明）」も手元にあるはず」

• 逆に、「構築できないなら n ≤ m は偽」という意味になる

つまり：

これが Lean の論理世界の基本だよ！

あとがき

やっぱり…めんどくさい。いや七面倒くさい言語だ😂（※数学言語世界も）
AI に任せよう（笑）

でもまあ、なんだろう？

やっぱりこれパズルゲームだね🎮️そっち系ゲーム好きは意外とハマるかも。そういう観点で遊んでみても良いかもしれない。それが何かの発見に繋がるかも？

定理 (theorem) は、無限に存在すると言われている。そんな数学定理構築のプロジェクト #Mathlib4 などだが、まだその数は数十万件しか無い。
無限には程遠い。ごく当たり前のことから、高難易度まであり幅広い。

そのうちの一つ。誰も書いてないパターンを書ければ、その積み上げに貢献しているのかもしれない。プロジェクトに参加せずとも、ネットの何処かに書き残せば良い。それをいつかは AI が覚えて活用してくれるだろう。✍️

2025/09/26 23:57

D.

Appendix

私と一緒に学ぼう！

GPTs

※あまり洗礼された教育はしていないので正しいコードは出力されません。