From 7cca6d753632919148bb4e584cbfaccbbda1dbdc Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 19 May 2026 06:30:39 +0000 Subject: [PATCH 1/2] Initial plan From e5b93567437481bfc095bcf80efc8f58da74a177 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 19 May 2026 06:46:59 +0000 Subject: [PATCH 2/2] docs: add termination_by example where rfl and decide fail Agent-Logs-Url: https://github.com/lean-ja/lean-by-example/sessions/06275766-93cb-4539-a56f-36abb4b035e6 Co-authored-by: Seasawher <47292598+Seasawher@users.noreply.github.com> --- LeanByExample/Modifier/TerminationBy.lean | 32 +++++++++++++++++++++++ 1 file changed, 32 insertions(+) diff --git a/LeanByExample/Modifier/TerminationBy.lean b/LeanByExample/Modifier/TerminationBy.lean index b2187dfd..c2177b60 100644 --- a/LeanByExample/Modifier/TerminationBy.lean +++ b/LeanByExample/Modifier/TerminationBy.lean @@ -134,6 +134,38 @@ def div (x y : Nat) : Nat := #guard div 10 3 = 3 +/- `termination_by` を使った定義は整礎再帰として扱われるため、同じ計算をする関数であっても +`rfl` や `decide` で示せなくなることがあります。 -/ + +/-- 文字列の左側を指定文字で埋めて、指定長にそろえる（整礎再帰バージョン）-/ +def String.padLeftWF (input : String) (padChar : Char) (length : Nat) : String := + if input.length ≥ length then + input + else + String.padLeftWF (padChar.toString ++ input) padChar length +termination_by length - input.length + +example : String.padLeftWF "42" '0' 5 = "00042" := by + -- 整礎再帰として定義された関数は定義展開されないので `rfl` では示せない + fail_if_success rfl + + -- `decide` でも示せない + fail_if_success decide + + native_decide + +/-- 文字列の左側を指定文字で埋めて、指定長にそろえる（非再帰バージョン）-/ +def String.padLeftSimple (input : String) (padChar : Char) (length : Nat) : String := + if input.length ≥ length then + input + else + let padding : String := String.pushn "" padChar (length - input.length) + padding ++ input + +example : String.padLeftSimple "42" '0' 5 = "00042" := by + -- こちらは単なる式展開だけで `rfl` が通る + rfl + /- ## 帰納法と整礎再帰 Lean では関数と証明項の間に大きな違いはないため、`termination_by` を再帰関数ではなくて `theorem` に対して使うこともできます。この場合、「再帰のたびに小さくなる指標」は「帰納法のステップごとに大きくなっていく指標」に相当します。これを利用することにより、証明の中で複雑な帰納法を書くことができます。