帰納法を `induction` タクティクでやらない方が良いことがある例（通常とは異なる帰納法を使いたいとき）

variable {α : Type}

@[grind]
inductive EvenLength : List α → Prop
  | nil : EvenLength []
  | cons_cons {a b : α} {l : List α} (h : EvenLength l) :
    EvenLength (a :: b :: l)


theorem EvenLength_spec (xs : List α) : EvenLength xs ↔ xs.length % 2 = 0 := by
  fail_if_success try?
  fail_if_success induction xs with grind

  match xs with
  | [] => grind
  | [_] => grind
  | a :: b :: l =>
    -- 明示的に再帰を使って帰納法の仮定を得ることが有用
    have ih := EvenLength_spec l
    grind

def EvenLengthRec (xs : List α) : Prop :=
  match xs with
  | [] => True
  | [_] => False
  | _ :: _ :: l => EvenLengthRec l

example (xs : List α) : EvenLength xs ↔ xs.length % 2 = 0 := by
  induction xs using EvenLengthRec.induct with grind

Start with the supplied Lean snippet and inspect the repository’s existing code-example organization to determine where this example belongs. The work is done when the example explains why ordinary induction is unsuitable here, shows the recursive hypothesis approach and the EvenLengthRec.induct approach, and renders correctly with the surrounding examples.