Zulip Chat Archive

Stream: general

Topic: apply induction_lemma, clear n


view this post on Zulip Kevin Buzzard (Nov 11 2020 at 19:44):

Reviewing a PR and I see apply nat.strong_induction_on n, clear n,. This reminded me of some code I was writing last week which had the line apply span_induction hx; clear hx x,. This is perhaps quite a common idiom? The reason one wants to clear the variable is because one is about to embark on a proof or proofs of results related to the original goal and ones instinct is to use the same variable names again -- for example I want to prove results about elements of submodules and I want to use x and y for these elements, so it's annoying if I don't clear the original x which is now useless to me. Is this style OK or is it worth modding some induction tactic to make this happen automatically? I'm not entirely sure what I want here, but given that I've now seen this twice in one week it made me wonder.

view this post on Zulip Mario Carneiro (Nov 11 2020 at 20:29):

I think ssreflect has something for this, a la have {h1} h2 := foo h1 which is like have h2 := foo h1, clear h1 except it works even if you reuse the variable names

view this post on Zulip Mario Carneiro (Nov 11 2020 at 20:33):

I don't see how we can offer something better than ; clear though

view this post on Zulip Mario Carneiro (Nov 11 2020 at 20:33):

in the examples, apply span_induction hx clearing hx x would be no better

view this post on Zulip Shing Tak Lam (Nov 11 2020 at 20:41):

fwiw induction n using nat.strong_induction_on with n hn works (does the same as apply nat.strong_induction_on n, clear n, intros n hn)

view this post on Zulip Kevin Buzzard (Nov 11 2020 at 21:42):

Yes, I realised when I was posting that I couldn't really see a solution which would be saving too many characters!


Last updated: May 15 2021 at 23:13 UTC