Merge pull request #1064 from lean-ja/Seasawher/issue758

「index in target's type is not a variable」エラーはいつ起こるのか？

Author: Seasawher

LeanByExample/Reference/Tactic/Induction.lean

@@ -186,6 +186,35 @@ def bar : Nat → Nat
 #guard_msgs (drop warning) in --#
 #check_failure bar.induct
 
+/- ## よくあるエラー
+`induction` タクティクを使ったときに、`index in target's type is not a variable` というエラーが出ることがあります。
+-/
+
+/-- 偶数であることを表す帰納的述語 -/
+inductive MyEven : Nat → Prop where
+  | zero : MyEven 0
+  | succ : {n : Nat} → MyEven n → MyEven (n + 2)
+
+/--
+error: index in target's type is not a variable (consider using the `cases` tactic instead)
+  0
+-/
+#guard_msgs in
+  example (h : MyEven 0) : True := by
+    induction h
+
+/- これは型族の添え字が変数ではないから起こることです。その証拠に、変数にするとエラーにならなくなります。-/
+
+example (n m : Nat) (h : MyEven (n + m)) : True := by
+  /-
+  index in target's type is not a variable (consider using the `cases` tactic instead)
+  n + m
+  -/
+  generalize n + m = x at h
+  induction h
+  · trivial
+  · trivial
+
 /-
 [^recursive]: [lean公式ブログの Functional induction についての記事](https://lean-lang.org/blog/2024-5-17-functional-induction/) で recursive theorem という言葉が使われています。
 -/