Michael Soegtrop (Mar 10 2021 at 11:38): Michael Soegtrop (Mar 10 2021 at 11:38):As it looks for large Q the output defaults to Hex, e.g. (0x7329a77b86b6c4e.16ba0c09fffffffe%xQ). For small Q I get (27 # 2). Is this intentional, e.g. a performance optimization? I find this rather inconvenient, because it makes it quite hard to past terms to math software like Maxima or Mathematica.
Pierre Roux (Mar 10 2021 at 15:27):@Michael Soegtrop looks like a bug, would you have a small example?
Michael Soegtrop (Mar 10 2021 at 17:06):@Pierre Roux : Here is a small example (Coq 8.13.1):
Require Import QArith.
Open Scope Q.
Eval compute in (10#2)^20.
gives
= 0x56bc75e2d631.00000%xQ
: Q
With exponent 10 the output is decimal.
Pierre Roux (Mar 10 2021 at 17:15):Thanks, I'll have a look
Michael Soegtrop (Mar 10 2021 at 17:37):Btw.: I think this only happens if the denominator is a power of two. If the denominator is a large power of 10 similar stuff happens, e.g.:
Require Import QArith.
Open Scope Q.
Eval compute in (13#10)^20.
gives
= 190.04963774880799438801
: Q
So there seems to be some heuristic to switch between fractional and dyadic representation.
Michael Soegtrop (Mar 10 2021 at 18:01):P.S.: I would really like if one could choose between fractional and dyadic/positional representation in some way.
I also have an idea on how to represent fractions with periodic positional form in a unique and short way. Since a/b - c/d = (a * d - c * b) / (b * d) is 0 if both fractions are equal and otherwise >= 1/b*d it is sufficient to truncate the periodic representation after twice the number of digits the denominator has. E.g. one could write 1/7=0.14... . Since the representation has two digits it denotes a fraction with one digit in the denominator and there can only be one fraction which has the truncated representation 0.14... since as shown different fractions with one digit in the denominator have a difference of at least 1/81 > 0.01.
Please note that the usual periodic representation one uses in school is not feasible since the number of digits in the periodic part of a positional representation can grow exponentially with the number of digits of the denominator, while the proposed representation has at most 2x the number of digits of the fractional form.
Pierre Roux (Mar 11 2021 at 15:53):Interesting, that reminds me the decimal notation used for floats.
Pierre Roux (Mar 11 2021 at 15:57):And indeed, the choice between decimal and hexadecimal representation seems to be based on the denominator, when t is a power of 10 --> decimal, otherwise when it is a power of 2 --> hexadecimal. A way to avoid that proposed by @Guillaume Melquiond would be to tag the constants with an identity function, you could declare it simpl never, but if you do a vm_compute, the tag will vanish anyway, so maybe not a perfect solution.
Michael Soegtrop (Mar 12 2021 at 18:13):Interesting, that reminds me the decimal notation used for floats.
Yes, but it would be a decimal notation for exact rationals. For me as physicist such a notation would be useful especially on output, because it gives an indication of the size of the number. Rationals with 20 digits in numerator and denominator are hard to judge without conversion to float. The proposal could solve this. Do you think it would make sense to have such a notation in Coq, so that one can choose between decimal and fractional notation of rationals on output? I would denote truncation decimal notations with 3 dots, say 0.33... = 1/3 to distinguish from 0.33=33/100.
Michael Soegtrop (Mar 12 2021 at 18:18):A way to avoid that proposed by @Guillaume Melquiond would be to tag the constants with an identity function, you could declare it simpl never, but if you do a vm_compute, the tag will vanish anyway, so maybe not a perfect solution.
I like this idea. It wouId be nice to be able to have 1/2 and 0.5 in one term.
Pierre Roux (Mar 17 2021 at 13:54):@Michael Soegtrop sorry for the late answer, I finally got a closer look, the code is here https://github.com/coq/coq/blob/master/theories/QArith/QArith_base.v#L425 (and above)
the logic is as follows (except if hex_Q_scope is opened):
n # dIn your example (10#2)^20, the denominator is literally 2^20, not a power of 10 but a power of 2. If instead of (10#2)^20 you compute
Eval compute in Qred (10#2)^20
the fraction is reduced with a denominator 1 and printed as decimal.
Pierre Roux (Mar 17 2021 at 13:57):I would denote truncation decimal notations with 3 dots, say 0.33... = 1/3 to distinguish from 0.33=33/100.
Would be nice. I wonder whether this is doable in pure Coq (without having to hack the OCaml code), the documentation is there: https://coq.inria.fr/refman/user-extensions/syntax-extensions.html feel free to ask about the Number Notation part which I know rather well, but I'm unfortunately less qualified about the non number parts (which would be required to print the trailing ...)
Michael Soegtrop (Mar 17 2021 at 15:54):I must say, I don't find the hex heuristic very agreeable. I would prefer if one could import different modules or open different scopes to choose between these representations. The a#b should be the default IMHO. But then this won't work well without the suggested truncated representation, because as is the positional representations only work for the very restricted set of denominators you stated.
I will look into it!
Pierre Roux (Mar 19 2021 at 10:01):There are already scopes, unfortunately, closing them does not deactivate printing (the semantics of open/cose scope on printing is still an issue in my opinion (it's not even consistent between number and regular notations), but that's a difficult to solve without completely breaking backward compatibility).
Last updated: Apr 16 2024 at 08:02 UTC