Typeclasses for reflecting order

Stream: mathlib4

[Yaël Dillies]

I think I've just put the finger on one of the things I find weird about the Covariant/Contravariant business. I can justify the existence of

abbrev PosMulMono : Prop := CovariantClass α≥0 α (fun x y => x * y) (· ≤ ·)
abbrev MulPosMono : Prop := CovariantClass α≥0 α (fun x y => y * x) (· ≤ ·)
abbrev PosMulStrictMono : Prop := CovariantClass α>0 α (fun x y => x * y) (· < ·)
abbrev MulPosStrictMono : Prop := CovariantClass α>0 α (fun x y => y * x) (· < ·)

[Yaël Dillies]

But I can't justify the existence of the other four:

abbrev PosMulReflectLT : Prop := ContravariantClass α≥0 α (fun x y => x * y) (· < ·)
abbrev MulPosReflectLT : Prop := ContravariantClass α≥0 α (fun x y => y * x) (· < ·)
abbrev PosMulMonoRev : Prop := ContravariantClass α>0 α (fun x y => x * y) (· ≤ ·)
abbrev MulPosMonoRev : Prop := ContravariantClass α>0 α (fun x y => y * x) (· ≤ ·)

[Yaël Dillies]

@Damiano Testa, is there really a situation where "reverse monotonicity" (f a < f b → a < b) is not deducible from linearity of the order + monotonicity (b ≤ a → f b ≤ f a)?

[Yaël Dillies]

I've tried looking for use cases in mathlib and none showed up

[Floris van Doorn]

the complex numbers with the evil order (a <= b iff a.im = b.im and a.re <= b.re) satisfies all these classes, I believe.
Now I'm not sure if that actually is used in mathlib, but I expect that are natural non-linear orders that also satisfy it.

[Yaël Dillies]

Oh! Good point

[Floris van Doorn]

And I think it's good if the Co(ntra)variant classes are also usable in rare cases: they are already a layer more explicit than the bundled classes like LinearOrderedRing and friends.

[Yaël Dillies]

The context is that today is the day I've decided I was done with docs#OrderedSMul, so I'm copying all the covariant/contravariant machinery from * to •

[Martin Dvořák]

I find OrderedSMul cumbersome, too.