I've just started with Coq and I don't understand why it does not accept rewrite
in the next situation. The following exercise is from "Coq in hurry":
Define add
as:
Fixpoint add n m := match n with 0 => m | S p => add p ( S m) end.
The exercise is:
forall n m, add n ( S m) = S ( add n m)
I was able to prove it but with a rather long solution. My second attempt, where the problem arises, was as follows:
Lemma addlemma1 : forall n m, add n ( S m) = S ( add n m).
Proof.
induction n.
intros m.
simpl.
reflexivity.
At this point I'd like to use rewrite IHn
but it doesn't work. Looking at the solution in the book, it is the following:
Lemma addlemma1 : forall n m, add n ( S m) = S ( add n m).
Proof.
induction n; intros m; simpl.
reflexivity.
rewrite IHn; reflexivity.
Qed.
This runs correctly. To me it looks like my attempt is the same as the solution, but I don't understand why in one case rewrite works and the other does not. Thank you in advance.