From 591f277098de4a8fa7585d8c4a2fa03c9245cad8 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Wed, 20 May 2026 06:48:23 +0000
Subject: [PATCH 1/3] Initial plan


From 3e75d98ca07f9756afc74586cdf915253a01840c Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Wed, 20 May 2026 06:58:05 +0000
Subject: [PATCH 2/3] =?UTF-8?q?DecreasingBy:=20=E3=82=AB=E3=83=AA=E3=83=BC?=
 =?UTF-8?q?=E3=83=BB=E3=83=8F=E3=83=AF=E3=83=BC=E3=83=89=E5=90=8C=E5=9E=8B?=
 =?UTF-8?q?=E5=AF=BE=E5=BF=9C=E3=81=AE=E8=A6=B3=E7=82=B9=E3=81=8B=E3=82=89?=
 =?UTF-8?q?=E9=83=A8=E5=88=86=E9=96=A2=E6=95=B0=E7=A6=81=E6=AD=A2=E3=81=AE?=
 =?UTF-8?q?=E8=A3=9C=E8=B6=B3=E8=AA=AC=E6=98=8E=E3=82=92=E8=BF=BD=E5=8A=A0?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Agent-Logs-Url: https://github.com/lean-ja/lean-by-example/sessions/57612611-2497-4a6a-80a0-9b2a2d1c44f6

Co-authored-by: Seasawher <47292598+Seasawher@users.noreply.github.com>
---
 LeanByExample/Modifier/DecreasingBy.lean | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/LeanByExample/Modifier/DecreasingBy.lean b/LeanByExample/Modifier/DecreasingBy.lean
index 78e0c111..cb527d81 100644
--- a/LeanByExample/Modifier/DecreasingBy.lean
+++ b/LeanByExample/Modifier/DecreasingBy.lean
@@ -89,6 +89,14 @@ unsafe example : False := by
   have _ : Empty := anything
   contradiction
 
+/- なお、[カリー・ハワード同型対応](#{root}/Type/Prop.md#CH)の観点からも、部分関数が禁止される理由を説明できます。カリー・ハワード同型対応によれば「帰納法は再帰に対応する」ので、停止しない再帰関数を許すということは、終わらない帰納法を許すことになり、直接的に不健全な証明に繋がります。`unsafe` キーワードを使うと停止性のチェックが迂回されるため、証明においても無限再帰が使えるようになります。 -/
+
+-- unsafe を使うと、証明の中で無限再帰（= 終わらない帰納法）が使える
+unsafe def proofLoop (P : Prop) : P := proofLoop P
+
+-- その結果、False のような矛盾した命題でも「証明」できてしまう
+unsafe example : False := proofLoop False
+
 /-
 [^recursive]: ここで紹介している例は Joachim Breitner さんによる [Recursive definitions in Lean](https://lean-lang.org/blog/2024-1-11-recursive-definitions-in-lean/) というブログ記事から引用しています。
 -/

From 0f72bb24eb22aa40e53502420820ec09a54a8154 Mon Sep 17 00:00:00 2001
From: Seasawher <47292598+Seasawher@users.noreply.github.com>
Date: Wed, 27 May 2026 01:42:57 +0900
Subject: [PATCH 3/3] =?UTF-8?q?=E6=A0=A1=E6=AD=A3?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 LeanByExample/Modifier/DecreasingBy.lean | 24 +++++++++++++-----------
 1 file changed, 13 insertions(+), 11 deletions(-)

diff --git a/LeanByExample/Modifier/DecreasingBy.lean b/LeanByExample/Modifier/DecreasingBy.lean
index cb527d81..8baec5dd 100644
--- a/LeanByExample/Modifier/DecreasingBy.lean
+++ b/LeanByExample/Modifier/DecreasingBy.lean
@@ -36,7 +36,7 @@ def Nat.toListNat (n : Nat) : List Nat :=
     Nat.toListNat (n / 10) ++ [(n % 10)]
 
 end Hidden --#
-/- `decreasing_by` に続けて停止することの証明を与えれば Lean に受け入れられるようになります。再帰のたびに引数が真に減少し、無限に減少し続けないことを示せば十分です。 -/
+/- `decreasing_by` に続けて停止することの証明を与えれば Lean に受け入れられるようになります。再帰のたびに(無限には減少できない)引数が真に減少することを示せば十分です。 -/
 
 def Nat.toListNat (n : Nat) : List Nat :=
   if n == 0 then
@@ -68,11 +68,21 @@ end Have --#
 
 そもそもなぜ Lean では関数の停止性を示す必要があるのでしょうか？それは、Lean の論理体系の健全性を保つためです。[^recursive]
 
-例として、停止する保証がない関数を定義してみましょう。以下の関数は引数の数列の `f` がいつか `some` になる保証がないので、無限に計算が終わらない可能性があります。
+[カリー・ハワード同型対応](#{root}/Type/Prop.md#CH)によれば「帰納法は再帰」なので、停止しない再帰を許すことは直接的に「終了しない帰納法」を許すことに繋がり、矛盾をもたらすことになってしまいます。
+-/
+
+-- unsafe を使うと終わらない帰納法が使えるので、何でも証明できる
+unsafe def loop_thm (P : Prop) : P :=
+  loop_thm P
+
+unsafe example : False := loop_thm False
+
+/-
+定理ではなくて通常の関数の場合も、停止しない関数を野放図に許すと矛盾を導くことができます。例として、以下の「`Option` 値の点列から `some` であるようなものを探す関数」を考えてみましょう。この関数は引数の点列の `f` がいつか `some` になる保証がないので、無限に計算が終わらない可能性があります。
 -/
 variable {α : Type}
 
-/-- 数列 `f : Nat → Option α` が `some` を返すような最初の `f n` を返す -/
+/-- 点列 `f : Nat → Option α` が `some` を返すような最初の `f n` を返す -/
 unsafe def search (f : Nat → Option α) (start : Nat) : α :=
   match f start with
   | .some x => x
@@ -89,14 +99,6 @@ unsafe example : False := by
   have _ : Empty := anything
   contradiction
 
-/- なお、[カリー・ハワード同型対応](#{root}/Type/Prop.md#CH)の観点からも、部分関数が禁止される理由を説明できます。カリー・ハワード同型対応によれば「帰納法は再帰に対応する」ので、停止しない再帰関数を許すということは、終わらない帰納法を許すことになり、直接的に不健全な証明に繋がります。`unsafe` キーワードを使うと停止性のチェックが迂回されるため、証明においても無限再帰が使えるようになります。 -/
-
--- unsafe を使うと、証明の中で無限再帰（= 終わらない帰納法）が使える
-unsafe def proofLoop (P : Prop) : P := proofLoop P
-
--- その結果、False のような矛盾した命題でも「証明」できてしまう
-unsafe example : False := proofLoop False
-
 /-
 [^recursive]: ここで紹介している例は Joachim Breitner さんによる [Recursive definitions in Lean](https://lean-lang.org/blog/2024-1-11-recursive-definitions-in-lean/) というブログ記事から引用しています。
 -/