fin induction principle

Stream: new members

[Yakov Pechersky]

I have a helper induction principle I like to use:

@[elab_as_eliminator] protected lemma fin.induction_on {n : ℕ} (i : fin (n + 1))
  {C : fin (n + 1) → Sort*}
  (h0 : C 0)
  (hs : ∀ i : fin n, C i.cast_succ → C i.succ) : C i :=
begin
  obtain ⟨i, hi⟩ := i,
  induction i with i IH,
  { rwa [fin.mk_zero] },
  { have : fin.succ ⟨i, nat.lt_of_succ_lt_succ hi⟩ = ⟨i.succ, hi⟩ := rfl,
    rw ←this,
    apply hs,
    apply IH }
end

Should that just be expressed as some version of fin.succ_rec_on?

[Yakov Pechersky]

Related, why does the cases tactic on fin n unfold the via the subtype defn as opposed to using fin.cases?

[Kevin Buzzard]

The reason cases does what it does is because it's some primitive tactic in core which is used to take apart inductive types according to their definitions, I'm not sure it can be modified to do what you want.