Question about FinEnum

Stream: mathlib4

[Ian Jauslin]

If I have a set A : Set Type u that is a finenum hA: FinEnum A, and I have an element of A: a : A, is it possible to access a+1 (the next item in the enumneration, wrapped periodically)?

[Kyle Miller]

I think you could do FinEnum.Equiv.symm (FinEnum.Equiv a + 1), since Fin has wraparound addition

[Ian Jauslin]

Thank you! I'm getting an error: failed to synthesize instance OfNat Does this mean I need to instantiate FinEnum somehow?

[Kyle Miller]

Oh, that's because it doesn't know that the cardinality of A isn't 0... Obviously it isn't because a witnesses that fact, but Lean doesn't know that 1 : Fin (FinEnum.card A) is ok

[Kyle Miller]

Here's a way to give it a hint:

import Mathlib.Data.FinEnum

def Fin.neZero_of (i : Fin n) : NeZero n := ⟨Nat.pos_iff_ne_zero.mp (Fin.pos i)⟩

def next [FinEnum α] (a : α) : α :=
  haveI := Fin.neZero_of (FinEnum.Equiv a)
  FinEnum.Equiv.symm (FinEnum.Equiv a + 1)

[Kyle Miller]

(haveI is a way to get Lean to subsitute in the expression where it's used, rather than the definition involving any extra let or fun)

[Ian Jauslin]

Thank you! Because A is Set Type u, I had to redefine next as

def next {A : Set α} (hA: FinEnum A) (a : A) : α :=
  haveI := Fin.neZero_of (hA.Equiv a)
  hA.Equiv.symm (hA.Equiv a + 1)

Does this make sense? Or is there an easier way to proceed that I am missing? (I am not sure at all that I am understanding FinEnum properly: I understood it as A is a set whose elements are of Type u, and A is a FinEnum.)

[Kyle Miller]

That's fine, it's that A coerced to a type is a FinEnum, though it's better to not name instance arguments.

def next {A : Set α} [FinEnum A] (a : A) : A :=
  haveI := Fin.neZero_of (FinEnum.Equiv a)
  FinEnum.Equiv.symm (FinEnum.Equiv a + 1)

It seems like if the expected type is α rather than (the coercion of) A then elaboration goes a little off the rails.

[Kyle Miller]

Here's a workaround if you do want to coerce the result from A to α

def next {A : Set α} [FinEnum A] (a : A) : α :=
  haveI := Fin.neZero_of (FinEnum.Equiv a)
  (FinEnum.Equiv.symm (FinEnum.Equiv a + 1) : A)

That's giving the elaborator a type hint so it can figure out which type FinEnum.Equiv is supposed to use.

[Ian Jauslin]

OK, that seems to work. Thank you so much!