can I force Coq to print parentheses?

Question

I'm new to Coq, working on set-theoretic proof writing.

I realized that parentheses are omitted, and it makes difficult for me to read the formula. For example,

1 subgoal
A, B : {set T}
H : B \subset A
______________________________________(1/1)
A :\: A :|: A :&: B = B

But I would like Coq to print (A :\: A) :|: (A :&: B) = B. This output above is gained by the foloowing code.

Require Import ssreflect ssrbool ssrnat fintype finset.
Theorem a_a_b__b' (A B : {set T}) : B \subset A -> (A :\: (A :\: B)) = B.
Proof.
  move=> H.
  rewrite setDDr.

To my surprise, if I see the original coding of setDDr in finset.v, it has parentheses as follows

Lemma setDDr A B C : A :\: (B :\: C) = (A :\: B) :|: (A :&: C).
Proof. by rewrite !setDE setCI setIUr setCK. Qed.

So I'm wondering why parentheses disappear and how to force Coq to print parentheses explicitly in CoqIde.

Answer 1

You can turn off all notations with this command:

Unset Printing Notations.

Printing Notations is a flag, Unset turns it off. You can find more information about notation from here: https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#syntax-extensions-and-interpretation-scopes.

For example,

(n + m) * 0 = n * 0 + m * 0

would be printed as

eq (Nat.mul (Nat.add n m) O) (Nat.add (Nat.mul n O) (Nat.mul m O))

I know, it's not a really good solution.

Answer 2

In the latest versions of Coq Set Printing Parentheses should work.

Answer 3

I am not aware of a mechanism to do what you propose (but it could well exist, Coq notation support is rich and complex).

Coq is supposed to insert parenthesis based on the precedence of the operators, that means that you'll have to redefine the precedence of :|: to achieve what you want. This is not possible to do easily, and most people won't like it. The current precedence of :|: is what is expected by mathematicians.

A possible workaround is to define a different, local notation for you own use:

From mathcomp
Require Import ssreflect ssrbool eqtype ssrnat seq choice fintype finset.

Section U.

Variable (T: finType).

Local Notation "A :||: B" := (@setU T A B) (at level 48, left associativity).

Theorem a_a_b__b' (A B : {set T}) : B \subset A -> (A :\: (A :\: B)) = B.
Proof.
move=> H; rewrite setDDr.

But I'd suggest you use this only temporarily, try to get used to the current precedence rules, as you'll have to read other people proofs, and they'll have to read yours, so deviating from standard practice has a non trivial cost.