Often doing `intros`

followed by `induction`

gets you a induction hypothesis that is not general enough. You can generalize some stuff before calling induction and then the IH has them quantified universally. I often have this pattern `intros x y z. gen x y. induction z. intros x y`

, is there a way to skip having to intro, gen, and then intro again x and y?

Changing the order the lemma quantifies over them is not always a solution, as sometimes you induct over an inductive type instead of just a variable. If you have `forall x y z, P x y`

you cannot pull the `P x y`

before the `z`

, so you will *have* to do `intros x y z H. gen z. induction H. intro z`

Well I guess you can push the `forall z`

to go after the `P x y`

but I don't like that as this way it will not let me instantiate the lemma with all the variables in a row

with ssreflect you can write `move => + + z. induction z. intros x y.`

, where `+`

means "introduce, but revert at the end of this command"

and ssreflect allows much _more_ concision than this

Is `induction z in x, y |- *`

what you want?

Last updated: Sep 28 2023 at 10:01 UTC