Switch product to using instances
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
70847d51db
commit
cf824dc744
@ -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
|
||||
|
||||
@ -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
|
||||
}
|
||||
|
||||
Loading…
Reference in New Issue
Block a user