Skip to content

Commit 20e9d7a

Browse files
MatthewDaggittMatthewDaggitt
committed
Add metric hierarchy
1 parent 4070b9c commit 20e9d7a

File tree

11 files changed

+750
-6
lines changed

11 files changed

+750
-6
lines changed

‎CHANGELOG.md

Lines changed: 40 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,8 @@ Highlights
1212
`NonPositive`, `NonNegative`, especially designed to work as instance
1313
arguments.
1414

15+
* Metric functions and metric spaces
16+
1517
Bug-fixes
1618
---------
1719

@@ -101,6 +103,25 @@ Deprecated names
101103
New modules
102104
-----------
103105

106+
* Added a hierarchy for metric spaces:
107+
```
108+
Function.Metric
109+
Function.Metric.Core
110+
Function.Metric.Definitions
111+
Function.Metric.Structures
112+
Function.Metric.Bundles
113+
```
114+
The distance functions above are defined over an arbitrary type for the image.
115+
Specialisations to the natural numbers are provided in the following modules:
116+
```
117+
Function.Metric.Nat
118+
Function.Metric.Nat.Core
119+
Function.Metric.Nat.Definitions
120+
Function.Metric.Nat.Structures
121+
Function.Metric.Nat.Bundles
122+
```
123+
and other specialisations can be created in a similar fashion.
124+
104125
* Instance modules:
105126
```agda
106127
Category.Monad.Partiality.Instances
@@ -143,11 +164,6 @@ New modules
143164
Relation.Binary.Construct.Subst.Equality
144165
```
145166

146-
* Consequences for basic morphism properties
147-
```
148-
Algebra.Morphism.Consequences
149-
```
150-
151167
* Subtraction for binary naturals:
152168
```
153169
Data.Nat.Binary.Subtraction
@@ -194,6 +210,25 @@ New modules
194210
Data.Vec.Relation.Unary.Unique.Setoid.Properties
195211
```
196212

213+
* Added a hierarchy for metric spaces:
214+
```
215+
Function.Metric
216+
Function.Metric.Core
217+
Function.Metric.Definitions
218+
Function.Metric.Structures
219+
Function.Metric.Bundles
220+
```
221+
The distance functions above are defined over an arbitrary type for the image.
222+
Specialisations to the natural numbers are provided in the following modules:
223+
```
224+
Function.Metric.Nat
225+
Function.Metric.Nat.Core
226+
Function.Metric.Nat.Definitions
227+
Function.Metric.Nat.Structures
228+
Function.Metric.Nat.Bundles
229+
```
230+
and other specialisations can be created in a similar fashion.
231+
197232
Other major changes
198233
-------------------
199234

‎src/Data/Nat/Properties.agda

Lines changed: 79 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,7 @@ open import Data.Sum.Base as Sum
2424
open import Data.Unit using (tt)
2525
open import Function.Base
2626
open import Function.Injection using (_↣_)
27+
open import Function.Metric.Nat
2728
open import Level using (0ℓ)
2829
open import Relation.Binary
2930
open import Relation.Binary.Consequences using (flip-Connex)
@@ -1690,6 +1691,9 @@ suc[pred[n]]≡n {suc n} n≢0 = refl
16901691
-- Properties of ∣_-_∣
16911692
------------------------------------------------------------------------
16921693

1694+
------------------------------------------------------------------------
1695+
-- Basic
1696+
16931697
m≡n⇒∣m-n∣≡0 : ∀ {m n} → m ≡ n → ∣ m - n ∣ ≡ 0
16941698
m≡n⇒∣m-n∣≡0 {zero} refl = refl
16951699
m≡n⇒∣m-n∣≡0 {suc m} refl = m≡n⇒∣m-n∣≡0 {m} refl
@@ -1764,12 +1768,12 @@ private
17641768

17651769
*-distribˡ-∣-∣ : _*_ DistributesOverˡ ∣_-_∣
17661770
*-distribˡ-∣-∣ a m n with ≤-total m n
1771+
... | inj₂ n≤m = *-distribˡ-∣-∣-aux a n m n≤m
17671772
... | inj₁ m≤n = begin-equality
17681773
a * ∣ m - n ∣ ≡⟨ cong (a *_) (∣-∣-comm m n) ⟩
17691774
a * ∣ n - m ∣ ≡⟨ *-distribˡ-∣-∣-aux a m n m≤n ⟩
17701775
∣ a * n - a * m ∣ ≡⟨ ∣-∣-comm (a * n) (a * m) ⟩
17711776
∣ a * m - a * n ∣ ∎
1772-
... | inj₂ n≤m = *-distribˡ-∣-∣-aux a n m n≤m
17731777

17741778
*-distribʳ-∣-∣ : _*_ DistributesOverʳ ∣_-_∣
17751779
*-distribʳ-∣-∣ = comm+distrˡ⇒distrʳ *-comm *-distribˡ-∣-∣
@@ -1788,6 +1792,80 @@ m≤n+∣m-n∣ m n = subst (m ≤_) (cong (n +_) (∣-∣-comm n m)) (m≤n+∣
17881792
m≤∣m-n∣+n : ∀ m n → m ≤ ∣ m - n ∣ + n
17891793
m≤∣m-n∣+n m n = subst (m ≤_) (+-comm n _) (m≤n+∣m-n∣ m n)
17901794

1795+
∣-∣-triangle : TriangleInequality ∣_-_∣
1796+
∣-∣-triangle zero y z = m≤n+∣n-m∣ z y
1797+
∣-∣-triangle x zero z = begin
1798+
∣ x - z ∣ ≤⟨ ∣m-n∣≤m⊔n x z ⟩
1799+
x ⊔ z ≤⟨ m⊔n≤m+n x z ⟩
1800+
x + z ≡⟨ cong₂ _+_ (sym (∣-∣-identityʳ x)) refl ⟩
1801+
∣ x - 0 ∣ + z ∎
1802+
where open ≤-Reasoning
1803+
∣-∣-triangle x y zero = begin
1804+
∣ x - 0 ∣ ≡⟨ ∣-∣-identityʳ x ⟩
1805+
x ≤⟨ m≤∣m-n∣+n x y ⟩
1806+
∣ x - y ∣ + y ≡⟨ cong₂ _+_ refl (sym (∣-∣-identityʳ y)) ⟩
1807+
∣ x - y ∣ + ∣ y - 0 ∣ ∎
1808+
where open ≤-Reasoning
1809+
∣-∣-triangle (suc x) (suc y) (suc z) = ∣-∣-triangle x y z
1810+
1811+
------------------------------------------------------------------------
1812+
-- Metric structures
1813+
1814+
∣-∣-isProtoMetric : IsProtoMetric _≡_ ∣_-_∣
1815+
∣-∣-isProtoMetric = record
1816+
{ isPartialOrder = ≤-isPartialOrder
1817+
; ≈-isEquivalence = isEquivalence
1818+
; cong = cong₂ ∣_-_∣
1819+
; nonNegative = z≤n
1820+
}
1821+
1822+
∣-∣-isPreMetric : IsPreMetric _≡_ ∣_-_∣
1823+
∣-∣-isPreMetric = record
1824+
{ isProtoMetric = ∣-∣-isProtoMetric
1825+
; ≈⇒0 = m≡n⇒∣m-n∣≡0
1826+
}
1827+
1828+
∣-∣-isQuasiSemiMetric : IsQuasiSemiMetric _≡_ ∣_-_∣
1829+
∣-∣-isQuasiSemiMetric = record
1830+
{ isPreMetric = ∣-∣-isPreMetric
1831+
; 0⇒≈ = ∣m-n∣≡0⇒m≡n
1832+
}
1833+
1834+
∣-∣-isSemiMetric : IsSemiMetric _≡_ ∣_-_∣
1835+
∣-∣-isSemiMetric = record
1836+
{ isQuasiSemiMetric = ∣-∣-isQuasiSemiMetric
1837+
; sym = ∣-∣-comm
1838+
}
1839+
1840+
∣-∣-isMetric : IsMetric _≡_ ∣_-_∣
1841+
∣-∣-isMetric = record
1842+
{ isSemiMetric = ∣-∣-isSemiMetric
1843+
; triangle = ∣-∣-triangle
1844+
}
1845+
1846+
------------------------------------------------------------------------
1847+
-- Metric bundles
1848+
1849+
∣-∣-quasiSemiMetric : QuasiSemiMetric 0ℓ 0ℓ
1850+
∣-∣-quasiSemiMetric = record
1851+
{ isQuasiSemiMetric = ∣-∣-isQuasiSemiMetric
1852+
}
1853+
1854+
∣-∣-semiMetric : SemiMetric 0ℓ 0ℓ
1855+
∣-∣-semiMetric = record
1856+
{ isSemiMetric = ∣-∣-isSemiMetric
1857+
}
1858+
1859+
∣-∣-preMetric : PreMetric 0ℓ 0ℓ
1860+
∣-∣-preMetric = record
1861+
{ isPreMetric = ∣-∣-isPreMetric
1862+
}
1863+
1864+
∣-∣-metric : Metric 0ℓ 0ℓ
1865+
∣-∣-metric = record
1866+
{ isMetric = ∣-∣-isMetric
1867+
}
1868+
17911869
------------------------------------------------------------------------
17921870
-- Properties of ⌊_/2⌋ and ⌈_/2⌉
17931871
------------------------------------------------------------------------

‎src/Function/Metric/Bundles.agda

Lines changed: 142 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,142 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Bundles for metrics
5+
------------------------------------------------------------------------
6+
7+
-- The contents of this module should be accessed via `Function.Metric`.
8+
9+
{-# OPTIONS --without-K --safe #-}
10+
11+
module Function.Metric.Bundles where
12+
13+
open import Algebra.Core using (Op₂)
14+
open import Level using (Level; suc; _⊔_)
15+
open import Relation.Binary.Core using (Rel)
16+
17+
open import Function.Metric.Structures
18+
open import Function.Metric.Core
19+
20+
------------------------------------------------------------------------
21+
-- ProtoMetric
22+
23+
record ProtoMetric (a i ℓ₁ ℓ₂ ℓ₃ : Level)
24+
: Set (suc (a ⊔ i ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃)) where
25+
field
26+
Carrier : Set a
27+
Image : Set i
28+
_≈_ : Rel Carrier ℓ₁
29+
_≈ᵢ_ : Rel Image ℓ₂
30+
_≤_ : Rel Image ℓ₃
31+
0# : Image
32+
d : DistanceFunction Carrier Image
33+
isProtoMetric : IsProtoMetric _≈_ _≈ᵢ_ _≤_ 0# d
34+
35+
open IsProtoMetric isProtoMetric public
36+
37+
------------------------------------------------------------------------
38+
-- PreMetric
39+
40+
record PreMetric (a i ℓ₁ ℓ₂ ℓ₃ : Level)
41+
: Set (suc (a ⊔ i ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃)) where
42+
field
43+
Carrier : Set a
44+
Image : Set i
45+
_≈_ : Rel Carrier ℓ₁
46+
_≈ᵢ_ : Rel Image ℓ₂
47+
_≤_ : Rel Image ℓ₃
48+
0# : Image
49+
d : DistanceFunction Carrier Image
50+
isPreMetric : IsPreMetric _≈_ _≈ᵢ_ _≤_ 0# d
51+
52+
open IsPreMetric isPreMetric public
53+
54+
protoMetric : ProtoMetric a i ℓ₁ ℓ₂ ℓ₃
55+
protoMetric = record
56+
{ isProtoMetric = isProtoMetric
57+
}
58+
59+
------------------------------------------------------------------------
60+
-- QuasiSemiMetric
61+
62+
record QuasiSemiMetric (a i ℓ₁ ℓ₂ ℓ₃ : Level)
63+
: Set (suc (a ⊔ i ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃)) where
64+
field
65+
Carrier : Set a
66+
Image : Set i
67+
_≈_ : Rel Carrier ℓ₁
68+
_≈ᵢ_ : Rel Image ℓ₂
69+
_≤_ : Rel Image ℓ₃
70+
0# : Image
71+
d : DistanceFunction Carrier Image
72+
isQuasiSemiMetric : IsQuasiSemiMetric _≈_ _≈ᵢ_ _≤_ 0# d
73+
74+
open IsQuasiSemiMetric isQuasiSemiMetric public
75+
76+
preMetric : PreMetric a i ℓ₁ ℓ₂ ℓ₃
77+
preMetric = record
78+
{ isPreMetric = isPreMetric
79+
}
80+
81+
open PreMetric preMetric public
82+
using (protoMetric)
83+
84+
------------------------------------------------------------------------
85+
-- SemiMetric
86+
87+
record SemiMetric (a i ℓ₁ ℓ₂ ℓ₃ : Level)
88+
: Set (suc (a ⊔ i ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃)) where
89+
field
90+
Carrier : Set a
91+
Image : Set i
92+
_≈_ : Rel Carrier ℓ₁
93+
_≈ᵢ_ : Rel Image ℓ₂
94+
_≤_ : Rel Image ℓ₃
95+
0# : Image
96+
d : DistanceFunction Carrier Image
97+
isSemiMetric : IsSemiMetric _≈_ _≈ᵢ_ _≤_ 0# d
98+
99+
open IsSemiMetric isSemiMetric public
100+
101+
quasiSemiMetric : QuasiSemiMetric a i ℓ₁ ℓ₂ ℓ₃
102+
quasiSemiMetric = record
103+
{ isQuasiSemiMetric = isQuasiSemiMetric
104+
}
105+
106+
open QuasiSemiMetric quasiSemiMetric public
107+
using (protoMetric; preMetric)
108+
109+
------------------------------------------------------------------------
110+
-- GeneralMetric
111+
112+
-- Note that this package is not necessarily a metric in the classical
113+
-- sense as there is no way to ensure that the _∙_ operator really
114+
-- represents addition. See `Function.Metric.Nat` and
115+
-- `Function.Metric.Rational` for more specialised `Metric` and
116+
-- `UltraMetric` packages.
117+
118+
-- See the discussion accompanying the `IsGeneralMetric` structure for
119+
-- more details.
120+
121+
record GeneralMetric (a i ℓ₁ ℓ₂ ℓ₃ : Level)
122+
: Set (suc (a ⊔ i ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃)) where
123+
field
124+
Carrier : Set a
125+
Image : Set i
126+
_≈_ : Rel Carrier ℓ₁
127+
_≈ᵢ_ : Rel Image ℓ₂
128+
_≤_ : Rel Image ℓ₃
129+
0# : Image
130+
_∙_ : Op₂ Image
131+
d : DistanceFunction Carrier Image
132+
isGeneralMetric : IsGeneralMetric _≈_ _≈ᵢ_ _≤_ 0# _∙_ d
133+
134+
open IsGeneralMetric isGeneralMetric public
135+
136+
semiMetric : SemiMetric a i ℓ₁ ℓ₂ ℓ₃
137+
semiMetric = record
138+
{ isSemiMetric = isSemiMetric
139+
}
140+
141+
open SemiMetric semiMetric public
142+
using (protoMetric; preMetric; quasiSemiMetric)

‎src/Function/Metric/Core.agda

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Core metric definitions
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --without-K --safe #-}
8+
9+
module Function.Metric.Core where
10+
11+
open import Level using (Level)
12+
private
13+
variable
14+
a i : Level
15+
16+
------------------------------------------------------------------------
17+
-- Distance functions
18+
19+
DistanceFunction : Set a → Set i → Set _
20+
DistanceFunction A I = A → A → I

0 commit comments

Comments
 (0)