agda
Real numbers, based on Cauchy sequences
Very much work-in-progress
From previous attempts, multiplication of real numbers will be the stalling point. But the HoTT book suggests this can be implemented in terms of addition, subtraction, and multiplication by a rational, which are all achievable, and squaring, which I don't know about.
I've written this on every channel concerned with constructive formalisations of the reals, but for the sake of clarity, I'll repeat myself here: please please please do NOT base the representation of ℝ on Cauchy sequences, because the rates of convergence (be it by 1/n convergence, or by 1/2^n...) are so bad, and so much pointless arithmetic is involved, but instead use the development in Russell O' Connor's PhD thesis (which we have had for 15+ years already...) in terms of the monad for metric space completion, based on functions from ε ∈ ℚ⁺ to ℚ representing nested decreasing ε-balls around a point... (IIRC; but it's all very clear in Russell's thesis, Coq or no Coq...)
The opportunity when passing from 'classical'/'orthodox' constructions in mathematics to ones 'better adapted' to the activity for formalisation, is one of the outstanding research challenges for our field, and a much-neglected one. We can (and should!!!) do better!
@jamesmckinna I'm reading Russel O'Connor's construction now. I haven't fully understood it yet, but I will note: I'm not using a fixed rate of convergence, so I don't think I have the rate of convergence issues you mention. For example, real number expressions involving only rational numbers so far converge immediately.
To press on my point: I think it's much more natural (Occam's Razor) to consider (regular) functions rather than streams for encoding the basic data underlying the 'Cauchy' property... and, given that stdlib does not commit to using HoTT-like quotients based on HI(I)Ts, in favour of a (legacy/historical, but still, ontologically less committed/more neutral) choice based on setoids, I don't see any especial need to mutually define distance-related concepts with the metric completion functor. But other opinions/design decisions are available!
This has stalled while I've been going on a sidequest to implement O'Connor-style reals. It's a lot more up-front work, but it does seem like it's going to win some advantages:
- It avoids going via a stream of rationals, skipping the potentially long indexing step and avoiding needing
--guardedness - A lot of the work implementing operators is done "up front", making the actual operations a lot easier
Both in this branch and my branch implementing the O'Connor reals (not currently online), I'm using Data.Rational.Solver a lot. This would be a little nicer perhaps if #1879 had been done, and if we were more willing to use these solvers within stdlib itself. It would also be very nice to have an inequality solver for rationals, but I have no idea how one could go about implementing that. Alternatively, I could put a bit of effort into factoring out common lemmas (mostly relating to ½ * x + ½ * x ≡ x) which might be enough to make this a lot less tedious.
Another thing that would be useful would be a type of strictly positive rationals, for example:
record ℚ⁺ : Set where
constructor 𝕢⁺
field
unℚ⁺ : ℚ
instance .{{unℚ⁺-pos}} : Positive unℚ⁺
(see also #1118). This looks like Data.Refinement, but it's not because of the instance-iness.
O'Connor defines metric spaces in terms of balls rather than distance functions, which allows him to define "real" metrics prior to having real numbers. Most of the challenge has been defining completion as a (strong!) monad on the category of these metric spaces and universally continuous functions.
Very interesting! Thanks for the update regarding "O'Connor Reals" (he'd probably say they they were Bishop/Bridges/Richman...?), and while I'm sorry for holding things up, I'm not actually sorry ;-)
As for deciding inequalities between rationals, this is a classic in the Automated Reasoning literature, via Shostak's algorithm for combining decision procedures, but may be tackled directly via the decidability (via quantifier elimination) of (the theory of) Dense Linear Order... of which the Rationals are the unique up-to countable model. (I added the proofs for density a while back...)
Definitely agree that we should tackle solvers for this and other similar theories, but I haven't quite got my head round the Reflection machinery yet...
@Taneb writes:
Another thing that would be useful would be a type of strictly positive rationals, for example:
record ℚ⁺ : Set where constructor 𝕢⁺ field unℚ⁺ : ℚ instance .{{unℚ⁺-pos}} : Positive unℚ⁺(see also #1118). This looks like
Data.Refinement, but it's not because of the instance-iness.
I'm confused... I though that the {{...}} bracketing would already mark the unℚ⁺-pos field as an instance, and available for proof search? What's the difference between your definition and eg.
record ℚ⁺ : Set where
constructor 𝕢⁺
field
unℚ⁺ : ℚ
.{{unℚ⁺-pos}} : Positive unℚ⁺
As for constructor/field names, my (ongoing; following PhIl Wadler) preference might be for 'minimum-ink' solutions, such as a postfix constructor _⁺ (or else as a pattern synonym taking explicit instance argument {{_}}?) and, whatever the actual field name chosen for the underlying value (though value springs to mind, echoing Data.Refinement... though I'd be inclined to keep it private?), a postfix synonym _⁻ to strip off the _⁺... but perhaps that might cause too much eye/mind strain? And pos would seem canonical for the associated irrelevant instance name?
Thanks @jamesmckinna , I've taken those suggestions into account. I'd been over-cautious with the instance declaration, and assumed I was right when Agda didn't complain about the redundant keyword
I'd appreciate the help! I've been alternatingly ill, busy, and distracted for a little while. I'll message you on Zulip about this later.
@Taneb I think there's already an implementation of O'Connor style reals out there here:
https://github.com/bobatkey/agda-metric-reals
We should check with @bobatkey, but I think he'd be happy to have them form the basis of something added here?
@MatthewDaggitt while that looks interesting, it doesn't seem to contain a full definition of real numbers, and isn't using O'Connor style reals (so far).
Ah sorry, my bad to you and @bobatkey! I have to confess I'm not too across the differences in the different formalisations and when I read the citations at the bottom, I assumed it was the same formalisation.
The merge conflict now reported is strange (and irritating! git can't do better?), so I wonder if, in the interests of making incremental progress, that the Data.Rational commits be split out as a smaller, simpler PR... or even two?
- one for the
nonPos/nonNeginstance arithmetic - another for the distance metric function, esp. modulo @JacquesCarette 's comment about
No idea on how to name this properly in
Data.Rational.Base. But I was surprised that it is ℚ-valued - do we not have non-negative rationals as a type? That way this would be nonNegative by construction instead of requiring a proof.
Each of those would seem a useful contribution in and of themselves as 'infrastructure'...? (as well as making the reviewing task more manageable?)
I already pulled the nonPos/nonNeg etc instance arithmetic out into PR #2496, it has since been merged, but I never updated this branch. Getting the distance metric function in would be great though.
@MatthewDaggitt while that looks interesting, it doesn't seem to contain a full definition of real numbers, and isn't using O'Connor style reals (so far).
Not everything is finished (esp multiplication) but my development does include a definition of the reals using O'Connor's definition (and the upper-semi-continuous reals):
- There is a definition of Upper Semi-continuous reals, which turns O'Connor's definitions using balls into a more standard looking pseudometric space definition.
- The completion monad is defined on pseudometric spaces, using regular functions.
- The Cauchy Reals are the completion of the rationals as a metric space.
- Addition and negation are defined, with the expected laws. Bounded multiplication is done, but unrestricted multiplication is unfinished because I never worked out how to incorporate the scaling properly. My memory is misty, but I think O'Connor does everything using uniformly continuous functions, and I'm using non-expansive functions, which made things a bit harder.
I do mean to go back and finish this, but the first thing I want to do is tidy up the Data.Real.UpperClosed to do proper Dedekind reals (with variations) before the reals as a metric space completion.
I'd appreciate the help! I've been alternatingly ill, busy, and distracted for a little while. I'll message you on Zulip about this later.
Sorry not have looped back to this before now. Happy to contribute, but it would be good to start form a clean PR, rebased against #2496 before looking at the diffs with @bobatkey 's incomplete development?
This progress on the Reals is exciting to see. I've been noodling on Reals via the so-called Eudoxus construction here: https://git.sr.ht/~bradleysaul/eudoxus. I'm not nearly as far along in terms of theorems about the Reals as this PR, but I thought I'd share for comparison's sake.
I see there's been quite a bit of progress since the last discussion happened. Perhaps @Taneb can give us an 'in words' status update?
