## Stream: maths

### Topic: Alternative representations of Z

#### 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/

#### Johan Commelin (Jul 02 2020 at 13:24):

I think that's already happening under the hood

#### 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)

#### Johan Commelin (Jul 02 2020 at 13:26):

What do you mean with that?

#### Johan Commelin (Jul 02 2020 at 13:26):

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

#### 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.

#### Reid Barton (Jul 02 2020 at 13:27):

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

#### 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

#### 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.

#### Karl Palmskog (Jul 02 2020 at 13:28):

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

#### 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.

#### Johan Commelin (Jul 02 2020 at 13:31):

@Karl Palmskog I never use of_nat explicitly.

#### Johan Commelin (Jul 02 2020 at 13:32):

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

#### 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.

#### 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.)

#### Mario Carneiro (Jul 02 2020 at 14:04):

norm_num does not use znum

#### Mario Carneiro (Jul 02 2020 at 14:04):

in fact it doesn't use integers at all

#### 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

#### 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

#### Reid Barton (Jul 02 2020 at 14:10):

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

#### Mario Carneiro (Jul 02 2020 at 14:14):

that would be interesting

#### Mario Carneiro (Jul 02 2020 at 14:15):

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

#### 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

#### 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

#### 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)

#### 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)

#### Kevin Buzzard (Jul 03 2020 at 19:27):

How is it different?

Last updated: May 11 2021 at 16:22 UTC