Question about List.getElem_idxOf

Stream: new members

[Yongxi Lin (Aaron)]

I want to prove that if r is a list (of some subtype) and a is an element of r, then r[List.idxOf a r] = a. I failed because of a type class instance problem. May someone help me understand what I did wrong?

import Mathlib

open Set

variable {ι : Type*} {t : ι} [LinearOrder ι] {r : List (Iic t)} {a : Iic t} {mar : a ∈ r}

#check List.idxOf_lt_length_of_mem mar
#check List.getElem_idxOf (List.idxOf_lt_length_of_mem mar)

[Snir Broshi]

I believe the problem is that docs#List.getElem_idxOf requires [DecidableEq α] while docs#List.idxOf_lt_length_of_mem requires [BEq α].

There's a "diamond" in the typeclasses because Subtype is involved, which causes there to be two different instances of BEq:

• docs#Subtype.instBEq
• docs#Subtype.instDecidableEq + docs#instBEqOfDecidableEq

Apart from changing both theorems to use DecidableEq, or deleting docs#Subtype.instBEq, I don't know how to fix it.

[Snir Broshi]

But you can do Option.some_injective _ <| getElem?_pos .. |>.symm.trans <| List.getElem?_idxOf mar instead, it only uses DecidableEq

[Snir Broshi]

Also if you don't need to know the underlying type Iic t of the list for what you need from idxOf, you can prove lemmas with {α : Type*} [DecidableEq α] and use them from the part of the code that does know about Iic t.
E.g.:

import Mathlib

lemma List.getElem_idxOf_of_mem {α : Type*} [DecidableEq α] {l : List α} {a : α} (h : a ∈ l) :
    l[l.idxOf a]'(List.idxOf_lt_length_of_mem h) = a :=
  List.getElem_idxOf ..

open Set

variable {ι : Type*} {t : ι} [LinearOrder ι] {r : List (Iic t)} {a : Iic t} {mar : a ∈ r}

#check List.getElem_idxOf_of_mem mar

[Robin Arnez]

Snir Broshi schrieb:

Apart from changing both theorems to use DecidableEq, or deleting docs#Subtype.instBEq, I don't know how to fix it.

The real fix would be to make both theorems use [BEq α] [LawfulBEq α]

[Ruben Van de Velde]

I thought https://github.com/leanprover/lean4/pull/8309 was the real fix

[Robin Arnez]

Also that :-) But until then, you should use BEq + LawfulBEq when talking about functions that use BEq (and maybe even after then to help unification)

[Snir Broshi]

Robin Arnez said:

Also that :-) But until then, you should use BEq + LawfulBEq when talking about functions that use BEq (and maybe even after then to help unification)

So how should docs#List.getElem_idxOf / docs#List.idxOf_lt_length_of_mem be changed?

[Robin Arnez]

docs#List.idxOf_lt_length_of_mem is perfectly fine,
docs#List.getElem_idxOf, docs#List.idxOf_get, docs#List.getElem?_idxOf and docs#List.idxOf_inj should all take [BEq α] [LawfulBEq α] instead of [DecidableEq α]

[Snir Broshi]

Robin Arnez said:

docs#List.idxOf_lt_length_of_mem is perfectly fine,
docs#List.getElem_idxOf, docs#List.idxOf_get, docs#List.getElem?_idxOf and docs#List.idxOf_inj should all take [BEq α] [LawfulBEq α] instead of [DecidableEq α]

Is the eventual goal to deprecate DecidableEq?

[Robin Arnez]

No, DecidableEq is good and all but docs#List.idxOf has a BEq assumption, not a DecidableEq one