From cdca2528e94069335bb58738f4f59251dc12fb87 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Fri, 14 Jul 2023 21:49:47 -0700 Subject: [PATCH] Add a lattice instance for products Signed-off-by: Danila Fedorin --- Lattice.agda | 129 ++++++++++++++++++++++++++++++++++----------------- 1 file changed, 87 insertions(+), 42 deletions(-) diff --git a/Lattice.agda b/Lattice.agda index 920a4cd..f2970d0 100644 --- a/Lattice.agda +++ b/Lattice.agda @@ -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-⊓-⊔ + } + }