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
@@ -1340,6 +1341,34 @@ module _ where
 *-cancelˡ-≤-neg : ∀ r .{{_ : Negative r}} → r * p ≤ r * q → p ≥ q
 *-cancelˡ-≤-neg {p} {q} r rewrite *-comm r p | *-comm r q = *-cancelʳ-≤-neg r
 
+nonNeg*nonNeg⇒nonNeg : ∀ p .{{_ : NonNegative p}} q .{{_ : NonNegative q}} → NonNegative (p * q)
+nonNeg*nonNeg⇒nonNeg p q = nonNegative $ begin
+ 0ℚ ≡⟨ *-zeroʳ p ⟨
+ p * 0ℚ ≤⟨ *-monoˡ-≤-nonNeg p (nonNegative⁻¹ q) ⟩
+ p * q ∎
+ where open ≤-Reasoning
+
+nonNeg*nonPos⇒nonPos : ∀ p .{{_ : NonNegative p}} q .{{_ : NonPositive q}} → NonPositive (p * q)
+nonNeg*nonPos⇒nonPos p q = nonPositive $ begin
+ p * q ≤⟨ *-monoˡ-≤-nonNeg p (nonPositive⁻¹ q) ⟩
+ p * 0ℚ ≡⟨ *-zeroʳ p ⟩
+ 0ℚ ∎
+ where open ≤-Reasoning
+
+nonPos*nonNeg⇒nonPos : ∀ p .{{_ : NonPositive p}} q .{{_ : NonNegative q}} → NonPositive (p * q)
+nonPos*nonNeg⇒nonPos p q = nonPositive $ begin
+ p * q ≤⟨ *-monoˡ-≤-nonPos p (nonNegative⁻¹ q) ⟩
+ p * 0ℚ ≡⟨ *-zeroʳ p ⟩
+ 0ℚ ∎
+ where open ≤-Reasoning
+
+nonPos*nonPos⇒nonNeg : ∀ p .{{_ : NonPositive p}} q .{{_ : NonPositive q}} → NonNegative (p * q)
+nonPos*nonPos⇒nonNeg p q = nonNegative $ begin
+ 0ℚ ≡⟨ *-zeroʳ p ⟨
+ p * 0ℚ ≤⟨ *-monoˡ-≤-nonPos p (nonPositive⁻¹ q) ⟩
+ p * q ∎
+ where open ≤-Reasoning
+
 ------------------------------------------------------------------------
 -- Properties of _*_ and _<_
 
@@ -1387,6 +1416,34 @@ module _ where
 *-cancelʳ-<-nonPos : ∀ r .{{_ : NonPositive r}} → p * r < q * r → p > q
 *-cancelʳ-<-nonPos {p} {q} r rewrite *-comm p r | *-comm q r = *-cancelˡ-<-nonPos r
 
+pos*pos⇒pos : ∀ p .{{_ : Positive p}} q .{{_ : Positive q}} → Positive (p * q)
+pos*pos⇒pos p q = positive $ begin-strict
+ 0ℚ ≡⟨ *-zeroʳ p ⟨
+ p * 0ℚ <⟨ *-monoʳ-<-pos p (positive⁻¹ q) ⟩
+ p * q ∎
+ where open ≤-Reasoning
+
+pos*neg⇒neg : ∀ p .{{_ : Positive p}} q .{{_ : Negative q}} → Negative (p * q)
+pos*neg⇒neg p q = negative $ begin-strict
+ p * q <⟨ *-monoʳ-<-pos p (negative⁻¹ q) ⟩
+ p * 0ℚ ≡⟨ *-zeroʳ p ⟩
+ 0ℚ ∎
+ where open ≤-Reasoning
+
+neg*pos⇒neg : ∀ p .{{_ : Negative p}} q .{{_ : Positive q}} → Negative (p * q)
+neg*pos⇒neg p q = negative $ begin-strict
+ p * q <⟨ *-monoʳ-<-neg p (positive⁻¹ q) ⟩
+ p * 0ℚ ≡⟨ *-zeroʳ p ⟩
+ 0ℚ ∎
+ where open ≤-Reasoning
+
+neg*neg⇒pos : ∀ p .{{_ : Negative p}} q .{{_ : Negative q}} → Positive (p * q)
+neg*neg⇒pos p q = positive $ begin-strict
+ 0ℚ ≡⟨ *-zeroʳ p ⟨
+ p * 0ℚ <⟨ *-monoʳ-<-neg p (negative⁻¹ q) ⟩
+ p * q ∎
+ where open ≤-Reasoning
+
 ------------------------------------------------------------------------
 -- Properties of _⊓_
 ------------------------------------------------------------------------
@@ -1719,6 +1776,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