I have this goal I want to prove.
1 goal
t1, t2 : FCPLang
H : evalS t1 = Some t2
______________________________________(1/1)
evalBS t1 = evalBS t2
To prove it I use induction t1., but these are the introduced induction hypothesis:
1 goal
t1_1, t1_2, t1_3, t2 : FCPLang
H : evalS (if_then_else t1_1 t1_2 t1_3) = Some t2
IHt1_1 : evalS t1_1 = Some t2 -> evalBS t1_1 = evalBS t2
IHt1_2 : evalS t1_2 = Some t2 -> evalBS t1_2 = evalBS t2
IHt1_3 : evalS t1_3 = Some t2 -> evalBS t1_3 = evalBS t2
______________________________________(1/1)
evalBS (if_then_else t1_1 t1_2 t1_3) = evalBS t2
which I believe are useless as t2 is used again, instead of introducing a new term for example:
IHt1_1 : evalS t1_1 = Some t2_1 -> evalBS t1_1 = evalBS t2_1
How can I fix this?
>Solution :
What you are trying to do is "have t2 quantified in your induction hypothesis." As you noted, t2 is fixed throughout the induction, but you want it to change. To allow that, you need to quantify it, so that the statement you prove by induction holds for all t2.
There are two ways to accomplish this. The "more primitive" method that actually tells you what is going on (and thus is good for learners) is to
revert t2. induction t1; intros t2.
You will notice that all your induction hypotheses now start with forall t2, ... and thus you can use them with arbitrary changed t2s.
Since typing revert and intros all the time is annoying, there is the more advanced trick of doing
induction t1 in t2|-*.
That generalizes to e.g. induction t1 in t2,t3,Ht23|-*. The |-* needs to be there, if you omit it, things do not work.