IsTotal typeclass

Stream: mathlib4

[Violeta Hernández]

A problem came up in #32499. The to_dual tactic can't dualize theorems about IsTotal α (· ≤ ·) properly because it avoids writing IsTotal α (· ≥ ·), instead opting to write IsTotal α fun x y ↦ y ≤ x. This then led us to the question of why even have an IsTotal typeclass instead of just writing IsTotalLE. Such a predicate could then be made its own order dual. Would that be a desirable change?

[Violeta Hernández]

Most uses of IsTotal in Mathlib seem to be about ≤, and of those a large proportion are an intermediate step to building a LinearOrder instance, which suggests it might be convenient to split out this condition from LinearOrder so as to then make LinearOrder extend IsTotalLE.

[Yaël Dillies]

What about introducing LinearPreorder, which is to LinearOrder what Preorder is to PartialOrder? People have been asking for it in the past.

[Violeta Hernández]

Does this come up in practice? If so, then I support this idea (though it does leave the IsTotal typeclass in somewhat of a limbo).

[Yaël Dillies]

Some recent conversation: #Is there code for X? > Linear Preorders and LawfulOrderMin. Can't find the one I was thinking of, though

[Snir Broshi]

btw #30855 (#mathlib4 > Relation properties duplication)