From 0f86c1c4224f8fd60a14197b6b568db57a096de1 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] 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⁻¹ ε ⟩
   ε ∎