Theorem Proving in Lean4 を読む会#3 ― 第2章 2.4-第3章 3.2

Theorem Proving in Lean 4 を読む会#3 2.4. Definitions ～ 3.2. Working with Propositions as Types 2026/10/30 21:30~

今日の流れ 21:15～21:30：開場 21:30～22:30：勉強会 ● Theorem Proving in Lean 4 の 2.4. Definitions から 勉強会終了後は雑談などご自由に ● 自由に退席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.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.4. Definitions def キーワードで、新しい名前付きオブジェクトを宣言できる。 -- 関数の定義 def double (x : Nat) : Nat := x+x #eval double 3 -- 結果：6 -- 定数も def で定義できる def pi := 3.141592654

2.4. Definitions 関数の書き方いろいろ def double (x : Nat) : Nat := x+x -- 引数をまとめて書く例 def add (x y : Nat) := x+y -- 引数 x を書かない例 def double’ : Nat → Nat := fun x => x + x -- 引数を分けて書く例 def add (x : Nat) (y : Nat) := x+y -- 型推論できる場合は、型の宣言を省略できる def double’’ := fun x => x + x ※関数の型は明示的に書くこと推奨 。 自分の意図が明確になり、定義の右辺が指定した型と一致しない 場合には、Leanがエラーを報告してくれる。

2.4. Definitions def double (x : Nat) : Nat := x+x -- 関数もパラメータとして渡せる def doTwice (f : Nat → Nat) (x : Nat) : Nat := f (f x) #eval doTwice double 2 -- 結果：8 -- 任意の2つの関数を合成する関数、ラムダ式の節でも扱ったもの def compose (α β γ : Type) (g : β → γ) (f : α → β) (x : α) : γ := g (f x) g・f g f α β γ

2.4. Definitions Leanは基本的に、定義された名前と、その定義を展開した式を同じものとして扱う 。た だし、すべての状況で名前が展開されるわけではない。 （本文では Nat と Natural の例があるが省略） def を使って名前を定義した場合、その名前は半簡約可能（ semireducible）と呼ばれ る性質を持つ。 Leanは、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.5. Local Definitions Leanでは、let キーワードを使って「ローカルな」定義を導入できる。 let a := t1; t2 はt2 に含まれる a の出現箇所をすべて t1 に置き換えた結果の式と、定義的に等しい。 #check let y := 2 + 2; y * y > let y := 2 + 2; > y * y : Nat #eval let y := 2 + 2; y * y > 16 def twice_double (x : Nat) : Nat := let y := x + x; y * y #eval twice_double 2 > 16 ここで、twice_double x は、(x + x) * (x + x) と定義的に等しい。

2.5. Local Definitions 複数の代入を組み合わせるには、let 文を連続して記述する。 #check let y := 2 + 2; let z := y + y; z * z > let y := 2 + 2; > let z := y + y; > z * z : Nat #eval let y := 2 + 2; let z := y + y; z * z > 64 改行を使う場合は、; を省略できる。 def t (x : Nat) : Nat := let y := x + x y*y

2.5. Local Definitions 以下の2つは似ているが同じ意味ではないことに注意。 1. 2. let a := t1; t2 (fun a => t2) t1 1つ目は、t2 に含まれる a の各出現箇所を、t1 に置き換える構文上の略記。 2つ目の a は変数のため、fun a => t2 という式は、a の値にかかわらず型チェックできなければならない。 つまり、let a := t1; t2 の形では表現できても、(fun a => t2) t1 の形では表現できない式が存在する。 例： def foo := let a := Nat; fun x : a => x + 2 /def bar := (fun a => fun x : a => x + 2) Nat -/ 次のスライドで bar がダメな理由を解説

2.5. Local Definitions 以下の2つは似ているが同じ意味ではないことに注意。 1. 2. let a := t1; t2 (fun a => t2) t1 1つ目は、t2 に含まれる a の各出現箇所を、t1 に置き換える構文上の略記。 2つ目の a は変数のため、fun a => t2 という式は、a の値にかかわらず型チェックできなければならない。 つまり、let a := t1; t2 の形では表現できても、(fun a => t2) t1 の形では表現できない式が存在する。 例： def foo := let a := Nat; fun x : a => x + 2 foo の a はlet構文の略記なので、 Nat に置き換えて型チェックできる /def bar := (fun a => fun x : a => x + 2) Nat -/ ラムダ式の引数 a は変数なので、関数本体が任意の a に対して型チェックできる 必要がある。しかし、任意の型の値に 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.6. Variables and Sections variable コマンド：宣言をまとめられる。任意の型の変数を宣言できる。この方法で宣言された変数は、作業中のファイルの末尾 までスコープ内に残る。 variable (α β γ : Type) variable (g : β → γ) (f : α → β) (h : α → α) variable (x : α) def compose := g (f x) def doTwice := h (h x) def doThrice := h (h (h x)) #print compose > def compose : (α β γ : Type) → (β → γ) → (α → β) → α → γ := > fun α β γ g f x => g (f x) #print doTwice > def doTwice : (α : Type) → (α → α) → α → α := > fun α h x => h (h x) #print doThrice > def doThrice : (α : Type) → (α → α) → α → α := > fun α h x => h (h (h x)) #printコマンド：定義した定数や関数などについて、Leanが 保持している定義の内容を表示するコマンド

2.6. Variables and Sections section ：変数のスコープを制限する。セクションを閉じると、その中で宣言された変数はスコープから外れ、 それ以降は参照できなくなる。セクションに名前を付けた場合は、同じ名前を使って閉じる必要あり。 section の 入れ子は可能。 section 内のインデントは不要。 section useful variable (α β γ : Type) variable (g : β → γ) (f : α → β) (h : α → α) variable (x : α) def compose := g (f x) def doTwice := h (h x) def doThrice := h (h (h x)) end useful

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.7. Namespaces namespace：定義をまとめる仕組み。section と異なり、名前が必須。 例：namespace Foo の外で Foo 内部の定義を使う場合、Foo.bar のようになる。 open：現在のコンテキストで、namespaceの名前を省略できる。 例：open Foo とすると、Foo.bar を現在のコンテキストで bar で使える。 一度閉じた namespace は、後から再び開くことが可能。 別のファイルで開き直すことも可能。

2.7. Namespaces namespace と section の使い分け ● ● namespace：定義などを整理するため section：定義に挿入する変数を宣言するため ○ set_option や open などのコマンドの適用範囲を区切るためにも役立つ 名前空間の内部で variable コマンドを使った場合、その変数のスコープは名前空間 の内部に限定されます。 同様に、名前空間の内部で open コマンドを使った場合、その効果は名前空間を閉じる と消える。

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.8. What makes dependent type theory dependent? 簡単な説明：型がパラメータに依存できる 。 例：List α は引数 α に依存していて、List Nat と List Bool は別の型。 例：Vector α n ：α 型の要素からなる、長さ n のベクトル（配列）型。 この型は、2つのパラメータに依存している。 ● ● ベクトルの要素の型である α : Type ベクトルの長さである n : Nat 2.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.9. Implicit Arguments 概要だけ解説。 例えば、次の関数を考える。 def ident (α : Type) (x : α) := x ident は、型 α と値 x を受け取り、x をそのまま返す関数。 #check ident Nat 10 > ident Nat 10 : Nat 型 α は、引数 x から推論できる場合がある。 そのため、型引数を暗黙の引数 にすれば、型を毎回指定せずに使える。

2.9. Implicit Arguments 引数 α を {α : Type} と書くと、暗黙の引数になる。 def ident {α : Type} (x : α) := x この定義では、α を明示的に渡す必要がない。 #check ident 10 > ident {α : Type} (x : α) : α Leanは 10 の型が Nat であることから、α = Nat と推論する。 ポイント ● ● (α : Type)：明示的な引数。呼び出し時に指定する {α : Type}：暗黙の引数。Leanが推論する ※ 暗黙の引数は、常に省略できるとは限らない。Leanが推論できない場合は、明示的に指定する必要 がある。

3. Propositions and Proofs

3. Propositions and Proofs 概要 「型は命題であり、その項は証明である」 という概念を理解するための章。証明という 名の型のパズル をするイメージ。最後の練習問題は解くと理解が深まるのでいくつか やってみることをおすすめします。 赤字は具体的な命題論理の話題。 3.1. Propositions as Types 3.2. Working with Propositions as Types 3.3. Propositional Logic 3.4. Introducing Auxiliary Subgoals 3.5. Classical Logic 3.6. Examples of Propositional Validities 3.7. Exercises

3.1. Propositions as Types 3.2. Working with Propositions as Types 3.3. Propositional Logic 3.4. Introducing Auxiliary Subgoals 3.5. Classical Logic 3.6. Examples of Propositional Validities 3.7. Exercises

3.1. Propositions as Types 概要 この節で言いたいことは本文最後のここ： To formally express a mathematical assertion in the language of dependent type theory, we need to exhibit a term p : Prop. To prove that assertion, we need to exhibit a term t : p. 訳）依存型理論の言語で数学的な主張を形式的に表現するには、項 p : Prop を提 示する必要がある。その主張を証明するには、項 t:p を提示する必要がある。 t:p t は p (命題)の証明 p : Prop は命題

3.1. Propositions as Types キーワード・ポイント ● ● ● ● ● ● axiom で公理を宣言、詳しくは3.2節 modus ponens（モーダスポネンス） ○ 論理学の推論規則 Curry-Howard isomorphism（カリー＝ハワード同型対応） ○ 証明とプログラムの間の対応関係のこと propositions-as-types ○ 命題を型として捉えるパラダイム 型 Prop は Sort 0 の糖衣構文 proof irrelevance（証明の無関連性） ○ 同じProp型の2つの証明は定義的に等しいものとして扱う

3.1. Propositions as Types 依存型言語に命題と証明を導入するたとえ話 ① 依存型理論は柔軟で表現力が高いため、主張と証明を同じ枠組みの中で表現できる。 たとえ話： ● ● ● ● 命題を表す型として Prop 型を作る p : Prop の証明を表す別の型 Proof p を作る Prop と Proof から公理（axiom）を作る 公理に加えてモーダスポネンスのような推論規則も導入する ○ Implies p q の証明と、p の証明があれば、 q の証明を得られる。 この方法によって、主張と証明を構築するための、妥当な仕組みを実現できる。すると、 式 t が主張 p の正しい証明であることを判定するには、単に t の型が Proof p で あることを確認すればよい （イメージは t : Proof p）。

3.1. Propositions as Types 依存型言語に命題と証明を導入するたとえ話 ② 式 t が主張 p の正しい証明であることを判定するには、単に t の型が Proof p で あることを確認すればよい （イメージは t : Proof p） これを簡略化 ● ● ● p : Prop のとき、Proof p と型 p は同じものとして扱う 項 t が 型 p を持つ、つまり t : p を「t が命題 p の証明である」 と読める さらに、含意(Implies)は関数型と同一視できる ○ p → q は、p の証明を受け取って q の証明を返す関数の型である。したがって、論理の含意に専 用の Implies を用意する必要はない。 自然演繹の証明体系における含意の規則が、関数の抽象化と適用を支配する規則に正確に対応しているとい う事実は、カリー＝ハワード同型対応（ Curry-Howard isomorphism）の一例である。これは 命題を型として 捉えるパラダイム（ propositions-as-types）とも呼ばれる。

3.1. Propositions as Types Prop 型の補足 ※糖衣構文（シンタックスシュガー）：プログラムの動作や意味を変えずに、 より短く、読み書きしやすく書き直された構文のこと Prop は Sort 0 の糖衣構文（シンタックスシュガー） ● ● Universe (2.2 Types as objects 参照)の階層のうち Sort 0 は一番低い階層 ほかの型のUniverseと同様に、→ の構成に関して閉じている ○ p q : Prop であれば、p→q : Prop ○ 勉強会での補足：q : Prop であれば p がどんな型でも、p→q : Prop Type u も Sort (u+1) の糖衣構文 本文にない補足： 「Sort 0 は命題を、 Sort 1 以上は通常のデータ型などを扱うための区別」 というイメージ

3.1. Propositions as Types 命題を型として捉える2つの方法 TPiLではこの2つの考え方を行き来しながら説明する ①論理や数学を構成的な立場から捉える場合 ● ● 命題 p は一種のデータ型を表しており、具体的には、証明を構成するデータの型を規定し ている。したがって、p の証明とは、適切な型を持つオブジェクト t:p にほかならない。 証明は抽象的な数学的オブジェクトであり、依存型理論の適切な式によって表現される と 考える。 ②単なる符号化のテクニックと捉える場合 ● ● それぞれの命題 p に対して、p が偽なら要素を持たず、真なら * という唯一の要素を持つ 型を対応づける（* は何か値があるという説明のための記号） 式を書き下し、それが正しい型を持つことを確認できるという事実によって、対象の命題が 真であることが保証される。言い換えれば、式そのものが証明。

3.1. Propositions as Types proof irrelevance（証明の無関連性） p : Prop が任意の命題であるとき、t1 t2:p である任意の 2つの要素を定義的に 等しいもの として扱う性質のこと ● ● (fun x => t) s と t[s/x] を定義的に等しいものとして扱うことに似ている Leanのカーネルはこの性質を使っている ※Leanのカーネル：証明が論理的に正しい かを最終確認するプログラム これは、依存型理論の言語において証明 t:p を通常のオブジェクトとして扱えるとして も、それらは p が真であるという事実を超える情報を持たないことを意味する。

3.1. Propositions as Types この節のまとめ 存型理論の言語で数学的な主張を形式的に表現するには、項 p : Prop を提示する 必要がある。その主張を証明するには、項 t:p を提示する必要がある。 t は p (命題)の証明 t:p p : Prop は命題 証明支援系としてのLeanの役割は、そのような項 t の構築を支援し、それが正しく形成 され、適切な型を持つことを検証することである。

3.1. Propositions as Types 3.2. Working with Propositions as Types 3.3. Propositional Logic 3.4. Introducing Auxiliary Subgoals 3.5. Classical Logic 3.6. Examples of Propositional Validities 3.7. Exercises

3.2. Working with Propositions as Types 概要 ● ● ● ● ● ● theorem の導入 → だけを含む定理の証明のやり方を説明 theorem と def の違い #print コマンドで実装を確認 show で示す命題（型）を先に宣言することができる axiom の説明

3.2. Working with Propositions as Types 補足：数学の公理、定義、定理、補題について 数学の用語 Leanで使う構文 証明の扱い 主な用途 公理 axiom 不要 証明せずに採用する命題 定義 def 不要 概念・関数・対象を定義する 定理 theorem 必要 採用した公理、定義、既知の定理などか ら証明された数学的な命題 補題 lemma または theorem 必要 別の定理を証明するために用いる命題 系 theorem または lemma 必要 既に証明された定理などから、比較的直 接的に導かれる命題 例 example 必要 名前を登録せずに証明を確認する Leanにおいては、theoremとlemmaは機能的には同じもの 。数学では定理と補題を使い分けるの で対応するように用意されている。第 3章では補題（lemma）は使わない

3.2. Working with Propositions as Types

theorem – 定理を導入する
「命題を型として扱う（propositions-as-types）」という考え方では、→ だけを含む定理
は、ラムダ抽象と関数適用を使って証明できる。
Leanでは、theorem コマンドによって新しい定理を導入する。
set_option linter.unusedVariables false
—
variable {p : Prop}
variable {q : Prop}
theorem t1 : p → q → p := fun hp : p => fun hq : q => hp
2章で扱った型が α→β→α である式 fun x:α=>fun y:β=>x と見たは同じだが、t1
は p q : Prop であり α, β のようなデータ型ではないことに注意。

3.2. Working with Propositions as Types theorem と def の違い – theorem は展開されない theorem は、実際には def の一種 ● 「命題と型の対応」に基づけば、定理 p→q→p を証明することは、対応する型の要素を定義する ことと同じである。カーネルの型チェッカーにとって、この2つに違いはない。 theorem にはあって def にない特徴 ● ● 通常、theorem の定義を展開する必要はない ○ 証明の無関連性 により、同じ定理の任意の2つの証明は定義的に等しいから 上記の性質を踏まえ、Leanは証明にirreducible（既約）という印を付ける ○ ファイルを処理する際、通常は証明の内部を展開する必要がないことを、パーサー（より 正確にはelaborator）に知らせるための手掛かりとなる

3.2. Working with Propositions as Types theorem と def の違い – セクション変数の扱いの違い def : 本体で参照されている変数は自動的にパラメータとして追加される theorem：定理の型で参照されている変数だけ 追加される ● 命題をどのように証明するかによって、証明対象である命題そのものが変わるべき ではないため

3.2. Working with Propositions as Types theorem と def の違い – セクション変数の具体例① def で本体にセクション変数が自動的に追加される例： section variable (α : Type) variable (defaultValue : α) def getDefault : α := defaultValue #check getDefault-- getDefault (α : Type) (defaultValue : α) : α #eval getDefault Nat 1 end

3.2. Working with Propositions as Types theorem と def の違い – セクション変数の具体例② theorem だと自動で追加されない例： 左の例を修正： section section variable (p q : Prop) variable (h : p) variable (p q : Prop) variable (h : p) theorem my_theorem : p := h end theorem my_theorem’ (h : p) : p := h #check (my_theorem') -- my_theorem' : ∀ (p : Prop), p → p end セクション変数で h を宣言しているから def の例 のように通るように思えるが、 hでUnknown identifier `h`エラーが出る。 つまり、theorem の場合は証明本体で使っている 変数は明示的に書かないといけない。

3.2. Working with Propositions as Types show の使い方 通常の書き方： show を使った書き方： set_option linter.unusedVariables false set_option linter.unusedVariables false variable {p : Prop} variable {q : Prop} variable {p : Prop} variable {q : Prop} theorem t1 : p → q → p := fun hp : p => fun hq : q => hp theorem t1 : p → q → p := fun hp : p => fun hq : q => show p from hp show 文を使って、最後の項 hp の型を明示的 に指定することができ、証明がわかりやすくな る。内部的には左の書き方と同じ項が生成され る。

3.2. Working with Propositions as Types 宣言した theorem の使い方と axiom の説明 set_option linter.unusedVariables false variable {p : Prop} variable {q : Prop} theorem t1 (hp : p) (hq : q) : p := hp axiom hp : p axiom は、指定した型の要素が存在するこ とを公理として仮定する。 定理 t1 は、通常の関数適用と同じように使 用できる theorem t2 : q → p := t1 hp hp : p という「公理」を宣言することは、hp が証拠となって、命題 p が真であると宣言 することに等しい。 p が真であるという事実を表す hp:p に定理 t1:p→q→p を適用すると、 定理 t1 hp:q→p が得られる。

3.2. Working with Propositions as Types axiom の注意点 axiom は論理の無矛盾性を損なう可能性がある。 例えば、空の型である False が要素を持つと仮定することもできてしまう。 axiom unsound : False -- Everything follows from false theorem ex : 1 = 0 := False.elim unsound

3.2. Working with Propositions as Types 定理の具体例① t1 を一般化すると、異なる命題の組に適用して、一般的な定理の異なる具体例を得られる。 theorem t1 (p q : Prop) (hp : p) (hq : q) : p := hp variable (p q r s : Prop) #check t1 p q > t1 p q : p → q → p #check t1 r s > t1 r s : r → s → r #check t1 (r → s) (s → r) > t1 (r → s) (s → r) : (r → s) → (s → r) → r → s variable (h : r → s) #check t1 (r → s) (s → r) h > t1 (r → s) (s → r) h : (s → r) → r → s

3.2. Working with Propositions as Types 定理の具体例② 前章で取り上げた合成関数を、今度はデータ型の代わりに命題を使って考える。 variable (p q r s : Prop) theorem t2 (h₁ : q → r) (h₂ : p → q) : p → r := fun h₃ : p => show r from h₁ (h₂ h₃) 命題論理の定理として、t2 は何を述べているだろうか？ ※h₁などの下付き番号文字は \0、\1、\2、… と入力して得られる

3.2. Working with Propositions as Types 定理の具体例②の補足 p→r variable (p q r s : Prop) q→r p→q p q r theorem t2 (h₁ : q → r) (h₂ : p → q) : p → r := fun h₃ : p => show r from h₁ (h₂ h₃) 「q → r と p → q が成り立つならば、 p → r が成り立つ 」 つまり、含意の推移性 を表す定理。 証明では、まず h₃ として p を仮定。すると h₂ h₃ によって q が得られ、さらに h₁ (h₂ h₃) によって r が得られる。

本日はここまで

次回 11/6(金) 21:30~22:30 基本的に、毎週金曜 21:30~22:30 に実施 次回は含意 (→)の証明の補足と 3.3節～演習問題まで 。