From 69d1ecebae10ff01ff52b2b47a8267b9f3728b31 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Thu, 9 May 2024 20:48:32 -0700 Subject: [PATCH] Prove that the bottom map's valyes are all bottoms Signed-off-by: Danila Fedorin --- Lattice/FiniteValueMap.agda | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/Lattice/FiniteValueMap.agda b/Lattice/FiniteValueMap.agda index 1c60ac9..998807c 100644 --- a/Lattice/FiniteValueMap.agda +++ b/Lattice/FiniteValueMap.agda @@ -28,6 +28,7 @@ open import Data.List.Relation.Unary.All using (All) open import Data.List.Relation.Unary.Any using (Any; here; there) open import Relation.Nullary using (¬_) open import Isomorphism using (IsInverseˡ; IsInverseʳ) +open import Chain using (Height) open import Lattice.Map ≡-dec-A lB using @@ -104,6 +105,14 @@ module IterProdIsomorphism where _∈ᵐ_ : ∀ {ks : List A} → A × B → FiniteMap ks → Set _∈ᵐ_ {ks} = _∈_ ks + to-build : ∀ {b : B} {ks : List A} (uks : Unique ks) → + let fm = to uks (IP.build b tt (length ks)) + in ∀ (k : A) (v : B) → (k , v) ∈ᵐ fm → v ≡ b + to-build {b} {k ∷ ks'} (push _ uks') k v (here refl) = refl + to-build {b} {k ∷ ks'} (push _ uks') k' v (there k',v∈m') = + to-build {ks = ks'} uks' k' v k',v∈m' + + -- The left inverse is: from (to x) = x from-to-inverseˡ : ∀ {ks : List A} (uks : Unique ks) → IsInverseˡ (_≈ᵐ_ {ks}) (_≈ⁱᵖ_ {length ks}) @@ -407,3 +416,12 @@ module IterProdIsomorphism where (to-⊔-distr uks) (from-⊔-distr {ks}) (from-to-inverseʳ uks) (from-to-inverseˡ uks) using (isFiniteHeightLattice; finiteHeightLattice) public + + -- Helpful lemma: all entries of the 'bottom' map are assigned to bottom. + + open Height (IsFiniteHeightLattice.fixedHeight isFiniteHeightLattice) using (⊥) + + ⊥-contains-bottoms : ∀ {k : A} {v : B} → (k , v) ∈ᵐ ⊥ → v ≡ (Height.⊥ fhB) + ⊥-contains-bottoms {k} {v} k,v∈⊥ + rewrite IP.⊥-built (length ks) ≈₂-dec ≈ᵘ-dec h₂ 0 fhB fixedHeightᵘ = + to-build uks k v k,v∈⊥