Real numbers, based on Cauchy sequences

src/Codata/Guarded/Stream/Relation/Binary/Pointwise.agda

@@ -12,7 +12,7 @@ open import Codata.Guarded.Stream as Stream using (Stream; head; tail)
 open import Data.Nat.Base using (ℕ; zero; suc)
 open import Function.Base using (_∘_; _on_)
 open import Level using (Level; _⊔_)
-open import Relation.Binary.Core using (REL; _⇒_)
+open import Relation.Binary.Core using (REL; Rel; _⇒_)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Definitions
   using (Reflexive; Sym; Trans; Antisym; Symmetric; Transitive)
@@ -104,6 +104,43 @@ drop⁺ : ∀ n → Pointwise R ⇒ (Pointwise R on Stream.drop n)
 drop⁺ zero    as≈bs = as≈bs
 drop⁺ (suc n) as≈bs = drop⁺ n (as≈bs .tail)
 
+------------------------------------------------------------------------
+-- Algebraic properties
+
+module _ {A : Set a} {_≈_ : Rel A ℓ} where
+
+  open import Algebra.Definitions
+
+  private
+    variable
+      _∙_ : A → A → A
+      _⁻¹ : A → A
+      ε : A
+
+  assoc : Associative _≈_ _∙_ → Associative (Pointwise _≈_) (Stream.zipWith _∙_)
+  head (assoc assoc₁ xs ys zs) = assoc₁ (head xs) (head ys) (head zs)
+  tail (assoc assoc₁ xs ys zs) = assoc assoc₁ (tail xs) (tail ys) (tail zs)
+
+  comm : Commutative _≈_ _∙_ → Commutative (Pointwise _≈_) (Stream.zipWith _∙_)
+  head (comm comm₁ xs ys) = comm₁ (head xs) (head ys)
+  tail (comm comm₁ xs ys) = comm comm₁ (tail xs) (tail ys)
+
+  identityˡ : LeftIdentity _≈_ ε _∙_ → LeftIdentity (Pointwise _≈_) (Stream.repeat ε) (Stream.zipWith _∙_)
+  head (identityˡ identityˡ₁ xs) = identityˡ₁ (head xs)
+  tail (identityˡ identityˡ₁ xs) = identityˡ identityˡ₁ (tail xs)
+
+  identityʳ : RightIdentity _≈_ ε _∙_ → RightIdentity (Pointwise _≈_) (Stream.repeat ε) (Stream.zipWith _∙_)
+  head (identityʳ identityʳ₁ xs) = identityʳ₁ (head xs)
+  tail (identityʳ identityʳ₁ xs) = identityʳ identityʳ₁ (tail xs)
+
+  inverseˡ : LeftInverse _≈_ ε _⁻¹ _∙_ → LeftInverse (Pointwise _≈_) (Stream.repeat ε) (Stream.map _⁻¹) (Stream.zipWith _∙_)
+  head (inverseˡ inverseˡ₁ xs) = inverseˡ₁ (head xs)
+  tail (inverseˡ inverseˡ₁ xs) = inverseˡ inverseˡ₁ (tail xs)
+
+  inverseʳ : RightInverse _≈_ ε _⁻¹ _∙_ → RightInverse (Pointwise _≈_) (Stream.repeat ε) (Stream.map _⁻¹) (Stream.zipWith _∙_)
+  head (inverseʳ inverseʳ₁ xs) = inverseʳ₁ (head xs)
+  tail (inverseʳ inverseʳ₁ xs) = inverseʳ inverseʳ₁ (tail xs)
+
 ------------------------------------------------------------------------
 -- Pointwise Equality as a Bisimilarity
 

src/Data/Rational/Properties.agda

@@ -49,6 +49,7 @@ open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_]′; _⊎_)
 import Data.Sign.Base as Sign
 open import Function.Base using (_∘_; _∘′_; _∘₂_; _$_; flip)
 open import Function.Definitions using (Injective)
+open import Function.Metric.Rational as Metric hiding (Symmetric)
 open import Level using (0ℓ)
 open import Relation.Binary
 open import Relation.Binary.Morphism.Structures
@@ -1799,6 +1800,89 @@ toℚᵘ-homo-∣-∣ (mkℚ -[1+ _ ] _ _) = *≡* refl
 ∣∣p∣∣≡∣p∣ : ∀ p → ∣ ∣ p ∣ ∣ ≡ ∣ p ∣
 ∣∣p∣∣≡∣p∣ p = 0≤p⇒∣p∣≡p (0≤∣p∣ p)
 
+------------------------------------------------------------------------
+-- Metric space
+------------------------------------------------------------------------
+
+private
+  d : ℚ → ℚ → ℚ
+  d p q = ∣ p - q ∣
+
+d-cong : Congruent _≡_ d
+d-cong = cong₂ _
+
+d-nonNegative : ∀ {p q} → 0ℚ ≤ d p q
+d-nonNegative {p} {q} = nonNegative⁻¹ _ {{∣-∣-nonNeg (p - q)}}
+
+d-definite : Definite _≡_ d
+d-definite {p} refl = cong ∣_∣ (+-inverseʳ p)
+
+d-indiscernable : Indiscernable _≡_ d
+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)) ⟩
+  p + (- p - - q) ≡⟨ +-assoc p (- p) (- - q) ⟨
+  (p - p) - - q   ≡⟨ cong₂ _+_ (+-inverseʳ p) (⁻¹-involutive q) ⟩
+  0ℚ + q          ≡⟨ +-identityˡ q ⟩
+  q               ∎
+  where
+    open ≡-Reasoning
+    open GroupProperties +-0-group
+
+d-sym : Metric.Symmetric d
+d-sym p q = begin
+  ∣ p - q ∣     ≡˘⟨ ∣-p∣≡∣p∣ (p - q) ⟩
+  ∣ - (p - q) ∣ ≡⟨ cong ∣_∣ (⁻¹-anti-homo-// p q) ⟩
+  ∣ q - p ∣     ∎
+  where
+    open ≡-Reasoning
+    open GroupProperties +-0-group
+
+d-triangle : TriangleInequality d
+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) ⟨
+  ∣ ((p - q) + q) - r ∣ ≡⟨ cong ∣_∣ (+-assoc (p - q) q (- r)) ⟩
+  ∣ (p - q) + (q - r) ∣ ≤⟨ ∣p+q∣≤∣p∣+∣q∣ (p - q) (q - r) ⟩
+  ∣ p - q ∣ + ∣ q - r ∣ ∎
+  where open ≤-Reasoning
+
+d-isProtoMetric : IsProtoMetric _≡_ d
+d-isProtoMetric = record
+  { isPartialOrder = ≤-isPartialOrder
+  ; ≈-isEquivalence = isEquivalence
+  ; cong = cong₂ _
+  ; nonNegative = λ {p q} → d-nonNegative {p} {q}
+  }
+
+d-isPreMetric : IsPreMetric _≡_ d
+d-isPreMetric = record
+  { isProtoMetric = d-isProtoMetric
+  ; ≈⇒0 = d-definite
+  }
+
+d-isQuasiSemiMetric : IsQuasiSemiMetric _≡_ d
+d-isQuasiSemiMetric = record
+  { isPreMetric = d-isPreMetric
+  ; 0⇒≈ = d-indiscernable
+  }
+
+d-isSemiMetric : IsSemiMetric _≡_ d
+d-isSemiMetric = record
+  { isQuasiSemiMetric = d-isQuasiSemiMetric
+  ; sym = d-sym
+  }
+
+d-isMetric : IsMetric _≡_ d
+d-isMetric = record
+  { isSemiMetric = d-isSemiMetric
+  ; triangle = d-triangle
+  }
+
+d-metric : Metric _ _
+d-metric = record { isMetric = d-isMetric }
 
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES

src/Data/Real/Base.agda

@@ -0,0 +1,220 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Real numbers
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible --guardedness #-}
+
+module Data.Real.Base where
+
+open import Codata.Guarded.Stream
+open import Codata.Guarded.Stream.Properties
+open import Data.Integer.Base using (+<+)
+open import Data.Nat.Base as ℕ using (z≤n; s≤s)
+import Data.Nat.Properties as ℕ
+open import Data.Product.Base hiding (map)
+open import Data.Rational.Base as ℚ hiding (_+_; -_; _*_)
+open import Data.Rational.Properties
+open import Data.Rational.Solver
+open import Data.Rational.Unnormalised using (*<*)
+open import Function.Base using (_$_)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; cong₂)
+open import Relation.Nullary
+
+open import Function.Metric.Rational.CauchySequence d-metric public renaming (CauchySequence to ℝ)
+
+fromℚ : ℚ → ℝ
+fromℚ = embed
+
+0ℝ : ℝ
+0ℝ = fromℚ 0ℚ
+
+_+_ : ℝ → ℝ → ℝ
+sequence (x + y) = zipWith ℚ._+_ (sequence x) (sequence y)
+isCauchy (x + y) ε = proj₁ [x] ℕ.+ proj₁ [y] , λ {m} {n} m≥N n≥N → begin-strict
+  ∣ lookup (zipWith ℚ._+_ (sequence x) (sequence y)) m - lookup (zipWith ℚ._+_ (sequence x) (sequence y)) n ∣
+    ≡⟨ cong₂ (λ a b → ∣ a - b ∣)
+      (lookup-zipWith m ℚ._+_ (sequence x) (sequence y))
+      (lookup-zipWith n ℚ._+_ (sequence x) (sequence y))
+    ⟩
+  ∣ (lookup (sequence x) m ℚ.+ lookup (sequence y) m) - (x ‼ n ℚ.+ y ‼ n) ∣
+    ≡⟨ cong ∣_∣ (lemma (lookup (sequence x) m) (lookup (sequence y) m) (x ‼ n) (y ‼ n)) ⟩
+  ∣ (lookup (sequence x) m - x ‼ n) ℚ.+ (lookup (sequence y) m - y ‼ n) ∣
+    ≤⟨ ∣p+q∣≤∣p∣+∣q∣
+      (lookup (sequence x) m - x ‼ n)
+      (lookup (sequence y) m - y ‼ n)
+    ⟩
+  ∣ lookup (sequence x) m - x ‼ n ∣ ℚ.+ ∣ lookup (sequence y) m - y ‼ n ∣
+    <⟨ +-mono-<
+      (proj₂ [x]
+        (ℕ.≤-trans (ℕ.m≤m+n (proj₁ [x]) (proj₁ [y])) m≥N)
+        (ℕ.≤-trans (ℕ.m≤m+n (proj₁ [x]) (proj₁ [y])) n≥N)
+      )
+      (proj₂ [y]
+        (ℕ.≤-trans (ℕ.m≤n+m (proj₁ [y]) (proj₁ [x])) m≥N)
+        (ℕ.≤-trans (ℕ.m≤n+m (proj₁ [y]) (proj₁ [x])) n≥N)
+      )
+    ⟩
+  ½ ℚ.* ε ℚ.+ ½ ℚ.* ε
+    ≡⟨ *-distribʳ-+ ε ½ ½ ⟨
+  1ℚ ℚ.* ε
+    ≡⟨ *-identityˡ ε ⟩
+  ε ∎
+  where
+    open ≤-Reasoning
+    instance _ : Positive (½ ℚ.* ε)
+    _ = pos*pos⇒pos ½ ε
+    [x] = isCauchy x (½ ℚ.* ε)
+    [y] = isCauchy y (½ ℚ.* ε)
+
+    lemma : ∀ a b c d → (a ℚ.+ b) - (c ℚ.+ d) ≡ (a - c) ℚ.+ (b - d)
+    lemma = solve 4 (λ a b c d → ((a :+ b) :- (c :+ d)) , ((a :- c) :+ (b :- d))) refl
+      where open +-*-Solver
+
+-_ : ℝ → ℝ
+sequence (- x) = map ℚ.-_ (sequence x)
+isCauchy (- x) ε = proj₁ (isCauchy x ε) , λ {m} {n} m≥N n≥N → begin-strict
+  ∣ lookup (map ℚ.-_ (sequence x)) m - lookup (map ℚ.-_ (sequence x)) n ∣
+    ≡⟨ cong₂ (λ a b → ∣ a - b ∣) (lookup-map m ℚ.-_ (sequence x)) (lookup-map n ℚ.-_ (sequence x)) ⟩
+  ∣ ℚ.- lookup (sequence x) m - ℚ.- x ‼ n ∣
+    ≡⟨ cong ∣_∣ (lemma (lookup (sequence x) m) (x ‼ n)) ⟩
+  ∣ ℚ.- (lookup (sequence x) m - x ‼ n) ∣
+    ≡⟨ ∣-p∣≡∣p∣ (lookup (sequence x) m - x ‼ n) ⟩
+  ∣ lookup (sequence x) m - x ‼ n ∣
+    <⟨ proj₂ (isCauchy x ε) m≥N n≥N ⟩
+  ε ∎
+  where
+    open ≤-Reasoning
+    lemma : ∀ a b → ℚ.- a - ℚ.- b ≡ ℚ.- (a - b)
+    lemma = solve 2 (λ a b → (:- a) :- (:- b) , (:- (a :- b))) refl
+      where open +-*-Solver
+
+_*ₗ_ : ℚ → ℝ → ℝ
+sequence (p *ₗ x) = map (p ℚ.*_) (sequence x)
+isCauchy (p *ₗ x) ε with p ≟ 0ℚ
+... | yes p≡0 = 0 , λ {m} {n} _ _ → begin-strict
+  ∣ lookup (map (p ℚ.*_) (sequence x)) m - lookup (map (p ℚ.*_) (sequence x)) n ∣
+    ≡⟨ cong₂ (λ a b → ∣ a - b ∣) (lookup-map m (p ℚ.*_) (sequence x)) (lookup-map n (p ℚ.*_) (sequence x)) ⟩
+  ∣ p ℚ.* lookup (sequence x) m - p ℚ.* x ‼ n ∣
+    ≡⟨ cong (λ # → ∣ p ℚ.* lookup (sequence x) m ℚ.+ # ∣) (neg-distribʳ-* p (x ‼ n)) ⟩
+  ∣ p ℚ.* lookup (sequence x) m ℚ.+ p ℚ.* ℚ.- x ‼ n ∣
+    ≡⟨ cong ∣_∣ (*-distribˡ-+ p (lookup (sequence x) m) (ℚ.- x ‼ n)) ⟨
+  ∣ p ℚ.* (lookup (sequence x) m - x ‼ n) ∣
+    ≡⟨ cong (λ # → ∣ # ℚ.* (lookup (sequence x) m - x ‼ n) ∣) p≡0 ⟩
+  ∣ 0ℚ ℚ.* (lookup (sequence x) m - x ‼ n) ∣
+    ≡⟨ cong ∣_∣ (*-zeroˡ (lookup (sequence x) m - x ‼ n)) ⟩
+  ∣ 0ℚ ∣
+    ≡⟨⟩
+  0ℚ
+    <⟨ positive⁻¹ ε ⟩
+  ε ∎
+  where open ≤-Reasoning
+... | no  p≢0 = proj₁ (isCauchy x (1/ ∣ p ∣ ℚ.* ε)) , λ {m} {n} m≥N n≥N → begin-strict
+  ∣ lookup (map (p ℚ.*_) (sequence x)) m - lookup (map (p ℚ.*_) (sequence x)) n ∣
+    ≡⟨ cong₂ (λ a b → ∣ a - b ∣) (lookup-map m (p ℚ.*_) (sequence x)) (lookup-map n (p ℚ.*_) (sequence x)) ⟩
+  ∣ p ℚ.* lookup (sequence x) m - p ℚ.* x ‼ n ∣
+    ≡⟨ cong (λ # → ∣ p ℚ.* lookup (sequence x) m ℚ.+ # ∣) (neg-distribʳ-* p (x ‼ n)) ⟩
+  ∣ p ℚ.* lookup (sequence x) m ℚ.+ p ℚ.* ℚ.- x ‼ n ∣
+    ≡⟨ cong ∣_∣ (*-distribˡ-+ p (lookup (sequence x) m) (ℚ.- x ‼ n)) ⟨
+  ∣ p ℚ.* (lookup (sequence x) m - x ‼ n) ∣
+    ≡⟨ ∣p*q∣≡∣p∣*∣q∣ p (lookup (sequence x) m - x ‼ n) ⟩
+  ∣ p ∣ ℚ.* ∣ lookup (sequence x) m - x ‼ n ∣
+    <⟨ *-monoʳ-<-pos ∣ p ∣ (proj₂ (isCauchy x (1/ ∣ p ∣ ℚ.* ε)) m≥N n≥N) ⟩
+  ∣ p ∣ ℚ.* (1/ ∣ p ∣ ℚ.* ε)
+    ≡⟨ *-assoc ∣ p ∣ (1/ ∣ p ∣) ε ⟨
+  (∣ p ∣ ℚ.* 1/ ∣ p ∣) ℚ.* ε
+    ≡⟨ cong (ℚ._* ε) (*-inverseʳ ∣ p ∣) ⟩
+  1ℚ ℚ.* ε
+    ≡⟨ *-identityˡ ε ⟩
+  ε ∎
+  where
+    open ≤-Reasoning
+    instance _ : NonZero ∣ p ∣
+    _ = ≢-nonZero {∣ p ∣} λ ∣p∣≡0 → p≢0 (∣p∣≡0⇒p≡0 p ∣p∣≡0)
+    instance _ : Positive ∣ p ∣
+    _ = nonNeg∧nonZero⇒pos ∣ p ∣ {{∣-∣-nonNeg p}}
+    instance _ : Positive (1/ ∣ p ∣)
+    _ = 1/pos⇒pos ∣ p ∣
+    instance _ : Positive (1/ ∣ p ∣ ℚ.* ε)
+    _ = pos*pos⇒pos (1/ ∣ p ∣) ε
+
+square : ℝ → ℝ
+sequence (square x) = map (λ p → p ℚ.* p) (sequence x)
+isCauchy (square x) ε = B ℕ.⊔ proj₁ (isCauchy x (1/ (b ℚ.+ b) ℚ.* ε)) , λ {m} {n} m≥N n≥N → begin-strict
+  ∣ lookup (map (λ p → p ℚ.* p) (sequence x)) m - lookup (map (λ p → p ℚ.* p) (sequence x)) n ∣
+    ≡⟨ cong₂ (λ a b → ∣ a - b ∣) (lookup-map m _ (sequence x)) (lookup-map n _ (sequence x)) ⟩
+  ∣ lookup (sequence x) m ℚ.* lookup (sequence x) m - x ‼ n ℚ.* x ‼ n ∣
+    ≡⟨ cong ∣_∣ (lemma (lookup (sequence x) m) (x ‼ n)) ⟩
+  ∣ (lookup (sequence x) m ℚ.+ x ‼ n) ℚ.* (lookup (sequence x) m - x ‼ n) ∣
+    ≡⟨ ∣p*q∣≡∣p∣*∣q∣ (lookup (sequence x) m ℚ.+ x ‼ n) (lookup (sequence x) m - x ‼ n) ⟩
+  ∣ lookup (sequence x) m ℚ.+ x ‼ n ∣ ℚ.* ∣ lookup (sequence x) m - x ‼ n ∣
+    ≤⟨ *-monoʳ-≤-nonNeg ∣ lookup (sequence x) m - x ‼ n ∣
+      {{∣-∣-nonNeg (lookup (sequence x) m - x ‼ n)}}
+      (∣p+q∣≤∣p∣+∣q∣ (lookup (sequence x) m) (x ‼ n))
+    ⟩
+  (∣ lookup (sequence x) m ∣ ℚ.+ ∣ x ‼ n ∣) ℚ.* ∣ lookup (sequence x) m - x ‼ n ∣
+    ≤⟨ *-monoʳ-≤-nonNeg ∣ lookup (sequence x) m - x ‼ n ∣
+      {{∣-∣-nonNeg (lookup (sequence x) m - x ‼ n)}}
+      (<⇒≤ (+-mono-<
+        (b-prop (ℕ.≤-trans (ℕ.m≤m⊔n B (proj₁ (isCauchy x (1/ (b ℚ.+ b) ℚ.* ε)))) m≥N))
+        (b-prop (ℕ.≤-trans (ℕ.m≤m⊔n B (proj₁ (isCauchy x (1/ (b ℚ.+ b) ℚ.* ε)))) n≥N))
+      ))
+    ⟩
+  (b ℚ.+ b) ℚ.* ∣ lookup (sequence x) m - x ‼ n ∣
+    <⟨ *-monoʳ-<-pos (b ℚ.+ b) (proj₂ (isCauchy x (1/ (b ℚ.+ b) ℚ.* ε))
+      (ℕ.≤-trans (ℕ.m≤n⊔m B (proj₁ (isCauchy x (1/ (b ℚ.+ b) ℚ.* ε)))) m≥N)
+      (ℕ.≤-trans (ℕ.m≤n⊔m B (proj₁ (isCauchy x (1/ (b ℚ.+ b) ℚ.* ε)))) n≥N)
+    ) ⟩
+  (b ℚ.+ b) ℚ.* (1/ (b ℚ.+ b) ℚ.* ε)
+    ≡⟨ *-assoc (b ℚ.+ b) (1/ (b ℚ.+ b)) ε ⟨
+  ((b ℚ.+ b) ℚ.* 1/ (b ℚ.+ b)) ℚ.* ε
+    ≡⟨ cong (ℚ._* ε) (*-inverseʳ (b ℚ.+ b)) ⟩
+  1ℚ ℚ.* ε
+    ≡⟨ *-identityˡ ε ⟩
+  ε ∎
+  where
+    open ≤-Reasoning
+
+    B : ℕ.ℕ
+    B = proj₁ (isCauchy x 1ℚ)
+
+    b : ℚ
+    b = 1ℚ ℚ.+ ∣ lookup (sequence x) B ∣
+
+    instance _ : Positive b
+    _ = pos+nonNeg⇒pos 1ℚ ∣ lookup (sequence x) B ∣ {{∣-∣-nonNeg (lookup (sequence x) B)}}
+
+    instance _ : NonZero b
+    _ = pos⇒nonZero b
+
+    instance _ : Positive (b ℚ.+ b)
+    _ = pos+pos⇒pos b b
+
+    instance _ : NonZero (b ℚ.+ b)
+    _ = pos⇒nonZero (b ℚ.+ b)
+
+    instance _ : Positive (1/ (b ℚ.+ b) ℚ.* ε)
+    _ = pos*pos⇒pos (1/ (b ℚ.+ b)) {{1/pos⇒pos (b ℚ.+ b)}} ε
+
+    b-prop : ∀ {n} → n ℕ.≥ B → ∣ x ‼ n ∣ < b
+    b-prop {n} n≥B = begin-strict
+     ∣ x ‼ n ∣
+       ≡⟨ cong ∣_∣ (+-identityʳ (x ‼ n)) ⟨
+     ∣ x ‼ n ℚ.+ 0ℚ ∣
+       ≡⟨ cong (λ # → ∣ x ‼ n ℚ.+ # ∣) (+-inverseˡ (lookup (sequence x) B)) ⟨
+     ∣ x ‼ n ℚ.+ (ℚ.- lookup (sequence x) B ℚ.+ lookup (sequence x) B) ∣
+       ≡⟨ cong ∣_∣ (+-assoc (x ‼ n) (ℚ.- lookup (sequence x) B) (lookup (sequence x) B)) ⟨
+     ∣ (x ‼ n - lookup (sequence x) B) ℚ.+ lookup (sequence x) B ∣
+       ≤⟨ ∣p+q∣≤∣p∣+∣q∣ (x ‼ n - lookup (sequence x) B) (lookup (sequence x) B) ⟩
+     ∣ x ‼ n - lookup (sequence x) B ∣ ℚ.+ ∣ lookup (sequence x) B ∣
+       <⟨ +-monoˡ-< ∣ lookup (sequence x) B ∣ (proj₂ (isCauchy x 1ℚ) n≥B ℕ.≤-refl) ⟩
+     1ℚ ℚ.+ ∣ lookup (sequence x) B ∣ ≡⟨⟩
+     b ∎
+
+    lemma : ∀ a b → a ℚ.* a - b ℚ.* b ≡ (a ℚ.+ b) ℚ.* (a - b)
+    lemma = solve 2 (λ a b → (a :* a :- b :* b) , ((a :+ b) :* (a :- b))) refl
+      where open +-*-Solver
+
+_*_ : ℝ → ℝ → ℝ
+a * b = square (a + b) + ((- square a) + (- square b))

src/Data/Real/Properties.agda

@@ -0,0 +1,127 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of real numbers
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible --guardedness #-}
+
+module Data.Real.Properties where
+
+open import Data.Real.Base
+
+open import Algebra.Definitions _≈_
+open import Codata.Guarded.Stream
+open import Codata.Guarded.Stream.Properties
+import Codata.Guarded.Stream.Relation.Binary.Pointwise as PW
+open import Data.Product.Base hiding (map)
+import Data.Integer.Base as ℤ
+import Data.Nat.Base as ℕ
+import Data.Nat.Properties as ℕ
+import Data.Rational.Base as ℚ
+import Data.Rational.Properties as ℚ
+open import Data.Rational.Solver
+open import Function.Base using (_$_)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; cong₂)
+
++-cong : Congruent₂ _+_
++-cong {x} {y} {u} {v} x≈y u≈v ε = proj₁ (x≈y (ℚ.½ ℚ.* ε)) ℕ.⊔ proj₁ (u≈v (ℚ.½ ℚ.* ε)) , λ {n} n≥N → begin-strict
+  ℚ.∣ lookup (zipWith ℚ._+_ (sequence x) (sequence u)) n ℚ.- lookup (zipWith ℚ._+_ (sequence y) (sequence v)) n ∣
+    ≡⟨ cong₂ (λ a b → ℚ.∣ a ℚ.- b ∣) (lookup-zipWith n ℚ._+_ (sequence x) (sequence u)) (lookup-zipWith n ℚ._+_ (sequence y) (sequence v)) ⟩
+  ℚ.∣ (x ‼ n ℚ.+ lookup (sequence u) n) ℚ.- (y ‼ n ℚ.+ lookup (sequence v) n) ∣
+    ≡⟨ cong ℚ.∣_∣ (lemma (x ‼ n) (lookup (sequence u) n) (y ‼ n) (lookup (sequence v) n)) ⟩
+  ℚ.∣ (x ‼ n ℚ.- y ‼ n) ℚ.+ (lookup (sequence u) n ℚ.- lookup (sequence v) n) ∣
+    ≤⟨ ℚ.∣p+q∣≤∣p∣+∣q∣ (x ‼ n ℚ.- y ‼ n) (lookup (sequence u) n ℚ.- lookup (sequence v) n) ⟩
+  ℚ.∣ x ‼ n ℚ.- y ‼ n ∣ ℚ.+ ℚ.∣ lookup (sequence u) n ℚ.- lookup (sequence v) n ∣
+    <⟨ ℚ.+-mono-<
+      (proj₂ (x≈y (ℚ.½ ℚ.* ε)) (ℕ.≤-trans (ℕ.m≤m⊔n (proj₁ (x≈y (ℚ.½ ℚ.* ε))) (proj₁ (u≈v (ℚ.½ ℚ.* ε)))) n≥N))
+      (proj₂ (u≈v (ℚ.½ ℚ.* ε)) (ℕ.≤-trans (ℕ.m≤n⊔m (proj₁ (x≈y (ℚ.½ ℚ.* ε))) (proj₁ (u≈v (ℚ.½ ℚ.* ε)))) n≥N))
+    ⟩
+  ℚ.½ ℚ.* ε ℚ.+ ℚ.½ ℚ.* ε
+    ≡˘⟨ ℚ.*-distribʳ-+ ε ℚ.½ ℚ.½ ⟩
+  ℚ.1ℚ ℚ.* ε
+    ≡⟨ ℚ.*-identityˡ ε ⟩
+  ε ∎
+  where
+    open ℚ.≤-Reasoning
+    instance _ : ℚ.Positive (ℚ.½ ℚ.* ε)
+    _ = ℚ.pos*pos⇒pos ℚ.½ ε
+
+    lemma : ∀ a b c d → (a ℚ.+ b) ℚ.- (c ℚ.+ d) ≡ (a ℚ.- c) ℚ.+ (b ℚ.- d)
+    lemma = solve 4 (λ a b c d → ((a :+ b) :- (c :+ d)) , ((a :- c) :+ (b :- d))) refl
+      where open +-*-Solver
+
++-assoc : Associative _+_
++-assoc x y z ε = 0 , λ {n} _ → begin-strict
+  ℚ.∣ lookup (zipWith ℚ._+_ (zipWith ℚ._+_ (sequence x) (sequence y)) (sequence z)) n ℚ.- lookup (zipWith ℚ._+_ (sequence x) (zipWith ℚ._+_ (sequence y) (sequence z))) n ∣
+    ≡⟨ ℚ.d-definite (cong-lookup (PW.assoc ℚ.+-assoc (sequence x) (sequence y) (sequence z)) n) ⟩
+  ℚ.0ℚ
+    <⟨ ℚ.positive⁻¹ ε ⟩
+  ε ∎
+  where open ℚ.≤-Reasoning
+
++-comm : Commutative _+_
++-comm x y ε = 0 , λ {n} _ → begin-strict
+  ℚ.∣ lookup (zipWith ℚ._+_ (sequence x) (sequence y)) n ℚ.- lookup (zipWith ℚ._+_ (sequence y) (sequence x)) n ∣
+    ≡⟨ ℚ.d-definite (cong-lookup (PW.comm ℚ.+-comm (sequence x) (sequence y)) n) ⟩
+  ℚ.0ℚ
+    <⟨ ℚ.positive⁻¹ ε ⟩
+  ε ∎
+  where open ℚ.≤-Reasoning
+
++-identityˡ : LeftIdentity 0ℝ _+_
++-identityˡ x ε = 0 , λ {n} _ → begin-strict
+  ℚ.∣ lookup (zipWith ℚ._+_ (repeat ℚ.0ℚ) (sequence x)) n ℚ.- x ‼ n ∣
+    ≡⟨ ℚ.d-definite (cong-lookup (PW.identityˡ ℚ.+-identityˡ (sequence x)) n) ⟩
+  ℚ.0ℚ
+    <⟨ ℚ.positive⁻¹ ε ⟩
+  ε ∎
+  where open ℚ.≤-Reasoning
+
++-identityʳ : RightIdentity 0ℝ _+_
++-identityʳ x ε = 0 , λ {n} _ → begin-strict
+  ℚ.∣ lookup (zipWith ℚ._+_ (sequence x) (repeat ℚ.0ℚ)) n ℚ.- x ‼ n ∣
+    ≡⟨ ℚ.d-definite (cong-lookup (PW.identityʳ ℚ.+-identityʳ (sequence x)) n) ⟩
+  ℚ.0ℚ
+    <⟨ ℚ.positive⁻¹ ε ⟩
+  ε ∎
+  where open ℚ.≤-Reasoning
+
+-‿cong : Congruent₁ -_
+-‿cong {x} {y} x≈y ε = proj₁ (x≈y ε) , λ {n} n≥N → begin-strict
+  ℚ.∣ lookup (map ℚ.-_ (sequence x)) n ℚ.- lookup (map ℚ.-_ (sequence y)) n ∣
+    ≡⟨ cong₂ (λ a b → ℚ.∣ a ℚ.- b ∣) (lookup-map n ℚ.-_ (sequence x)) (lookup-map n ℚ.-_ (sequence y)) ⟩
+  ℚ.∣ (ℚ.- x ‼ n) ℚ.- (ℚ.- y ‼ n) ∣
+    ≡⟨ cong ℚ.∣_∣ (ℚ.neg-distrib-+ (x ‼ n) (ℚ.- y ‼ n)) ⟨
+  ℚ.∣ ℚ.- (x ‼ n ℚ.- y ‼ n) ∣
+    ≡⟨ ℚ.∣-p∣≡∣p∣ (x ‼ n ℚ.- y ‼ n) ⟩
+  ℚ.∣ x ‼ n ℚ.- y ‼ n ∣
+    <⟨ proj₂ (x≈y ε) n≥N ⟩
+  ε ∎
+  where open ℚ.≤-Reasoning
+
+-‿inverseˡ : LeftInverse 0ℝ -_ _+_
+-‿inverseˡ x ε = 0 , λ {n} _ → begin-strict
+  ℚ.∣ lookup (zipWith ℚ._+_ (map ℚ.-_ (sequence x)) (sequence x)) n ℚ.- lookup (repeat ℚ.0ℚ) n ∣
+    ≡⟨ cong₂ (λ a b → ℚ.∣ a ℚ.- b ∣) (lookup-zipWith n ℚ._+_ (map ℚ.-_ (sequence x)) (sequence x)) (lookup-repeat n ℚ.0ℚ) ⟩
+  ℚ.∣ (lookup (map ℚ.-_ (sequence x)) n ℚ.+ x ‼ n) ℚ.+ ℚ.0ℚ ∣
+    ≡⟨ cong (λ a → ℚ.∣ (a ℚ.+ x ‼ n) ℚ.+ ℚ.0ℚ ∣) (lookup-map n ℚ.-_ (sequence x)) ⟩
+  ℚ.∣ (ℚ.- x ‼ n ℚ.+ x ‼ n) ℚ.+ ℚ.0ℚ ∣
+    ≡⟨ cong (λ a → ℚ.∣ a ℚ.+ ℚ.0ℚ ∣) (ℚ.+-inverseˡ (x ‼ n)) ⟩
+  ℚ.∣ ℚ.0ℚ ∣
+    <⟨ ℚ.positive⁻¹ ε ⟩
+  ε ∎
+  where open ℚ.≤-Reasoning
+
+-‿inverseʳ : RightInverse 0ℝ -_ _+_
+-‿inverseʳ x ε = 0 , λ {n} _ → begin-strict
+  ℚ.∣ (x + (- x)) ‼ n ℚ.- 0ℝ ‼ n ∣
+    ≡⟨ cong₂ (λ a b → ℚ.∣ a ℚ.- b ∣) (lookup-zipWith n ℚ._+_ (sequence x) (sequence (- x))) (lookup-repeat n ℚ.0ℚ) ⟩
+  ℚ.∣ (x ‼ n ℚ.+ (- x) ‼ n) ℚ.+ ℚ.0ℚ ∣
+    ≡⟨ cong (λ a → ℚ.∣ (x ‼ n ℚ.+ a) ℚ.+ ℚ.0ℚ ∣) (lookup-map n ℚ.-_ (sequence x)) ⟩
+  ℚ.∣ (x ‼ n ℚ.- x ‼ n) ℚ.+ ℚ.0ℚ ∣
+    ≡⟨ cong (λ a → ℚ.∣ a ℚ.+ ℚ.0ℚ ∣) (ℚ.+-inverseʳ (x ‼ n)) ⟩
+  ℚ.0ℚ
+    <⟨ ℚ.positive⁻¹ ε ⟩
+  ε ∎
+  where open ℚ.≤-Reasoning

src/Function/Metric/Rational/CauchySequence.agda

@@ -0,0 +1,83 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Cauchy sequences on a metric over the rationals
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible --guardedness #-}
+
+open import Function.Metric.Rational.Bundles
+
+module Function.Metric.Rational.CauchySequence {a ℓ} (M : Metric a ℓ) where
+
+open Metric M hiding (_≈_)
+
+open import Codata.Guarded.Stream
+open import Codata.Guarded.Stream.Properties
+open import Data.Nat.Base as ℕ using (ℕ; z≤n; s≤s)
+import Data.Nat.Properties as ℕ
+open import Data.Integer.Base using (+<+)
+open import Data.Product.Base
+open import Data.Rational.Base
+open import Data.Rational.Properties
+open import Function.Base
+open import Level
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality using (cong₂)
+
+record CauchySequence : Set a where
+  field
+    sequence : Stream Carrier
+  _‼_ : ℕ → Carrier
+  _‼_ = lookup sequence
+  field
+    isCauchy : ∀ ε → .{{Positive ε}} → Σ[ N ∈ ℕ ] ∀ {m n} → m ℕ.≥ N → n ℕ.≥ N → d (_‼_ m) (_‼_ n) < ε
+
+open CauchySequence public
+
+_≈_ : Rel CauchySequence zero
+x ≈ y = ∀ ε → .{{Positive ε}} → Σ[ N ∈ ℕ ] (∀ {n} → n ℕ.≥ N → d (x ‼ n) (y ‼ n) < ε)
+
+≈-refl : Reflexive _≈_
+≈-refl {x} ε = 0 , λ {n} _ → begin-strict
+  d (x ‼ n) (x ‼ n) ≡⟨ ≈⇒0 EqC.refl ⟩
+  0ℚ                                                <⟨ positive⁻¹ ε ⟩
+  ε                                                 ∎
+  where open ≤-Reasoning
+
+≈-sym : Symmetric _≈_
+≈-sym {x} {y} p ε = proj₁ (p ε) , λ {n} n≥N → begin-strict
+  d (y ‼ n) (x ‼ n) ≡⟨ sym (y ‼ n) (x ‼ n) ⟩
+  d (x ‼ n) (y ‼ n) <⟨ proj₂ (p ε) n≥N ⟩
+  ε                                                 ∎
+  where open ≤-Reasoning
+
+≈-trans : Transitive _≈_
+≈-trans {x} {y} {z} p q ε = proj₁ (p (½ * ε)) ℕ.⊔ proj₁ (q (½ * ε)) , λ {n} n≥N → begin-strict
+  d (x ‼ n) (z ‼ n)
+    ≤⟨ triangle (x ‼ n) (y ‼ n) (z ‼ n) ⟩
+  d (x ‼ n) (y ‼ n) + d (y ‼ n) (z ‼ n)
+    <⟨ +-mono-<
+      (proj₂ (p (½ * ε)) (ℕ.≤-trans (ℕ.m≤m⊔n (proj₁ (p (½ * ε))) (proj₁ (q (½ * ε)))) n≥N))
+      (proj₂ (q (½ * ε)) (ℕ.≤-trans (ℕ.m≤n⊔m (proj₁ (p (½ * ε))) (proj₁ (q (½ * ε)))) n≥N))
+    ⟩
+  ½ * ε + ½ * ε
+    ≡˘⟨ *-distribʳ-+ ε ½ ½ ⟩
+  1ℚ * ε
+    ≡⟨ *-identityˡ ε ⟩
+  ε
+    ∎
+  where
+    open ≤-Reasoning
+    instance _ : Positive (½ * ε)
+    _ = pos*pos⇒pos ½ ε
+
+embed : Carrier → CauchySequence
+embed x = record
+  { sequence = repeat x
+  ; isCauchy = λ ε → 0 , λ {m n} _ _ → begin-strict
+    d (lookup (repeat x) m) (lookup (repeat x) n) ≡⟨ cong₂ d (lookup-repeat m x) (lookup-repeat n x) ⟩
+    d x x                                         ≡⟨ ≈⇒0 EqC.refl ⟩
+    0ℚ                                            <⟨ positive⁻¹ ε ⟩
+    ε                                             ∎
+  } where open ≤-Reasoning