Merge pull request #11 from lean-ja/strong-induction

強い帰納法に言及する
lean-ja · Oct 8, 2023 · 0aeb356 · 0aeb356
2 parents e946162 + 7918204
commit 0aeb356
Show file tree

Hide file tree

Showing 2 changed files with 30 additions and 0 deletions.
diff --git a/Examples/Induction.lean b/Examples/Induction.lean
@@ -41,3 +41,19 @@ example (n : Nat) : 0 < fac n := by
   · simp [fac]
     positivity
 -- ANCHOR_END: dash
+
+
+-- ANCHOR: strong
+variable (P : Nat → Prop)
+
+example (n : Nat) : P n := by
+  -- `n` についての強い帰納法で示す
+  induction' n using Nat.strong_induction_on with n ih
+
+  -- 仮定が追加される
+  guard_hyp ih : ∀ (m : ℕ), m < n → P m
+
+  match n with
+  | 0 => sorry
+  | k + 1 => sorry
+-- ANCHOR_END: strong
diff --git a/src/induction.md b/src/induction.md
@@ -30,3 +30,17 @@ needs: `import Mathlib.Tactic.Cases`
 ```lean
 {{#include ../Examples/Induction.lean:dash}}
 ```
+
+## 強い帰納法
+
+時には，より強い帰納法が必要なこともあります．強い帰納法とは，たとえば
+
+* `P(0)` を示す
+* `(∀ k < n, P (k)) → P (n)` を示す
+* したがって `∀ n, P (n)` である
+
+という形式で表されるような帰納法のことです．これは超限帰納法の特別な場合です．これを使用するには，`Nat.strong_induction_on` を使って次のようにします．
+
+```lean
+{{#include ../Examples/Induction.lean:strong}}
+```