Git rid of the bundles (for now) use IsWhatever
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
7b993827bf
commit
46ff4465f2
116
Lattice.agda
116
Lattice.agda
|
|
@ -16,14 +16,6 @@ record IsSemilattice {a} (A : Set a) (_⊔_ : A → A → A) : Set a where
|
|||
⊔-comm : (x y : A) → x ⊔ y ≡ y ⊔ x
|
||||
⊔-idemp : (x : A) → x ⊔ x ≡ x
|
||||
|
||||
record Semilattice {a} (A : Set a) : Set (lsuc a) where
|
||||
field
|
||||
_⊔_ : A → A → A
|
||||
|
||||
isSemilattice : IsSemilattice A _⊔_
|
||||
|
||||
open IsSemilattice isSemilattice public
|
||||
|
||||
record IsLattice {a} (A : Set a) (_⊔_ : A → A → A) (_⊓_ : A → A → A) : Set a where
|
||||
field
|
||||
joinSemilattice : IsSemilattice A _⊔_
|
||||
|
|
@ -39,6 +31,14 @@ record IsLattice {a} (A : Set a) (_⊔_ : A → A → A) (_⊓_ : A → A → A)
|
|||
; ⊔-idemp to ⊓-idemp
|
||||
)
|
||||
|
||||
record Semilattice {a} (A : Set a) : Set (lsuc a) where
|
||||
field
|
||||
_⊔_ : A → A → A
|
||||
|
||||
isSemilattice : IsSemilattice A _⊔_
|
||||
|
||||
open IsSemilattice isSemilattice public
|
||||
|
||||
|
||||
record Lattice {a} (A : Set a) : Set (lsuc a) where
|
||||
field
|
||||
|
|
@ -49,74 +49,67 @@ record Lattice {a} (A : Set a) : Set (lsuc a) where
|
|||
|
||||
open IsLattice isLattice public
|
||||
|
||||
module SemilatticeInstances where
|
||||
module IsSemilatticeInstances where
|
||||
module ForNat where
|
||||
open Nat
|
||||
open NatProps
|
||||
open Eq
|
||||
|
||||
NatMaxSemilattice : Semilattice ℕ
|
||||
NatMaxSemilattice = record
|
||||
{ _⊔_ = _⊔_
|
||||
; isSemilattice = record
|
||||
NatIsMaxSemilattice : IsSemilattice ℕ _⊔_
|
||||
NatIsMaxSemilattice = record
|
||||
{ ⊔-assoc = ⊔-assoc
|
||||
; ⊔-comm = ⊔-comm
|
||||
; ⊔-idemp = ⊔-idem
|
||||
}
|
||||
}
|
||||
|
||||
NatMinSemilattice : Semilattice ℕ
|
||||
NatMinSemilattice = record
|
||||
{ _⊔_ = _⊓_
|
||||
; isSemilattice = record
|
||||
NatIsMinSemilattice : IsSemilattice ℕ _⊓_
|
||||
NatIsMinSemilattice = record
|
||||
{ ⊔-assoc = ⊓-assoc
|
||||
; ⊔-comm = ⊓-comm
|
||||
; ⊔-idemp = ⊓-idem
|
||||
}
|
||||
}
|
||||
|
||||
module ForProd {a} {A B : Set a} (sA : Semilattice A) (sB : Semilattice B) where
|
||||
module ForProd {a} {A B : Set a}
|
||||
(_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B)
|
||||
(sA : IsSemilattice A _⊔₁_) (sB : IsSemilattice B _⊔₂_) where
|
||||
|
||||
open Eq
|
||||
open Data.Product
|
||||
|
||||
private
|
||||
_⊔_ : A × B → A × B → A × B
|
||||
(a₁ , b₁) ⊔ (a₂ , b₂) = (Semilattice._⊔_ sA a₁ a₂ , Semilattice._⊔_ sB b₁ b₂)
|
||||
(a₁ , b₁) ⊔ (a₂ , b₂) = (a₁ ⊔₁ a₂ , b₁ ⊔₂ b₂)
|
||||
|
||||
⊔-assoc : (p₁ p₂ p₃ : A × B) → (p₁ ⊔ p₂) ⊔ p₃ ≡ p₁ ⊔ (p₂ ⊔ p₃)
|
||||
⊔-assoc (a₁ , b₁) (a₂ , b₂) (a₃ , b₃)
|
||||
rewrite Semilattice.⊔-assoc sA a₁ a₂ a₃
|
||||
rewrite Semilattice.⊔-assoc sB b₁ b₂ b₃ = refl
|
||||
rewrite IsSemilattice.⊔-assoc sA a₁ a₂ a₃
|
||||
rewrite IsSemilattice.⊔-assoc sB b₁ b₂ b₃ = refl
|
||||
|
||||
⊔-comm : (p₁ p₂ : A × B) → p₁ ⊔ p₂ ≡ p₂ ⊔ p₁
|
||||
⊔-comm (a₁ , b₁) (a₂ , b₂)
|
||||
rewrite Semilattice.⊔-comm sA a₁ a₂
|
||||
rewrite Semilattice.⊔-comm sB b₁ b₂ = refl
|
||||
rewrite IsSemilattice.⊔-comm sA a₁ a₂
|
||||
rewrite IsSemilattice.⊔-comm sB b₁ b₂ = refl
|
||||
|
||||
⊔-idemp : (p : A × B) → p ⊔ p ≡ p
|
||||
⊔-idemp (a , b)
|
||||
rewrite Semilattice.⊔-idemp sA a
|
||||
rewrite Semilattice.⊔-idemp sB b = refl
|
||||
rewrite IsSemilattice.⊔-idemp sA a
|
||||
rewrite IsSemilattice.⊔-idemp sB b = refl
|
||||
|
||||
ProdSemilattice : Semilattice (A × B)
|
||||
ProdSemilattice = record
|
||||
{ _⊔_ = _⊔_
|
||||
; isSemilattice = record
|
||||
ProdIsSemilattice : IsSemilattice (A × B) _⊔_
|
||||
ProdIsSemilattice = record
|
||||
{ ⊔-assoc = ⊔-assoc
|
||||
; ⊔-comm = ⊔-comm
|
||||
; ⊔-idemp = ⊔-idemp
|
||||
}
|
||||
}
|
||||
|
||||
module LatticeInstances where
|
||||
module IsLatticeInstances where
|
||||
module ForNat where
|
||||
open Nat
|
||||
open NatProps
|
||||
open Eq
|
||||
open SemilatticeInstances.ForNat
|
||||
open IsSemilatticeInstances.ForNat
|
||||
open Data.Product
|
||||
|
||||
|
||||
private
|
||||
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)
|
||||
|
|
@ -144,29 +137,28 @@ module LatticeInstances where
|
|||
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
|
||||
|
||||
NatLattice : Lattice ℕ
|
||||
NatLattice = record
|
||||
{ _⊔_ = _⊔_
|
||||
; _⊓_ = _⊓_
|
||||
; isLattice = record
|
||||
{ joinSemilattice = Semilattice.isSemilattice NatMaxSemilattice
|
||||
; meetSemilattice = Semilattice.isSemilattice NatMinSemilattice
|
||||
NatIsLattice : IsLattice ℕ _⊔_ _⊓_
|
||||
NatIsLattice = record
|
||||
{ joinSemilattice = NatIsMaxSemilattice
|
||||
; meetSemilattice = NatIsMinSemilattice
|
||||
; absorb-⊔-⊓ = λ x y → maxmin-absorb {x} {y}
|
||||
; absorb-⊓-⊔ = λ x y → minmax-absorb {x} {y}
|
||||
}
|
||||
}
|
||||
|
||||
module ForProd {a} {A B : Set a} (lA : Lattice A) (lB : Lattice B) where
|
||||
module ForProd {a} {A B : Set a}
|
||||
(_⊔₁_ : A → A → A) (_⊓₁_ : A → A → A)
|
||||
(_⊔₂_ : B → B → B) (_⊓₂_ : B → B → B)
|
||||
(lA : IsLattice A _⊔₁_ _⊓₁_) (lB : IsLattice B _⊔₂_ _⊓₂_) where
|
||||
|
||||
private
|
||||
module ProdJoin = SemilatticeInstances.ForProd
|
||||
record { _⊔_ = Lattice._⊔_ lA; isSemilattice = Lattice.joinSemilattice lA }
|
||||
record { _⊔_ = Lattice._⊔_ lB; isSemilattice = Lattice.joinSemilattice lB }
|
||||
module ProdMeet = SemilatticeInstances.ForProd
|
||||
record { _⊔_ = Lattice._⊓_ lA; isSemilattice = Lattice.meetSemilattice lA }
|
||||
record { _⊔_ = Lattice._⊓_ lB; isSemilattice = Lattice.meetSemilattice lB }
|
||||
module ProdJoin = IsSemilatticeInstances.ForProd _⊔₁_ _⊔₂_ (IsLattice.joinSemilattice lA) (IsLattice.joinSemilattice lB)
|
||||
module ProdMeet = IsSemilatticeInstances.ForProd _⊓₁_ _⊓₂_ (IsLattice.meetSemilattice lA) (IsLattice.meetSemilattice lB)
|
||||
|
||||
_⊔_ = Semilattice._⊔_ ProdJoin.ProdSemilattice
|
||||
_⊓_ = Semilattice._⊔_ ProdMeet.ProdSemilattice
|
||||
_⊔_ : (A × B) → (A × B) → (A × B)
|
||||
(a₁ , b₁) ⊔ (a₂ , b₂) = (a₁ ⊔₁ a₂ , b₁ ⊔₂ b₂)
|
||||
|
||||
_⊓_ : (A × B) → (A × B) → (A × B)
|
||||
(a₁ , b₁) ⊓ (a₂ , b₂) = (a₁ ⊓₁ a₂ , b₁ ⊓₂ b₂)
|
||||
|
||||
open Eq
|
||||
open Data.Product
|
||||
|
|
@ -174,22 +166,18 @@ module LatticeInstances where
|
|||
private
|
||||
absorb-⊔-⊓ : (p₁ p₂ : A × B) → p₁ ⊔ (p₁ ⊓ p₂) ≡ p₁
|
||||
absorb-⊔-⊓ (a₁ , b₁) (a₂ , b₂)
|
||||
rewrite Lattice.absorb-⊔-⊓ lA a₁ a₂
|
||||
rewrite Lattice.absorb-⊔-⊓ lB b₁ b₂ = refl
|
||||
rewrite IsLattice.absorb-⊔-⊓ lA a₁ a₂
|
||||
rewrite IsLattice.absorb-⊔-⊓ lB b₁ b₂ = refl
|
||||
|
||||
absorb-⊓-⊔ : (p₁ p₂ : A × B) → p₁ ⊓ (p₁ ⊔ p₂) ≡ p₁
|
||||
absorb-⊓-⊔ (a₁ , b₁) (a₂ , b₂)
|
||||
rewrite Lattice.absorb-⊓-⊔ lA a₁ a₂
|
||||
rewrite Lattice.absorb-⊓-⊔ lB b₁ b₂ = refl
|
||||
rewrite IsLattice.absorb-⊓-⊔ lA a₁ a₂
|
||||
rewrite IsLattice.absorb-⊓-⊔ lB b₁ b₂ = refl
|
||||
|
||||
ProdLattice : Lattice (A × B)
|
||||
ProdLattice = record
|
||||
{ _⊔_ = _⊔_
|
||||
; _⊓_ = _⊓_
|
||||
; isLattice = record
|
||||
{ joinSemilattice = Semilattice.isSemilattice ProdJoin.ProdSemilattice
|
||||
; meetSemilattice = Semilattice.isSemilattice ProdMeet.ProdSemilattice
|
||||
ProdIsLattice : IsLattice (A × B) _⊔_ _⊓_
|
||||
ProdIsLattice = record
|
||||
{ joinSemilattice = ProdJoin.ProdIsSemilattice
|
||||
; meetSemilattice = ProdMeet.ProdIsSemilattice
|
||||
; absorb-⊔-⊓ = absorb-⊔-⊓
|
||||
; absorb-⊓-⊔ = absorb-⊓-⊔
|
||||
}
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user