induction' の使用例を追加

lean-ja · Oct 26, 2023 · 11d1352 · 11d1352
1 parent c719cf9
commit 11d1352
Show file tree

Hide file tree

Showing 2 changed files with 35 additions and 5 deletions.
diff --git a/Examples/Induction.lean b/Examples/Induction.lean
@@ -1,6 +1,4 @@
--- `induction'` のために必要
-import Mathlib.Tactic.Cases
-
+import Mathlib.Tactic.Cases -- `induction'` のために必要
 import Mathlib.Tactic.Positivity
 
 namespace Examples
@@ -42,6 +40,30 @@ example (n : Nat) : 0 < fac n := by
     positivity
 -- ANCHOR_END: dash
 
+variable (α : Type)
+
+-- ANCHOR: induction_on_length
+example (l : List α) (P : List α → Prop) : P l := by
+  -- リストの長さに対する帰納法
+  induction' h : l.length generalizing l
+
+  case zero =>
+    -- リストの長さが 0 のとき
+    guard_hyp h: List.length l = 0
+
+    show P l
+    sorry
+
+  case succ n IH =>
+    -- リストの長さが `n + 1` のとき
+    guard_hyp h: List.length l = n + 1
+
+    -- 帰納法の仮定が使える
+    guard_hyp IH: ∀ (l : List α), List.length l = n → P l
+
+    show P l
+    sorry
+-- ANCHOR_END: induction_on_length
 
 -- ANCHOR: strong
 variable (P : Nat → Prop)
@@ -56,4 +78,4 @@ example (n : Nat) : P n := by
   match n with
   | 0 => sorry
   | k + 1 => sorry
--- ANCHOR_END: strong
+-- ANCHOR_END: strong
diff --git a/src/induction.md b/src/induction.md
@@ -31,7 +31,15 @@ needs: `import Mathlib.Tactic.Cases`
 {{#include ../Examples/Induction.lean:dash}}
 ```
 
-## 強い帰納法
+### 一般の～についての帰納法
+
+また，`induction'` では「リストの長さに対する帰納法」のようなより複雑な帰納法を行うことができます．
+
+```lean
+{{#include ../Examples/Induction.lean:induction_on_length}}
+```
+
+### 強い帰納法
 
 時には，より強い帰納法が必要なこともあります．強い帰納法とは，たとえば