Theorem Proving in Lean4 を読む会#2 ― 第2章 2.1-2.3

Theorem Proving in Lean 4 を読む会#2 2026/10/23 21:30~

今日の流れ 21:15～21:30：開場 21:30～22:30：勉強会 ● Theorem Proving in Lean 4 の2章を読む 勉強会終了後は雑談などご自由に ● 自由に退席OK

• https://leanprover.github.io/theorem_proving_in_lean4/

Theorem Proving in Lean 4 を読む

資料について この資料の作成者もLean学習中です。 資料はChatGPTを使用して原文の翻訳や概要を作ってからスライドにまとめています。 学習中のため、誤った説明や用語の使い方があるかもしれませんが、その際はご指摘 いただければと思います。

Leanの実行環境について ブラウザで動作する Lean Playground が手軽です ● おそらく、Theorem Proving in Lean 4 を読むだけならこれで完結できるはず ローカルにセットアップしたい場合は公式へ ● https://lean-lang.org/install/ ○ ● ● 公式ではVSCodeの拡張経由で入れる方法推奨とのこと VSCode拡張を経由しない場合：https://lean-lang.org/install/manual/ Dev Containerを使いたい場合は Mathlib を参考にするとよさそう ○ https://github.com/leanprover-community/mathlib4/tree/master/.devcontainer

• https://live.lean-lang.org/
• https://lean-lang.org/install/
• https://lean-lang.org/install/manual/
• https://github.com/leanprover-community/mathlib4/tree/master/.devcontainer

2. Dependent Type Theory

2. Dependent Type Theory（依存型理論）概要 依存型の話をがっつりするというよりは、Leanの書き方の入門をして、最後に依存型に 簡単に触れる章。 赤字の節を中心に解説。 2.1 Simple Type Theory：Leanの基本 2.2 Types as objects：概要だけ 2.3 Function Abstraction and Evaluation：Leanの基本 2.4 Definitions：Leanの基本 2.5 Local Definitions：Leanの基本 2.6 Variables and Sections：概要だけ 2.7 Namespaces：概要だけ 2.8 What makes dependent type theory dependent?：解説 2.9 Implicit Arguments：概要だけ

序文 （序文の日本語訳 by ChatGPT） 依存型理論（ dependent type theory）は、強力で表現力豊かな言語です。複雑な数 学的主張を表現したり、複雑なハードウェアやソフトウェアの仕様を記述したりできるだ けでなく、これらの両方について、自然で統一的な方法で推論することができます。 Leanは、Calculus of Constructions として知られる依存型理論の一種を基礎として います。そこに、可算な階層をなす非累積的なUniverseと、Inductive typeが組み合 わされています。 この章を終える頃には、これらの用語が意味することの多くを理解できるようになるで しょう。

序文の補足 キーワード 依存型（dependent type） ● 値によって型が変わる仕組み、2.8節で解説 Calculus of Constructions（CoC） ● 依存型理論の一種。LeanはCoCをベースに拡張した型理論を採用している。この勉強会では深入 りしません。 Universes ● Leanには型そのものにも型があり、その階層のこと。2.2節で少し解説。 Inductive types：帰納型 ● Nat や List などのデータ型を定義する仕組み。8章で詳しく扱う。

2.1 Simple Type Theory：Leanの基本 2.2 Types as objects：概要だけ 2.3 Function Abstraction and Evaluation：Leanの基本 2.4 Definitions：Leanの基本 2.5 Local Definitions：Leanの基本 2.6 Variables and Sections：概要だけ 2.7 Namespaces：概要だけ 2.8 What makes dependent type theory dependent?：解説 2.9 Implicit Arguments：概要だけ

2.1. Simple Type Theory 「型理論（Type theory）」 →すべての式（ expression）に、それに対応する型（ type）があることが由来 予約語・コマンド /- -/ 説明 コメントブロック、複数行可 -- 1行コメント def 新しい定数や定義を宣言する。例えば、 def m : Nat := 1 は値が1であるNat型の新しい定数mを定義している。 #check 型を調べるコマンド #eval 与えられた式を評価するコマンド ※Nat型：自然数（0以上の整数）を表す型

2.1. Simple Type Theory /- Define some constants. -/ def m : Nat := 1 変数 変数の型 -- m is a natural number 値 def b1 : Bool := true -- b1 is a Boolean /- Check their types. -/ #check m -- m : Nat /- Evaluate -/ #eval 5 * 4 -- 20

2.1. Simple Type Theory 単純型理論を強力にしているのは、既存の型から新しい型を構築できること 例： a と b が型なら、a → b は a から b への関数の型 ● ● イメージは「a型の引数をとって b型を返す」 関数 Pythonだと、def sample(x : a) b: … のイメージ a × b は a の要素と b の要素を組み合わせたペアの型 ● ● Pythonだとのタプルのイメージ、(1, “abc”): tuple[int, str] 直積（Cartesian product）とも呼ばれる

2.1. Simple Type Theory LeanはUnicode記号でコードを書くことができる 例： ● \times, \x → × ● \r, \to → すべて→になる ● ギリシャ文字もよく使う ○ \a, \b, \g → α, β, γ ● だいたいLaTeXの数学記号と対応している ● よく使う記号は決まっているので、全部覚えようとしなくてもOK

2.1. Simple Type Theory #check Nat → Nat -- Nat → Nat : Type #check Nat × Nat -- Nat × Nat : Type #check Nat → Nat → Nat #check Nat → (Nat → Nat) -- これは上と同じ。 →は右結合 #check Nat × Nat → Nat -- 直積を受け取って、 Natを返す関数 #check (Nat → Nat) → Nat -- 関数を受け取って、 Natを返す関数

2.1. Simple Type Theory 関数 f を値 x に適用することは、f x と書く。 例：Nat型に定義されたsucc関数とadd関数 #check Nat.succ -- Nat.succ (n : Nat) : Nat #check Nat.succ 2 -- Nat.succ 2 : Nat #check Nat.add -- Nat.add : Nat → Nat → Nat #check Nat.add 3 -- Nat.add 3 : Nat → Nat #check Nat.add 5 2 -- Nat.add 5 2 : Nat

2.1. Simple Type Theory Nat.add は、「自然数を 1つ受け取り、さらに自然数を 1つ受け取って自然数を返す 関数」と考えることができる。 型理論では、Nat.add を「自然数のペアを入力として受け取り、自然数を返す関数 」 と考えるよりも、この形のほうが一般に便利。 キーワード：カリー化、部分適用 例：Nat.add 3の型はNat → Nat。つまり、Nat.add 3は2つ目の引数である n を 「待っている」関数を返す。Nat.add 3 nと書くことと同じ。

2.1. Simple Type Theory 直積は(m, n)のように書ける。 m : Nat, n : Natなら、(m, n)の型はNat ×Nat。 直積の値p : Nat × Natがある場合、p.1, p.2でそれぞれの値を取り出 すことができる。

2.1 Simple Type Theory：Leanの基本 2.2 Types as objects：概要だけ 2.3 Function Abstraction and Evaluation：Leanの基本 2.4 Definitions：Leanの基本 2.5 Local Definitions：Leanの基本 2.6 Variables and Sections：概要だけ 2.7 Namespaces：概要だけ 2.8 What makes dependent type theory dependent?：解説 2.9 Implicit Arguments：概要だけ

2.2. Types as objects LeanのUniverseについて説明している節。 いきなり読むと難しいので簡単にまとめ： 「Leanでは型も第一級オブジェクトであり、型にも型がある。 ※第一級オブジェクト：代入や演算、変数への受 け渡しなどの基本的な操作ができる対象 そのため、型を分類するために Universe という仕組みがある」 以下のようなイメージ： Nat : Type – Nat の型は Type (Type 0 の省略形) Type : Type 1 – Type の型は Type 1 Type 1 : Type 2 – Type 1 の型は Type 2 … Universe にはレベル（Universe level）があり、Type 0、Type 1、Type 2、…という階層（Universe hierarchy）を 形成している。 Nat や Bool などの基本的な型は Type 0 (Type) に属する。

2.2. Types as objects （本文にはない補足） 型の階層は無限に続く。 ただし、Universeは累積的ではないため、あるUniverseに属する型が、自動的により上位の Universeにも属するわけではない。 例： def OK : Type := Nat def NG : Type 1 := Nat -- Nat は Type なのではこれはOK -- Nat は Type 1 に属さないのでエラー

2.1 Simple Type Theory：Leanの基本 2.2 Types as objects：概要だけ 2.3 Function Abstraction and Evaluation：Leanの基本 2.4 Definitions：Leanの基本 2.5 Local Definitions：Leanの基本 2.6 Variables and Sections：概要だけ 2.7 Namespaces：概要だけ 2.8 What makes dependent type theory dependent?：解説 2.9 Implicit Arguments：概要だけ

2.3. Function Abstraction and Evaluation 概要#1 ラムダ計算 で扱うような、関数を作る・適用する操作をLeanでもできる、という節。 ざっくりイメージ ● ● ラムダ計算は「ラムダ抽象」 と「関数適用」 がある ○ ラムダ抽象 ≒ 関数 ○ 関数適用 ≒ 関数に引数を渡す 例：関数 f に引数 1を渡す（≒適用する）とき、f 1とかく -- ラムダ抽象：引数 x を受け取り、x + 5 を返す関数を作る fun (x : Nat) => x + 5 -- 関数適用：上の関数に 10 を渡すと 15 になる #eval (fun (x : Nat) => x + 5) 10

• https://ja.wikipedia.org/wiki/ラムダ計算

2.3. Function Abstraction and Evaluation 概要#2 ほかの言語にあるラムダ式（っぽいやつも含めて）とイメージは似てる。 ● ● ● ● python: lambda x, y: x + y JavaScript(ES6~): (x, y) => x + y Java(8~): (x, y) -> x + y C#: (x, y) => x + y こうした構文は、名前を付けずに関数を作る方法の一つ。 まずは、 ● ● 関数を作る≒ラムダ抽象 関数に引数を渡す≒関数適用 というイメージをつかめばOK。

2.3. Function Abstraction and Evaluation Leanで fun または λ キーワードを使って、式から関数を作ることができる。 式から型が推論できる場合は、その型を省略できる。 引数を渡すことで関数を評価（≒計算）できる。 別の式から関数を作ることを、 ラムダ抽象（ lambda abstraction）と呼ぶ。 #check fun (x : Nat) => x + 5 -- fun x => x + 5 : Nat → Nat -- λ を使って書いても同じ #check λ (x : Nat) => x + 5 -- fun x => x + 5 : Nat → Nat -- 5を足すことから、 Leanがxの型を推論してくれるので Natを省略できる #check fun x => x + 5 #eval (λ x : Nat => x + 5) 10 -- 結果：15

2.3. Function Abstraction and Evaluation -- if 式の例 #check fun x : Nat => fun y : Bool => if not y then x + 1 else x + 2 -- 引数は最初にまとめて書ける #check fun (x : Nat) (y : Bool) => if not y then x + 1 else x + 2 -- 引数の型は式から推論できるなら省略できる #check fun x y => if not y then x + 1 else x + 2

2.3. Function Abstraction and Evaluation def f (n : Nat) : String := toString n def g (s : String) : Bool := s.length > 0 #check fun x : Nat => x -- 恒等関数：引数をそのまま返す関数 #check fun x : Nat => true -- 定数関数：引数に関係なく定数を返す関数 #check fun x : Nat => g (f x) -- 関数合成 g・f #check fun x => g (f x) g f Nat String Bool

2.3. Function Abstraction and Evaluation -- 関数も引数として渡せる #check fun (g : String → Bool) (f : Nat → String) (x : Nat) => g (f x) g・f g f Nat String Bool -- 型も引数として渡せる #check fun (α β γ : Type) (g : β → γ) (f : α → β) (x : α) => g (f x) g・f g f α β γ

2.3. Function Abstraction and Evaluation ラムダ式の一般形： fun (x : α) => t 束縛変数（ bound variable）： ● ラムダ式の一般系の変数 x のこと。そのスコープは式 t の外側には影響しない。 α同値（ alpha equivalent）： ● ● ● 束縛変数の名前を変更しただけで同じになる式 例：fun (b : β) (x : α) => b と fun (u : β) (z : α) => u は束縛変数名が変わっただけで同じなので α同値 Leanはこの同値性を認識する

2.3. Function Abstraction and Evaluation Leanでは、項（term）は簡約できる。 例えば、(fun x => x + 1) 2 は関数適用によって 3 になる。 このように、項を 簡約して、これ以上簡約できない形にすることを 正規化（ normalization）という。 また、同じ値に簡約される 2つの項 のことを、定義的に等しい（ definitionally equal）と呼ぶ。 Leanの型チェッカーは、この性質を利用して、項や型が同じものとして扱えるかどうかを判断する。 ※項：値、型、式などを表すもの ※簡約：項を規則に従って別の形に変形すること

本日はここまで

次回 10/30(金) 21:30~22:30 基本的に、毎週金曜 21:30~22:30 に実施 次回は2.4節から