Roger Bosman (Jun 29 2021 at 15:00): Roger Bosman (Jun 29 2021 at 15:00):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
Roger Bosman (Jun 29 2021 at 15:01):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
Paolo Giarrusso (Jun 29 2021 at 15:02):with ssreflect you can write move => + + z. induction z. intros x y., where + means "introduce, but revert at the end of this command"
Paolo Giarrusso (Jun 29 2021 at 15:04):and ssreflect allows much _more_ concision than this
Yannick Forster (Jun 30 2021 at 10:14):Is induction z in x, y |- * what you want?
Last updated: Sep 28 2023 at 10:01 UTC