9

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.

Pengin
  • 771
  • 1
  • 10
  • 16

3 Answers3

3

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.

Khoa Vo
  • 334
  • 3
  • 11
  • It would be great if there was an intermediate flag that only added the implicit parentheses. Perhaps something like "Set Printing Parentheses". – Ricardo Jan 05 '20 at 03:57
3

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

Rincewind
  • 197
  • 1
  • 1
  • 9
1

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.

ejgallego
  • 6,709
  • 1
  • 14
  • 29
  • 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. – Anton Trunov Oct 04 '16 at 09:17
  • You indeed can do that, but doesn't it break normal parenthesis parsing? – ejgallego Oct 04 '16 at 09:53
  • I've tried several examples, but didn't find it breaks parsing in any way. Maybe I just wasn't lucky enough. – Anton Trunov Oct 04 '16 at 09:56
  • Can you post a complete example? – ejgallego Oct 04 '16 at 10:28
  • 4
    `Notation "'(' x + y ')'" := (plus x y) (at level 0, left associativity).` – Anton Trunov Oct 04 '16 at 10:33
  • 1
    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? – ejgallego Oct 04 '16 at 10:46
  • 1
    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. – Anton Trunov Oct 04 '16 at 10:50
  • I tried and I got mixed results: `(A :&: A) :|: A :&: B = B` – ejgallego Oct 04 '16 at 10:54
  • 1
    Interesting, so it dropped the second pair of parens in this expression `(A :&: A) :|: (A :&: B) = B`? I tried a somewhat analogous thing with `nat`s: `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. – Anton Trunov Oct 04 '16 at 11:13
  • I did a mistake, sorry, my bad. It seems to work fine now. – ejgallego Oct 04 '16 at 11:20
  • 1
    `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). ` – ejgallego Oct 04 '16 at 11:21
  • 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 Notation`s. 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? – Pengin Oct 04 '16 at 15:14
  • 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_. – Pengin Oct 04 '16 at 15:19
  • 1
    @Pengin 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 – Anton Trunov Oct 04 '16 at 17:05
  • In addition to the very good suggestions by Anton, the concrete definition for the set notations is here: https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/ssrfun.v#L281 – ejgallego Oct 04 '16 at 21:38