No Std.MaxOrEq Int instance, but yes Std.MinOrEq Int

Stream: lean4

[Ayhon]

I've noticed that Std.MaxOrEq Int is not synthetized by Lean, while Std.MinOrEq Int is.

I wonder if this is an issue with the class instance not being synthetized correctly.

MWE

#synth Std.MinEqOr Int -- ✅

#synth Std.MaxEqOr Int -- ❌

[Eric Wieser]

Adding

instance [LinearOrder α] : Std.LawfulOrderSup α where
  max_le_iff _ _ _ := max_le_iff

instance [LinearOrder α] : Std.LawfulOrderInf α where
  le_min_iff _ _ _ := le_min_iff

to mathlib seems to fix it (#34471)

[Eric Wieser]

Obviously this should also work without Mathlib imported, but we want the mathlib instances so that it works for an arbitrary linear order too.

[Markus Himmel]

Thank you for the report, we're also fixing this in core: lean4#12181.

[Eric Wieser]

Should those be LawfulOrderInf instances instead?

[Eric Wieser]

Ah no, I guess there are some instance loops here

[Eric Wieser]

Which instance should mathlib prefer to provide from LinearOrder?

[Markus Himmel]

I don't think it matters since in the presence of Std.IsLinearOrder and DecidableLE all of the conditions on max become equivalent. One option would be to use docs#Std.LawfulOrderLeftLeaningMin.of_eq, which should be easy to obtain from LinearOrder.