to_additive and matchers

Stream: mathlib4

[Joachim Breitner]

It seems that to_additive does not additivize matchers in a way that they are still recognized as such:

/--
info: def WithOne.recOneCoe.{u, u_1} : {α : Type u} →
  {C : WithOne α → Sort u_1} → C 1 → ((a : α) → C ↑a) → (n : WithOne α) → C n :=
fun {α} {C} h₁ h₂ x ↦
  match x with
  | none => h₁
  | some x => h₂ x
-/
#guard_msgs in
#print WithOne.recOneCoe
/--
info: def WithZero.recZeroCoe.{u, u_1} : {α : Type u} →
  {C : WithZero α → Sort u_1} → C 0 → ((a : α) → C ↑a) → (n : WithZero α) → C n :=
fun {α} {C} h₁ h₂ x ↦ WithZero.instRepr.match_1 (fun x ↦ C x) x (fun _ ↦ h₁) fun x ↦ h₂ x
-/
#guard_msgs in
#print WithZero.recZeroCoe

Is this a known problem, or am I just the first to be bothered by this?
I haven’t looked yet, but I assume it’s just™ a matter of calling docs#Lean.Meta.Match.Extension.addMatcherInfo in the right place.
(I don't mind the lack of pretty-printing, but I’m working on generating equational theorems also for non-recursive definition, and that needs to recognize matcher applications.)

[Floris van Doorn]

Yes, this is known and the bottom item here: #1074. Please PR a fix if you know how to!
The relevant lines where the additive declaration is added is here: https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/ToAdditive/Frontend.lean#L801-L805

[Joachim Breitner]

Seem to be fairly straight-forward, it seems https://github.com/leanprover-community/mathlib4/commit/f11401e21dea90e60b0fe8bdb289fb1d067a4667 sufficed.

Plus the busywork of adding

Mathlib/Tactic/ToAdditive/Frontend.lean : line 1 : ERR_NUM_LIN : 1700 file contains 1504 lines, try to split it up

[Joachim Breitner]

PR'ed this at https://github.com/leanprover-community/mathlib4/pull/16026