Zulip Chat Archive

Stream: mathlib4

Topic: to_additive failure


Frédéric Dupuis (Dec 11 2022 at 03:13):

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 (Dec 11 2022 at 10:57):

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 (Dec 11 2022 at 11:02):

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 (Dec 11 2022 at 11:12):

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 (Dec 11 2022 at 11:30):

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

Floris van Doorn (Dec 11 2022 at 16:12):

Fixed by mathlib4#952

Kevin Buzzard (Dec 11 2022 at 19:09):

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

Floris van Doorn (Dec 11 2022 at 19:17):

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 (Dec 11 2022 at 19:21):

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


Last updated: Dec 20 2023 at 11:08 UTC