# Problem with rewrite

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.

Semicolon ; and period . have different meanings in Coq proof. So, while your solution looks similar to the given solution, they are not the same: ; performs tactics in parallel and . in series.

Lemma addlemma1 : forall n m, add n ( S m) = S ( add n m).
Proof.
induction n.
intros m.
simpl.
reflexivity.


If you read the goal at this point, it should be something like:

1 goal

goal 1 (ID 22) is:
forall m : nat, add (S n) (S m) = S (add (S n) m)


But the goal doesn't meet the "shape" that IHn expects.

So, to complete your solution, you need to repeat the intros m. simpl. tactics:

Lemma addlemma1 : forall n m, add n ( S m) = S ( add n m).
Proof.
induction n.
- (* when n = 0 *)
intros m.
simpl.
reflexivity.
- (* when n = S n *)
intros m.
simpl.
rewrite IHn.
reflexivity.
Qed.


Note: I prefer using - for each subgoal.