`to_additive` feature requests / issues

[fpvandoorn]

This is a single issue for new features or feature requests for to_additive, that I'll try to keep up-to-date. Feel free to comment with other suggestions

• [x] Reorder arguments using an arbitrary permutation. This can be used to fix some to_additive connections in #1056
• [x] Improve output of to_additive?, showing the type of the generated declaration (and not the body for lemmas)
• [ ] Even more reorder features, so that we can reorder Pow.mk to SMul.mk (requires re-ordering the function arguments in a particular argument)
• [ ] to_additive (attr := scoped simp) can scope the additive version in the wrong namespace (Zulip).
• [x] [bug] additivize lemmas generated by norm_cast (and other attributes).
• [ ] Allow specifying types where to_additive doesn't translate operations. Zulip 1 2
• [ ] [probably wontfix]: to_additive does not support match ... with. Zulip
• [ ] noncomputable definitions in a noncomputable sections won't be translated properly unless you explicitly specify noncomputable (this is https://github.com/leanprover/lean4/pull/2610)
• [ ] The congr can generate complicated terms involving Eq.rec that to_additive has a hard time to additivize. E.g. MeasureTheory.Measure.haar.prehaar_sup_eq
• [ ] Apparently to_additive doesn't work well with private: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60.40.5Bto_additive.5D.60.20bug.3F
• [ ] to_additive doesn't copy the docstring of alias: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/to_additive.20and.20deprecated.20alias

[YaelDillies]

to_additive does not seem to support the auxiliary lemmas generated by norm_cast: See #8916

[fpvandoorn]

Can you please minimize the example?

[YaelDillies]

Is this minimal enough?

import Mathlib.Data.Finset.Pointwise

open scoped Pointwise

@[to_additive]
lemma mul_foo {α : Type*} [DecidableEq α] [Mul α] (s t : Finset α) :
    (↑(s * t) : Set α) = ↑s * ↑t := by norm_cast
/-
application type mismatch
  Mathlib.Data.Finset.Pointwise._auxLemma.9
argument has type
  Add α
but function has type
  ∀ [inst : Mul α] (s t : Finset α), ↑s * ↑t = ↑(s * t)
-/

[fpvandoorn]

Yes, thanks! This was actually already a todo in the code. I will see if I can find a more systematic way to additivize new declarations generated attributes.

[fpvandoorn]

norm_cast handling is fixed in #14628