Parameterize by equivalence type
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
46ff4465f2
commit
971d75bb2b
117
Lattice.agda
117
Lattice.agda
|
|
@ -10,19 +10,26 @@ open import Agda.Primitive using (lsuc; Level)
|
||||||
|
|
||||||
open import NatMap using (NatMap)
|
open import NatMap using (NatMap)
|
||||||
|
|
||||||
record IsSemilattice {a} (A : Set a) (_⊔_ : A → A → A) : Set a where
|
record IsSemilattice {a} (A : Set a)
|
||||||
field
|
(_≈_ : A → A → Set a)
|
||||||
⊔-assoc : (x y z : A) → (x ⊔ y) ⊔ z ≡ x ⊔ (y ⊔ z)
|
(_⊔_ : A → A → A) : Set a where
|
||||||
⊔-comm : (x y : A) → x ⊔ y ≡ y ⊔ x
|
|
||||||
⊔-idemp : (x : A) → x ⊔ x ≡ x
|
|
||||||
|
|
||||||
record IsLattice {a} (A : Set a) (_⊔_ : A → A → A) (_⊓_ : A → A → A) : Set a where
|
|
||||||
field
|
field
|
||||||
joinSemilattice : IsSemilattice A _⊔_
|
⊔-assoc : (x y z : A) → ((x ⊔ y) ⊔ z) ≈ (x ⊔ (y ⊔ z))
|
||||||
meetSemilattice : IsSemilattice A _⊓_
|
⊔-comm : (x y : A) → (x ⊔ y) ≈ (y ⊔ x)
|
||||||
|
⊔-idemp : (x : A) → (x ⊔ x) ≈ x
|
||||||
|
|
||||||
absorb-⊔-⊓ : (x y : A) → x ⊔ (x ⊓ y) ≡ x
|
record IsLattice {a} (A : Set a)
|
||||||
absorb-⊓-⊔ : (x y : A) → x ⊓ (x ⊔ y) ≡ x
|
(_≈_ : A → A → Set a)
|
||||||
|
(_⊔_ : A → A → A)
|
||||||
|
(_⊓_ : A → A → A) : Set a where
|
||||||
|
|
||||||
|
field
|
||||||
|
joinSemilattice : IsSemilattice A _≈_ _⊔_
|
||||||
|
meetSemilattice : IsSemilattice A _≈_ _⊓_
|
||||||
|
|
||||||
|
absorb-⊔-⊓ : (x y : A) → (x ⊔ (x ⊓ y)) ≈ x
|
||||||
|
absorb-⊓-⊔ : (x y : A) → (x ⊓ (x ⊔ y)) ≈ x
|
||||||
|
|
||||||
open IsSemilattice joinSemilattice public
|
open IsSemilattice joinSemilattice public
|
||||||
open IsSemilattice meetSemilattice public renaming
|
open IsSemilattice meetSemilattice public renaming
|
||||||
|
|
@ -33,19 +40,21 @@ record IsLattice {a} (A : Set a) (_⊔_ : A → A → A) (_⊓_ : A → A → A)
|
||||||
|
|
||||||
record Semilattice {a} (A : Set a) : Set (lsuc a) where
|
record Semilattice {a} (A : Set a) : Set (lsuc a) where
|
||||||
field
|
field
|
||||||
|
_≈_ : A → A → Set a
|
||||||
_⊔_ : A → A → A
|
_⊔_ : A → A → A
|
||||||
|
|
||||||
isSemilattice : IsSemilattice A _⊔_
|
isSemilattice : IsSemilattice A _≈_ _⊔_
|
||||||
|
|
||||||
open IsSemilattice isSemilattice public
|
open IsSemilattice isSemilattice public
|
||||||
|
|
||||||
|
|
||||||
record Lattice {a} (A : Set a) : Set (lsuc a) where
|
record Lattice {a} (A : Set a) : Set (lsuc a) where
|
||||||
field
|
field
|
||||||
|
_≈_ : A → A → Set a
|
||||||
_⊔_ : A → A → A
|
_⊔_ : A → A → A
|
||||||
_⊓_ : A → A → A
|
_⊓_ : A → A → A
|
||||||
|
|
||||||
isLattice : IsLattice A _⊔_ _⊓_
|
isLattice : IsLattice A _≈_ _⊔_ _⊓_
|
||||||
|
|
||||||
open IsLattice isLattice public
|
open IsLattice isLattice public
|
||||||
|
|
||||||
|
|
@ -55,14 +64,14 @@ module IsSemilatticeInstances where
|
||||||
open NatProps
|
open NatProps
|
||||||
open Eq
|
open Eq
|
||||||
|
|
||||||
NatIsMaxSemilattice : IsSemilattice ℕ _⊔_
|
NatIsMaxSemilattice : IsSemilattice ℕ _≡_ _⊔_
|
||||||
NatIsMaxSemilattice = record
|
NatIsMaxSemilattice = record
|
||||||
{ ⊔-assoc = ⊔-assoc
|
{ ⊔-assoc = ⊔-assoc
|
||||||
; ⊔-comm = ⊔-comm
|
; ⊔-comm = ⊔-comm
|
||||||
; ⊔-idemp = ⊔-idem
|
; ⊔-idemp = ⊔-idem
|
||||||
}
|
}
|
||||||
|
|
||||||
NatIsMinSemilattice : IsSemilattice ℕ _⊓_
|
NatIsMinSemilattice : IsSemilattice ℕ _≡_ _⊓_
|
||||||
NatIsMinSemilattice = record
|
NatIsMinSemilattice = record
|
||||||
{ ⊔-assoc = ⊓-assoc
|
{ ⊔-assoc = ⊓-assoc
|
||||||
; ⊔-comm = ⊓-comm
|
; ⊔-comm = ⊓-comm
|
||||||
|
|
@ -70,32 +79,42 @@ module IsSemilatticeInstances where
|
||||||
}
|
}
|
||||||
|
|
||||||
module ForProd {a} {A B : Set a}
|
module ForProd {a} {A B : Set a}
|
||||||
|
(_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a)
|
||||||
(_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B)
|
(_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B)
|
||||||
(sA : IsSemilattice A _⊔₁_) (sB : IsSemilattice B _⊔₂_) where
|
(sA : IsSemilattice A _≈₁_ _⊔₁_) (sB : IsSemilattice B _≈₂_ _⊔₂_) where
|
||||||
|
|
||||||
open Eq
|
open Eq
|
||||||
open Data.Product
|
open Data.Product
|
||||||
|
|
||||||
private
|
private
|
||||||
|
infix 4 _≈_
|
||||||
|
infixl 20 _⊔_
|
||||||
|
|
||||||
|
_≈_ : A × B → A × B → Set a
|
||||||
|
(a₁ , b₁) ≈ (a₂ , b₂) = (a₁ ≈₁ a₂) × (b₁ ≈₂ b₂)
|
||||||
|
|
||||||
_⊔_ : A × B → A × B → A × B
|
_⊔_ : A × B → A × B → A × B
|
||||||
(a₁ , b₁) ⊔ (a₂ , b₂) = (a₁ ⊔₁ a₂ , b₁ ⊔₂ b₂)
|
(a₁ , b₁) ⊔ (a₂ , b₂) = (a₁ ⊔₁ a₂ , b₁ ⊔₂ b₂)
|
||||||
|
|
||||||
⊔-assoc : (p₁ p₂ p₃ : A × B) → (p₁ ⊔ p₂) ⊔ p₃ ≡ p₁ ⊔ (p₂ ⊔ p₃)
|
⊔-assoc : (p₁ p₂ p₃ : A × B) → (p₁ ⊔ p₂) ⊔ p₃ ≈ p₁ ⊔ (p₂ ⊔ p₃)
|
||||||
⊔-assoc (a₁ , b₁) (a₂ , b₂) (a₃ , b₃)
|
⊔-assoc (a₁ , b₁) (a₂ , b₂) (a₃ , b₃) =
|
||||||
rewrite IsSemilattice.⊔-assoc sA a₁ a₂ a₃
|
( IsSemilattice.⊔-assoc sA a₁ a₂ a₃
|
||||||
rewrite IsSemilattice.⊔-assoc sB b₁ b₂ b₃ = refl
|
, IsSemilattice.⊔-assoc sB b₁ b₂ b₃
|
||||||
|
)
|
||||||
|
|
||||||
⊔-comm : (p₁ p₂ : A × B) → p₁ ⊔ p₂ ≡ p₂ ⊔ p₁
|
⊔-comm : (p₁ p₂ : A × B) → p₁ ⊔ p₂ ≈ p₂ ⊔ p₁
|
||||||
⊔-comm (a₁ , b₁) (a₂ , b₂)
|
⊔-comm (a₁ , b₁) (a₂ , b₂) =
|
||||||
rewrite IsSemilattice.⊔-comm sA a₁ a₂
|
( IsSemilattice.⊔-comm sA a₁ a₂
|
||||||
rewrite IsSemilattice.⊔-comm sB b₁ b₂ = refl
|
, IsSemilattice.⊔-comm sB b₁ b₂
|
||||||
|
)
|
||||||
|
|
||||||
⊔-idemp : (p : A × B) → p ⊔ p ≡ p
|
⊔-idemp : (p : A × B) → p ⊔ p ≈ p
|
||||||
⊔-idemp (a , b)
|
⊔-idemp (a , b) =
|
||||||
rewrite IsSemilattice.⊔-idemp sA a
|
( IsSemilattice.⊔-idemp sA a
|
||||||
rewrite IsSemilattice.⊔-idemp sB b = refl
|
, IsSemilattice.⊔-idemp sB b
|
||||||
|
)
|
||||||
|
|
||||||
ProdIsSemilattice : IsSemilattice (A × B) _⊔_
|
ProdIsSemilattice : IsSemilattice (A × B) _≈_ _⊔_
|
||||||
ProdIsSemilattice = record
|
ProdIsSemilattice = record
|
||||||
{ ⊔-assoc = ⊔-assoc
|
{ ⊔-assoc = ⊔-assoc
|
||||||
; ⊔-comm = ⊔-comm
|
; ⊔-comm = ⊔-comm
|
||||||
|
|
@ -112,10 +131,13 @@ module IsLatticeInstances where
|
||||||
|
|
||||||
private
|
private
|
||||||
max-bound₁ : {x y z : ℕ} → x ⊔ y ≡ z → x ≤ z
|
max-bound₁ : {x y z : ℕ} → x ⊔ y ≡ z → x ≤ z
|
||||||
max-bound₁ {x} {y} {z} x⊔y≡z rewrite sym x⊔y≡z rewrite ⊔-comm x y = m≤n⇒m≤o⊔n y (≤-refl)
|
max-bound₁ {x} {y} {z} x⊔y≡z
|
||||||
|
rewrite sym x⊔y≡z
|
||||||
|
rewrite ⊔-comm x y = m≤n⇒m≤o⊔n y (≤-refl)
|
||||||
|
|
||||||
min-bound₁ : {x y z : ℕ} → x ⊓ y ≡ z → z ≤ x
|
min-bound₁ : {x y z : ℕ} → x ⊓ y ≡ z → z ≤ x
|
||||||
min-bound₁ {x} {y} {z} x⊓y≡z rewrite sym x⊓y≡z = m≤n⇒m⊓o≤n y (≤-refl)
|
min-bound₁ {x} {y} {z} x⊓y≡z
|
||||||
|
rewrite sym x⊓y≡z = m≤n⇒m⊓o≤n y (≤-refl)
|
||||||
|
|
||||||
minmax-absorb : {x y : ℕ} → x ⊓ (x ⊔ y) ≡ x
|
minmax-absorb : {x y : ℕ} → x ⊓ (x ⊔ y) ≡ x
|
||||||
minmax-absorb {x} {y} = ≤-antisym x⊓x⊔y≤x (helper x⊓x≤x⊓x⊔y (⊓-idem x))
|
minmax-absorb {x} {y} = ≤-antisym x⊓x⊔y≤x (helper x⊓x≤x⊓x⊔y (⊓-idem x))
|
||||||
|
|
@ -137,7 +159,7 @@ module IsLatticeInstances where
|
||||||
helper : x ⊔ (x ⊓ y) ≤ x ⊔ x → x ⊔ x ≡ x → x ⊔ (x ⊓ y) ≤ x
|
helper : x ⊔ (x ⊓ y) ≤ x ⊔ x → x ⊔ x ≡ x → x ⊔ (x ⊓ y) ≤ x
|
||||||
helper x⊔x⊓y≤x⊔x x⊔x≡x rewrite x⊔x≡x = x⊔x⊓y≤x⊔x
|
helper x⊔x⊓y≤x⊔x x⊔x≡x rewrite x⊔x≡x = x⊔x⊓y≤x⊔x
|
||||||
|
|
||||||
NatIsLattice : IsLattice ℕ _⊔_ _⊓_
|
NatIsLattice : IsLattice ℕ _≡_ _⊔_ _⊓_
|
||||||
NatIsLattice = record
|
NatIsLattice = record
|
||||||
{ joinSemilattice = NatIsMaxSemilattice
|
{ joinSemilattice = NatIsMaxSemilattice
|
||||||
; meetSemilattice = NatIsMinSemilattice
|
; meetSemilattice = NatIsMinSemilattice
|
||||||
|
|
@ -146,13 +168,20 @@ module IsLatticeInstances where
|
||||||
}
|
}
|
||||||
|
|
||||||
module ForProd {a} {A B : Set a}
|
module ForProd {a} {A B : Set a}
|
||||||
|
(_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a)
|
||||||
(_⊔₁_ : A → A → A) (_⊓₁_ : A → A → A)
|
(_⊔₁_ : A → A → A) (_⊓₁_ : A → A → A)
|
||||||
(_⊔₂_ : B → B → B) (_⊓₂_ : B → B → B)
|
(_⊔₂_ : B → B → B) (_⊓₂_ : B → B → B)
|
||||||
(lA : IsLattice A _⊔₁_ _⊓₁_) (lB : IsLattice B _⊔₂_ _⊓₂_) where
|
(lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_) (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
|
||||||
|
|
||||||
private
|
private
|
||||||
module ProdJoin = IsSemilatticeInstances.ForProd _⊔₁_ _⊔₂_ (IsLattice.joinSemilattice lA) (IsLattice.joinSemilattice lB)
|
module ProdJoin = IsSemilatticeInstances.ForProd _≈₁_ _≈₂_ _⊔₁_ _⊔₂_ (IsLattice.joinSemilattice lA) (IsLattice.joinSemilattice lB)
|
||||||
module ProdMeet = IsSemilatticeInstances.ForProd _⊓₁_ _⊓₂_ (IsLattice.meetSemilattice lA) (IsLattice.meetSemilattice lB)
|
module ProdMeet = IsSemilatticeInstances.ForProd _≈₁_ _≈₂_ _⊓₁_ _⊓₂_ (IsLattice.meetSemilattice lA) (IsLattice.meetSemilattice lB)
|
||||||
|
|
||||||
|
infix 4 _≈_
|
||||||
|
infixl 20 _⊔_
|
||||||
|
|
||||||
|
_≈_ : (A × B) → (A × B) → Set a
|
||||||
|
(a₁ , b₁) ≈ (a₂ , b₂) = (a₁ ≈₁ a₂) × (b₁ ≈₂ b₂)
|
||||||
|
|
||||||
_⊔_ : (A × B) → (A × B) → (A × B)
|
_⊔_ : (A × B) → (A × B) → (A × B)
|
||||||
(a₁ , b₁) ⊔ (a₂ , b₂) = (a₁ ⊔₁ a₂ , b₁ ⊔₂ b₂)
|
(a₁ , b₁) ⊔ (a₂ , b₂) = (a₁ ⊔₁ a₂ , b₁ ⊔₂ b₂)
|
||||||
|
|
@ -164,17 +193,19 @@ module IsLatticeInstances where
|
||||||
open Data.Product
|
open Data.Product
|
||||||
|
|
||||||
private
|
private
|
||||||
absorb-⊔-⊓ : (p₁ p₂ : A × B) → p₁ ⊔ (p₁ ⊓ p₂) ≡ p₁
|
absorb-⊔-⊓ : (p₁ p₂ : A × B) → p₁ ⊔ (p₁ ⊓ p₂) ≈ p₁
|
||||||
absorb-⊔-⊓ (a₁ , b₁) (a₂ , b₂)
|
absorb-⊔-⊓ (a₁ , b₁) (a₂ , b₂) =
|
||||||
rewrite IsLattice.absorb-⊔-⊓ lA a₁ a₂
|
( IsLattice.absorb-⊔-⊓ lA a₁ a₂
|
||||||
rewrite IsLattice.absorb-⊔-⊓ lB b₁ b₂ = refl
|
, IsLattice.absorb-⊔-⊓ lB b₁ b₂
|
||||||
|
)
|
||||||
|
|
||||||
absorb-⊓-⊔ : (p₁ p₂ : A × B) → p₁ ⊓ (p₁ ⊔ p₂) ≡ p₁
|
absorb-⊓-⊔ : (p₁ p₂ : A × B) → p₁ ⊓ (p₁ ⊔ p₂) ≈ p₁
|
||||||
absorb-⊓-⊔ (a₁ , b₁) (a₂ , b₂)
|
absorb-⊓-⊔ (a₁ , b₁) (a₂ , b₂) =
|
||||||
rewrite IsLattice.absorb-⊓-⊔ lA a₁ a₂
|
( IsLattice.absorb-⊓-⊔ lA a₁ a₂
|
||||||
rewrite IsLattice.absorb-⊓-⊔ lB b₁ b₂ = refl
|
, IsLattice.absorb-⊓-⊔ lB b₁ b₂
|
||||||
|
)
|
||||||
|
|
||||||
ProdIsLattice : IsLattice (A × B) _⊔_ _⊓_
|
ProdIsLattice : IsLattice (A × B) _≈_ _⊔_ _⊓_
|
||||||
ProdIsLattice = record
|
ProdIsLattice = record
|
||||||
{ joinSemilattice = ProdJoin.ProdIsSemilattice
|
{ joinSemilattice = ProdJoin.ProdIsSemilattice
|
||||||
; meetSemilattice = ProdMeet.ProdIsSemilattice
|
; meetSemilattice = ProdMeet.ProdIsSemilattice
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue
Block a user