Real numbers, based on Cauchy sequences #2487
Conversation
| d-indiscernable {p} {q} ∣p-q∣≡0 = begin | ||
| p ≡˘⟨ +-identityʳ p ⟩ | ||
| p - 0ℚ ≡˘⟨ cong (_-_ p) (∣p∣≡0⇒p≡0 (p - q) ∣p-q∣≡0) ⟩ | ||
| p - (p - q) ≡⟨ cong (_+_ p) (neg-distrib-+ p (- q)) ⟩ |
There was a problem hiding this comment.
It feels like p - (p - q) ≡ q should be a lemma in GroupProperties?
There was a problem hiding this comment.
It actually requires commutativity! (this is hidden in neg-distrib-+). As far as I can tell it doesn't exist yet.
There was a problem hiding this comment.
The following proof looks commutativity-free to me?
p - (p - q) = p + - (p + - q) = p + (-p + q) = (p + -p) + q = 0# + q = q
There was a problem hiding this comment.
The step - (p + - q) = - p + q requires commutativity
There was a problem hiding this comment.
Oh whoops. Yes, you don't get distributivity for free.
There was a problem hiding this comment.
See Algebra.Properties.AbelianGroup.⁻¹-anti-homo‿- added in #2349 ?
|
|
||
| private | ||
| d : ℚ → ℚ → ℚ | ||
| d p q = ∣ p - q ∣ |
There was a problem hiding this comment.
This is really very frustrating. Anyone have any nice ideas how we can make this a function in Data.Rational.Base? I guess we could use some weird unicode bars?
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
See my global comment: we should have ℚ⁺ as a first class thing in the library before we proceed!
There was a problem hiding this comment.
Re: notation. UPDATED since I learnt how to write the symbols ;-)
It is a norm, so does using the following offer any assistance?
| d p q = ∣ p - q ∣ | |
| -- distance function | |
| ∥_─_∥ : ℚ → ℚ → ℚ | |
| ∥ p ─ q ∥ = ∣ p - q ∣ |
which reuses the 'long minus' \ - - - (used in Data.List.Relation.Unary.Any so hopefully the two uses won't be in scope at the same time...), and whose "weird Unicode bars" here are in fact simply given by \ | |... so they aren't too bad, either...
| open import Relation.Binary | ||
| open import Relation.Binary.PropositionalEquality using (cong₂) | ||
|
|
||
| record CauchySequence : Set a where |
There was a problem hiding this comment.
So I think this and the equality definition needs to be defined over a DistanceFunction rather than a full Metric with laws. Otherwise we're forced to define completeness over the whole metric space bundle, and we try and avoid defining predicates over bundles like that in the library.
There was a problem hiding this comment.
The added advantage of this, is that we could definite the notion of Cauchy sequence generically, rather than just for Rational.
There was a problem hiding this comment.
This record would also benefit from a constructor I think? Which would allow us to avoid writing sequence x and sequence y everywhere and instead write x and y?
There was a problem hiding this comment.
Hmm. I want to make isCauchy irrelevant. Would both doing that and introducing a constructor run into Irrelevant Projections stuff?
There was a problem hiding this comment.
Well we use a record constructor with irrelevant fields in Data.Rational.Base and I'm not aware we've run into any problems there...
There was a problem hiding this comment.
See also Data.Refinement for an already-'officially-sanctioned' stdlib approach to such matters...
There was a problem hiding this comment.
As for irrelevant projections, the discussion on agda/agda#7063 , upstream from #2199 (and others label:irrelevance/label:irrelevant-projections) suggest... (probably) not?
This makes it easier to supply either explicitly
| ε : A | ||
|
|
||
| assoc : Associative _≈_ _∙_ → Associative (Pointwise _≈_) (Stream.zipWith _∙_) | ||
| head (assoc assoc₁ xs ys zs) = assoc₁ (head xs) (head ys) (head zs) |
There was a problem hiding this comment.
Here (and for all the newly added bits): assoc assoc₁ is super ugly. One of the two should be renamed.
|
|
||
| private | ||
| d : ℚ → ℚ → ℚ | ||
| d p q = ∣ p - q ∣ |
There was a problem hiding this comment.
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.
| d-triangle p q r = begin | ||
| ∣ p - r ∣ ≡⟨ cong (λ # → ∣ # - r ∣) (+-identityʳ p) ⟨ | ||
| ∣ p + 0ℚ - r ∣ ≡⟨ cong (λ # → ∣ p + # - r ∣) (+-inverseˡ q) ⟨ | ||
| ∣ p + (- q + q) - r ∣ ≡⟨ cong (λ # → ∣ # - r ∣) (+-assoc p (- q) q) ⟨ |
There was a problem hiding this comment.
Isn't this 'middle4' for semigroup? (i.e. all these +-assoc moves).
| (lookup-zipWith m ℚ._+_ (sequence x) (sequence y)) | ||
| (lookup-zipWith n ℚ._+_ (sequence x) (sequence y)) | ||
| ⟩ | ||
| ∣ (lookup (sequence x) m ℚ.+ lookup (sequence y) m) - (lookup (sequence x) n ℚ.+ lookup (sequence y) n) ∣ |
There was a problem hiding this comment.
Looks like some notation for lookup (sequence x) m would make all of this way more readable.
| open ≤-Reasoning | ||
| instance _ : Positive (½ * ε) | ||
| _ = pos*pos⇒pos ½ ε | ||
| [x] = isCauchy x (½ * ε) |
There was a problem hiding this comment.
you name isCauchy but only use its first component -- maybe name that instead, to save all the projections above?
There was a problem hiding this comment.
I do use the second component, on lines 50 and 54. But I use the first component a lot more
| lemma = solve 4 (λ a b c d → ((a :+ b) :- (c :+ d)) , ((a :- c) :+ (b :- d))) refl | ||
| where open +-*-Solver | ||
|
|
||
| +-assoc : Associative _+_ |
There was a problem hiding this comment.
all the next properties seem to be lifting properties, i.e. if some binary operation + has property P then its lift to streams will have the same property.
|
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 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 |
|
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:
Both in this branch and my branch implementing the O'Connor reals (not currently online), I'm using 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 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 |
|
@Taneb writes:
I'm confused... I though that the 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 |
|
Thanks @jamesmckinna , I've taken those suggestions into account. I'd been over-cautious with the |
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.