Std Trichotomous

Stream: Is there code for X?

[Wrenna Robson]

Is there a spelling in Std for Mathlib's IsTrichotomous (in the same way that Std.Total is essentially the same as IsTotal)?

[Kenny Lau]

presumably you're asking because there isn't one?

[Wrenna Robson]

Well, I can't find it, but perhaps it is named something unexpected.

[Wrenna Robson]

The various order typeclasses (and the fact that Std and Mathlib seem to disagree about how to define them...) are quite confusing.

[Kenny Lau]

Loogle "Std.", ⊢ Prop, LT, and i presume it's Std.LawfulOrderLT + Std.IsLinearOrder

[Kenny Lau]

Loogle "Std.", ⊢ Prop, (?a → ?a → Prop) didn't suggest anything more useful

[Wrenna Robson]

Well, Std.LawfulOrderLT + Std.IsLinearOrder is stronger.

[Wrenna Robson]

This would just be "a < b or a = b or b < a".

[Alex Meiburg]

I was going to joke that Std.Antisymm (¬· < ·) is a logically correct spelling but terrible and obviously shouldn't actually be used. But then I threw it into Loogle and it actually does seem to be the standard spelling, it's used in a lot of instances: https://loogle.lean-lang.org/?q=Std.Antisymm+%28%C2%AC%C2%B7+%3C+%C2%B7%29

[Wrenna Robson]

Oh no.

[Wrenna Robson]

What a horrible mess.

[Kenny Lau]

we can at least have an abbrev...

[Wrenna Robson]

For context, I was trying to work out what (in general) is the minimal typeclass where sorting algorithms make sense. Honestly we should probably use Ord for them...

[Wrenna Robson]

Insisting on using a relation seems to invite all sorts of headaches.

[Snir Broshi]

Wrenna Robson said:

(in the same way that Std.Total is essentially the same as IsTotal)?

(IsTotal is not the only one - #mathlib4 > Relation properties duplication )

[Wrenna Robson]

Yes, that was just an example of the sorry state of affairs.

[Paul Reichert]

Std.LawfulOrderLT + Std.Total (· ≤ ·) is equivalent to IsTrichotomous under the mild assumption that Asymm (· < ·) holds, but it needs LE to be present. (That's not true, in fact.)

That said, I would accept a PR introducing IsTrichotomous into Std -- given that Antisymm is used for not-lt in lots of places, this seems like a real improvement. Std has the philosophy that the more complex properties of orders are expressed in terms of LE in order to avoid too much duplication, but we still want to support simple, low-level properties such as this one.

Besides, are you actually able to prove something meaningful about a sorting algorithm without assuming transitivity? Otherwise, I think I would indeed have required Std.IsLinearOrder (perhaps + Std.LawfulOrderLT or Std.LawfulOrderOrd, depending on whether the sorting algorithm uses aLT, LE or Ord operation; mergeSort uses a less-than-or-equal relation).

[Wrenna Robson]

mergeSort uses a LE I think?

[Wrenna Robson]

But no I think you have to assume transitivity at least.

[Paul Reichert]

Wrenna Robson said:

mergeSort uses a LE I think?

Yes, sorry, I mistyped.

[Wrenna Robson]

My suspicion is that in fact there is nowhere we use the notion of sorted-ness which does not apply to <=, on the basis that in a partial order "sorted by <" is the same as "sorted by <= and also no duplicates".

[Wrenna Robson]

If you look at, say, [List.sorted_mergeSort](https://leanprover-community.github.io/mathlib4_docs/Init/Data/List/Sort/Lemmas.html#List.sorted_mergeSort), this uses transitivity and totality. I think those properties are sufficient there.

[Wrenna Robson]

Array.insertionSort takes a LT (or rather that seems to be the default) but nothing is proved about it. Mathlib has List.insertionSort - but actually my current efforts are going towards tidying up this file and hopefully killing off the current definition of List.Sorted (which isn't very good).

[Wrenna Robson]

But then consider List.Perm.eq_of_sorted.

[Wrenna Robson]

Essentially I would say that this suggests that the sentence "List L is the sorted version of list K` is well-defined for an antisymmetric relation. Like it may not exist... indeed I think you need totality and transitivity for that... but it's unique - you can't swap elements round and get another sorted list.

[Wrenna Robson]

Notably... I am not sure you need reflexivity.

[Wrenna Robson]

I see in that thread that @Markus Himmel mentions that the purpose of these nice Std classes is to e.g. enable verified sorting algorithms in core - that is of interest to me though because core is so (rightly!) selective in terms of what it admits, I will say I hope it isn't just core that gets this.

[Paul Reichert]

I'm not sure I fully understand what you are wishing for -- can you try to rephrase it a bit? What is it that you hope not just core gets?

[Wrenna Robson]

Oh - sorting algorithms. Like, in particular I would like the chance to contribute to such work.

[Wrenna Robson]

Right now I would not say they have a clear home (there's some in Mathlib, which feels an odd fit, and some in core, but in some cases not accompanied with proofs).

[Markus Himmel]

Sorting algorithms that actually make sense in real Lean programs (the kind that are compiled and executed) are very interesting for core, and the FRO will make a move on this sometime in 2026. If at that time we find that there is a nice downstream repository which contains great verified implementations, we will be very interested in seeing this work upstreamed to core.

As for more academic aspects of sorting algorithms, these will probably not be in core.

Edit: I had to revise the above a bit to be more precise.

[Wrenna Robson]

Oh, and a little in Batteries! They're everywhere.

[Wrenna Robson]

My research interest in particular is in sorting networks which are a little specialised. But I am attempting at present to, I suppose, tidy up the downstream situation somewhat.

[Wrenna Robson]

I should say that in particular I am interested in executing sorting networks - in cryptographic applications but that isn't quite relevant here.

[Markus Himmel]

At first glance, that sounds like something that would be most likely to be of interest to CSlib

[Wrenna Robson]

Yes. Is CSLib downstream of Mathlib?

[Wrenna Robson]

I suppose that isn't the end of the world but it feels somewhat untidy to have the big maths monorepo to be upstream of "computer science in particular".

[Wrenna Robson]

What is the current vision for Batteries?

[Wrenna Robson]

Anyway: returning to the question I asked.

[Wrenna Robson]

theorem total_iff_refl_and_trichotomous {α : Type u} {r : α → α → Prop} :
    (∀ a b, r a b ∨ r b a) ↔ (∀ a, r a a) ∧ (∀ a b, r a b ∨ a = b ∨ r b a) := by grind

[Wrenna Robson]

My suggestion therefore would be:

• Add Std.Trichotomous in the obvious way.
• Do exactly one of the following:
  ** Make Std.instReflOfTotal a def, not an instance, and add Std.instTotalOfReflOfTrichotomous as an instance
  ** Add Std.instTrichotomousOfTotal as an instance and add Std.instTotalOfReflOfTrichotomous as a def.

[Wrenna Robson]

(I assume these can't all be instances because that clearly creates a loop.)

[Wrenna Robson]

There is also a natural
def compareOfTrichotomous (r) [Decidable (r x y)] [Decidable (r y x)] [Std.Trichotomous r] (x y : α) : Ordering := if r x y then Ordering.lt else if r y x then Ordering.gt else Ordering.eq or something like that, and then probably there's things to do with Std.LawfulCmp.

[Wrenna Robson]

@Paul Reichert I would appreciate some guidance as to what PR you'd prefer - as in, what you would like to be instances versus non-instances.

[Wrenna Robson]

public instance Refl.irrefl {α : Type u} {r : α → α → Prop} [i : Std.Refl (¬ r · ·)] :
    Std.Irrefl r where irrefl := i.refl

Oh also we seem to be missing this (which I infer from the presence of Total.asymm_of_total_not would be desired).

[Wrenna Robson]

Also, similar to the above:

theorem asymm_iff_irrefl_and_antisymm {α : Type u} {r : α → α → Prop} :
    (∀ a b, r a b → ¬ r b a) ↔ (∀ a, ¬ r a a) ∧ (∀ a b, r a b → r b a → a = b) := by grind

Asymm is equivalent to Irrefl and Antisymm in an analogous way to Total being equivalent to Refl and Trichotomous.

[Wrenna Robson]

(Also, I think substantially less useful, but:

theorem trivial_iff_total_and_symm {α : Type u} {r : α → α → Prop} :
  (∀ a b, r a b) ↔ (∀ a b, r a b ∨ r b a) ∧ (∀ a b, r a b → r b a) := by grind

theorem empty_iff_asymm_and_symm {α : Type u} {r : α → α → Prop} :
  (∀ a b, ¬ r a b) ↔ (∀ a b, r a b → ¬ r b a) ∧ (∀ a b, r a b → r b a) := by grind

I think these theorems somewhat characterise how Std.Symm plugs into all this.

[Wrenna Robson]

Though we don't have an Std.Empty and Std.Trivial typeclass, we certainly could.

[Paul Reichert]

Please forgive my delayed answer, but you are raising lots of delicate questions that need serious thought and I don't have ready-made opinions how exactly the trade-off should be for each of them.

Nevertheless, here are my current thoughts:

All these low-level relational type classes can be related to each other in lots of ways, but we cannot and should not encode all of them in the type class hierarchy. (I'd also rather prevent cycles due to their complexity and performance cost, although they aren't a strict show stopper for propositional classes.)

So I think which ones we add should be guided by common use cases in the standard library or practical software verification.

I prefer having instTrichotomousOfTotal over instTotalOfReflOfTrichotomous as an instance. instReflOfTotal is an instance I found very useful in the standard library. As a user, I would be less surprised if Lean failed to automatically combine Refl and Trichotomous into Total, but if it failed to derive something as simple Refl from Total, I would be slightly annoyed.

Regarding Refl.irrefl: I tend to believe that entailments from (¬ r · ·) properties to their equivalent properties stated in terms of r could be useful in order to normalize them. But I wonder whether it wouldn't be even better to avoid Std.Refl (¬ r · ·) at all. The standard library does not use it; are there actual use cases for it?

I tend to think that lemmas, instead of instances, are a good thing in the simple cases, including the ones you proposed. However, I hesitate to add Empty and Trivial classes as long as there is no sufficient evidence that these are needed.

[Wrenna Robson]

I am sorry for raising delicate questions - assuming you meant that as a criticism.

[Wrenna Robson]

Thank you for your thoughtful responses.

[Wrenna Robson]

For what it's worth I also think it would be best to avoid Std.Refl (not etc.) (apologies, am on phone) but as was pointed out above, we do seem to use a similar thing with Std.Antisymm in some places (I'm not sure if that's true in core, however).

[Wrenna Robson]

Can grind use these order typeclass much at all? I don't know enough about if the resulting theorems are suitable to receive appropriate attributes.

Regardless of that I think I have enough information to put hopefully a small PR together.

[Paul Reichert]

Wrenna Robson said:

I am sorry for raising delicate questions - assuming you meant that as a criticism.

Oh, sorry, I didn't mean "delicate" as "taboo" or "provocative" -- merely difficult to answer! Perhaps the wrong word.

[Paul Reichert]

Wrenna Robson said:

Regardless of that I think I have enough information to put hopefully a small PR together.

It would be well-appreciated! :thank_you:

[Wrenna Robson]

Ah I see! I was worried I had inadvertently caused offence, perhaps by pushing at a tension point I was unaware of (I find anything that involves dealing directly with core/the FRO quite stressful in this regard).

[Paul Reichert]

Okay, I really hope that I manage not to make the interactions stressful in the future.

[Wrenna Robson]

How do you feel about Tricho as a name? (Rather than spelling out Trichotomous, which is a mouthful).

[Wrenna Robson]

(Also, some sources have "trichotomous" meaning that exactly one of R a b, a = b and R b a is true, but similarly "strongly connected" is sometimes used to mean what we have defined as "total", where "total" then = "strongly connected partial order".)

[Wrenna Robson]

https://books.google.co.uk/books?id=AInDCgAAQBAJ&pg=PA182&redir_esc=y#v=onepage&q&f=false

[Wrenna Robson]

https://mathworld.wolfram.com/TrichotomyLaw.html

[Wrenna Robson]

I'm not quite sure what to do about this - I don't know if Core has a preferred ground text it uses as the source for its definitions.

[Wrenna Robson]

(Other sources seem to use "connex" and "strictly connex" for what we have here as "total" and "trichotomous".)

[Paul Reichert]

I'm not at all sure, but:

I tend to just call it Trichotomous. The meaning of "trichotomy" is then consistent with Mathlib. Additionally, at least for my feelings, it's not quite as well-known as the axioms of reflexivity, antisymetry and so on, and therefore arguably deserves a less abbreviated and more self-descriptive name. I also hope that the theory of these axiomatic classes does not get so complicated that we need to write Trichotomous all the time. Occasionally writing it out seems okay to me.

[Wrenna Robson]

Yes I have to say I don't personally worry about whether it's "exactly one" or "one".

[Wrenna Robson]

But for instance one could define Std.Trichotomous as a \ne b -> r a b ∨ r b a. It depends what is most useful for core's purpose - which I suppose is the same as "what is most useful for Lean as a programming language"?

[Paul Reichert]

Yes -- perhaps Antisymm-not isn't so bad after all? At least, everybody knows what is meant by it -- at least after processing the double negation :wink:

[Wrenna Robson]

I think it is useful to have a name for it - in the same way that you don't "need" a name for Irrefl but it is clearly useful.

[Wrenna Robson]

But yes - the advantage of using Antisymm (¬ r · ·) as the definition is that it saves on case-splitting on or - or from a programming point of view, it is an easier axiom to use: "if you give me a proof that neither r a b nor r b a, then I can produce a proof that a = b"

[Wrenna Robson]

I wouldn't want to make it an abbrev or anything though - good for it to have its own field name.

[Wrenna Robson]

However, I will say that, on identical logic, ∀ a b, ¬r a b → r b a would be a better definition of Total.

[Wrenna Robson]

Or if you like, "Total" as Asymm (¬ r · ·)

[Wrenna Robson]

(Entirely separately - the fact that Trans is not limited to a propositional class but has a more general definition is somewhat odd to me - but I suppose there are probably good reasons.)

[Ruben Van de Velde]

Using calc with Equivs!

[Wrenna Robson]

Yeah - I just assume you could do a similiar trick with e.g. Symm?

[Wrenna Robson]

But I guess it must not come up.

[Wrenna Robson]

Still, the lack of a Std.Trans might trip/surprise some users.

[Wrenna Robson]

Wrenna Robson said:

However, I will say that, on identical logic, ∀ a b, ¬r a b → r b a would be a better definition of Total.

(Unfortunately I feel like changing the definition of Total would be way too much work overall.)

[Wrenna Robson]

(But it irritates me that we're stuck with an untidy asymmetry - in, ironically, the definition of asymmetry.)

[Wrenna Robson]

Hmm - and actually that asymmetry does seem to lead to problems with inferred instances.

[Paul Reichert]

What do you mean by untidy asymmetry?

[Wrenna Robson]

So I think this is the clear example from what is currently defined.

[Wrenna Robson]

We have

class Total (r : α → α → Prop) : Prop where
  /-- A total relation satisfies `r a b` or `r b a`. -/
  total : ∀ a b, r a b ∨ r b a

and also

class Asymm (r : α → α → Prop) : Prop where
  /-- An asymmetric relation satisfies `r a b → ¬ r b a`. -/
  asymm : ∀ a b, r a b → ¬r b a

However, my argument is that these are dual/complementary properties: in particular, we could take the definition of the latter as

class Asymm (r : α → α → Prop) : Prop where
  /-- An asymmetric relation satisfies `r a b → ¬ r b a`. -/
  asymm : ∀ a b, ¬r a b ∨ ¬r b a

[Wrenna Robson]

Equally we could take the definition of Total as

class Total (r : α → α → Prop) : Prop where
  /-- A total relation satisfies `r a b` or `r b a`. -/
  total : ∀ a b, ¬r a b → r b a

[Wrenna Robson]

Obviously there are lots of relationships between these properties of relations - but in particular these two are analogous to each other.

We were just discussing how it might make sense to take the definition of Tricho as

class Tricho (r : α → α → Prop) : Prop where
  /-- An trichotomous relation `r` satisfies `¬ r a b → ¬ r b a → a = b`. -/
  tricho (a b : α) : ¬ r a b → ¬ r b a → a = b

to as to be analogous to

class Antisymm (r : α → α → Prop) : Prop where
  /-- An antisymmetric relation `r` satisfies `r a b → r b a → a = b`. -/
  antisymm (a b : α) : r a b → r b a → a = b

rather than the equivalent r a b ∨ a = b ∨ r b a.

[Wrenna Robson]

It isn't hard to prove these equivalent, of course, but you can make ergonomic and non-ergonomic choices, I think.

[Wrenna Robson]

I had hoped that suitable instances for the "not" versions would help smooth this out, but now I think that might be problematic even when there aren't loops.

public instance (r : α → α → Prop) [Asymm r] : Irrefl r where
  irrefl a h := Asymm.asymm a a h h

public instance Refl.irrefl_of_refl_not {α : Type u} {r : α → α → Prop} [i : Refl (¬ r · ·)] :
    Irrefl r where irrefl := i.refl

public instance Irrefl.refl_of_irrefl_not {α : Type u} {r : α → α → Prop}
    [i : Irrefl (¬ r · ·)] : Refl r where
  refl a := by simpa using i.irrefl a

public instance {α : Type u} [LT α] [LE α] [LawfulOrderLT α] :
    Asymm (α := α) (· < ·) where
  asymm a b := by
    simp only [LawfulOrderLT.lt_iff]
    intro h h'
    exact h.2.elim h'.1

public instance {α : Type u} [LT α] [LE α] [LawfulOrderLT α] :
    Irrefl (α := α) (· < ·) := inferInstance

I get a problem here (I think this should be a minimal example, at least needing only the prelude of Init.Core): removing either of Refl.irrefl_of_refl_not or Irrefl.refl_of_irrefl_not removes the issue but when both are present it sets up a loop. I guess that makes sense - at least I see the infinite chain it gets stuck down.

[Wrenna Robson]

It somewhat suggests that Std.Total.asymm_of_total_not is a problem instance - or at least, it might be a problem if Std.Asymm.total_of_asymm_not also existed as an instance. Why should one of these be an instance and not the other? I'm struggling to grasp the heuristic.

On some level it feels kind of about "do you think <-like relations or <=-like relations are the more important ones": and I think Lean generally takes the view that <=-like relations are the important ones - but not always!

[Wrenna Robson]

Side point: Std.instIrreflLtOfLawfulOrderLT has a requirement for [IsPreorder α] as currently existant - I believe this is an erroneous over-specialisation, and that is not required. But that could be fixed independently of all of this.

[Wrenna Robson]

(lean4#10941 for that one)

[Paul Reichert]

Wrenna Robson said:

It somewhat suggests that Std.Total.asymm_of_total_not is a problem instance - or at least, it might be a problem if Std.Asymm.total_of_asymm_not also existed as an instance. Why should one of these be an instance and not the other? I'm struggling to grasp the heuristic.

You're right, asymm_of_total_not would not have been a very good instance if not for historical reasons. The only reason it exists is that when I replaced some uses of Total-not with Asymm, I wanted to minimize breakage. There's no reason beyond that, but we shouldn't add more of these...

[Wrenna Robson]

Yes, I think that's certainly true - if anything I would like to find a way to remove that one!

[Paul Reichert]

Wrenna Robson said:

However, my argument is that these are dual/complementary properties: in particular, we could take the definition of the latter as

class Asymm (r : α → α → Prop) : Prop where
  /-- An asymmetric relation satisfies `r a b → ¬ r b a`. -/
  asymm : ∀ a b, ¬r a b ∨ ¬r b a

I'm not sold on the importance of the exact intensional definition of these classes that it would justify making a change. Did it ever really hurt that these definitions aren't perfectly symmetrical? I don't really see the practical problem here.

[Wrenna Robson]

You are probably right - I am quite symmetry-brained :)

[Wrenna Robson]

@Paul Reichert lean4#10945