How can I avoid stack overflow or segmentation fault in Coq nats?

Question

I'm currently working with vellvm, developing a transformation on it. I'm a coq newbie.

While programming, I faced the following warning:

Warning: Stack overflow or segmentation fault happens when working with large numbers in nat (observed threshold may vary from 5000 to 70000 depending on your system limits and on the command executed).

My function that generates this warning calculates a signature. The signature is divided in superior and inferior bits. Given two nats n1 and n2 representing the superior bits and the inferior bits, it calculates (n1*65536)+n2 - this is an abstraction for put two binary numbers of 16 bits side-by-side.

I was quite surprised because coq nat definition appears to handle big ints from outside, thanks to the S constructor.

How should I avoid this warning/use big numbers in coq? I'm open to change the implementation from nat to some kind of binary construction.

Thanks!

Cabezon

Working with nats is crufty, because they're built with S, meaning every number will literally be a sequence of S applications: you might work with integers instead, which have similar proof principles but have a sign / magnitude (bit) based representation: coq.inria.fr/library/Coq.ZArith.BinInt.html – Scalene

How can I use the operations then? (Zpos 1) + (Zpos 2) don't seems to work... - Error: The term "1%Z" has type "|" while it is expected to have type "nat". – Cabezon

that's because "+" means multiple things depending on where you are. In reality "+" is just syntactic sugar for adding nats, where plus is defined struturally on two nats. You want to use the plus for integers, which lives in a different interpretation scope than for nat (namely, Int_scope). Read about interpretation scopes and how to open them and use them. – Scalene

Thanks, I was fighting against scopes and this worked just fine. One last question: I Made it work with Z_scope instead of Int_scope. Is that ok? (Please, answer in order to me select your answer) – Cabezon

Answer 1

Instead of using the nat type in Coq, it's sometimes (when you have to manipulate big numbers) better to use the Z type, which is a formalization of integers using a sign magnitude pair representation. The tradeoff is that your proofs might get slightly more complex; nat is very simple, and so admits simple proof principles.

However, in Coq there's an extensive use of notation to make it simpler to write definitions, theorems, and proofs. Coq has an extremely small kernel (we want this because we want to be able to believe the proof checker is correct, and we can read that) with a lot of notation on top of it. However, as there are different representations of things, and only a few good symbols, our symbols typically clash. To get past this, coq uses interpretation scopes to disambiguate symbols, and resolve them into names (because "+" means add, plus, etc...).

You are correct, using Z_scope is where, + for plus within Z.

Scalene