Computable Fin Induction

Stream: mathlib4

[zbatt]

I was attempting to port Data.Fin.VecNotation.lean and I noticed that many Fin definitions were marked noncomputable. I traced it back to Fin.induction which was using induction' which is not suported by the compiler yet. If you change the definition to

def induction {C : Fin (n + 1) → Sort _} (h0 : C 0)
    (hs : ∀ i : Fin n, C (castSucc i) → C i.succ) :
    ∀ i : Fin (n + 1), C i :=
  fun ⟨i, hi⟩ => by cases i with
  | zero => rwa [Fin.mk_zero]
  | succ i => exact hs ⟨i, lt_of_succ_lt_succ hi⟩ (Fin.induction h0 hs ⟨i, lt_of_succ_lt hi⟩)
#align fin.induction Fin.induction

it works computably!
Because of this, a couple of previously noncomputable definitions that relied on Fin.induction can be made computable. I guess my questions are is there a reason this was left uncomputable, and if not, should I PR this change along with removing noncomputable tags where possible?

[Mario Carneiro]

I don't think we want to optimize this yet, as it depends on the work on the new compiler. A change in the definition could cause breakage in mathlib due to different defeqs

[Mario Carneiro]

One way to get the best of both worlds would be to use your definition as Fin.inductionImpl and then use @[implemented_by Fin.inductionImpl] on Fin.induction, without changing the definition

[Mario Carneiro]

but ultimately we want the original definition to Just Work

[Kevin Buzzard]

I'm surprised this is called induction when it's doing recursion (ie constructing data). Is it ever used to construct data in mathlib? Probably.

[zbatt]

Mario Carneiro said:

One way to get the best of both worlds would be to use your definition as Fin.inductionImpl and then use @[implemented_by Fin.inductionImpl] on Fin.induction, without changing the definition

Sounds good! I'll implement this with a porting note and PR it a bit later today

[Eric Wieser]

(deleted)