Internal error in mkElimApp: Expected first 3 arguments of motive in conclusion to be one of the targets

[kuruczgy]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• [X] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
• [X] Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.
• [X] Test your test case against the latest nightly release, for example on https://live.lean-lang.org/#project=lean-nightly (You can also use the settings there to switch to “Lean nightly”)

Description

inductive Ind (pair : Type × Unit) : Unit → pair.fst → Type where
| mk q : Ind _ () q

example (i : Ind (Unit, ()) () ()) : True := by
  cases i -- Error here
  sorry

Produces:

Internal error in mkElimApp: Expected first 3 arguments of motive in conclusion to be one of the targets:
  ?m.10 () ()

Expected behavior: The cases tactic succeeds.

Actual behavior: It fails with an internal error.

Versions

Lean 4.24.0-nightly-2025-09-06 Target: x86_64-unknown-linux-gnu

Impact

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

[kmill]

Zulip thread with context: #general > Help: "Internal error in mkElimApp: Expected first 3 arg..." @ 💬

Message reproduced here:

When upgrading to v4.22.0 from v4.18.0, some of my induction proofs now fail with the following error: "Internal error in mkElimApp: Expected first 3 arguments of motive in conclusion to be one of the targets: ?m.6180 t c H". Any ideas?

Reproducer:

structure FSM {Act : Type} where
  Q : Type
  α : Act → Prop
  [dec_α : DecidablePred α]
  Δ : Q → (Subtype α ⊕ Unit) → Q → Prop
  q₀ : Q
  F : Q → Prop

inductive FSM.reachable (M : FSM (Act := Act)) : (q₁ : M.Q) → (t : List Act) → (q : M.Q) → Prop where
| rfl q t (_ : t = []) : FSM.reachable _ q t q
| step q t q₁ q₁' a
  (prf_r : FSM.reachable _ q t q₁)
  (prf_step : M.Δ q₁ (.inl a) q₁')
  t' (_ : t' = (t ++ [a.val]))
    : FSM.reachable _ q t' q₁'
| tau q t q₁ q₁'
  (prf_r : FSM.reachable _ q t q₁)
  (prf_step : M.Δ q₁ (.inr ()) q₁')
    : FSM.reachable _ q t q₁'

def FSM.language (M : FSM (Act := Act)) : (List Act → Prop) :=
  fun t => ∃ q, M.reachable M.q₀ t q ∧ M.F q

def FSM.comp (M₁ M₂ : FSM (Act := Act)) : FSM (Act := Act) := {
  Q := M₁.Q × M₂.Q
  α := fun a => M₁.α a ∨ M₂.α a
  dec_α :=
    let _ := M₁.dec_α
    let _ := M₂.dec_α
    inferInstance
  Δ := fun (s₁, s₂) a (s₁', s₂') =>
    match a with
    | .inl ⟨a, a_prop⟩ =>
      match M₁.dec_α a, M₂.dec_α a with
      | .isFalse _, .isFalse _ => by exfalso; cases a_prop <;> contradiction
      | .isTrue h, .isFalse _ => M₁.Δ s₁ (.inl ⟨a, h⟩) s₁' ∧ s₂ = s₂'
      | .isFalse _, .isTrue h => M₂.Δ s₂ (.inl ⟨a, h⟩) s₂' ∧ s₁ = s₁'
      | .isTrue h₁, .isTrue h₂ => M₁.Δ s₁ (.inl ⟨a, h₁⟩) s₁' ∧ M₂.Δ s₂ (.inl ⟨a, h₂⟩) s₂'
    | .inr _ =>
      (M₁.Δ s₁ (.inr ()) s₁' ∧ s₂ = s₂') ∨
      (M₂.Δ s₂ (.inr ()) s₂' ∧ s₁ = s₁')
  q₀ := (M₁.q₀, M₂.q₀)
  F := fun (a₁, a₂) => M₁.F a₁ ∧ M₂.F a₂
}

def dec_filter {α : Act → Prop} (l : List Act) (dec : DecidablePred α) : List Act :=
  l.filter (fun i => (dec i).decide)

theorem FSM.comp_language (M₁ M₂ : FSM (Act := Act))
  : ∀ t, (M₁.comp M₂).language t → M₁.language (dec_filter t M₁.dec_α)
  := by
  intros t
  simp [FSM.language]
  intros c H end_state_comp_accepting
  simp [FSM.comp] at c end_state_comp_accepting
  exists c.fst
  clear end_state_comp_accepting
  induction H -- Error here
  sorry

[nomeata]

Most likely culprit: https://github.com/leanprover/lean4/pull/8096

[kuruczgy]

Yep, a partial revert of the complexArgs stuff in that PR seems to fix this issue.

Diff (this applies to the current master, e75e6fbe9e85f953accdd8ac44280397e20ab695)

diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index 24ff98b00c..fa92428557 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -147,7 +147,6 @@ structure Result where
   motive      : MVarId
   alts        : Array Alt
   others      : Array MVarId
-  complexArgs : Array Expr
 
 /--
   Construct the an eliminator/recursor application. `targets` contains the explicit and implicit
@@ -215,20 +214,10 @@ partial def mkElimApp (elimInfo : ElimInfo) (targets : Array Expr) (tag : Name)
   let alts ← s.alts.filterM fun alt => return !(← alt.mvarId.isAssigned)
   let some motive := s.motive |
       throwError "Internal error in mkElimApp: Motive not found"
-  let complexArgs ← s.fType.withApp fun f motiveArgs => do
-    unless f == mkMVar motive do
-      throwError "Internal error in mkElimApp: Expected application of {motive}:{indentExpr s.fType}"
-    -- Sanity-checking that the motive is applied to the targets.
-    -- NB: The motive can take them in a different order than the eliminator itself
-    for motiveArg in motiveArgs[*...targets.size] do
-      unless targets.contains motiveArg do
-        throwError "Internal error in mkElimApp: Expected first {targets.size} arguments of motive \
-          in conclusion to be one of the targets:{indentExpr s.fType}"
-    pure motiveArgs[targets.size...*]
   let elimApp ← instantiateMVars s.f
   -- `elimArgs` is the argument list that the offsets in `elimInfo` work with
   let elimArgs := elimApp.getAppArgs[elimInfo.elimExpr.getAppNumArgs...*]
-  return { elimApp, elimArgs, alts, others, motive, complexArgs }
+  return { elimApp, elimArgs, alts, others, motive }
 
 /--
 Given a goal `... targets ... |- C[targets, complexArgs]` associated with `mvarId`,
@@ -240,29 +229,11 @@ ignores them otherwise. This limits the ability of `cases` to use unfolding func
 principles with dependent types, because after generalization of the targets, the types do
 no longer match. This can likely be improved.
 -/
-def setMotiveArg (mvarId : MVarId) (motiveArg : MVarId) (targets : Array FVarId) (complexArgs : Array Expr := #[]) : MetaM Unit := do
+def setMotiveArg (mvarId : MVarId) (motiveArg : MVarId) (targets : Array FVarId) : MetaM Unit := do
   let type ← inferType (mkMVar mvarId)
 
   let motiveType ← inferType (mkMVar motiveArg)
-  let exptComplexArgTypes ← arrowDomainsN complexArgs.size (← instantiateForall motiveType (targets.map mkFVar))
-
-  let mut absType := type
-  for complexArg in complexArgs.reverse, exptComplexArgType in exptComplexArgTypes.reverse do
-    trace[Elab.induction] "setMotiveArg: trying to abstract over {complexArg}, expected type {exptComplexArgType}"
-    let complexArgType ← inferType complexArg
-    if (← isDefEq complexArgType exptComplexArgType) then
-      let absType' ← kabstract absType complexArg
-      let absType' := .lam (← mkFreshUserName `x) complexArgType absType' .default
-      if (← isTypeCorrect absType') then
-        absType := absType'
-      else
-        trace[Elab.induction] "Not abstracting goal over {complexArg}, resulting term is not type correct:{indentExpr absType'} }"
-        absType := .lam (← mkFreshUserName `x) complexArgType absType .default
-    else
-      trace[Elab.induction] "Not abstracting goal over {complexArg}, its type {complexArgType} does not match the expected {exptComplexArgType}"
-      absType := .lam (← mkFreshUserName `x) exptComplexArgType absType .default
-
-  let motive ← mkLambdaFVars (targets.map mkFVar) absType
+  let motive ← mkLambdaFVars (targets.map mkFVar) type
   let motiverInferredType ← inferType motive
   unless (← isDefEqGuarded motiverInferredType motiveType) do
     throwError "Type mismatch when assigning motive{indentExpr motive}\n{← mkHasTypeButIsExpectedMsg motiverInferredType motiveType}"
@@ -947,7 +918,7 @@ private def evalInductionCore (stx : Syntax) (elimInfo : ElimInfo) (targets : Ar
       let result ← withRef stx[1] do -- use target position as reference
         ElimApp.mkElimApp elimInfo targets tag
       trace[Elab.induction] "elimApp: {result.elimApp}"
-      ElimApp.setMotiveArg mvarId result.motive targetFVarIds result.complexArgs
+      ElimApp.setMotiveArg mvarId result.motive targetFVarIds
       -- drill down into old and new syntax: allow reuse of an rhs only if everything before it is
       -- unchanged
       -- everything up to the alternatives must be unchanged for reuse
@@ -1070,7 +1041,7 @@ def evalCasesCore (stx : Syntax) (elimInfo : ElimInfo) (targets : Array Expr)
     let mvarId ← generalizeTargetsEq mvarId motiveType targets
     let (targetsNew, mvarId) ← mvarId.introN targets.size
     mvarId.withContext do
-      ElimApp.setMotiveArg mvarId elimArgs[elimInfo.motivePos]!.mvarId! targetsNew result.complexArgs
+      ElimApp.setMotiveArg mvarId elimArgs[elimInfo.motivePos]!.mvarId! targetsNew
       -- drill down into old and new syntax: allow reuse of an rhs only if everything before it is
       -- unchanged
       -- everything up to the alternatives must be unchanged for reuse