Relation properties duplication

Stream: mathlib4

[Snir Broshi]

Mathlib and Std combined have 3 versions of many properties of relations:

	Std class	Mathlib class	Mathlib prop
reflexive relation	docs#Std.Refl	docs#IsRefl	docs#Reflexive
irreflexive relation	docs#Std.Irrefl	docs#IsIrrefl	docs#Irreflexive
symmetric relation	docs#Std.Symm	docs#IsSymm	docs#Symmetric
antisymmetric relation	docs#Std.Antisymm	docs#IsAntisymm	docs#AntiSymmetric
asymmetric relation	docs#Std.Asymm	docs#IsAsymm
total relation	docs#Std.Total	docs#IsTotal	docs#Total
transitive relation	docs#Trans (more generic)	docs#IsTrans	docs#Transitive
equivalence relation	docs#Equivalence (structure)	docs#IsEquiv

There are also classes for orders which were upstreamed to core because of the new grind, although the situation here is different because of bundling:

	Std class using LE	Mathlib class using LE	Mathlib unbundled class
preorder	docs#Std.IsPreorder	docs#Preorder	docs#IsPreorder
partial order	docs#Std.IsPartialOrder	docs#PartialOrder	docs#IsPartialOrder
linear order	docs#Std.IsLinearOrder	docs#LinearOrder	docs#IsLinearOrder

I also found docs#emptyRelation and docs#EmptyRelation.

Some relations have instances/theorems for all classes/props, some only for some:

docs#Eq: Equivalence ✓, IsEquiv ✓
docs#Ne: Std.Irrefl x (docs#Ne.irrefl is close), IsIrrefl x, Irreflexive x, Std.Symm x (docs#Ne.symm is close), IsSymm x, Symmetric x
docs#Iff: Equivalence x, IsEquiv ✓
docs#Relation.ReflGen: Std.Refl x, IsRefl ✓, Reflexive ✓
docs#Relation.TransGen: Trans ✓, IsTrans ✓, Transitive ✓
docs#Relation.ReflTransGen: Std.Refl x, IsRefl ✓, Reflexive ✓, Trans ✓, IsTrans ✓, Transitive ✓
docs#Relation.EqvGen: Equivalence ✓, IsEquiv x

I think we should either fill the missing ones and add instances relating everything (already exist for transitive and the order ones) and theorems for the classes to imply the props (already exist for reflexive and transitive), or deprecate Mathlib's classes and props where possible, or at least document this table somewhere.

Thoughts? I assume this has been brought up before but I couldn't find it.

[Kim Morrison]

The order classes require more discussion (particularly LinearOrder, which is a mess.)

But personally I would be happy to see docs#IsAntisymm deprecated in favour of Std.Antisymm (and similarly for everything in the first table).

[Markus Himmel]

Snir Broshi said:

There are also classes for orders which were upstreamed to core because of the new grind,

Just noting that grind was not the primary motivation for adding these classes. Rather, they were added to support various future standard library developments like consolidating the lemmas for List.min? and adding verified sorting algorithms, binary search, and more. The fact that the classes are useful for grind was more of a happy accident.

[Wrenna Robson]

I'm extremely enthusiastic about tidying up this situation.

[Ruben Van de Velde]

I'm currently working on Total

[Ruben Van de Velde]

Which is now #30855

[Ruben Van de Velde]

If anyone has thoughts on deduplicating relation properties like IsTotal/Std.Total, please have a look at #30855.