FunInd: Redundant assumptions due to match-elaboration

[nomeata]

Reported by @TwoFX:

Consider

def f (n : Nat) (hn : n % 2 = 1) (m : Nat) (hm : (n + m) % 2 = 1) : Nat :=
  match n with
  | 1 => 0
  | n' + 3 =>
    match m with
    | 0 => 1
    | m' + 1 => f n' (by sorry) m' (by sorry)

/--
info: f.induct (motive : (n : Nat) → n % 2 = 1 → (m : Nat) → (n + m) % 2 = 1 → Prop)
  (case1 : ∀ (m : Nat) (hn : 1 % 2 = 1) (hm : (1 + m) % 2 = 1), 1 % 2 = 1 → (1 + m) % 2 = 1 → motive 1 hn m hm)
  (case2 :
    ∀ (n' : Nat) (hn : (n' + 3) % 2 = 1) (hm : (n' + 3 + 0) % 2 = 1),
      n'.succ.succ.succ % 2 = 1 →
        (n' + 3 + 0) % 2 = 1 → (n'.succ.succ.succ + 0) % 2 = 1 → motive n'.succ.succ.succ hn 0 hm)
  (case3 :
    ∀ (n' : Nat) (hn : (n' + 3) % 2 = 1) (m' : Nat) (hm : (n' + 3 + (m' + 1)) % 2 = 1),
      n'.succ.succ.succ % 2 = 1 →
        (n' + 3 + m'.succ) % 2 = 1 →
          (n'.succ.succ.succ + m'.succ) % 2 = 1 → motive n' ⋯ m' ⋯ → motive n'.succ.succ.succ hn m'.succ hm)
  (n : Nat) (hn : n % 2 = 1) (m : Nat) (hm : (n + m) % 2 = 1) : motive n hn m hm
-/
#guard_msgs in
#check f.induct

and note that case2 has effectively two copies (or more?) of hn and hm.

These originate from the match-elaboror, which refines hn and hm.

It would be desirable if it didn’t have these copies, and instead only kept the innermost, the one that talks about the refined version, to match the user-visible local context seen when the user looks at the info view at this position.

Versions

Lean 4.15.0-rc1

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.