agda-spa/Lattice/IterProd.agda
Danila Fedorin a920608bef Tweak IterProd to expose more (including a bundle)
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-02-11 20:45:14 -08:00

119 lines
4.3 KiB
Agda
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

open import Lattice
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.
private module _ where
BLattice : Lattice B
BLattice = record
{ _≈_ = _≈₂_
; _⊔_ = _⊔₂_
; _⊓_ = _⊓₂_
; isLattice = lB
}
IterProdLattice : {k : } Lattice (IterProd k)
IterProdLattice {0} = BLattice
IterProdLattice {suc k'} = record
{ _≈_ = _≈_
; _⊔_ = _⊔_
; _⊓_ = _⊓_
; isLattice = isLattice
}
where
Right : Lattice (IterProd k')
Right = IterProdLattice {k'}
open import Lattice.Prod
_≈₁_ (Lattice._≈_ Right)
_⊔₁_ (Lattice._⊔_ Right)
_⊓₁_ (Lattice._⊓_ Right)
lA (Lattice.isLattice Right)
module _ (k : ) where
open Lattice.Lattice (IterProdLattice {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
BFiniteHeightLattice : FiniteHeightAndDecEq B
BFiniteHeightLattice = record
{ height = h₂
; _≈_ = _≈₂_
; _⊔_ = _⊔₂_
; _⊓_ = _⊓₂_
; isFiniteHeightLattice = record
{ isLattice = lB
; fixedHeight = fhB
}
; ≈-dec = ≈₂-dec
}
IterProdFiniteHeightLattice : {k : } FiniteHeightAndDecEq (IterProd k)
IterProdFiniteHeightLattice {0} = BFiniteHeightLattice
IterProdFiniteHeightLattice {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 = IterProdFiniteHeightLattice {k'}
open import Lattice.Prod
_≈₁_ (FiniteHeightAndDecEq._≈_ Right)
_⊔₁_ (FiniteHeightAndDecEq._⊔_ Right)
_⊓₁_ (FiniteHeightAndDecEq._⊓_ Right)
lA (FiniteHeightAndDecEq.isLattice Right) as P
module _ (k : ) where
open FiniteHeightAndDecEq (IterProdFiniteHeightLattice {k}) using (isFiniteHeightLattice) public
private
FHD = IterProdFiniteHeightLattice {k}
finiteHeightLattice : FiniteHeightLattice (IterProd k)
finiteHeightLattice = record
{ height = FiniteHeightAndDecEq.height FHD
; _≈_ = FiniteHeightAndDecEq._≈_ FHD
; _⊔_ = FiniteHeightAndDecEq._⊔_ FHD
; _⊓_ = FiniteHeightAndDecEq._⊓_ FHD
; isFiniteHeightLattice = isFiniteHeightLattice
}