Skip to content

Commit a2da970

Browse files
MatthewDaggittMatthewDaggitt
committed
Merge branch 'master' into experimental
2 parents 63f012f + 9076c9b commit a2da970

12 files changed

+1460
-1123
lines changed

‎CHANGELOG.md

+16-1,113
Large diffs are not rendered by default.

‎CHANGELOG/v1.6.md

+1,111
Large diffs are not rendered by default.

‎README.agda

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
module README where
44

55
------------------------------------------------------------------------
6-
-- The Agda standard library, version 1.6-dev
6+
-- The Agda standard library, version 1.7
77
--
88
-- Authors: Nils Anders Danielsson, Matthew Daggitt, Guillaume Allais
99
-- with contributions from Andreas Abel, Stevan Andjelkovic,

‎agda-stdlib-utils.cabal

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
name: agda-stdlib-utils
2-
version: 1.6-dev
2+
version: 1.7
33
cabal-version: >= 1.10
44
build-type: Simple
55
description: Helper programs.

‎notes/installation-guide.md

+6-6
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,19 @@
11
Installation instructions
22
=========================
33

4-
Use version v1.5 of the standard library with Agda 2.6.1 and 2.6.1.1.
4+
Use version v1.6 of the standard library with Agda 2.6.1 and 2.6.1.1.
55

66
1. Navigate to a suitable directory `$HERE` (replace appropriately) where
77
you would like to install the library.
88

9-
2. Download the tarball of v1.5 of the standard library. This can either be
9+
2. Download the tarball of v1.6 of the standard library. This can either be
1010
done manually by visiting the Github repository for the library, or via the
1111
command line as follows:
1212
```
13-
wget -O agda-stdlib.tar https://github.com/agda/agda-stdlib/archive/v1.5.tar.gz
13+
wget -O agda-stdlib.tar https://github.com/agda/agda-stdlib/archive/v1.6.tar.gz
1414
```
1515
Note that you can replace `wget` with other popular tools such as `curl` and that
16-
you can replace `1.5` with any other version of the library you desire.
16+
you can replace `1.6` with any other version of the library you desire.
1717

1818
3. Extract the standard library from the tarball. Again this can either be
1919
done manually or via the command line as follows:
@@ -24,14 +24,14 @@ Use version v1.5 of the standard library with Agda 2.6.1 and 2.6.1.1.
2424
4. [ OPTIONAL ] If using [cabal](https://www.haskell.org/cabal/) then run
2525
the commands to install via cabal:
2626
```
27-
cd agda-stdlib-1.5
27+
cd agda-stdlib-1.6
2828
cabal install
2929
```
3030

3131
5. Register the standard library with Agda's package system by adding
3232
the following line to `$HOME/.agda/libraries`:
3333
```
34-
$HERE/agda-stdlib-1.5/standard-library.agda-lib
34+
$HERE/agda-stdlib-1.6/standard-library.agda-lib
3535
```
3636

3737
Now, the standard library is ready to be used either:

‎src/Data/Nat/Properties.agda

+1-2
Original file line numberDiff line numberDiff line change
@@ -418,8 +418,7 @@ m<n⇒n≢0 : ∀ {m n} → m < n → n ≢ 0
418418
m<n⇒n≢0 (s≤s m≤n) ()
419419

420420
m<n⇒m≤1+n : ∀ {m n} → m < n → m ≤ suc n
421-
m<n⇒m≤1+n (s≤s z≤n) = z≤n
422-
m<n⇒m≤1+n (s≤s (s≤s m<n)) = s≤s (m<n⇒m≤1+n (s≤s m<n))
421+
m<n⇒m≤1+n = ≤-step ∘ <⇒≤
423422

424423
∀[m≤n⇒m≢o]⇒n<o : ∀ n o → (∀ {m} → m ≤ n → m ≢ o) → n < o
425424
∀[m≤n⇒m≢o]⇒n<o _ zero m≤n⇒n≢0 = contradiction refl (m≤n⇒n≢0 z≤n)

‎src/Function/Metric.agda

+14
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Metrics with arbitrary domains and codomains
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --without-K --safe #-}
8+
9+
module Function.Metric where
10+
11+
open import Function.Metric.Core public
12+
open import Function.Metric.Definitions public
13+
open import Function.Metric.Structures public
14+
open import Function.Metric.Bundles public

‎src/Function/Metric/Rational.agda

+14
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Metrics with ℚ as the codomain of the metric function
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --without-K --safe #-}
8+
9+
module Function.Metric.Rational where
10+
11+
open import Function.Metric.Rational.Core public
12+
open import Function.Metric.Rational.Definitions public
13+
open import Function.Metric.Rational.Structures public
14+
open import Function.Metric.Rational.Bundles public

‎src/Function/Metric/Rational/Bundles.agda

+134
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,134 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Bundles for metrics over ℚ
5+
------------------------------------------------------------------------
6+
7+
-- Unfortunately, unlike definitions and structures, the bundles over
8+
-- general metric spaces cannot be reused as it is impossible to
9+
-- constrain the image set to ℚ.
10+
11+
{-# OPTIONS --without-K --safe #-}
12+
13+
open import Data.Rational.Base hiding (_⊔_)
14+
open import Function using (const)
15+
open import Level using (Level; suc; _⊔_)
16+
open import Relation.Binary.Core
17+
open import Relation.Binary.PropositionalEquality
18+
using (_≡_; isEquivalence)
19+
20+
open import Function.Metric.Rational.Core
21+
open import Function.Metric.Rational.Structures
22+
open import Function.Metric.Bundles as Base
23+
using (GeneralMetric)
24+
25+
module Function.Metric.Rational.Bundles where
26+
27+
------------------------------------------------------------------------
28+
-- Proto-metric
29+
30+
record ProtoMetric a ℓ : Set (suc (a ⊔ ℓ)) where
31+
field
32+
Carrier : Set a
33+
_≈_ : Rel Carrier ℓ
34+
d : DistanceFunction Carrier
35+
isProtoMetric : IsProtoMetric _≈_ d
36+
37+
open IsProtoMetric isProtoMetric public
38+
39+
------------------------------------------------------------------------
40+
-- PreMetric
41+
42+
record PreMetric a ℓ : Set (suc (a ⊔ ℓ)) where
43+
field
44+
Carrier : Set a
45+
_≈_ : Rel Carrier ℓ
46+
d : DistanceFunction Carrier
47+
isPreMetric : IsPreMetric _≈_ d
48+
49+
open IsPreMetric isPreMetric public
50+
51+
protoMetric : ProtoMetric a ℓ
52+
protoMetric = record
53+
{ isProtoMetric = isProtoMetric
54+
}
55+
56+
------------------------------------------------------------------------
57+
-- QuasiSemiMetric
58+
59+
record QuasiSemiMetric a ℓ : Set (suc (a ⊔ ℓ)) where
60+
field
61+
Carrier : Set a
62+
_≈_ : Rel Carrier ℓ
63+
d : DistanceFunction Carrier
64+
isQuasiSemiMetric : IsQuasiSemiMetric _≈_ d
65+
66+
open IsQuasiSemiMetric isQuasiSemiMetric public
67+
68+
preMetric : PreMetric a ℓ
69+
preMetric = record
70+
{ isPreMetric = isPreMetric
71+
}
72+
73+
open PreMetric preMetric public
74+
using (protoMetric)
75+
76+
------------------------------------------------------------------------
77+
-- SemiMetric
78+
79+
record SemiMetric a ℓ : Set (suc (a ⊔ ℓ)) where
80+
field
81+
Carrier : Set a
82+
_≈_ : Rel Carrier ℓ
83+
d : DistanceFunction Carrier
84+
isSemiMetric : IsSemiMetric _≈_ d
85+
86+
open IsSemiMetric isSemiMetric public
87+
88+
quasiSemiMetric : QuasiSemiMetric a ℓ
89+
quasiSemiMetric = record
90+
{ isQuasiSemiMetric = isQuasiSemiMetric
91+
}
92+
93+
open QuasiSemiMetric quasiSemiMetric public
94+
using (protoMetric; preMetric)
95+
96+
------------------------------------------------------------------------
97+
-- Metrics
98+
99+
record Metric a ℓ : Set (suc (a ⊔ ℓ)) where
100+
field
101+
Carrier : Set a
102+
_≈_ : Rel Carrier ℓ
103+
d : DistanceFunction Carrier
104+
isMetric : IsMetric _≈_ d
105+
106+
open IsMetric isMetric public
107+
108+
semiMetric : SemiMetric a ℓ
109+
semiMetric = record
110+
{ isSemiMetric = isSemiMetric
111+
}
112+
113+
open SemiMetric semiMetric public
114+
using (protoMetric; preMetric; quasiSemiMetric)
115+
116+
------------------------------------------------------------------------
117+
-- UltraMetrics
118+
119+
record UltraMetric a ℓ : Set (suc (a ⊔ ℓ)) where
120+
field
121+
Carrier : Set a
122+
_≈_ : Rel Carrier ℓ
123+
d : DistanceFunction Carrier
124+
isUltraMetric : IsUltraMetric _≈_ d
125+
126+
open IsUltraMetric isUltraMetric public
127+
128+
semiMetric : SemiMetric a ℓ
129+
semiMetric = record
130+
{ isSemiMetric = isSemiMetric
131+
}
132+
133+
open SemiMetric semiMetric public
134+
using (protoMetric; preMetric; quasiSemiMetric)

‎src/Function/Metric/Rational/Core.agda

+18
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Core definitions for metrics over ℕ
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --without-K --safe #-}
8+
9+
open import Data.Rational.Base using (ℚ)
10+
import Function.Metric.Core as Base
11+
12+
module Function.Metric.Rational.Core where
13+
14+
------------------------------------------------------------------------
15+
-- Definition
16+
17+
DistanceFunction : ∀ {a} → Set a → Set a
18+
DistanceFunction A = Base.DistanceFunction A ℚ

‎src/Function/Metric/Rational/Definitions.agda

+68
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,68 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Core definitions for metrics over ℚ
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --without-K --safe #-}
8+
9+
open import Algebra.Core using (Op₂)
10+
open import Data.Rational.Base
11+
open import Level using (Level)
12+
open import Relation.Binary.Core
13+
open import Relation.Binary.PropositionalEquality.Core using (_≡_)
14+
15+
open import Function.Metric.Rational.Core
16+
import Function.Metric.Definitions as Base
17+
18+
module Function.Metric.Rational.Definitions where
19+
20+
private
21+
variable
22+
a ℓ : Level
23+
A : Set a
24+
25+
------------------------------------------------------------------------
26+
-- Properties
27+
28+
-- Basic
29+
30+
Congruent : Rel A ℓ → DistanceFunction A → Set _
31+
Congruent _≈ₐ_ d = Base.Congruent _≈ₐ_ _≡_ d
32+
33+
Indiscernable : Rel A ℓ → DistanceFunction A → Set _
34+
Indiscernable _≈ₐ_ d = Base.Indiscernable _≈ₐ_ _≡_ d 0ℚ
35+
36+
Definite : Rel A ℓ → DistanceFunction A → Set _
37+
Definite _≈ₐ_ d = Base.Definite _≈ₐ_ _≡_ d 0ℚ
38+
39+
Symmetric : DistanceFunction A → Set _
40+
Symmetric = Base.Symmetric _≡_
41+
42+
Bounded : DistanceFunction A → Set _
43+
Bounded = Base.Bounded _≤_
44+
45+
TranslationInvariant : Op₂ A → DistanceFunction A → Set _
46+
TranslationInvariant = Base.TranslationInvariant _≡_
47+
48+
-- Inequalities
49+
50+
TriangleInequality : DistanceFunction A → Set _
51+
TriangleInequality = Base.TriangleInequality _≤_ _+_
52+
53+
MaxTriangleInequality : DistanceFunction A → Set _
54+
MaxTriangleInequality = Base.TriangleInequality _≤_ _⊔_
55+
56+
-- Contractions
57+
58+
Contracting : (A → A) → DistanceFunction A → Set _
59+
Contracting = Base.Contracting _≤_
60+
61+
ContractingOnOrbits : (A → A) → DistanceFunction A → Set _
62+
ContractingOnOrbits = Base.ContractingOnOrbits _≤_
63+
64+
StrictlyContracting : Rel A ℓ → (A → A) → DistanceFunction A → Set _
65+
StrictlyContracting _≈_ = Base.StrictlyContracting _≈_ _<_
66+
67+
StrictlyContractingOnOrbits : Rel A ℓ → (A → A) → DistanceFunction A → Set _
68+
StrictlyContractingOnOrbits _≈_ = Base.StrictlyContractingOnOrbits _≈_ _<_

‎src/Function/Metric/Rational/Structures.agda

+76
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,76 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Core definitions for metrics over ℚ
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --without-K --safe #-}
8+
9+
open import Data.Rational.Base
10+
open import Function using (const)
11+
open import Level using (Level; suc)
12+
open import Relation.Binary hiding (Symmetric)
13+
open import Relation.Binary.PropositionalEquality using (_≡_)
14+
15+
open import Function.Metric.Rational.Core
16+
open import Function.Metric.Rational.Definitions
17+
import Function.Metric.Structures as Base
18+
19+
module Function.Metric.Rational.Structures where
20+
21+
private
22+
variable
23+
a ℓ : Level
24+
A : Set a
25+
26+
------------------------------------------------------------------------
27+
-- Proto-metrics
28+
29+
IsProtoMetric : Rel A ℓ → DistanceFunction A → Set _
30+
IsProtoMetric _≈_ = Base.IsProtoMetric _≈_ _≡_ _≤_ 0ℚ
31+
32+
open Base using (module IsProtoMetric) public
33+
34+
------------------------------------------------------------------------
35+
-- Pre-metrics
36+
37+
IsPreMetric : Rel A ℓ → DistanceFunction A → Set _
38+
IsPreMetric _≈_ = Base.IsPreMetric _≈_ _≡_ _≤_ 0ℚ
39+
40+
open Base using (module IsPreMetric) public
41+
42+
------------------------------------------------------------------------
43+
-- Quasi-semi-metrics
44+
45+
IsQuasiSemiMetric : Rel A ℓ → DistanceFunction A → Set _
46+
IsQuasiSemiMetric _≈_ = Base.IsQuasiSemiMetric _≈_ _≡_ _≤_ 0ℚ
47+
48+
open Base using (module IsQuasiSemiMetric) public
49+
50+
------------------------------------------------------------------------
51+
-- Semi-metrics
52+
53+
IsSemiMetric : Rel A ℓ → DistanceFunction A → Set _
54+
IsSemiMetric _≈_ = Base.IsSemiMetric _≈_ _≡_ _≤_ 0ℚ
55+
56+
open Base using (module IsSemiMetric) public
57+
58+
------------------------------------------------------------------------
59+
-- Metrics
60+
61+
IsMetric : Rel A ℓ → DistanceFunction A → Set _
62+
IsMetric _≈_ = Base.IsGeneralMetric _≈_ _≡_ _≤_ 0ℚ _+_
63+
64+
module IsMetric {_≈_ : Rel A ℓ} {d : DistanceFunction A}
65+
(M : IsMetric _≈_ d) where
66+
open Base.IsGeneralMetric M public
67+
68+
------------------------------------------------------------------------
69+
-- Ultra-metrics
70+
71+
IsUltraMetric : Rel A ℓ → DistanceFunction A → Set _
72+
IsUltraMetric _≈_ = Base.IsGeneralMetric _≈_ _≡_ _≤_ 0ℚ _⊔_
73+
74+
module IsUltraMetric {_≈_ : Rel A ℓ} {d : DistanceFunction A}
75+
(UM : IsUltraMetric _≈_ d) where
76+
open Base.IsGeneralMetric UM public

0 commit comments

Comments
 (0)