symm & comm

Stream: general

[Yaël Dillies]

symm and comm seem to really be the same thing, but one being about functions α → Prop and the other about functions α → Type*. Why come we, the mathlib people, not have taken this opportunity to unify vocabulary and definitions? Here are a few potential reasons I came up with:

• There are contexts where both are used concurrently and incompatibly. Doesn't seem to be the case?
• The names are pretty anchored in mathematicians' minds so we keep them for historical reason. We took radical solutions in other similar situations (module/vector space, rank/dim...) and I don't think there's that much attachment to the distinction symmetry/commutativity. I found myself trying to use symm for comm or vice versa.
• Nobody yet bothered changing it.

So what should we do?

[Yaël Dillies]

/poll What should happen of symm and comm?
Not change anything
Change all comm to symm
Change all symm to comm

[Kevin Buzzard]

#check eq.symm -- a = b → b = a
#check eq_comm -- a = b ↔ b = a

[Kevin Buzzard]

They are different

[Yaël Dillies]

But they are all defined everywhere? It didn't seem to me.

[Johan Commelin]

It is a common pattern, but there might be some gaps

[Anne Baanen]

Yaël Dillies said:

• We took radical solutions in other similar situations (module/vector space, rank/dim...)

I'd like to caution against inferring a pattern from only this refactor which was done for mostly technical reasons (and I still have fixing the loss of recognizability on my todo list). Having semimodule and vector_space mean something else than module resulted in subtle breakages in the category theory library and workarounds involving re-instantiating the same definition under a different name like here.

[Eric Wieser]

I assume docs#and.symm and docs#and_comm is another example

[Eric Wieser]

If we added a has_coe_to_fun (iff a b) (a -> b) then dot notation would work for comm which would remove the need for symm; but that was met with substantial resistance last time I suggested it due to students already being confused by rw vs apply. I'll try to find that topic, and edit this message with a link when I do.

[Yaël Dillies]

Very interesting! Please tell me more

[Eric Wieser]

Updated with a link to the topic