Linear Preorders and LawfulOrderMin

Stream: Is there code for X?

[Wrenna Robson]

We seem to lack the following.

instance [LE α] [Std.IsPreorder α] [Std.Total (α := α) (· ≤ ·)] : Std.IsLinearPreorder α where
  le_total := Std.Total.total

instance [Min α] [LE α] [Std.LawfulOrderMin α] [Std.Refl (α := α) (· ≤ ·)] :
    Std.Total (α := α) (· ≤ ·) where
  total a b := by
    have := Std.LawfulOrderInf.le_min_iff b
    have := Std.LawfulOrderInf.le_min_iff a
    have := Std.MinEqOr.min_eq_or a b
    have := Std.Refl.refl (r := (· ≤ ·)) a
    have := Std.Refl.refl (r := (· ≤ ·)) b
    grind

This allows one to infer as follows:

instance [Min α] [LE α] [Std.LawfulOrderMin α] [Std.IsPreorder α] :
    Std.IsLinearPreorder α := inferInstance

This inference is stated in the docstring for Std.LawfulOrderMin but - as far as I can tell - never actually proved. Would these be a welcome PR?

[Wrenna Robson]

Also, in Mathlib, we appear to be missing these:

instance [LinearOrder A] : Std.LawfulOrderLeftLeaningMax A where
  max_eq_left := by grind
  max_eq_right := by grind

instance [LinearOrder A] : Std.LawfulOrderLeftLeaningMin A where
  min_eq_left := by grind
  min_eq_right := by grind

which then gives:

instance [LinearOrder A] : Std.LawfulOrderSup A := inferInstance

instance [LinearOrder A] : Std.LawfulOrderInf A := inferInstance

which we also don't have (but can infer from this).

[Wrenna Robson]

This is a particularly odd one to me: we don't seem to have this instance registered but nothing actually seems needed to do so:

instance [LinearOrder A] : Std.LawfulOrd A where

[Paul Reichert]

Thanks for your thoughtful proposal!

I omitted the first ones deliberately from the standard library. Automatically assembling weak instances into strong ones has its problems -- even for Prop-valued classes, I try to minimize the number of loops in the typeclass graph as I found performance to be sensitive to such changes. If a type is a linear order, IsLinearOrder needs to be provided explicitly, just like it is the case for LinearOrder in Mathlib.

Note that IsTotalPreorder.of_le is already able to create the first instance you proposed:

public theorem IsLinearPreorder.of_isPreorder_of_total {α : Type u} [LE α]
    [IsPreorder α] [Total (α := α) (· ≤ ·)] : IsLinearPreorder α := .of_le

With regard to the second, I'm sure there are lots of fine-grained hypotheses that imply some other low-level instance, but as long as there is no evidence of such a lemma being very profitable in actual code, I don't want to add all of this type class inference complexity to the library. I found type class inference to be a bad fit for multidirectional logical reasoning. When possible, the high-level typeclasses should be used and the API is optimized for that (and could be optimized further, perhaps).

Thanks for pointing out Std.LawfulOrderMin's docstring. I wanted to describe how that class logically relates to the others, but I should clarify that there is no instance for it. As written, it really sounds like there is an instance. I do think that a plain theorem would make sense for that, though.

[Wrenna Robson]

Thank you for the feedback. It's very much appreciated. Honestly the thing I find most confusing is the different approaches between Mathlib and Std to the order hierarchy - bundled or unbundled - which reaches its zenith with LinearOrder (which is like it is for a good reason, mind - and unbundling it seems an intimidating task).

[Wrenna Robson]

If an instance wasn't intended, then I do agree that the docstring could well be altered (and as you say perhaps one could have a theorem). I just want to make sure I'm writing theorems that are as tight as possible (that is, do not contain redundant assumptions). That's I think why I end up lower level than is perhaps intended.

[Paul Reichert]

The reason why Std takes a different approach than Mathlib is that the use cases are different. When writing programs, having good control over the data-carrying syntactical classes (LE, LT, Min, Ord, DecidableLE, ...) is important for efficiency, and it should be convenient to provide a linear order on whatever subset of these has been implemented -- without automatically providing inefficient implementations of the other ones. By unbundling, we promise ourselves more flexibility in this regard.

[Wrenna Robson]

That makes sense - I just often find myself wanting to do reasoning of a style that is more program-y but that needs to dip into MathLib.