coe_add

Stream: mathlib4

[Kenny Lau]

import Mathlib

example (I : Ideal ℝ) (x y : I) : (x + y).val = x.val + y.val := by
  simp? [-Submodule.coe_add, -AddMemClass.coe_add]

These two names seem suboptimal, didn't we have Subtype.coe_add at one point? Also with the current de facto standard I would have assumed that it would be Subtype.add_coe?

[Kenny Lau]

@Yaël Dillies you probably have something to say about this

[Edison Xie]

Does rfl work?

[Kenny Lau]

@Edison Xie not for rw purposes

[Edison Xie]

Ideal is defeq to submodule so Submodule.coe_add should just work?

[Floris van Doorn]

I don't think that coe as postfix in names is the standard?

[Kenny Lau]

It's de facto standard

[Kenny Lau]

Edison Xie said:

Ideal is defeq to submodule so Submodule.coe_add should just work?

I'm saying that it shouldn't be in the Submodule namespace because it puts extra work on the user to figure out which add-submonoid-class the user happens to be in

[Kenny Lau]

Floris van Doorn said:

I don't think that coe as postfix in names is the standard?

when 1000 lemmas all have coe as postfix (because of simps), then the user (i.e. me) will learn that coe goes at the end. It is not reasonable to expect otherwise.

[Aaron Liu]

Kenny Lau said:

It's de facto standard

I don't think I've ever seen it with coe as postfix, can you point to some theorems that are named like that?

[Edison Xie]

Kenny Lau said:

Edison Xie said:

Ideal is defeq to submodule so Submodule.coe_add should just work?

I'm saying that it shouldn't be in the Submodule namespace because it puts extra work on the user to figure out which add-submonoid-class the user happens to be in

Is there not Ideal.coe_add or similar lemmas? If not we should probly have them

[Kenny Lau]

Aaron Liu said:

I don't think I've ever seen it with coe as postfix, can you point to some theorems that are named like that?

https://loogle.lean-lang.org/?q=%22_apply_coe%22%2C+Subtype.val+_+%3D+_

[Kenny Lau]

and https://loogle.lean-lang.org/?q=%22_coe%22%2C+DFunLike.coe+_+%3D+_ with coeFn instead of Subtype.val

[Floris van Doorn]

Kenny Lau said:

Floris van Doorn said:

I don't think that coe as postfix in names is the standard?

when 1000 lemmas all have coe as postfix (because of simps), then the user (i.e. me) will learn that coe goes at the end. It is not reasonable to expect otherwise.

Probably Mathlib is inconsistent, but it's hard to say it's the standard. coe is configured as a prefix for 43 structures/classes in Mathlib (search as_prefix coe). Also, I find ~484 result where coe is probably a prefix (search ^lemma[a-zA-Z_. ]*[ .]coe_) and ~130 where it is probably a postfix (search ^lemma[a-zA-Z_. ]*_coe including trailing space)

[Floris van Doorn]

(Loogle also gives twice as many results for "coe_" as for "_coe")

[Kenny Lau]

ah, maybe it's because we interact with different typeclasses, and the ones I interact with have not configured coe to be prefix?

[Kenny Lau]

I'm just saying that I see coe as postfix all the time

[Floris van Doorn]

Yes, there are plenty that are not configured as prefix as well. Feel free to add as_prefix coe to more initialize_simps_projections commands (With deprecations).

[Kenny Lau]

I think there's an ongoing discussion about this so I don't think I should just suddenly make a PR in the middle of that

[Floris van Doorn]

for projection notation I agree that there is a discussion. I don't think for coercions there is anyone proposing that it should be a postfix(?)

[Kenny Lau]

no, again I'm saying that that's a pattern I have learnt from interacting with mathlib theorems

[Kenny Lau]

and, coe is a projection

[Andrew Yang]

coe is not a field in the structure so it is not the projection. The projection is carrier/val.

[Andrew Yang]

The notation also comes before the argument so under every convention that has appeared in that thread coe should be a prefix.

[Kenny Lau]

"_apply_coe" is a common pattern, see https://loogle.lean-lang.org/?q=%22_apply_coe%22

[Kenny Lau]

I retract my point above about coeFn, but apply_coe still stands

[Jireh Loreaux]

Kenny, this just needs as_prefix coe, please add it wherever you note that it's missing.

[Kenny Lau]

Doesn't this lead to 1000's of deprecations

[Jireh Loreaux]

Yes, perhaps. Maybe @Thomas Murrills is interested in writing some meta code to auto generate the necessary deprecations? I think he mentioned this in a another thread.

[Kenny Lau]

yeah, so I don't think I should do it

[Thomas Murrills]

I think it might be reasonable (and easiest) to simply extend the initialize_simps_projections syntax to allow something like as_prefix (since := "<date>") coe (or something more explicit that mentions deprecation, if desired), and perform the deprecation within @[simps] (rather than having separate deprecations).

Happy to PR this code so it can be used when relevant! :) (I’ll personally remain silent on whether it should actually be used here, though—not my area of expertise. :grinning_face_with_smiling_eyes:)

[Jireh Loreaux]

I think incorporating the deprecation into simps is not ideal. It widens the surface of the deprecation code, and then that won't be caught by the new auto-removal of old deprecations. I think the ideal thing would be to use something like Leaff to determine all the moves automatically, and then generate the deprecations from that diff. However, I'm not sure Leaff is even usable currently.

[Thomas Murrills]

It can definitely be caught by auto-removal of deprecations, simply by extending what that code removes!

Not sure what you mean by “widens the surface of the deprecation code” here?

[Jireh Loreaux]

Thomas Murrills said:

simply by extending what that code removes!

Right, but then you are making extra work.

Thomas Murrills said:

Not sure what you mean by “widens the surface of the deprecation code” here?

I mean there is more code that implements deprecations, so that there are more things that need to be changed when you modify deprecation code.

This idea of changing the simps code in my mind totally violates the principle that tools should do one thing and do it well. simps is for generating simp lemmas, not for generating deprecations. But having said my piece, I'll shut up and let someone else agree or disagree with you about this. At the very least, I'm not offering to implement it myself and you (I think) are, so your opinion probably matters a bit more.

[Aaron Liu]

I feel like @[simps] isn't even good at making simp lemmas

[Thomas Murrills]

I do want to understand what you’re saying, because maybe you’re right, and I haven’t considered something! :grinning_face_with_smiling_eyes: I am just a bit confused about what you mean by “when you modify deprecation code” here. Are you still talking about deprecation removal, or does “deprecation code” mean the API for marking something as deprecated itself? (Which I didn’t get the sense was unstable—is it?)

[Jireh Loreaux]

Right, I mean that if we allow deprecations to do more sophisticated things, e.g., something more than just date tracking and referencing the replacements, then we'll need to update that in the simps code too, which is weird. At the moment, the deprecation API is not unstable, but that doesn't mean we won't change it or improve it.

[Thomas Murrills]

A couple points, just to put them out there:

• The extra work for adjusting deprecation removal code is real, but (if I’m right about how it’s implemented!) quite small. We should definitely take care to adjust both at once, though.
• Deprecating inside @[simps] means that downstream libraries using it get deprecations for free! :)
• To my mind, if a tool gives one the ability to manage the generation of lemmas, it’s reasonable for it to give one the ability to manage changes in the generation of lemmas too. I’m not so much intending to disagree with the philosophy you put forward here, as with the notion that deprecation shouldn’t be considered part of the “thing” it’s doing—especially because all the information necessary for name generation and the information of which declaration replaces which other one is present inside simps. It’s kind of awkward and difficult (and therefore not as maintainable, in some ways) to try to infer that information from outside simps.

[Thomas Murrills]

Jireh Loreaux said:

Right, I mean that if we allow deprecations to do more sophisticated things, e.g., something more than just date tracking and referencing the replacements, then we'll need to update that in the simps code too, which is weird. At the moment, the deprecation API is not unstable, but that doesn't mean we won't change it or improve it.

Ah, okay. I agree, then—I think considering long-term changes here is important!

What if we passed the full deprecation attribute syntax to initialize_simps_projections? Then, presumably, it would be as easy to update as every other instance of the syntax, and not require changes to simps (which would just be passing the attribute syntax along). Ah, we’d need some placeholder for the name if we did this, which is ugly. Perhaps passing components of the syntax is enough, and simps could still simply pass it along, in such a way that it’s not too costly to keep it in sync if the syntax changes or is extended. This lowers the cost, but you’re right that it’s still an extra cost, then.

My sense is that this infrequent maintenance cost is worth it to have the tool be a “good citizen” about taking responsibility for the declarations it creates, but it’s fair for opinions to differ here. :)

[Damiano Testa]

I did not understand what the suggestion about deprecations is, but the code that auto-removes them uses that a declaration has been added to the deprecation extension and the date that is present there. Is the issue that these deprecations would not have a date associated to them?

[Ruben Van de Velde]

Rather that it's new syntax for the tool to deal with, perhaps

[Damiano Testa]

The tool does not inspect the syntax, it inspects the environment that is present with import Mathlib.

[Ruben Van de Velde]

The removal does eventually happen at the level of bytes in a file, though

[Damiano Testa]

Yes, the code finds the deprecations and the ranges of the corresponding declarations from the environment and then removes those ranges from the files.

[Damiano Testa]

If the range assignments are handled correctly, then the deprecations should be removed.

[Damiano Testa]

Having said that, I am also aware that all automated software has plenty of bugs, so it would definitely require making sure that it really works! :slight_smile: