Zulip Chat Archive

Stream: general

Topic: semireducible non-instances


Junyan Xu (Oct 09 2022 at 18:31):

#15681 fails linting because it uses two semireducible defs to define two instances:

Error: homotopy_group.group - This instance contains the declarations [equiv.group], which are semireducible non-instances.
Error: homotopy_group.comm_group - This instance contains the declarations [eckmann_hilton.comm_group, _private.1983293365.aux_group], which are semireducible non-instances.

I've tried local attribute [reducible] equiv.group eckmann_hilton.comm_group, then #lint succeeds within the section but fails once placed outside of the section. I've also tried @[inline] which seems to have no effect. Should I:

  • Add @[nolint check_reducibility] to the two instance declarations homotopy.group.comm_group;
  • Make equiv.group and eckmann_hilton.comm_group globally reducible;
  • or is there a better solution?

Floris van Doorn (Oct 09 2022 at 21:01):

#15681

Floris van Doorn (Oct 09 2022 at 21:05):

docs#eckmann_hilton.comm_group should 100% be reducible. If it is not, I'm quite sure that type-class inference doesn't know that the multiplication in comm_group (π_(n+2) X x) and the multiplication in group (π_(n+1) X x) are definitionally equal, which is (obviously) problematic.

Floris van Doorn (Oct 09 2022 at 21:07):

docs#equiv.group might be fine semireducible: assuming you don't define a homotopy_group.monoid or homotopy_group.semigroup or homotopy_group.has_mul or something, then it doesn't hurt to nolint it. However, it also doesn't hurt (much) to make it reducible...

Floris van Doorn (Oct 09 2022 at 21:09):

Btw: the reason that the linter complains even if you change the reducibility locally is because the linter is intended to be a global-coherence linter: it needs to check if in other files two instances (like homotopy_group.group and homotopy_group.comm_group have unifiable fields).

Junyan Xu (Oct 10 2022 at 03:48):

Thanks for your input. It turns out the is a solution (or hack?) in earlier code which I thought was unnecessary repetition but in fact does work to as a way to appease the linter: simply make an auxiliary definition

@[reducible] def comm_group_aux : comm_group (π_(n+2) X x) :=
@eckmann_hilton.comm_group ...

and then

instance comm_group : comm_group (π_(n+2) X x) := comm_group_aux

then the linter no longer complains. I'm not sure whether everything is actually made reducible with this trick; maybe the linter is confused by this trick and isn't working as expected.

Eric Wieser (Oct 10 2022 at 04:51):

I don't see any reason not to make equiv.group etc reducible

Junyan Xu (Oct 10 2022 at 04:53):

Let me open a PR and see if CI is happy :)

Junyan Xu (Oct 10 2022 at 05:19):

#16884

Floris van Doorn (Oct 10 2022 at 08:36):

Junyan Xu said:

Thanks for your input. It turns out the is a solution (or hack?) in earlier code which I thought was unnecessary repetition but in fact does work to as a way to appease the linter: simply make an auxiliary definition

@[reducible] def comm_group_aux : comm_group (π_(n+2) X x) :=
@eckmann_hilton.comm_group ...

and then

instance comm_group : comm_group (π_(n+2) X x) := comm_group_aux

then the linter no longer complains. I'm not sure whether everything is actually made reducible with this trick; maybe the linter is confused by this trick and isn't working as expected.

This is a bad solution and just shows that the linter doesn't catch all problematic behavior. Don't do this and just mark eckmann_hilton.comm_group as reducible.

Junyan Xu (Oct 10 2022 at 16:32):

There is docs#tactic.transport that use equiv.group etc. under the hood, but it doesn't take care of making things reducible, as far as I can see from the code; if it could take care of it, we may be able to keep equiv.group etc. semireducible, but probably there's no point in doing so.

(Update: I may be wrong, I'm not actually sure if the transport tactic uses stuff in transfer_instance ...)

Eric Wieser (Oct 10 2022 at 17:28):

I don't think that's a reason to make equiv.group reducible; any manual users of equiv.group will also likely want it reducible, so it should just be globally reducible

Eric Wieser (Oct 10 2022 at 17:28):

But also, pretty much everywhere in mathlib where src#equiv.group could be used, we use docs#function.injective.group instead

Junyan Xu (Oct 10 2022 at 17:59):

docs#function.injective.group is inconvenient in that you have to first provide the has_one/mul/inv/div/npow/zpow instances and what are transferred by function.injective.group are only the group properties. This would be cumbersome to do in the case of homotopy groups.

Junyan Xu (Oct 10 2022 at 18:02):

docs#function.injective.group is used to build instances like docs#mul_opposite.group and docs#ulift.group etc. one by one from ground up, but if you want to do it in one stretch then docs#equiv.group and alike are certainly more convenient.

Junyan Xu (Oct 10 2022 at 18:03):

In fact docs#equiv.group uses docs#function.injective.group under the hood


Last updated: Dec 20 2023 at 11:08 UTC