to_additive and module system

Stream: metaprogramming / tactics

[Joachim Breitner]

After a PR to Lean of mine, to_additive fails with

error: Mathlib/GroupTheory/Congruence/Basic.lean:200:2: @[to_additive] failed. The translated value is not type correct. For help, see the docstring of `to_additive`, section `Troubleshooting`. Failed to add declaration
AddCon.quotientKerEquivRange:
Unknown constant `AddMonoidHom.mrangeRestrict._proof_2`

I could fix this by

+import all Mathlib.Algebra.Group.Submonoid.Operations`

Is that the right away to expose to to_additive such helper theorems?

[Sebastian Ullrich]

Currently yes, I think so. Curiously there is only one other such import right now, maybe a few more I haven't annotated with a comment. It would be great to come up with better approaches.

[Floris van Doorn]

Can either of you explain what is going on here? Presumably the module system doesn't make such internal declarations available anymore by default? However, if AddMonoidHom.mrangeRestrict._proof_2 is not available, then why is MonoidHom.mrangeRestrict._proof_2 (i.e. the multiplicative of the auxiliary decl) available (which I presume it is, since it should occurs in the definition of Con.quotientKerEquivRange - the declaration we are currently additivizing).

[Joachim Breitner]

These theorems are available, but without their body (for almost everything but to_additive theorem bodies are irrelevant)

Ah, I see what you are saying: Because MonoidHom.mrangeRestrict has been to-additivized, the aux proof should be as well (in a context where there the proof body is visible)?

[Jovan Gerbscheid]

The definition MonoidHom.mrangeRestrict has two auxiliary theorems: mrangeRestrict._proof_1 and mrangeRestrict._proof_2. The additive version of mrangeRestrict._proof_1 already exists, and is AddMonoidHom.mrange_comp._proof_1. As a result, the additive version of mrangeRestrict._proof_2 is AddMonoidHom.mrangeRestrict._proof_1. So, we should translate mrangeRestrict._proof_2 to AddMonoidHom.mrangeRestrict._proof_1 instead of AddMonoidHom.mrangeRestrict._proof_2 (which doesn't exist).

The reason why AddMonoidHom.mrange_comp._proof_1 already exists and MonoidHom.mrange_comp._proof_1 does not, is that to_additive is too aggressive with abstracting proofs: is should only do this in the value of defs (which is what normal definitions do). For this I've made #32393.

I do not know why any of these proofs were showing up for you though, because I would have expected them to all be private to the module system.

[Floris van Doorn]

So #32393 is likely an unrelated bug, not fixing the "Unknown constant"-error Joachim encountered, right?
One thing that might be relevant is that to_additive unfolds all aux-declarations occurring in its value. This is necessary to have enough context for to_additive translation heuristics to work correctly.

[Joachim Breitner]

Right, and that needs access to the non exposed bodies, so same module or import all