# Coq eats expression parentheses

**URL:** <https://discourse.rocq-prover.org/t/coq-eats-expression-parentheses/2442>\
**Category:** Using Rocq\
**Created:** [October 3, 2024, 10:45pm UTC](https://discourse.rocq-prover.org/t/coq-eats-expression-parentheses/2442 "2024-10-03T22:45:55Z")\
**Posts on this page:** 11\
**Page:** 1

<div class="post-metadata">

**Author:** ![shutterrecoil](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/shutterrecoil/32/1036_2.png) [@shutterrecoil](https://discourse.rocq-prover.org/u/shutterrecoil)\
**Post date:** [October 3, 2024, 10:45pm UTC](https://discourse.rocq-prover.org/t/coq-eats-expression-parentheses/2442/1 "2024-10-03T22:45:55Z")

</div>

Hi,

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.

```auto

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:

```auto
  n', m, p : nat
  IHn : n' + (m + p) = n' + m + p
  ============================
  S (n' + (m + p)) = S (n' + m + p)

```

---

<div class="post-metadata">

**Author:** ![davidjao](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/davidjao/32/866_2.png) [@davidjao](https://discourse.rocq-prover.org/u/davidjao)\
**Post date:** [October 3, 2024, 11:10pm UTC](https://discourse.rocq-prover.org/t/coq-eats-expression-parentheses/2442/2 "2024-10-03T23:10:37Z")

</div>

```auto
Set Printing Parentheses.

```

---

<div class="post-metadata">

**Author:** ![shutterrecoil](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/shutterrecoil/32/1036_2.png) [@shutterrecoil](https://discourse.rocq-prover.org/u/shutterrecoil)\
**Post date:** [October 4, 2024, 1:25am UTC](https://discourse.rocq-prover.org/t/coq-eats-expression-parentheses/2442/3 "2024-10-04T01:25:04Z")

</div>

Thanks for the option, but it affects only formatting imho, because following prove is accepted:

```auto
Set Printing Parentheses.
Lemma l : forall n m p : nat, n + m + p = (n + m) + p.
Proof.
  reflexivity.
Qed.

```

---

<div class="post-metadata">

**Author:** ![davidjao](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/davidjao/32/866_2.png) [@davidjao](https://discourse.rocq-prover.org/u/davidjao)\
**Post date:** [October 4, 2024, 1:37am UTC](https://discourse.rocq-prover.org/t/coq-eats-expression-parentheses/2442/4 "2024-10-04T01:37:13Z")

</div>

Well, Coq can only control what it prints. If you want parentheses in your own theorem statement, you need to put the parentheses in there yourself.

---

<div class="post-metadata">

**Author:** ![shutterrecoil](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/shutterrecoil/32/1036_2.png) [@shutterrecoil](https://discourse.rocq-prover.org/u/shutterrecoil)\
**Post date:** [October 4, 2024, 4:15am UTC](https://discourse.rocq-prover.org/t/coq-eats-expression-parentheses/2442/5 "2024-10-04T04:15:53Z")

</div>

reflexivity tactic is too smart. Is there **strcmp** tactic in the Coq toolbox?  
Such literal reflexivity tactic would be faster.

---

<div class="post-metadata">

**Author:** ![JoJoDeveloping](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/jojodeveloping/32/886_2.png) [@JoJoDeveloping](https://discourse.rocq-prover.org/u/JoJoDeveloping)\
**Post date:** [October 4, 2024, 4:49am UTC](https://discourse.rocq-prover.org/t/coq-eats-expression-parentheses/2442/6 "2024-10-04T04:49:22Z")

</div>

I’m not sure what you expected here…

Coq does not work with “stream of symbol” expressions. Expressions are naturally tree-shaped, and Coq internally uses that tree everywhere, except when printing and parsing human-readable 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 left-associative, 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.

---

<div class="post-metadata">

**Author:** ![Matafou](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/matafou/32/18_2.png) [@Matafou](https://discourse.rocq-prover.org/u/Matafou)\
**Post date:** [October 4, 2024, 7:23am UTC](https://discourse.rocq-prover.org/t/coq-eats-expression-parentheses/2442/7 "2024-10-04T07:23:49Z")

</div>

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 “left-associativity 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 re-read into an identical one”, this is called the “re-entering pretty printing”.

---

<div class="post-metadata">

**Author:** ![yforster](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/yforster/32/30_2.png) [@yforster](https://discourse.rocq-prover.org/u/yforster)\
**Post date:** [October 4, 2024, 7:37am UTC](https://discourse.rocq-prover.org/t/coq-eats-expression-parentheses/2442/8 "2024-10-04T07:37:44Z")

</div>

`Set Printing Parentheses.` will ensure all parantheses are printed

---

<div class="post-metadata">

**Author:** ![shutterrecoil](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/shutterrecoil/32/1036_2.png) [@shutterrecoil](https://discourse.rocq-prover.org/u/shutterrecoil)\
**Post date:** [October 4, 2024, 5:00pm UTC](https://discourse.rocq-prover.org/t/coq-eats-expression-parentheses/2442/9 "2024-10-04T17:00:15Z")

</div>

> [@JoJoDeveloping](#):
>
> I’m not sure what you expected here…
> 
> Coq does not work with “stream of symbol” expressions. Expressions are naturally tree-shaped, and Coq internally uses that tree everywhere, except when printing and parsing human-readable 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 left-associative, 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.

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:

```auto
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) }@
  ...

```

---

<div class="post-metadata">

**Author:** ![JoJoDeveloping](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/jojodeveloping/32/886_2.png) [@JoJoDeveloping](https://discourse.rocq-prover.org/u/JoJoDeveloping)\
**Post date:** [October 8, 2024, 10:01am UTC](https://discourse.rocq-prover.org/t/coq-eats-expression-parentheses/2442/10 "2024-10-08T10:01:51Z")

</div>

> [@shutterrecoil](#):
>
> expression type doesn’t have data constructor for parentheses like Haskell does:

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.

---

<div class="post-metadata">

**Author:** ![shutterrecoil](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/shutterrecoil/32/1036_2.png) [@shutterrecoil](https://discourse.rocq-prover.org/u/shutterrecoil)\
**Post date:** [October 8, 2024, 7:44pm UTC](https://discourse.rocq-prover.org/t/coq-eats-expression-parentheses/2442/11 "2024-10-08T19:44:59Z")

</div>

> [@JoJoDeveloping](#):
>
> 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.

I knew that Coq doesn’t have a built-in 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).  
coq-lsp must have a forked parser to cover this then.