The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond 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

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.

Best regards,

Guillaume