How to apply rewrite inside a specific subexpression?

Question

I'm using the online book "Software Foundations" to learn about Coq.

In the second chapter, it is asked to prove the "plus_assoc" theorem:

Theorem plus_assoc : forall n m p : nat, n + (m + p) = (n + m) + p.

I make use of two previously proven theorems:

Theorem plus_comm : forall n m : nat, n + m = m + n.
Theorem plus_n_Sm : forall n m : nat, S (n + m) = n + (S m).

I prove the plus_assoc theorem using induction on n:

Proof.
  intros n m p.
  induction n as [ | n' ].
    reflexivity.

    rewrite plus_comm.
    rewrite <- plus_n_Sm.
    rewrite plus_comm.
    rewrite IHn'.
    symmetry.
    rewrite plus_comm.

At this point, the context (*) is:

1 subgoals
case := "n = S n'" : String.string
n' : nat
m : nat
p : nat
IHn' : n' + (m + p) = n' + m + p
______________________________________(1/1)
p + (S n' + m) = S (n' + m + p)

I would like to use plus_comm to get

p + (m + S n') = S (n' + m + p)

then plus_n_sm

p + S (m + n') = S (n' + m + p)

then again plus_n_sm

S (p + (m + n')) = S (n' + m + p)

and finish the proof using plus_comm twice then reflexivity

S (p + (n' + m)) = S (n' + m + p)
S (n' + m + p) = S (n' + m + p)

The small question is that I don't know how to apply plus_comm to (S n' + m).

The great question is: why issuing

apply plus_comm.

finishes the proof instantly (in the given context (*)) ?

Thank you in advance for any clarification !

Fabian Pijcke

Answer 1

You can apply plus_comm to (S n' + m) by instantiating it with (S n') and m.

    Check plus_comm.
    Check plus_comm (S n').
    Check plus_comm (S n') m.
    rewrite (plus_comm (S n') m).
    rewrite <- plus_n_Sm.
    rewrite <- plus_n_Sm.
    rewrite (plus_comm m n').
    rewrite plus_comm.
    reflexivity.
Qed.

I think using Require Import Coq.Setoids.Setoid. and then using rewrite plus_comm at 2. is supposed to have the same effect, but it doesn't work.

The reason apply plus_comm finishes the goal is because apply performs unification modulo conversion. That is to say, p + (S n' + m) = S (n' + m + p) is convertible to p + (S n' + m) = S n' + m + p, and p + (S n' + m) = S n' + m + p is unifiable with ?1 + ?2 = ?2 + ?1.

In fact, if you perform reduction using the simpl tactic the proof becomes shorter.

Theorem plus_assoc : forall n m p : nat, n + (m + p) = (n + m) + p.
Proof.
induction n.
  reflexivity.

  intros.
  simpl.
  apply f_equal.
  apply IHn.
Qed.