agda-spa/Lattice/IterProd.agda

117 lines
4.2 KiB
Agda
Raw Normal View History

open import Lattice
-- Due to universe levels, it becomes relatively annoying to handle the case
-- where the levels of A and B are not the same. For the time being, constrain
-- them to be the same.
module Lattice.IterProd {a} {A B : Set a}
(_≈₁_ : A A Set a) (_≈₂_ : B B Set a)
(_⊔₁_ : A A A) (_⊔₂_ : B B B)
(_⊓₁_ : A A A) (_⊓₂_ : B B B)
(lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_) (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
open import Agda.Primitive using (lsuc)
open import Data.Nat using (; suc; _+_)
open import Data.Product using (_×_)
open import Utils using (iterate)
open IsLattice lA renaming (FixedHeight to FixedHeight₁)
open IsLattice lB renaming (FixedHeight to FixedHeight₂)
IterProd : Set a
IterProd k = iterate k (λ t A × t) B
-- To make iteration more convenient, package the definitions in Lattice
-- records, perform the recursion, and unpackage.
module _ where
lattice : {k : } Lattice (IterProd k)
lattice {0} = record
{ _≈_ = _≈₂_
; _⊔_ = _⊔₂_
; _⊓_ = _⊓₂_
; isLattice = lB
}
lattice {suc k'} = record
{ _≈_ = _≈_
; _⊔_ = _⊔_
; _⊓_ = _⊓_
; isLattice = isLattice
}
where
Right : Lattice (IterProd k')
Right = lattice {k'}
open import Lattice.Prod
_≈₁_ (Lattice._≈_ Right)
_⊔₁_ (Lattice._⊔_ Right)
_⊓₁_ (Lattice._⊓_ Right)
lA (Lattice.isLattice Right)
module _ (k : ) where
open Lattice.Lattice (lattice {k}) public
module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
(h₁ h₂ : )
(fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where
private module _ where
record FiniteHeightAndDecEq (A : Set a) : Set (lsuc a) where
field
height :
_≈_ : A A Set a
_⊔_ : A A A
_⊓_ : A A A
isFiniteHeightLattice : IsFiniteHeightLattice A height _≈_ _⊔_ _⊓_
≈-dec : IsDecidable _≈_
open IsFiniteHeightLattice isFiniteHeightLattice public
finiteHeightAndDec : {k : } FiniteHeightAndDecEq (IterProd k)
finiteHeightAndDec {0} = record
{ height = h₂
; _≈_ = _≈₂_
; _⊔_ = _⊔₂_
; _⊓_ = _⊓₂_
; isFiniteHeightLattice = record
{ isLattice = lB
; fixedHeight = fhB
}
; ≈-dec = ≈₂-dec
}
finiteHeightAndDec {suc k'} = record
{ height = h₁ + FiniteHeightAndDecEq.height Right
; _≈_ = P._≈_
; _⊔_ = P._⊔_
; _⊓_ = P._⊓_
; isFiniteHeightLattice = isFiniteHeightLattice
≈₁-dec (FiniteHeightAndDecEq.≈-dec Right)
h₁ (FiniteHeightAndDecEq.height Right)
fhA (IsFiniteHeightLattice.fixedHeight (FiniteHeightAndDecEq.isFiniteHeightLattice Right))
; ≈-dec = ≈-dec ≈₁-dec (FiniteHeightAndDecEq.≈-dec Right)
}
where
Right = finiteHeightAndDec {k'}
open import Lattice.Prod
_≈₁_ (FiniteHeightAndDecEq._≈_ Right)
_⊔₁_ (FiniteHeightAndDecEq._⊔_ Right)
_⊓₁_ (FiniteHeightAndDecEq._⊓_ Right)
lA (FiniteHeightAndDecEq.isLattice Right) as P
module _ (k : ) where
open FiniteHeightAndDecEq (finiteHeightAndDec {k}) using (isFiniteHeightLattice) public
private
FHD = finiteHeightAndDec {k}
finiteHeightLattice : FiniteHeightLattice (IterProd k)
finiteHeightLattice = record
{ height = FiniteHeightAndDecEq.height FHD
; _≈_ = FiniteHeightAndDecEq._≈_ FHD
; _⊔_ = FiniteHeightAndDecEq._⊔_ FHD
; _⊓_ = FiniteHeightAndDecEq._⊓_ FHD
; isFiniteHeightLattice = isFiniteHeightLattice
}