Stream: Coq users

Topic: intro nth variable


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip Paolo Giarrusso (Jun 29 2021 at 15:04):

and ssreflect allows much _more_ concision than this

view this post on Zulip Yannick Forster (Jun 30 2021 at 10:14):

Is induction z in x, y |- * what you want?


Last updated: Feb 06 2023 at 12:04 UTC