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
