Prove that the iterated product is made from iterated bottom elements

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-05-09 19:45:15 -07:00
parent 6857f60465
commit 95669b2c65

View File

@ -11,8 +11,8 @@ module Lattice.IterProd {a} {A B : Set a}
(lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_) (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where (lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_) (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
open import Agda.Primitive using (lsuc) open import Agda.Primitive using (lsuc)
open import Data.Nat using (; suc; _+_) open import Data.Nat using (; zero; suc; _+_)
open import Data.Product using (_×_) open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Utils using (iterate) open import Utils using (iterate)
open IsLattice lA renaming (FixedHeight to FixedHeight₁) open IsLattice lA renaming (FixedHeight to FixedHeight₁)
@ -30,31 +30,50 @@ IterProd k = iterate k (λ t → A × t) B
-- that are built up by the two iterations. So, do everything in one iteration. -- that are built up by the two iterations. So, do everything in one iteration.
-- This requires some odd code. -- This requires some odd code.
build : A B (k : ) IterProd k
build _ b zero = b
build a b (suc s) = (a , build a b s)
private private
record RequiredForFixedHeight : Set (lsuc a) where record RequiredForFixedHeight : Set (lsuc a) where
field field
≈₁-dec : IsDecidable _≈₁_ ≈₁-dec : IsDecidable _≈₁_
≈₂-dec : IsDecidable _≈₂_ ≈₂-dec : IsDecidable _≈₂_
h₁ h₂ : h₁ h₂ :
fhA : FixedHeight₁ h₁ fhA : FixedHeight₁ h₁
fhB : FixedHeight₂ h₂ fhB : FixedHeight₂ h₂
record IsFiniteHeightAndDecEq {A : Set a} {_≈_ : A A Set a} {_⊔_ : A A A} {_⊓_ : A A A} (isLattice : IsLattice A _≈_ _⊔_ _⊓_) : Set (lsuc a) where ⊥₁ : A
⊥₁ = proj₁ (proj₁ (proj₁ fhA))
⊥₂ : B
⊥₂ = proj₁ (proj₁ (proj₁ fhB))
⊥k : (k : ) IterProd k
⊥k = build ⊥₁ ⊥₂
record IsFiniteHeightWithBotAndDecEq {A : Set a} {_≈_ : A A Set a} {_⊔_ : A A A} {_⊓_ : A A A} (isLattice : IsLattice A _≈_ _⊔_ _⊓_) ( : A) : Set (lsuc a) where
field field
height : height :
fixedHeight : IsLattice.FixedHeight isLattice height fixedHeight : IsLattice.FixedHeight isLattice height
≈-dec : IsDecidable _≈_ ≈-dec : IsDecidable _≈_
record Everything (A : Set a) : Set (lsuc a) where ⊥-correct : proj₁ (proj₁ (proj₁ fixedHeight))
record Everything (k : ) : Set (lsuc a) where
T = IterProd k
field field
_≈_ : A A Set a _≈_ : T T Set a
_⊔_ : A A A _⊔_ : T T T
_⊓_ : A A A _⊓_ : T T T
isLattice : IsLattice A _≈_ _⊔_ _⊓_ isLattice : IsLattice T _≈_ _⊔_ _⊓_
isFiniteHeightIfSupported : RequiredForFixedHeight IsFiniteHeightAndDecEq isLattice isFiniteHeightIfSupported :
(req : RequiredForFixedHeight)
IsFiniteHeightWithBotAndDecEq isLattice (RequiredForFixedHeight.⊥k req k)
everything : (k : ) Everything (IterProd k) everything : (k : ) Everything k
everything 0 = record everything 0 = record
{ _≈_ = _≈₂_ { _≈_ = _≈₂_
; _⊔_ = _⊔₂_ ; _⊔_ = _⊔₂_
@ -64,6 +83,7 @@ private
{ height = RequiredForFixedHeight.h₂ req { height = RequiredForFixedHeight.h₂ req
; fixedHeight = RequiredForFixedHeight.fhB req ; fixedHeight = RequiredForFixedHeight.fhB req
; ≈-dec = RequiredForFixedHeight.≈₂-dec req ; ≈-dec = RequiredForFixedHeight.≈₂-dec req
; ⊥-correct = IsLattice.≈-refl lB
} }
} }
everything (suc k') = record everything (suc k') = record
@ -76,13 +96,14 @@ private
fhlRest = Everything.isFiniteHeightIfSupported everythingRest req fhlRest = Everything.isFiniteHeightIfSupported everythingRest req
in in
record record
{ height = (RequiredForFixedHeight.h₁ req) + IsFiniteHeightAndDecEq.height fhlRest { height = (RequiredForFixedHeight.h₁ req) + IsFiniteHeightWithBotAndDecEq.height fhlRest
; fixedHeight = ; fixedHeight =
P.fixedHeight P.fixedHeight
(RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightAndDecEq.≈-dec fhlRest) (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightWithBotAndDecEq.≈-dec fhlRest)
(RequiredForFixedHeight.h₁ req) (IsFiniteHeightAndDecEq.height fhlRest) (RequiredForFixedHeight.h₁ req) (IsFiniteHeightWithBotAndDecEq.height fhlRest)
(RequiredForFixedHeight.fhA req) (IsFiniteHeightAndDecEq.fixedHeight fhlRest) (RequiredForFixedHeight.fhA req) (IsFiniteHeightWithBotAndDecEq.fixedHeight fhlRest)
; ≈-dec = P.≈-dec (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightAndDecEq.≈-dec fhlRest) ; ≈-dec = P.≈-dec (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightWithBotAndDecEq.≈-dec fhlRest)
; ⊥-correct = (IsLattice.≈-refl lA , IsFiniteHeightWithBotAndDecEq.⊥-correct fhlRest)
} }
} }
where where
@ -121,14 +142,16 @@ module _ (k : ) where
; fhB = fhB ; fhB = fhB
} }
fixedHeight = IsFiniteHeightWithBotAndDecEq.fixedHeight (Everything.isFiniteHeightIfSupported (everything k) required)
isFiniteHeightLattice = record isFiniteHeightLattice = record
{ isLattice = isLattice { isLattice = isLattice
; fixedHeight = IsFiniteHeightAndDecEq.fixedHeight (Everything.isFiniteHeightIfSupported (everything k) required) ; fixedHeight = fixedHeight
} }
finiteHeightLattice : FiniteHeightLattice (IterProd k) finiteHeightLattice : FiniteHeightLattice (IterProd k)
finiteHeightLattice = record finiteHeightLattice = record
{ height = IsFiniteHeightAndDecEq.height (Everything.isFiniteHeightIfSupported (everything k) required) { height = IsFiniteHeightWithBotAndDecEq.height (Everything.isFiniteHeightIfSupported (everything k) required)
; _≈_ = _≈_ ; _≈_ = _≈_
; _⊔_ = _⊔_ ; _⊔_ = _⊔_
; _⊓_ = _⊓_ ; _⊓_ = _⊓_