Implement version of Data.Nat.Binary.fromℕ that runs in O(log n)

[Taneb]

This makes the dependency footprint of this module a fair bit heavier I'm afraid.

I'll add a changelog entry after the 1.5 release to avoid rebasing difficulties.

I tested this with a little program that prints 10000000 round-tripped through ℕᵇ. With the old one, this took 1.5s, with the new version 0.002s.

[oisdk]

Instead of using well-founded recursion, you can use the number itself to prove termination. I have found this to be much quicker in practice. (and it doesn't require as many dependencies)

I also have proofs that the fast version is the same as the slow, if that is of any help: https://oisdk.github.io/agda-playground/Data.Binary.Conversion.Fast.Properties.html

[MatthewDaggitt]

@Taneb thanks for the PR! You'll also need to update all the relevant proofs as well which may prove to be a bit harder given the increase in complexity. @oisdk's version does look a lot neater with less dependencies and the former might be a significant advantage when it comes to proving properties about it...

[Taneb]

I'm not a huge fan of @oisdk's version, but if I'm being honest with myself, about 70% of that is "I didn't come up with it".
The remaining 30% is that it makes me sad there's an auxiliary variable to prove termination, that doesn't actually match what it means for the function to terminate, and also that I wanted to learn how to use the Induction machinery.
I accept that these don't add up to anything near a reason not to use it, but I still want to try to prove the properties of this form, as a learning exercise if nothing else.

[MatthewDaggitt]

I accept that these don't add up to anything near a reason not to use it, but I still want to try to prove the properties of this form, as a learning exercise if nothing else.

Definitely an admirable goal! Though fair warning I suspect it's going to pretty messy 😄

We probably want the best code in the standard library though so just a heads up that if you continue with this definition, I probably won't merge the results in! Not a problem of course, but I thought I should give you an explicit heads up 👍

[MatthewDaggitt]

Okay, closing this PR. However, I've opened an issue #1468 to keep track of the problem.