Prove in List subtypes, idxOf Subtype = idxOf Subtype.val

Stream: new members

[An Qi Zhang]

Hello, I was wondering if there's a simple proof to show that if I have a list l of a subtype, and a list where I take the subtype values out of l, i.e. l.map (·.val), then the idxOf an element n of l is equal to the idxOf n.val of l.map (·.val)? I can't think of any obvious proof strategy here.

An example stated in Lean:

import Mathlib

def Nat.lt_ten (n : Nat) : Prop := n < 10

def N : Type := {n : Nat // n < 10}
deriving DecidableEq

example (l : List N) (n : N) : List.idxOf n l = List.idxOf n.val (l.map (·.val)) := by
  sorry

[Notification Bot]

An Qi Zhang has marked this topic as resolved.

[An Qi Zhang]

Nevermind, figured it out

[Kenny Lau]

(btw your N is called Fin 10)

[Notification Bot]

An Qi Zhang has marked this topic as unresolved.

[An Qi Zhang]

Actually, when I try to use the completed lemma, Lean complains about the subtype using idxOf Subtype.instBEq but Lean is expecting instBEqOfDecidableEq. Is there a way to use instBEqOfDecidableEq instead of the subtype's Subtype.instBEq?

Additionally, I'd also prefer not to make the subtype an instance of BEq, since that breaks other proofs expecting instBEqOfDecidableEq.

It looks like this right now:

import Mathlib

lemma List.idxOf_subtype_eq_idxOf_subtype_val {β : Type} {p : β → Prop} [DecidableEq β] [DecidableEq {x : β // p x}]
  (l : List {x : β // p x}) (n : {x : β // p x}) : idxOf n l = idxOf n.val (l.map (·.val)) := by
  sorry

def N : Type := {n : Nat // n < 10}
deriving DecidableEq

lemma List.test' (e : N) (l : List N) : idxOf e l = idxOf e.val (l.map (·.val)) := by
  have h := idxOf_subtype_eq_idxOf_subtype_val l e
  exact h

[Aaron Liu]

Just make it an abbrev

[An Qi Zhang]

is there a way without using abbrev? (using abbrev breaks other proofs)

[Aaron Liu]

make the DecidableEq defeq to the one from Subtype

[Robin Arnez]

Use [BEq β] [LawfulBEq β]

[Robin Arnez]

instead of [DecidableEq β] [DecidableEq {x : β // p x}]

[Robin Arnez]

Or wait for lean#8309 :-)

[Robin Arnez]

And deriving BEq, LawfulBEq, DecidableEq for N probably