Add a lattice instance for products

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2023-07-14 21:49:47 -07:00
parent 3b29ee0f74
commit cdca2528e9

View File

@ -256,53 +256,98 @@ module SemilatticeInstances where
}
}
private module NatInstances where
open Nat
open NatProps
open Eq
open SemilatticeInstances.ForNat
open Data.Product
module LatticeInstances where
module ForNat where
open Nat
open NatProps
open Eq
open SemilatticeInstances.ForNat
open Data.Product
private
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))
where
x⊓x⊔y≤x = proj₁ (Semilattice.⊔-bound NatMinSemilattice x (x y) (x (x y)) refl)
x⊓x≤x⊓x⊔y = ⊓-mono-≤ {x} {x} ≤-refl (proj₁ (Semilattice.⊔-bound NatMaxSemilattice x y (x y) refl))
private
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))
where
x⊓x⊔y≤x = proj₁ (Semilattice.⊔-bound NatMinSemilattice x (x y) (x (x y)) refl)
x⊓x≤x⊓x⊔y = ⊓-mono-≤ {x} {x} ≤-refl (proj₁ (Semilattice.⊔-bound NatMaxSemilattice x y (x y) refl))
-- >:(
helper : x x x (x y) x x x x x (x y)
helper x⊓x≤x⊓x⊔y x⊓x≡x rewrite x⊓x≡x = x⊓x≤x⊓x⊔y
-- >:(
helper : x x x (x y) x x x x x (x y)
helper x⊓x≤x⊓x⊔y x⊓x≡x rewrite x⊓x≡x = x⊓x≤x⊓x⊔y
maxmin-absorb : {x y : } x (x y) x
maxmin-absorb {x} {y} = ≤-antisym (helper x⊔x⊓y≤x⊔x (⊔-idem x)) x≤x⊔x⊓y
where
x≤x⊔x⊓y = proj₁ (Semilattice.⊔-bound NatMaxSemilattice x (x y) (x (x y)) refl)
x⊔x⊓y≤x⊔x = ⊔-mono-≤ {x} {x} ≤-refl (proj₁ (Semilattice.⊔-bound NatMinSemilattice x y (x y) refl))
maxmin-absorb : {x y : } x (x y) x
maxmin-absorb {x} {y} = ≤-antisym (helper x⊔x⊓y≤x⊔x (⊔-idem x)) x≤x⊔x⊓y
where
x≤x⊔x⊓y = proj₁ (Semilattice.⊔-bound NatMaxSemilattice x (x y) (x (x y)) refl)
x⊔x⊓y≤x⊔x = ⊔-mono-≤ {x} {x} ≤-refl (proj₁ (Semilattice.⊔-bound NatMinSemilattice x y (x y) refl))
-- >:(
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 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
; absorb-⊔-⊓ = λ x y maxmin-absorb {x} {y}
; absorb-⊓-⊔ = λ x y minmax-absorb {x} {y}
NatLattice : Lattice
NatLattice = record
{ _≼_ = _≤_
; _⊔_ = _⊔_
; _⊓_ = _⊓_
; isLattice = record
{ joinSemilattice = Semilattice.isSemilattice NatMaxSemilattice
; meetSemilattice = Semilattice.isSemilattice NatMinSemilattice
; absorb-⊔-⊓ = λ x y maxmin-absorb {x} {y}
; absorb-⊓-⊔ = λ x y minmax-absorb {x} {y}
}
}
}
-- ProdSemilattice : {a : Level} → {A B : Set a} → {{ Semilattice A }} → {{ Semilattice B }} → Semilattice (A × B)
-- ProdSemilattice {a} {A} {B} {{slA}} {{slB}} = record
-- { _≼_ = λ (a₁ , b₁) (a₂ , b₂) → Semilattice._≼_ slA a₁ a₂ × Semilattice._≼_ slB b₁ b₂
-- ; _⊔_ = λ (a₁ , b₁) (a₂ , b₂) → (Semilattice._⊔_ slA a₁ a₂ , Semilattice._⊔_ slB b₁ b₂)
-- ; isSemilattice = record
-- {
-- }
-- }
module ForProd {a} {A B : Set a} (lA : Lattice A) (lB : Lattice B) where
private
_≼₁_ = Lattice._≼_ lA
_≼₂_ = Lattice._≼_ lB
_⊔₁_ = Lattice._⊔_ lA
_⊔₂_ = Lattice._⊔_ lB
_⊓₁_ = Lattice._⊓_ lA
_⊓₂_ = Lattice._⊓_ lB
joinA = record { _≼_ = _≼₁_; _⊔_ = _⊔₁_; isSemilattice = Lattice.joinSemilattice lA }
joinB = record { _≼_ = _≼₂_; _⊔_ = _⊔₂_; isSemilattice = Lattice.joinSemilattice lB }
meetA = record { _≼_ = λ a b b ≼₁ a; _⊔_ = _⊓₁_; isSemilattice = Lattice.meetSemilattice lA }
meetB = record { _≼_ = λ a b b ≼₂ a; _⊔_ = _⊓₂_; isSemilattice = Lattice.meetSemilattice lB }
module ProdJoin = SemilatticeInstances.ForProd joinA joinB
module ProdMeet = SemilatticeInstances.ForProd meetA meetB
_≼_ = Semilattice._≼_ ProdJoin.ProdSemilattice
_⊔_ = Semilattice._⊔_ ProdJoin.ProdSemilattice
_⊓_ = Semilattice._⊔_ ProdMeet.ProdSemilattice
open Eq
open Data.Product
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
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
ProdLattice : Lattice (A × B)
ProdLattice = record
{ _≼_ = _≼_
; _⊔_ = _⊔_
; _⊓_ = _⊓_
; isLattice = record
{ joinSemilattice = Semilattice.isSemilattice ProdJoin.ProdSemilattice
; meetSemilattice = Semilattice.isSemilattice ProdMeet.ProdSemilattice
; absorb-⊔-⊓ = absorb-⊔-⊓
; absorb-⊓-⊔ = absorb-⊓-⊔
}
}