Pierre Roux (Sep 06 2023 at 07:41): Pierre Roux (Sep 06 2023 at 07:41):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
Hugo Herbelin (Sep 06 2023 at 14:25):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.
Hugo Herbelin (Sep 06 2023 at 14:39):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) * yBinInt.Zopp_mult_distr_l : - (n * m) = - n * mZdivfloor.div_opp_opp : b~=0 -> -a/-b == a/bField_theory.rdiv5 : - (a / b) == - a / bUint63.opp_spec : φ (- x) = - φ x mod wB-a÷b in Zquote.v- Qnum x * Zpos (Qden y) in QArith_base.vI'm afraid this starts to be significant.
Pierre Roux (Sep 06 2023 at 14:44):Hugo Herbelin said:
I also experimented moving binders to level 10 in #18014: it morally introduces one real conflict: the
λutf8 notation forfunconflicts with a legitimate notation"'λ' t"for lambda-terms in de Bruijn notation.
That sounds very positive, the number of conflicts look very limited.
Pierre Roux (Sep 06 2023 at 14:45):Hugo Herbelin said:
Regarding changing
- x * yto- (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.
Paolo Giarrusso (Sep 06 2023 at 18:17):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
Paolo Giarrusso (Sep 06 2023 at 18:21):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.
Pierre Roux (Sep 06 2023 at 18:49):Sure, we're expecting an impact, the question is more about its "size".
Guillaume Melquiond (Sep 06 2023 at 19:03):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
Guillaume Melquiond (Sep 06 2023 at 19:24):I expect 0 - x and - x with x a multiplicative term to have the same value.
Guillaume Melquiond (Sep 06 2023 at 19:26):The arity of the minus symbol should not change the interpretation of a multiplicative term.
Paolo Giarrusso (Sep 06 2023 at 19:27):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.
Guillaume Melquiond (Sep 06 2023 at 19:32):The whole issue us about the precedence. If your example does not rely on the precedence, then it kind of misses the point.
Paolo Giarrusso (Sep 06 2023 at 20:07):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.
Guillaume Melquiond (Sep 07 2023 at 06:59):This is just Euclidean division. Most people would agree (I hope) that it is hardly exotic.
Guillaume Melquiond (Sep 07 2023 at 06:59):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.
Guillaume Melquiond (Sep 07 2023 at 06:59):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.
Michael Soegtrop (Sep 07 2023 at 13:21):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.
Guillaume Melquiond (Sep 07 2023 at 14:48):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).
Pierre Roux (Sep 07 2023 at 14:58):FYI, making the change requires adding:
Last updated: Sep 09 2024 at 04:02 UTC