While I was writing a prove for the theorem below, I noticed that parentheses on the right magically disappeared. I would like to keep them and avoid auto simplification in the exercise.
Theorem add_assoc : forall n m p : nat,
n + (m + p) = (n + m) + p.
Proof.
intros n m p.
induction n as [n' IHn].
 reflexivity.

goals state:
n', m, p : nat
IHn : n' + (m + p) = n' + m + p
============================
S (n' + (m + p)) = S (n' + m + p)
Coq does not work with â€śstream of symbolâ€ť expressions. Expressions are naturally treeshaped, and Coq internally uses that tree everywhere, except when printing and parsing humanreadable input.
As such, parentheses are â€śconsumedâ€ť during parsing. They affect the tree produced by parsing but there is no â€śparenthesized expressionâ€ť internally. Coq did not eat your parentheses, it accounted for them when it created the syntax tree.
When printing an expression, the printer inserts parentheses wherever necessary. Since + is leftassociative, they are not necessary, so none are inserted.
So even if reflexivity is too smart (it runs unification), a dumber version of it (not running unification) would also be able to prove that (a+b)+c = a+b+c because these are the same expression, syntactically, in Coq. They have the exact same syntax tree, there is no way of telling them apart.
As such, strcmp seems the wrong function for comparing trees. They are not strings.
TL;DR: Parentheses are not real, there are only trees.
This is folklore in almost any programming language, but it can be surprising:
Coq reads x+y+z as a parenthesized expression (because + is a binary operator). In this case it applies a â€śleftassociativity parsing ruleâ€ť so it reads (x+y)+z. The exact same way it would read a+b*c as a+(b*c).
Moreover the printer by default omits parenthesis when they are not â€śneeded for the expression to be reread into an identical oneâ€ť, this is called the â€śreentering pretty printingâ€ť.
Thanks for detailed explanation. Now I see why my abstract representation about Coq leaked  expression type doesnâ€™t have data constructor for parentheses like Haskell does:
module Language.Haskell.TH.Syntax
data Exp
= VarE Name  ^ @{ x }@
 ConE Name  ^ @data T1 = C1 t1 t2; p = {C1} e1 e2 @
 LitE Lit  ^ @{ 5 or \'c\'}@
 UInfixE Exp Exp Exp  ^ @{x + y}@
 ParensE Exp  ^ @{ (e) }@
...
Indeed, it does not. I also donâ€™t know why you would want to have such a thing, since it has no functionality, and also it suggests the wrong mental model about abstract syntax trees. It makes you think the parentheses are necessary or affect the meaning, when they donâ€™t.
Edit: Also, you can create a tree that does not have the ParensE constructor, but still requires parentheses to be faithfully â€ślinearizedâ€ť into a line of text.
I knew that Coq doesnâ€™t have a builtin type for booleans and assumed similar approach for notationâ€™s semantic.
Absence of parentheses complicates formatting preservation during automatic code refactoring (e.g. theorem / variable rename).
coqlsp must have a forked parser to cover this then.