Clean up the Lattice definitions a fair bit

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2023-08-20 19:02:47 -07:00
parent e62f429b86
commit 421f187e8b

View File

@ -91,6 +91,31 @@ record Lattice {a} (A : Set a) : Set (lsuc a) where
open IsLattice isLattice public open IsLattice isLattice public
module IsEquivalenceInstances where module IsEquivalenceInstances where
module ForProd {a} {A B : Set a}
(_≈₁_ : A A Set a) (_≈₂_ : B B Set a)
(eA : IsEquivalence A _≈₁_) (eB : IsEquivalence B _≈₂_) where
infix 4 _≈_
_≈_ : A × B A × B Set a
(a₁ , b₁) (a₂ , b₂) = (a₁ ≈₁ a₂) × (b₁ ≈₂ b₂)
ProdEquivalence : IsEquivalence (A × B) _≈_
ProdEquivalence = record
{ ≈-refl = λ {p}
( IsEquivalence.≈-refl eA
, IsEquivalence.≈-refl eB
)
; ≈-sym = λ {p₁} {p₂} (a₁≈a₂ , b₁≈b₂)
( IsEquivalence.≈-sym eA a₁≈a₂
, IsEquivalence.≈-sym eB b₁≈b₂
)
; ≈-trans = λ {p₁} {p₂} {p₃} (a₁≈a₂ , b₁≈b₂) (a₂≈a₃ , b₂≈b₃)
( IsEquivalence.≈-trans eA a₁≈a₂ a₂≈a₃
, IsEquivalence.≈-trans eB b₁≈b₂ b₂≈b₃
)
}
module ForMap {a b} (A : Set a) (B : Set b) module ForMap {a b} (A : Set a) (B : Set b)
(≡-dec-A : Decidable (_≡_ {a} {A})) (≡-dec-A : Decidable (_≡_ {a} {A}))
(_≈₂_ : B B Set b) (_≈₂_ : B B Set b)
@ -105,13 +130,13 @@ module IsEquivalenceInstances where
; ≈-trans to ≈₂-trans ; ≈-trans to ≈₂-trans
) )
private
_≈_ : Map Map Set (Agda.Primitive._⊔_ a b) _≈_ : Map Map Set (Agda.Primitive._⊔_ a b)
_≈_ = lift _≈₂_ _≈_ = lift _≈₂_
_⊆_ : Map Map Set (Agda.Primitive._⊔_ a b) _⊆_ : Map Map Set (Agda.Primitive._⊔_ a b)
_⊆_ = subset _≈₂_ _⊆_ = subset _≈₂_
private
⊆-refl : (m : Map) m m ⊆-refl : (m : Map) m m
⊆-refl _ k v k,v∈m = (v , (≈₂-refl , k,v∈m)) ⊆-refl _ k v k,v∈m = (v , (≈₂-refl , k,v∈m))
@ -122,23 +147,14 @@ module IsEquivalenceInstances where
(v'' , (v'≈v'' , k,v''∈m₃)) = m₂⊆m₃ k v' k,v'∈m₂ (v'' , (v'≈v'' , k,v''∈m₃)) = m₂⊆m₃ k v' k,v'∈m₂
in (v'' , (≈₂-trans v≈v' v'≈v'' , k,v''∈m₃)) in (v'' , (≈₂-trans v≈v' v'≈v'' , k,v''∈m₃))
≈-refl : (m : Map) m m LiftEquivalence : IsEquivalence Map _≈_
≈-refl m = (⊆-refl m , ⊆-refl m) LiftEquivalence = record
{ ≈-refl = λ {m} (⊆-refl m , ⊆-refl m)
≈-sym : (m₁ m₂ : Map) m₁ m₂ m₂ m₁ ; ≈-sym = λ {m₁} {m₂} (m₁⊆m₂ , m₂⊆m₁) (m₂⊆m₁ , m₁⊆m₂)
≈-sym _ _ (m₁⊆m₂ , m₂⊆m₁) = (m₂⊆m₁ , m₁⊆m₂) ; ≈-trans = λ {m₁} {m₂} {m₃} (m₁⊆m₂ , m₂⊆m₁) (m₂⊆m₃ , m₃⊆m₂)
≈-trans : (m₁ m₂ m₃ : Map) m₁ m₂ m₂ m₃ m₁ m₃
≈-trans m₁ m₂ m₃ (m₁⊆m₂ , m₂⊆m₁) (m₂⊆m₃ , m₃⊆m₂) =
( ⊆-trans m₁ m₂ m₃ m₁⊆m₂ m₂⊆m₃ ( ⊆-trans m₁ m₂ m₃ m₁⊆m₂ m₂⊆m₃
, ⊆-trans m₃ m₂ m₁ m₃⊆m₂ m₂⊆m₁ , ⊆-trans m₃ m₂ m₁ m₃⊆m₂ m₂⊆m₁
) )
LiftEquivalence : IsEquivalence Map _≈_
LiftEquivalence = record
{ ≈-refl = λ {m₁} ≈-refl m₁
; ≈-sym = λ {m₁} {m₂} ≈-sym m₁ m₂
; ≈-trans = λ {m₁} {m₂} {m₃} ≈-trans m₁ m₂ m₃
} }
module IsSemilatticeInstances where module IsSemilatticeInstances where
@ -179,63 +195,29 @@ module IsSemilatticeInstances where
open Eq open Eq
open Data.Product open Data.Product
private module ProdEquiv = IsEquivalenceInstances.ForProd _≈₁_ _≈₂_ (IsSemilattice.≈-equiv sA) (IsSemilattice.≈-equiv sB)
infix 4 _≈_ open ProdEquiv using (_≈_) public
infixl 20 _⊔_
_≈_ : A × B A × B Set a infixl 20 _⊔_
(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₃) ProdIsSemilattice : IsSemilattice (A × B) _≈_ _⊔_
⊔-assoc (a₁ , b₁) (a₂ , b₂) (a₃ , b₃) = ProdIsSemilattice = record
{ ≈-equiv = ProdEquiv.ProdEquivalence
; ⊔-assoc = λ (a₁ , b₁) (a₂ , b₂) (a₃ , b₃)
( IsSemilattice.⊔-assoc sA a₁ a₂ a₃ ( IsSemilattice.⊔-assoc sA a₁ a₂ a₃
, IsSemilattice.⊔-assoc sB b₁ b₂ b₃ , IsSemilattice.⊔-assoc sB b₁ b₂ b₃
) )
; ⊔-comm = λ (a₁ , b₁) (a₂ , b₂)
⊔-comm : (p₁ p₂ : A × B) p₁ p₂ p₂ p₁
⊔-comm (a₁ , b₁) (a₂ , b₂) =
( IsSemilattice.⊔-comm sA a₁ a₂ ( IsSemilattice.⊔-comm sA a₁ a₂
, IsSemilattice.⊔-comm sB b₁ b₂ , IsSemilattice.⊔-comm sB b₁ b₂
) )
; ⊔-idemp = λ (a , b)
⊔-idemp : (p : A × B) p p p
⊔-idemp (a , b) =
( IsSemilattice.⊔-idemp sA a ( IsSemilattice.⊔-idemp sA a
, IsSemilattice.⊔-idemp sB b , IsSemilattice.⊔-idemp sB b
) )
≈-refl : {p : A × B} p p
≈-refl =
( IsSemilattice.≈-refl sA
, IsSemilattice.≈-refl sB
)
≈-sym : {p₁ p₂ : A × B} p₁ p₂ p₂ p₁
≈-sym (a₁≈a₂ , b₁≈b₂) =
( IsSemilattice.≈-sym sA a₁≈a₂
, IsSemilattice.≈-sym sB b₁≈b₂
)
≈-trans : {p₁ p₂ p₃ : A × B} p₁ p₂ p₂ p₃ p₁ p₃
≈-trans (a₁≈a₂ , b₁≈b₂) (a₂≈a₃ , b₂≈b₃) =
( IsSemilattice.≈-trans sA a₁≈a₂ a₂≈a₃
, IsSemilattice.≈-trans sB b₁≈b₂ b₂≈b₃
)
ProdIsSemilattice : IsSemilattice (A × B) _≈_ _⊔_
ProdIsSemilattice = record
{ ≈-equiv = record
{ ≈-refl = ≈-refl
; ≈-sym = ≈-sym
; ≈-trans = ≈-trans
}
; ⊔-assoc = ⊔-assoc
; ⊔-comm = ⊔-comm
; ⊔-idemp = ⊔-idemp
} }
module ForMap {a} {A B : Set a} module ForMap {a} {A B : Set a}
@ -250,12 +232,11 @@ module IsSemilatticeInstances where
; ⊔-assoc to ⊔₂-assoc; ⊔-comm to ⊔₂-comm; ⊔-idemp to ⊔₂-idemp ; ⊔-assoc to ⊔₂-assoc; ⊔-comm to ⊔₂-comm; ⊔-idemp to ⊔₂-idemp
) )
private module MapEquiv = IsEquivalenceInstances.ForMap A B ≡-dec-A _≈₂_ (IsSemilattice.≈-equiv sB)
infix 4 _≈_ open MapEquiv using (_≈_) public
infixl 20 _⊔_
_≈_ : Map Map Set a infixl 20 _⊔_
_≈_ = lift (_≈₂_) infixl 20 _⊓_
_⊔_ : Map Map Map _⊔_ : Map Map Map
m₁ m₂ = union _⊔₂_ m₁ m₂ m₁ m₂ = union _⊔₂_ m₁ m₂
@ -263,8 +244,6 @@ module IsSemilatticeInstances where
_⊓_ : Map Map Map _⊓_ : Map Map Map
m₁ m₂ = intersect _⊔₂_ m₁ m₂ m₁ m₂ = intersect _⊔₂_ m₁ m₂
module MapEquiv = IsEquivalenceInstances.ForMap A B ≡-dec-A _≈₂_ (IsSemilattice.≈-equiv sB)
MapIsUnionSemilattice : IsSemilattice Map _≈_ _⊔_ MapIsUnionSemilattice : IsSemilattice Map _≈_ _⊔_
MapIsUnionSemilattice = record MapIsUnionSemilattice = record
{ ≈-equiv = MapEquiv.LiftEquivalence { ≈-equiv = MapEquiv.LiftEquivalence
@ -333,44 +312,24 @@ module IsLatticeInstances where
(_⊔₂_ : 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
module ProdJoin = IsSemilatticeInstances.ForProd _≈₁_ _≈₂_ _⊔₁_ _⊔₂_ (IsLattice.joinSemilattice lA) (IsLattice.joinSemilattice lB) module ProdJoin = IsSemilatticeInstances.ForProd _≈₁_ _≈₂_ _⊔₁_ _⊔₂_ (IsLattice.joinSemilattice lA) (IsLattice.joinSemilattice lB)
open ProdJoin using (_⊔_; _≈_) public
module ProdMeet = IsSemilatticeInstances.ForProd _≈₁_ _≈₂_ _⊓₁_ _⊓₂_ (IsLattice.meetSemilattice lA) (IsLattice.meetSemilattice lB) module ProdMeet = IsSemilatticeInstances.ForProd _≈₁_ _≈₂_ _⊓₁_ _⊓₂_ (IsLattice.meetSemilattice lA) (IsLattice.meetSemilattice lB)
open ProdMeet using () renaming (_⊔_ to _⊓_) public
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₁ ⊔₁ a₂ , b₁ ⊔₂ b₂)
_⊓_ : (A × B) (A × B) (A × B)
(a₁ , b₁) (a₂ , b₂) = (a₁ ⊓₁ a₂ , b₁ ⊓₂ b₂)
open Eq
open Data.Product
private
absorb-⊔-⊓ : (p₁ p₂ : A × B) p₁ (p₁ p₂) p₁
absorb-⊔-⊓ (a₁ , b₁) (a₂ , b₂) =
( IsLattice.absorb-⊔-⊓ lA a₁ a₂
, IsLattice.absorb-⊔-⊓ lB b₁ b₂
)
absorb-⊓-⊔ : (p₁ p₂ : A × B) p₁ (p₁ p₂) p₁
absorb-⊓-⊔ (a₁ , b₁) (a₂ , b₂) =
( IsLattice.absorb-⊓-⊔ lA a₁ a₂
, 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
; absorb-⊔-⊓ = absorb-⊔-⊓ ; absorb-⊔-⊓ = λ (a₁ , b₁) (a₂ , b₂)
; absorb-⊓-⊔ = absorb-⊓-⊔ ( IsLattice.absorb-⊔-⊓ lA a₁ a₂
, IsLattice.absorb-⊔-⊓ lB b₁ b₂
)
; absorb-⊓-⊔ = λ (a₁ , b₁) (a₂ , b₂)
( IsLattice.absorb-⊓-⊔ lA a₁ a₂
, IsLattice.absorb-⊓-⊔ lB b₁ b₂
)
} }
module ForMap {a} {A B : Set a} module ForMap {a} {A B : Set a}
@ -387,21 +346,11 @@ module IsLatticeInstances where
; absorb-⊔-⊓ to absorb-⊔₂-⊓₂; absorb-⊓-⊔ to absorb-⊓₂-⊔₂ ; absorb-⊔-⊓ to absorb-⊔₂-⊓₂; absorb-⊓-⊔ to absorb-⊓₂-⊔₂
) )
private
module MapJoin = IsSemilatticeInstances.ForMap ≡-dec-A _≈₂_ _⊔₂_ (IsLattice.joinSemilattice lB) module MapJoin = IsSemilatticeInstances.ForMap ≡-dec-A _≈₂_ _⊔₂_ (IsLattice.joinSemilattice lB)
open MapJoin using (_⊔_; _≈_) public
module MapMeet = IsSemilatticeInstances.ForMap ≡-dec-A _≈₂_ _⊓₂_ (IsLattice.meetSemilattice lB) module MapMeet = IsSemilatticeInstances.ForMap ≡-dec-A _≈₂_ _⊓₂_ (IsLattice.meetSemilattice lB)
open MapMeet using (_⊓_) public
infix 4 _≈_
infixl 20 _⊔_
_≈_ : Map Map Set a
_≈_ = lift (_≈₂_)
_⊔_ : Map Map Map
m₁ m₂ = union _⊔₂_ m₁ m₂
_⊓_ : Map Map Map
m₁ m₂ = intersect _⊓₂_ m₁ m₂
MapIsLattice : IsLattice Map _≈_ _⊔_ _⊓_ MapIsLattice : IsLattice Map _≈_ _⊔_ _⊓_
MapIsLattice = record MapIsLattice = record