Compute 121393+121393 causes stack overflow

Using Coq
1

Hello!
I tried to test this line of code in CoqIDE, but got a confusing error.

Compute 121393+121393.

To avoid stack overflow, large numbers in nat
are interpreted as applications of
Nat.of_num_uint.
[abstract-large-number,numbers]
To avoid stack overflow, large numbers in nat
are interpreted as applications of
Nat.of_num_uint.
[abstract-large-number,numbers]
Stack overflow.

It seems like a bug, or maybe I do something wrong.

I do a search for this problem, there are no useful results,
a related topic I found is coq github issue 5485,
but it should be fixed;
I could not figure out why this expression would be a large number.

Any helps will be appreciated.

2

A search in the manual yields Syntax extensions and notation scopes — Coq 8.16.1 documentation

3

Hi,

natural numbers in Coq are represented as unary number.
So 121393 is represented as the application of
121393 successors. This is too big for Coq. The error message just tells you that it has parsed 121393 but manipulating such big terms may lead to Stack overfflow.
You can be lucky and not have one. For example,

Compute 0 * 121393.

If you want compute with such big numbers my advice is to use binary numbers.

Require Import ZArith.
Compute (121393 * 121393)%Z.
4

Thanks for your answer, it does works.
Well, it is surprising to me, since there are other words about the range of natural, in Coq 8.16.1 manual 2.1.1 lexical convention:

integer and natural are limited to the range that fits into an OCaml integer (63-bit integers on most archi-
tectures). bigint and bignat have no range limitation.

If using ZArith just works,why it is not the default one, and what are the differences between them? Should I always avoid to use nat?

5

There is a lack of documents about when a nat or a bignat is over range.
and the link point out that

returns (qualidparse m) when parsing a literal m that’s greater than bignat rather than reducing it to a normal form.

I feel puzzled, if as the manuals saying, and we notice that 121393*2 is less than 2^20, then the range of bignat may so small that it can not well suit for any real-world cases.

6

nat and Z are not built-in in Coq. They are defined objects. If you look at the definition of nat, the nice thing about it is that the derived induction principle is exactly the induction you are used to.


Print nat.
(* Inductive nat : Set :=  O : nat | S : nat -> nat. *)
Check nat_ind.
(* 
  forall P : nat -> Prop,
       P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n
*)

For Z it is a bit more intricate


Require Import ZArith.

Print Z.
(* Inductive Z : Set :=  Z0 : Z | Zpos : positive -> Z | Zneg : positive -> Z. *)
Check Z_ind.
(*
Z_ind
	 : forall P : Z -> Prop,
       P 0%Z ->
       (forall p : positive, P (Z.pos p)) ->
       (forall p : positive, P (Z.neg p)) -> forall z : Z, P z
*)
7

Z is a type suitable for (moderate) computations but it is awful for proofs. On the contrary, nat is a type suitable for proofs but it is awful for computations. Since Coq is originally a proof assistant, nat is the default interpretation.

8

Yes,that is right. I found nat is much simpler than Z, e.g. , I found no simple ways to destruct a value of Z, and maybe I lost the big picture of the COQ, nevertheless, I would like to read more tutorials before making any wheels by my own.

In fact, there is a long story: I tried to write a silly recursive function to compute fibonacci numbers, then it took me some hours before I recognized that computation of plus would cause stack overflow.

Well, I believe that COQ is a great and powerful tool, however, there are many things about COQ I have to learn, and I will try my best; I expect that one day I could understand the whole reference manual of COQ.

9

We could do better in the doc. Please see Explain stack overflow for nat, number examples

there are many things about COQ I have to learn, and I will try my best; I expect that one day I could understand the whole reference manual of COQ.

A fine goal, however, alas, not everything in the manual is clearly and accurately explained, nor does it cover everything it should. I’ve been working on improving it for a while. If you identify weak points in Github or here in Discourse, I will look at them. The more specific you can be, the sooner it is likely to be addressed.

1 Like