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

[Seasawher]

induction タクティクを使用したときにたまに起こるエラー。そもそも何を言っているのか？

theorem while_congr {B : State → Prop} {c c' : Stmt} {s t : State} (h : c ≈ c') (h_while : (whileDo B c, s) ==> t) :
    (whileDo B c', s) ==> t := by
  -- `whileDo B C` を `x` とおく
  -- TODO: この generalize がないと次の induction がエラーになるのはなぜか？
  -- generalize hx : whileDo B c = x at h_while

  -- `h_while` に関する帰納法を使う
  -- `h_while` は BigStep のコンストラクタのどこかから来るが、
  -- `hx` を使うと `while_true` または `while_false` から来ていることが結論できる
  induction h_while <;> cases hx

  -- 条件式が偽の場合
  case while_false s' hcond =>
    apply BigStep.while_false
    assumption

  -- 条件式が真の場合
  case while_true s' t' u' hcond' hbody' _ _hrest ih =>
    apply BigStep.while_true (t := t') (hcond := by assumption)

    case hbody =>
      -- `c ≈ c'` を使って rw することができる！（知らなかった）
      rw [← h]
      assumption

    -- 帰納法の仮定を使う
    case hrest => simpa using ih

[spinylobster]

"index in target's type" は型族についている添字(Natに限りません)ことなので、それが変数じゃない、ってことでしょうね。
以下のコードでも同じエラーが出ました。

inductive PNat : Nat → Prop where
  | zero : PNat 0
  | succ (h : PNat n) : PNat (n + 1)

example (h : PNat 0) : PNat 1 := by
  induction h
  sorry

[Seasawher]

このコードでも再現できる。(よく見たら当然だが…)

/--  偶数であることを表す帰納的述語 -/
inductive Even : Nat → Prop where
  | zero : Even 0
  | succ : Even n → Even (n + 2)

example (h : Even 0) : True := by
  /- 
  index in target's type is not a variable (consider using the `cases` tactic instead)
  0
  -/
  induction h

example (h : Even 0) : True := by
  generalize 0 = x at h  
  induction h
  · trivial
  · trivial  

example (n m : Nat) (h : Even (n + m)) : True := by
  /- 
  index in target's type is not a variable (consider using the `cases` tactic instead)
  n + m
  -/
  induction h

  case zero =>
    trivial

  case succ n ih =>
    
    trivial