Why isn't plus_assoc rewriting correctly?

Question

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?

Answer 1

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.
  Show. (* Now the goal is shown as: eq (Nat.add n (Nat.add m p)) (Nat.add m (Nat.add n p)) *)
  rewrite -> plus_assoc. (* Now the goal is: eq (Nat.add (Nat.add n m) p) (Nat.add m (Nat.add n p)) *)