「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