apply induction_lemma, clear n

Stream: general

[Kevin Buzzard]

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.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Shing Tak Lam]

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)

[Kevin Buzzard]

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