Skip to content

Commit 4cbd95e

Browse files
sstuckisstucki
committed
[ fix #1694 ] Add ordered algebraic structures.
1 parent 650e05f commit 4cbd95e

File tree

9 files changed

+547
-3
lines changed

9 files changed

+547
-3
lines changed

‎CHANGELOG.md

Lines changed: 17 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -800,6 +800,14 @@ New modules
800800
Algebra.Morphism.Construct.Identity
801801
```
802802

803+
* Ordered algebraic structures (pomonoids, posemigroups, etc.)
804+
```
805+
Algebra.Ordered
806+
Algebra.Ordered.Bundles
807+
Algebra.Ordered.Definitions
808+
Algebra.Ordered.Structures
809+
```
810+
803811
* 'Optimised' tail-recursive exponentiation properties:
804812
```
805813
Algebra.Properties.Semiring.Exp.TailRecursiveOptimised
@@ -1549,10 +1557,18 @@ Other minor changes
15491557

15501558
* Added new proofs to `Relation.Binary.Lattice.Properties.{Join,Meet}Semilattice`:
15511559
```agda
1560+
isPosemigroup : IsPosemigroup _≈_ _≤_ _∨_
1561+
posemigroup : Posemigroup c ℓ₁ ℓ₂
15521562
≈-dec⇒≤-dec : Decidable _≈_ → Decidable _≤_
15531563
≈-dec⇒isDecPartialOrder : Decidable _≈_ → IsDecPartialOrder _≈_ _≤_
15541564
```
15551565

1566+
* Added new proofs to `Relation.Binary.Lattice.Properties.Bounded{Join,Meet}Semilattice`:
1567+
```agda
1568+
isCommutativePomonoid : IsCommutativePomonoid _≈_ _≤_ _∨_ ⊥
1569+
commutativePomonoid : CommutativePomonoid c ℓ₁ ℓ₂
1570+
```
1571+
15561572
* Added new proofs to `Relation.Binary.Properties.Poset`:
15571573
```agda
15581574
≤-dec⇒≈-dec : Decidable _≤_ → Decidable _≈_
@@ -1945,4 +1961,4 @@ This is a full list of proofs that have changed form to use irrelevant instance
19451961
```agda
19461962
Inverse⇒Injection : Inverse S T → Injection S T
19471963
↔⇒↣ : A ↔ B → A ↣ B
1948-
```
1964+
```

‎src/Algebra/Ordered.agda

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Definitions of ordered algebraic structures like promonoids and
5+
-- posemigroups (packed in records together with sets, orders,
6+
-- operations, etc.)
7+
------------------------------------------------------------------------
8+
9+
{-# OPTIONS --without-K --safe #-}
10+
11+
module Algebra.Ordered where
12+
13+
open import Algebra.Ordered.Definitions public
14+
open import Algebra.Ordered.Structures public
15+
open import Algebra.Ordered.Bundles public

‎src/Algebra/Ordered/Bundles.agda

Lines changed: 223 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,223 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Definitions of ordered algebraic structures like promonoids and
5+
-- posemigroups (packed in records together with sets, orders,
6+
-- operations, etc.)
7+
------------------------------------------------------------------------
8+
9+
-- The contents of this module should be accessed via `Algebra.Order`.
10+
11+
{-# OPTIONS --without-K --safe #-}
12+
13+
module Algebra.Ordered.Bundles where
14+
15+
open import Algebra.Core
16+
open import Algebra.Bundles
17+
open import Algebra.Ordered.Structures
18+
open import Level using (suc; _⊔_)
19+
open import Relation.Binary using (Rel)
20+
open import Relation.Binary.Bundles using (Preorder; Poset)
21+
22+
------------------------------------------------------------------------
23+
-- Bundles of preordered structures
24+
25+
-- Preordered semigroups (prosemigroups)
26+
27+
record Prosemigroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
28+
infix 4 _≈_ _∼_
29+
infixl 7 _∙_
30+
field
31+
Carrier : Set c
32+
_≈_ : Rel Carrier ℓ₁ -- The underlying equality.
33+
_∼_ : Rel Carrier ℓ₂ -- The preorder.
34+
_∙_ : Op₂ Carrier -- Multiplication.
35+
isProsemigroup : IsProsemigroup _≈_ _∼_ _∙_
36+
37+
open IsProsemigroup isProsemigroup public
38+
39+
preorder : Preorder c ℓ₁ ℓ₂
40+
preorder = record { isPreorder = isPreorder }
41+
42+
semigroup : Semigroup c ℓ₁
43+
semigroup = record { isSemigroup = isSemigroup }
44+
45+
open Semigroup semigroup public using (magma)
46+
47+
-- Preordered monoids (promonoids)
48+
49+
record Promonoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
50+
infix 4 _≈_ _∼_
51+
infixl 7 _∙_
52+
field
53+
Carrier : Set c
54+
_≈_ : Rel Carrier ℓ₁ -- The underlying equality.
55+
_∼_ : Rel Carrier ℓ₂ -- The preorder.
56+
_∙_ : Op₂ Carrier -- The monoid multiplication.
57+
ε : Carrier -- The monoid unit.
58+
isPromonoid : IsPromonoid _≈_ _∼_ _∙_ ε
59+
60+
open IsPromonoid isPromonoid public
61+
62+
prosemigroup : Prosemigroup c ℓ₁ ℓ₂
63+
prosemigroup = record { isProsemigroup = isProsemigroup }
64+
65+
open Prosemigroup prosemigroup public using (preorder; magma; semigroup)
66+
67+
monoid : Monoid c ℓ₁
68+
monoid = record { isMonoid = isMonoid }
69+
70+
record CommutativePromonoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
71+
infix 4 _≈_ _∼_
72+
infixl 7 _∙_
73+
field
74+
Carrier : Set c
75+
_≈_ : Rel Carrier ℓ₁ -- The underlying equality.
76+
_∼_ : Rel Carrier ℓ₂ -- The preorder.
77+
_∙_ : Op₂ Carrier -- The monoid multiplication.
78+
ε : Carrier -- The monoid unit.
79+
isCommutativePromonoid : IsCommutativePromonoid _≈_ _∼_ _∙_ ε
80+
81+
open IsCommutativePromonoid isCommutativePromonoid public
82+
83+
promonoid : Promonoid c ℓ₁ ℓ₂
84+
promonoid = record { isPromonoid = isPromonoid }
85+
86+
open Promonoid promonoid public
87+
using (preorder; magma; semigroup; monoid)
88+
89+
commutativeMonoid : CommutativeMonoid c ℓ₁
90+
commutativeMonoid = record { isCommutativeMonoid = isCommutativeMonoid }
91+
92+
record Prosemiring c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
93+
infix 4 _≈_ _∼_
94+
infixl 7 _*_
95+
infixl 6 _+_
96+
field
97+
Carrier : Set c
98+
_≈_ : Rel Carrier ℓ₁
99+
_∼_ : Rel Carrier ℓ₂
100+
_+_ : Op₂ Carrier
101+
_*_ : Op₂ Carrier
102+
0# : Carrier
103+
1# : Carrier
104+
isProsemiring : IsProsemiring _≈_ _∼_ _+_ _*_ 0# 1#
105+
106+
open IsProsemiring isProsemiring public
107+
108+
+-commutativePromonoid : CommutativePromonoid c ℓ₁ ℓ₂
109+
+-commutativePromonoid = record
110+
{ isCommutativePromonoid = +-isCommutativePromonoid }
111+
112+
open CommutativePromonoid +-commutativePromonoid public
113+
using (preorder)
114+
renaming
115+
( magma to +-magma
116+
; semigroup to +-semigroup
117+
; monoid to +-monoid
118+
)
119+
120+
*-promonoid : Promonoid c ℓ₁ ℓ₂
121+
*-promonoid = record { isPromonoid = *-isPromonoid }
122+
123+
open Promonoid *-promonoid public
124+
using ()
125+
renaming
126+
( magma to *-magma
127+
; semigroup to *-semigroup
128+
)
129+
130+
------------------------------------------------------------------------
131+
-- Bundles of partially ordered structures
132+
133+
-- Partially ordered semigroups (posemigroups)
134+
135+
record Posemigroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
136+
infix 4 _≈_ _≤_
137+
infixl 7 _∙_
138+
field
139+
Carrier : Set c
140+
_≈_ : Rel Carrier ℓ₁ -- The underlying equality.
141+
_≤_ : Rel Carrier ℓ₂ -- The partial order.
142+
_∙_ : Op₂ Carrier -- Multiplication.
143+
isPosemigroup : IsPosemigroup _≈_ _≤_ _∙_
144+
145+
open IsPosemigroup isPosemigroup public
146+
147+
poset : Poset c ℓ₁ ℓ₂
148+
poset = record { isPartialOrder = isPartialOrder }
149+
150+
open Poset poset public using (preorder)
151+
152+
semigroup : Semigroup c ℓ₁
153+
semigroup = record { isSemigroup = isSemigroup }
154+
155+
open Semigroup semigroup public using (setoid; magma)
156+
157+
prosemigroup : Prosemigroup c ℓ₁ ℓ₂
158+
prosemigroup = record { isProsemigroup = isProsemigroup }
159+
160+
-- Partially ordered monoids (pomonoids)
161+
162+
record Pomonoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
163+
infix 4 _≈_ _≤_
164+
infixl 7 _∙_
165+
field
166+
Carrier : Set c
167+
_≈_ : Rel Carrier ℓ₁ -- The underlying equality.
168+
_≤_ : Rel Carrier ℓ₂ -- The partial order.
169+
_∙_ : Op₂ Carrier -- The monoid multiplication.
170+
ε : Carrier -- The monoid unit.
171+
isPomonoid : IsPomonoid _≈_ _≤_ _∙_ ε
172+
173+
open IsPomonoid isPomonoid public
174+
175+
posemigroup : Posemigroup c ℓ₁ ℓ₂
176+
posemigroup = record { isPosemigroup = isPosemigroup }
177+
178+
open Posemigroup posemigroup public using
179+
( setoid
180+
; preorder
181+
; poset
182+
; magma
183+
; semigroup
184+
; prosemigroup
185+
)
186+
187+
promonoid : Promonoid c ℓ₁ ℓ₂
188+
promonoid = record { isPromonoid = isPromonoid }
189+
190+
open Promonoid promonoid public using (monoid)
191+
192+
-- Partially ordered commutative monoids (commutative pomonoids)
193+
194+
record CommutativePomonoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
195+
infix 4 _≈_ _≤_
196+
infixl 7 _∙_
197+
field
198+
Carrier : Set c
199+
_≈_ : Rel Carrier ℓ₁ -- The underlying equality.
200+
_≤_ : Rel Carrier ℓ₂ -- The partial order.
201+
_∙_ : Op₂ Carrier -- The monoid multiplication.
202+
ε : Carrier -- The monoid unit.
203+
isCommutativePomonoid : IsCommutativePomonoid _≈_ _≤_ _∙_ ε
204+
205+
open IsCommutativePomonoid isCommutativePomonoid public
206+
207+
pomonoid : Pomonoid c ℓ₁ ℓ₂
208+
pomonoid = record { isPomonoid = isPomonoid }
209+
210+
open Pomonoid pomonoid public using
211+
( setoid
212+
; preorder
213+
; poset
214+
; magma
215+
; semigroup
216+
; posemigroup
217+
; prosemigroup
218+
; promonoid
219+
)
220+
221+
commutativePromonoid : CommutativePromonoid c ℓ₁ ℓ₂
222+
commutativePromonoid =
223+
record { isCommutativePromonoid = isCommutativePromonoid }

‎src/Algebra/Ordered/Definitions.agda

Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Properties of functions on ordered structures
5+
------------------------------------------------------------------------
6+
7+
-- The contents of this module should be accessed via `Algebra.Ordered`.
8+
9+
{-# OPTIONS --without-K --safe #-}
10+
11+
open import Relation.Binary.Core
12+
13+
module Algebra.Ordered.Definitions
14+
{a ℓ} {A : Set a} -- The underlying set
15+
(_≤_ : Rel A ℓ) -- The underlying order
16+
where
17+
18+
open import Algebra.Core
19+
open import Function.Base using (flip)
20+
open import Data.Product using (_×_)
21+
22+
Monotonic₁ : Op₁ A → Set _
23+
Monotonic₁ f = f Preserves _≤_ ⟶ _≤_
24+
25+
Antitonic₁ : Op₁ A → Set _
26+
Antitonic₁ f = f Preserves (flip _≤_) ⟶ _≤_
27+
28+
Monotonic₂ : Op₂ A → Set _
29+
Monotonic₂ f = f Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_
30+
31+
MonotonicAntitonic : Op₂ A → Set _
32+
MonotonicAntitonic f = f Preserves₂ _≤_ ⟶ (flip _≤_) ⟶ _≤_
33+
34+
AntitonicMonotonic : Op₂ A → Set _
35+
AntitonicMonotonic f = f Preserves₂ (flip _≤_) ⟶ _≤_ ⟶ _≤_
36+
37+
Antitonic₂ : Op₂ A → Set _
38+
Antitonic₂ f = f Preserves₂ (flip _≤_) ⟶ (flip _≤_) ⟶ _≤_
39+
40+
Adjoint : ∀ {b ℓ′} {B : Set b} → Rel B ℓ′ → (A → B) → (B → A) → Set _
41+
Adjoint _⊑_ f g = ∀ {x y} → (f x ⊑ y → x ≤ g y) × (x ≤ g y → f x ⊑ y)

0 commit comments

Comments
 (0)