Preorder / PartialOrder synthesised <

Stream: mathlib4

[Pieter Collins]

I was experimenting with partial orders in Lean and was very surprised to find that using PartialOrder automatically synthesises a LT operator < from LE ≤. Even more so because for the application I am thinking about, the synthesised <, which is defined as a < b := a ≤ b ∧ ¬b ≤ a, is definitely not what one wants! There also doesn't seem to be any way around this (there are no subclasses of PartialOrder with just ≤ and its properties).

I looked for Zulip threads or Github issues mentioning this but couldn't find anything, am I missing something?

I also looked in the source file and docs, and there's no real rationale given, only the following comment in mathlib4/Mathlib/Order/Defs/PartialOrder.lean :

/-- A preorder is a reflexive, transitive relation ≤ with a < b defined in the obvious way. -/

I notice the files mathlib4/Mathlib/Order/Defs/PartialOrder.lean (de Moura, 2016) and mathlib4/Mathlib/Order/Basic.lean (Avigad, Carneiro 2014) pretty old. Maybe this was just added for convenience for certain uses, and the design wasn't deeply thought through or discussed at the time. But it seems like an unnecessarily non-orthogonal design, and makes life awkward if the particular choice of < is not what one wants.

Alternative definitions of < which are natural in certain contexts are:

• For f,g:X→Y with a partial order on Y, define f < g ↔ ∀ x, f x < g x
• On a topological space X, we often have { (x1, x2) | x1 ≤ x2 } a closed set, and want { (x1, x2) | x1 < x2 } to be open, so taking the interior makes sense. In general, { (x1, x2) | (x1 ≤ x2) ∧ ( ¬ (x2 ≤ x1) ) } is neither closed nor open.
• Computably, ≤ is often falsifiable, and we want < to be verifiable; again the synthesised < is neither falsifiable nor verifiable.
  And in some cases, maybe you don't want to allow < at all.

Would it be possible to refactor the hierarchy to separate ≤ (WeakPartialOrder) and < (StrictPartialOrder) with the natural properties? One could combine these into a WeakStrictPartialOrder under the less restrictive assumption a<b → a≤b (probably also mixed transitivity a<b∧b≤c→a<c and a≤b∧b<≤>c→a<c), with the current PartialOrder on top of these. Presumably, the refactoring would not affect code only using PartialOrder.

[Johan Commelin]

Hi Pieter! Welcome!

I think we should indeed consider this. A long time ago a - b was defined to be a + -b. We've also decoupled that. We should probably do the same here. (And using default arguments, we can still keep the current behaviour for almost all purposes.)

[Violeta Hernández]

Hard disagree here. A preorder comes bundled with both a ≤ and a < relation, and they're always related via docs#lt_iff_le_not_ge. If that's not what you have, then you don't have a preorder.

[Violeta Hernández]

What exactly is the application you have in mind?

[Aaron Liu]

see also #mathlib4 > Conflicting `≤` and `<` @ 💬

[Violeta Hernández]

If you need a custom relation that's stronger than < then you should just define it and give it the appropriate API.

[Johan Commelin]

Maybe that's what Pieter is proposing? And one of the question is whether < can be used as notation. I don't think that's unreasonable. I'm a bit surprised that you're dismissing this so strongly.

[Violeta Hernández]

If I saw a type with a Group instance, I'd be very surprised to then find a - b defined as anything other than a + (-b)(or something equivalent). And if I saw a type with a Preorder instance, I'd feel the same seeing a < b defined as anything other than a ≤ b and not b ≤ a.

[Yury G. Kudryashov]

If you want a preorder without any restrictions on <, then you may use docs#Std.IsPreorder

[Bhavik Mehta]

Johan, I think Pieter's proposal is not quite comparable to the subtraction example. We already have a default argument for Preorder's < argument, ie it already is like subtraction, and (just like subtraction), one can decouple the definition of < from what it must be, provided we prove it's propositionally equal. Instead, this proposal would _remove_ the property of < from PartialOrder, and thus many of the theorems about it that we currently have would become false.

[Robin Arnez]

I don't think this is the proposal, from what I can tell the proposal is rather something like this:

class GeneralPreorder (α : Type u) extends LE α, LT α where
  le_refl : ∀ a : α, a ≤ a
  le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c
  le_of_lt : ∀ a b : α, a < b → a ≤ b
  not_ge_of_lt : ∀ a b : α, a < b → ¬ b ≤ a
  lt_of_le_of_lt : ∀ a b c : α, a ≤ b → b < c → a < c
  lt_of_lt_of_le : ∀ a b c : α, a < b → b ≤ c → a < c

class Preorder (α : Type u) extends GeneralPreorder α where
  lt_iff_le_not_le : ∀ a b : α, a < b ↔ a ≤ b ∧ ¬ b ≤ a
  le_of_lt := fun a b h => lt_iff_le_not_le a b |>.1 h |>.1
  not_ge_of_lt := fun a b h => lt_iff_le_not_le a b |>.1 h |>.2
  lt_of_le_of_lt := fun a b c h₁ h₂ =>
    lt_iff_le_not_le a c |>.2
      ⟨le_trans a b c h₁ (le_of_lt b c h₂),
        fun h => absurd (le_trans c a b h h₁) (not_ge_of_lt b c h₂)⟩
  lt_of_lt_of_le := fun a b c h₁ h₂ =>
    lt_iff_le_not_le a c |>.2
      ⟨le_trans a b c (le_of_lt a b h₁) h₂,
        fun h => absurd (le_trans b c a h₂ h) (not_ge_of_lt a b h₁)⟩

class GeneralPartialOrder (α : Type u) extends GeneralPreorder α where
  le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = b

class PartialOrder (α : Type u) extends GeneralPartialOrder α, Preorder α where

So pretty much nothing would change for someone just using Preorder or PartialOrder but there would be an earlier class, however it may be called, that makes less assumptions about < (if we don't like Preorder extending it we could always also make it a separate class with the right instances).

[Aaron Liu]

GeneralPreorder feels way to permissive

[Aaron Liu]

you can set lt a b := False and it works with any le (that forms a preorder)

[Robin Arnez]

Yeah, I'm not sure what kind of properties would be reasonable to put in there; I suppose at least though

1. lt a b := a ≤ b ∧ ¬ b ≤ a should satisfy those properties
2. If < on β has those properties, then lt f g := ∀ x : α, f x < g x should also have those properties on α → β
3. If ≤ forms a linear order, then < should be uniquely determined

[Aaron Liu]

unfortunately those conditions are incompatible

[Aaron Liu]

ah no, the thing I was thinking of doesn't work

[Aaron Liu]

Robin Arnez said:

should also have those properties on α → β

I was tricked by the non-dependent arrow

[Yury G. Kudryashov]

There are 2 separate discussions here:

• should we change the canonical instance of LT on a product/pi type?
• if yes, then what could be the axioms describing this new instance?

[Yury G. Kudryashov]

I think that we should keep these 2 discussions separate. If we decide "no" for the first one, then the second one can turn into "should we turn docs#StrongLT into a typeclass with some axioms?"

[Robin Arnez]

Oh I get what you mean about these being incompatible; if we looked at Unit × ℝ then pointwise < would end up with (a, b) < (c, d) := False but Unit × ℝ has a linearly ordered ≤ and should thus induce a unique <. So either

1. we introduce a new typeclass for <, which will have to be more permissive (i.e. allow an empty relation) to apply to products and pi types
2. we introduce a new typeclass for <, which will not be permissive but therefore also not apply to products and pi types in general
3. we introduce a new typeclass and new notation that will represent a generalized strict <
4. we don't introduce a new typeclass but something else
5. we don't change anything

[Bhavik Mehta]

My view is that we shouldn't change anything here, and docs#Std.IsPreorder or docs#IsStrictOrder or the related could be used if necessary. But we do already have another ordering defined on Prod and Pi, via docs#Lex, so in particular situations (and downstream applications) a new instance can be put on these types anyway.

[Jireh Loreaux]

In the past there have been discussions about making a new class which would allow for a "StrongLT" in different contexts in such a way that it is compatible with, but does not induce, the existing order structure. This would be a strict order, let's denote it ≪, that has some properties like: a ≪ b → a < b, a ≪ b → b ≤ c → a ≪ c and a ≤ b → b ≪ c → a ≪ c. Potentially there could be further mixins analogous to IsOrderedMonoid which specify the interaction with ≤, ≪, < and +.

Besides pi types, another place this comes up is with strictly positive operators on a Hilbert space and strictly positive elements in a C⋆-algebra.

But no, I don't think we should redefine < or decouple it from PartialOrder, although I have considered it in the past.

[Bolton Bailey]

I think that the "obvious" docstring should at least be changed. It is not very useful to see something described as obvious in the docstring of an unfamiliar typeclass that forgets many of the hypotheses of a stronger more common typeclass like partial order or linear order. I would have thought the obvious definition of lt would have been "le but not equal".

[Bolton Bailey]

It is not helpful to my confusion level that the usual reading of ≤ in English is "less-than or equal to" but le_iff_lt_or_eq is a theorem of PartialOrder that does not hold in general for Preorder

[Bolton Bailey]

If we are going to keep things as they are, what is the standard advice for someone who wants the lt on their type to be something different than what it is, like in the function type example? Define a new LT instance to use locally? Use some other notation?

[Violeta Hernández]

Bolton Bailey said:

I think that the "obvious" docstring should at least be changed.

I agree. The definition is standard, but certainly not obvious. Preorders are very jarring if you're used to thinking of less-or-equal as either less or equal. (This is really the fault of the naming, to be fair)

[Bolton Bailey]

I have put a PR here #34512

[Pieter Collins]

@Aaron Liu Thanks for spotting this discussion! I issue they have with the (strict) Loewer is a good example of an existing natural usage where < is not that of Lean's PartialOrder.

[Pieter Collins]

Violeta Hernández :

Hard disagree here. A preorder comes bundled with both a ≤ and a < relation, and they're always related via docs#lt_iff_le_not_ge. If that's not what you have, then you don't have a preorder.

That's the current Lean Mathlib definition of a preorder. But this is particular to Lean; other sources (e.g. Wikipedia, Wolfram Mathworld) don't bundle ≤ with <. Even Std.IsPreorder doesn't require LT.

[Pieter Collins]

Here's the basic idea for refactoring I had in mind. This means one can use ≤ and < separately, combine them with weaker restrictions (essentially a < b → a ≤ b and mixed-transitivity) or use the synthesised version of <.

class WeakPreorder (α : Type u) extends LE α where
  le_refl : ∀ a : α, a ≤ a
  le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c

class StrictPreorder (α : Type u) extends LT α where
  lt_irrefl : ∀ a : α, ¬ (a < a)
  lt_trans : ∀ a b c : α, a < b → b < c → a < c

class WeakStrictPreorder (α : Type u) extends WeakPreorder α, StrictPreorder α where
  le_of_lt : ∀ a b : α, a < b → a ≤ b
  lt_of_le_of_lt : ∀ a b c : α, a ≤ b → b < c → a < c
  lt_of_lt_of_le : ∀ a b c : α, a < b → b ≤ c → a < c

class Preorder (α : Type u) extends WeakStrictPreorder α where
  lt := fun a b ↦ a ≤ b ∧ ¬b ≤ a
  lt_iff_le_not_ge : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a := by intros; rfl
  lt_irrefl := by intros; rfl
  lt_trans := by intros; rfl
  le_of_lt := by intros; rfl
  lt_of_le_of_lt := by intros; rfl
  lt_of_lt_of_le := by intros; rfl


class WeakPartialOrder (α : Type u) extends WeakPreorder α where
  le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = b

class StrictPartialOrder (α : Type u) extends StrictPreorder α where
  lt_asymm : ∀ a b : α, a < b → ¬ (b < a) := by intros; rfl

class WeakStrictPartialOrder (α : Type u)
    extends WeakPartialOrder α, StrictPreorder α, Preorder α where

class PartialOrder (α : Type u) extends WeakStrictPartialOrder α, Preorder α where

[Edward van de Meent]

Note that lt_asymm is a theorem following from irreflexivity and transitivity...

[Edward van de Meent]

So it should already hold for StrictPreorder

[Pieter Collins]

@Edward van de Meent
I didn't put lt_asymm in StrictPreorder for consistency with WeakPreorder. Of course, it could go in StrictPreorder. One could even omit one of the StrictPreorder or StrictPartialOrder typeclasses.

[Jakub Nowak]

Having two definitions for the same thing sounds like unnecessary code duplication.

[Edward van de Meent]

Not to mention the fact that this very well may invite instance diamonds. Indeed, i am more in favor of Jireh's proposal.

[Jakub Nowak]

We could try and use scoped notation more. We could have both proposals and the user can choose by opening some one or other namespace.

[Edward van de Meent]

Now that sounds like unnecessary code duplication

[Jakub Nowak]

How would scoped notation lead to code duplication?

[Edward van de Meent]

The "having both proposals" part

[Pieter Collins]

Bhavik Mehta said:

My view is that we shouldn't change anything here, and docs#Std.IsPreorder or docs#IsStrictOrder or the related could be used if necessary.

Ah, I didn't spot Std.IsPreorder and Mathlib.Order.Defs.Unbundled.IsStrictOrder earlier.

But why then does Mathlib's Preorderhave < when Std.IsPreorderdoes not? And why aren't these typeclasses extended by Mathlib's Preorder?

This gives me the impression that (i) the conceptualisation has not been clearly thought through, and (ii) typeclasses have been added piecemeal without being properly integrated (maybe to avoid refactorisation).

For a new user, which should one use for just ≤, Std.IsPartialOrder or Mathlib's PartialOrder? Are there results available for one but not the other? Why is (to give an example I am working with) is Dyadic an instance of both Std.IsPartialOrder and PartialOrderbut Rat only of PartialOrder?

[Jakub Nowak]

Edward van de Meent said:

The "having both proposals" part

But from the implementation perspective both proposals are the same I think? They only differ in what is the notation.

[Edward van de Meent]

I dont believe we want both of StrictPreorder and LawfulStrongLT

[Jakub Nowak]

Hm, maybe not the same. But I meant to implement one implementation, and then have namespace A in which a < b is notation for a ≤ b ∧ ¬ b ≤ a, and a ≪ b is notation for LT or StrongLT (that depends on the implemntation). And in another namespace B a < b would be the notation for LT/StrongLT. And either we don't have notation for a ≤ b ∧ ¬ b ≤ a in namespace B, or we could come up with some yet another notation.

[Aaron Liu]

this sounds like it will be really unnecessarily confusing

[Jakub Nowak]

In mathlib we would always stick to one.

[Jakub Nowak]

But it lets the user choose a different notation.

[Edward van de Meent]

The user can always choose a different notation, just not <

[Jakub Nowak]

It's already present in math papers that notation can mean something different, depending on the field. So it's the question of whether we want a consistent notation across all math, or whether scoped notation is necessary evil.

[Jakub Nowak]

I can see the appeal of having consistent notation across all math. The problem that could lead to is that you would have to remember 30 different symbols and how to read and type them. It might be easier after all to just have the same notation mean something different depending on the namespace. I'm not sure if that would be confusing. The mathlib would still standardize the notation, so you just would just have to learn what notation is used for the field you're plan to work in. Even if you work in multiple fields, you should at every time be aware of what are you're working on at the given moment and which notation is in place in the file you're working in.

[Jakub Nowak]

I can share a story from my lectures. The professor wrote a theorem on a board, and I spotted, that the theorem is wrong. So I raised a question, and it turned out, that the notation v < u (v, u were vectors) that the professor wrote, didn't mean v ≤ u ∧v ≠ u as I wrongly assumed, but pointwise <.
If the professor used some other symbol, that I still would have to ask the question, because I wouldn't know what the symbol meant. I guess it might be less confusing that way, though not really by much. I quickly spotted that something was wrong, asked a question, and my confusion was resolved. We used this notation a lot and it wasn't confusing anymore after I learned what it meant. And in the end, < was easier to write than some other symbol like ≪.
I also had another lectures, about partial orders, and on these lectures a < b meant just a ≤ b ∧ ¬ b ≤ a . Even though we used the same notation on these two different lectures I was never confused by it. I was always aware of the context and knew what the notation meant.

[Aaron Liu]

sorry, I lost track of what you're proposing should be done

[Aaron Liu]

are you still proposing to override the core notation for LT.lt?

[Vlad Tsyrklevich]

Pieter Collins said:

But why then does Mathlib's Preorderhave < when Std.IsPreorderdoes not? And why aren't these typeclasses extended by Mathlib's Preorder?

Order typeclasses in Std are still relatively new and some of the justification for their design can be found in #general > Request for feedback: new order typeclasses in std library @ 💬 I'm not sure about why Preorder has an Std.IsPreorder instance versus being extended. Some of the other classes that map onto mathlib better have been/are being adopted in mathlib already e.g. see #mathlib4 > Relation properties duplication

[Vlad Tsyrklevich]

Pieter Collins said:

For a new user, which should one use for just ≤, Std.IsPartialOrder or Mathlib's PartialOrder? Are there results available for one but not the other? Why is (to give an example I am working with) is Dyadic an instance of both Std.IsPartialOrder and PartialOrderbut Rat only of PartialOrder?

Well PartialOrder is not supported for just $\le$ so that seems to be out of the question. The Std classes will surely have less API than the mathlib ones given that the mathlib ones provide instances for Std and are older and have more API, but maybe you can comment more about what specifically you'd like to do to get more relevant feedback. I can #synth Std.IsPartialOrder Rat so I assume you mean the question the other way around: Why is there no PartialOrder for Dyadic: probably it just hasn't been done yet but would be welcome as mentioned in the other thread where you asked about Dyadic.

[Jakub Nowak]

Aaron Liu said:

are you still proposing to override the core notation for LT.lt?

I wasn't proposing any particular implementation though, but argumenting that scoped notation might not be confusing. Implementation wise we don't necessarily have to change anything in core, but we would need a feature that let's you overwrite a notation from core inside a namespace, which I think is not currently possible.

[Edward van de Meent]

i think in a lecture series, it's definitely possible to have notation conflict with lectures on other topics. However, not in mathlib. I think this will cause a headache when learning/teaching mathlib. In particular, the docs will not show you what instance of LT is meant by <, so this can lead to confusing situations similar to when one writes [Ring Real] to then try to apply sq_nonneg, except that in the < situation, the fact that it won't work is intended

[Edward van de Meent]

which feels maniacal/evil to me. (i understand it isn't and comes from a logical train of thought, but it still feels that way)

[Violeta Hernández]

Pieter Collins said:

That's the current Lean Mathlib definition of a preorder. But this is particular to Lean; other sources (e.g. Wikipedia, Wolfram Mathworld) don't bundle ≤ with <. Even Std.IsPreorder doesn't require LT.

Wikipedia: Any preorder $\lesssim$ gives rise to a strict partial order defined by $a < b$ if and only if $a \lesssim b$ and not $b \lesssim a$.

[Violeta Hernández]

It's also worth noting that it's exactly this definition of < which guarantees the relation can be lifted to the docs#Antisymmetrization of the preorder.

[Violeta Hernández]

Violeta Hernández said:

What exactly is the application you have in mind?

Might I ask this again? This entire thread feels like a huge #xy. We're trying to come up for a design for a "stronger < relation" without even knowing what we want it for.

[Violeta Hernández]

Do you want the pointwise < relation on functions? We have that already. Do you want some kind of matrix ordering? There's existing API for that. Is this just a hypothetical? Then no action is needed.

[Pieter Collins]

Violeta Hernández said:

Wikipedia: Any preorder $\lesssim$ gives rise to a strict partial order defined by $a < b$ if and only if $a \lesssim b$ and not $b \lesssim a$.

Indeed it's a general definition of a particular preorder. But there are others, and this is not always the one that's wanted.

[Pieter Collins]

Violeta Hernández said:

What exactly is the application you have in mind?

The main application I have in mind is developing constructive analysis and rigorous numerical methods. Here, the natural relation between < and ≤ is that < should be verifiable (topologically: true on an open set of pairs), and ≤ falsifiable (true on a closed set). The synthesised < doesn't satisfy this in general (though it does for a total order). I would like the (topo)logically-natural orders on R^n and C(X->R), but also on spaces of subsets ordered by inclusion.

But I think the issue is bigger than my particular application. (Otherwise I probably wouldn't have posted on this channel.) The examples we've seen above are all related to topology; < should be robustly true, so hold on an open set. For discrete mathematics it may well be a non-issue, but for continuous mathematics the current definition is unnatural.

[Pieter Collins]

Things get problematic once we combine Lean partial orders with the order topology.
Given the (total) partial order on R, we can define the product order on R^2 given by (x1,y1) ≤ (x2,y2) ↔ x1 ≤ x2 ∧ y1 ≤ y2. (I can't find this definition in Lean/Mathlib, but it's standard and hopefully uncontroversial). We then define the order topology on R^2 docs#OrderTopology which uses the synthesised < to generate basic opens { (x,y) | (a,b) < (x,y) < (c,d) }. By taking intersections, we see that sets { (x,y) : a<x<c ∧ y=b } and { (x,y) : x=a ∧ b<y<d } are open. Intersecting sets of this form shows that all singletons { (a,b) } are open, so we have the discrete topology! This is not what we want!!
Defining (x1,y1) < (x2,y2) ↔ x1 < x2 ∧ y1 < y2, which is the natural product strict partial order, gives the Euclidean topology as the order topology.

[Pieter Collins]

I think synthesising < is a genuinely bad design (and I don't say that lightly), and unnecessarily so.

• I think orthogonality is a good design principle. It seems to be present in the arithmetic classes (e.g. Neg, Add and Sub are separate, and only in SubNegMonoid do we have sub_eq_add_neg : ∀ a b, a - b = a + -b.) So why not here? Moreover, I think a - b = a + -b is probably closer to being universal than lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a.

• The definition of PartialOrder doesn't correspond to (what I believe is by far) the most common definition which only mentions ≤.

• The choice is general, but is not canonical there are other reasonable choices (notably in continuous mathematics).

• Providing a convenience to some users shouldn't also be an inconvenience to others.

• It's unnecessary, since one can easily refactor to keep a typeclass (even called PartialOrder) with this particular relationship between ≤ and <, and also have typeclasses with weaker reasonable definitions of compatibilty, and with only one of the two.

• I think an important goal in formalising mathematics is to keep assumptions to a minimum. This means that abstractions should be graded so that one can use precisely the conditions needed for the result. This increases generality, and clearly shows what assumptions are needed. The algebra classes in Lean seem to follow this design.

  • For a result which only needs ≤, we shouldn't have to have a <. For a result which needs weaker conditions on <, we shouldn't restrict to cases assuming the stronger condition.
  • Suppose we have an alternative < (let's call it ⋖) which is a strict partial order satisfying some compatibilty conditions with ≤. Maybe these are already sufficient to apply the particular Big Theorem we am interested in using. But if the Big Theorem assumes PartialOrder because there's nothing weaker in the library, then presumably we have to redo the proof of Big Theorem to use it.

Now I'm sure that one can work around many issues, like using different operator symbols. But then the user/reader still has to realise that '<' is wrong, and doesn't mean what it does in the domain literature, which could lead to errors. I also don't see a workaround for the Big Theorem issue.

Since this is a fundamental concept, it is probably widely used and one of the first things many new users will work with. So it's important to get things right! I realise it's also harder to change, and changes should definitely be well-considered. Here, I think the library could be majorly improved by refactoring PartialOrder, which hopefully is a non-breaking change for the rest of Mathlib.

[Wrenna Robson]

@Pieter Collins Interesting thoughts! Can I ask: what do you think < and <= should mean?

[Violeta Hernández]

The order topology is not meant for partial orders or preorders. In fact I believe there is a pending refactor to use LinearOrder as an assumption throughout.

[Bhavik Mehta]

Pieter Collins said:

That's the current Lean Mathlib definition of a preorder. But this is particular to Lean; other sources (e.g. Wikipedia, Wolfram Mathworld) don't bundle ≤ with <.

I don't believe this is fair, Violeta has given one wikipedia link which contradicts your claim, and here is another. Page 2 of Davey & Priestley Introduction to Lattices and Order also has this definition, as does Page 4 of Roman's Lattices and Ordered Sets. Birkhoff's Lattice theory also does this bundling (though in partial orders, using the equivalent version which is valid there). Do you have references which don't do this?

Pieter Collins said:

• It seems to be present in the arithmetic classes (e.g. Neg, Add and Sub are separate, and only in SubNegMonoid do we have sub_eq_add_neg : ∀ a b, a - b = a + -b.) So why not here?

This is exactly the pattern taken in mathlib for Preorder and PartialOrder, we have the classes LE and LT corresponding to Neg, Add and Sub, and they are only combined in Preorder. The pattern is exactly the same: we have notational typeclasses with no axioms, and structural typeclasses combining them with axioms. As such, I think it's unfair to call this bad design.

On the product order, I think this discussion https://mathoverflow.net/a/296355/117945 is particularly relevant.

[Violeta Hernández]

Let me address some of your other points.

Orthogonality: we already have that! If you want ≤ and < as bare notation, the docs#LE and docs#LT typeclasses exist. And then docs#Preorder is the weakest typeclass combining both in a reasonable way. It's not any different from the algebraic examples you give.

Textbook definition: Orders are usually defined from just a ≤ relation, yes, but you'd be hard-pressed to find anyone who doesn't also implicitly define a < relation as well. In the partial order case, the obvious way to do this is via a ≤ b and a ≠ b. In the preorder case, the most reasonable generalization is precisely a ≤ b and not b ≤ a, for the reason that it will not distinguish between order-indistinguishable elements the way that the partial order definition would.

Other possible choices: the symbol < can mean any number of things, yes. What I'm arguing is that the path of least resistance is to just define a new symbol for what you want to do, and prove whatever API is appropriate to it.

Easy refactoring: I'd like to emphasize that typeclasses aren't cheap. With every new typeclass comes a large amount of boilerplate, plus API and theorems that now have to be generalized to use it. Mathlib has more than a million lines of code. Any large change in something as basic as the order library would take dozens of hours of refactoring effort. It's not easy as you seem to be suggesting.

Minimum assumptions: carrying around < does not decrease generality anymore than carrying subtraction and negation separately in a group. If you only want to talk about ≤ in a preorder, you can let < be defined automatically and just never mention it.

[Wrenna Robson]

https://en.wikipedia.org/wiki/Partially_ordered_set

There is a discussion on this page about the fact that every strict partial order gives rise to a weak partial order and vice versa - I think this precisely corresponds to the fact that < and <= correspond.

Is the same true with preorders? I know Mathlib defines some of this stuff but I am not sure if all of its definitions are the same as other sources etc.

[Wrenna Robson]

To me, at the very least for PartialOrder, you need <= and < to be compatible because the typeclass represents both orders at once.

[Wrenna Robson]

I do think it would be good to use the Std classes where possible.

[Wrenna Robson]

Hmm: this paragraph from https://en.wikipedia.org/wiki/Weak_ordering suggests that in fact they are not equivalent.
image.png

[Bhavik Mehta]

Wrenna Robson said:

https://en.wikipedia.org/wiki/Partially_ordered_set

There is a discussion on this page about the fact that every strict partial order gives rise to a weak partial order and vice versa - I think this precisely corresponds to the fact that < and <= correspond.

Is the same true with preorders? I know Mathlib defines some of this stuff but I am not sure if all of its definitions are the same as other sources etc.

For preorders, < doesn't uniquely determine <= (see eg https://mathoverflow.net/a/286674/117945), but <= is used to define < in the order theory textbooks I could think of to check

[Wrenna Robson]

That page somewhat implies that you could define x < y as "y is not <= x".

[Wrenna Robson]

Which is equivalent to the above I think only on linear orders?

[Wrenna Robson]

I think on reflection I am of the view, therefore, that Preorder defining the equivalence between < and <= that it does might be a mistake, but that certainly I would want le_iff_lt_or_eq for Partial Orders.

[Wrenna Robson]

(Preorder should therefore perhaps only be an extension of LE, or possibly dependent on [LE _], the approach Std.IsPreorder takes.)

[Wrenna Robson]

Essentially currrently we have docs#instLawfulOrderLT_mathlib dependent on Preorder. Would it be so bad if it was dependent on Partial Order? I am not sure.

[Aaron Liu]

Wrenna Robson said:

That page somewhat implies that you could define x < y as "y is not <= x".

You can do this, but it doesn't work very well, for example "y is not <= x" is not in general a transitive relation

[Wrenna Robson]

Well that's fine. I mean it doesn't seem very useful but that I would expect.

[Wrenna Robson]

If I am reading https://en.wikipedia.org/wiki/Preorder#Strict_partial_order_induced_by_a_preorder and your posts correctly, which Violeta linked above, every preorder <= gives rise to a < which is "lawful", but that you could have some non-lawful < which would still give rise to <= if it was defined from it.

[Aaron Liu]

correct no that doesn't seem right

[Aaron Liu]

< only gives rise to <= if you additionally specify an equivalence relation compatible with < (the "inseparable wrt <=" relation)

[Wrenna Robson]

Right, sorry, I see.

[Wrenna Robson]

yes because a <= b iff a < b or a ~ b, which I see is actually equivalent to:
a <=b iff a < b or (a <=b and b <= a).

[Edward van de Meent]

Something something LEM

[Wrenna Robson]

(which is clearly simpler when <= is a partial order.)

[Aaron Liu]

if you specify = as the equivalence relation you always get a partial order, this is what docs#partialOrderOfSO does

[Wrenna Robson]

Right because then you are essentially saying no loops in your order graph.

[Wrenna Robson]

something something univalence ;)

[Wrenna Robson]

I don't think the full refactor proposed above is at all the right one, but I do see the argument that mayvbe

Wrenna Robson said:

yes because a <= b iff a < b or a ~ b, which I see is actually equivalent to:
a <=b iff a < b or (a <=b and b <= a).

Is a <=b iff a < b or (a <=b and b <= a) equivalent to a < b iff a <= b and ¬b <= a?

[Aaron Liu]

what conditions are you assuming on <

[Aaron Liu]

< could be equal to <=

[Wrenna Robson]

none other than what is there I guess? Or maybe that it's a strict preorder I suppose.

[Wrenna Robson]

Yes one would want that.

[Aaron Liu]

if it's just a strict preorder then < could have some fine structure inside the equivalence classes of <=

[Wrenna Robson]

Hm. Which is ruled out by a < b iff a <= b and ¬b <= a?

[Aaron Liu]

yeah

[Wrenna Robson]

Hmm.

[Wrenna Robson]

Then yeah it does somewhat feel like the current definition of Preorder precludes such structure?

[Aaron Liu]

I really don't see why you would want it

[Wrenna Robson]

It feels very delicate and quite niche though.

[Wrenna Robson]

Aaron Liu said:

I really don't see why you would want it

Neither do I - I think I am just obsessive about never eliminating possible structures unnecessarily.

[Wrenna Robson]

Std has LawfulOrderLT.of_lt which basically says that the <= induced by "not <" is a lawful one.

[Wrenna Robson]

I think my general opinion is more that I would support using the Std classes if at all possible, but that it is also good to make sure that the setup we use doesn't rule them out.

[Bhavik Mehta]

Don't forget we also have https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Defs/Unbundled.html#IsStrictOrder and related, to express these concepts

[Wrenna Robson]

Yes - I think there is an effort to remove them and replace them with the Std ones maybe? At least a subset.

[Bhavik Mehta]

I don't know that these ones in particular have Std analogues?

[Kim Morrison]

Violeta Hernández said:

Easy refactoring: I'd like to emphasize that typeclasses aren't cheap. With every new typeclass comes a large amount of boilerplate, plus API and theorems that now have to be generalized to use it. Mathlib has more than a million lines of code. Any large change in something as basic as the order library would take dozens of hours of refactoring effort. It's not easy as you seem to be suggesting.

Without saying anything about this particular change, I do want to push back against reflexively saying "this refactor is too hard, Mathlib is too big". I think over the years we have actively embraced refactors that go right to the roots of Mathlib/Lean, and this has been good, and we should always remain open to doing these refactors when they are motivated!

[Wrenna Robson]

Kim Morrison said:

Violeta Hernández said:

Easy refactoring: I'd like to emphasize that typeclasses aren't cheap. With every new typeclass comes a large amount of boilerplate, plus API and theorems that now have to be generalized to use it. Mathlib has more than a million lines of code. Any large change in something as basic as the order library would take dozens of hours of refactoring effort. It's not easy as you seem to be suggesting.

Without saying anything about this particular change, I do want to push back against reflexively saying "this refactor is too hard, Mathlib is too big". I think over the years we have actively embraced refactors that go right to the roots of Mathlib/Lean, and this has been good, and we should always remain open to doing these refactors when they are motivated!

Strongly agree with this. I think it's vital for Mathlib that over time it does not ossify and become conservative in what it is willing to change.

[Snir Broshi]

Wrenna Robson said:

Yes - I think there is an effort to remove them and replace them with the Std ones maybe? At least a subset.

Yes but Kim suggested to leave the order classes alone for now

[Pieter Collins]

Violeta Hernández said:

And then docs#Preorder is the weakest typeclass combining both in a reasonable way.

No! Precisely my main point is that there are weaker and reasonable relationships between < and ≤. In particular, the combination

  le_of_lt : ∀ a b : α, a < b → a ≤ b

requiring that < is not too big, and

  lt_of_le_of_lt : ∀ a b c : α, a ≤ b → b < c → a < c
  lt_of_lt_of_le : ∀ a b c : α, a < b → b ≤ c → a < c

requiring that < is not too small, is reasonable. We've seen concrete examples of product orders and the Loewner order where these are used.

[Bhavik Mehta]

Note that earlier in the thread we already have a counterexample explaining why this is not reasonable: #mathlib4 > Preorder / PartialOrder synthesised < @ 💬

[Pieter Collins]

Note that in a topological space, taking a<b ↔ (a,b) ∈ interior { (x,y) | x ≤ y } satisfies lt_of_le_of_lt and lt_of_lt_of_le.

[Violeta Hernández]

I'm not sure which topology you're using here, since:
Violeta Hernández said:

The order topology is not meant for partial orders or preorders. In fact I believe there is a pending refactor to use LinearOrder as an assumption throughout.

[Pieter Collins]

Regarding the example lt a b := False being compatible with any le preorder:
I don't mean to imply that the relations #mathlib4 > Preorder / PartialOrder synthesised < @ 💬 define what is meant for le and lt to be compatible. However, they do form weaker conditions which are satisfied by some pairs of relations which do not satisfy lt_iff_le_not_ge but are still natural to consider together. The transitivity conditions are precisely what is needed to chain < and ≤, which seems like a useful yet fairly minimal requirement which is definable purely and easily in terms of the order relations.