porting names

Stream: mathlib4

[Scott Morrison]

What is our intention fixing up names from mathports output? e.g. currently mathport changes the typeclass is_empty to IsEmpty (great!), but then leaves the name of lemmas like

theorem is_empty_ulift {α} : IsEmpty (ULift α) ↔ IsEmpty α := ...

as they were.

I'm hoping/proposing that for now we don't manually change the names of these lemmas as porting happens, for compatibility between files.

One day (TM) we can hope for nice code helpers to do renaming across the whole library, right? :-)

[Scott Morrison]

Another view on this question is: should we plan to improve mathport's name translation, or should we declare it canonical for now?

[Mario Carneiro]

there are certainly issues in mathport name translation where it can't possibly know how a name should be chunked up. Common cases of this are when a theorem about my_foo and my_bar was called my_foo_eq_my_bar and the functions were renamed to myFoo and myBar so the theorem should now be myFoo_eq_myBar. Given that there might also be definitions my and foo this is just a fundamentally ambiguous problem

[Mario Carneiro]

check out the names of the lemmas for the interactions of filter, map and filter_map :bangbang:

[Mario Carneiro]

I think we shouldn't gratuitously change the names, but on the other hand if we're going to do a name translation we should be allowed to do it on the spot and accommodate later uses with an #align annotation

[Jireh Loreaux]

Sorry, what is an #align annotation?

[David Renshaw]

see https://leanprover-community.github.io/blog/posts/intro-to-mathport/
and https://github.com/leanprover-community/mathlib4/blob/1203930f75e86aa6260e8c1b9e5b5fbeed7656b7/Mathlib/Mathport/Rename.lean#L34