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
induction z in x, y |- * what you want?
Last updated: Feb 06 2023 at 12:04 UTC