Unifying relation typeclasses

Stream: mathlib4

[Violeta Hernández]

Hopefully I'm not opening Pandora's box here, but I think we have somewhat of an unfortunate situation around unbundled relation typeclasses. Instead of having one single spelling, we seem to have three spellings used throughout different parts of Lean/Mathlib.

a) What appears to be the most common one, the docs#IsRefl, docs#IsIrrefl, etc. typeclasses defined in Mathlib.Order.Defs.Unbundled.
b) The predicates docs#Reflexive, docs#Irreflexive, etc. also defined lower in the file, which see some but seemingly not nearly as much use.
c) The Core typeclasses docs#Std.Refl, docs#Std.Irrefl, etc. which see zero use in Mathlib.

This became a particular annoyance to me recently, when I found out I couldn't use the new List.le lemmas in Core because there's no useful instances for the Std typeclasses they use.

[Violeta Hernández]

Personally I think the predicates from (b) can just be deprecated, since using a typeclass rather than a "raw" proposition provides useful functionality (for instance, one can use theorems about List.sort (· < ·) or List.sort (· ≤ ·) and have transitivity inferred). Whether we replace the core predicates by the Mathlib ones or the other way around I don't really care for.

[Robin Arnez]

I feel like this is also important for #mathlib4 > Simp turning `≠` into `¬ =` if we want a Not.symm in core (for which we would have to have a Std.Symm class in core). I think due to how it was handled with IsAssociative / Std.Associative it's probably reasonable to move over to the Std variants and deprecate IsRefl / IsSymm / etc. Regarding b) we'd probably just want Std.refl_iff etc. and then the need for such predicates decreases significantly

[Markus Himmel]

I think core would also be happy with having the Is* classes in core and deprecating the Std.* names if mathlib prefers that.

[Robin Arnez]

Yeah you're right that would probably cause less impact on mathlib

[Robin Arnez]

Hmm one relevant difference between them though is that IsRefl takes the type as a explicit parameter and Std.Refl as an implicit