Add specialisation of metrics to rational numbers (#1471)

Author: MatthewDaggitt

CHANGELOG.md

@@ -9,6 +9,10 @@ Highlights
 Bug-fixes
 ---------
 
+* Added missing module `Function.Metric` which re-exports 
+  `Function.Metric.(Core/Definitions/Structures/Bundles)`. This module was referred
+  to in the documentation of its children but until now was not present.
+
 Non-backwards compatible changes
 --------------------------------
 
@@ -21,5 +25,13 @@ Deprecated names
 New modules
 -----------
 
+* Metrics specialised to co-domains with rational numbers:
+  ```
+  Function.Metric.Rational
+  Function.Metric.Rational.Definitions
+  Function.Metric.Rational.Structures
+  Function.Metric.Rational.Bundles
+  ```
+
 Other minor additions
 ---------------------

src/Function/Metric.agda

@@ -0,0 +1,14 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Metrics with arbitrary domains and codomains
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Function.Metric where
+
+open import Function.Metric.Core public
+open import Function.Metric.Definitions public
+open import Function.Metric.Structures public
+open import Function.Metric.Bundles public

src/Function/Metric/Rational.agda

@@ -0,0 +1,14 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Metrics with ℚ as the codomain of the metric function
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Function.Metric.Rational where
+
+open import Function.Metric.Rational.Core public
+open import Function.Metric.Rational.Definitions public
+open import Function.Metric.Rational.Structures public
+open import Function.Metric.Rational.Bundles public

src/Function/Metric/Rational/Bundles.agda

@@ -0,0 +1,134 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Bundles for metrics over ℚ
+------------------------------------------------------------------------
+
+-- Unfortunately, unlike definitions and structures, the bundles over
+-- general metric spaces cannot be reused as it is impossible to
+-- constrain the image set to ℚ.
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Data.Rational.Base hiding (_⊔_)
+open import Function using (const)
+open import Level using (Level; suc; _⊔_)
+open import Relation.Binary.Core
+open import Relation.Binary.PropositionalEquality
+  using (_≡_; isEquivalence)
+
+open import Function.Metric.Rational.Core
+open import Function.Metric.Rational.Structures
+open import Function.Metric.Bundles as Base
+  using (GeneralMetric)
+
+module Function.Metric.Rational.Bundles where
+
+------------------------------------------------------------------------
+-- Proto-metric
+
+record ProtoMetric a ℓ : Set (suc (a ⊔ ℓ)) where
+  field
+    Carrier       : Set a
+    _≈_           : Rel Carrier ℓ
+    d             : DistanceFunction Carrier
+    isProtoMetric : IsProtoMetric _≈_ d
+
+  open IsProtoMetric isProtoMetric public
+
+------------------------------------------------------------------------
+-- PreMetric
+
+record PreMetric a ℓ : Set (suc (a ⊔ ℓ)) where
+  field
+    Carrier     : Set a
+    _≈_         : Rel Carrier ℓ
+    d           : DistanceFunction Carrier
+    isPreMetric : IsPreMetric _≈_ d
+
+  open IsPreMetric isPreMetric public
+
+  protoMetric : ProtoMetric a ℓ
+  protoMetric = record
+    { isProtoMetric = isProtoMetric
+    }
+
+------------------------------------------------------------------------
+-- QuasiSemiMetric
+
+record QuasiSemiMetric a ℓ : Set (suc (a ⊔ ℓ)) where
+  field
+    Carrier           : Set a
+    _≈_               : Rel Carrier ℓ
+    d                 : DistanceFunction Carrier
+    isQuasiSemiMetric : IsQuasiSemiMetric _≈_ d
+
+  open IsQuasiSemiMetric isQuasiSemiMetric public
+
+  preMetric : PreMetric a ℓ
+  preMetric = record
+    { isPreMetric = isPreMetric
+    }
+
+  open PreMetric preMetric public
+    using (protoMetric)
+
+------------------------------------------------------------------------
+-- SemiMetric
+
+record SemiMetric a ℓ : Set (suc (a ⊔ ℓ)) where
+  field
+    Carrier      : Set a
+    _≈_          : Rel Carrier ℓ
+    d            : DistanceFunction Carrier
+    isSemiMetric : IsSemiMetric _≈_ d
+
+  open IsSemiMetric isSemiMetric public
+
+  quasiSemiMetric : QuasiSemiMetric a ℓ
+  quasiSemiMetric = record
+    { isQuasiSemiMetric = isQuasiSemiMetric
+    }
+
+  open QuasiSemiMetric quasiSemiMetric public
+    using (protoMetric; preMetric)
+
+------------------------------------------------------------------------
+-- Metrics
+
+record Metric a ℓ : Set (suc (a ⊔ ℓ)) where
+  field
+    Carrier  : Set a
+    _≈_      : Rel Carrier ℓ
+    d        : DistanceFunction Carrier
+    isMetric : IsMetric _≈_ d
+
+  open IsMetric isMetric public
+
+  semiMetric : SemiMetric a ℓ
+  semiMetric = record
+    { isSemiMetric = isSemiMetric
+    }
+
+  open SemiMetric semiMetric public
+    using (protoMetric; preMetric; quasiSemiMetric)
+
+------------------------------------------------------------------------
+-- UltraMetrics
+
+record UltraMetric a ℓ : Set (suc (a ⊔ ℓ)) where
+  field
+    Carrier       : Set a
+    _≈_           : Rel Carrier ℓ
+    d             : DistanceFunction Carrier
+    isUltraMetric : IsUltraMetric _≈_ d
+
+  open IsUltraMetric isUltraMetric public
+
+  semiMetric : SemiMetric a ℓ
+  semiMetric = record
+    { isSemiMetric = isSemiMetric
+    }
+
+  open SemiMetric semiMetric public
+    using (protoMetric; preMetric; quasiSemiMetric)

src/Function/Metric/Rational/Core.agda

@@ -0,0 +1,18 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Core definitions for metrics over ℕ
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Data.Rational.Base using (ℚ)
+import Function.Metric.Core as Base
+
+module Function.Metric.Rational.Core where
+
+------------------------------------------------------------------------
+-- Definition
+
+DistanceFunction : ∀ {a} → Set a → Set a
+DistanceFunction A = Base.DistanceFunction A ℚ

src/Function/Metric/Rational/Definitions.agda

@@ -0,0 +1,68 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Core definitions for metrics over ℚ
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra.Core using (Op₂)
+open import Data.Rational.Base
+open import Level using (Level)
+open import Relation.Binary.Core
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
+
+open import Function.Metric.Rational.Core
+import Function.Metric.Definitions as Base
+
+module Function.Metric.Rational.Definitions where
+
+private
+  variable
+    a ℓ : Level
+    A   : Set a
+
+------------------------------------------------------------------------
+-- Properties
+
+-- Basic
+
+Congruent : Rel A ℓ → DistanceFunction A → Set _
+Congruent _≈ₐ_ d = Base.Congruent _≈ₐ_ _≡_ d
+
+Indiscernable : Rel A ℓ → DistanceFunction A → Set _
+Indiscernable _≈ₐ_ d = Base.Indiscernable _≈ₐ_ _≡_ d 0ℚ
+
+Definite : Rel A ℓ → DistanceFunction A → Set _
+Definite _≈ₐ_ d = Base.Definite _≈ₐ_ _≡_ d 0ℚ
+
+Symmetric : DistanceFunction A → Set _
+Symmetric = Base.Symmetric _≡_
+
+Bounded : DistanceFunction A → Set _
+Bounded = Base.Bounded _≤_
+
+TranslationInvariant : Op₂ A → DistanceFunction A → Set _
+TranslationInvariant = Base.TranslationInvariant _≡_
+
+-- Inequalities
+
+TriangleInequality : DistanceFunction A → Set _
+TriangleInequality = Base.TriangleInequality _≤_ _+_
+
+MaxTriangleInequality : DistanceFunction A → Set _
+MaxTriangleInequality = Base.TriangleInequality _≤_ _⊔_
+
+-- Contractions
+
+Contracting : (A → A) → DistanceFunction A → Set _
+Contracting = Base.Contracting _≤_
+
+ContractingOnOrbits : (A → A) → DistanceFunction A → Set _
+ContractingOnOrbits = Base.ContractingOnOrbits _≤_
+
+StrictlyContracting : Rel A ℓ → (A → A) → DistanceFunction A → Set _
+StrictlyContracting _≈_ = Base.StrictlyContracting _≈_ _<_
+
+StrictlyContractingOnOrbits : Rel A ℓ → (A → A) → DistanceFunction A → Set _
+StrictlyContractingOnOrbits _≈_ = Base.StrictlyContractingOnOrbits _≈_ _<_

src/Function/Metric/Rational/Structures.agda

@@ -0,0 +1,76 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Core definitions for metrics over ℚ
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Data.Rational.Base
+open import Function using (const)
+open import Level using (Level; suc)
+open import Relation.Binary hiding (Symmetric)
+open import Relation.Binary.PropositionalEquality using (_≡_)
+
+open import Function.Metric.Rational.Core
+open import Function.Metric.Rational.Definitions
+import Function.Metric.Structures as Base
+
+module Function.Metric.Rational.Structures where
+
+private
+  variable
+    a ℓ : Level
+    A   : Set a
+
+------------------------------------------------------------------------
+-- Proto-metrics
+
+IsProtoMetric : Rel A ℓ → DistanceFunction A → Set _
+IsProtoMetric _≈_ = Base.IsProtoMetric _≈_ _≡_ _≤_ 0ℚ
+
+open Base using (module IsProtoMetric) public
+
+------------------------------------------------------------------------
+-- Pre-metrics
+
+IsPreMetric : Rel A ℓ → DistanceFunction A → Set _
+IsPreMetric _≈_ = Base.IsPreMetric _≈_ _≡_ _≤_ 0ℚ
+
+open Base using (module IsPreMetric) public
+
+------------------------------------------------------------------------
+-- Quasi-semi-metrics
+
+IsQuasiSemiMetric : Rel A ℓ → DistanceFunction A → Set _
+IsQuasiSemiMetric _≈_ = Base.IsQuasiSemiMetric _≈_ _≡_ _≤_ 0ℚ
+
+open Base using (module IsQuasiSemiMetric) public
+
+------------------------------------------------------------------------
+-- Semi-metrics
+
+IsSemiMetric : Rel A ℓ → DistanceFunction A → Set _
+IsSemiMetric _≈_ = Base.IsSemiMetric _≈_ _≡_ _≤_ 0ℚ
+
+open Base using (module IsSemiMetric) public
+
+------------------------------------------------------------------------
+-- Metrics
+
+IsMetric : Rel A ℓ → DistanceFunction A → Set _
+IsMetric _≈_ = Base.IsGeneralMetric _≈_ _≡_ _≤_ 0ℚ _+_
+
+module IsMetric {_≈_ : Rel A ℓ} {d : DistanceFunction A}
+                (M : IsMetric _≈_ d) where
+  open Base.IsGeneralMetric M public
+
+------------------------------------------------------------------------
+-- Ultra-metrics
+
+IsUltraMetric : Rel A ℓ → DistanceFunction A → Set _
+IsUltraMetric _≈_ = Base.IsGeneralMetric _≈_ _≡_ _≤_ 0ℚ _⊔_
+
+module IsUltraMetric {_≈_ : Rel A ℓ} {d : DistanceFunction A}
+                     (UM : IsUltraMetric _≈_ d) where
+  open Base.IsGeneralMetric UM public