Add an 'iterated product' lattice for A x A ... x A x B.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
33b7bc37f0
commit
7e5cc1b316
56
Lattice/IterProd.agda
Normal file
56
Lattice/IterProd.agda
Normal file
|
@ -0,0 +1,56 @@
|
|||
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 Data.Nat using (ℕ; suc)
|
||||
open import Data.Product using (_×_)
|
||||
open import Utils using (iterate)
|
||||
|
||||
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
|
||||
ALattice : Lattice A
|
||||
ALattice = record
|
||||
{ _≈_ = _≈₁_
|
||||
; _⊔_ = _⊔₁_
|
||||
; _⊓_ = _⊓₁_
|
||||
; isLattice = lA
|
||||
}
|
||||
|
||||
BLattice : Lattice B
|
||||
BLattice = record
|
||||
{ _≈_ = _≈₂_
|
||||
; _⊔_ = _⊔₂_
|
||||
; _⊓_ = _⊓₂_
|
||||
; isLattice = lB
|
||||
}
|
||||
|
||||
IterProdLattice : ∀ {k : ℕ} → Lattice (IterProd k)
|
||||
IterProdLattice {0} = BLattice
|
||||
IterProdLattice {suc k'} = record
|
||||
{ _≈_ = _≈_
|
||||
; _⊔_ = _⊔_
|
||||
; _⊓_ = _⊓_
|
||||
; isLattice = isLattice
|
||||
}
|
||||
where
|
||||
RightLattice : Lattice (IterProd k')
|
||||
RightLattice = IterProdLattice {k'}
|
||||
|
||||
open import Lattice.Prod
|
||||
_≈₁_ (Lattice._≈_ RightLattice)
|
||||
_⊔₁_ (Lattice._⊔_ RightLattice)
|
||||
_⊓₁_ (Lattice._⊓_ RightLattice)
|
||||
lA (Lattice.isLattice RightLattice)
|
||||
|
||||
-- Expose the computed definition in public.
|
||||
module _ (k : ℕ) where
|
||||
open Lattice.Lattice (IterProdLattice {k}) public
|
Loading…
Reference in New Issue
Block a user