to_additive failure

Stream: mathlib4

[Frédéric Dupuis]

I've got mathlib4#944 working up to an issue with to_additive that I can't figure out:

@[to_additive "`0` is the homomorphism sending all elements to `0`."]
instance : One (α →*o β) :=
  ⟨{ (1 : α →* β) with monotone' := monotone_const }⟩

This gives me the error message (kernel) invalid projection AddZeroClass.toZero.1. It does exist, just like its counterpart MulOneClass.toOne.1. This is on line 428 of Algebra.Order.Hom.Monoid.lean in that PR. I have no idea how to deal with it; any help is greatly appreciated!

[Kevin Buzzard]

The issue seems to be to do with instance naming conventions. This fixes all the errors:

-- note: we're in namespace `OrderMonoidHom` right now
/-- `1` is the homomorphism sending all elements to `1`. -/
instance foo : One (α →*o β) :=
  ⟨{ (1 : α →* β) with monotone' := monotone_const }⟩

/-- `0` is the homomorphism sending all elements to `0`. -/
instance _root_.OrderAddMonoidHom.foo {α β : Type _} [Preorder α] [Preorder β] [AddZeroClass α]
    [AddZeroClass β] : Zero (α →+o β) :=
  ⟨{ (0 : α →+ β) with monotone' := monotone_const }⟩

attribute [to_additive] foo

So this seems to be an issue with @[to_additive].

[Kevin Buzzard]

The autogenerated name for the multiplicative instance is OrderMonoidHom.instOneOrderMonoidHom, so if you want to stick with the new instance names you can do

/-- `1` is the homomorphism sending all elements to `1`. -/
instance : One (α →*o β) :=
  ⟨{ (1 : α →* β) with monotone' := monotone_const }⟩

/-- `0` is the homomorphism sending all elements to `0`. -/
instance _root_.OrderAddMonoidHom.instZeroOrderAddMonoidHom {α β : Type _} [Preorder α] [Preorder β] [AddZeroClass α]
    [AddZeroClass β] : Zero (α →+o β) :=
  ⟨{ (0 : α →+ β) with monotone' := monotone_const }⟩

attribute [to_additive] instOneOrderMonoidHom

[Yaël Dillies]

Does the following work?

/-- `0` is the homomorphism sending all elements to `0`. -/
instance _root_.OrderAddMonoidHom.instZeroOrderAddMonoidHom {α β : Type _} [Preorder α] [Preorder β] [AddZeroClass α]
    [AddZeroClass β] : Zero (α →+o β) :=
  ⟨{ (0 : α →+ β) with monotone' := monotone_const }⟩

@[to_additive]
/-- `1` is the homomorphism sending all elements to `1`. -/
instance : One (α →*o β) :=
  ⟨{ (1 : α →* β) with monotone' := monotone_const }⟩

[Kevin Buzzard]

Oh this might be related to mathlib4#939 ? It's the same error.

[Floris van Doorn]

Fixed by mathlib4#952

[Kevin Buzzard]

@Floris van Doorn do you understand why my "write the instance names" fix works in this case?

[Floris van Doorn]

What is the "write the instance names" fix? In your earlier message you write all the additive declarations manually, so that to_additive doesn't have to do any translation anymore.

[Floris van Doorn]

the part of your message that fixed the problem is giving the additive declaration explicitly, not giving the instance an explicit name.