CODEWITHSUNDEEP
syntaxcoq
Langston
Langston

Reputation: 1103

Why does a proof with semicolons not work with periods?

The following proof is given in Coq in a Hurry:

Fixpoint add n m := match n with 0 => m | S p => add p (S m) end.
Lemma exercise6 : forall n m, add n (S m) = S (add n m).
Proof.
  induction n; intros m; simpl.
    reflexivity.
  rewrite IHn; reflexivity.
Qed.

I tried writing this step by step to understand what was happening, but the inductive hypothesis isn't the same after solving the base case! Therefore, the tactics fail:

Lemma exercise6' : forall n m, add n (S m) = S (add n m).
Proof.
  induction n.
  intros m.
  simpl.
  reflexivity.
  rewrite IHn. reflexivity.
Qed.

They fail at the line staring with "rewrite", with the following error:

Error: Found no subterm matching add n (S ?M1580) in the current goal.

Why does the same code fail when written step-by-step? What is the difference between the semicolon and period?

Furthermore, is there a way I can view the step-by-step progression of the proof given in Coq in a Hurry?

Upvotes: 1

Views: 130

Answers (1)

gallais
gallais

Reputation: 12123

Here is a related answer.

In short:

  • induction n generates 2 subgoals.
  • A;B applies the tactics B to all the subgoals generated by A

So here, intros m; simpl is applied to the 2 goals generated by induction. Which means that you can fix your second script by inserting an extra intros m and an extra simpl before the rewrite:

Lemma exercise6' : forall n m, add n (S m) = S (add n m).
Proof.
  induction n.
  intros m.
  simpl.
  reflexivity.
  intros m.
  simpl.
  rewrite IHn.
  reflexivity.
Qed.

By the way, you can make the structure of the proof script a lot clearer by using bullets to delimit the various subgoals. This gives the following two scripts where you can see that in exercise6 the intros m; simpl is performed before entering either subgoal whereas in exercise6' they have been pushed into each subgoal:

Lemma exercise6 : forall n m, add n (S m) = S (add n m).
Proof.
  induction n; intros m; simpl.
  - reflexivity.
  - rewrite IHn; reflexivity.
Qed.

Lemma exercise6' : forall n m, add n (S m) = S (add n m).
Proof.
  induction n.
  - intros m.
    simpl.
    reflexivity.
  - intros m.
    simpl.
    rewrite IHn.
    reflexivity.
Qed.

Upvotes: 2

Related Questions