From b78cb91f2addc18b5742bcaf2e480d8bd9f5c8c7 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Thu, 9 May 2024 20:20:11 -0700 Subject: [PATCH] Strengthen lemma about IterProd bottom to definition equality Signed-off-by: Danila Fedorin --- Lattice/IterProd.agda | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/Lattice/IterProd.agda b/Lattice/IterProd.agda index 249f58e..6841d59 100644 --- a/Lattice/IterProd.agda +++ b/Lattice/IterProd.agda @@ -13,6 +13,7 @@ module Lattice.IterProd {a} {A B : Set a} open import Agda.Primitive using (lsuc) open import Data.Nat using (ℕ; zero; suc; _+_) open import Data.Product using (_×_; _,_; proj₁; proj₂) +open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; cong) open import Utils using (iterate) open import Chain using (Height) @@ -59,7 +60,7 @@ private fixedHeight : IsLattice.FixedHeight isLattice height ≈-dec : IsDecidable _≈_ - ⊥-correct : Height.⊥ fixedHeight ≈ ⊥ + ⊥-correct : Height.⊥ fixedHeight ≡ ⊥ record Everything (k : ℕ) : Set (lsuc a) where T = IterProd k @@ -84,7 +85,7 @@ private { height = RequiredForFixedHeight.h₂ req ; fixedHeight = RequiredForFixedHeight.fhB req ; ≈-dec = RequiredForFixedHeight.≈₂-dec req - ; ⊥-correct = IsLattice.≈-refl lB + ; ⊥-correct = refl } } everything (suc k') = record @@ -104,7 +105,9 @@ private (RequiredForFixedHeight.h₁ req) (IsFiniteHeightWithBotAndDecEq.height fhlRest) (RequiredForFixedHeight.fhA req) (IsFiniteHeightWithBotAndDecEq.fixedHeight 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 @@ -158,3 +161,7 @@ module _ (k : ℕ) where ; _⊓_ = _⊓_ ; isFiniteHeightLattice = isFiniteHeightLattice } + + ⊥-built : Height.⊥ fixedHeight ≡ (build (Height.⊥ fhA) (Height.⊥ fhB) k) + ⊥-built = IsFiniteHeightWithBotAndDecEq.⊥-correct (Everything.isFiniteHeightIfSupported (everything k) required) +