Two `List.LE` instances?

Stream: mathlib4

[Violeta Hernández]

The latest version of Mathlib seems to have introduced an unfortunate phenomenon: there are now two instances docs#List.instLE and docs#List.LE', and they're not def-eq:

import Mathlib.Data.List.Lex

/-
type mismatch
  List.cons_le_cons_iff
has type
  @LE.le (List ?m.48) List.instLE (?m.55 :: ?m.57) (?m.56 :: ?m.58) ↔
    ?m.55 < ?m.56 ∨ ?m.55 = ?m.56 ∧ ?m.57 ≤ ?m.58 : Prop
but is expected to have type
  @LE.le (List ℕ) List.LE' (a :: l) (b :: m) ↔ a < b ∨ a = b ∧ l ≤ m : Prop
-/
example (a b : ℕ) (l m : List ℕ) : a :: l ≤ b :: m ↔ a < b ∨ a = b ∧ l ≤ m :=
  List.cons_le_cons_iff

[Violeta Hernández]

@Kim Morrison

[Violeta Hernández]

I think the fix is to set the correct def-eq in docs#List.instLinearOrder, and remove the docs#List.LE' override (along with docs#List.LT' while we're at it, though that's not problematic since both instances are def-eq)

[Violeta Hernández]

Although, I think a better fix might be not to define docs#List.le to begin with. It doesn't mean what you'd expect when the list type isn't linearly ordered, and when it is, we should probably go through the linear order instance instead.

[Violeta Hernández]

(While we're at it, something I find unfortunate with the new List.Lex file is that it uses the Std relation classes instead of those defined in Mathlib. Unifying these would be a worthwhile endeavor.)

[Violeta Hernández]

I've opened #21339 which provides a quick and dirty fix

[Eric Wieser]

I don't think we should touch the override instance in mathlib; rather, we should ensure any downstream instances are compatible with the override.

[Violeta Hernández]

Keeping the override makes any of the new List.le theorems in code unusable in Mathlib.

[Eric Wieser]

I think that's fine, don't we have all those theorems for List.Lex anyway?

[Violeta Hernández]

I think we upstreamed a lot of them to core. In fact, I updated my personal project to v4.16 precisely to be able to use these theorems (and ended up not being able to...)

[Violeta Hernández]

For instance I can't find Mathlib variants of docs#List.nil_le or docs#List.cons_le_cons_iff

[Violeta Hernández]

I'd like Kim to comment on this, I think they're the one who added List.le in the latest release.