`to_additive` unable to translate `toOneHomClass`

[winstonyin]

See PR #659, in Algebra.Hom.Group, around theorem MonoidHom.coe_coe. If the quickfix

attribute [to_additive AddMonoidHomClass.toZeroHomClass] MonoidHomClass.toOneHomClass

is removed, the to_additive tactic seems to be looking for AddMonoidHomClass.toOneHomClass, when it should look for AddMonoidHomClass.toZeroHomClass. It has no trouble translating OneHomClass to ZeroHomClass, but has trouble with toOneHomClass.

[joneugster]

I'll look into that tonight :)

[joneugster]

Looks like to_additive always has problems if a class extends 2+ other classes. The relevant TODO is this here:

https://github.com/leanprover-community/mathlib4/blob/085e7ab46bbf282a3911e738f2407e2aef50e22c/Mathlib/Tactic/ToAdditive.lean#L590-L600

MWE to reproduce error

``` -- First, all the additive versions class ZeroA (A : Type _) where zero : ℕ zero_add : zero + zero = zero class ZeroB (A : Type _) extends ZeroA A where zero_sub : zero - zero = 0 class ZeroC (A : Type _) extends ZeroA A where zero_refl : zero = zero class ZeroD (A : Type _) extends ZeroB A, ZeroC A -- Now all the multiplicative versions @[to_additive] class OneA (A : Type _) where one : ℕ one_mul : one * one = one @[to_additive] class OneB (A : Type _) extends OneA A where one_sub : one - one = 0 @[to_additive] class OneC (A : Type _) extends OneA A where one_refl : one = one @[to_additive] class OneD (A : Type _) extends OneB A, OneC A -- check `to_additive` deals properly with all extensions. @[to_additive] lemma one_mul_test_one {A : Type _} [x : OneD A] : true := by have := x.toOneA have := x.toOneC have := x.toOneB trivial ``` Error: `(kernel) unknown constant 'Test.ZeroD.toOneC'` (Because it fails to translate `OneD.toOneC` to `ZeroD.toZeroC`)

Unfortunately I don't know how to fix this just now, maybe somebody else does.

[fpvandoorn]

That todo is not quite the right one. It is for translating constructors, like AddMonoidHomClass.mk. However, this is not actually necessary: the implementation will do fine without these translations.

@digama0: Am I correct that the environment does not contain information about which structures a given structure extends? What is the best way forward? The @[ancestor] hack from Lean 3? Make a Core PR that records this information?

[digama0]

When I removed the ancestor attribute from mathport, my understanding was that this information either already exists or would be stored by lean to avoid the need for duplicating the information. (That said I haven't looked at it in detail and a core PR may be needed.)

[fpvandoorn]

I created a RFC for a core PR at leanprover/lean4#1881

[eric-wieser]

This has come up again in #3171; it would be great to revisit it.