open import Lattice
open import Relation.Binary.PropositionalEquality as Eq
    using (_≡_;refl; sym; trans; cong; subst)
open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
open import Data.List using (List; _∷_; [])

module Lattice.FiniteMap {A : Set} {B : Set}
    {_≈₂_ : B → B → Set}
    {_⊔₂_ : B → B → B} {_⊓₂_ : B → B → B}
    (≡-dec-A : IsDecidable (_≡_ {_} {A}))
    (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where

open IsLattice lB using () renaming (_≼_ to _≼₂_)
open import Lattice.Map ≡-dec-A lB as Map
    using
        ( Map
        ; ⊔-equal-keys
        ; ⊓-equal-keys
        ; subset-impl
        ; Map-functional
        ; Expr-Provenance
        ; Expr-Provenance-≡
        ; `_; _∪_; _∩_
        ; in₁; in₂; bothᵘ; single
        ; ⊔-combines
        )
    renaming
        ( _≈_ to _≈ᵐ_
        ; _⊔_ to _⊔ᵐ_
        ; _⊓_ to _⊓ᵐ_
        ; ≈-equiv to ≈ᵐ-equiv
        ; ≈-⊔-cong to ≈ᵐ-⊔ᵐ-cong
        ; ⊔-assoc to ⊔ᵐ-assoc
        ; ⊔-comm to ⊔ᵐ-comm
        ; ⊔-idemp to ⊔ᵐ-idemp
        ; ≈-⊓-cong to ≈ᵐ-⊓ᵐ-cong
        ; ⊓-assoc to ⊓ᵐ-assoc
        ; ⊓-comm to ⊓ᵐ-comm
        ; ⊓-idemp to ⊓ᵐ-idemp
        ; absorb-⊔-⊓ to absorb-⊔ᵐ-⊓ᵐ
        ; absorb-⊓-⊔ to absorb-⊓ᵐ-⊔ᵐ
        ; ≈-dec to ≈ᵐ-dec
        ; _[_] to _[_]ᵐ
        ; []-∈ to []ᵐ-∈
        ; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ
        ; m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ to m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ᵐ
        ; locate to locateᵐ
        ; keys to keysᵐ
        ; _updating_via_ to _updatingᵐ_via_
        ; updating-via-keys-≡ to updatingᵐ-via-keys-≡
        ; updating-via-k∈ks to updatingᵐ-via-k∈ks
        ; updating-via-k∈ks-≡ to updatingᵐ-via-k∈ks-≡
        ; updating-via-∈k-forward to updatingᵐ-via-∈k-forward
        ; updating-via-k∉ks-forward to updatingᵐ-via-k∉ks-forward
        ; updating-via-k∉ks-backward to updatingᵐ-via-k∉ks-backward
        ; f'-Monotonic to f'-Monotonicᵐ
        ; _≼_ to _≼ᵐ_
        ; ∈k-dec to ∈k-decᵐ
        )
open import Data.Empty using (⊥-elim)
open import Data.List using (List; length; []; _∷_; map)
open import Data.List.Membership.Propositional using () renaming (_∈_ to _∈ˡ_)
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 Data.Nat using (ℕ)
open import Data.Product using (_×_; _,_; Σ; proj₁; proj₂)
open import Equivalence
open import Function using (_∘_)
open import Relation.Binary.Definitions using (Decidable)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Utils using (Pairwise; _∷_; []; Unique; push; empty; All¬-¬Any)
open import Showable using (Showable; show)
open import Isomorphism using (IsInverseˡ; IsInverseʳ)
open import Chain using (Height)

module WithKeys (ks : List A) where
    FiniteMap : Set
    FiniteMap = Σ Map (λ m → Map.keys m ≡ ks)

    instance
        showable : {{ showableA : Showable A }} {{ showableB : Showable B }} →
                   Showable FiniteMap
        showable = record { show = λ (m₁ , _) → show m₁ }

    _≈_ : FiniteMap → FiniteMap → Set
    _≈_ (m₁ , _) (m₂ , _) = m₁ ≈ᵐ m₂

    ≈₂-dec⇒≈-dec : IsDecidable _≈₂_ → IsDecidable _≈_
    ≈₂-dec⇒≈-dec ≈₂-dec fm₁ fm₂ = ≈ᵐ-dec ≈₂-dec (proj₁ fm₁) (proj₁ fm₂)

    _⊔_ : FiniteMap → FiniteMap → FiniteMap
    _⊔_ (m₁ , km₁≡ks) (m₂ , km₂≡ks) =
        ( m₁ ⊔ᵐ m₂
        , trans (sym (⊔-equal-keys {m₁} {m₂} (trans (km₁≡ks) (sym km₂≡ks))))
                km₁≡ks
        )

    _⊓_ : FiniteMap → FiniteMap → FiniteMap
    _⊓_ (m₁ , km₁≡ks) (m₂ , km₂≡ks) =
        ( m₁ ⊓ᵐ m₂
        , trans (sym (⊓-equal-keys {m₁} {m₂} (trans (km₁≡ks) (sym km₂≡ks))))
                km₁≡ks
        )

    _∈_ : A × B → FiniteMap → Set
    _∈_ k,v (m₁ , _) = k,v ∈ˡ (proj₁ m₁)

    _∈k_ : A → FiniteMap → Set
    _∈k_ k (m₁ , _) = k ∈ˡ (keysᵐ m₁)

    open Map using (forget) public

    ∈k-dec = ∈k-decᵐ

    locate : ∀ {k : A} {fm : FiniteMap} → k ∈k fm → Σ B (λ v → (k , v) ∈ fm)
    locate {k} {fm = (m , _)} k∈kfm = locateᵐ {k} {m} k∈kfm

    _updating_via_ : FiniteMap → List A → (A → B) → FiniteMap
    _updating_via_ (m₁ , ksm₁≡ks) ks f =
        ( m₁ updatingᵐ ks via f
        , trans (sym (updatingᵐ-via-keys-≡ m₁ ks f)) ksm₁≡ks
        )

    _[_] : FiniteMap → List A → List B
    _[_] (m₁ , _) ks = m₁ [ ks ]ᵐ

    []-∈ : ∀ {k : A} {v : B} {ks' : List A} (fm : FiniteMap) →
           k ∈ˡ ks' → (k , v) ∈ fm → v ∈ˡ (fm [ ks' ])
    []-∈ {k} {v} {ks'} (m , _) k∈ks' k,v∈fm = []ᵐ-∈ m k,v∈fm k∈ks' 

    ≈-equiv : IsEquivalence FiniteMap _≈_
    ≈-equiv = record
        { ≈-refl =
            λ {(m , _)} → IsEquivalence.≈-refl ≈ᵐ-equiv {m}
        ; ≈-sym =
            λ {(m₁ , _)} {(m₂ , _)} → IsEquivalence.≈-sym ≈ᵐ-equiv {m₁} {m₂}
        ; ≈-trans =
            λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} →
                IsEquivalence.≈-trans ≈ᵐ-equiv {m₁} {m₂} {m₃}
        }

    isUnionSemilattice : IsSemilattice FiniteMap _≈_ _⊔_
    isUnionSemilattice = record
        { ≈-equiv = ≈-equiv
        ; ≈-⊔-cong =
            λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} {(m₄ , _)} m₁≈m₂ m₃≈m₄ →
                ≈ᵐ-⊔ᵐ-cong {m₁} {m₂} {m₃} {m₄} m₁≈m₂ m₃≈m₄
        ; ⊔-assoc = λ (m₁ , _) (m₂ , _) (m₃ , _) → ⊔ᵐ-assoc m₁ m₂ m₃
        ; ⊔-comm = λ (m₁ , _) (m₂ , _) → ⊔ᵐ-comm m₁ m₂
        ; ⊔-idemp = λ (m , _) → ⊔ᵐ-idemp m
        }

    isIntersectSemilattice : IsSemilattice FiniteMap _≈_ _⊓_
    isIntersectSemilattice = record
        { ≈-equiv = ≈-equiv
        ; ≈-⊔-cong =
            λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} {(m₄ , _)} m₁≈m₂ m₃≈m₄ →
                ≈ᵐ-⊓ᵐ-cong {m₁} {m₂} {m₃} {m₄} m₁≈m₂ m₃≈m₄
        ; ⊔-assoc = λ (m₁ , _) (m₂ , _) (m₃ , _) → ⊓ᵐ-assoc m₁ m₂ m₃
        ; ⊔-comm = λ (m₁ , _) (m₂ , _) → ⊓ᵐ-comm m₁ m₂
        ; ⊔-idemp = λ (m , _) → ⊓ᵐ-idemp m
        }

    isLattice : IsLattice FiniteMap _≈_ _⊔_ _⊓_
    isLattice = record
        { joinSemilattice = isUnionSemilattice
        ; meetSemilattice = isIntersectSemilattice
        ; absorb-⊔-⊓ = λ (m₁ , _) (m₂ , _) → absorb-⊔ᵐ-⊓ᵐ m₁ m₂
        ; absorb-⊓-⊔ = λ (m₁ , _) (m₂ , _) → absorb-⊓ᵐ-⊔ᵐ m₁ m₂
        }

    open IsLattice isLattice using (_≼_; ⊔-Monotonicˡ; ⊔-Monotonicʳ) public

    lattice : Lattice FiniteMap
    lattice = record
        { _≈_ = _≈_
        ; _⊔_ = _⊔_
        ; _⊓_ = _⊓_
        ; isLattice = isLattice
        }

    m₁≼m₂⇒m₁[k]≼m₂[k] : ∀ (fm₁ fm₂ : FiniteMap) {k : A} {v₁ v₂ : B} →
                        fm₁ ≼ fm₂ → (k , v₁) ∈ fm₁ → (k , v₂) ∈ fm₂ → v₁ ≼₂ v₂
    m₁≼m₂⇒m₁[k]≼m₂[k] (m₁ , _) (m₂ , _) m₁≼m₂ k,v₁∈m₁ k,v₂∈m₂ = m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ m₁ m₂ m₁≼m₂ k,v₁∈m₁ k,v₂∈m₂

    m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ : ∀ (fm₁ fm₂ : FiniteMap) {k : A} →
                             fm₁ ≈ fm₂ → ∀ (k∈kfm₁ : k ∈k fm₁) (k∈kfm₂ : k ∈k fm₂) →
                             proj₁ (locate {fm = fm₁} k∈kfm₁) ≈₂ proj₁ (locate {fm = fm₂} k∈kfm₂)
    m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ (m₁ , _) (m₂ , _) = m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ᵐ m₁ m₂

    module GeneralizedUpdate
             {l} {L : Set l}
             {_≈ˡ_ : L → L → Set l} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L}
             (lL : IsLattice L _≈ˡ_ _⊔ˡ_ _⊓ˡ_)
             (f : L → FiniteMap) (f-Monotonic : Monotonic (IsLattice._≼_ lL) _≼_ f)
             (g : A → L → B) (g-Monotonicʳ : ∀ k → Monotonic (IsLattice._≼_ lL) _≼₂_ (g k))
             (ks : List A) where

        open IsLattice lL using () renaming (_≼_ to _≼ˡ_)

        updater : L → A → B
        updater l k = g k l

        f' : L → FiniteMap
        f' l = (f l) updating ks via (updater l)

        f'-Monotonic : Monotonic _≼ˡ_ _≼_ f'
        f'-Monotonic {l₁} {l₂} l₁≼l₂ = f'-Monotonicᵐ lL (proj₁ ∘ f) f-Monotonic g g-Monotonicʳ ks l₁≼l₂

        f'-∈k-forward : ∀ {k l} → k ∈k (f l) → k ∈k (f' l)
        f'-∈k-forward {k} {l} = updatingᵐ-via-∈k-forward (proj₁ (f l)) ks (updater l)

        f'-k∈ks : ∀ {k l} → k ∈ˡ ks → k ∈k (f' l) → (k , updater l k) ∈ (f' l)
        f'-k∈ks {k} {l} = updatingᵐ-via-k∈ks (proj₁ (f l)) (updater l)

        f'-k∈ks-≡ : ∀ {k v l} → k ∈ˡ ks → (k , v) ∈ (f' l) → v ≡ updater l k
        f'-k∈ks-≡ {k} {v} {l} = updatingᵐ-via-k∈ks-≡ (proj₁ (f l)) (updater l)

        f'-k∉ks-forward : ∀ {k v l} → ¬ k ∈ˡ ks → (k , v) ∈ (f l) → (k , v) ∈ (f' l)
        f'-k∉ks-forward {k} {v} {l} = updatingᵐ-via-k∉ks-forward (proj₁ (f l)) (updater l)

        f'-k∉ks-backward : ∀ {k v l} → ¬ k ∈ˡ ks → (k , v) ∈ (f' l) → (k , v) ∈ (f l)
        f'-k∉ks-backward {k} {v} {l} = updatingᵐ-via-k∉ks-backward (proj₁ (f l)) (updater l)

    all-equal-keys : ∀ (fm₁ fm₂ : FiniteMap) → (Map.keys (proj₁ fm₁) ≡ Map.keys (proj₁ fm₂))
    all-equal-keys (fm₁ , km₁≡ks) (fm₂ , km₂≡ks) = trans km₁≡ks (sym km₂≡ks)

    ∈k-exclusive : ∀ (fm₁ fm₂ : FiniteMap) {k : A} → ¬ ((k ∈k fm₁) × (¬ k ∈k fm₂))
    ∈k-exclusive fm₁ fm₂ {k} (k∈kfm₁ , k∉kfm₂) =
        let
            k∈kfm₂ = subst (λ l → k ∈ˡ l) (all-equal-keys fm₁ fm₂) k∈kfm₁
        in
            k∉kfm₂ k∈kfm₂

    m₁≼m₂⇒m₁[ks]≼m₂[ks] : ∀ (fm₁ fm₂ : FiniteMap) (ks' : List A) →
                          fm₁ ≼ fm₂ → Pairwise _≼₂_ (fm₁ [ ks' ]) (fm₂ [ ks' ])
    m₁≼m₂⇒m₁[ks]≼m₂[ks] _ _ [] _ = []
    m₁≼m₂⇒m₁[ks]≼m₂[ks] fm₁@(m₁ , km₁≡ks) fm₂@(m₂ , km₂≡ks) (k ∷ ks'') m₁≼m₂
        with ∈k-decᵐ k (proj₁ m₁) | ∈k-decᵐ k (proj₁ m₂)
    ...   | yes k∈km₁ | yes k∈km₂ =
            let
                (v₁ , k,v₁∈m₁) = locateᵐ {m = m₁} k∈km₁
                (v₂ , k,v₂∈m₂) = locateᵐ {m = m₂} k∈km₂
            in
                (m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ m₁ m₂ m₁≼m₂ k,v₁∈m₁ k,v₂∈m₂) ∷ m₁≼m₂⇒m₁[ks]≼m₂[ks] fm₁ fm₂ ks'' m₁≼m₂
    ...   | no k∉km₁ | no k∉km₂ = m₁≼m₂⇒m₁[ks]≼m₂[ks] fm₁ fm₂ ks'' m₁≼m₂
    ...   | yes k∈km₁ | no k∉km₂ = ⊥-elim (∈k-exclusive fm₁ fm₂ (k∈km₁ , k∉km₂))
    ...   | no k∉km₁ | yes k∈km₂ = ⊥-elim (∈k-exclusive fm₂ fm₁ (k∈km₂ , k∉km₁))

open WithKeys 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₁ 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} = _∈_ 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})
                                 (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'₁))

    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) ∈ᵐ (_⊔_ ks 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-≡ ((` m₁) ∪ (` m₂)) k,v∈fm₁fm₂
    ...   | in₁ (single k,v∈m₁) k∉km₂
            with k∈km₁ ← (forget 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 k,v∈m₂)
            rewrite trans ks₁≡ks (sym ks₂≡ks) =
            ⊥-elim (k∉km₁ k∈km₂)
    ...   | bothᵘ {v₁} {v₂} (single k,v₁∈m₁) (single k,v₂∈m₂) =
            ((v₁ , v₂) , (refl , (k,v₁∈m₁ , k,v₂∈m₂)))

    private
        first-key-in-map : ∀ {k : A} {ks : List A} (fm : FiniteMap (k ∷ ks)) →
                           Σ B (λ v → (k , v) ∈ᵐ 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 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 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'

        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 k,v∈fm₁fm₂)
    ...       | (_ , (in₁ _ k∉km₂ , _)) = ⊥-elim (k∉km₂ (forget k,v₂∈fm₂))
    ...       | (_ , (in₂ k∉km₁ _ , _)) = ⊥-elim (k∉km₁ (forget 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 k',v₂∈fm₂')))
            ...   | there k',v₁∈fm₁' | here refl =
                    ⊥-elim (All¬-¬Any k≢ks' (subst (k' ∈ˡ_) (proj₂ fm₁')
                                                   (forget 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 WithUniqueKeysAndFixedHeight {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

        -- 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∈⊥