Rational order

[LuuBluum]

Defines an ordering over the rationals and proves several key properties. Also refactors the rationals to use the integers instead of QuoInt; the original definition are relabeled as QuoQ and put into MoreRationals.

At some point, ideally under a different PR, QuoQ should be removed and all proofs involving it replaced with proofs against the variant using the default version of Int rather than QuoInt.

[mortberg]

Thanks, lots of good stuff in this PR!

A general question, can't the ring solver be used to prove a lot of the equations for Z that are needed in the proofs?

[mortberg]

Don't have this for nat and int already? Should be upstreamed

[LuuBluum]

We do, but the issue here is that it only works for [ a , b ] [ c , d ] cases. Upstreaming it would require a gnarly pattern match like the definition of < or <=.

[mortberg]

Can someone who knows how the CI really works help with fixing:

agda: Heap exhausted;
agda: Current maximum heap size is 3758096384 bytes (3584 MB).
agda: Use `+RTS -M<size>' to increase it.
make: *** [GNUmakefile:53: check] Error 251
Error: Process completed with exit code 2.

Maybe @felixwellen or @mzeuner ?

[LuuBluum]

The heap issue seems to be happening on master as well, so it's a broader issue with the library.

[felixwellen]

Please rebase/merge master

[mortberg]

Thanks for this! Looking forward to future PRs cleaning things even more

[MatthiasHu]

@LuuBluum Could you explain the motivation for 1bc03c7 ? The previous definition of rec2 was shorter and seems more readable and elegant to me.

[LuuBluum]

@LuuBluum Could you explain the motivation for 1bc03c7 ? The previous definition of rec2 was shorter and seems more readable and elegant to me.

Pattern matching. Defining rec2 recursively (as it was before) results in significant slowdown on usage due to needing to carry over the proof of transitivity over the quotient relation every time you invoke it, particularly with things that don't care about that proof at all.

For context, under the previous definition of rec2, if I were to define the operations on the rational numbers that way, you would never be able to use them because they could never compute. It was just prohibitively slow. This was the only way to actually define the rationals as a set quotient so that it could actually be used.