From b0c259ac57e786abbd8e159b42e5c99b1c6b3620 Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Fri, 27 Sep 2024 11:26:58 +0200
Subject: [PATCH 01/16] WIP real numbers

---
 src/Data/Rational/Properties.agda             | 86 +++++++++++++++++++
 src/Data/Real/Base.agda                       | 73 ++++++++++++++++
 .../Metric/Rational/CauchySequence.agda       | 83 ++++++++++++++++++
 3 files changed, 242 insertions(+)
 create mode 100644 src/Data/Real/Base.agda
 create mode 100644 src/Function/Metric/Rational/CauchySequence.agda

diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda
index 0341f53c45..7eea1f24a3 100644
--- a/src/Data/Rational/Properties.agda
+++ b/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,91 @@ 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 ∣       ≡˘⟨ cong (λ # → ∣ # - q ∣) (⁻¹-involutive p) ⟩
+  ∣ - - p - q ∣   ≡˘⟨ cong ∣_∣ (neg-distrib-+ (- p) q) ⟩
+  ∣ - (- p + q) ∣ ≡⟨ cong (λ # → ∣ - # ∣) (+-comm (- p) q) ⟩
+  ∣ - (q - p) ∣   ≡⟨ ∣-p∣≡∣p∣ (q - p) ⟩
+  ∣ 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
diff --git a/src/Data/Real/Base.agda b/src/Data/Real/Base.agda
new file mode 100644
index 0000000000..f0aa3fa4cc
--- /dev/null
+++ b/src/Data/Real/Base.agda
@@ -0,0 +1,73 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Real numbers
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K --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 Function.Metric.Rational.CauchySequence d-metric public renaming (CauchySequence to ℝ)
+
+fromℚ : ℚ → ℝ
+fromℚ = embed
+
+_+_ : ℝ → ℝ → ℝ
+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) - (lookup (sequence x) n ℚ.+ lookup (sequence y) n) ∣
+    ≡⟨ cong ∣_∣ (lemma (lookup (sequence x) m) (lookup (sequence y) m) (lookup (sequence x) n) (lookup (sequence y) n)) ⟩
+  ∣ (lookup (sequence x) m - lookup (sequence x) n) ℚ.+ (lookup (sequence y) m - lookup (sequence y) n) ∣
+    ≤⟨ ∣p+q∣≤∣p∣+∣q∣
+      (lookup (sequence x) m - lookup (sequence x) n)
+      (lookup (sequence y) m - lookup (sequence y) n)
+    ⟩
+  ∣ lookup (sequence x) m - lookup (sequence x) n ∣ ℚ.+ ∣ lookup (sequence y) m - lookup (sequence 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 (½ * ε)
+    _ = positive {½ * ε} $ begin-strict
+      0ℚ     ≡˘⟨ *-zeroˡ ε ⟩
+      0ℚ * ε <⟨ *-monoˡ-<-pos ε {0ℚ} {½} (*<* (+<+ (s≤s z≤n))) ⟩
+      ½ * ε  ∎
+    [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
+
diff --git a/src/Function/Metric/Rational/CauchySequence.agda b/src/Function/Metric/Rational/CauchySequence.agda
new file mode 100644
index 0000000000..abb20e3a3c
--- /dev/null
+++ b/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
+    isCauchy : ∀ ε → {{Positive ε}} → Σ[ N ∈ ℕ ] ∀ {m n} → m ℕ.≥ N → n ℕ.≥ N → d (lookup sequence m) (lookup sequence n) < ε
+
+open CauchySequence public
+
+_≈_ : Rel CauchySequence zero
+x ≈ y = ∀ ε → .{{_ : Positive ε}} → Σ[ N ∈ ℕ ] (∀ {n} → n ℕ.≥ N → d (lookup (sequence x) n) (lookup (sequence y) n) < ε)
+
+≈-refl : Reflexive _≈_
+≈-refl {x} ε = 0 , λ {n} _ → begin-strict
+  d (lookup (sequence x) n) (lookup (sequence x) n) ≡⟨ ≈⇒0 EqC.refl ⟩
+  0ℚ                                                <⟨ positive⁻¹ ε ⟩
+  ε                                                 ∎
+  where open ≤-Reasoning
+
+≈-sym : Symmetric _≈_
+≈-sym {x} {y} p ε = proj₁ (p ε) , λ {n} n≥N → begin-strict
+  d (lookup (sequence y) n) (lookup (sequence x) n) ≡⟨ sym (lookup (sequence y) n) (lookup (sequence x) n) ⟩
+  d (lookup (sequence x) n) (lookup (sequence 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 (lookup (sequence x) n) (lookup (sequence z) n)
+    ≤⟨ triangle (lookup (sequence x) n) (lookup (sequence y) n) (lookup (sequence z) n) ⟩
+  d (lookup (sequence x) n) (lookup (sequence y) n) + d (lookup (sequence y) n) (lookup (sequence 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 (½ * ε)
+    _ = positive {½ * ε} $ begin-strict
+      0ℚ     ≡˘⟨ *-zeroˡ ε ⟩
+      0ℚ * ε <⟨ *-monoˡ-<-pos ε {0ℚ} {½} (*<* (+<+ (s≤s z≤n))) ⟩
+      ½ * ε  ∎
+
+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

From 2f83c326df495bf5591be5295c8e74fbee847e17 Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Fri, 27 Sep 2024 12:48:15 +0200
Subject: [PATCH 02/16] Add left multiplication by a rational

---
 src/Data/Real/Base.agda | 37 +++++++++++++++++++++++++++++++++++++
 1 file changed, 37 insertions(+)

diff --git a/src/Data/Real/Base.agda b/src/Data/Real/Base.agda
index f0aa3fa4cc..56b95edc1a 100644
--- a/src/Data/Real/Base.agda
+++ b/src/Data/Real/Base.agda
@@ -20,6 +20,7 @@ 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 ℝ)
 
@@ -71,3 +72,39 @@ isCauchy (x + y) ε = proj₁ [x] ℕ.+ proj₁ [y] , λ {m} {n} m≥N n≥N →
     lemma = solve 4 (λ a b c d → ((a :+ b) :- (c :+ d)) , ((a :- c) :+ (b :- d))) 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 * lookup (sequence x) n ∣                   ≡⟨ cong (λ # → ∣ p * lookup (sequence x) m ℚ.+ # ∣) (neg-distribʳ-* p (lookup (sequence x) n)) ⟩
+  ∣ p * lookup (sequence x) m ℚ.+ p * - lookup (sequence x) n ∣               ≡˘⟨ cong ∣_∣ (*-distribˡ-+ p (lookup (sequence x) m) (- lookup (sequence x) n)) ⟩
+  ∣ p * (lookup (sequence x) m - lookup (sequence x) n) ∣                     ≡⟨ cong (λ # → ∣ # * (lookup (sequence x) m - lookup (sequence x) n) ∣) p≡0 ⟩
+  ∣ 0ℚ * (lookup (sequence x) m - lookup (sequence x) n) ∣                    ≡⟨ cong ∣_∣ (*-zeroˡ (lookup (sequence x) m - lookup (sequence 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 * lookup (sequence x) n ∣                   ≡⟨ cong (λ # → ∣ p * lookup (sequence x) m ℚ.+ # ∣) (neg-distribʳ-* p (lookup (sequence x) n)) ⟩
+  ∣ p * lookup (sequence x) m ℚ.+ p * - lookup (sequence x) n ∣               ≡˘⟨ cong ∣_∣ (*-distribˡ-+ p (lookup (sequence x) m) (- lookup (sequence x) n)) ⟩
+  ∣ p * (lookup (sequence x) m - lookup (sequence x) n) ∣                     ≡⟨ ∣p*q∣≡∣p∣*∣q∣ p (lookup (sequence x) m - lookup (sequence x) n) ⟩
+  ∣ p ∣ * ∣ lookup (sequence x) m - lookup (sequence 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 ∣ * ε)
+    _ = positive $ begin-strict
+      0ℚ            ≡˘⟨ *-zeroʳ (1/ ∣ p ∣) ⟩
+      1/ ∣ p ∣ * 0ℚ <⟨ *-monoʳ-<-pos (1/ ∣ p ∣) (positive⁻¹ ε) ⟩
+      1/ ∣ p ∣ * ε  ∎

From 2b4bb6243b647b56886082ad164906bb68c25cfd Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Fri, 27 Sep 2024 12:51:57 +0200
Subject: [PATCH 03/16] cubical compatible

---
 src/Data/Real/Base.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Real/Base.agda b/src/Data/Real/Base.agda
index 56b95edc1a..54498246ff 100644
--- a/src/Data/Real/Base.agda
+++ b/src/Data/Real/Base.agda
@@ -4,7 +4,7 @@
 -- Real numbers
 ------------------------------------------------------------------------
 
-{-# OPTIONS --safe --without-K --guardedness #-}
+{-# OPTIONS --safe --cubical-compatible --guardedness #-}
 
 module Data.Real.Base where
 

From 7b8988c70c438aad3c1bfe7df3a354717a7429be Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Fri, 27 Sep 2024 14:25:16 +0200
Subject: [PATCH 04/16] Define square function

---
 src/Data/Real/Base.agda | 78 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 78 insertions(+)

diff --git a/src/Data/Real/Base.agda b/src/Data/Real/Base.agda
index 54498246ff..18d3806d84 100644
--- a/src/Data/Real/Base.agda
+++ b/src/Data/Real/Base.agda
@@ -108,3 +108,81 @@ isCauchy (p *ₗ x) ε with p ≟ 0ℚ
       0ℚ            ≡˘⟨ *-zeroʳ (1/ ∣ p ∣) ⟩
       1/ ∣ p ∣ * 0ℚ <⟨ *-monoʳ-<-pos (1/ ∣ p ∣) (positive⁻¹ ε) ⟩
       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 - lookup (sequence x) n * lookup (sequence x) n ∣
+    ≡⟨ cong ∣_∣ (lemma (lookup (sequence x) m) (lookup (sequence x) n)) ⟩
+  ∣ (lookup (sequence x) m ℚ.+ lookup (sequence x) n) * (lookup (sequence x) m - lookup (sequence x) n) ∣
+    ≡⟨ ∣p*q∣≡∣p∣*∣q∣ (lookup (sequence x) m ℚ.+ lookup (sequence x) n) (lookup (sequence x) m - lookup (sequence x) n) ⟩
+  ∣ lookup (sequence x) m ℚ.+ lookup (sequence x) n ∣ * ∣ lookup (sequence x) m - lookup (sequence x) n ∣
+    ≤⟨ *-monoʳ-≤-nonNeg ∣ lookup (sequence x) m - lookup (sequence x) n ∣ {{∣-∣-nonNeg (lookup (sequence x) m - lookup (sequence x) n)}} (∣p+q∣≤∣p∣+∣q∣ (lookup (sequence x) m) (lookup (sequence x) n)) ⟩
+  (∣ lookup (sequence x) m ∣ ℚ.+ ∣ lookup (sequence x) n ∣) * ∣ lookup (sequence x) m - lookup (sequence x) n ∣
+    ≤⟨ *-monoʳ-≤-nonNeg ∣ lookup (sequence x) m - lookup (sequence x) n ∣ {{∣-∣-nonNeg (lookup (sequence x) m - lookup (sequence 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 - lookup (sequence 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
+    _ = positive $ begin-strict
+      0ℚ                               ≤⟨ 0≤∣p∣ (lookup (sequence x) B) ⟩
+      ∣ lookup (sequence x) B ∣        ≡˘⟨ +-identityˡ ∣ lookup (sequence x) B ∣ ⟩
+      0ℚ ℚ.+ ∣ lookup (sequence x) B ∣ <⟨ +-monoˡ-< ∣ lookup (sequence x) B ∣ {0ℚ} {1ℚ} (*<* (+<+ (s≤s z≤n))) ⟩
+      1ℚ ℚ.+ ∣ lookup (sequence x) B ∣ ≡⟨⟩
+      b                                ∎
+
+    instance _ : NonZero b
+    _ = pos⇒nonZero b
+
+    instance _ : Positive (b ℚ.+ b)
+    _ = positive $ begin-strict
+      0ℚ        ≡⟨⟩
+      0ℚ ℚ.+ 0ℚ <⟨ +-mono-< (positive⁻¹ b) (positive⁻¹ b) ⟩
+      b ℚ.+ b   ∎
+
+    instance _ : NonZero (b ℚ.+ b)
+    _ = pos⇒nonZero (b ℚ.+ b)
+
+    instance _ : Positive (1/ (b ℚ.+ b) * ε)
+    _ = positive $ begin-strict
+      0ℚ               ≡⟨⟩
+      0ℚ * 0ℚ          ≡˘⟨ *-zeroˡ ε ⟩
+      0ℚ * ε           <⟨ *-monoˡ-<-pos ε (positive⁻¹ (1/ (b ℚ.+ b)) {{1/pos⇒pos (b ℚ.+ b)}}) ⟩
+      1/ (b ℚ.+ b) * ε ∎
+
+    b-prop : ∀ {n} → n ℕ.≥ B → ∣ lookup (sequence x) n ∣ < b
+    b-prop {n} n≥B = begin-strict
+     ∣ lookup (sequence x) n ∣ ≡˘⟨ cong ∣_∣ (+-identityʳ (lookup (sequence x) n)) ⟩
+     ∣ lookup (sequence x) n ℚ.+ 0ℚ ∣ ≡˘⟨ cong (λ # → ∣ lookup (sequence x) n ℚ.+ # ∣) (+-inverseˡ (lookup (sequence x) B)) ⟩
+     ∣ lookup (sequence x) n ℚ.+ (- lookup (sequence x) B ℚ.+ lookup (sequence x) B) ∣ ≡˘⟨ cong ∣_∣ (+-assoc (lookup (sequence x) n) (- lookup (sequence x) B) (lookup (sequence x) B)) ⟩
+     ∣ (lookup (sequence x) n - lookup (sequence x) B) ℚ.+ lookup (sequence x) B ∣ ≤⟨ ∣p+q∣≤∣p∣+∣q∣ (lookup (sequence x) n - lookup (sequence x) B) (lookup (sequence x) B) ⟩
+     ∣ lookup (sequence 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

From 2eb083c146b23363038d7d4141d31f381cf5fcbd Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Fri, 27 Sep 2024 14:36:08 +0200
Subject: [PATCH 05/16] Implement negation

---
 src/Data/Real/Base.agda | 22 ++++++++++++++++++----
 1 file changed, 18 insertions(+), 4 deletions(-)

diff --git a/src/Data/Real/Base.agda b/src/Data/Real/Base.agda
index 18d3806d84..b5e05f0d39 100644
--- a/src/Data/Real/Base.agda
+++ b/src/Data/Real/Base.agda
@@ -14,7 +14,7 @@ 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.Base as ℚ hiding (_+_; -_)
 open import Data.Rational.Properties
 open import Data.Rational.Solver
 open import Data.Rational.Unnormalised using (*<*)
@@ -72,13 +72,27 @@ isCauchy (x + y) ε = proj₁ [x] ℕ.+ proj₁ [y] , λ {m} {n} m≥N n≥N →
     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 - ℚ.- lookup (sequence x) n ∣ ≡⟨ cong ∣_∣ (lemma (lookup (sequence x) m) (lookup (sequence x) n)) ⟩
+  ∣ ℚ.- (lookup (sequence x) m - lookup (sequence x) n) ∣ ≡⟨ ∣-p∣≡∣p∣ (lookup (sequence x) m - lookup (sequence x) n) ⟩
+  ∣ lookup (sequence x) m - lookup (sequence 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 * lookup (sequence x) n ∣                   ≡⟨ cong (λ # → ∣ p * lookup (sequence x) m ℚ.+ # ∣) (neg-distribʳ-* p (lookup (sequence x) n)) ⟩
-  ∣ p * lookup (sequence x) m ℚ.+ p * - lookup (sequence x) n ∣               ≡˘⟨ cong ∣_∣ (*-distribˡ-+ p (lookup (sequence x) m) (- lookup (sequence x) n)) ⟩
+  ∣ p * lookup (sequence x) m ℚ.+ p * ℚ.- lookup (sequence x) n ∣             ≡˘⟨ cong ∣_∣ (*-distribˡ-+ p (lookup (sequence x) m) (ℚ.- lookup (sequence x) n)) ⟩
   ∣ p * (lookup (sequence x) m - lookup (sequence x) n) ∣                     ≡⟨ cong (λ # → ∣ # * (lookup (sequence x) m - lookup (sequence x) n) ∣) p≡0 ⟩
   ∣ 0ℚ * (lookup (sequence x) m - lookup (sequence x) n) ∣                    ≡⟨ cong ∣_∣ (*-zeroˡ (lookup (sequence x) m - lookup (sequence x) n)) ⟩
   ∣ 0ℚ ∣                                                                      ≡⟨⟩
@@ -88,7 +102,7 @@ isCauchy (p *ₗ x) ε with p ≟ 0ℚ
 ... | 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 * lookup (sequence x) n ∣                   ≡⟨ cong (λ # → ∣ p * lookup (sequence x) m ℚ.+ # ∣) (neg-distribʳ-* p (lookup (sequence x) n)) ⟩
-  ∣ p * lookup (sequence x) m ℚ.+ p * - lookup (sequence x) n ∣               ≡˘⟨ cong ∣_∣ (*-distribˡ-+ p (lookup (sequence x) m) (- lookup (sequence x) n)) ⟩
+  ∣ p * lookup (sequence x) m ℚ.+ p * ℚ.- lookup (sequence x) n ∣             ≡˘⟨ cong ∣_∣ (*-distribˡ-+ p (lookup (sequence x) m) (ℚ.- lookup (sequence x) n)) ⟩
   ∣ p * (lookup (sequence x) m - lookup (sequence x) n) ∣                     ≡⟨ ∣p*q∣≡∣p∣*∣q∣ p (lookup (sequence x) m - lookup (sequence x) n) ⟩
   ∣ p ∣ * ∣ lookup (sequence x) m - lookup (sequence x) n ∣                   <⟨ *-monoʳ-<-pos ∣ p ∣ (proj₂ (isCauchy x (1/ ∣ p ∣ * ε)) m≥N n≥N) ⟩
   ∣ p ∣ * (1/ ∣ p ∣ * ε)                                                      ≡˘⟨ *-assoc ∣ p ∣ (1/ ∣ p ∣) ε ⟩
@@ -177,7 +191,7 @@ isCauchy (square x) ε = B ℕ.⊔ proj₁ (isCauchy x (1/ (b ℚ.+ b) * ε)) ,
     b-prop {n} n≥B = begin-strict
      ∣ lookup (sequence x) n ∣ ≡˘⟨ cong ∣_∣ (+-identityʳ (lookup (sequence x) n)) ⟩
      ∣ lookup (sequence x) n ℚ.+ 0ℚ ∣ ≡˘⟨ cong (λ # → ∣ lookup (sequence x) n ℚ.+ # ∣) (+-inverseˡ (lookup (sequence x) B)) ⟩
-     ∣ lookup (sequence x) n ℚ.+ (- lookup (sequence x) B ℚ.+ lookup (sequence x) B) ∣ ≡˘⟨ cong ∣_∣ (+-assoc (lookup (sequence x) n) (- lookup (sequence x) B) (lookup (sequence x) B)) ⟩
+     ∣ lookup (sequence x) n ℚ.+ (ℚ.- lookup (sequence x) B ℚ.+ lookup (sequence x) B) ∣ ≡˘⟨ cong ∣_∣ (+-assoc (lookup (sequence x) n) (ℚ.- lookup (sequence x) B) (lookup (sequence x) B)) ⟩
      ∣ (lookup (sequence x) n - lookup (sequence x) B) ℚ.+ lookup (sequence x) B ∣ ≤⟨ ∣p+q∣≤∣p∣+∣q∣ (lookup (sequence x) n - lookup (sequence x) B) (lookup (sequence x) B) ⟩
      ∣ lookup (sequence 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 ∣ ≡⟨⟩

From fdf3da7d4de6c7a41244efa0bd10c131cb773def Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Fri, 27 Sep 2024 15:49:37 +0200
Subject: [PATCH 06/16] Start adding properties

---
 src/Data/Real/Properties.agda | 93 +++++++++++++++++++++++++++++++++++
 1 file changed, 93 insertions(+)
 create mode 100644 src/Data/Real/Properties.agda

diff --git a/src/Data/Real/Properties.agda b/src/Data/Real/Properties.agda
new file mode 100644
index 0000000000..3a314cadf0
--- /dev/null
+++ b/src/Data/Real/Properties.agda
@@ -0,0 +1,93 @@
+------------------------------------------------------------------------
+-- 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
+open import Data.Product.Base
+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)) ⟩
+  ℚ.∣ (lookup (sequence x) n ℚ.+ lookup (sequence u) n) ℚ.- (lookup (sequence y) n ℚ.+ lookup (sequence v) n) ∣
+    ≡⟨ cong ℚ.∣_∣ (lemma (lookup (sequence x) n) (lookup (sequence u) n) (lookup (sequence y) n) (lookup (sequence v) n)) ⟩
+  ℚ.∣ (lookup (sequence x) n ℚ.- lookup (sequence y) n) ℚ.+ (lookup (sequence u) n ℚ.- lookup (sequence v) n) ∣
+    ≤⟨ ℚ.∣p+q∣≤∣p∣+∣q∣ (lookup (sequence x) n ℚ.- lookup (sequence y) n) (lookup (sequence u) n ℚ.- lookup (sequence v) n) ⟩
+  ℚ.∣ lookup (sequence x) n ℚ.- lookup (sequence 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 (ℚ.½ ℚ.* ε)
+    _ = ℚ.positive $ begin-strict
+      ℚ.0ℚ       ≡˘⟨ ℚ.*-zeroˡ ε ⟩
+      ℚ.0ℚ ℚ.* ε <⟨ ℚ.*-monoˡ-<-pos ε {ℚ.0ℚ} {ℚ.½} (ℚ.*<* (ℤ.+<+ (ℕ.s≤s ℕ.z≤n))) ⟩
+      ℚ.½ ℚ.* ε  ∎
+
+    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 ∣
+    ≡⟨ cong₂ (λ a b → ℚ.∣ a ℚ.- b ∣)
+      (lookup-zipWith n ℚ._+_ (zipWith ℚ._+_ (sequence x) (sequence y)) (sequence z))
+      (lookup-zipWith n ℚ._+_ (sequence x) (zipWith ℚ._+_ (sequence y) (sequence z))) ⟩
+  ℚ.∣ (lookup (zipWith ℚ._+_ (sequence x) (sequence y)) n ℚ.+ lookup (sequence z) n) ℚ.- (lookup (sequence x) n ℚ.+ lookup (zipWith ℚ._+_ (sequence y) (sequence z)) n) ∣
+    ≡⟨ cong₂ (λ a b → ℚ.∣ (a ℚ.+ lookup (sequence z) n) ℚ.- (lookup (sequence x) n ℚ.+ b) ∣)
+      (lookup-zipWith n ℚ._+_ (sequence x) (sequence y))
+      (lookup-zipWith n ℚ._+_ (sequence y) (sequence z)) ⟩
+  ℚ.∣ ((lookup (sequence x) n ℚ.+ lookup (sequence y) n) ℚ.+ lookup (sequence z) n) ℚ.- (lookup (sequence x) n ℚ.+ (lookup (sequence y) n ℚ.+ lookup (sequence z) n)) ∣
+    ≡⟨ cong (λ a → ℚ.∣ a ℚ.- (lookup (sequence x) n ℚ.+ (lookup (sequence y) n ℚ.+ lookup (sequence z) n)) ∣) (ℚ.+-assoc (lookup (sequence x) n) (lookup (sequence y) n) (lookup (sequence z) n)) ⟩
+  ℚ.∣ (lookup (sequence x) n ℚ.+ (lookup (sequence y) n ℚ.+ lookup (sequence z) n)) ℚ.- (lookup (sequence x) n ℚ.+ (lookup (sequence y) n ℚ.+ lookup (sequence z) n)) ∣
+    ≡⟨ cong ℚ.∣_∣ (ℚ.+-inverseʳ (lookup (sequence x) n ℚ.+ (lookup (sequence y) n ℚ.+ lookup (sequence z) n))) ⟩
+  ℚ.∣ ℚ.0ℚ ∣
+    ≡⟨⟩
+  ℚ.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 ∣
+    ≡⟨ cong₂ (λ a b → ℚ.∣ a ℚ.- b ∣)
+      (lookup-zipWith n ℚ._+_ (sequence x) (sequence y))
+      (lookup-zipWith n ℚ._+_ (sequence y) (sequence x)) ⟩
+  ℚ.∣ (lookup (sequence x) n ℚ.+ lookup (sequence y) n) ℚ.- (lookup (sequence y) n ℚ.+ lookup (sequence x) n) ∣
+    ≡⟨ cong (λ a → ℚ.∣ a ℚ.- (lookup (sequence y) n ℚ.+ lookup (sequence x) n) ∣) (ℚ.+-comm (lookup (sequence x) n) (lookup (sequence y) n)) ⟩
+  ℚ.∣ (lookup (sequence y) n ℚ.+ lookup (sequence x) n) ℚ.- (lookup (sequence y) n ℚ.+ lookup (sequence x) n) ∣
+    ≡⟨ cong ℚ.∣_∣ (ℚ.+-inverseʳ (lookup (sequence y) n ℚ.+ lookup (sequence x) n)) ⟩
+  ℚ.∣ ℚ.0ℚ ∣
+    ≡⟨⟩
+  ℚ.0ℚ
+    <⟨ ℚ.positive⁻¹ ε ⟩
+  ε ∎
+  where open ℚ.≤-Reasoning
+

From 978c945322129ee384d74d9ec57411ec2e7f6c79 Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Sat, 28 Sep 2024 08:50:36 +0200
Subject: [PATCH 07/16] Simplify d-sym proof

---
 src/Data/Rational/Properties.agda | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda
index 7eea1f24a3..9165b3c4ac 100644
--- a/src/Data/Rational/Properties.agda
+++ b/src/Data/Rational/Properties.agda
@@ -1832,11 +1832,9 @@ d-indiscernable {p} {q} ∣p-q∣≡0 = begin
 
 d-sym : Metric.Symmetric d
 d-sym p q = begin
-  ∣ p - q ∣       ≡˘⟨ cong (λ # → ∣ # - q ∣) (⁻¹-involutive p) ⟩
-  ∣ - - p - q ∣   ≡˘⟨ cong ∣_∣ (neg-distrib-+ (- p) q) ⟩
-  ∣ - (- p + q) ∣ ≡⟨ cong (λ # → ∣ - # ∣) (+-comm (- p) q) ⟩
-  ∣ - (q - p) ∣   ≡⟨ ∣-p∣≡∣p∣ (q - p) ⟩
-  ∣ q - p ∣       ∎
+  ∣ p - q ∣     ≡˘⟨ ∣-p∣≡∣p∣ (p - q) ⟩
+  ∣ - (p - q) ∣ ≡⟨ cong ∣_∣ (⁻¹-anti-homo-// p q) ⟩
+  ∣ q - p ∣     ∎
   where
     open ≡-Reasoning
     open GroupProperties +-0-group

From 4fa5d9ddf97040383bd6103efbf9ebc1aa0f27aa Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Sat, 28 Sep 2024 08:50:49 +0200
Subject: [PATCH 08/16] Irrelevant positivity

---
 src/Function/Metric/Rational/CauchySequence.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Function/Metric/Rational/CauchySequence.agda b/src/Function/Metric/Rational/CauchySequence.agda
index abb20e3a3c..1848f97dac 100644
--- a/src/Function/Metric/Rational/CauchySequence.agda
+++ b/src/Function/Metric/Rational/CauchySequence.agda
@@ -28,12 +28,12 @@ open import Relation.Binary.PropositionalEquality using (cong₂)
 record CauchySequence : Set a where
   field
     sequence : Stream Carrier
-    isCauchy : ∀ ε → {{Positive ε}} → Σ[ N ∈ ℕ ] ∀ {m n} → m ℕ.≥ N → n ℕ.≥ N → d (lookup sequence m) (lookup sequence n) < ε
+    isCauchy : ∀ ε → .{{Positive ε}} → Σ[ N ∈ ℕ ] ∀ {m n} → m ℕ.≥ N → n ℕ.≥ N → d (lookup sequence m) (lookup sequence n) < ε
 
 open CauchySequence public
 
 _≈_ : Rel CauchySequence zero
-x ≈ y = ∀ ε → .{{_ : Positive ε}} → Σ[ N ∈ ℕ ] (∀ {n} → n ℕ.≥ N → d (lookup (sequence x) n) (lookup (sequence y) n) < ε)
+x ≈ y = ∀ ε → .{{Positive ε}} → Σ[ N ∈ ℕ ] (∀ {n} → n ℕ.≥ N → d (lookup (sequence x) n) (lookup (sequence y) n) < ε)
 
 ≈-refl : Reflexive _≈_
 ≈-refl {x} ε = 0 , λ {n} _ → begin-strict

From 84e02abaecefa6c6043b5180b88b216aa7ee8d66 Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Sat, 28 Sep 2024 08:58:16 +0200
Subject: [PATCH 09/16] Add and use pos*pos=>pos

---
 src/Data/Real/Base.agda                          | 16 +++-------------
 src/Data/Real/Properties.agda                    |  5 +----
 src/Function/Metric/Rational/CauchySequence.agda |  5 +----
 3 files changed, 5 insertions(+), 21 deletions(-)

diff --git a/src/Data/Real/Base.agda b/src/Data/Real/Base.agda
index b5e05f0d39..85c3d68204 100644
--- a/src/Data/Real/Base.agda
+++ b/src/Data/Real/Base.agda
@@ -61,10 +61,7 @@ isCauchy (x + y) ε = proj₁ [x] ℕ.+ proj₁ [y] , λ {m} {n} m≥N n≥N →
   where
     open ≤-Reasoning
     instance _ : Positive (½ * ε)
-    _ = positive {½ * ε} $ begin-strict
-      0ℚ     ≡˘⟨ *-zeroˡ ε ⟩
-      0ℚ * ε <⟨ *-monoˡ-<-pos ε {0ℚ} {½} (*<* (+<+ (s≤s z≤n))) ⟩
-      ½ * ε  ∎
+    _ = pos*pos⇒pos ½ ε
     [x] = isCauchy x (½ * ε)
     [y] = isCauchy y (½ * ε)
 
@@ -118,10 +115,7 @@ isCauchy (p *ₗ x) ε with p ≟ 0ℚ
     instance _ : Positive (1/ ∣ p ∣)
     _ = 1/pos⇒pos ∣ p ∣
     instance _ : Positive (1/ ∣ p ∣ * ε)
-    _ = positive $ begin-strict
-      0ℚ            ≡˘⟨ *-zeroʳ (1/ ∣ p ∣) ⟩
-      1/ ∣ p ∣ * 0ℚ <⟨ *-monoʳ-<-pos (1/ ∣ p ∣) (positive⁻¹ ε) ⟩
-      1/ ∣ p ∣ * ε  ∎
+    _ = pos*pos⇒pos (1/ ∣ p ∣) ε
 
 square : ℝ → ℝ
 sequence (square x) = map (λ p → p * p) (sequence x)
@@ -181,11 +175,7 @@ isCauchy (square x) ε = B ℕ.⊔ proj₁ (isCauchy x (1/ (b ℚ.+ b) * ε)) ,
     _ = pos⇒nonZero (b ℚ.+ b)
 
     instance _ : Positive (1/ (b ℚ.+ b) * ε)
-    _ = positive $ begin-strict
-      0ℚ               ≡⟨⟩
-      0ℚ * 0ℚ          ≡˘⟨ *-zeroˡ ε ⟩
-      0ℚ * ε           <⟨ *-monoˡ-<-pos ε (positive⁻¹ (1/ (b ℚ.+ b)) {{1/pos⇒pos (b ℚ.+ b)}}) ⟩
-      1/ (b ℚ.+ b) * ε ∎
+    _ = pos*pos⇒pos (1/ (b ℚ.+ b)) ε {{1/pos⇒pos (b ℚ.+ b)}}
 
     b-prop : ∀ {n} → n ℕ.≥ B → ∣ lookup (sequence x) n ∣ < b
     b-prop {n} n≥B = begin-strict
diff --git a/src/Data/Real/Properties.agda b/src/Data/Real/Properties.agda
index 3a314cadf0..79cce497e9 100644
--- a/src/Data/Real/Properties.agda
+++ b/src/Data/Real/Properties.agda
@@ -44,10 +44,7 @@ open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; cong
   where
     open ℚ.≤-Reasoning
     instance _ : ℚ.Positive (ℚ.½ ℚ.* ε)
-    _ = ℚ.positive $ begin-strict
-      ℚ.0ℚ       ≡˘⟨ ℚ.*-zeroˡ ε ⟩
-      ℚ.0ℚ ℚ.* ε <⟨ ℚ.*-monoˡ-<-pos ε {ℚ.0ℚ} {ℚ.½} (ℚ.*<* (ℤ.+<+ (ℕ.s≤s ℕ.z≤n))) ⟩
-      ℚ.½ ℚ.* ε  ∎
+    _ = ℚ.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
diff --git a/src/Function/Metric/Rational/CauchySequence.agda b/src/Function/Metric/Rational/CauchySequence.agda
index 1848f97dac..b82ac55c92 100644
--- a/src/Function/Metric/Rational/CauchySequence.agda
+++ b/src/Function/Metric/Rational/CauchySequence.agda
@@ -67,10 +67,7 @@ x ≈ y = ∀ ε → .{{Positive ε}} → Σ[ N ∈ ℕ ] (∀ {n} → n ℕ.≥
   where
     open ≤-Reasoning
     instance _ : Positive (½ * ε)
-    _ = positive {½ * ε} $ begin-strict
-      0ℚ     ≡˘⟨ *-zeroˡ ε ⟩
-      0ℚ * ε <⟨ *-monoˡ-<-pos ε {0ℚ} {½} (*<* (+<+ (s≤s z≤n))) ⟩
-      ½ * ε  ∎
+    _ = pos*pos⇒pos ½ ε
 
 embed : Carrier → CauchySequence
 embed x = record

From c71b937b8dff711aac549ea78f66065ea6453c58 Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Sat, 28 Sep 2024 08:59:19 +0200
Subject: [PATCH 10/16] Fiddle with order of instance arguments

This makes it easier to supply either explicitly
---
 src/Data/Real/Base.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Real/Base.agda b/src/Data/Real/Base.agda
index 85c3d68204..8765b5e683 100644
--- a/src/Data/Real/Base.agda
+++ b/src/Data/Real/Base.agda
@@ -175,7 +175,7 @@ isCauchy (square x) ε = B ℕ.⊔ proj₁ (isCauchy x (1/ (b ℚ.+ b) * ε)) ,
     _ = pos⇒nonZero (b ℚ.+ b)
 
     instance _ : Positive (1/ (b ℚ.+ b) * ε)
-    _ = pos*pos⇒pos (1/ (b ℚ.+ b)) ε {{1/pos⇒pos (b ℚ.+ b)}}
+    _ = pos*pos⇒pos (1/ (b ℚ.+ b)) {{1/pos⇒pos (b ℚ.+ b)}} ε
 
     b-prop : ∀ {n} → n ℕ.≥ B → ∣ lookup (sequence x) n ∣ < b
     b-prop {n} n≥B = begin-strict

From 16a497c27c199e10dfb7ad1b2a7d38f8ccda3dc5 Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Sat, 28 Sep 2024 10:21:31 +0200
Subject: [PATCH 11/16] Use new symmetric syntax in Data.Rational.Properties

---
 src/Data/Rational/Properties.agda | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda
index 9165b3c4ac..13bda7b636 100644
--- a/src/Data/Rational/Properties.agda
+++ b/src/Data/Rational/Properties.agda
@@ -1819,10 +1819,10 @@ 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               ≡⟨ +-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) ≡⟨ +-assoc p (- p) (- - q) ⟨
   (p - p) - - q   ≡⟨ cong₂ _+_ (+-inverseʳ p) (⁻¹-involutive q) ⟩
   0ℚ + q          ≡⟨ +-identityˡ q ⟩
   q               ∎
@@ -1841,9 +1841,9 @@ d-sym p q = begin
 
 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 - 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 ∣ ∎

From f40c0854023f3582bd22021b2b1bf31a39ac3d79 Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Sat, 28 Sep 2024 10:26:32 +0200
Subject: [PATCH 12/16] Use new symmetric syntax elsewhere

---
 src/Data/Real/Base.agda | 95 +++++++++++++++++++++++++++--------------
 1 file changed, 62 insertions(+), 33 deletions(-)

diff --git a/src/Data/Real/Base.agda b/src/Data/Real/Base.agda
index 8765b5e683..bb8c37968a 100644
--- a/src/Data/Real/Base.agda
+++ b/src/Data/Real/Base.agda
@@ -54,7 +54,7 @@ isCauchy (x + y) ε = proj₁ [x] ℕ.+ proj₁ [y] , λ {m} {n} m≥N n≥N →
       )
     ⟩
   ½ * ε ℚ.+ ½ * ε
-    ≡˘⟨ *-distribʳ-+ ε ½ ½ ⟩
+    ≡⟨ *-distribʳ-+ ε ½ ½ ⟨
   1ℚ * ε
     ≡⟨ *-identityˡ ε ⟩
   ε ∎
@@ -72,10 +72,14 @@ isCauchy (x + y) ε = proj₁ [x] ℕ.+ proj₁ [y] , λ {m} {n} m≥N n≥N →
 -_ : ℝ → ℝ
 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 - ℚ.- lookup (sequence x) n ∣ ≡⟨ cong ∣_∣ (lemma (lookup (sequence x) m) (lookup (sequence x) n)) ⟩
-  ∣ ℚ.- (lookup (sequence x) m - lookup (sequence x) n) ∣ ≡⟨ ∣-p∣≡∣p∣ (lookup (sequence x) m - lookup (sequence x) n) ⟩
-  ∣ lookup (sequence x) m - lookup (sequence x) n ∣ <⟨ proj₂ (isCauchy x ε) m≥N n≥N ⟩
+  ∣ 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 - ℚ.- lookup (sequence x) n ∣
+    ≡⟨ cong ∣_∣ (lemma (lookup (sequence x) m) (lookup (sequence x) n)) ⟩
+  ∣ ℚ.- (lookup (sequence x) m - lookup (sequence x) n) ∣
+    ≡⟨ ∣-p∣≡∣p∣ (lookup (sequence x) m - lookup (sequence x) n) ⟩
+  ∣ lookup (sequence x) m - lookup (sequence x) n ∣
+    <⟨ proj₂ (isCauchy x ε) m≥N n≥N ⟩
   ε ∎
   where
     open ≤-Reasoning
@@ -87,25 +91,39 @@ _*ₗ_ : ℚ → ℝ → ℝ
 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 * lookup (sequence x) n ∣                   ≡⟨ cong (λ # → ∣ p * lookup (sequence x) m ℚ.+ # ∣) (neg-distribʳ-* p (lookup (sequence x) n)) ⟩
-  ∣ p * lookup (sequence x) m ℚ.+ p * ℚ.- lookup (sequence x) n ∣             ≡˘⟨ cong ∣_∣ (*-distribˡ-+ p (lookup (sequence x) m) (ℚ.- lookup (sequence x) n)) ⟩
-  ∣ p * (lookup (sequence x) m - lookup (sequence x) n) ∣                     ≡⟨ cong (λ # → ∣ # * (lookup (sequence x) m - lookup (sequence x) n) ∣) p≡0 ⟩
-  ∣ 0ℚ * (lookup (sequence x) m - lookup (sequence x) n) ∣                    ≡⟨ cong ∣_∣ (*-zeroˡ (lookup (sequence x) m - lookup (sequence x) n)) ⟩
-  ∣ 0ℚ ∣                                                                      ≡⟨⟩
-  0ℚ                                                                          <⟨ positive⁻¹ ε ⟩
-  ε                                                                           ∎
+  ∣ 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 * lookup (sequence x) n ∣
+    ≡⟨ cong (λ # → ∣ p * lookup (sequence x) m ℚ.+ # ∣) (neg-distribʳ-* p (lookup (sequence x) n)) ⟩
+  ∣ p * lookup (sequence x) m ℚ.+ p * ℚ.- lookup (sequence x) n ∣
+    ≡⟨ cong ∣_∣ (*-distribˡ-+ p (lookup (sequence x) m) (ℚ.- lookup (sequence x) n)) ⟨
+  ∣ p * (lookup (sequence x) m - lookup (sequence x) n) ∣
+    ≡⟨ cong (λ # → ∣ # * (lookup (sequence x) m - lookup (sequence x) n) ∣) p≡0 ⟩
+  ∣ 0ℚ * (lookup (sequence x) m - lookup (sequence x) n) ∣
+    ≡⟨ cong ∣_∣ (*-zeroˡ (lookup (sequence x) m - lookup (sequence 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)) ⟩
+  ∣ 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 * lookup (sequence x) n ∣                   ≡⟨ cong (λ # → ∣ p * lookup (sequence x) m ℚ.+ # ∣) (neg-distribʳ-* p (lookup (sequence x) n)) ⟩
-  ∣ p * lookup (sequence x) m ℚ.+ p * ℚ.- lookup (sequence x) n ∣             ≡˘⟨ cong ∣_∣ (*-distribˡ-+ p (lookup (sequence x) m) (ℚ.- lookup (sequence x) n)) ⟩
-  ∣ p * (lookup (sequence x) m - lookup (sequence x) n) ∣                     ≡⟨ ∣p*q∣≡∣p∣*∣q∣ p (lookup (sequence x) m - lookup (sequence x) n) ⟩
-  ∣ p ∣ * ∣ lookup (sequence x) m - lookup (sequence 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ˡ ε ⟩
-  ε                                                                           ∎
+  ∣ p * lookup (sequence x) m ℚ.+ p * ℚ.- lookup (sequence x) n ∣
+    ≡⟨ cong ∣_∣ (*-distribˡ-+ p (lookup (sequence x) m) (ℚ.- lookup (sequence x) n)) ⟨
+  ∣ p * (lookup (sequence x) m - lookup (sequence x) n) ∣
+    ≡⟨ ∣p*q∣≡∣p∣*∣q∣ p (lookup (sequence x) m - lookup (sequence x) n) ⟩
+  ∣ p ∣ * ∣ lookup (sequence x) m - lookup (sequence 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 ∣
@@ -127,19 +145,25 @@ isCauchy (square x) ε = B ℕ.⊔ proj₁ (isCauchy x (1/ (b ℚ.+ b) * ε)) ,
   ∣ (lookup (sequence x) m ℚ.+ lookup (sequence x) n) * (lookup (sequence x) m - lookup (sequence x) n) ∣
     ≡⟨ ∣p*q∣≡∣p∣*∣q∣ (lookup (sequence x) m ℚ.+ lookup (sequence x) n) (lookup (sequence x) m - lookup (sequence x) n) ⟩
   ∣ lookup (sequence x) m ℚ.+ lookup (sequence x) n ∣ * ∣ lookup (sequence x) m - lookup (sequence x) n ∣
-    ≤⟨ *-monoʳ-≤-nonNeg ∣ lookup (sequence x) m - lookup (sequence x) n ∣ {{∣-∣-nonNeg (lookup (sequence x) m - lookup (sequence x) n)}} (∣p+q∣≤∣p∣+∣q∣ (lookup (sequence x) m) (lookup (sequence x) n)) ⟩
+    ≤⟨ *-monoʳ-≤-nonNeg ∣ lookup (sequence x) m - lookup (sequence x) n ∣
+      {{∣-∣-nonNeg (lookup (sequence x) m - lookup (sequence x) n)}}
+      (∣p+q∣≤∣p∣+∣q∣ (lookup (sequence x) m) (lookup (sequence x) n))
+    ⟩
   (∣ lookup (sequence x) m ∣ ℚ.+ ∣ lookup (sequence x) n ∣) * ∣ lookup (sequence x) m - lookup (sequence x) n ∣
-    ≤⟨ *-monoʳ-≤-nonNeg ∣ lookup (sequence x) m - lookup (sequence x) n ∣ {{∣-∣-nonNeg (lookup (sequence x) m - lookup (sequence 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))
-    )) ⟩
+    ≤⟨ *-monoʳ-≤-nonNeg ∣ lookup (sequence x) m - lookup (sequence x) n ∣
+      {{∣-∣-nonNeg (lookup (sequence x) m - lookup (sequence 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 - lookup (sequence 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)) ε ⟩
+    ≡⟨ *-assoc (b ℚ.+ b) (1/ (b ℚ.+ b)) ε ⟨
   ((b ℚ.+ b) * 1/ (b ℚ.+ b)) * ε
     ≡⟨ cong (_* ε) (*-inverseʳ (b ℚ.+ b)) ⟩
   1ℚ * ε
@@ -157,7 +181,7 @@ isCauchy (square x) ε = B ℕ.⊔ proj₁ (isCauchy x (1/ (b ℚ.+ b) * ε)) ,
     instance _ : Positive b
     _ = positive $ begin-strict
       0ℚ                               ≤⟨ 0≤∣p∣ (lookup (sequence x) B) ⟩
-      ∣ lookup (sequence x) B ∣        ≡˘⟨ +-identityˡ ∣ lookup (sequence x) B ∣ ⟩
+      ∣ lookup (sequence x) B ∣        ≡⟨ +-identityˡ ∣ lookup (sequence x) B ∣ ⟨
       0ℚ ℚ.+ ∣ lookup (sequence x) B ∣ <⟨ +-monoˡ-< ∣ lookup (sequence x) B ∣ {0ℚ} {1ℚ} (*<* (+<+ (s≤s z≤n))) ⟩
       1ℚ ℚ.+ ∣ lookup (sequence x) B ∣ ≡⟨⟩
       b                                ∎
@@ -179,11 +203,16 @@ isCauchy (square x) ε = B ℕ.⊔ proj₁ (isCauchy x (1/ (b ℚ.+ b) * ε)) ,
 
     b-prop : ∀ {n} → n ℕ.≥ B → ∣ lookup (sequence x) n ∣ < b
     b-prop {n} n≥B = begin-strict
-     ∣ lookup (sequence x) n ∣ ≡˘⟨ cong ∣_∣ (+-identityʳ (lookup (sequence x) n)) ⟩
-     ∣ lookup (sequence x) n ℚ.+ 0ℚ ∣ ≡˘⟨ cong (λ # → ∣ lookup (sequence x) n ℚ.+ # ∣) (+-inverseˡ (lookup (sequence x) B)) ⟩
-     ∣ lookup (sequence x) n ℚ.+ (ℚ.- lookup (sequence x) B ℚ.+ lookup (sequence x) B) ∣ ≡˘⟨ cong ∣_∣ (+-assoc (lookup (sequence x) n) (ℚ.- lookup (sequence x) B) (lookup (sequence x) B)) ⟩
-     ∣ (lookup (sequence x) n - lookup (sequence x) B) ℚ.+ lookup (sequence x) B ∣ ≤⟨ ∣p+q∣≤∣p∣+∣q∣ (lookup (sequence x) n - lookup (sequence x) B) (lookup (sequence x) B) ⟩
-     ∣ lookup (sequence x) n - lookup (sequence x) B ∣ ℚ.+ ∣ lookup (sequence x) B ∣ <⟨ +-monoˡ-< ∣ lookup (sequence x) B ∣ (proj₂ (isCauchy x 1ℚ) n≥B ℕ.≤-refl) ⟩
+     ∣ lookup (sequence x) n ∣
+       ≡⟨ cong ∣_∣ (+-identityʳ (lookup (sequence x) n)) ⟨
+     ∣ lookup (sequence x) n ℚ.+ 0ℚ ∣
+       ≡⟨ cong (λ # → ∣ lookup (sequence x) n ℚ.+ # ∣) (+-inverseˡ (lookup (sequence x) B)) ⟨
+     ∣ lookup (sequence x) n ℚ.+ (ℚ.- lookup (sequence x) B ℚ.+ lookup (sequence x) B) ∣
+       ≡⟨ cong ∣_∣ (+-assoc (lookup (sequence x) n) (ℚ.- lookup (sequence x) B) (lookup (sequence x) B)) ⟨
+     ∣ (lookup (sequence x) n - lookup (sequence x) B) ℚ.+ lookup (sequence x) B ∣
+       ≤⟨ ∣p+q∣≤∣p∣+∣q∣ (lookup (sequence x) n - lookup (sequence x) B) (lookup (sequence x) B) ⟩
+     ∣ lookup (sequence 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 ∎
 

From 3b796db4024f21dfe41f028d8105f43a23961210 Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Sat, 28 Sep 2024 11:26:41 +0200
Subject: [PATCH 13/16] Add some algebraic properties of pointwise relations on
 streams

---
 .../Stream/Relation/Binary/Pointwise.agda     | 39 ++++++++++++++++++-
 1 file changed, 38 insertions(+), 1 deletion(-)

diff --git a/src/Codata/Guarded/Stream/Relation/Binary/Pointwise.agda b/src/Codata/Guarded/Stream/Relation/Binary/Pointwise.agda
index 0ba8d9539c..6448881947 100644
--- a/src/Codata/Guarded/Stream/Relation/Binary/Pointwise.agda
+++ b/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
 

From e2ef3fb15ca0d71086d9b82ce2c928de65d23e41 Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Sat, 28 Sep 2024 11:26:54 +0200
Subject: [PATCH 14/16] Simplify and continue algebraic properties of reals

---
 src/Data/Real/Base.agda       |  3 +++
 src/Data/Real/Properties.agda | 34 ++++++++++++----------------------
 2 files changed, 15 insertions(+), 22 deletions(-)

diff --git a/src/Data/Real/Base.agda b/src/Data/Real/Base.agda
index bb8c37968a..bdef196ac4 100644
--- a/src/Data/Real/Base.agda
+++ b/src/Data/Real/Base.agda
@@ -27,6 +27,9 @@ open import Function.Metric.Rational.CauchySequence d-metric public renaming (Ca
 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
diff --git a/src/Data/Real/Properties.agda b/src/Data/Real/Properties.agda
index 79cce497e9..66e6abda91 100644
--- a/src/Data/Real/Properties.agda
+++ b/src/Data/Real/Properties.agda
@@ -13,6 +13,7 @@ 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
 import Data.Integer.Base as ℤ
 import Data.Nat.Base as ℕ
@@ -53,19 +54,7 @@ open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; cong
 +-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 ∣
-    ≡⟨ cong₂ (λ a b → ℚ.∣ a ℚ.- b ∣)
-      (lookup-zipWith n ℚ._+_ (zipWith ℚ._+_ (sequence x) (sequence y)) (sequence z))
-      (lookup-zipWith n ℚ._+_ (sequence x) (zipWith ℚ._+_ (sequence y) (sequence z))) ⟩
-  ℚ.∣ (lookup (zipWith ℚ._+_ (sequence x) (sequence y)) n ℚ.+ lookup (sequence z) n) ℚ.- (lookup (sequence x) n ℚ.+ lookup (zipWith ℚ._+_ (sequence y) (sequence z)) n) ∣
-    ≡⟨ cong₂ (λ a b → ℚ.∣ (a ℚ.+ lookup (sequence z) n) ℚ.- (lookup (sequence x) n ℚ.+ b) ∣)
-      (lookup-zipWith n ℚ._+_ (sequence x) (sequence y))
-      (lookup-zipWith n ℚ._+_ (sequence y) (sequence z)) ⟩
-  ℚ.∣ ((lookup (sequence x) n ℚ.+ lookup (sequence y) n) ℚ.+ lookup (sequence z) n) ℚ.- (lookup (sequence x) n ℚ.+ (lookup (sequence y) n ℚ.+ lookup (sequence z) n)) ∣
-    ≡⟨ cong (λ a → ℚ.∣ a ℚ.- (lookup (sequence x) n ℚ.+ (lookup (sequence y) n ℚ.+ lookup (sequence z) n)) ∣) (ℚ.+-assoc (lookup (sequence x) n) (lookup (sequence y) n) (lookup (sequence z) n)) ⟩
-  ℚ.∣ (lookup (sequence x) n ℚ.+ (lookup (sequence y) n ℚ.+ lookup (sequence z) n)) ℚ.- (lookup (sequence x) n ℚ.+ (lookup (sequence y) n ℚ.+ lookup (sequence z) n)) ∣
-    ≡⟨ cong ℚ.∣_∣ (ℚ.+-inverseʳ (lookup (sequence x) n ℚ.+ (lookup (sequence y) n ℚ.+ lookup (sequence z) n))) ⟩
-  ℚ.∣ ℚ.0ℚ ∣
-    ≡⟨⟩
+    ≡⟨ ℚ.d-definite (cong-lookup (PW.assoc ℚ.+-assoc (sequence x) (sequence y) (sequence z)) n) ⟩
   ℚ.0ℚ
     <⟨ ℚ.positive⁻¹ ε ⟩
   ε ∎
@@ -74,15 +63,16 @@ open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; cong
 +-comm : Commutative _+_
 +-comm x y ε = 0 , λ {n} _ → begin-strict
   ℚ.∣ lookup (zipWith ℚ._+_ (sequence x) (sequence y)) n ℚ.- lookup (zipWith ℚ._+_ (sequence y) (sequence x)) n ∣
-    ≡⟨ cong₂ (λ a b → ℚ.∣ a ℚ.- b ∣)
-      (lookup-zipWith n ℚ._+_ (sequence x) (sequence y))
-      (lookup-zipWith n ℚ._+_ (sequence y) (sequence x)) ⟩
-  ℚ.∣ (lookup (sequence x) n ℚ.+ lookup (sequence y) n) ℚ.- (lookup (sequence y) n ℚ.+ lookup (sequence x) n) ∣
-    ≡⟨ cong (λ a → ℚ.∣ a ℚ.- (lookup (sequence y) n ℚ.+ lookup (sequence x) n) ∣) (ℚ.+-comm (lookup (sequence x) n) (lookup (sequence y) n)) ⟩
-  ℚ.∣ (lookup (sequence y) n ℚ.+ lookup (sequence x) n) ℚ.- (lookup (sequence y) n ℚ.+ lookup (sequence x) n) ∣
-    ≡⟨ cong ℚ.∣_∣ (ℚ.+-inverseʳ (lookup (sequence y) n ℚ.+ lookup (sequence x) n)) ⟩
-  ℚ.∣ ℚ.0ℚ ∣
-    ≡⟨⟩
+    ≡⟨ ℚ.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 ℚ.- lookup (sequence x) n ∣
+    ≡⟨ ℚ.d-definite (cong-lookup (PW.identityˡ ℚ.+-identityˡ (sequence x)) n) ⟩
   ℚ.0ℚ
     <⟨ ℚ.positive⁻¹ ε ⟩
   ε ∎

From a14f5fd577d8875ddb4b726e337b15efb1af39f9 Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Sat, 28 Sep 2024 17:31:04 +0200
Subject: [PATCH 15/16] Use new properties to simplify Real

---
 src/Data/Real/Base.agda | 12 ++----------
 1 file changed, 2 insertions(+), 10 deletions(-)

diff --git a/src/Data/Real/Base.agda b/src/Data/Real/Base.agda
index bdef196ac4..3774427b6b 100644
--- a/src/Data/Real/Base.agda
+++ b/src/Data/Real/Base.agda
@@ -182,21 +182,13 @@ isCauchy (square x) ε = B ℕ.⊔ proj₁ (isCauchy x (1/ (b ℚ.+ b) * ε)) ,
     b = 1ℚ ℚ.+ ∣ lookup (sequence x) B ∣
 
     instance _ : Positive b
-    _ = positive $ begin-strict
-      0ℚ                               ≤⟨ 0≤∣p∣ (lookup (sequence x) B) ⟩
-      ∣ lookup (sequence x) B ∣        ≡⟨ +-identityˡ ∣ lookup (sequence x) B ∣ ⟨
-      0ℚ ℚ.+ ∣ lookup (sequence x) B ∣ <⟨ +-monoˡ-< ∣ lookup (sequence x) B ∣ {0ℚ} {1ℚ} (*<* (+<+ (s≤s z≤n))) ⟩
-      1ℚ ℚ.+ ∣ lookup (sequence x) B ∣ ≡⟨⟩
-      b                                ∎
+    _ = pos+nonNeg⇒pos 1ℚ ∣ lookup (sequence x) B ∣ {{∣-∣-nonNeg (lookup (sequence x) B)}}
 
     instance _ : NonZero b
     _ = pos⇒nonZero b
 
     instance _ : Positive (b ℚ.+ b)
-    _ = positive $ begin-strict
-      0ℚ        ≡⟨⟩
-      0ℚ ℚ.+ 0ℚ <⟨ +-mono-< (positive⁻¹ b) (positive⁻¹ b) ⟩
-      b ℚ.+ b   ∎
+    _ = pos+pos⇒pos b b
 
     instance _ : NonZero (b ℚ.+ b)
     _ = pos⇒nonZero (b ℚ.+ b)

From 84270bb504925d14277920243066dc9b555b0743 Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Sat, 28 Sep 2024 17:41:54 +0200
Subject: [PATCH 16/16] Don't know what this line was doing over there

---
 src/Data/Real/Base.agda | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Data/Real/Base.agda b/src/Data/Real/Base.agda
index 3774427b6b..0da5045fc9 100644
--- a/src/Data/Real/Base.agda
+++ b/src/Data/Real/Base.agda
@@ -113,7 +113,8 @@ isCauchy (p *ₗ x) ε with p ≟ 0ℚ
 ... | 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 * lookup (sequence x) n ∣                   ≡⟨ cong (λ # → ∣ p * lookup (sequence x) m ℚ.+ # ∣) (neg-distribʳ-* p (lookup (sequence x) n)) ⟩
+  ∣ p * lookup (sequence x) m - p * lookup (sequence x) n ∣
+    ≡⟨ cong (λ # → ∣ p * lookup (sequence x) m ℚ.+ # ∣) (neg-distribʳ-* p (lookup (sequence x) n)) ⟩
   ∣ p * lookup (sequence x) m ℚ.+ p * ℚ.- lookup (sequence x) n ∣
     ≡⟨ cong ∣_∣ (*-distribˡ-+ p (lookup (sequence x) m) (ℚ.- lookup (sequence x) n)) ⟨
   ∣ p * (lookup (sequence x) m - lookup (sequence x) n) ∣