Failure of induction

Stream: mathlib4

[Jeremy Tan]

This is from SetTheory.Lists:

theorem subset_def {l₁ l₂ : Lists' α true} : l₁ ⊆ l₂ ↔ ∀ a ∈ l₁.toList, a ∈ l₂ :=
  ⟨fun H _ => mem_of_subset' H, fun H => by
    rw [← of_toList l₁]
    revert H; induction toList l₁ with intro H
    | nil => exact Subset.nil
    | cons h t t_ih =>
      simp only [ofList, List.find?, List.mem_cons, forall_eq_or_imp] at *
      exact cons_subset.2 ⟨H.1, t_ih H.2⟩⟩

The revert + induction cannot be replaced by induction toList l₁ generalizing H with, because no lemma is generated relating h to anything else in the cons branch:

α : Type u_1
l₁ l₂ : Lists' α true
h : Lists α
t : List (Lists α)
t_ih : (∀ a ∈ l₁.toList, a ∈ l₂) → ofList t ⊆ l₂
H : ∀ a ∈ l₁.toList, a ∈ l₂
⊢ ofList (h :: t) ⊆ l₂

What is going on?

[Jeremy Tan]

(cc @Eric Wieser)

[Eric Wieser]

I think adding this missing recursor helps:

@[elab_as_elim]
def recOfList {motive : Lists' α true → Sort*} (ofList : ∀ l, motive (ofList l)) : ∀ l, motive l :=
  fun l => cast (by simp) <| ofList (l.toList)

[Jeremy Tan]

Thanks for that, now back to you on the PR #25512