induction tactic that doesn't destroy the input from context

Stream: general

[Kris Brown]

I have a scenario where I need to do induction on a list and (in the cons case) keep track that the introduced variables for head and tail are equal to the original term in my context. i.e. after doing induction y with hy ty Hy in the second branch I need an equation y = hy::ty. Normally doing induction on x makes x disappear from the context. The docs say

induction h : t will introduce an equality of the form h : t = C x y,
asserting that the input term is equal to the current constructor case, to the context.

That sounds like what I'm looking for, but I don't know what t is supposed to be (just putting the type of h doesn't work).

[Reid Barton]

induction h : y with hy ty Hy I think

[Reid Barton]

I can see why you thought something named t that occurs after a colon was a type though.

[Kris Brown]

Ah makes sense, thanks!

[Kris Brown]

Is there an analogous trick that works with cases? I have a situation where induction doesn't work (I don't really understand the error "generalize tactic failed, failed to find expression in the target"), but cases would work if I could keep track of the equality.

lemma example (l:list ℕ): true :=
begin
cases l.length with n,
 {sorry},
 {sorry} -- how do I get something like succ n = l.length ?
end

[Simon Hudon]

try cases h : l.length with n. It also works with rcases