help with a failing to_additive

Stream: mathlib4

[Scott Morrison]

Could I summon some help with mathlib4's to_additive? I've been porting the bare minimum of the material about OrderedRing that linarith requires, and run into a problem with to_additive that I can't diagnose.

On the branch semorrison/OrderedRing, when I try to add @[to_additive] to

theorem one_lt_div' : 1 < a / b ↔ b < a  := ...

(see here I get the error message

application type mismatch
  instHDiv
argument has type
  Sub α
but function has type
  [inst : Div α] → HDiv α α α

I'm sure this is a missing or broken @[to_additive] attribute somewhere earlier, but I'm failing to find it.

If anyone could have a dig around for me that would be wonderful.

[Mario Carneiro]

It sounds like instHDiv needs a to_additive attribute

[Winston Yin]

I've encountered a similar problem with to_additive in Algebra.Hom.Group.

@[simp, to_additive]
theorem map_one {F M N : Type _} [One M] [One N] [OneHomClass F M N] (f : F) : f 1 = 1 :=

gives the error

application type mismatch
  @OneHomClass F M N inst✝¹
argument has type
  Zero M
but function has type
  [inst : outParam (One M)] → [inst : outParam (One N)] → Type (max (max u_1 u_2) u_3)

Except here, OneHomClass already has the to_additive attribute.

[Scott Morrison]

Is this on some branch / PR? Probably easier to diagnose in situ.

[Heather Macbeth]

I encountered some errors like this and the fix was to provide to_additive with the additivized declaration name (so

@[simp, to_additive map_zero]
theorem map_one {F M N : Type _} [One M] [One N] [OneHomClass F M N] (f : F) : f 1 = 1 :=

[Winston Yin]

Looks like I don't have permission to push to mathlib4 yet. Could somebody grant permission please?

[Winston Yin]

@Heather Macbeth Thanks for the tip. I managed to remove the error by adding ZeroHomClass to the to_additive attribute of OneHomClass:

@[to_additive ZeroHomClass]
class OneHomClass

Is this an indication that to_additive's heuristic isn't parsing the new naming convention properly?

[Scott Morrison]

@Winston Yin please provide your github username. (You can also add it to your user profile here on zulip.)

[Winston Yin]

winstonyin on GitHub

[Scott Morrison]

Invite sent.

[Winston Yin]

Another issue with to_additive: it seems to be unable to translate MonoidHomClass.toOneHomClass to AddMonoidHomClass.toZeroHomClass, even though MonoidHomClass has been explicitly marked with to_additive AddMonoidHomClass, and OneHomClass with to_additive ZeroHomClass. See map_mul_eq_one in PR#659 <--- how do I link to mathlib4 PRs?

[Winston Yin]

Ah. The issue is in ToAdditive.guessNameDict, which has yet to be updated to the new naming convention. @Edward Ayers

[Mario Carneiro]

There was a recent PR about the naming convention of ToAdditive, I thought this was fixed?

[Mario Carneiro]

mathlib4#579

[Mario Carneiro]

given that guessNameDict doesn't exist after that PR, I'm guessing you haven't merged master in a while

[Winston Yin]

Thanks for pointing me to this. I'll merge these into my branch

[Winston Yin]

A while = 3 days :sweat_smile:

[Mario Carneiro]

lol

[Winston Yin]

Another issue with to_additive: it seems to be unable to translate MonoidHomClass.toOneHomClass to AddMonoidHomClass.toZeroHomClass, even though MonoidHomClass has been explicitly marked with to_additive AddMonoidHomClass, and OneHomClass with to_additive ZeroHomClass. See map_mul_eq_one in mathlib4#659

Problem still persists after merging :(

[Winston Yin]

Adding the following line fixed it:

attribute [to_additive AddMonoidHomClass.toZeroHomClass] MonoidHomClass.toOneHomClass

although ideally this should be handled by the to_additive tactic

[Mario Carneiro]

please report an issue, I don't think this is on the high priority list of the maintainers

[Mario Carneiro]

but if you or someone else wants to investigate it, great

[Winston Yin]

Created issue: https://github.com/leanprover-community/mathlib4/issues/660

[Moritz Doll]

is this the same problem as https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/to_additive.20and.20instances
The error is obviously different, but it might come from the same bug in to_additive

[Moritz Doll]

I've tried your fix and it does not work, the defLemma linter still complains

[Moritz Doll]

but you seem to have no problems with the to_additive version not being an instance