Induction not applied to hypothesis

Stream: lean4

[Marcus Rossel]

In a similar fashion as a previous problem with cases, I'm having problems when performing induction:

inductive Thing (a : Nat) : List Nat → Prop
| one   : a = 1 → Thing a []
| two   : a = 2 → Thing a [a]

structure Combo where
  list : List ℕ
  thing : Thing 1 list

example (c : Combo) : False := by
  have t := c.thing
  induction c.list
  ...

Here, the goal state before and after the induction is exactly the same:

c : Combo
t : Thing 1 c.list
⊢ False

I need c.list to be resolved as [] in the nil case though to move on.
Why is this not happening?

[Mario Carneiro]

I don't think induction will replace occurrences of the expression in the hypotheses unless you use them in generalizing

[Marcus Rossel]

Mario Carneiro said:

I don't think induction will replace occurrences of the expression in the hypotheses unless you use them in generalizing

example (c : Combo) : False := by
  have t := c.thing
  induction c.list generalizing t with
  case nil =>
    ...

doesn't do it either :/

[Chris B]

In lean 3 the pattern was basically this:

example (c : Combo) : False := by
  generalize hx : c.list = x
  induction x

Which seems to work still.