2
$\begingroup$

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.

$\endgroup$

1 Answer 1

7
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.