Lemma names in cauchy_integral.lean

Stream: general

[Mario Carneiro]

oh my goodness there are so many long names in that file

[Yury G. Kudryashov]

Do you have better suggestions?

[Mario Carneiro]

I would try something like cauchy_thm_rect

[Mario Carneiro]

it's a little hard to tell what the distinguishing characteristics of these theorems are, they are all pretty hard to read

[Yury G. Kudryashov]

I assumed that this goes against our naming convention.

[Mario Carneiro]

let's just not use the symbol reading convention for named lemmas then, like I have suggested many times before

[Mario Carneiro]

it has some clear failure modes for theorems like this

[Yury G. Kudryashov]

I'll make a PR that renames lemmas after #11770 will be either accepted or rejected.

[Yury G. Kudryashov]

And I'll request your review.

[Kevin Buzzard]

Mario I remember telling you in 2018 that this silly computer science idea of having a naming convention would never work because beyond some point it gets really complicated. This was back when I knew nothing and was naming things lemma37 (on the basis that this approach had worked for centuries). I must be honest and say that the naming convention idea has scaled far far better than I could ever have imagined.

[Vincent Beffara]

As a beginner it still feels weird to see all these long names, but it seems possible to shorten the names while keeping the naming convention by naming more things (after all you do use differentiable as part of the names and not has_limit_minus_div_minus_along_whatever_filter_or_other). So I guess, say that f is cauchy if it satisfies the Cauchy integral formula and then have cauchy_of_differentiable_off_countable or something? It might be running towards failure in exactly the way that is taken care of by the naming conventions though.

[Yaël Dillies]

This works so far as you don't have too many similar lemmas. Consider for example file#algebra/order/rearrangement. We had to make the names rather explicit to differentiate all variants.