Zulip Chat Archive

Stream: general

Topic: symm & comm

Yaël Dillies (May 26 2021 at 20:20):

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 (May 26 2021 at 20:21):

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

Kevin Buzzard (May 26 2021 at 20:21):

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

Kevin Buzzard (May 26 2021 at 20:21):

They are different

Yaël Dillies (May 26 2021 at 20:22):

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

Johan Commelin (May 26 2021 at 20:24):

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

Anne Baanen (May 27 2021 at 08:11):

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 (May 27 2021 at 08:15):

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

Eric Wieser (May 27 2021 at 08:17):

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 (May 27 2021 at 08:55):

Very interesting! Please tell me more

Eric Wieser (May 27 2021 at 09:05):

Updated with a link to the topic

Last updated: Aug 03 2023 at 10:10 UTC