Functional induction principles should prune parmeters

[nomeata]

It can happen that (fixed) function parameters end up completely unused in the function’s induction principle. For example in

/--
info: Array.mapFinIdxM.map.induct.{u, v, w} {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α)
  (f : Fin as.size → α → m β) (motive : (i j : Nat) → i + j = as.size → Array β → Prop)
  (case1 : ∀ (j : Nat) (bs : Array β) (x : 0 + j = as.size), 0 + j = as.size → motive 0 j x bs)
  (case2 :
    ∀ (j : Nat) (bs : Array β) (i : Nat) (inv : i + 1 + j = as.size),
      j < as.size →
        ∀ (this : i + (j + 1) = as.size),
          i.succ + j = as.size →
            (∀ (__do_lift : β), motive i (j + 1) this (bs.push __do_lift)) → motive i.succ j inv bs)
  (i j : Nat) (inv : i + j = as.size) (bs : Array β) : motive i j inv bs
-/
#guard_msgs in #check Array.mapFinIdxM.map.induct

The parameter f is used neither in the theorem statement nor the proof.

I originally left these parameters there, assuming they wouldn’t hurt and would help the user knowing how to instantiate the induction principle.

But in practice they get in the way, for example in this proof, where the function of interest appears under a lambda:

axiom monotone : ∀ {α} {β}, (α → β) → Prop

theorem monotone_mapIdxM
    (m : Type u → Type v) [Monad m]
    {α β : Type u}
    {γ : Type w}
    (xs : Array α)
    (f : γ → Fin xs.size → α → m β) :
    monotone (fun x => xs.mapFinIdxM (fun i y => f x i y)) := by
  -- This shows a limitation of the induction principles:
  -- the parameter `f` isn't strictly needed, and cannot actually be instantiated here
  suffices
    ∀ i j (h : i + j = xs.size) r, monotone (fun x => Array.mapFinIdxM.map xs (fun i y => f x i y) i j h r) by
    apply this
  intros i j h r
  induction i, j, h, r using Array.mapFinIdxM.map.induct (m := m) xs
  case case1 =>
    sorry
  case case2 ih =>
    sorry
  case f i y => exact f sorry i y -- cannot be instantiated

Here I cannot pass any f to the induction principle, but the proof would make perfect sense otherwise.

Version

info: Lean 4.16.0-nightly-2024-12-05

[nomeata]

Likely just a matter of changing this code:

lean4/src/Lean/Meta/Tactic/FunInd.lean

Lines 722 to 728 in 019f8e1

	-- We could pass (usedOnly := true) below, and get nicer induction principles that
	-- do not mention odd unused parameters.
	-- But the downside is that automatic instantiation of the principle (e.g. in a tactic
	-- that derives them from an function application in the goal) is harder, as
	-- one would have to infer or keep track of which parameters to pass.
	-- So for now lets just keep them around.
	let e' ← mkLambdaFVars (binderInfoForMVars := .default) fixedParams e'