The Coq mailing list

[Xavier Leroy <Xavier.Leroy AT inria.fr>]

Le 20/12/2020 à 19:10, jonikelee AT gmail.com a écrit :
> What is the best performing way to use large numbers in Gallina?  I am
> getting the following warning, which seems to imply I could have done
> something better with this definition:
>
> Definition fuel : nat := 10000.
>
> Warning: To avoid stack overflow, large numbers in nat are interpreted
> as applications of Nat.of_num_uint. [abstract-large-number,numbers]
> fuel is defined

The types N and Z from the standard library (modules NArith, ZArith) are exponentially more efficient than type nat, as N and Z use a base-2 representation internally.

Using N instead of nat in your code is usually easy.  The tricky part is Peano-style recursion, which is a Fixpoint+pattern-matching in the case of nat and a library function in the case of N:

Fixpoint foo (n: nat) := match n with O => base | S m => f n (foo m) end

becomes

Definition foo (n: N) := N.recursion base f n.

Alternatively, you can use well-founded induction over N.

For additional performance, there is also the "Numbers" library, using a base-2^N representation, but it has so little documentation that I don't know how to use it.

On Mon, Dec 21, 2020 at 8:10 AM Guillaume Melquiond <guillaume.melquiond AT inria.fr> wrote:

 

Before trying to represent large numbers (e.g., using Z.to_nat), you
should first reconsider whether you actually need such large numbers.

Indeed, even to ensure termination, this is mightily inefficient.
Consider the following function as an example:

Fixpoint foo (n:nat) x :=
  match n with
  | S n => foo n (foo n x)
  | O => bar x
  end.

With n = 64, it will already run past the end of the solar system.

So, if you need more fuel than that, it presumably means that your
function was not properly written.

This is a nice trick when it applies, i.e. not that often in my experience.  It's not a proper answer to the question "What is the best performing way to use large numbers in Gallina?".

 

Kind regards,

- Xavier Leroy

Best regards,

Guillaume