Unclarity about Preorder class in Lean4

Question

I realize the port of Mathlib to Lean4 is not finished yet, but I've run into a definition that I do not quite understand. I'm quite new at using theoremprovers as well as stackexchange, so please be patient with me :-)

The class Preorder is defined as follows (relying on the standard LE and LT for defining order and strict order relations):

universe u
class Preorder (\alpha : Type u) extends LE \alpha, LT \alpha :=
  (le_refl : \forall a : \alpha, a \leq a)
  (le_trans : \forall a b c : \alpha, a \leq b \impl b \leq c \impl a \leq c)
  (lt := \lambda a b => a \leq b \and \neg b \leq a)
  (lt_iff_le_not_le : \forall a b : \alpha, a < b \iff (a \leq b \and \not b \leq a))

My question is: why are the last two lines both necessary? Each of them can, as far as I can see, be considered a definition. In particular, I've managed to derive the former from the latter as follows (defining my own MyPreorder for the purpose of showing what I mean):

universe u
class MyPreorder (\alpha : Type u) extends LE \alpha, LT \alpha :=
  (le_refl : \forall a : \alpha, a \leq a)
  (le_trans : \forall a b c : \alpha, a \leq b \impl b \leq c \impl a \leq c)  
  (lt_iff_le_not_le : \forall a b : \alpha, a < b \iff (a \leq b \and \not b \leq a))

example (\alpha : Type u) [P : MyPreorder \alpha] : P.lt = (\lambda a b : a => a \leq b \and \not b \leq a) := by
  funext x y
  apply propext
  apply P.lt_iff_le_not_le

From this I would say that MyPreorder is just as powerful as a definition as the one in the Mathlib port. What am I overlooking?

Interestingly, I've so far not managed to derive the latter from the former. That may just be my own inexperience, or it may be a "typetheoretic thing" that I'm not spotting.

Can anyone explain this to me? And is there someone who can derive the latter from the former, perhaps?

Many thanks!

Answer 1

The extra fields are a convenience. It is useful to have both $<$ and $\leq$ at disposal when working with preorders, so how can we have that?

We could decide which one is “primary”, include it in the structure, and let the other one be an auxiliary definition. This is always going to be a bit unsatisfactory, because we will have to remember forever that access to one is a field in the structure but the other one is to be found elsewhere.

It is more convenient and robust to include both as fields in the structure, and include a third field that relates them (in the case at hand lt_iff_le_not_le). Moreover, we can provide a default definition of one in terms of the other (the lt := … field) so that later on we don't have to keep defining both of them. And if someone wants a custom definition of lt in a particular case, they're free to do so, as long as they also provide lt_iff_le_not_le that shows the custom definition is equivalent to the intended one.

Answer 2

[Edit: I completely rewrote this answer.]

I would say that Andrej's answer is only half the story. Lean uses type classes for overloading notation. If I have -1 < 1, Lean looks up the type class instance for the LT type class to find the meaning of < in this context. The LE and LT type classes are less about mathematical definitions and more about bookkeeping for the < and ≤ notations.

A Preorder on the other hand (and other structures like an PartialOrder and a TotalOrder) is a capturing a mathematical concept (namely a structure with a reflexive and transitive binary relation le). A preorder also has a common set of notation, namely the usual < and ≤ notations. So in the end we have to have the following instances for Preorder:

instance [Preorder α] : LE α
instance [Preorder α] : LT α

We could do it as follows:

class Preorder.{u} (α : Type u) where
  (le : α -> α -> Prop)
  (le_refl : ∀ a : α, le a a)
  (le_trans : ∀ a b c : α, le a b → le b c → le a c)

instance [P : Preorder α] : LE α where
  le := P.le
instance [P : Preorder α] : LT α where
  lt := fun x y => (P.le x y) ∨ ¬ (P.le x y)

However, this will lead to a painful diamond issue. A diamond is when you get the same thing from two different type class instances and they are not the exact same thing.

For example let's say we try to add this instance.

instance instNatPreorder : Preorder Nat where
  le := Nat.le
  le_refl := Nat.le_refl
  le_trans := @Nat.le_trans

Let's also say we have this theorem for Preorder.

theorem Preorder.le_antisymm [Preorder α] (x y : α): x < y -> ¬ (y < x)

The theorem is stated in terms of < for Preorder which is defined as (P.le x y) ∨ ¬ (P.le x y). That means we can't apply it easily to Nat. If we try to do so:

theorem Nat.le_antisymm2 (x y : Nat) : x < y -> ¬ (y < x) :=
Preorder.le_antisymm x y  -- error

We get the annoying error:

type mismatch
  Preorder.le_antisymm x y
has type
  x < y → ¬y < x : Prop
but is expected to have type
  x < y → ¬y < x : Prop

The first line in the error is talking about < for Preorder, which when specialized to Nat is (Nat.le x y) ∨ ¬ (Nat.le x y). The second line in the error is talking about < for Nat, which is Nat.lt (which is defined as Nat.le (succ x) y). Since these are not definitionally equal, the type checker gives you this error.

To address this, Lean (especially mathlib) tries to adopt the Forgetful Inheritance Pattern. The idea is that instead of defining an instance for LT which may conflict with other instances, just have the Preorder class extend LT (and LE) and then give an axiom saying that LT behaves the right way.

So in your MyPreorder, you can define an instance for Nat as

instance instNatMyPreorder : MyPreorder Nat where
      le_refl := Nat.le_refl
      le_trans := @Nat.le_trans
      lt_iff_le_not_le := sorry  -- fill in proof

Now things work correctly!

Note, by leaving lt out, we are not using the default values since lt is a field of the LT which we are extending, and there is already an instance of < for Nat, so it takes precedence. (And that is exactly what we need in this case.)

However, in cases where we are working with a new type which doesn't already have a LT or LE instance, then it will use the default if we supply le field only. I think default values are even more important for Prop fields of classes you are extending, since all you need is some proof and there is no diamond issues then.

Besides the important diamond issues, this pattern has a few smaller, but helpful advantages:

• The instances for LE and LT are added automatically.
• You don't have to add the le (or lt) field if there is already an instance of LE (and LT).
• The fields le_refl and le_trans are stated with the more natural ≤ notation instead of P.le.
• (Like Andrej said) you have flexibility of how you define lt. (For example, you could define lt directly and define le in terms of <, or define both in terms of more common known relations.)

Finally, note that as François G. Dorais said, in the Lean 3 version of preorder there is special notation added to automatically fill in the lt_iff_le_not_le proof with the order_laws_tac tactic so you don't need to manually write the proof in many cases.