Integer operations using built-ins

[hexwell]

The implementations of the operations over the integers of sum, multiplication and also untrucated subtraction of two naturals (_ℕ-_ : ℕ → ℕ → ℤ) currently present in the library take a long time to normalize when trying to calculate results with big operands.

This is likely the case because they are implemented recursively, instead of relying on linking them to builtin operations via a pragma.

To achieve better performances, our proposed implementation defines the multiplication using signs and (fast) multiplication over the naturals, for example.
(Currently pattern matching, but we plan to switch to the same approach as the std-lib (using a sign datatype) very soon)
There can also be a discussion about the what the std-lib does for _ℕ-_ (there named _⊖_, and defined with with-abstraction and without a helper) and _·_, and if it's advantageous to do the same here.

This new approach is due to @marcinjangrzybowski, and follows the standard library agda/agda-stdlib#1303.

Here is a gist where we tried some simple calculations with both implementations of the operations and report the results:

• CurrentAddition vs FastAddition
• CurrentMultiplication vs FastMultiplication
• our results

In the same gist, there is also a file with a proof of concept showing the computation of the digits of Euler's number.

In fact, a motivation for this work is to enable performant computation of real numbers, as defined in draft PR #1182.

This draft PR contains the bare minimum required for the examples to work, but we have more work in progress (e.g. properties) in this branch.

A lot of the code there is very similar to the current one, but instead of introducing a common abstraction to avoid this repetition we decided to rewrite everything from scratch, because if this implementation is accepted as the default one, then we find this approach cleaner in the long term.

With this goal in mind, it is also necessary that users of the integer operations in question do not rely directly on the structure of the implementation, and instead only use the abstract properties exported from Properties.agda, etc.

Indeed, we tried to export the new operations as the default in place of the current ones already, and found some incompatible code (for example in the Homotopy folder).
We spent considerable time trying to refactor existing code to make it work but it's too large of an endeavour, and hence the decision to separate the new implementation from the current one instead of replacing it.

Notes

• In Agda, there already are builtin helper operations for division and modulo. These are currently not used, not even for the naturals. It might be good to write an optimized implementation of division and modulo using them. An example of this can be found in the previously linked gist. We already tried to reimplement them and the needed properties to obtain faster code in Int/Fast/Divisibility, as can be seen in this branch.

• We are thinking about a faster implementation of min/max (over the integers and the naturals) before proving their properties.
  We were planning to adapt the alternative definitions of min and max (_⊓′_ and _⊔′_) present in the standard library.
  Here we tested the performances of the alternative definition.

• The new file is currently in the folder Int/Fast. There was already the MoreInts folder in the library, but we didn't put it there, because our code does not redefine the integers datatype, it just redefines the operations.
  We are looking for a better place to move this, if you have one in mind.

We are open to other suggestions and discussion.

[felixwellen]

It makes sense to me to have this fast version of the integers, even if it will not be possible to use it everywhere -> merging.