Help: "Internal error in mkElimApp: Expected first 3 arg..."

Stream: general

[György Kurucz]

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

[György Kurucz]

Managed to reduce the example to this:

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

[Kyle Miller]

Thanks for the minimization. It appears that cases/induction are having trouble with this dependence. I see you just reported it a minute ago (lean4#10279), thanks!