Zulip Chat Archive

Stream: general

Topic: induction tactic that doesn't destroy the input from context


view this post on Zulip Kris Brown (Jul 16 2020 at 18:41):

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).

view this post on Zulip Reid Barton (Jul 16 2020 at 18:44):

induction h : y with hy ty Hy I think

view this post on Zulip Reid Barton (Jul 16 2020 at 18:45):

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

view this post on Zulip Kris Brown (Jul 16 2020 at 18:45):

Ah makes sense, thanks!

view this post on Zulip Kris Brown (Jul 31 2020 at 21:58):

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

view this post on Zulip Simon Hudon (Jul 31 2020 at 22:03):

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


Last updated: May 10 2021 at 17:39 UTC