From cf824dc7443ce9ff78127200d4886838114e310c Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 4 Jan 2025 21:33:59 -0800 Subject: [PATCH] Switch product to using instances Signed-off-by: Danila Fedorin --- Lattice/IterProd.agda | 22 +++---- Lattice/Prod.agda | 134 ++++++++++++++++++++++-------------------- 2 files changed, 77 insertions(+), 79 deletions(-) diff --git a/Lattice/IterProd.agda b/Lattice/IterProd.agda index a3e3acb..b63f67a 100644 --- a/Lattice/IterProd.agda +++ b/Lattice/IterProd.agda @@ -40,11 +40,11 @@ build a b (suc s) = (a , build a b s) private record RequiredForFixedHeight : Set (lsuc a) where field - ≈₁-Decidable : IsDecidable _≈₁_ - ≈₂-Decidable : IsDecidable _≈₂_ + {{≈₁-Decidable}} : IsDecidable _≈₁_ + {{≈₂-Decidable}} : IsDecidable _≈₂_ h₁ h₂ : ℕ - fhA : FixedHeight₁ h₁ - fhB : FixedHeight₂ h₂ + {{fhA}} : FixedHeight₁ h₁ + {{fhB}} : FixedHeight₂ h₂ ⊥₁ : A ⊥₁ = Height.⊥ fhA @@ -102,10 +102,9 @@ private { height = (RequiredForFixedHeight.h₁ req) + IsFiniteHeightWithBotAndDecEq.height fhlRest ; fixedHeight = P.fixedHeight - (RequiredForFixedHeight.≈₁-Decidable req) (IsFiniteHeightWithBotAndDecEq.≈-Decidable fhlRest) - (RequiredForFixedHeight.h₁ req) (IsFiniteHeightWithBotAndDecEq.height fhlRest) - (RequiredForFixedHeight.fhA req) (IsFiniteHeightWithBotAndDecEq.fixedHeight fhlRest) - ; ≈-Decidable = P.≈-Decidable (RequiredForFixedHeight.≈₁-Decidable req) (IsFiniteHeightWithBotAndDecEq.≈-Decidable fhlRest) + {{≈₂-Decidable = IsFiniteHeightWithBotAndDecEq.≈-Decidable fhlRest}} + {{fhB = IsFiniteHeightWithBotAndDecEq.fixedHeight fhlRest}} + ; ≈-Decidable = P.≈-Decidable {{≈₂-Decidable = IsFiniteHeightWithBotAndDecEq.≈-Decidable fhlRest}} ; ⊥-correct = cong ((Height.⊥ (RequiredForFixedHeight.fhA req)) ,_) (IsFiniteHeightWithBotAndDecEq.⊥-correct fhlRest) @@ -113,12 +112,7 @@ private } where everythingRest = everything k' - - import Lattice.Prod - _≈₁_ (Everything._≈_ everythingRest) - _⊔₁_ (Everything._⊔_ everythingRest) - _⊓₁_ (Everything._⊓_ everythingRest) - lA (Everything.isLattice everythingRest) as P + import Lattice.Prod A (IterProd k') {{lB = Everything.isLattice everythingRest}} as P module _ {k : ℕ} where open Everything (everything k) using (_≈_; _⊔_; _⊓_) public diff --git a/Lattice/Prod.agda b/Lattice/Prod.agda index 87bc45a..b5c9628 100644 --- a/Lattice/Prod.agda +++ b/Lattice/Prod.agda @@ -1,10 +1,10 @@ open import Lattice -module Lattice.Prod {a b} {A : Set a} {B : Set b} - (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set b) - (_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B) - (_⊓₁_ : A → A → A) (_⊓₂_ : B → B → B) - (lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_) (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where +module Lattice.Prod {a b} (A : Set a) (B : Set b) + {_≈₁_ : A → A → Set a} {_≈₂_ : B → B → Set b} + {_⊔₁_ : A → A → A} {_⊔₂_ : B → B → B} + {_⊓₁_ : A → A → A} {_⊓₂_ : B → B → B} + {{lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_}} {{lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_}} where open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_) open import Data.Nat using (ℕ; _≤_; _+_; suc) @@ -40,13 +40,14 @@ open IsLattice lB using () renaming _≈_ : A × B → A × B → Set (a ⊔ℓ b) (a₁ , b₁) ≈ (a₂ , b₂) = (a₁ ≈₁ a₂) × (b₁ ≈₂ b₂) -≈-equiv : IsEquivalence (A × B) _≈_ -≈-equiv = record - { ≈-refl = λ {p} → (≈₁-refl , ≈₂-refl) - ; ≈-sym = λ {p₁} {p₂} (a₁≈a₂ , b₁≈b₂) → (≈₁-sym a₁≈a₂ , ≈₂-sym b₁≈b₂) - ; ≈-trans = λ {p₁} {p₂} {p₃} (a₁≈a₂ , b₁≈b₂) (a₂≈a₃ , b₂≈b₃) → - ( ≈₁-trans a₁≈a₂ a₂≈a₃ , ≈₂-trans b₁≈b₂ b₂≈b₃ ) - } +instance + ≈-equiv : IsEquivalence (A × B) _≈_ + ≈-equiv = record + { ≈-refl = λ {p} → (≈₁-refl , ≈₂-refl) + ; ≈-sym = λ {p₁} {p₂} (a₁≈a₂ , b₁≈b₂) → (≈₁-sym a₁≈a₂ , ≈₂-sym b₁≈b₂) + ; ≈-trans = λ {p₁} {p₂} {p₃} (a₁≈a₂ , b₁≈b₂) (a₂≈a₃ , b₂≈b₃) → + ( ≈₁-trans a₁≈a₂ a₂≈a₃ , ≈₂-trans b₁≈b₂ b₂≈b₃ ) + } _⊔_ : A × B → A × B → A × B (a₁ , b₁) ⊔ (a₂ , b₂) = (a₁ ⊔₁ a₂ , b₁ ⊔₂ b₂) @@ -76,35 +77,36 @@ private module ProdIsSemilattice (f₁ : A → A → A) (f₂ : B → B → B) ( ) } -isJoinSemilattice : IsSemilattice (A × B) _≈_ _⊔_ -isJoinSemilattice = ProdIsSemilattice.isSemilattice _⊔₁_ _⊔₂_ joinSemilattice₁ joinSemilattice₂ +instance + isJoinSemilattice : IsSemilattice (A × B) _≈_ _⊔_ + isJoinSemilattice = ProdIsSemilattice.isSemilattice _⊔₁_ _⊔₂_ joinSemilattice₁ joinSemilattice₂ -isMeetSemilattice : IsSemilattice (A × B) _≈_ _⊓_ -isMeetSemilattice = ProdIsSemilattice.isSemilattice _⊓₁_ _⊓₂_ meetSemilattice₁ meetSemilattice₂ + isMeetSemilattice : IsSemilattice (A × B) _≈_ _⊓_ + isMeetSemilattice = ProdIsSemilattice.isSemilattice _⊓₁_ _⊓₂_ meetSemilattice₁ meetSemilattice₂ -isLattice : IsLattice (A × B) _≈_ _⊔_ _⊓_ -isLattice = record - { joinSemilattice = isJoinSemilattice - ; meetSemilattice = isMeetSemilattice - ; absorb-⊔-⊓ = λ (a₁ , b₁) (a₂ , b₂) → - ( 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₂ - ) - } + isLattice : IsLattice (A × B) _≈_ _⊔_ _⊓_ + isLattice = record + { joinSemilattice = isJoinSemilattice + ; meetSemilattice = isMeetSemilattice + ; absorb-⊔-⊓ = λ (a₁ , b₁) (a₂ , b₂) → + ( 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₂ + ) + } -lattice : Lattice (A × B) -lattice = record - { _≈_ = _≈_ - ; _⊔_ = _⊔_ - ; _⊓_ = _⊓_ - ; isLattice = isLattice - } + lattice : Lattice (A × B) + lattice = record + { _≈_ = _≈_ + ; _⊔_ = _⊔_ + ; _⊓_ = _⊓_ + ; isLattice = isLattice + } -module _ (≈₁-Decidable : IsDecidable _≈₁_) (≈₂-Decidable : IsDecidable _≈₂_) where +module _ {{≈₁-Decidable : IsDecidable _≈₁_}} {{≈₂-Decidable : IsDecidable _≈₂_}} where open IsDecidable ≈₁-Decidable using () renaming (R-dec to ≈₁-dec) open IsDecidable ≈₂-Decidable using () renaming (R-dec to ≈₂-dec) @@ -115,11 +117,12 @@ module _ (≈₁-Decidable : IsDecidable _≈₁_) (≈₂-Decidable : IsDecidab ... | no a₁̷≈a₂ | _ = no (λ (a₁≈a₂ , _) → a₁̷≈a₂ a₁≈a₂) ... | _ | no b₁̷≈b₂ = no (λ (_ , b₁≈b₂) → b₁̷≈b₂ b₁≈b₂) - ≈-Decidable : IsDecidable _≈_ - ≈-Decidable = record { R-dec = ≈-dec } + instance + ≈-Decidable : IsDecidable _≈_ + ≈-Decidable = record { R-dec = ≈-dec } - module _ (h₁ h₂ : ℕ) - (fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where + module _ {h₁ h₂ : ℕ} + {{fhA : FixedHeight₁ h₁}} {{fhB : FixedHeight₂ h₂}} where open import Data.Nat.Properties open IsLattice isLattice using (_≼_; _≺_; ≺-cong) @@ -167,29 +170,30 @@ module _ (≈₁-Decidable : IsDecidable _≈₁_) (≈₂-Decidable : IsDecidab , m≤n⇒m≤o+n 1 (subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂)) )) - fixedHeight : IsLattice.FixedHeight isLattice (h₁ + h₂) - fixedHeight = record - { ⊥ = (⊥₁ , ⊥₂) - ; ⊤ = (⊤₁ , ⊤₂) - ; longestChain = concat - (ChainMapping₁.Chain-map (λ a → (a , ⊥₂)) (∙,b-Monotonic _) proj₁ (∙,b-Preserves-≈₁ _) longestChain₁) - (ChainMapping₂.Chain-map (λ b → (⊤₁ , b)) (a,∙-Monotonic _) proj₂ (a,∙-Preserves-≈₂ _) longestChain₂) - ; bounded = λ a₁b₁a₂b₂ → - let ((n₁ , n₂) , ((a₁a₂ , b₁b₂) , n≤n₁+n₂)) = unzip a₁b₁a₂b₂ - in ≤-trans n≤n₁+n₂ (+-mono-≤ (bounded₁ a₁a₂) (bounded₂ b₁b₂)) - } + instance + fixedHeight : IsLattice.FixedHeight isLattice (h₁ + h₂) + fixedHeight = record + { ⊥ = (⊥₁ , ⊥₂) + ; ⊤ = (⊤₁ , ⊤₂) + ; longestChain = concat + (ChainMapping₁.Chain-map (λ a → (a , ⊥₂)) (∙,b-Monotonic _) proj₁ (∙,b-Preserves-≈₁ _) longestChain₁) + (ChainMapping₂.Chain-map (λ b → (⊤₁ , b)) (a,∙-Monotonic _) proj₂ (a,∙-Preserves-≈₂ _) longestChain₂) + ; bounded = λ a₁b₁a₂b₂ → + let ((n₁ , n₂) , ((a₁a₂ , b₁b₂) , n≤n₁+n₂)) = unzip a₁b₁a₂b₂ + in ≤-trans n≤n₁+n₂ (+-mono-≤ (bounded₁ a₁a₂) (bounded₂ b₁b₂)) + } - isFiniteHeightLattice : IsFiniteHeightLattice (A × B) (h₁ + h₂) _≈_ _⊔_ _⊓_ - isFiniteHeightLattice = record - { isLattice = isLattice - ; fixedHeight = fixedHeight - } + isFiniteHeightLattice : IsFiniteHeightLattice (A × B) (h₁ + h₂) _≈_ _⊔_ _⊓_ + isFiniteHeightLattice = record + { isLattice = isLattice + ; fixedHeight = fixedHeight + } - finiteHeightLattice : FiniteHeightLattice (A × B) - finiteHeightLattice = record - { height = h₁ + h₂ - ; _≈_ = _≈_ - ; _⊔_ = _⊔_ - ; _⊓_ = _⊓_ - ; isFiniteHeightLattice = isFiniteHeightLattice - } + finiteHeightLattice : FiniteHeightLattice (A × B) + finiteHeightLattice = record + { height = h₁ + h₂ + ; _≈_ = _≈_ + ; _⊔_ = _⊔_ + ; _⊓_ = _⊓_ + ; isFiniteHeightLattice = isFiniteHeightLattice + }