Prove that finite value-maps are finite height
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
ca90f6509c
commit
ae09a27f64
|
|
@ -12,11 +12,12 @@ open import Function.Definitions using (Inverseˡ; Inverseʳ)
|
|||
module Lattice.FiniteValueMap (A : Set) (B : Set)
|
||||
(_≈₂_ : B → B → Set)
|
||||
(_⊔₂_ : B → B → B) (_⊓₂_ : B → B → B)
|
||||
(≈-dec-A : Decidable (_≡_ {_} {A}))
|
||||
(≡-dec-A : Decidable (_≡_ {_} {A}))
|
||||
(lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
|
||||
|
||||
open import Data.List using (List; length; []; _∷_; map)
|
||||
open import Data.List.Membership.Propositional using () renaming (_∈_ to _∈ˡ_)
|
||||
open import Data.Nat using (ℕ)
|
||||
open import Data.Product using (Σ; proj₁; proj₂; _×_)
|
||||
open import Data.Empty using (⊥-elim)
|
||||
open import Utils using (Unique; push; empty; All¬-¬Any)
|
||||
|
|
@ -26,14 +27,14 @@ 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 Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≈-dec-A lB using (subset-impl; locate; forget; _∈_; Map-functional; Expr-Provenance; _∩_; _∪_; `_; in₁; in₂; bothᵘ; single; ⊔-combines)
|
||||
open import Lattice.FiniteMap A B _≈₂_ _⊔₂_ _⊓₂_ ≈-dec-A lB public
|
||||
open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB using (subset-impl; locate; forget; _∈_; Map-functional; Expr-Provenance; _∩_; _∪_; `_; in₁; in₂; bothᵘ; single; ⊔-combines)
|
||||
open import Lattice.FiniteMap A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB public
|
||||
|
||||
module IterProdIsomorphism where
|
||||
open import Data.Unit using (⊤; tt)
|
||||
open import Lattice.Unit using () renaming (_≈_ to _≈ᵘ_; _⊔_ to _⊔ᵘ_; _⊓_ to _⊓ᵘ_; ≈-dec to ≈ᵘ-dec; isLattice to isLatticeᵘ; ≈-equiv to ≈ᵘ-equiv)
|
||||
open import Lattice.Unit using () renaming (_≈_ to _≈ᵘ_; _⊔_ to _⊔ᵘ_; _⊓_ to _⊓ᵘ_; ≈-dec to ≈ᵘ-dec; isLattice to isLatticeᵘ; ≈-equiv to ≈ᵘ-equiv; fixedHeight to fixedHeightᵘ)
|
||||
open import Lattice.IterProd _≈₂_ _≈ᵘ_ _⊔₂_ _⊔ᵘ_ _⊓₂_ _⊓ᵘ_ lB isLatticeᵘ as IP using (IterProd)
|
||||
open IsLattice lB using () renaming (≈-trans to ≈₂-trans; ≈-sym to ≈₂-sym)
|
||||
open IsLattice lB using () renaming (≈-trans to ≈₂-trans; ≈-sym to ≈₂-sym; FixedHeight to FixedHeight₂)
|
||||
|
||||
from : ∀ {ks : List A} → FiniteMap ks → IterProd (length ks)
|
||||
from {[]} (([] , _) , _) = tt
|
||||
|
|
@ -175,20 +176,20 @@ module IterProdIsomorphism where
|
|||
from-rest : ∀ {k : A} {ks : List A} (fm : FiniteMap (k ∷ ks)) → proj₂ (from fm) ≡ from (pop fm)
|
||||
from-rest (((_ ∷ fm') , push _ ufm') , refl) = refl
|
||||
|
||||
from-preserves-≈ : ∀ {ks : List A} → (fm₁ fm₂ : FiniteMap ks) → fm₁ ≈ᵐ fm₂ → (_≈ⁱᵖ_ {ks}) (from fm₁) (from fm₂)
|
||||
from-preserves-≈ {[]} (([] , _) , _) (([] , _) , _) _ = IsEquivalence.≈-refl ≈ᵘ-equiv
|
||||
from-preserves-≈ {k ∷ ks'} fm₁@(m₁ , _) fm₂@(m₂ , _) fm₁≈fm₂@(kvs₁⊆kvs₂ , kvs₂⊆kvs₁)
|
||||
from-preserves-≈ : ∀ {ks : List A} → {fm₁ fm₂ : FiniteMap ks} → fm₁ ≈ᵐ fm₂ → (_≈ⁱᵖ_ {ks}) (from fm₁) (from fm₂)
|
||||
from-preserves-≈ {[]} {([] , _) , _} {([] , _) , _} _ = IsEquivalence.≈-refl ≈ᵘ-equiv
|
||||
from-preserves-≈ {k ∷ ks'} {fm₁@(m₁ , _)} {fm₂@(m₂ , _)} fm₁≈fm₂@(kvs₁⊆kvs₂ , kvs₂⊆kvs₁)
|
||||
with first-key-in-map fm₁ | first-key-in-map fm₂ | from-first-value fm₁ | from-first-value fm₂
|
||||
... | (v₁ , k,v₁∈fm₁) | (v₂ , k,v₂∈fm₂) | refl | refl
|
||||
with kvs₁⊆kvs₂ _ _ k,v₁∈fm₁
|
||||
... | (v₁' , (v₁≈v₁' , k,v₁'∈fm₂))
|
||||
rewrite Map-functional {m = m₂} k,v₂∈fm₂ k,v₁'∈fm₂
|
||||
rewrite from-rest fm₁ rewrite from-rest fm₂
|
||||
= (v₁≈v₁' , from-preserves-≈ (pop fm₁) (pop fm₂) (pop-≈ fm₁ fm₂ fm₁≈fm₂))
|
||||
= (v₁≈v₁' , from-preserves-≈ {ks'} {pop fm₁} {pop fm₂} (pop-≈ fm₁ fm₂ fm₁≈fm₂))
|
||||
|
||||
to-preserves-≈ : ∀ {ks : List A} (uks : Unique ks) (ip₁ ip₂ : IterProd (length ks)) → _≈ⁱᵖ_ {ks} ip₁ ip₂ → to uks ip₁ ≈ᵐ to uks ip₂
|
||||
to-preserves-≈ {[]} empty tt tt _ = ((λ k v ()), (λ k v ()))
|
||||
to-preserves-≈ {k ∷ ks'} uks@(push k≢ks' uks') ip₁@(v₁ , rest₁) ip₂@(v₂ , rest₂) (v₁≈v₂ , rest₁≈rest₂) = (fm₁⊆fm₂ , fm₂⊆fm₁)
|
||||
to-preserves-≈ : ∀ {ks : List A} (uks : Unique ks) {ip₁ ip₂ : IterProd (length ks)} → _≈ⁱᵖ_ {ks} ip₁ ip₂ → to uks ip₁ ≈ᵐ to uks ip₂
|
||||
to-preserves-≈ {[]} empty {tt} {tt} _ = ((λ k v ()), (λ k v ()))
|
||||
to-preserves-≈ {k ∷ ks'} uks@(push k≢ks' uks') {ip₁@(v₁ , rest₁)} {ip₂@(v₂ , rest₂)} (v₁≈v₂ , rest₁≈rest₂) = (fm₁⊆fm₂ , fm₂⊆fm₁)
|
||||
where
|
||||
fm₁⊆fm₂ : to uks ip₁ ⊆ᵐ to uks ip₂
|
||||
fm₁⊆fm₂ k v k,v∈kvs₁
|
||||
|
|
@ -196,7 +197,7 @@ module IterProdIsomorphism where
|
|||
with ((fm'₂ , ufm'₂) , fm'₂≡ks') ← to uks' rest₂ in p₂
|
||||
with k,v∈kvs₁
|
||||
... | here refl = (v₂ , (v₁≈v₂ , here refl))
|
||||
... | there k,v∈fm'₁ with refl ← p₁ with refl ← p₂ = let (v' , (v≈v' , k,v'∈kvs₁)) = proj₁ (to-preserves-≈ uks' rest₁ rest₂ rest₁≈rest₂) k v k,v∈fm'₁ in (v' , (v≈v' , there k,v'∈kvs₁))
|
||||
... | there k,v∈fm'₁ with refl ← p₁ with refl ← p₂ = let (v' , (v≈v' , k,v'∈kvs₁)) = proj₁ (to-preserves-≈ uks' {rest₁} {rest₂} rest₁≈rest₂) k v k,v∈fm'₁ in (v' , (v≈v' , there k,v'∈kvs₁))
|
||||
|
||||
fm₂⊆fm₁ : to uks ip₂ ⊆ᵐ to uks ip₁
|
||||
fm₂⊆fm₁ k v k,v∈kvs₂
|
||||
|
|
@ -204,7 +205,7 @@ module IterProdIsomorphism where
|
|||
with ((fm'₂ , ufm'₂) , fm'₂≡ks') ← to uks' rest₂ in p₂
|
||||
with k,v∈kvs₂
|
||||
... | here refl = (v₁ , (IsLattice.≈-sym lB v₁≈v₂ , here refl))
|
||||
... | there k,v∈fm'₂ with refl ← p₁ with refl ← p₂ = let (v' , (v≈v' , k,v'∈kvs₂)) = proj₂ (to-preserves-≈ uks' rest₁ rest₂ rest₁≈rest₂) k v k,v∈fm'₂ in (v' , (v≈v' , there k,v'∈kvs₂))
|
||||
... | there k,v∈fm'₂ with refl ← p₁ with refl ← p₂ = let (v' , (v≈v' , k,v'∈kvs₂)) = proj₂ (to-preserves-≈ uks' {rest₁} {rest₂} rest₁≈rest₂) k v k,v∈fm'₂ in (v' , (v≈v' , there k,v'∈kvs₂))
|
||||
|
||||
from-⊔-distr : ∀ {ks : List A} → (fm₁ fm₂ : FiniteMap ks) → _≈ⁱᵖ_ {ks} (from (fm₁ ⊔ᵐ fm₂)) (_⊔ⁱᵖ_ {ks} (from fm₁) (from fm₂))
|
||||
from-⊔-distr {[]} fm₁ fm₂ = IsEquivalence.≈-refl ≈ᵘ-equiv
|
||||
|
|
@ -220,7 +221,7 @@ module IterProdIsomorphism where
|
|||
rewrite Map-functional {m = proj₁ (fm₁ ⊔ᵐ fm₂)} k,v∈fm₁fm₂ k,v₁⊔v₂∈m₁m₂
|
||||
rewrite from-rest (fm₁ ⊔ᵐ fm₂) rewrite from-rest fm₁ rewrite from-rest fm₂
|
||||
= ( IsLattice.≈-refl lB
|
||||
, IsEquivalence.≈-trans (IP.≈-equiv (length ks)) (from-preserves-≈ (pop (fm₁ ⊔ᵐ fm₂)) (pop fm₁ ⊔ᵐ pop fm₂) (pop-⊔-distr fm₁ fm₂)) ((from-⊔-distr (pop fm₁) (pop fm₂)))
|
||||
, IsEquivalence.≈-trans (IP.≈-equiv (length ks)) (from-preserves-≈ {_} {pop (fm₁ ⊔ᵐ fm₂)} {pop fm₁ ⊔ᵐ pop fm₂} (pop-⊔-distr fm₁ fm₂)) ((from-⊔-distr (pop fm₁) (pop fm₂)))
|
||||
)
|
||||
|
||||
|
||||
|
|
@ -262,3 +263,12 @@ module IterProdIsomorphism where
|
|||
in
|
||||
(v' , (v₁⊔v₂≈v' , there v'∈fm'))
|
||||
|
||||
module _ {ks : List A} (uks : Unique ks) (≈₂-dec : Decidable _≈₂_) (h₂ : ℕ) (fhB : FixedHeight₂ h₂) where
|
||||
import Isomorphism
|
||||
open Isomorphism.TransportFiniteHeight
|
||||
(IP.isFiniteHeightLattice (length ks) ≈₂-dec ≈ᵘ-dec h₂ 0 fhB fixedHeightᵘ) (isLattice ks)
|
||||
{f = to uks} {g = from {ks}}
|
||||
(to-preserves-≈ uks) (from-preserves-≈ {ks})
|
||||
(to-⊔-distr uks) (from-⊔-distr {ks})
|
||||
(from-to-inverseʳ uks) (from-to-inverseˡ uks)
|
||||
using (isFiniteHeightLattice) public
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user