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":
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.