[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.
lt_iff_le_not_le
. This tactic should succeed whenever the defaultlt
is used (and maybe other cases too) so that neither of the last two fields are actually necessary. Ideally, it's only when a nontriviallt
is used thatlt_iff_le_not_le
is necessary. $\endgroup$