to_additive and #align

Stream: mathlib4

[Kevin Buzzard]

@[simp, to_additive coe_unzero]
theorem coe_unone {x : WithOne α} (hx : x ≠ 1) : ↑(unone hx) = x :=
  WithBot.coe_unbot x hx
#align with_one.coe_unone WithOne.coe_unone

says the autoporter. But should we also be doing

#align with_zero.coe_unzero WithZero.coe_unzero

?

[Yakov Pechersky]

Yes

[Kevin Buzzard]

thought so. And can someone write some code to flag all the times in mathlib where this hasn't happened? While they're at it, currently all @[coe, to_additive] and @[norm_cast, to_additive] are not affecting the additivised declarations either :-/

[Kevin Buzzard]

And perhaps @[elab_as_elim, to_additive] too, although I don't know how to check this because I only half-understand elab_as_elim and it is apparently difficult to figure out if a declaration is tagged with an attribute.

[Moritz Doll]

except for simp and instance all attributes are ignored by to_additive

[Kevin Buzzard]

So I conjecture that there are a bunch of errors in mathlib4 coming from these issues. I was about to merge Algebra.Group.WithOne.Defs but now I'm going through methodically fixing all of these things in this one file.

[Moritz Doll]

I would assumet that these will become more annoying later on, when proofs randomly break.

[Moritz Doll]

if you find any more attributes that are used with to_additive either ping me or add an issue on github. In my current PR for norm_cast I've added todos for symm and refl already and I will add elab_as_elim later

[Eric Wieser]

Should unzero be called unZero?

[Moritz Doll]

a bit off-topic, but the reason why it is non-trivial to add attributes is that they can do whatever they want, so it is up to the implementation of the attribute whether it has API to find out whether an declaration is flagged with that attribute. In the case of simp and norm_cast this is easy because one just copies the SimpExtension and this has said API, for instance I had to make a core issue (Leo added the API immediately), but for example for symm and refl this is very weird, because it does not provide a list/hashmap to lookup the names.

[Kevin Buzzard]

Moritz Doll said:

if you find any more attributes that are used with to_additive either ping me or add an issue on github. In my current PR for norm_cast I've added todos for symm and refl already and I will add elab_as_elim later

pinging you to say that coe is the other one I've seen.