semireducible non-instances

Stream: general

[Junyan Xu]

#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]

#15681

[Floris van Doorn]

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]

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]

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]

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]

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

[Junyan Xu]

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

[Junyan Xu]

#16884

[Floris van Doorn]

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]

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]

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]

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

[Junyan Xu]

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]

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]

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