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.

Hofmann

Answer 1

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

Ctenoid

Answer 2

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.

Liar

It would be great if there was an intermediate flag that only added the implicit parentheses. Perhaps something like "Set Printing Parentheses". – Nitroglycerin

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.

Mcalister

Hmm, here is a crazy idea: can we include parens into the notation "'(' A :||: B ')'" and send it to level 0? I tried it on nat's +: e.g. 1 + 2 * 3 parses correctly, and (1 + 2) + (3 + 4) gets printed with all the parens, including the toplevel ones, unfortunately. I'm wondering what would be the downsides of this approach. – Haletta

You indeed can do that, but doesn't it break normal parenthesis parsing? – Mcalister

I've tried several examples, but didn't find it breaks parsing in any way. Maybe I just wasn't lucky enough. – Haletta

Can you post a complete example? – Mcalister

Notation "'(' x + y ')'" := (plus x y) (at level 0, left associativity). – Haletta

I see. However, you need to declare it at level 0, this will print ` (A :\: A :||: A :&: B)` instead of ` (A :\: A) :||: (A :&: B)`, right? – Mcalister

You're right. I meant we could redefine (A :\: A) and (A :&: B) in that way. Can't try it right now, it seems I somehow broke my ssreflect installation. – Haletta

I tried and I got mixed results: (A :&: A) :|: A :&: B = B – Mcalister

Interesting, so it dropped the second pair of parens in this expression (A :&: A) :|: (A :&: B) = B? I tried a somewhat analogous thing with nats: Notation "'(' x * y ')'" := (Nat.mul x y) (at level 0, left associativity)., and it seems to keep the parens: Goal (1 * 1) + (1 * 2) = 3. gives as (1 * 1) + (1 * 2) = 3 as a goal. – Haletta

I did a mistake, sorry, my bad. It seems to work fine now. – Mcalister

Local Notation "'(' A :\: B ')'" := (@setD T A B) (at level 0, left associativity). Local Notation "'(' A :&: B ')'" := (@setI A B) (at level 0, left associativity). – Mcalister

Thank you for your answer and informative comments. Indeed, the work around is much more complicated (and nasty) than I had expected... I had imagined that Coq might have a command like Set Print Parentheses Level 4. I should learn the precedence of the operators rather than introducing Local Notations. Is there any reference that explain the precedence? For example, why can you tell me :\: and :&: are higher than :|:? Where in its source code does Coq define these? – Hofmann

Let me explain my concern more... You wrote The current precedence of :|: is what is expected by mathematicians. But I guess mathematicians dislike an ill-defined formula such as $A \cup B \cap C$ unless the precedence is not pre-given. So I guess that Coq (or related libraries) strictly define the precedence. I would like to know the precedence in Coq. – Hofmann

@Hofmann I'm not aware of any easy command for that, but (1) You can look for precedence levels in the source (but it's not always there). You need Notation ... (at level ...). But it can be Reserved Notation defined elsewhere. (2) So you could just load your modules and issue the Print Grammar constr. command and search through the output. Backslashes are doubled due to escaping. You need to search for :\\: if you want to find out the level of :\: (it's level 50 and left-associative, by the way). P.S. Just in case: level 0 means the most strong binding. HTH – Haletta

In addition to the very good suggestions by Anton, the concrete definition for the set notations is here: github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/… – Mcalister