How to Efficiently Define the Natural Numbers in Type Theory

Question

A while ago I wondered about how Proof Assistants like Coq prove $m \leq n$ and the like. It looks like they actually need to traverse the natural numbers based on the successor/predecessor formulation:

Coq < Eval compute in le_lt_dec 100000 1000000. 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). Stack overflow.

One of the answers suggested using the BinInt (Binary Integers representation) to perform this operation.

When a mathematician looks at a claim like $1000 ≤ 1000000$ and says "obviously", they are taking advantage of the fact that we wrote the claim in decimal notation. If you want to do something similar in CoQ, you could try to prove, e.g., $10∗10∗10≤10∗10∗10∗10∗10$.

So I'm wondering if there is a standard way of representing numbers as types without defining them like Peano's axioms style, using successor/predecessor and the like. Something that allows you to prove two numbers have a relation such as $m \leq n$ or $m \neq n$ or do other common things with numbers like adding/subtracting, in such a way where the "formal definition" (i.e. succ/pred) of the numbers is combined with some more computationally optimal version so you can use it in practice. Not sure what best-practice is to do here, but I would like to define a numbers type and have it gain all the advantages of proof theory / proof assistants, while also being the actual type definition used to construct i.e. integers.

Answer 1

There's nothing stopping you from defining binary numbers in type theory, and this should give greater efficiency in practice.

For example:

https://coq.inria.fr/library/Coq.Numbers.BinNums.html

EDIT: Why not base 10?

Comparison on binary numbers can be done in $O(\log_2 n))$ time. If you have base 10, you can do it in $O(\log_{10} n)$ time. But if we apply the change of base formula, $O(\log_{10} n) = O(\log_{2} n / \log_{2} 10) = O(\log_2 n)$, since $O(\log_2 10)$ is constant.

There's a speed tradeoff. You get constant speedup for some operations, but you get constant slowdown for others. For example, each pattern match now has 11 options instead of 3. So, given that they have the same asymptotic behavior, we usually go with the simplest one.

Finally, the advantage with base 2 is that, if you limit yourself to 32 or 64 bits, you can represent them using machine integers, for example, if you extract your Coq code to OCaml, which means you can get very fast extracted code.