From 81b958d1f321dd624a2fe29968f9b2edefe7a094 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Wed, 20 May 2026 16:45:22 +0000 Subject: [PATCH 1/3] Initial plan From 6f2f03e7309d3ee27726c9df882c3e0e95e3a719 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Wed, 20 May 2026 17:09:47 +0000 Subject: [PATCH 2/3] docs: explain why partial_fixpoint preserves soundness Agent-Logs-Url: https://github.com/lean-ja/lean-by-example/sessions/5fb49daf-989b-4a16-9aab-db7643d94b3b Co-authored-by: Seasawher <47292598+Seasawher@users.noreply.github.com> --- LeanByExample/Modifier/PartialFixpoint.lean | 37 +++++++++++++++++++++ 1 file changed, 37 insertions(+) diff --git a/LeanByExample/Modifier/PartialFixpoint.lean b/LeanByExample/Modifier/PartialFixpoint.lean index 34e5868c..3781231d 100644 --- a/LeanByExample/Modifier/PartialFixpoint.lean +++ b/LeanByExample/Modifier/PartialFixpoint.lean @@ -39,6 +39,41 @@ example (f : Nat → Option α) (n : Nat) (h : (f n).isSome) : (searchF f n).isS grind | succ n ih => grind +/- +## なぜ `partial_fixpoint` では健全性が壊れないのか？ + +`partial_fixpoint` の要点は「停止しない可能性」を **定義上の簡約** ではなく **命題としての展開定理** で扱うところにあります。[^partial-fixpoint-ref] + +実際、`searchF` の本体は `rfl` では展開できず、`searchF.eq_def` という補題を使ってはじめて展開できます。 +-/ + +example (f : Nat → Option α) (n : Nat) : + searchF f n = (match f n with + | some _ => some n + | none => searchF f (n + 1)) := by + fail_if_success exact rfl + rw [searchF.eq_def] + +/- +そのため「`P` は `P` だから真」のような循環を定義上の簡約で作ることはできません。`partial_fixpoint` で得られるのは `Option` などのモナド上での部分正当性に限られます。たとえば次の関数は `n ≠ 0` のとき停止しない可能性がありますが、`False` を直接取り出すことはできません。 +-/ + +@[grind] def divergeOrNone (n : Nat) : Option False := + if n = 0 then + none + else + divergeOrNone (n + 1) +partial_fixpoint + +example : divergeOrNone 0 = none := by + rw [divergeOrNone.eq_def] + simp + +example (n : Nat) : (∃ p : False, divergeOrNone n = some p) → False := by + intro h + rcases h with ⟨p, _⟩ + exact False.elim p + /- ## 名前の由来 @@ -96,4 +131,6 @@ example (f : Nat → Nat) (h : f = factBody f) つまり、階乗関数を「`f = factBody f` を満たす `f`」として定義することができるというわけです。 ここで `f = factBody f` という等式をよく見ると、`f` が `factBody` という高階関数の不動点(fixpoint)であると主張していることがわかります。ここでは階乗関数を具体例にしましたが、一般に再帰関数は関数の不動点として捉えられることが知られています。`partial_fixpoint` の名前は、まさにこの「再帰関数は不動点である」という考え方に由来します。 + +[^partial-fixpoint-ref]: Lean 公式リファレンス「Recursive functions as partial fixpoints」「Partial functions with nonempty codomains」を参照： -/ From c23c747c13911b0f40025c0abe72c607b47651be Mon Sep 17 00:00:00 2001 From: Codex Date: Mon, 25 May 2026 02:39:28 +0900 Subject: [PATCH 3/3] fix: use Empty in partial_fixpoint example --- LeanByExample/Modifier/PartialFixpoint.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/LeanByExample/Modifier/PartialFixpoint.lean b/LeanByExample/Modifier/PartialFixpoint.lean index 3781231d..4d326f19 100644 --- a/LeanByExample/Modifier/PartialFixpoint.lean +++ b/LeanByExample/Modifier/PartialFixpoint.lean @@ -55,10 +55,10 @@ example (f : Nat → Option α) (n : Nat) : rw [searchF.eq_def] /- -そのため「`P` は `P` だから真」のような循環を定義上の簡約で作ることはできません。`partial_fixpoint` で得られるのは `Option` などのモナド上での部分正当性に限られます。たとえば次の関数は `n ≠ 0` のとき停止しない可能性がありますが、`False` を直接取り出すことはできません。 +そのため「`P` は `P` だから真」のような循環を定義上の簡約で作ることはできません。`partial_fixpoint` で得られるのは `Option` などのモナド上での部分正当性に限られます。たとえば次の関数は `n ≠ 0` のとき停止しない可能性がありますが、矛盾を表す `Empty` の値を直接取り出すことはできません。 -/ -@[grind] def divergeOrNone (n : Nat) : Option False := +@[grind] def divergeOrNone (n : Nat) : Option Empty := if n = 0 then none else @@ -69,10 +69,10 @@ example : divergeOrNone 0 = none := by rw [divergeOrNone.eq_def] simp -example (n : Nat) : (∃ p : False, divergeOrNone n = some p) → False := by +example (n : Nat) : (∃ p : Empty, divergeOrNone n = some p) → False := by intro h rcases h with ⟨p, _⟩ - exact False.elim p + exact Empty.elim p /- ## 名前の由来