Renaming monotonicity of powers lemmas

Stream: mathlib4

[Yaël Dillies]

This is an announcement that #9095 landed. This is a rather disruptive PR since it renamed 58 lemmas that are among the most used in mathlib. If you have a project depending on mathlib, you should check how the lemmas were renamed to adapt.

[Yaël Dillies]

The lemmas in question are all about monotonicity of (a ^ ·) and (· ^ n). The full list of renames by file is

Algebra.GroupPower.Order

• pow_mono → pow_right_mono
• pow_le_pow → pow_le_pow_right
• pow_le_pow_of_le_left → pow_le_pow_left
• pow_lt_pow_of_lt_left → pow_lt_pow_left
• strictMonoOn_pow → pow_left_strictMonoOn
• pow_strictMono_right → pow_right_strictMono
• pow_lt_pow → pow_lt_pow_right
• pow_lt_pow_iff → pow_lt_pow_iff_right
• pow_le_pow_iff → pow_le_pow_iff_right
• self_lt_pow → lt_self_pow
• strictAnti_pow → pow_right_strictAnti
• pow_lt_pow_iff_of_lt_one → pow_lt_pow_iff_right_of_lt_one
• pow_lt_pow_of_lt_one → pow_lt_pow_right_of_lt_one
• lt_of_pow_lt_pow → lt_of_pow_lt_pow_left
• le_of_pow_le_pow → le_of_pow_le_pow_left
• pow_lt_pow₀ → pow_lt_pow_right₀

Algebra.GroupPower.CovariantClass

• pow_le_pow_of_le_left' → pow_le_pow_left'
• nsmul_le_nsmul_of_le_right → nsmul_le_nsmul_right
• pow_lt_pow' → pow_lt_pow_right'
• nsmul_lt_nsmul → nsmul_lt_nsmul_left
• pow_strictMono_left → pow_right_strictMono'
• nsmul_strictMono_right → nsmul_left_strictMono
• StrictMono.pow_right' → StrictMono.pow_const
• StrictMono.nsmul_left → StrictMono.const_nsmul
• pow_strictMono_right' → pow_left_strictMono
• nsmul_strictMono_left → nsmul_right_strictMono
• Monotone.pow_right → Monotone.pow_const
• Monotone.nsmul_left → Monotone.const_nsmul
• lt_of_pow_lt_pow' → lt_of_pow_lt_pow_left'
• lt_of_nsmul_lt_nsmul → lt_of_nsmul_lt_nsmul_right
• pow_le_pow' → pow_le_pow_right'
• nsmul_le_nsmul → nsmul_le_nsmul_left
• pow_le_pow_of_le_one' → pow_le_pow_right_of_le_one'
• nsmul_le_nsmul_of_nonpos → nsmul_le_nsmul_left_of_nonpos
• le_of_pow_le_pow' → le_of_pow_le_pow_left'
• le_of_nsmul_le_nsmul' → le_of_nsmul_le_nsmul_right'
• pow_le_pow_iff' → pow_le_pow_iff_right'
• nsmul_le_nsmul_iff → nsmul_le_nsmul_iff_left
• pow_lt_pow_iff' → pow_lt_pow_iff_right'
• nsmul_lt_nsmul_iff → nsmul_lt_nsmul_iff_left

Data.Nat.Pow

• Nat.pow_lt_pow_of_lt_left → Nat.pow_lt_pow_left
• Nat.pow_le_iff_le_left → Nat.pow_le_pow_iff_left
• Nat.pow_lt_iff_lt_left → Nat.pow_lt_pow_iff_left

[Yaël Dillies]

On top of that, the following lemmas were removed:

• self_le_pow was a duplicate of le_self_pow.
• Nat.pow_lt_pow_of_lt_right is defeq to pow_lt_pow_right.
• Nat.pow_right_strictMono is defeq to pow_right_strictMono.
• Nat.pow_le_iff_le_right is defeq to pow_le_pow_iff_right.
• Nat.pow_lt_iff_lt_right is defeq to pow_lt_pow_iff_right.

[Yaël Dillies]

And finally:

• Some lemma assumptions have been turned from 0 < n or 1 ≤ n to n ≠ 0.
• A few Nat lemmas have been protected.

[Yaël Dillies]

There are other changes that are non-breaking that you can look up in #9095 if you're interested.

[Yaël Dillies]

I should remind you that the information of what lemma has been changed in what PR is available in the #changelog. The changelog does not however contain lists of renames.

[Johan Commelin]

Thanks for clearly documenting the changes!

[Tudor achim]

Just curious, what is the benefit of these changes? The cost of the change is substantial since existing non-mathlib codebases have to be refactored, and muscle memory needs to be re-trained. In this case the lemmas seem to be among the most-used in mathlib which is especially rough.

And if renames are necessary, it seems that an alternative that should be considered is leaving the old lemmas in place as aliases for the new lemmas, possibly with a deprecation attribute or something of the sort. It would be great to introduce those for this change if possible. That way there's a smooth off-ramp from the old lemmas to the new ones.

[Jireh Loreaux]

@Alex J. Best I meant to send this earlier, but got caught during the Zulip outage. This PR would be an ideal test candidate for evaluating Leaff's renaming detection. It would be awesome if you could generate the list that Yaël created manually above automatically from Leaff.

[Johan Commelin]

@Tudor achim Thanks for posting. You are right, and I think mathlib might need to start thinking about these issues. In general, I think we are quite unaware of all the projects that depend on mathlib. So it's good that you tell us about such examples.
I'm optimistic that in the near future we will have much better tooling around such renames.
Already the latest Lean release seems to have brought us functionality for automatically renaming declarations. If we can run that in batch mode, and those batches can be scripted, then these transitions should become almost painfree.

[Yaël Dillies]

In that specific case, my motivation was that the lemma names were all over the place and as a result it was impossible to infer what the name of a lemma is going off the name of a similar lemma, and in fact some of those similar lemmas were missing!

[Ruben Van de Velde]

And in particular, mathlib strongly leans on "guessability" of names, so there's also a cost to having inconsistent names. That doesn't mean we can't have a deprecation period, though

[Johan Commelin]

Certainly! We shouldn't stop making these changes. But we can try to be a bit less disruptive, in support of other projects depending on mathlib.

[Yaël Dillies]

I know there's a new deprecation feature, but it's a bit unergonomic to use within mathlib since it throws warnings on uses of the deprecated lemmas, and mathlib CI errors on warnings.

[Mario Carneiro]

well yeah, mathlib should not have warnings in itself, doesn't mean it shouldn't flag deprecations for downstream use

[Mario Carneiro]

besides you can always suppress the deprecation warning if you can't be bothered / it's a larger project to update mathlib itself after a deprecation

[Mario Carneiro]

certainly if this is pushing you to just remove instead of deprecate then it's the wrong reaction

[Yaël Dillies]

How can I suppress the deprecation warning? With a nolint?

[Mario Carneiro]

the linter warning should tell you the name of the linter to disable

[Mario Carneiro]

if it's the kind of warning that pops up immediately rather than at the end of the build with #lint, you suppress it using set_option linter.foo false in

[Mario Carneiro]

all linter warnings (including the unused variable linter) can be suppressed in this way

[Yaël Dillies]

Yes but that involves disabling the linter of $n$ declarations where $n$ is the number of downstream uses. When I first heard of the deprecation tool, I was hoping this meant I could touch $0$ (zero) declarations downstream while still saying "you shouldn't use this lemma, but that one instead".

[Johan Commelin]

I think the workflow should be something like:

1. Rename a lemma, and tag it with @[old_name foo_bar].
2. The attribute creates an alias, and deprecates the old name in favour of the new name.
3. mathlib has a boatload of warnings
4. automatic tooling fixes all those warnings to switch over to the new names
5. PR
6. a week later: remove all the @[old_name] attributes.

[Mario Carneiro]

what the heck kind of deprecation is that @Yaël Dillies

[Mario Carneiro]

the whole point is to get the downstream uses to use something else

[Yaël Dillies]

Listen, the way I do refactors is

1. Shuffle many lemmas around, possibly leaving duplicates for me to clean up afterwards
2. Fix the downstream uses

[Mario Carneiro]

okay?

[Mario Carneiro]

warnings don't break the build

[Yaël Dillies]

Each step is a sufficiently hard to review PR on its own. I don't want to mix the steps together.

[Mario Carneiro]

at least they shouldn't

[Yaël Dillies]

Mario Carneiro said:

warnings don't break the build

Sorry, what??

[Mario Carneiro]

they make CI fail but it should still produce oleans and such

[Yaël Dillies]

All I'm complaining here is that @[deprecated] doesn't naturally let me split steps 1 and 2 into two PRs.

[Mario Carneiro]

Sure it does, step 1 can not deprecate the old declaration and just have both

[Yaël Dillies]

I'm not a super big fan of this, but if the PR deprecating them comes around quickly I guess it's alright.

[Mario Carneiro]

Johan Commelin said:

6. a week later: remove all the @[old_name] attributes.

I would really like us to start thinking on a time scale more like 3 months for this kind of thing

[Johan Commelin]

also fine with me

[Mario Carneiro]

this is the kind of thing that gives mathlib a bad name

[Johan Commelin]

week was a meta-syntactic variable in that step (-;

[Yaël Dillies]

FWIW, I'm happy with having a long list of @[deprecated] alias for a long time.

[Mario Carneiro]

The thing is, deprecation and migration are aspects of library design too, and they actually take work to achieve

[Yaël Dillies]

The amount of work I spent in my PR description is probably no less than what it would have taken me to deprecate. Migration I don't know.

[Mario Carneiro]

Right now our best tools for migration are tied up in deprecations

[Mario Carneiro]

Maybe we want a @[soft_deprecated] which is a info message instead of a warning, this should fix the issue with breaking CI since noisy files also cause CI to fail but lake will run to completion

[Newell Jensen]

Mario Carneiro said:

this is the kind of thing that gives mathlib a bad name

blasphemy! ... :grinning_face_with_smiling_eyes:

[Yaël Dillies]

Yes, that would be an improvement as I could then fix all of mathlib in one go instead of many

[Mario Carneiro]

seems like a hack around our current tools though, I wouldn't want to actually have users dealing with that

[Mario Carneiro]

deprecations are morally warnings

[Yaël Dillies]

No but I mean I could @[soft_deprecated] all the lemmas I want, build mathlib, remove all downstream uses, replace all the @[soft_deprecated] with @[deprecated].

[Mario Carneiro]

right, I was imagining exactly that workflow

[Mario Carneiro]

unfortunately it doesn't help consumers that are also big projects

[Newell Jensen]

Does mathlib have some sort of stable release schedule? From what it seems most of the tagged releases are from toolchain updates.

[Mario Carneiro]

It has a version compatible with each lean stable release, but it doesn't have stable releases in the "stable" sense

[Yaël Dillies]

Mario Carneiro said:

unfortunately it doesn't help consumers that are also big projects

Then maybe the solution is to have a lake flag for warning/info on deprecation?

[Mario Carneiro]

I think lake should just not stop on warnings-as-errors

[Yaël Dillies]

That's a fair position. I always found that a bit surprising.

[Mario Carneiro]

it's a very low effort implementation

[Yaël Dillies]

It would also be interesting to have an extra date argument to @[deprecated] so that a bot can watch for them and send a reminder $n$ months later "Those lemmas have been deprecated for a long time. Should we delete them?" (and also for general information of the source code readers).

[Mario Carneiro]

it literally just turns all warning messages into error messages, with all the downstream effects of an error message on the server and lake

[Mario Carneiro]

yes the whole thing could be redesigned, someone needs to look into how other languages do it

[Yaël Dillies]

Without that bot checking for long-deprecated lemmas, I would be a bit wary of using @[deprecated].

[Mario Carneiro]

since := NNN is part of most deprecation mechanisms I know

[Mario Carneiro]

or will_be_removed_in := NNN

[Yaël Dillies]

Also, do deprecated lemmas show up in search tools like rw?, apply?, exact? and the docs?

[Mario Carneiro]

I think so

[Mario Carneiro]

every such tool has to implement this kind of logic independently so it's very haphazard what is checked

[Yaël Dillies]

Okay, docs#and_assoc' does show up the docs with a @[deprecated and_assoc] tag, but it's not as flashing yellow as I would have wanted it to.

[Mario Carneiro]

there are half a dozen isInternal or isBlacklisted functions in lean+mathlib

[Mario Carneiro]

that also relates to the fact that there is no generic way to show attributes on a definition like lean 3 #print

[Mario Carneiro]

so every such metaprogram has to go and query every attribute it cares about, and since this is extensible in both programs and attributes you can see why this is difficult to arrange

[Yaël Dillies]

I should also say I have many other breaking refactors underway and I am willing for them to be the testing ground of any deprecation/migration method we come up with.

[Mario Carneiro]

I think we need a holistic proposal for how deprecation is supposed to work, what the attribute looks like, the code action, auto fix etc

[Yaël Dillies]

Mario/Johan, would you welcome a PR that turns the PR description of #9095 into a long list of @[deprecated] alias in the relevant files?

[Yaël Dillies]

(for the lemmas whose old name hasn't been taken by a new lemma)

[Johan Commelin]

I don't want to push you to do that work now. But if you do it, I'm happy to merge that PR

[Johan Commelin]

Yaël Dillies said:

(for the lemmas whose old name hasn't been taken by a new lemma)

This is also something that the holistic deprecation proposal should address.

[Yaël Dillies]

It should be pretty easy. Let's try.

[Yaël Dillies]

I've just deprecated my first ever lemmas in #9219.

[Thomas Murrills]

For documentation purposes, it would be nice for the deprecated attribute to be able to store a blurb on why something was deprecated, even if it’s just a link to a PR or issue. (Ideally it would be a little bit more.) :)

[Johan Commelin]

The value of deprecated since should ideally be updated just before the PR is merged by bors...

[Johan Commelin]

@Thomas Murrills you can already give a string argument, if you want to

[Thomas Murrills]

Ah, I’ve just never seen that string argument used, so I assumed it didn’t exist :sweat_smile:

[Yaël Dillies]

Johan Commelin said:

The value of deprecated since should ideally be updated just before the PR is merged by bors...

Yes, although I think it's fine if the date is off by a few days. It's not like huge refactor PRs sit around for a long time anyway.

[Thomas Murrills]

What would the value of since be, in general? A date, a PR number, a commit…? (All three?)

[Yaël Dillies]

#9235

[Mario Carneiro]

PR number sounds like the most reliable

[Mario Carneiro]

I think we could still make a script to find old deprecations with only PR numbers to go by

[Yaël Dillies]

And then we say something like "The deprecation period is 3000 PRs long"?

[Thomas Murrills]

If we stored time as well, and if each mathlib commit somehow knew the time at which the commit itself was committed, we wouldn’t need soft_deprecated: we could calculate the amount of time from the deprecation to the current commit you were on, and decide to either log info or warn based on the result.

E.g. log “this declaration will be deprecated in the version of <project> released <x> days after the current version” where x = deprecationTime + gracePeriodDuration – projectCommitTime (where here mathlib is the project). If x ≤ 0, you get a warning instead.

(Maybe there are reasons not to want this behavior, but just putting it out there as an idea.)

[Johan Commelin]

@Mario Carneiro Can you tell me whether there is now a way to do batch renames? Can we give Lean or VScode or the LSP a dictionary of names mapping to new names , and it will just update all of mathlib to use those new names?

[Eric Wieser]

Mario Carneiro said:

Maybe we want a @[soft_deprecated] which is a info message instead of a warning

Python has PendingDeprecationWarning for this

[Eric Rodriguez]

I guess the way to deprecate lemmas that have a name that is then used elsewhere is to have a special deprecation attribute that only comes up if there's an error applying the lemma (e.g. if there's a type error applying the lemma/a rw doesn't work/etc, it can say 'you may be wanting lemma X, which was recently renamed from this')

[Tudor achim]

To me, mathlib feels like the standard library of other languages (and less like functionality-specific libraries that developers build around the core language). Generally speaking, standard libraries rarely if ever undergo breaking API changes outside of major version bumps. This includes both renaming things as well as changing API type signatures in a breaking way. The counterargument to this, of course, is that the mathlib library is significantly more complex than the stdlib of any major language, and it's also early days, so it's natural that there should be more breaking changes otherwise the long-term potential of the library is diminished. I don't think anybody would argue this point.

I would suggest the following principles:

1. If a function or definition exists in a given mathlib master commit without the deprecated tag, it is guaranteed to be preserved (with the exact module/name/type signature) for at least 6 months. However, it may later be tagged as deprecated.
2. If a function is deprecated, that means that it cannot be used elsewhere in mathlib, which ensures that it doesn't propagate to the core codebase in ways that other people would pattern match on. So it is the responsibility of someone deprecating functions to replace them in the rest of mathlib.
3. Over time, as the library matures and design patterns are solidified, I think it's reasonable to increase the 6 month window to something on the order of several years (but likely not beyond).

Following these principles would provide a much more stable platform to build on, and I think they, in spirit, capture the key points of the discussion above.

There was a suggestion in the thread about deprecating more quickly and providing migration tools to keep up -- just note that these can be serious papercuts to impose on a user community (e.g. even python's 2to3 was pretty annoying to use, speaking from personal experience). I think for folks working on mathlib who are very familiar with these things they don't seem like a big deal, but as the popularity of mathlib keeps growing, there will be lots of users for whom it will be a turnoff to have to regularly run housekeeping scripts on their repos.

[Tudor achim]

As a test case, in this specific instance, would it be acceptable to open a PR to reintroduce those functions with whatever deprecated tag is most appropriate? I'd be happy to handle that.

[Johan Commelin]

@Tudor achim thanks for your thoughts. @Yaël Dillies also offered to add back the functions, together with deprecated tags. I'll be happy to merge that PR.

[Yaël Dillies]

I don't think deprecation even makes sense for most of mathlib. Many parts of the library are leaves that are under active development, and each lemma can change many times in a few months. In contrast, the lemmas that I renamed here are part of the algebraic order hierarchy, which is very central.

[Yury G. Kudryashov]

I opened a new topic for the discussion about backward compatibility of mathlib: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Backward.20compatibility

[Eric Rodriguez]

(also, @Joachim Breitner, when will loogle be updated? It doesn't have the new lemma names yet)

[Yuyang Zhao]

I recall that I have an ancient mathlib3 PR that uses ₚ suffixes for some lemmas with positivity assumptions. I felt this looks better than suffixes like ' and _of_pos_of_nonneg.

[Yaël Dillies]

Sadly, many search tools don't support unicode, so I think it would in practice be a downgrade.

[Eric Rodriguez]

I disagree and think it would be a strong upgrade. ' is unsearchable anyways, and searching for _of_blah sucks

[Yaël Dillies]

The other thing is that _of_pos and _of_nonneg are sometimes good ways to disambiguate similar lemmas.

[Yury G. Kudryashov]

E.g., I think that we should have many versions of docs#mul_lt_mul

[Yury G. Kudryashov]

And of_le_of_lt/of_lt_of_le/..., possibly with extra of_pos/of_nonneg seem like a good way to disambiguate.

[Yuyang Zhao]

I came up with this idea inspired by the suffix ₀ (also a unicode).

[Yuyang Zhao]

Another motivation is that lemmas like docs#mul_lt_mul_of_nonneg_of_pos and docs#mul_lt_mul_of_le_of_lt' have inconsistent names. Using the suffix p allows them to have consistent names with no more than one ', and can clearly distinguish docs#mul_lt_mul_of_le_of_lt which does not require positivity assumptions.

[Yuyang Zhao]

#782 is the old synchronizing PR, I'll make a new one.

[Yaël Dillies]

Please don't! I am halfway through a PR touching those lemmas.

[Eric Rodriguez]

Yael, if you are doing this already, can we at least add aliases with names of that form? I think it's very valuable, and aliases are _cheap_

[Yuyang Zhao]

I think I kept the original name as an alias in my previous PR. No, but most of them.

[Joachim Breitner]

Eric Rodriguez said:

(also, Joachim Breitner, when will loogle be updated? It doesn't have the new lemma names yet)

Manually, once in a while. Thanks for the ping :-)

I should automate it if course eventually.

[Yuyang Zhao]

It looks like some inconsistent names and wrong names like docs#mul_lt_mul_of_le_of_le' are not kept. In any case I can wait for the other changes to be done first. I'm in no hurry to change it. I already have several PRs that have been there for more than 6 months.

[Yuyang Zhao]

#9249 In fact, nothing in mathlib has been broken.

upd: Wait, I may have misunderstood. But I can wait for other PRs anyway.

[Tudor achim]

@Yaël Dillies , just to confirm, are you currently making a PR to mathlib to reintroduce those lemmas as aliases that are marked deprecated? If you guys want to defer this decision until later that's also totally cool, just trying to plan out some things internally.

[Yaël Dillies]

Yaël Dillies said:

#9235

Yes, see :wait_one_second: