Prove that finite value-maps are finite height

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

Lattice/FiniteValueMap.agda

@@ -12,10 +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; []; _∷_)
+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)
@@ -25,32 +27,32 @@ 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
-    from {k ∷ ks'} (((k' , v) ∷ kvs' , push _ uks') , refl) = (v , from ((kvs' , uks'), refl))
+    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)
-        with to uks' rest
-    ...   | ((kvs' , ukvs') , kvs'≡ks') =
+    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≢kvs' = subst (λ ks → All (λ k' → ¬ k ≡ k') ks) (sym kvs'≡ks') k≢ks'
-                kvs≡ks = cong (k ∷_) kvs'≡ks'
+            k≢fm' = subst (λ ks → All (λ k' → ¬ k ≡ k') ks) (sym fm'≡ks') k≢ks'
+            kvs≡ks = cong (k ∷_) fm'≡ks'
         in
-                (((k , v) ∷ kvs' , push k≢kvs' ukvs') , kvs≡ks)
+            (((k , v) ∷ fm' , push k≢fm' ufm') , kvs≡ks)
 
 
     private
@@ -76,10 +78,10 @@ module IterProdIsomorphism where
                       Inverseˡ (_≈ᵐ_ {ks}) (_≈ⁱᵖ_ {ks}) (from {ks}) (to {ks} uks) -- from (to x) = x
     from-to-inverseˡ {[]} _ _ = IsEquivalence.≈-refl (IP.≈-equiv 0)
     from-to-inverseˡ {k ∷ ks'} (push k≢ks' uks') (v , rest)
-        with ((kvs' , ukvs') , refl) ← to uks' rest in p rewrite sym p =
+        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 (kvs', ...). So, put it back
+            -- 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`.
 
@@ -88,24 +90,24 @@ module IterProdIsomorphism where
     from-to-inverseʳ : ∀ {ks : List A} (uks : Unique ks) →
                        Inverseʳ (_≈ᵐ_ {ks}) (_≈ⁱᵖ_ {ks}) (from {ks}) (to {ks} uks) -- to (from x) = x
     from-to-inverseʳ {[]} _ (([] , empty) , kvs≡ks) rewrite kvs≡ks = ((λ k v ()) , (λ k v ()))
-    from-to-inverseʳ {k ∷ ks'} uks@(push k≢ks'₁ uks'₁) fm₁@(m₁@((k , v) ∷ kvs'₁ , push k≢ks'₂ uks'₂) , refl)
-        with to uks'₁ (from ((kvs'₁ , uks'₂) , refl)) | from-to-inverseʳ {ks'} uks'₁ ((kvs'₁ , uks'₂) , refl)
-    ...   | ((kvs'₂ , ukvs'₂) , _) | (kvs'₂⊆kvs'₁ , kvs'₁⊆kvs'₂) = (m₂⊆m₁ , m₁⊆m₂)
+    from-to-inverseʳ {k ∷ ks'} uks@(push k≢ks'₁ uks'₁) fm₁@(m₁@((k , v) ∷ fm'₁ , push k≢ks'₂ 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) ∷ kvs'₁
-                    kvs₂ = (k , v) ∷ kvs'₂
+                    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'∈kvs'₁) =
-                        let (v'' , (v'≈v'' , k',v''∈kvs'₂)) = kvs'₁⊆kvs'₂ k' v' k',v'∈kvs'₁
-                        in (v'' , (v'≈v'' , there k',v''∈kvs'₂))
+                    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'∈kvs'₂) =
-                        let (v'' , (v'≈v'' , k',v''∈kvs'₁)) = kvs'₂⊆kvs'₁ k' v' k',v'∈kvs'₂
-                        in (v'' , (v'≈v'' , there k',v''∈kvs'₁))
+                    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)
@@ -119,40 +121,39 @@ module IterProdIsomorphism where
         -- matching into a helper functions, and write solutions in terms
         -- of that.
         pop : ∀ {k : A} {ks : List A} → FiniteMap (k ∷ ks) → FiniteMap ks
-        pop (((_ ∷ kvs') , push _ ukvs') , refl) = ((kvs' , ukvs') , refl)
+        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'∈kvs'₁ = kvs₁⊆kvs₂ k' v' (there k',v'∈kvs'₁)
+                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₂ = (_ ∷ kvs'₂ , push k≢ks _) , kvs≡ks@refl} kvs₁⊆kvs₂ k' v' k',v'∈kvs'₁
-                    with kvs₁⊆kvs₂ k' v' k',v'∈kvs'₁
-                ...   | (v'' , (v'≈v'' , here refl)) rewrite sym (proj₂ fm₁) = ⊥-elim (All¬-¬Any k≢ks (forget {m = proj₁ fm₁} k',v'∈kvs'₁))
-                ...   | (v'' , (v'≈v'' , there k',v'∈kvs'₂)) = (v'' , (v'≈v'' , k',v'∈kvs'₂))
+                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 , _) ∷ kvs' , push k≢ks uks') , refl) k',v∈fm =
-            ((λ { refl → All¬-¬Any k≢ks (forget {m = (kvs' , uks')} k',v∈fm) }), there 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 {k} {ks} {k'} {v} (m@((k , _) ∷ kvs' , push k≢ks uks') , refl) k≢k' (here refl) = ⊥-elim (k≢k' refl)
-        k,v∈⇒k,v∈pop {k} {ks} {k'} {v} (m@((k , _) ∷ kvs' , push k≢ks uks') , refl) k≢k' (there k,v'∈kvs') = k,v'∈kvs'
+        k,v∈⇒k,v∈pop {k} {ks} {k'} {v} (m@((k , _) ∷ fm' , push k≢ks uks') , refl) k≢k' (here refl) = ⊥-elim (k≢k' refl)
+        k,v∈⇒k,v∈pop {k} {ks} {k'} {v} (m@((k , _) ∷ fm' , push k≢ks uks') , refl) k≢k' (there k,v'∈fm') = k,v'∈fm'
 
-        Provenance-union : ∀ {ks : List A} (fm₁ fm₂ : FiniteMap ks) (k : A) (v : B) → (k , v) ∈ᵐ (fm₁ ⊔ᵐ fm₂) → Σ (B × B) (λ (v₁ , v₂) → ((v ≡ v₁ ⊔₂ v₂) × ((k , v₁) ∈ᵐ fm₁ × (k , v₂) ∈ᵐ fm₂)))
-        Provenance-union fm₁@(m₁ , ks₁≡ks) fm₂@(m₂ , ks₂≡ks) k v k,v∈fm₁fm₂
+        Provenance-union : ∀ {ks : List A} (fm₁ fm₂ : FiniteMap ks) {k : A} {v : B} → (k , v) ∈ᵐ (fm₁ ⊔ᵐ fm₂) → Σ (B × B) (λ (v₁ , v₂) → ((v ≡ v₁ ⊔₂ v₂) × ((k , v₁) ∈ᵐ fm₁ × (k , v₂) ∈ᵐ 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
@@ -160,51 +161,51 @@ module IterProdIsomorphism where
                 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' k',v'∈fm₁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' 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 (((_ ∷ kvs') , push _ ukvs') , refl) = refl
+        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₁
-                with ((kvs'₁ , ukvs'₁) , kvs'₁≡ks') ← to uks' rest₁ in p₁
-                with ((kvs'₂ , ukvs'₂) , kvs'₂≡ks') ← to uks' rest₂ in p₂
+                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∈kvs'₁ 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∈kvs'₁ 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₂
-                with ((kvs'₁ , ukvs'₁) , kvs'₁≡ks') ← to uks' rest₁ in p₁
-                with ((kvs'₂ , ukvs'₂) , kvs'₂≡ks') ← to uks' rest₂ in p₂
+                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₁ , (IsLattice.≈-sym lB v₁≈v₂ , here refl))
-            ...   | there k,v∈kvs'₂ 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∈kvs'₂ 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,5 +221,54 @@ 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₂)))
                   )
+
+
+    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 (λ list → k' ∈ˡ list) (proj₂ fm₂') (forget {m = proj₁ fm₂'} k',v₂∈fm₂')))
+            ...   | there k',v₁∈fm₁' | here refl = ⊥-elim (All¬-¬Any k≢ks' (subst (λ list → k' ∈ˡ list) (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) public

Lattice/IterProd.agda

@@ -23,94 +23,97 @@ IterProd k = iterate k (λ t → A × t) B
 
 -- To make iteration more convenient, package the definitions in Lattice
 -- records, perform the recursion, and unpackage.
+--
 
-module _ where
-    lattice : ∀ {k : ℕ} → Lattice (IterProd k)
-    lattice {0} = record
-        { _≈_ = _≈₂_
-        ; _⊔_ = _⊔₂_
-        ; _⊓_ = _⊓₂_
-        ; isLattice = lB
-        }
-    lattice {suc k'} = record
-        { _≈_ = _≈_
-        ; _⊔_ = _⊔_
-        ; _⊓_ = _⊓_
-        ; isLattice = isLattice
-        }
-        where
-            Right : Lattice (IterProd k')
-            Right = lattice {k'}
+-- If we prove isLattice and isFiniteHeightLattice by induction separately,
+-- we lose the connection between the operations (which should be the same)
+-- that are built up by the two iterations. So, do everything in one iteration.
+-- This requires some odd code.
 
-            open import Lattice.Prod
-                _≈₁_ (Lattice._≈_ Right)
-                _⊔₁_ (Lattice._⊔_ Right)
-                _⊓₁_ (Lattice._⊓_ Right)
-                lA  (Lattice.isLattice Right)
+private
+    record RequiredForFixedHeight : Set (lsuc a) where
+         field
+            ≈₁-dec : IsDecidable _≈₁_
+            ≈₂-dec : IsDecidable _≈₂_
+            h₁ h₂ : ℕ
+            fhA : FixedHeight₁ h₁
+            fhB : FixedHeight₂ h₂
 
-module _ (k : ℕ) where
-    open Lattice.Lattice (lattice {k}) public
-
-module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
-         (h₁ h₂ : ℕ)
-         (fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where
-
-    private module _ where
-        record FiniteHeightAndDecEq (A : Set a) : Set (lsuc a) where
+    record IsFiniteHeightAndDecEq {A : Set a} {_≈_ : A → A → Set a} {_⊔_ : A → A → A} {_⊓_ : A → A → A} (isLattice : IsLattice A _≈_ _⊔_ _⊓_) : Set (lsuc a) where
         field
             height : ℕ
+            fixedHeight : IsLattice.FixedHeight isLattice height
+            ≈-dec : IsDecidable _≈_
+
+    record Everything (A : Set a) : Set (lsuc a) where
+        field
             _≈_ : A → A → Set a
             _⊔_ : A → A → A
             _⊓_ : A → A → A
 
-                isFiniteHeightLattice : IsFiniteHeightLattice A height _≈_ _⊔_ _⊓_
-                ≈-dec : IsDecidable _≈_
+            isLattice : IsLattice A _≈_ _⊔_ _⊓_
+            isFiniteHeightIfSupported : RequiredForFixedHeight → IsFiniteHeightAndDecEq isLattice
 
-            open IsFiniteHeightLattice isFiniteHeightLattice public
-
-        finiteHeightAndDec : ∀ {k : ℕ} → FiniteHeightAndDecEq (IterProd k)
-        finiteHeightAndDec {0} = record
-            { height = h₂
-            ; _≈_ = _≈₂_
+    everything : ∀ (k : ℕ) → Everything (IterProd k)
+    everything 0 = record
+        { _≈_ = _≈₂_
         ; _⊔_ = _⊔₂_
         ; _⊓_ = _⊓₂_
-            ; isFiniteHeightLattice = record
-                { isLattice = lB
-                ; fixedHeight = fhB
+        ; isLattice = lB
+        ; isFiniteHeightIfSupported = λ req → record
+            { height = RequiredForFixedHeight.h₂ req
+            ; fixedHeight = RequiredForFixedHeight.fhB req
+            ; ≈-dec = RequiredForFixedHeight.≈₂-dec req
             }
-            ; ≈-dec = ≈₂-dec
         }
-        finiteHeightAndDec {suc k'} = record
-            { height = h₁ + FiniteHeightAndDecEq.height Right
-            ; _≈_ = P._≈_
+    everything (suc k') = record
+        { _≈_ = P._≈_
         ; _⊔_ = P._⊔_
         ; _⊓_ = P._⊓_
-            ; isFiniteHeightLattice = isFiniteHeightLattice
-                ≈₁-dec (FiniteHeightAndDecEq.≈-dec Right)
-                h₁ (FiniteHeightAndDecEq.height Right)
-                fhA (IsFiniteHeightLattice.fixedHeight (FiniteHeightAndDecEq.isFiniteHeightLattice Right))
-            ; ≈-dec = ≈-dec ≈₁-dec (FiniteHeightAndDecEq.≈-dec Right)
+        ; isLattice = P.isLattice
+        ; isFiniteHeightIfSupported = λ req →
+            let
+                fhlRest = Everything.isFiniteHeightIfSupported everythingRest req
+            in
+                record
+                    { height = (RequiredForFixedHeight.h₁ req) + IsFiniteHeightAndDecEq.height fhlRest
+                    ; fixedHeight =
+                        P.fixedHeight
+                        (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightAndDecEq.≈-dec fhlRest)
+                        (RequiredForFixedHeight.h₁ req) (IsFiniteHeightAndDecEq.height fhlRest)
+                        (RequiredForFixedHeight.fhA req) (IsFiniteHeightAndDecEq.fixedHeight fhlRest)
+                    ; ≈-dec = P.≈-dec (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightAndDecEq.≈-dec fhlRest)
+                    }
         }
         where
-                Right = finiteHeightAndDec {k'}
+            everythingRest = everything k'
 
-                open import Lattice.Prod
-                    _≈₁_ (FiniteHeightAndDecEq._≈_ Right)
-                    _⊔₁_ (FiniteHeightAndDecEq._⊔_ Right)
-                    _⊓₁_ (FiniteHeightAndDecEq._⊓_ Right)
-                    lA  (FiniteHeightAndDecEq.isLattice Right) as P
+            import Lattice.Prod
+                _≈₁_ (Everything._≈_ everythingRest)
+                _⊔₁_ (Everything._⊔_ everythingRest)
+                _⊓₁_ (Everything._⊓_ everythingRest)
+                lA  (Everything.isLattice everythingRest) as P
 
-    module _ (k : ℕ) where
-        open FiniteHeightAndDecEq (finiteHeightAndDec {k}) using (isFiniteHeightLattice) public
+module _ (k : ℕ) where
+    open Everything (everything k) using (_≈_; _⊔_; _⊓_; isLattice) public
+    open Lattice.IsLattice isLattice public
+
+    module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
+             (h₁ h₂ : ℕ)
+             (fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where
 
         private
-            FHD = finiteHeightAndDec {k}
-
-        finiteHeightLattice : FiniteHeightLattice (IterProd k)
-        finiteHeightLattice = record
-            { height = FiniteHeightAndDecEq.height FHD
-            ; _≈_ = FiniteHeightAndDecEq._≈_ FHD
-            ; _⊔_ = FiniteHeightAndDecEq._⊔_ FHD
-            ; _⊓_ = FiniteHeightAndDecEq._⊓_ FHD
-            ; isFiniteHeightLattice = isFiniteHeightLattice
+            required : RequiredForFixedHeight
+            required = record
+                { ≈₁-dec = ≈₁-dec
+                ; ≈₂-dec = ≈₂-dec
+                ; h₁ = h₁
+                ; h₂ = h₂
+                ; fhA = fhA
+                ; fhB = fhB
+                }
+
+        isFiniteHeightLattice = record
+            { isLattice = isLattice
+            ; fixedHeight = IsFiniteHeightAndDecEq.fixedHeight (Everything.isFiniteHeightIfSupported (everything k) required)
             }

Lattice/Prod.agda

@@ -171,10 +171,8 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
                                      , ≤-stepsˡ 1 (subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂))
                                      ))
 
-    isFiniteHeightLattice : IsFiniteHeightLattice (A × B) (h₁ + h₂) _≈_ _⊔_ _⊓_
-    isFiniteHeightLattice = record
-        { isLattice = isLattice
-        ; fixedHeight =
+    fixedHeight : IsLattice.FixedHeight isLattice (h₁ + h₂)
+    fixedHeight =
       ( ( ((amin , bmin) , (amax , bmax))
         , concat
             (ChainMapping₁.Chain-map (λ a → (a , bmin)) (∙,b-Monotonic _) proj₁ (∙,b-Preserves-≈₁ _) (proj₂ (proj₁ fhA)))
@@ -183,6 +181,11 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
       , λ a₁b₁a₂b₂ → let ((n₁ , n₂) , ((a₁a₂ , b₁b₂) , n≤n₁+n₂)) = unzip a₁b₁a₂b₂
                      in ≤-trans n≤n₁+n₂ (+-mono-≤ (proj₂ fhA a₁a₂) (proj₂ fhB b₁b₂))
       )
+
+    isFiniteHeightLattice : IsFiniteHeightLattice (A × B) (h₁ + h₂) _≈_ _⊔_ _⊓_
+    isFiniteHeightLattice = record
+        { isLattice = isLattice
+        ; fixedHeight = fixedHeight
         }
 
     finiteHeightLattice : FiniteHeightLattice (A × B)

Lattice/Unit.agda

@@ -107,10 +107,13 @@ private
     isLongest {tt} {tt} (step (tt⊔tt≈tt , tt̷≈tt) _ _) = ⊥-elim (tt̷≈tt refl)
     isLongest (done _) = z≤n
 
+fixedHeight : IsLattice.FixedHeight isLattice 0
+fixedHeight = (((tt , tt) , longestChain) , isLongest)
+
 isFiniteHeightLattice : IsFiniteHeightLattice ⊤ 0 _≈_ _⊔_ _⊓_
 isFiniteHeightLattice = record
     { isLattice = isLattice
-    ; fixedHeight = (((tt , tt) , longestChain) , isLongest)
+    ; fixedHeight = fixedHeight
     }
 
 finiteHeightLattice : FiniteHeightLattice ⊤

Utils.agda

@@ -32,6 +32,10 @@ All¬-¬Any : ∀ {p c} {C : Set c} {P : C → Set p} {l : List C} → All (λ x
 All¬-¬Any {l = x ∷ xs} (¬Px ∷ _) (here Px) = ¬Px Px
 All¬-¬Any {l = x ∷ xs} (_ ∷ ¬Pxs) (there Pxs) = All¬-¬Any ¬Pxs Pxs
 
+All-single : ∀ {p c} {C : Set c} {P : C → Set p} {c : C} {l : List C} → All P l → c ∈ l → P c
+All-single {c = c} {l = x ∷ xs} (p ∷ ps) (here refl) = p
+All-single {c = c} {l = x ∷ xs} (p ∷ ps) (there c∈xs) = All-single ps c∈xs
+
 All-x∈xs : ∀ {a} {A : Set a} (xs : List A) → All (λ x → x ∈ xs) xs
 All-x∈xs [] = []
 All-x∈xs (x ∷ xs') = here refl ∷ map there (All-x∈xs xs')