Lean4 lemma names

Stream: general

[Patrick Massot]

@Sebastian Ullrich Unless I misunderstood, in Pittsburgh you told us there was not yet a naming convention for lemma names in Lean 4. But https://github.com/leanprover/lean4/commit/db3d9c9284dfb9b27dfa17214d7c3c2ce7409f08 suggests this is no longer true. Do you have any comment here? My understanding was that we could hope to keep lean 3 underscore separated names.

[Sebastian Ullrich]

@Patrick Massot It's not something we have explicitly decided on yet, at least. We should probably start that discussion by now.

[Patrick Massot]

Great! Can I respectfully suggest another discussion topic that seems timely? As a user and teacher using Lean, it would be nice if intro and cases were the powerfull mathlib versions or if it were possible for mathlib to completely replace the core lib intro and cases without having a different name (and without hacks).

[Mario Carneiro]

One problem is that cases has an incompatible syntax with rcases, so if we replace it then we will need to keep cases_old around or change the formatting everywhere

[Johan Commelin]

Or we make the parser just a bit more complex to figure out which of the two syntaxes is used. Because I think they can be distinguished.

[Patrick Massot]

My hope is it's not too late to change everywhere. I expect there are currently very few proofs using the interactive cases tactic in Lean 4.

[Patrick Massot]

(if any)

[Sebastian Ullrich]

Patrick Massot said:

or if it were possible for mathlib to completely replace the core lib intro and cases without having a different name (and without hacks).

That version sounds reasonable. It's the same customization story we want to have for other parts of the language (commands, terms, ...) as well.

[Patrick Massot]

Indeed, that would be consistent with everything else.

[Patrick Massot]

And that would be the most flexible solution, as planned with the whole Lean 4 story.