From 7b993827bf953398db9da997a9e0fbaac7f4b255 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 15 Jul 2023 12:18:50 -0700 Subject: [PATCH] Delete the unneeded <= relation from instances Signed-off-by: Danila Fedorin --- Lattice.agda | 218 +++++++-------------------------------------------- 1 file changed, 30 insertions(+), 188 deletions(-) diff --git a/Lattice.agda b/Lattice.agda index f2970d0..139b90e 100644 --- a/Lattice.agda +++ b/Lattice.agda @@ -10,57 +10,24 @@ open import Agda.Primitive using (lsuc; Level) open import NatMap using (NatMap) -record IsPreorder {a} (A : Set a) (_≼_ : A → A → Set a) : Set a where +record IsSemilattice {a} (A : Set a) (_⊔_ : A → A → A) : Set a where field - ≼-refl : Reflexive (_≼_) - ≼-trans : Transitive (_≼_) - ≼-antisym : Antisymmetric (_≡_) (_≼_) - -isPreorderFlip : {a : Level} → {A : Set a} → {_≼_ : A → A → Set a} → IsPreorder A _≼_ → IsPreorder A (λ x y → y ≼ x) -isPreorderFlip isPreorder = record - { ≼-refl = IsPreorder.≼-refl isPreorder - ; ≼-trans = λ {x} {y} {z} x≽y y≽z → IsPreorder.≼-trans isPreorder y≽z x≽y - ; ≼-antisym = λ {x} {y} x≽y y≽x → IsPreorder.≼-antisym isPreorder y≽x x≽y - } - -record Preorder {a} (A : Set a) : Set (lsuc a) where - field - _≼_ : A → A → Set a - - isPreorder : IsPreorder A _≼_ - - open IsPreorder isPreorder public - -record IsSemilattice {a} (A : Set a) (_≼_ : A → A → Set a) (_⊔_ : A → A → A) : Set a where - field - isPreorder : IsPreorder A _≼_ - ⊔-assoc : (x y z : A) → (x ⊔ y) ⊔ z ≡ x ⊔ (y ⊔ z) ⊔-comm : (x y : A) → x ⊔ y ≡ y ⊔ x ⊔-idemp : (x : A) → x ⊔ x ≡ x - ⊔-bound : (x y z : A) → x ⊔ y ≡ z → (x ≼ z × y ≼ z) - ⊔-least : (x y z : A) → x ⊔ y ≡ z → ∀ (z' : A) → (x ≼ z' × y ≼ z') → z ≼ z' - - open IsPreorder isPreorder public - record Semilattice {a} (A : Set a) : Set (lsuc a) where field - _≼_ : A → A → Set a _⊔_ : A → A → A - isSemilattice : IsSemilattice A _≼_ _⊔_ + isSemilattice : IsSemilattice A _⊔_ open IsSemilattice isSemilattice public -record IsLattice {a} (A : Set a) (_≼_ : A → A → Set a) (_⊔_ : A → A → A) (_⊓_ : A → A → A) : Set a where - - _≽_ : A → A → Set a - a ≽ b = b ≼ a - +record IsLattice {a} (A : Set a) (_⊔_ : A → A → A) (_⊓_ : A → A → A) : Set a where field - joinSemilattice : IsSemilattice A _≼_ _⊔_ - meetSemilattice : IsSemilattice A _≽_ _⊓_ + joinSemilattice : IsSemilattice A _⊔_ + meetSemilattice : IsSemilattice A _⊓_ absorb-⊔-⊓ : (x y : A) → x ⊔ (x ⊓ y) ≡ x absorb-⊓-⊔ : (x y : A) → x ⊓ (x ⊔ y) ≡ x @@ -70,139 +37,49 @@ record IsLattice {a} (A : Set a) (_≼_ : A → A → Set a) (_⊔_ : A → A ( ⊔-assoc to ⊓-assoc ; ⊔-comm to ⊓-comm ; ⊔-idemp to ⊓-idemp - ; ⊔-bound to ⊓-bound - ; ⊔-least to ⊓-least ) record Lattice {a} (A : Set a) : Set (lsuc a) where field - _≼_ : A → A → Set a _⊔_ : A → A → A _⊓_ : A → A → A - isLattice : IsLattice A _≼_ _⊔_ _⊓_ + isLattice : IsLattice A _⊔_ _⊓_ open IsLattice isLattice public -module PreorderInstances where - module ForNat where - open NatProps - - NatPreorder : Preorder ℕ - NatPreorder = record - { _≼_ = _≤_ - ; isPreorder = record - { ≼-refl = ≤-refl - ; ≼-trans = ≤-trans - ; ≼-antisym = ≤-antisym - } - } - - module ForProd {a} {A B : Set a} (pA : Preorder A) (pB : Preorder B) where - open Eq - - private - _≼_ : A × B → A × B → Set a - (a₁ , b₁) ≼ (a₂ , b₂) = Preorder._≼_ pA a₁ a₂ × Preorder._≼_ pB b₁ b₂ - - ≼-refl : {p : A × B} → p ≼ p - ≼-refl {(a , b)} = (Preorder.≼-refl pA {a}, Preorder.≼-refl pB {b}) - - ≼-trans : {p₁ p₂ p₃ : A × B} → p₁ ≼ p₂ → p₂ ≼ p₃ → p₁ ≼ p₃ - ≼-trans (a₁≼a₂ , b₁≼b₂) (a₂≼a₃ , b₂≼b₃) = - ( Preorder.≼-trans pA a₁≼a₂ a₂≼a₃ - , Preorder.≼-trans pB b₁≼b₂ b₂≼b₃ - ) - - ≼-antisym : {p₁ p₂ : A × B} → p₁ ≼ p₂ → p₂ ≼ p₁ → p₁ ≡ p₂ - ≼-antisym (a₁≼a₂ , b₁≼b₂) (a₂≼a₁ , b₂≼b₁) = cong₂ (_,_) (Preorder.≼-antisym pA a₁≼a₂ a₂≼a₁) (Preorder.≼-antisym pB b₁≼b₂ b₂≼b₁) - - ProdPreorder : Preorder (A × B) - ProdPreorder = record - { _≼_ = _≼_ - ; isPreorder = record - { ≼-refl = ≼-refl - ; ≼-trans = ≼-trans - ; ≼-antisym = ≼-antisym - } - } - module SemilatticeInstances where module ForNat where open Nat open NatProps open Eq - open PreorderInstances.ForNat - - 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) - - max-bound₂ : {x y z : ℕ} → x ⊔ y ≡ z → y ≤ z - max-bound₂ {x} {y} {z} x⊔y≡z rewrite sym x⊔y≡z = m≤n⇒m≤o⊔n x (≤-refl) - - max-least : (x y z : ℕ) → x ⊔ y ≡ z → ∀ (z' : ℕ) → (x ≤ z' × y ≤ z') → z ≤ z' - max-least x y z x⊔y≡z z' (x≤z' , y≤z') with (⊔-sel x y) - ... | inj₁ x⊔y≡x rewrite trans (sym x⊔y≡z) (x⊔y≡x) = x≤z' - ... | inj₂ x⊔y≡y rewrite trans (sym x⊔y≡z) (x⊔y≡y) = y≤z' NatMaxSemilattice : Semilattice ℕ NatMaxSemilattice = record - { _≼_ = _≤_ - ; _⊔_ = _⊔_ + { _⊔_ = _⊔_ ; isSemilattice = record - { isPreorder = Preorder.isPreorder NatPreorder - ; ⊔-assoc = ⊔-assoc + { ⊔-assoc = ⊔-assoc ; ⊔-comm = ⊔-comm ; ⊔-idemp = ⊔-idem - ; ⊔-bound = λ x y z x⊔y≡z → (max-bound₁ x⊔y≡z , max-bound₂ x⊔y≡z) - ; ⊔-least = max-least } } - private - 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 → z ≤ y - min-bound₂ {x} {y} {z} x⊓y≡z rewrite sym x⊓y≡z rewrite ⊓-comm x y = m≤n⇒m⊓o≤n x (≤-refl) - - min-greatest : (x y z : ℕ) → x ⊓ y ≡ z → ∀ (z' : ℕ) → (z' ≤ x × z' ≤ y) → z' ≤ z - min-greatest x y z x⊓y≡z z' (z'≤x , z'≤y) with (⊓-sel x y) - ... | inj₁ x⊓y≡x rewrite trans (sym x⊓y≡z) (x⊓y≡x) = z'≤x - ... | inj₂ x⊓y≡y rewrite trans (sym x⊓y≡z) (x⊓y≡y) = z'≤y - - NatMinSemilattice : Semilattice ℕ NatMinSemilattice = record - { _≼_ = _≥_ - ; _⊔_ = _⊓_ + { _⊔_ = _⊓_ ; isSemilattice = record - { isPreorder = isPreorderFlip (Preorder.isPreorder NatPreorder) - ; ⊔-assoc = ⊓-assoc + { ⊔-assoc = ⊓-assoc ; ⊔-comm = ⊓-comm ; ⊔-idemp = ⊓-idem - ; ⊔-bound = λ x y z x⊓y≡z → (min-bound₁ x⊓y≡z , min-bound₂ x⊓y≡z) - ; ⊔-least = min-greatest } } module ForProd {a} {A B : Set a} (sA : Semilattice A) (sB : Semilattice B) where - private - _≼₁_ = Semilattice._≼_ sA - _≼₂_ = Semilattice._≼_ sB - - pA = record { _≼_ = _≼₁_; isPreorder = Semilattice.isPreorder sA } - pB = record { _≼_ = _≼₂_; isPreorder = Semilattice.isPreorder sB } - - open PreorderInstances.ForProd pA pB open Eq open Data.Product private - _≼_ = Preorder._≼_ ProdPreorder - _⊔_ : A × B → A × B → A × B (a₁ , b₁) ⊔ (a₂ , b₂) = (Semilattice._⊔_ sA a₁ a₂ , Semilattice._⊔_ sB b₁ b₂) @@ -221,38 +98,13 @@ module SemilatticeInstances where rewrite Semilattice.⊔-idemp sA a rewrite Semilattice.⊔-idemp sB b = refl - ⊔-bound₁ : {p₁ p₂ p₃ : A × B} → p₁ ⊔ p₂ ≡ p₃ → p₁ ≼ p₃ - ⊔-bound₁ {(a₁ , b₁)} {(a₂ , b₂)} {(a₃ , b₃)} p₁⊔p₂≡p₃ = (⊔-bound-a , ⊔-bound-b) - where - ⊔-bound-a = proj₁ (Semilattice.⊔-bound sA a₁ a₂ a₃ (cong proj₁ p₁⊔p₂≡p₃)) - ⊔-bound-b = proj₁ (Semilattice.⊔-bound sB b₁ b₂ b₃ (cong proj₂ p₁⊔p₂≡p₃)) - - ⊔-bound₂ : {p₁ p₂ p₃ : A × B} → p₁ ⊔ p₂ ≡ p₃ → p₂ ≼ p₃ - ⊔-bound₂ {(a₁ , b₁)} {(a₂ , b₂)} {(a₃ , b₃)} p₁⊔p₂≡p₃ = (⊔-bound-a , ⊔-bound-b) - where - ⊔-bound-a = proj₂ (Semilattice.⊔-bound sA a₁ a₂ a₃ (cong proj₁ p₁⊔p₂≡p₃)) - ⊔-bound-b = proj₂ (Semilattice.⊔-bound sB b₁ b₂ b₃ (cong proj₂ p₁⊔p₂≡p₃)) - - ⊔-least : (p₁ p₂ p₃ : A × B) → p₁ ⊔ p₂ ≡ p₃ → ∀ (p₃' : A × B) → (p₁ ≼ p₃' × p₂ ≼ p₃') → p₃ ≼ p₃' - ⊔-least (a₁ , b₁) (a₂ , b₂) (a₃ , b₃) p₁⊔p₂≡p₃ (a₃' , b₃') (p₁≼p₃' , p₂≼p₃') = (⊔-least-a , ⊔-least-b) - where - ⊔-least-a : a₃ ≼₁ a₃' - ⊔-least-a = Semilattice.⊔-least sA a₁ a₂ a₃ (cong proj₁ p₁⊔p₂≡p₃) a₃' (proj₁ p₁≼p₃' , proj₁ p₂≼p₃') - - ⊔-least-b : b₃ ≼₂ b₃' - ⊔-least-b = Semilattice.⊔-least sB b₁ b₂ b₃ (cong proj₂ p₁⊔p₂≡p₃) b₃' (proj₂ p₁≼p₃' , proj₂ p₂≼p₃') - ProdSemilattice : Semilattice (A × B) ProdSemilattice = record - { _≼_ = _≼_ - ; _⊔_ = _⊔_ + { _⊔_ = _⊔_ ; isSemilattice = record - { isPreorder = Preorder.isPreorder ProdPreorder - ; ⊔-assoc = ⊔-assoc + { ⊔-assoc = ⊔-assoc ; ⊔-comm = ⊔-comm ; ⊔-idemp = ⊔-idemp - ; ⊔-bound = λ x y z x⊓y≡z → (⊔-bound₁ x⊓y≡z , ⊔-bound₂ x⊓y≡z) - ; ⊔-least = ⊔-least } } @@ -266,11 +118,17 @@ module LatticeInstances where 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) + + 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) + 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)) + x⊓x⊔y≤x = min-bound₁ {x} {x ⊔ y} {x ⊓ (x ⊔ y)} refl + x⊓x≤x⊓x⊔y = ⊓-mono-≤ {x} {x} ≤-refl (max-bound₁ {x} {y} {x ⊔ y} refl) -- >:( helper : x ⊓ x ≤ x ⊓ (x ⊔ y) → x ⊓ x ≡ x → x ≤ x ⊓ (x ⊔ y) @@ -279,8 +137,8 @@ module LatticeInstances where 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)) + x≤x⊔x⊓y = max-bound₁ {x} {x ⊓ y} {x ⊔ (x ⊓ y)} refl + x⊔x⊓y≤x⊔x = ⊔-mono-≤ {x} {x} ≤-refl (min-bound₁ {x} {y} {x ⊓ y} refl) -- >:( helper : x ⊔ (x ⊓ y) ≤ x ⊔ x → x ⊔ x ≡ x → x ⊔ (x ⊓ y) ≤ x @@ -288,8 +146,7 @@ module LatticeInstances where NatLattice : Lattice ℕ NatLattice = record - { _≼_ = _≤_ - ; _⊔_ = _⊔_ + { _⊔_ = _⊔_ ; _⊓_ = _⊓_ ; isLattice = record { joinSemilattice = Semilattice.isSemilattice NatMaxSemilattice @@ -301,27 +158,13 @@ module LatticeInstances where module ForProd {a} {A B : Set a} (lA : Lattice A) (lB : Lattice B) where private - _≼₁_ = Lattice._≼_ lA - _≼₂_ = Lattice._≼_ lB + 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 } - _⊔₁_ = 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 @@ -341,8 +184,7 @@ module LatticeInstances where ProdLattice : Lattice (A × B) ProdLattice = record - { _≼_ = _≼_ - ; _⊔_ = _⊔_ + { _⊔_ = _⊔_ ; _⊓_ = _⊓_ ; isLattice = record { joinSemilattice = Semilattice.isSemilattice ProdJoin.ProdSemilattice