Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Book cauchy reals #1182

Draft
wants to merge 10 commits into
base: master
Choose a base branch
from

Conversation

marcinjangrzybowski
Copy link
Contributor

@marcinjangrzybowski marcinjangrzybowski commented Jan 22, 2025

This is an implementation of real numbers as defined in Chapter 11.3: Cauchy Reals of the HoTT Book.
(Note: results 11.3.11 and 11.3.50 are currently missing.)

Modules:

  • Cubical/HITs/CauchyReals/Base.agda
  • Cubical/HITs/CauchyReals/Closeness.agda
  • Cubical/HITs/CauchyReals/Continuous.agda
  • Cubical/HITs/CauchyReals/Inverse.agda
  • Cubical/HITs/CauchyReals/Lems.agda
  • Cubical/HITs/CauchyReals/Lipschitz.agda
  • Cubical/HITs/CauchyReals/Multiplication.agda
  • Cubical/HITs/CauchyReals/Order.agda

These modules closely follow the book. However, I had to adjust the order of definitions due to the issue discussed here: HoTT/book#899.

Additionally, the following modules:

  • Cubical/HITs/CauchyReals/Sequence.agda
  • Cubical/HITs/CauchyReals/Derivative.agda

are attempts to benchmark the definitions and evaluate their behavior. In Derivative.agda, I've managed to derive the Power rule (for natural exponents). In Sequence.agda, I defined exp (currently only for ℚ₊), allowing the definition of e.

To implement these properly (assuming we want to continue without countable choice or LEM), I plan to consult some books on constructive analysis. The HoTT Book references "Errett Bishop. Foundations of Constructive Analysis," but I welcome other suggestions.

While the development is not yet up to library standards, everything currently type checks. I will likely split this into smaller PRs. There is one remaining definition, invℝ, hidden behind abstract. However, I have a promising idea based on previous optimizations to expose it (or at least manage its evaluation more controllably by guarding it with lockUnit).

There is some redundancy, as I am still experimenting with different versions of definitions.

TODO:

  • Implement square root
  • Implement chain rule
  • Complete results 11.3.11 and 11.3.50 from the HoTT Book
  • Extend exp to all reals and provide a characterization
  • Properly generalize convergence tests and add a few more
  • Define logarithm
  • Parameterize definitions by implementation of Rationals
  • Figure out a more elegant way to employ CommRingSolver (temporary solution in Cubical/HITs/CauchyReals/Lems.agda)

@felixwellen
Copy link
Collaborator

Congrats! This is great :-)
Why don't you use opaque instead of abstract?

@marcinjangrzybowski
Copy link
Contributor Author

I did not saw opaque utilised too much thru the library, did not considered it really :), will do now thanks!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants