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.

[Martin Dvořák]

[probably offtopic]

If I have a vector space over a LinearOrderedField, does PosSMulMono imply everything else listed here?

Actually it seems to be documented here:
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Order/Module/Defs.html#Implications

[Scott Carnahan]

I have been experimenting with multiplicative forms of docs#OrderedVAdd and docs#OrderedCancelVAdd but I run into a naming conflict with the existing docs#OrderedSMul. I was considering MonoSMulMono and MonoSMulReflectLE (with additive forms MonoVAddMono and MonoVAddReflectLE). Are there better names?

[Scott Carnahan]

To be honest, I only see a use for docs#OrderedCancelVAdd at this moment because of the nice antidiagonal properties, and the rest came along for the ride.