DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Strengthen lemma about IterProd bottom to definition equality

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-05-09 20:20:11 -07:00
parent 16fa4cd1d8
commit b78cb91f2a
1 changed files with 10 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
Lattice/IterProd.agda
View File

@ -13,6 +13,7 @@ module Lattice.IterProd {a} {A B : Set a}
open import Agda.Primitive using (lsuc) open import Agda.Primitive using (lsuc)
open import Data.Nat using (ℕ; zero; suc; _+_) open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Product using (_×_; _,_; proj₁; proj₂) open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; cong)
open import Utils using (iterate) open import Utils using (iterate)
open import Chain using (Height) open import Chain using (Height)
@ -59,7 +60,7 @@ private
fixedHeight : IsLattice.FixedHeight isLattice height fixedHeight : IsLattice.FixedHeight isLattice height
≈-dec : IsDecidable _≈_ ≈-dec : IsDecidable _≈_
⊥-correct : Height.⊥ fixedHeight ≈ ⊥ ⊥-correct : Height.⊥ fixedHeight ≡ ⊥
record Everything (k : ℕ) : Set (lsuc a) where record Everything (k : ℕ) : Set (lsuc a) where
T = IterProd k T = IterProd k
@ -84,7 +85,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 ; ⊥-correct = refl
} }
} }
everything (suc k') = record everything (suc k') = record
@ -104,7 +105,9 @@ private
(RequiredForFixedHeight.h₁ req) (IsFiniteHeightWithBotAndDecEq.height fhlRest) (RequiredForFixedHeight.h₁ req) (IsFiniteHeightWithBotAndDecEq.height fhlRest)
(RequiredForFixedHeight.fhA req) (IsFiniteHeightWithBotAndDecEq.fixedHeight fhlRest) (RequiredForFixedHeight.fhA req) (IsFiniteHeightWithBotAndDecEq.fixedHeight fhlRest)
; ≈-dec = P.≈-dec (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightWithBotAndDecEq.≈-dec fhlRest) ; ≈-dec = P.≈-dec (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightWithBotAndDecEq.≈-dec fhlRest)
; ⊥-correct = (IsLattice.≈-refl lA , IsFiniteHeightWithBotAndDecEq.⊥-correct fhlRest) ; ⊥-correct =
cong ((Height.⊥ (RequiredForFixedHeight.fhA req)) ,_)
(IsFiniteHeightWithBotAndDecEq.⊥-correct fhlRest)
} }
} }
where where
@ -158,3 +161,7 @@ module _ (k : ℕ) where
; _⊓_ = _⊓_ ; _⊓_ = _⊓_
; isFiniteHeightLattice = isFiniteHeightLattice ; isFiniteHeightLattice = isFiniteHeightLattice
} }
⊥-built : Height.⊥ fixedHeight ≡ (build (Height.⊥ fhA) (Height.⊥ fhB) k)
⊥-built = IsFiniteHeightWithBotAndDecEq.⊥-correct (Everything.isFiniteHeightIfSupported (everything k) required)