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.

[Violeta Hernández]

Well, this is still an issue.

[Violeta Hernández]

Could we just remove docs#List.le from core? This is very misleading in the case where α is something like a preorder. Besides, we can literally just write ¬ y < x if that is what we want.

[Violeta Hernández]

@Yaël Dillies

[Yaël Dillies]

I agree, but I have no power over this

[Violeta Hernández]

I'd PR this myself but last time I tried making a core PR I made a total mess

[Kim Morrison]

No, there definitely needs to be an LE instance in core.

[Violeta Hernández]

Why?

[Violeta Hernández]

Talking about lexicographic ≤ only really makes sense in the context of a linear order. If we mean x = y or x < y or not y < x, I think that should be made explicit.

[Yury G. Kudryashov]

1. Currently, Mathlib instance is defined for linear orders only. We can fix the diamond by changing the le field.
2. If we care about partial orders (or preorders), then we can define an inductive predicate similar to List.Lex so that it gives the right answer in these cases.

[Violeta Hernández]

1. Is there any simple mechanism for changing just the order def-eqs? Or would we have to do the entire instance from the ground up?
2. Does such a definition exist? In my experience when I've had to prove theorems about lexicographic ≤ it ends up being easier restating them as one or the two alternatives I gave.

[Wrenna Robson]

Kim Morrison said:

No, there definitely needs to be an LE instance in core.

Incidentally, presumably that LE instance could use LE.ofLT to make it...

[Wrenna Robson]

Anyway: it looks like the LE instances here are defined as, for x <= y, as
x = y ∨ List.Lex x y fun a b => (a < b) (Mathlib one) and ¬ List.Lex y x fun a b => (a < b) (core one).

[Wrenna Robson]

I am a bit bemused as to why core uses the latter when it only really makes sense in a total order.

[Kim Morrison]

From memory it would be quite a big change to switch to the Mathlib one in lean4. I'm open to someone investigating, however.

[Wrenna Robson]

It might be simpler to have some kind of typeclass restriction?

[Kim Morrison]

I'm not that keen on having typeclass restrictions for this sort of thing. It might make sense for verification users, but it's annoying for programming applications to have to provide these "useless" typeclass instances for a new type you define.

[Floris van Doorn]

Yury G. Kudryashov said:

1. Currently, Mathlib instance is defined for linear orders only. We can fix the diamond by changing the le field.

I think this is the best short-term fix.
And probably we should wait with fixing the definition of List.le for partial orders until someone has a good use case for it.

[Floris van Doorn]

Violeta Hernández said:

1. Is there any simple mechanism for changing just the order def-eqs? Or would we have to do the entire instance from the ground up?

This is not hard. You just define the Mathlib LinearOrder instance so that it uses the existing LE instance. It does require you to prove the axioms for a LinearOrder, but that shouldn't be hard (perhaps you can even reuse the existing proof if you first show that the two orders are equivalent).

[Violeta Hernández]

sure, my question was moreso whether there's some LinearOrder.copy or similar constructor that allows easily changing the def-eqs

[Aaron Liu]

not yet