From 113fba8235c3c66780933ea38acfc773bf45d051 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Thu, 30 May 2024 02:44:07 +0900
Subject: [PATCH] =?UTF-8?q?noncomputable=20=E3=82=92=E7=B4=B9=E4=BB=8B?=
 =?UTF-8?q?=E3=81=99=E3=82=8B?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Src/Noncomputable.lean | 61 ++++++++++++++++++++++++++++++++++++++++++
 md/SUMMARY.md          |  1 +
 2 files changed, 62 insertions(+)
 create mode 100644 Src/Noncomputable.lean

diff --git a/Src/Noncomputable.lean b/Src/Noncomputable.lean
new file mode 100644
index 0000000..cef224d
--- /dev/null
+++ b/Src/Noncomputable.lean
@@ -0,0 +1,61 @@
+/- # noncomputable
+`noncomputable` は，宣言された関数が計算可能でないことを Lean に伝えるために使われます．
+
+Lean は，`def` で定義された関数はすべて計算可能であると想定しています．したがって，計算可能でない関数を定義すると，エラーが発生します．
+
+計算可能でない関数が生じるのは，選択原理 `Classical.choice` を使用したときです．選択原理は，型が「空ではない」という証明だけから，その型の項を魔法のように構成できると主張している公理です．空ではないという情報から具体的な項の情報は得られないため，選択原理を使用した関数は計算不能になります．
+-/
+
+variable {X Y : Type}
+
+-- 写像 `f : X → Y` が全射であること
+def Surjective (f : X → Y) : Prop := ∀ y, ∃ x, f x = y
+
+-- 全射な関数の逆写像を構成する
+-- しかし，全射という情報だけからは逆写像を具体的に作ることはできないので，
+-- 計算不能になりエラーになってしまう
+/--
+error: failed to compile definition, consider marking it as 'noncomputable'
+because it depends on 'Classical.choice', and it does not have executable code
+-/
+#guard_msgs in def inverse' (f : X → Y) (hf : Surjective f) : Y → X := by
+  -- `y : Y` が与えられたとする
+  intro y
+
+  -- `f` は全射なので `{x // f x = y}` は空ではない
+  have : Nonempty {x // f x = y} := by
+    let ⟨x, hx⟩ := hf y
+    exact ⟨⟨x, hx⟩⟩
+
+  -- 選択原理を用いて，`f x = y` なる `x : X` を構成する
+  have x := Classical.choice this
+  exact x.val
+
+-- `noncomputable` という修飾子を付ければ，エラーは回避できる
+noncomputable def inverse (f : X → Y) (hf : Surjective f) : Y → X := by
+  intro y
+
+  have : Nonempty {x // f x = y} := by
+    let ⟨x, hx⟩ := hf y
+    exact ⟨⟨x, hx⟩⟩
+
+  have x := Classical.choice this
+  exact x.val
+
+/- `noncomputable` とマークされた式を含む式は文字通り評価不能になり，`#eval` に渡すことができなくなります．-/
+
+-- 補助として `id` という恒等写像が全射であることを示しておく
+theorem id_surjective : Surjective (id : Nat → Nat) := by
+  intro y
+  exists y
+
+-- `id` の逆写像を構成する
+#check inverse (id : Nat → Nat) id_surjective
+
+-- 逆写像の `3` での値を評価しようとするとエラーになる
+/--
+error: failed to compile definition, consider marking it as 'noncomputable'
+because it depends on 'inverse', and it does not have executable code
+-/
+#guard_msgs in
+#eval inverse (id : Nat → Nat) id_surjective 3
diff --git a/md/SUMMARY.md b/md/SUMMARY.md
index 28dc735..68cf080 100644
--- a/md/SUMMARY.md
+++ b/md/SUMMARY.md
@@ -38,6 +38,7 @@
 * [partial: 再帰関数の停止証明をしない](./build/Partial.md)
 * [private: 定義を不可視にする](./build/Private.md)
 * [protected: フルネームを強制する](./build/Protected.md)
+* [noncomputable: 計算不能な関数を定義](./build/Noncomputable.md)
 
 # 型