Why isn't plus_assoc rewriting correctly?
It is rewriting correctly. Coq doesn't print redundant parentheses. The + operator is left-associative, so n + m + p is a valid way of writing the term (n + m) + p, and Coq prints it without the parentheses.
Coq &lt; Check (n + m) + p.
n + m + p
     : nat

Just to be clear, n + m +p and (n + m) + p are exactly the same term, not just terms that are equal. They're different ways to use notations to write Nat.add (Nat.add n m).
Theorem plus_swap : forall n m p : nat,
  n + (m + p) = m + (n + p).
Proof.
  intros n m p.
  Unset Printing Notations.
  Show. (* Now the goal is shown as: eq (Nat.add n (Nat.add m p)) (Nat.add m (Nat.add n p)) *)
  rewrite -&gt; plus_assoc. (* Now the goal is: eq (Nat.add (Nat.add n m) p) (Nat.add m (Nat.add n p)) *)