Zulip Chat Archive

Stream: mathlib4

Topic: Computable Fin Induction


zbatt (Jan 18 2023 at 02:17):

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 (Jan 18 2023 at 07:47):

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 (Jan 18 2023 at 07:48):

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 (Jan 18 2023 at 07:48):

but ultimately we want the original definition to Just Work

Kevin Buzzard (Jan 18 2023 at 09:01):

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 (Jan 18 2023 at 14:27):

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 (Jan 18 2023 at 14:52):

(deleted)


Last updated: Dec 20 2023 at 11:08 UTC