Coq eats expression parentheses

Using Coq
1

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.


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)
2 
Set Printing Parentheses.
1 Like
3

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

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

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.

5

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

6

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.

1 Like
7

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

8

Set Printing Parentheses. will ensure all parantheses are printed

9

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

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.

11

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.