DecidableEq causing type problem

Stream: new members

[Vivek Rajesh Joshi]

Why is there a type error here, and how do I resolve it?

import Mathlib.Data.Matrix.Notation

variable (M : Matrix (Fin m) (Fin n) Rat) (hm : m>0) (hn : n>0)

abbrev rowListofMat := List.map List.ofFn (List.ofFn M)

lemma rowListLength_eq_numRow : (rowListofMat M).length = m := by simp

lemma rowListofMat_elt_length_eq_numCol : ∀ i, ((rowListofMat M).get i).length = n := by simp

lemma rowLengthEq : ∀ i j, (List.ofFn (M i)).length = (List.ofFn (M j)).length := by simp

abbrev colListofMat := List.map List.ofFn (List.ofFn M.transpose)

lemma colListLength_eq_numCol : (colListofMat M).length = n := by simp

abbrev list_allZero (l : List Rat) : Bool := l.all (fun x => (x==0))

lemma nonzInRowList_imp_nonzInColList (h : ∃ r ∈ rowListofMat M, ¬list_allZero r) :
  ∃ c ∈ colListofMat M, ¬list_allZero c := by
  rcases h with ⟨row,row_rl,hrow⟩
  rw [List.all_eq_true] at hrow; push_neg at hrow
  rcases hrow with ⟨x,xrow,xn0⟩
  have : List.indexOf x row < (colListofMat M).length := by
    rw [colListLength_eq_numCol]
    have := List.indexOf_lt_length.mpr row_rl
    rw [←rowListofMat_elt_length_eq_numCol M ⟨(rowListofMat M).indexOf row,this⟩]

The error:

application type mismatch
  ⟨List.indexOf row (rowListofMat M), this⟩
argument
  this
has type
  @List.indexOf (List ℚ) instBEqOfDecidableEq row (rowListofMat M) < (rowListofMat M).length : Prop
but is expected to have type
  @List.indexOf (List ℚ) List.instBEq row (rowListofMat M) < (rowListofMat M).length : Prop

[Eric Wieser]

This looks like the LawfulBEq / DecidableEq diamond that I'm struggling to find the tracking issue for

[Eric Wieser]

The issue is:

example {α} [DecidableEq α] : (instBEqOfDecidableEq : BEq (List α)) = List.instBEq :=
  rfl -- fails

[Vivek Rajesh Joshi]

They do mean the same though, right?

[Vivek Rajesh Joshi]

How do I show that to Lean?

[Eric Wieser]

Ah, lean4#2038 is the tracking PR

[Vivek Rajesh Joshi]

I'm kinda new to all this DecidableEq, Beq and InstBeq stuff, can you explain what is going on here?

[Eric Wieser]

I think the best advice for now is to avoid == as much as possible when using Mathlib (by changing to abbrev list_allZero (l : List Rat) : Prop := ∀ x ∈ l, x = 0)

[Vivek Rajesh Joshi]

Okay, but how do I resolve the difference between the type of this and the expected type in the code above?

[Eric Wieser]

by convert this fixes it

[Eric Wieser]

But ultimately this is really a lean bug

[Vivek Rajesh Joshi]

Okay, thanks!