I added a few notes about yesterday's call: https://github.com/coq/coq/wiki/Coq-Call-2023-09-05

Those are not actual notes but only what I remember this morning, I certainly forgot many things, feel free to edit @Gaëtan Gilbert @Guillaume Melquiond @Hugo Herbelin @Matthieu Sozeau @Pierre-Marie Pédrot

I then added Guillaume's remark on unary minus parsing on its right at the same level of the previous symbol. If other symbols than unary minus behave so, that may be worth a specific kind of notations. Otherwise, adding specific notations `x + - y`

, `x * - y`

and `x ^ - y`

would be enough. I also experimented moving binders to level 10 in #18014: it morally introduces one real conflict: the `λ`

utf8 notation for `fun`

conflicts with a legitimate notation `"'λ' t"`

for lambda-terms in de Bruijn notation.

Regarding changing `- x * y`

to `- (x * y)`

by default, there are several instances in stdlib which would be impacted:

`Ring_theory.Ropp_mul_l : -(x * y) == -x * y`

(also in`Ncring.v`

) and`Ring_theory.ARopp_mul_l : -(x * y) == (-x) * y`

`BinInt.Zopp_mult_distr_l : - (n * m) = - n * m`

`Zdivfloor.div_opp_opp : b~=0 -> -a/-b == a/b`

`Field_theory.rdiv5 : - (a / b) == - a / b`

`Uint63.opp_spec : φ (- x) = - φ x mod wB`

`-a÷b`

in`Zquote.v`

`- Qnum x * Zpos (Qden y)`

in`QArith_base.v`

- etc.

I'm afraid this starts to be significant.

Hugo Herbelin said:

I also experimented moving binders to level 10 in #18014: it morally introduces one real conflict: the

`λ`

utf8 notation for`fun`

conflicts with a legitimate notation`"'λ' t"`

for lambda-terms in de Bruijn notation.

That sounds very positive, the number of conflicts look very limited.

Hugo Herbelin said:

Regarding changing

`- x * y`

to`- (x * y)`

by default, there are several instances in stdlib which would be impacted:

[...]

I'm afraid this starts to be significant.

We were expecting that. If there are just a few dozen places where parentheses have tobe added, I would tend to think it's fine.

would fix - a * b being parsed (- a) * b instead of - (a * b)

Why's that a fix? I'm not sure I've seen languages with this strange priority

Hm, it seems both conventions are in use https://en.wikipedia.org/wiki/Order_of_operations#Unary_minus_sign. Either way, the impact surely isn't limited to the stdlib.

Sure, we're expecting an impact, the question is more about its "size".

Here is an example that shows how broken the current notation is:

```
Require Import Zdiv.
Goal (- 1/2 <> 0 - 1/2)%Z.
Proof. discriminate. Qed.
```

IDK, is that broken? I feel like `((-1) / 2 = -1)%Z`

causes my intuition to break down so I don't know what to expect

I expect `0 - x`

and `- x`

with `x`

a multiplicative term to have the same value.

The arity of the minus symbol should not change the interpretation of a multiplicative term.

I agree with Gaëtan, I can't tell if I've ever used `- 1/2`

when precedence matters; usually unary minus is equivalent `(-1)*`

so precedence doesn't matter by associativity.

```
Require Import Zdiv.
Eval cbv in ((-1) / 2)%Z. (* = (-1)%Z : Z *)
Eval cbv in (1 / 2)%Z. (* = 0%Z : Z *)
Goal ((- 1)/2 <> - (1/2))%Z.
Proof. discriminate. Qed.
```

^^ A variant of that example not relying on precedence.

The whole issue us about the precedence. If your example does not rely on the precedence, then it kind of misses the point.

either that, or the real problem is with division in `Z`

, and worrying about precedence kind of misses the point. I genuinely don't know which precedence would fit more the expectation of Coq users at large.

This is just Euclidean division. Most people would agree (I hope) that it is hardly exotic.

Consider another example. What would you think of a parser of mathematical formulas that parses `- x^y`

as `(- x)^y`

(and in particular, of a tool such as Excel where `- 3^2`

ends up being equal to `9`

due to parsing)? Luckily, in Coq, this is not the case, because the precedence of unary minus was set between multiplication and exponentiation. But this is just a lucky accident.

In my opinion, the precedence of an operator should match its most common semantics to reduce the amount of surprise for users. In other words, all the additive operators (addition, subtraction, negation) should have roughly the same precedence, all the multiplicative operators (multiplication, division, inverse) should have roughly the same precedence, and so on. You should not just give some random precedence to operators.

I am not sure one can say this is about precedence - it is about if division should "round" towards minus infinity or zero. Actually the Coq standard library has an implementation for both flavours of division:

```
Require Import ZArith.
Eval cbv in Z.div (-1) 2. (* -1 "rounded" towards - inf *)
Eval cbv in Z.div 1 2. (* 0 "rounded" towards - inf *)
Eval cbv in Z.quot (-1) 2. (* 0 "rounded" towards 0 *)
Eval cbv in Z.quot 1 2. (* 0 "rounded" towards 0 *)
```

I agree with Coq that the "usual" integer division should "round" towards minus infinity, so that the remainder of a negative number over a positive number is positive (= the modulus). If one rounds division towards 0, so that one can pull in/out the sign of the numerator, the remainder of negative / positive is negative and unequal the modulus, which is rather inconvenient in many cases.

Again, I was not advocating for or against the way the division is defined in `Zdiv`

. My point was just that `0 - 1/2`

and `- 1/2`

are parsed in two completely different ways (which is painfully apparent when the division happens to be the Euclidean one).

FYI, making the change requires adding:

- in the stdlib, about 130 pairs of parentheses (mostyl in proofs in Real): https://github.com/proux01/coq/commit/020d6f6da2306b73ad937de05ad50b493644d1f5
- in mathcomp, 28 pairs of parentheses: https://github.com/proux01/math-comp/commit/58749977d0d7c1c045a3f07b93888efe1588cc25

Last updated: Sep 09 2024 at 04:02 UTC