Alternative representations of Z

Stream: maths

[Karl Palmskog]

I just listened quickly to Kevin Buzzard's Tuesday Lean lecture on Twitch, where the issue of representing the integers/Z was raised. Is the Lean community aware of the binary encoding of integers used in the Coq standard library? https://coq.inria.fr/distrib/V8.11.0/stdlib/Coq.Numbers.BinNums.html#Z - perhaps this is something that could be adapted to Mathlib, since it has nice properties for computation and reasoning (generally doesn't overflow).

In particular, the representations works well in extracted code: the CompCert compiler internally uses this Z in lieu of (bounded) machine integers. There is also a Coq framework which allows automatically refining any functions that use nat to instead use binary integers defined in this way: https://github.com/CoqEAL/CoqEAL/

[Johan Commelin]

I think that's already happening under the hood

[Karl Palmskog]

well, in any case, it could still be nice to use as the surface representation (most Coq people do)

[Johan Commelin]

What do you mean with that?

[Johan Commelin]

We have nat (unary), and num (binary nats).

[Reid Barton]

We have docs#znum but it doesn't see much use because we tend not to rely on kernel reduction, and for int there is another mechanism to override the implementation in the VM.

[Reid Barton]

Does norm_num use znum somehow? I don't know.

[Karl Palmskog]

well, I just mean it has more natural constructors than what Kevin showed in the lecture, Z0, Zpos, Zneg

[Johan Commelin]

@Karl Palmskog You don't suggest to prove theorems about int using the binary representation, right? So you must mean something else.

[Karl Palmskog]

I see, so you have it, but instead people use the of_nat constructors?

[Reid Barton]

For int, I think the choice of representation doesn't matter too much for proving, once one has all the standard API bits. For nat it is common to do cases/induction forever, though.

[Johan Commelin]

@Karl Palmskog I never use of_nat explicitly.

[Johan Commelin]

Maybe under the hood, but the API doesn't let me know about it.

[Johan Commelin]

If I have a nat and I need an int, automatic coercion will deal with it for me.

[Johan Commelin]

But maybe I'm still misunderstanding you. (I'm far from an expert on the foundational things and design decisions.)

[Mario Carneiro]

norm_num does not use znum

[Mario Carneiro]

in fact it doesn't use integers at all

[Mario Carneiro]

well, I suppose int is used during execution in the VM to keep track of how the proof is going, but the generated proofs contain no references to int unless the proof is actually about int

[Mario Carneiro]

When the VM computes with int, it uses GMP bignums, which is more efficient than Coq's Z

[Reid Barton]

In principle znum could also get the special GMP treatment, right?

[Mario Carneiro]

that would be interesting

[Mario Carneiro]

it would mean that znum -> int and vice versa is a no-op

[Reid Barton]

I was thinking that if it's indeed the case that the definitional behavior of int isn't so important once the basic theory is set up, we could even swap in znum for int and get both fast(er) kernel reduction and fast VM computation

[Mario Carneiro]

I think the definition of int is inspected sufficiently often that this would be far from painless

[Mario Carneiro]

plus you can always use znum for those particular cases where kernel computation matters (which is essentially zero cases right now AFAIK, probably in no small part due to my explicit discouragement of the practice when it comes up)

[Karl Palmskog]

For completeness here, I should also mention the int representation in MathComp, which is subtly different from, but very close to, Lean's Z: https://github.com/math-comp/math-comp/blob/master/mathcomp/algebra/ssrint.v#L58 (as usual in MathComp, this one is to my understanding optimized for computations/reflection inside proofs)

[Kevin Buzzard]

How is it different?