Zulip Chat Archive

Stream: maths

Topic: Alternative representations of Z


view this post on Zulip Karl Palmskog (Jul 02 2020 at 13:23):

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/

view this post on Zulip Johan Commelin (Jul 02 2020 at 13:24):

I think that's already happening under the hood

view this post on Zulip Karl Palmskog (Jul 02 2020 at 13:25):

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

view this post on Zulip Johan Commelin (Jul 02 2020 at 13:26):

What do you mean with that?

view this post on Zulip Johan Commelin (Jul 02 2020 at 13:26):

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

view this post on Zulip Reid Barton (Jul 02 2020 at 13:26):

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.

view this post on Zulip Reid Barton (Jul 02 2020 at 13:27):

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

view this post on Zulip Karl Palmskog (Jul 02 2020 at 13:27):

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

view this post on Zulip Johan Commelin (Jul 02 2020 at 13:27):

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

view this post on Zulip Karl Palmskog (Jul 02 2020 at 13:28):

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

view this post on Zulip Reid Barton (Jul 02 2020 at 13:29):

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.

view this post on Zulip Johan Commelin (Jul 02 2020 at 13:31):

@Karl Palmskog I never use of_nat explicitly.

view this post on Zulip Johan Commelin (Jul 02 2020 at 13:32):

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

view this post on Zulip Johan Commelin (Jul 02 2020 at 13:32):

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

view this post on Zulip Johan Commelin (Jul 02 2020 at 13:32):

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

view this post on Zulip Mario Carneiro (Jul 02 2020 at 14:04):

norm_num does not use znum

view this post on Zulip Mario Carneiro (Jul 02 2020 at 14:04):

in fact it doesn't use integers at all

view this post on Zulip Mario Carneiro (Jul 02 2020 at 14:06):

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

view this post on Zulip Mario Carneiro (Jul 02 2020 at 14:07):

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

view this post on Zulip Reid Barton (Jul 02 2020 at 14:10):

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

view this post on Zulip Mario Carneiro (Jul 02 2020 at 14:14):

that would be interesting

view this post on Zulip Mario Carneiro (Jul 02 2020 at 14:15):

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

view this post on Zulip Reid Barton (Jul 02 2020 at 14:19):

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

view this post on Zulip Mario Carneiro (Jul 02 2020 at 14:24):

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

view this post on Zulip Mario Carneiro (Jul 02 2020 at 14:25):

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)

view this post on Zulip Karl Palmskog (Jul 03 2020 at 18:14):

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)

view this post on Zulip Kevin Buzzard (Jul 03 2020 at 19:27):

How is it different?


Last updated: May 11 2021 at 16:22 UTC