Prove that the bottom map's valyes are all bottoms

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-05-09 20:48:32 -07:00
parent b78cb91f2a
commit 69d1ecebae

View File

@ -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 Data.List.Relation.Unary.Any using (Any; here; there)
open import Relation.Nullary using (¬_) open import Relation.Nullary using (¬_)
open import Isomorphism using (IsInverseˡ; IsInverseʳ) open import Isomorphism using (IsInverseˡ; IsInverseʳ)
open import Chain using (Height)
open import Lattice.Map ≡-dec-A lB open import Lattice.Map ≡-dec-A lB
using using
@ -104,6 +105,14 @@ module IterProdIsomorphism where
_∈ᵐ_ : {ks : List A} A × B FiniteMap ks Set _∈ᵐ_ : {ks : List A} A × B FiniteMap ks Set
_∈ᵐ_ {ks} = _∈_ ks _∈ᵐ_ {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 -- The left inverse is: from (to x) = x
from-to-inverseˡ : {ks : List A} (uks : Unique ks) from-to-inverseˡ : {ks : List A} (uks : Unique ks)
IsInverseˡ (_≈ᵐ_ {ks}) (_≈ⁱᵖ_ {length ks}) IsInverseˡ (_≈ᵐ_ {ks}) (_≈ⁱᵖ_ {length ks})
@ -407,3 +416,12 @@ module IterProdIsomorphism where
(to-⊔-distr uks) (from-⊔-distr {ks}) (to-⊔-distr uks) (from-⊔-distr {ks})
(from-to-inverseʳ uks) (from-to-inverseˡ uks) (from-to-inverseʳ uks) (from-to-inverseˡ uks)
using (isFiniteHeightLattice; finiteHeightLattice) public 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∈⊥