eq_of_cmp_eq

Stream: batteries

[Kim Morrison]

I would like the typeclass

class FooCmp (cmp : α → α → Ordering) : Prop where
  eq_of_cmp_eq : cmp x y = .eq → x = y

What should it be called?

[James Gallicchio]

in leancolls i started naming these like Lawful<class>.<property; I don't like it or recommend it but have no better suggestions than LawfulCmp.Eq :laughing:

[Kim Morrison]

The problem here is that it is only a small fraction of Lawful.

[Kim Morrison]

We already have TransCmp and OrientedCmp.

[Mario Carneiro]

AntisymmCmp?

[Damiano Testa]

Or InjectiveCmp? :upside_down:

[Eric Wieser]

DistinguishingCmp?

[Eric Wieser]

Do you really not want the typeclass to also require cmp x x = .eq at the same time?

[James Gallicchio]

It seems lake has a typeclass for this? docs#Lake.EqOfCmp

[Eric Wieser]

and docs#Lake.LawfulCmpEq is the version that has the other property I'm suggesting

[Kim Morrison]

Eric Wieser said:

Do you really not want the typeclass to also require cmp x x = .eq at the same time?

So far I've been finding that when I need cmp x x = .eq, I needed OrientedCmp anyway, which implies this.

[Kim Morrison]

But sure, I wouldn't mind either way.