Problem with rewrite

Question

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.

Answer 1

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.

For your solution:

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.