agda-spa/Lattice/FiniteValueMap.agda

413 lines
23 KiB
Agda
Raw Normal View History

-- Because iterated products currently require both A and B to be of the same
-- universe, and the FiniteMap is written in a universe-polymorphic way,
-- specialize the FiniteMap module with Set-typed types only.
open import Lattice
open import Equivalence
open import Relation.Binary.PropositionalEquality as Eq
using (_≡_; refl; sym; trans; cong; subst)
open import Relation.Binary.Definitions using (Decidable)
open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔_)
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}))
(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)
open import Data.Product using (_,_)
open import Data.List.Properties using (∷-injectiveʳ)
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 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
; fixedHeight to fixedHeightᵘ
)
open import Lattice.IterProd _≈₂_ _≈ᵘ_ _⊔₂_ _⊔ᵘ_ _⊓₂_ _⊓ᵘ_ lB isLatticeᵘ
as IP
using (IterProd)
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
from {k ks'} (((k' , v) fm' , push _ uks') , refl) =
(v , from ((fm' , uks'), refl))
to : {ks : List A} Unique ks IterProd (length ks) FiniteMap ks
to {[]} _ = (([] , empty) , refl)
to {k ks'} (push k≢ks' uks') (v , rest) =
let
((fm' , ufm') , fm'≡ks') = to uks' rest
-- This would be easier if we pattern matched on the equiality proof
-- to get refl, but that makes it harder to reason about 'to' when
-- the arguments are not known to be refl.
k≢fm' = subst (λ ks All (λ k' ¬ k k') ks) (sym fm'≡ks') k≢ks'
kvs≡ks = cong (k ∷_) fm'≡ks'
in
(((k , v) fm' , push k≢fm' ufm') , kvs≡ks)
private
_≈ᵐ_ : {ks : List A} FiniteMap ks FiniteMap ks Set
_≈ᵐ_ {ks} = _≈_ ks
_⊔ᵐ_ : {ks : List A} FiniteMap ks FiniteMap ks FiniteMap ks
_⊔ᵐ_ {ks} = _⊔_ ks
_⊆ᵐ_ : {ks₁ ks₂ : List A} FiniteMap ks₁ FiniteMap ks₂ Set
_⊆ᵐ_ fm₁ fm₂ = subset-impl (proj₁ (proj₁ fm₁)) (proj₁ (proj₁ fm₂))
_≈ⁱᵖ_ : {n : } IterProd n IterProd n Set
_≈ⁱᵖ_ {n} = IP._≈_ n
_⊔ⁱᵖ_ : {ks : List A}
IterProd (length ks) IterProd (length ks) IterProd (length ks)
_⊔ⁱᵖ_ {ks} = IP._⊔_ (length ks)
_∈ᵐ_ : {ks : List A} A × B FiniteMap ks Set
_∈ᵐ_ {ks} k,v fm = k,v proj₁ fm
-- The left inverse is: from (to x) = x
from-to-inverseˡ : {ks : List A} (uks : Unique ks)
IsInverseˡ (_≈ᵐ_ {ks}) (_≈ⁱᵖ_ {length ks})
(from {ks}) (to {ks} uks)
from-to-inverseˡ {[]} _ _ = IsEquivalence.≈-refl (IP.≈-equiv 0)
from-to-inverseˡ {k ks'} (push k≢ks' uks') (v , rest)
with ((fm' , ufm') , refl) to uks' rest in p rewrite sym p =
(IsLattice.≈-refl lB , from-to-inverseˡ {ks'} uks' rest)
-- the rewrite here is needed because the IH is in terms of `to uks' rest`,
-- but we end up with the 'unpacked' form (fm', ...). So, put it back
-- in the 'packed' form after we've performed enough inspection
-- to know we take the cons branch of `to`.
-- The map has its own uniqueness proof, but the call to 'to' needs a standalone
-- uniqueness proof too. Work with both proofs as needed to thread things through.
--
-- The right inverse is: to (from x) = x
from-to-inverseʳ : {ks : List A} (uks : Unique ks)
IsInverseʳ (_≈ᵐ_ {ks}) (_≈ⁱᵖ_ {length ks})
(from {ks}) (to {ks} uks)
from-to-inverseʳ {[]} _ (([] , empty) , kvs≡ks) rewrite kvs≡ks =
( (λ k v ())
, (λ k v ())
)
from-to-inverseʳ {k ks'} uks@(push _ uks'₁) fm₁@(((k , v) fm'₁ , push _ uks'₂) , refl)
with to uks'₁ (from ((fm'₁ , uks'₂) , refl))
| from-to-inverseʳ {ks'} uks'₁ ((fm'₁ , uks'₂) , refl)
... | ((fm'₂ , ufm'₂) , _)
| (fm'₂⊆fm'₁ , fm'₁⊆fm'₂) = (m₂⊆m₁ , m₁⊆m₂)
where
kvs₁ = (k , v) fm'₁
kvs₂ = (k , v) fm'₂
m₁⊆m₂ : subset-impl kvs₁ kvs₂
m₁⊆m₂ k' v' (here refl) =
(v' , (IsLattice.≈-refl lB , here refl))
m₁⊆m₂ k' v' (there k',v'∈fm'₁) =
let (v'' , (v'≈v'' , k',v''∈fm'₂)) =
fm'₁⊆fm'₂ k' v' k',v'∈fm'₁
in (v'' , (v'≈v'' , there k',v''∈fm'₂))
m₂⊆m₁ : subset-impl kvs₂ kvs₁
m₂⊆m₁ k' v' (here refl) =
(v' , (IsLattice.≈-refl lB , here refl))
m₂⊆m₁ k' v' (there k',v'∈fm'₂) =
let (v'' , (v'≈v'' , k',v''∈fm'₁)) =
fm'₂⊆fm'₁ k' v' k',v'∈fm'₂
in (v'' , (v'≈v'' , there k',v''∈fm'₁))
private
first-key-in-map : {k : A} {ks : List A} (fm : FiniteMap (k ks))
Σ B (λ v (k , v) proj₁ fm)
first-key-in-map (((k , v) _ , _) , refl) = (v , here refl)
from-first-value : {k : A} {ks : List A} (fm : FiniteMap (k ks))
proj₁ (from fm) proj₁ (first-key-in-map fm)
from-first-value {k} {ks} (((k , v) _ , push _ _) , refl) = refl
-- We need pop because reasoning about two distinct 'refl' pattern
-- matches is giving us unification errors. So, stash the 'refl' pattern
-- matching into a helper functions, and write solutions in terms
-- of that.
pop : {k : A} {ks : List A} FiniteMap (k ks) FiniteMap ks
pop (((_ fm') , push _ ufm') , refl) = ((fm' , ufm') , refl)
pop-≈ : {k : A} {ks : List A} (fm₁ fm₂ : FiniteMap (k ks))
fm₁ ≈ᵐ fm₂ pop fm₁ ≈ᵐ pop fm₂
pop-≈ {k} {ks} fm₁ fm₂ (fm₁⊆fm₂ , fm₂⊆fm₁) =
(narrow fm₁⊆fm₂ , narrow fm₂⊆fm₁)
where
narrow₁ : {fm₁ fm₂ : FiniteMap (k ks)}
fm₁ ⊆ᵐ fm₂ pop fm₁ ⊆ᵐ fm₂
narrow₁ {(_ _ , push _ _) , refl} kvs₁⊆kvs₂ k' v' k',v'∈fm'₁ =
kvs₁⊆kvs₂ k' v' (there k',v'∈fm'₁)
narrow₂ : {fm₁ : FiniteMap ks} {fm₂ : FiniteMap (k ks)}
fm₁ ⊆ᵐ fm₂ fm₁ ⊆ᵐ pop fm₂
narrow₂ {fm₁} {fm₂ = (_ fm'₂ , push k≢ks _) , kvs≡ks@refl} kvs₁⊆kvs₂ k' v' k',v'∈fm'₁
with kvs₁⊆kvs₂ k' v' k',v'∈fm'₁
... | (v'' , (v'≈v'' , here refl)) rewrite sym (proj₂ fm₁) =
⊥-elim (All¬-¬Any k≢ks (forget {m = proj₁ fm₁} k',v'∈fm'₁))
... | (v'' , (v'≈v'' , there k',v'∈fm'₂)) =
(v'' , (v'≈v'' , k',v'∈fm'₂))
narrow : {fm₁ fm₂ : FiniteMap (k ks)}
fm₁ ⊆ᵐ fm₂ pop fm₁ ⊆ᵐ pop fm₂
narrow {fm₁} {fm₂} x = narrow₂ {pop fm₁} (narrow₁ {fm₂ = fm₂} x)
k,v∈pop⇒k,v∈ : {k : A} {ks : List A} {k' : A} {v : B} (fm : FiniteMap (k ks))
(k' , v) ∈ᵐ pop fm (¬ k k' × ((k' , v) ∈ᵐ fm))
k,v∈pop⇒k,v∈ {k} {ks} {k'} {v} (m@((k , _) fm' , push k≢ks uks') , refl) k',v∈fm =
( (λ { refl All¬-¬Any k≢ks (forget {m = (fm' , uks')} k',v∈fm) })
, there k',v∈fm
)
k,v∈⇒k,v∈pop : {k : A} {ks : List A} {k' : A} {v : B} (fm : FiniteMap (k ks))
¬ k k' (k' , v) ∈ᵐ fm (k' , v) ∈ᵐ pop fm
k,v∈⇒k,v∈pop (m@(_ _ , push k≢ks _) , refl) k≢k' (here refl) = ⊥-elim (k≢k' refl)
k,v∈⇒k,v∈pop (m@(_ _ , push k≢ks _) , refl) k≢k' (there k,v'∈fm') = k,v'∈fm'
FromBothMaps : (k : A) (v : B) {ks : List A} (fm₁ fm₂ : FiniteMap ks) Set
FromBothMaps k v fm₁ fm₂ =
Σ (B × B)
(λ (v₁ , v₂) ( (v v₁ ⊔₂ v₂) × ((k , v₁) ∈ᵐ fm₁ × (k , v₂) ∈ᵐ fm₂)))
Provenance-union : {ks : List A} (fm₁ fm₂ : FiniteMap ks) {k : A} {v : B}
(k , v) ∈ᵐ (fm₁ ⊔ᵐ fm₂) FromBothMaps k v fm₁ fm₂
Provenance-union fm₁@(m₁ , ks₁≡ks) fm₂@(m₂ , ks₂≡ks) {k} {v} k,v∈fm₁fm₂
with Expr-Provenance k ((` m₁) (` m₂)) (forget {m = proj₁ (fm₁ ⊔ᵐ fm₂)} k,v∈fm₁fm₂)
... | (_ , (in (single k,v∈m₁) k∉km₂ , _))
with k∈km₁ (forget {m = m₁} k,v∈m₁)
rewrite trans ks₁≡ks (sym ks₂≡ks) =
⊥-elim (k∉km₂ k∈km₁)
... | (_ , (in k∉km₁ (single k,v∈m₂) , _))
with k∈km₂ (forget {m = m₂} k,v∈m₂)
rewrite trans ks₁≡ks (sym ks₂≡ks) =
⊥-elim (k∉km₁ k∈km₂)
... | (v₁⊔v₂ , (bothᵘ {v₁} {v₂} (single k,v₁∈m₁) (single k,v₂∈m₂) , k,v₁⊔v₂∈m₁m₂))
rewrite Map-functional {m = proj₁ (fm₁ ⊔ᵐ fm₂)} k,v∈fm₁fm₂ k,v₁⊔v₂∈m₁m₂ =
((v₁ , v₂) , (refl , (k,v₁∈m₁ , k,v₂∈m₂)))
pop-⊔-distr : {k : A} {ks : List A} (fm₁ fm₂ : FiniteMap (k ks))
pop (fm₁ ⊔ᵐ fm₂) ≈ᵐ (pop fm₁ ⊔ᵐ pop fm₂)
pop-⊔-distr {k} {ks} fm₁@(m₁ , _) fm₂@(m₂ , _) =
(pfm₁fm₂⊆pfm₁pfm₂ , pfm₁pfm₂⊆pfm₁fm₂)
where
-- pfm₁fm₂⊆pfm₁pfm₂ = {!!}
pfm₁fm₂⊆pfm₁pfm₂ : pop (fm₁ ⊔ᵐ fm₂) ⊆ᵐ (pop fm₁ ⊔ᵐ pop fm₂)
pfm₁fm₂⊆pfm₁pfm₂ k' v' k',v'∈pfm₁fm₂
with (k≢k' , k',v'∈fm₁fm₂) k,v∈pop⇒k,v∈ (fm₁ ⊔ᵐ fm₂) k',v'∈pfm₁fm₂
with ((v₁ , v₂) , (refl , (k,v₁∈fm₁ , k,v₂∈fm₂)))
Provenance-union fm₁ fm₂ k',v'∈fm₁fm₂
with k',v₁∈pfm₁ k,v∈⇒k,v∈pop fm₁ k≢k' k,v₁∈fm₁
with k',v₂∈pfm₂ k,v∈⇒k,v∈pop fm₂ k≢k' k,v₂∈fm₂
=
( v₁ ⊔₂ v₂
, (IsLattice.≈-refl lB
, ⊔-combines {m₁ = proj₁ (pop fm₁)}
{m₂ = proj₁ (pop fm₂)}
k',v₁∈pfm₁ k',v₂∈pfm₂
)
)
pfm₁pfm₂⊆pfm₁fm₂ : (pop fm₁ ⊔ᵐ pop fm₂) ⊆ᵐ pop (fm₁ ⊔ᵐ fm₂)
pfm₁pfm₂⊆pfm₁fm₂ k' v' k',v'∈pfm₁pfm₂
with ((v₁ , v₂) , (refl , (k,v₁∈pfm₁ , k,v₂∈pfm₂)))
Provenance-union (pop fm₁) (pop fm₂) k',v'∈pfm₁pfm₂
with (k≢k' , k',v₁∈fm₁) k,v∈pop⇒k,v∈ fm₁ k,v₁∈pfm₁
with (_ , k',v₂∈fm₂) k,v∈pop⇒k,v∈ fm₂ k,v₂∈pfm₂
=
( v₁ ⊔₂ v₂
, ( IsLattice.≈-refl lB
, k,v∈⇒k,v∈pop (fm₁ ⊔ᵐ fm₂) k≢k'
(⊔-combines {m₁ = m₁} {m₂ = m₂}
k',v₁∈fm₁ k',v₂∈fm₂)
)
)
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₂ (_≈ⁱᵖ_ {length 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-≈ {ks'} {pop fm₁} {pop fm₂}
(pop-≈ fm₁ fm₂ fm₁≈fm₂)
)
to-preserves-≈ : {ks : List A} (uks : Unique ks) {ip₁ ip₂ : IterProd (length ks)}
_≈ⁱᵖ_ {length 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
inductive-step : {v₁ v₂ : B} {rest₁ rest₂ : IterProd (length ks')}
v₁ ≈₂ v₂ _≈ⁱᵖ_ {length ks'} rest₁ rest₂
to uks (v₁ , rest₁) ⊆ᵐ to uks (v₂ , rest₂)
inductive-step {v₁} {v₂} {rest₁} {rest₂} v₁≈v₂ rest₁≈rest₂ k v k,v∈kvs₁
with ((fm'₁ , ufm'₁) , fm'₁≡ks') to uks' rest₁ in p₁
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
(fm'₁⊆fm'₂ , _) = to-preserves-≈ uks' {rest₁} {rest₂}
rest₁≈rest₂
(v' , (v≈v' , k,v'∈kvs₁)) = fm'₁⊆fm'₂ k v k,v∈fm'₁
in
(v' , (v≈v' , there k,v'∈kvs₁))
fm₁⊆fm₂ : to uks ip₁ ⊆ᵐ to uks ip₂
fm₁⊆fm₂ = inductive-step v₁≈v₂ rest₁≈rest₂
fm₂⊆fm₁ : to uks ip₂ ⊆ᵐ to uks ip₁
fm₂⊆fm₁ = inductive-step (≈₂-sym v₁≈v₂)
(IP.≈-sym (length ks') rest₁≈rest₂)
from-⊔-distr : {ks : List A} (fm₁ fm₂ : FiniteMap ks)
_≈ⁱᵖ_ {length ks} (from (fm₁ ⊔ᵐ fm₂))
(_⊔ⁱᵖ_ {ks} (from fm₁) (from fm₂))
from-⊔-distr {[]} fm₁ fm₂ = IsEquivalence.≈-refl ≈ᵘ-equiv
from-⊔-distr {k ks} fm₁@(m₁ , _) fm₂@(m₂ , _)
with first-key-in-map (fm₁ ⊔ᵐ fm₂)
| first-key-in-map fm₁
| first-key-in-map fm₂
| from-first-value (fm₁ ⊔ᵐ fm₂)
| from-first-value fm₁ | from-first-value fm₂
... | (v , k,v∈fm₁fm₂) | (v₁ , k,v₁∈fm₁) | (v₂ , k,v₂∈fm₂) | refl | refl | refl
with Expr-Provenance k ((` m₁) (` m₂)) (forget {m = proj₁ (fm₁ ⊔ᵐ fm₂)} k,v∈fm₁fm₂)
... | (_ , (in _ k∉km₂ , _)) = ⊥-elim (k∉km₂ (forget {m = m₂}
k,v₂∈fm₂))
... | (_ , (in k∉km₁ _ , _)) = ⊥-elim (k∉km₁ (forget {m = m₁}
k,v₁∈fm₁))
... | (v₁⊔v₂ , (bothᵘ {v₁'} {v₂'} (single k,v₁'∈m₁) (single k,v₂'∈m₂) , k,v₁⊔v₂∈m₁m₂))
rewrite Map-functional {m = m₁} k,v₁∈fm₁ k,v₁'∈m₁
rewrite Map-functional {m = m₂} k,v₂∈fm₂ k,v₂'∈m₂
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₂)))
)
to-⊔-distr : {ks : List A} (uks : Unique ks) (ip₁ ip₂ : IterProd (length ks))
to uks (_⊔ⁱᵖ_ {ks} ip₁ ip₂) ≈ᵐ (to uks ip₁ ⊔ᵐ to uks ip₂)
to-⊔-distr {[]} empty tt tt = ((λ k v ()), (λ k v ()))
to-⊔-distr {ks@(k ks')} uks@(push k≢ks' uks') ip₁@(v₁ , rest₁) ip₂@(v₂ , rest₂) = (fm⊆fm₁fm₂ , fm₁fm₂⊆fm)
where
fm₁ = to uks ip₁
fm₁' = to uks' rest₁
fm₂ = to uks ip₂
fm₂' = to uks' rest₂
fm = to uks (_⊔ⁱᵖ_ {k ks'} ip₁ ip₂)
fm⊆fm₁fm₂ : fm ⊆ᵐ (fm₁ ⊔ᵐ fm₂)
fm⊆fm₁fm₂ k v (here refl) =
(v₁ ⊔₂ v₂
, (IsLattice.≈-refl lB
, ⊔-combines {k} {v₁} {v₂} {proj₁ fm₁} {proj₁ fm₂}
(here refl) (here refl)
)
)
fm⊆fm₁fm₂ k' v (there k',v∈fm')
with (fm'⊆fm'₁fm'₂ , _) to-⊔-distr uks' rest₁ rest₂
with (v' , (v₁⊔v₂≈v' , k',v'∈fm'₁fm'₂))
fm'⊆fm'₁fm'₂ k' v k',v∈fm'
with (_ , (refl , (v₁∈fm'₁ , v₂∈fm'₂)))
Provenance-union fm₁' fm₂' k',v'∈fm'₁fm'₂ =
( v'
, ( v₁⊔v₂≈v'
, ⊔-combines {m₁ = proj₁ fm₁} {m₂ = proj₁ fm₂}
(there v₁∈fm'₁) (there v₂∈fm'₂)
)
)
fm₁fm₂⊆fm : (fm₁ ⊔ᵐ fm₂) ⊆ᵐ fm
fm₁fm₂⊆fm k' v k',v∈fm₁fm₂
with (_ , fm'₁fm'₂⊆fm')
to-⊔-distr uks' rest₁ rest₂
with (_ , (refl , (v₁∈fm₁ , v₂∈fm₂)))
Provenance-union fm₁ fm₂ k',v∈fm₁fm₂
with v₁∈fm₁ | v₂∈fm₂
... | here refl | here refl =
(v , (IsLattice.≈-refl lB , here refl))
... | here refl | there k',v₂∈fm₂' =
⊥-elim (All¬-¬Any k≢ks' (subst (k' ∈ˡ_) (proj₂ fm₂')
(forget {m = proj₁ fm₂'} k',v₂∈fm₂')))
... | there k',v₁∈fm₁' | here refl =
⊥-elim (All¬-¬Any k≢ks' (subst (k' ∈ˡ_) (proj₂ fm₁')
(forget {m = proj₁ fm₁'} k',v₁∈fm₁')))
... | there k',v₁∈fm₁' | there k',v₂∈fm₂' =
let
k',v₁v₂∈fm₁'fm₂' =
⊔-combines {m₁ = proj₁ fm₁'} {m₂ = proj₁ fm₂'}
k',v₁∈fm₁' k',v₂∈fm₂'
(v' , (v₁⊔v₂≈v' , v'∈fm')) =
fm'₁fm'₂⊆fm' _ _ k',v₁v₂∈fm₁'fm₂'
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; finiteHeightLattice) public