search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
446 stars 136 forks source link

Rational order #1071

Closed LuuBluum closed 9 months ago

LuuBluum commented 10 months ago

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 commented 9 months ago

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 commented 9 months ago

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

felixwellen commented 9 months ago

Please rebase/merge master

mortberg commented 9 months ago

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

MatthiasHu commented 1 month ago

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

LuuBluum commented 1 month ago

@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.