-
Notifications
You must be signed in to change notification settings - Fork 299
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(group_action/defs): add missing comp_hom smul instances #8707
Conversation
…hom`, ring_homs are linear maps
The new instances seem to be creating a loop along with instances further down the import hierarchy, see the linting errors. I've been testing a few files by adding the command #eval tactic.get_decl ``smul_comm_class >>= fails_quickly 3000 >>= tactic.trace which returns |
In fact, running the command in the auto-generated |
I think it might be a reducibility issue. I think if I introduce a semireducible def to wrap the smul field then the problem will go away |
* The problem was that when writing `@[to_additive] def foo ...` every declaration used in `foo` in namespace `foo` would be additivized without changing the last part of the name. This behavior was intended to translate automatically generated declarations like `foo._proof_1`. However, if `foo` contains a non-internal declaration `foo.bar` and `add_foo.bar` didn't exist yet, it would also create a declaration `add_foo.bar` additivizing `foo.bar`. * This PR changes the behavior: if `foo.bar` has the `@[to_additive]` attribute (potentially with a custom additive name), then we won't create a second additive version of `foo.bar`, and succeed normally. However, if `foo.bar` doesn't have the `@[to_additive]` attribute, then we fail with a nice error message. We could potentially support this behavior, but it doesn't seem that worthwhile and it would require changing a couple low-level definitions that `@[to_additive]` uses (e.g. by replacing `name.map_prefix` so that it only maps prefixes if the name is `internal`). * So far this didn't happen in the library yet. There are currently 5 non-internal declarations `foo.bar` that are used in `foo` where `foo` has the `@[to_additive]` attribute, but all of these declarations were already had an additive version `add_foo.bar`. * These 5 declarations are `[Mon.has_limits.limit_cone, Mon.has_limits.limit_cone_is_limit, con_gen.rel, magma.free_semigroup.r, localization.r]` * This fixes the error in #8707 and resolves the Zulip thread https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.238707.20linter.20weirdness * I also added some documentation / comments to the function `transform_decl_with_prefix_fun_aux`, made it non-private, and rewrote some steps.
657c008
to
084ec62
Compare
Co-authored-by: Johan Commelin <johan@commelin.net>
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks 🎉
bors merge
This adds missing `smul_comm_class` and `is_scalar_tower` instances about the `comp_hom` definitions. To resolve unification issues in finding these instances caused by the reducibility of the `comp_hom` defs, this introduces a semireducible def `has_scalar.comp.smul`.
Pull request successfully merged into master. Build succeeded: |
This adds missing
smul_comm_class
andis_scalar_tower
instances about thecomp_hom
definitions.To resolve unification issues in finding these instances caused by the reducibility of the
comp_hom
defs, this introduces a semireducible defhas_scalar.comp.smul
.I'll follow up with a PR about
ring_hom.to_algebra
.