Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

帰納法の説明を修正し、丁寧にする #992

Merged
merged 1 commit into from
Oct 15, 2024
Merged

帰納法の説明を修正し、丁寧にする #992

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
29 changes: 17 additions & 12 deletions LeanByExample/Reference/Tactic/Induction.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,18 +2,22 @@

`induction` は、帰納法のためのタクティクです。

たとえば、Lean では自然数 `Nat` は
たとえば、Lean では自然数 `Nat` は以下のように定義されています。

* 0 は自然数
* `succ : Nat → Nat` という関数がある。つまり `n` が自然数ならば `succ n` も自然数
* `0` は自然数。
* `succ : Nat → Nat` という関数がある。つまり `n` が自然数ならば `succ n` も自然数。
* 上記のルールによって自然数だとわかるものだけが自然数。

というように帰納的に定義されています。このように帰納的に定義されたものに対して何か証明しようとしているとき、帰納法を使うことが自然な選択になります。
-/
import Mathlib.Tactic.Ring -- `ring` を使うため
このように、「既に `A` だとわかっているものから、`A` を作り出すルール」を定めることで `A` という概念を構成するというやり方を、**帰納的(inductive)** であるといいます。帰納的に定義されたものに対して何か証明しようとしているとき、帰納法を使うことが自然な選択になります。

典型的な例は、自然数に対する数学的帰納法です。前提として、ある述語 `P : Nat → Prop` に対して `∀ n, P n` を示そうとしているとします。このとき、以下を示せば十分であるというのが、数学的帰納法の主張です。

namespace Induction --#
* `P 0` が成り立つ。
* `∀ n, P n → P (n + 1)` が成り立つ。
-/
import Mathlib.Tactic.Ring -- `ring` を使うため --#

/-- `1` から `n` までの和を計算する関数 -/
/-- `0` から `n` までの和を計算する関数 -/
def sum (n : Nat) : Rat :=
match n with
| 0 => 0
Expand All @@ -29,14 +33,17 @@ example (n : Nat) : sum n = n * (n + 1) / 2 := by

-- `0` から `n` までの自然数で成り立つと仮定する
| succ n ih =>
-- 帰納法の仮定が手に入る
guard_hyp ih : sum n = n * (n + 1) / 2

-- `sum` の定義を展開し、帰納法の仮定を適用する
simp [sum, ih]

-- 後は可換環の性質から示せる
ring

/- ## 再帰定理
Lean では、実は帰納法を使用するのに必ずしも `induction` は必要ありません。場合分けの中で示されたケースを帰納法の仮定として使うことができます。これは recursive theorem(再帰定理) と呼ばれることがあります。[^recursive]
/- ## 再帰的定理
Lean では、実は帰納法を使用するのに必ずしも `induction` は必要ありません。場合分けの中で示されたケースを帰納法の仮定として使うことができます。これは recursive theorem(再帰的定理) と呼ばれることがあります。[^recursive]
-/

theorem sum_exp (n : Nat) : sum n = n * (n + 1) / 2 := by
Expand Down Expand Up @@ -179,8 +186,6 @@ def bar : Nat → Nat
#guard_msgs (drop warning) in --#
#check_failure bar.induct

end Induction --#

/-
[^recursive]: [lean公式ブログの Functional induction についての記事](https://lean-lang.org/blog/2024-5-17-functional-induction/) で recursive theorem という言葉が使われています。
-/