# Why isn't plus_assoc rewriting correctly?

First I have plus_assoc ready.

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


for simplicity we omit the proof of plus_assoc.

now I want to prove plus_swap:

Theorem plus_swap : forall n m p : nat,
n + (m + p) = m + (n + p).
Proof. intros n m p. rewrite -> plus_assoc. ...


the equation was rewritten into n + m + p = m + ( n + p ), rather than the expected (n + m) + p = m + (n + p). why?

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 < 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.