Is there any reason why the `int`

type (primitive integers) is actually for *unsigned* integers?

I second this question. (See also https://github.com/coq/coq/issues/12109) Assuming there is no deep reason, is someone working on extending the Coq primitive integers to actual signed integers? And if there isn't, would there be interest in this?

My team wants to use primitive signed integers and we're probably going to come up with a way of doing it, more or less hacky. We would be glad to do it in a way that actually improves Coq for everyone.

I'd also motion for fixing the name, beyond all other things. A bit disappointed nobody noticed (me included), especially since this was a recent addition.

Fixing the name is pointless. This is modulo arithmetic. Whether the type is signed or not, the results will be absolutely identical for addition, subtraction, multiplication, and so on. The only operations that actually care about signedness are comparison and division. So, it would be much more productive to just add a signed comparison and a signed division.

What about shift and sign-extension (conversion to Z)?

Guillaume Melquiond said:

Fixing the name is pointless. This is modulo arithmetic. Whether the type is signed or not, the results will be absolutely identical for addition, subtraction, multiplication, and so on. The only operations that actually care about signedness are comparison and division. So, it would be much more productive to just add a signed comparison and a signed division.

This is not entirely true, the interpretation from and to `Z`

would also differ.

And the printing...

Actually, it would be more accurate to say that only the addition, subtraction and multiplication are the same....

(i.e. the ring structure)

uh, https://coq.github.io/doc/v8.12/refman/changes.html#id420 claims that this was the `UInt63`

module?

but https://coq.github.io/doc/v8.12/refman/language/core/primitive.html#primitive-integers suggests that Coq's Int maps to OCaml UInt.

the `UInt63`

ref might be to this file: https://github.com/coq/coq/blob/master/kernel/uint63.mli

Cyril Cohen said:

(i.e. the ring structure)

That is a rather restrictive view. There are also: clz (head0), ctz (tail0), and, or, xor, lsl, lsr, funnel shifter (addmuldiv), sqrt. But I agree that conversion to Z would be different (and thus printing too).

I think there are at least two options:

- Define signed comparison, division, etc by, for example, taking
`[0, max_int/2]`

as the positive numbers and`]max_int/2, max_int]`

as the negative numbers. - Actually use the OCaml integers, instead of only OCaml's unsigned integers.

As far as I can tell, Option 1 is more high-level, possibly easier, but less efficient, while Option 2 would imply increasing the kernel, but it would then allow for efficient extraction to Ocaml's `int`

, including `int`

functions such as comparison.

Am I accurately describing reality? Which of these options would you prefer?

I am not sure why you say that Option 1 is higher level. I would call it lower level, as it is much closer to the actual hardware. Most (if not all) processors do not have separate signed and unsigned registers. They do not have signed and unsigned additions. By the way, even for OCaml, the situation is not that clear cut. For example, the `Int32`

module provides both a signed division `div`

and an unsigned one `unsigned_div`

(and similarly for comparison).

I think processors have at least distinct (1) shifts (2) number extensions — but that's not so important.

the efficiency question is important

@Guillaume Melquiond can one make primitive integers (and their axiom) match standard processors, and then do the remaining reasoning in Coq?

for shared operations, instead of having 2 copies of the same axioms, maybe one could have only 1 copy (say, for addition), and some "adapters".

so one axiom on "primitive addition" can imply theorems both about "Coq unsigned integers" (today) and "Coq signed integers".

I realize this sounds like option 1, except this should not affect efficiency of the actual code.

OTOH, @Guillaume Melquiond, signed and unsigned comparisons _are_ distinct operations even in assembly, IIUC (on x86 there's a single operation, but you test different flags for the signed and unsigned cases)

Last updated: Oct 13 2024 at 01:02 UTC