Index from List membership?

Stream: Is there code for X?

[Scott Morrison]

Any suggestions for

def idx_of_mem' [DecidableEq α] (xs : List α) (w : y ∈ xs) :
    { i : Nat // xs.get? i = some y } := by

I can probably get there by bashing at List.findIdx? for a bit, but it seems awkward.

[Scott Morrison]

Done, but it doesn't fit in the margin here... Still curious if anyone sees something less icky.

[Kayla Thomas]

List.mem_iff_get? ?

[Kayla Thomas]

Not sure if this is what you are looking for. Kind of hacked at it.

def idx_of_mem' {α : Type} [DecidableEq α] (y : α) (xs : List α) (w : y ∈ xs) :
    { i : Nat // xs.get? i = some y } := by
    simp only [List.mem_iff_get?] at w
    exact Encodable.chooseX w

[Kayla Thomas]

Added y as a param.

[Scott Morrison]

Ah, nice. I'd use Nat.find and Nat.find_spec as they are less deeply embedded in Mathlib than Encodable.chooseX.

[Kayla Thomas]

Cool. I just did an apply? and it gave me the last line :)

[Eric Wieser]

Would it be better to return the element of Fin xs.length here?

[Ioannis Konstantoulas]

Indeed, I would find the following more convenient:

def fidx_of_mem {α : Type} [DecidableEq α] (x : α) (xs : List α) (h : x ∈ xs) :
    {i : Fin xs.length // xs[i] = x} :=
  sorry

I don't see any shortcuts on how to write this function compared to Kayla's suggestion, though.