Request for feedback: new order typeclasses in std library

Stream: general

[Paul Reichert]

The standard library now provides typeclasses representing order structures
such as preorders, partial orders and linear orders. This post serves as a short introduction, but hopefully long enough that you feel qualified to give your opinion. I hope you like it, but now would be the best time to make adjustments if something was wrong with the design.

Given an LE α instance, there are a few new propositional typeclasses:

• IsLinearOrder α is the proposition that ≤ satisfies the axioms of a linear order.
• Similarly IsPreorder, IsLinearPreorder and IsPartialOrder.
• LawfulOrderLT is the proposition that LT α is "compatible" with LE α.
• LawfulOrderOrd is the proposition that Ord α is "compatible" with LE α.
• Similarly for BEq, Min and Max.

As you can see, everything is centered around LE -- I'll explain the reasons below.

More fine-grained instances such as Std.Antisymm remain. IsLinearOrder
entails many of them and lemmas are free to only require a few axioms for the sake of
generality if they do not need a full linear order.

The factories LinearOrderPackage.ofLE α or LinearOrderPackage.ofOrd α make it
convenient to provide LE α, LT α, Ord α, Min α, Max α, BEq α,
IsLinearOrder α and other useful instances.

For the motivation behind this design, see below -- but let us look at an example first.

Creating a linear order with as many operations as possible

You can try the following in Lean 4 Web on the latest nightly:

inductive Day where
  | mon | tue | wed | thu | fri | sat | sun

/-! Define *any* `Ord`, `TransOrd` and `LawfulEqOrd` instances on `Day`. -/

instance : Ord Day := sorry
instance : Std.TransOrd Day := sorry
instance : Std.LawfulEqOrd Day := sorry

/-!
Having defined `Ord`, let us automatically derive `LE`, `LT`, `Min`, `Max` and `BEq`
as well as typeclasses relating them.
-/


instance : Std.LinearOrderPackage Day := .ofOrd Day

/-!
Now we have all operations at our disposal and have enough lemmas to prove things about them:
-/

example (d₁ d₂ d₃ : Day) (h₁₂ : d₁ ≤ d₂) (h₂₃ : d₂ ≤ d₃) : d₁ ≤ d₃ :=
  Std.le_trans h₁₂ h₂₃

example (d₁ d₂ d₃ : Day) (h₁₂ : d₁ < d₂) (h₂₃ : d₂ ≤ d₃) : d₁ < d₃ :=
  Std.lt_of_lt_of_le h₁₂ h₂₃

example (d₁ d₂ : Day) : compare d₁ d₂ = .lt ↔ d₁ < d₂ :=
  Std.compare_eq_lt

The factory LinearOrderFactory.ofOrd uses auto-param magic to provide sensible defaults for all instances where possible. If it is not able to automatically derive some instance, it explains to the user in an error message what is missing and how to provide it manually. If any of the data-carrying instances (LT, LE, Min, ...) already exists, the factory will prefer the pre-existing one over generating a new one that might not be definitionally equal.

A good example for how to use the new classes in lemma signatures is List.min?_eq_some_iff. Its signature was:

theorem max?_eq_some_iff [Max α] [LE α] [anti : Std.Antisymm (· ≤ · : α → α → Prop)]
    (le_refl : ∀ a : α, a ≤ a)
    (max_eq_or : ∀ a b : α, max a b = a ∨ max a b = b)
    (max_le_iff : ∀ a b c : α, max b c ≤ a ↔ b ≤ a ∧ c ≤ a) {xs : List α} :
    xs.max? = some a ↔ a ∈ xs ∧ ∀ b ∈ xs, b ≤ a

Its new signature is:

theorem max?_eq_some_iff [Max α] [LE α] {xs : List α} [IsLinearOrder α]
    [LawfulOrderMax α] : xs.max? = some a ↔ a ∈ xs ∧ ∀ b, b ∈ xs → b ≤ a

Motivation

Previously, talking about linear orders using the standard library was tedious and
there was no unified way to do it. Different lemmas in the standard
library used seemingly different sets of hypotheses that were equivalent to
having a linear order.

There are multiple data-carrying typeclasses for different basic operations:
LE, LT, BEq, Ord, Min and Max.

One solution would be to use exactly the same approach like Mathlib, providing
typeclasses like LinearOrder which bundle all applicable operations and certain laws
about them.

But the standard library has different requirements than Mathlib.
Many programming tasks only require a few of these operations and it is desirable
for code to assume as few data-carrying instances as necessary.
It is also not always desirable to implement or generate all of them at once
because it is tedious and generating them automatically might produce inefficient
implementations that cannot easily be replaced downstream.
Even if some operations are (still) missing, it should be possible to talk about
linear orders.

The given design is a compromise: It requires an LE instance in order to say
what a linear order is, but other operations may or may not be present.

Another pain point is that it's tedious to construct linear orders and all instances
one may want for them. The LinearOrderPackage.of* factories make this more convenient.

Mathlib integration

Right now, IsLinearOrder (etc.) coexists independently from Mathlib's LinearOrder.

While the details need to be discussed, it should be relatively easy to make them compatible:

-- cannot cause diamonds because `IsLinearOrder α` is a proposition
instance [LinearOrder α] : IsLinearOrder α :=
  sorry -- translate Mathlib's formulation of the axioms

It might make sense to move lemmas such as Std.le_trans into the global
namespace, replacing the corresponding lemmas in Mathlib.

(EDIT: removed workaround in the example after nightly landed)

[Jovan Gerbscheid]

• I would have expected LawfulOrderLT to be called LawfulLT.
• Here's a controversial question: do you want to allow using max and min for partial orders? I see that there is Std.LawfulOrderInf (with min as the operator), so I guess the answer is yes.

[Paul Reichert]

I tend to think of LawfulClass as an intrinsic description when Class is to be considered lawful. However, LawfulOrderLT relates LT to the order data encoded in LE. Another option would be to call it LawfulLELT, but it doesn't convey the intent of the typeclass as well (and it looks weird). Also, LawfulBEq (another can of worms) already has a different meaning.

Regarding Min and Max, yes, that's a difficult question. Mathlib also chose to use min/max for partial orders (Prod.instMin_mathlib) and I believe it's the better choice: Practically, having a separate Inf class would require duplicating a lot of the API. But agreed that it can be misleading that it's called min and not inf!

[Kim Morrison]

I'd had the same thought about LawfulLT, and I think I'd still be in favour of this rename. I appreciate the point about it being a less principled name, but nevertheless less surprising.

[Wrenna Robson]

I think I was having a conversation just the other day about how nice it would be to make a similar change in Mathlib... it would be great if that happened, I feel.

[Wrenna Robson]

So this looks super to me :)