From 971d75bb2b666871993d6741939f3fde2a7334db Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 15 Jul 2023 14:40:11 -0700 Subject: [PATCH] Parameterize by equivalence type Signed-off-by: Danila Fedorin --- Lattice.agda | 117 ++++++++++++++++++++++++++++++++------------------- 1 file changed, 74 insertions(+), 43 deletions(-) diff --git a/Lattice.agda b/Lattice.agda index 18ef662..1873547 100644 --- a/Lattice.agda +++ b/Lattice.agda @@ -10,19 +10,26 @@ open import Agda.Primitive using (lsuc; Level) open import NatMap using (NatMap) -record IsSemilattice {a} (A : Set a) (_⊔_ : A → A → A) : Set a where - field - ⊔-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 +record IsSemilattice {a} (A : Set a) + (_≈_ : A → A → Set a) + (_⊔_ : A → A → A) : Set a where -record IsLattice {a} (A : Set a) (_⊔_ : A → A → A) (_⊓_ : A → A → A) : Set a where field - joinSemilattice : IsSemilattice A _⊔_ - meetSemilattice : IsSemilattice 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 - absorb-⊔-⊓ : (x y : A) → x ⊔ (x ⊓ y) ≡ x - absorb-⊓-⊔ : (x y : A) → x ⊓ (x ⊔ y) ≡ x +record IsLattice {a} (A : Set a) + (_≈_ : A → A → Set a) + (_⊔_ : A → A → A) + (_⊓_ : A → A → A) : Set a where + + field + joinSemilattice : IsSemilattice A _≈_ _⊔_ + meetSemilattice : IsSemilattice A _≈_ _⊓_ + + absorb-⊔-⊓ : (x y : A) → (x ⊔ (x ⊓ y)) ≈ x + absorb-⊓-⊔ : (x y : A) → (x ⊓ (x ⊔ y)) ≈ x open IsSemilattice joinSemilattice public open IsSemilattice meetSemilattice public renaming @@ -33,19 +40,21 @@ record IsLattice {a} (A : Set a) (_⊔_ : A → A → A) (_⊓_ : A → A → A) 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 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 @@ -55,14 +64,14 @@ module IsSemilatticeInstances where open NatProps open Eq - NatIsMaxSemilattice : IsSemilattice ℕ _⊔_ + NatIsMaxSemilattice : IsSemilattice ℕ _≡_ _⊔_ NatIsMaxSemilattice = record { ⊔-assoc = ⊔-assoc ; ⊔-comm = ⊔-comm ; ⊔-idemp = ⊔-idem } - NatIsMinSemilattice : IsSemilattice ℕ _⊓_ + NatIsMinSemilattice : IsSemilattice ℕ _≡_ _⊓_ NatIsMinSemilattice = record { ⊔-assoc = ⊓-assoc ; ⊔-comm = ⊓-comm @@ -70,32 +79,42 @@ module IsSemilatticeInstances where } module ForProd {a} {A B : Set a} + (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a) (_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B) - (sA : IsSemilattice A _⊔₁_) (sB : IsSemilattice B _⊔₂_) where + (sA : IsSemilattice A _≈₁_ _⊔₁_) (sB : IsSemilattice B _≈₂_ _⊔₂_) where open Eq open Data.Product private + 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₂) - ⊔-assoc : (p₁ p₂ p₃ : A × B) → (p₁ ⊔ p₂) ⊔ p₃ ≡ p₁ ⊔ (p₂ ⊔ p₃) - ⊔-assoc (a₁ , b₁) (a₂ , b₂) (a₃ , b₃) - rewrite IsSemilattice.⊔-assoc sA a₁ a₂ a₃ - rewrite IsSemilattice.⊔-assoc sB b₁ b₂ b₃ = refl + ⊔-assoc : (p₁ p₂ p₃ : A × B) → (p₁ ⊔ p₂) ⊔ p₃ ≈ p₁ ⊔ (p₂ ⊔ p₃) + ⊔-assoc (a₁ , b₁) (a₂ , b₂) (a₃ , b₃) = + ( IsSemilattice.⊔-assoc sA a₁ a₂ a₃ + , IsSemilattice.⊔-assoc sB b₁ b₂ b₃ + ) - ⊔-comm : (p₁ p₂ : A × B) → p₁ ⊔ p₂ ≡ p₂ ⊔ p₁ - ⊔-comm (a₁ , b₁) (a₂ , b₂) - rewrite IsSemilattice.⊔-comm sA a₁ a₂ - rewrite IsSemilattice.⊔-comm sB b₁ b₂ = refl + ⊔-comm : (p₁ p₂ : A × B) → p₁ ⊔ p₂ ≈ p₂ ⊔ p₁ + ⊔-comm (a₁ , b₁) (a₂ , b₂) = + ( IsSemilattice.⊔-comm sA a₁ a₂ + , IsSemilattice.⊔-comm sB b₁ b₂ + ) - ⊔-idemp : (p : A × B) → p ⊔ p ≡ p - ⊔-idemp (a , b) - rewrite IsSemilattice.⊔-idemp sA a - rewrite IsSemilattice.⊔-idemp sB b = refl + ⊔-idemp : (p : A × B) → p ⊔ p ≈ p + ⊔-idemp (a , b) = + ( IsSemilattice.⊔-idemp sA a + , IsSemilattice.⊔-idemp sB b + ) - ProdIsSemilattice : IsSemilattice (A × B) _⊔_ + ProdIsSemilattice : IsSemilattice (A × B) _≈_ _⊔_ ProdIsSemilattice = record { ⊔-assoc = ⊔-assoc ; ⊔-comm = ⊔-comm @@ -112,10 +131,13 @@ module IsLatticeInstances 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) + 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) + 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)) @@ -137,7 +159,7 @@ module IsLatticeInstances 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 - NatIsLattice : IsLattice ℕ _⊔_ _⊓_ + NatIsLattice : IsLattice ℕ _≡_ _⊔_ _⊓_ NatIsLattice = record { joinSemilattice = NatIsMaxSemilattice ; meetSemilattice = NatIsMinSemilattice @@ -146,13 +168,20 @@ module IsLatticeInstances where } module ForProd {a} {A B : Set a} + (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a) (_⊔₁_ : A → A → A) (_⊓₁_ : A → A → A) (_⊔₂_ : 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 ProdMeet = IsSemilatticeInstances.ForProd _⊓₁_ _⊓₂_ (IsLattice.meetSemilattice lA) (IsLattice.meetSemilattice lB) + module ProdJoin = IsSemilatticeInstances.ForProd _≈₁_ _≈₂_ _⊔₁_ _⊔₂_ (IsLattice.joinSemilattice lA) (IsLattice.joinSemilattice lB) + module ProdMeet = IsSemilatticeInstances.ForProd _≈₁_ _≈₂_ _⊓₁_ _⊓₂_ (IsLattice.meetSemilattice lA) (IsLattice.meetSemilattice lB) + + 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₂) @@ -164,17 +193,19 @@ module IsLatticeInstances where open Data.Product private - absorb-⊔-⊓ : (p₁ p₂ : A × B) → p₁ ⊔ (p₁ ⊓ p₂) ≡ p₁ - absorb-⊔-⊓ (a₁ , b₁) (a₂ , b₂) - 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₂) = + ( IsLattice.absorb-⊔-⊓ lA a₁ a₂ + , IsLattice.absorb-⊔-⊓ lB b₁ b₂ + ) - absorb-⊓-⊔ : (p₁ p₂ : A × B) → p₁ ⊓ (p₁ ⊔ p₂) ≡ p₁ - absorb-⊓-⊔ (a₁ , b₁) (a₂ , b₂) - 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₂) = + ( IsLattice.absorb-⊓-⊔ lA a₁ a₂ + , IsLattice.absorb-⊓-⊔ lB b₁ b₂ + ) - ProdIsLattice : IsLattice (A × B) _⊔_ _⊓_ + ProdIsLattice : IsLattice (A × B) _≈_ _⊔_ _⊓_ ProdIsLattice = record { joinSemilattice = ProdJoin.ProdIsSemilattice ; meetSemilattice = ProdMeet.ProdIsSemilattice