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.