Fix typo in FixedHeightLattice definition

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

Lattice.agda

@@ -145,3 +145,14 @@ record Lattice {a} (A : Set a) : Set (lsuc a) where
         isLattice : IsLattice A _≈_ _⊔_ _⊓_
 
     open IsLattice isLattice public
+
+record FiniteHeightLattice {a} (A : Set a) : Set (lsuc a) where
+    field
+        height : ℕ
+        _≈_ : A → A → Set a
+        _⊔_ : A → A → A
+        _⊓_ : A → A → A
+
+        isFiniteHeightLattice : IsFiniteHeightLattice A height _≈_ _⊔_ _⊓_
+
+    open IsFiniteHeightLattice isFiniteHeightLattice public

Lattice/FiniteMap.agda

@@ -0,0 +1,78 @@
+open import Lattice
+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 Data.List using (List)
+
+module Lattice.FiniteMap {a b : Level} (A : Set a) (B : Set b)
+    (_≈₂_ : B → B → Set b)
+    (_⊔₂_ : B → B → B) (_⊓₂_ : B → B → B)
+    (≡-dec-A : Decidable (_≡_ {a} {A}))
+    (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
+
+open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB as Map
+    using (Map; ⊔-equal-keys; ⊓-equal-keys)
+    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-⊓ᵐ-⊔ᵐ
+        )
+open import Data.Product using (_×_; _,_; Σ; proj₁ ; proj₂)
+open import Equivalence
+
+module _ (ks : List A) where
+    FiniteMap : Set (a ⊔ℓ b)
+    FiniteMap = Σ Map (λ m → Map.keys m ≡ ks)
+
+    _≈_ : FiniteMap → FiniteMap → Set (a ⊔ℓ b)
+    _≈_ (m₁ , _) (m₂ , _) = m₁ ≈ᵐ m₂
+
+    _⊔_ : 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)
+
+    ≈-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₂
+        }

Lattice/IterProd.agda

@@ -0,0 +1,107 @@
+open import Lattice
+
+module Lattice.IterProd {a} {A B : Set a}
+    (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a)
+    (_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B)
+    (_⊓₁_ : A → A → A) (_⊓₂_ : B → B → B)
+    (lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_) (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
+
+open import Agda.Primitive using (lsuc)
+open import Data.Nat using (ℕ; suc; _+_)
+open import Data.Product using (_×_)
+open import Utils using (iterate)
+
+open IsLattice lA renaming (FixedHeight to FixedHeight₁)
+open IsLattice lB renaming (FixedHeight to FixedHeight₂)
+
+IterProd : ℕ → Set a
+IterProd k = iterate k (λ t → A × t) B
+
+-- To make iteration more convenient, package the definitions in Lattice
+-- records, perform the recursion, and unpackage.
+
+private module _ where
+    BLattice : Lattice B
+    BLattice = record
+        { _≈_ = _≈₂_
+        ; _⊔_ = _⊔₂_
+        ; _⊓_ = _⊓₂_
+        ; isLattice = lB
+        }
+
+    IterProdLattice : ∀ {k : ℕ} → Lattice (IterProd k)
+    IterProdLattice {0} = BLattice
+    IterProdLattice {suc k'} = record
+        { _≈_ = _≈_
+        ; _⊔_ = _⊔_
+        ; _⊓_ = _⊓_
+        ; isLattice = isLattice
+        }
+        where
+            Right : Lattice (IterProd k')
+            Right = IterProdLattice {k'}
+
+            open import Lattice.Prod
+                _≈₁_ (Lattice._≈_ Right)
+                _⊔₁_ (Lattice._⊔_ Right)
+                _⊓₁_ (Lattice._⊓_ Right)
+                lA  (Lattice.isLattice Right)
+
+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
+            field
+                height : ℕ
+                _≈_ : A → A → Set a
+                _⊔_ : A → A → A
+                _⊓_ : A → A → A
+
+                isFiniteHeightLattice : IsFiniteHeightLattice A height _≈_ _⊔_ _⊓_
+                ≈-dec : IsDecidable _≈_
+
+            open IsFiniteHeightLattice isFiniteHeightLattice public
+
+        BFiniteHeightLattice : FiniteHeightAndDecEq B
+        BFiniteHeightLattice = record
+            { height = h₂
+            ; _≈_ = _≈₂_
+            ; _⊔_ = _⊔₂_
+            ; _⊓_ = _⊓₂_
+            ; isFiniteHeightLattice = record
+                { isLattice = lB
+                ; fixedHeight = fhB
+                }
+            ; ≈-dec = ≈₂-dec
+            }
+
+        IterProdFiniteHeightLattice : ∀ {k : ℕ} → FiniteHeightAndDecEq (IterProd k)
+        IterProdFiniteHeightLattice {0} = BFiniteHeightLattice
+        IterProdFiniteHeightLattice {suc k'} = record
+            { height = h₁ + FiniteHeightAndDecEq.height Right
+            ; _≈_ = _≈_
+            ; _⊔_ = _⊔_
+            ; _⊓_ = _⊓_
+            ; isFiniteHeightLattice = isFiniteHeightLattice
+                ≈₁-dec (FiniteHeightAndDecEq.≈-dec Right)
+                h₁ (FiniteHeightAndDecEq.height Right)
+                fhA (IsFiniteHeightLattice.fixedHeight (FiniteHeightAndDecEq.isFiniteHeightLattice Right))
+            ; ≈-dec = ≈-dec ≈₁-dec (FiniteHeightAndDecEq.≈-dec Right)
+            }
+            where
+                Right = IterProdFiniteHeightLattice {k'}
+
+                open import Lattice.Prod
+                    _≈₁_ (FiniteHeightAndDecEq._≈_ Right)
+                    _⊔₁_ (FiniteHeightAndDecEq._⊔_ Right)
+                    _⊓₁_ (FiniteHeightAndDecEq._⊓_ Right)
+                    lA  (FiniteHeightAndDecEq.isLattice Right)
+
+    module _ (k : ℕ) where
+        open FiniteHeightAndDecEq (IterProdFiniteHeightLattice {k}) using (fixedHeight) public
+
+-- Expose the computed definition in public.
+module _ (k : ℕ) where
+    open Lattice.Lattice (IterProdLattice {k}) public

Lattice/Map.agda

@@ -19,6 +19,7 @@ open import Data.List.Relation.Unary.Any using (Any; here; there) -- TODO: re-ex
 open import Data.Product using (_×_; _,_; Σ; proj₁ ; proj₂)
 open import Data.Empty using (⊥; ⊥-elim)
 open import Equivalence
+open import Utils using (Unique; push; empty; Unique-append; All¬-¬Any; All-x∈xs)
 
 open IsLattice lB using () renaming
     ( ≈-refl to ≈₂-refl; ≈-sym to ≈₂-sym; ≈-trans to ≈₂-trans
@@ -28,35 +29,13 @@ open IsLattice lB using () renaming
     ; absorb-⊔-⊓ to absorb-⊔₂-⊓₂; absorb-⊓-⊔ to absorb-⊓₂-⊔₂
     )
 
-keys : List (A × B) → List A
-keys = map proj₁
-
-data Unique {c} {C : Set c} : List C → Set c where
-    empty : Unique []
-    push : ∀ {x : C} {xs : List C}
-        → All (λ x' → ¬ x ≡ x') xs
-        → Unique xs
-        → Unique (x ∷ xs)
-
-Unique-append : ∀ {c} {C : Set c} {x : C} {xs : List C} →
-                ¬ MemProp._∈_ x xs → Unique xs →  Unique (xs ++ (x ∷ []))
-Unique-append {c} {C} {x} {[]} _ _ = push [] empty
-Unique-append {c} {C} {x} {x' ∷ xs'} x∉xs (push x'≢ uxs') =
-    push (help x'≢) (Unique-append (λ x∈xs' → x∉xs (there x∈xs')) uxs')
-    where
-        x'≢x : ¬ x' ≡ x
-        x'≢x x'≡x = x∉xs (here (sym x'≡x))
-
-        help : {l : List C} → All (λ x'' → ¬ x' ≡ x'') l → All (λ x'' → ¬ x' ≡ x'') (l ++ (x ∷ []))
-        help {[]} _ = x'≢x ∷ []
-        help {e ∷ es} (x'≢e ∷ x'≢es) = x'≢e ∷ help x'≢es
-
-All¬-¬Any : ∀ {p c} {C : Set c} {P : C → Set p} {l : List C} → All (λ x → ¬ P x) l → ¬ Any P l
-All¬-¬Any {l = x ∷ xs} (¬Px ∷ _) (here Px) = ¬Px Px
-All¬-¬Any {l = x ∷ xs} (_ ∷ ¬Pxs) (there Pxs) = All¬-¬Any ¬Pxs Pxs
+private module ImplKeys where
+    keys : List (A × B) → List A
+    keys = map proj₁
 
 private module _ where
     open MemProp using (_∈_)
+    open ImplKeys
 
     unique-not-in : ∀ {k : A} {v : B} {l : List (A × B)}  →
                     ¬ (All (λ k' → ¬ k ≡ k') (keys l) × (k , v) ∈ l)
@@ -108,6 +87,7 @@ private module ImplRelation where
 private module ImplInsert (f : B → B → B) where
     open import Data.List using (map)
     open MemProp using (_∈_)
+    open ImplKeys
 
     private
         _∈k_ : A → List (A × B) → Set a
@@ -153,6 +133,20 @@ private module ImplInsert (f : B → B → B) where
     ...   | yes k∈kl rewrite insert-keys-∈ {v = v} k∈kl = u
     ...   | no k∉kl rewrite sym (insert-keys-∉ {v = v} k∉kl) = Unique-append k∉kl u
 
+    union-subset-keys : ∀ {l₁ l₂ : List (A × B)} →
+                        All (λ k → k ∈k l₂) (keys l₁) →
+                        keys l₂ ≡ keys (union l₁ l₂)
+    union-subset-keys {[]} _ = refl
+    union-subset-keys {(k , v) ∷ l₁'} (k∈kl₂ ∷ kl₁'⊆kl₂)
+        rewrite union-subset-keys kl₁'⊆kl₂ =
+        insert-keys-∈ k∈kl₂
+
+    union-equal-keys : ∀ {l₁ l₂ : List (A × B)} →
+                       keys l₁ ≡ keys l₂ → keys l₁ ≡ keys (union l₁ l₂)
+    union-equal-keys {l₁} {l₂} kl₁≡kl₂
+        with subst (λ l → All (λ k → k ∈ l) (keys l₁)) kl₁≡kl₂ (All-x∈xs (keys l₁))
+    ...   | kl₁⊆kl₂ = trans kl₁≡kl₂ (union-subset-keys {l₁} {l₂} kl₁⊆kl₂)
+
     union-preserves-Unique : ∀ (l₁ l₂ : List (A × B)) →
                              Unique (keys l₂) → Unique (keys (union l₁ l₂))
     union-preserves-Unique [] l₂ u₂ = u₂
@@ -366,6 +360,29 @@ private module ImplInsert (f : B → B → B) where
             let (k∈kl₁ , k∈kxs) = restrict-needs-both k∈l₁xs
             in (k∈kl₁ , there k∈kxs)
 
+    restrict-subset-keys : ∀ {l₁ l₂ : List (A × B)} →
+                           All (λ k → k ∈k l₁) (keys l₂) →
+                           keys l₂ ≡ keys (restrict l₁ l₂)
+    restrict-subset-keys {l₁} {[]} _ = refl
+    restrict-subset-keys {l₁} {(k , v) ∷ l₂'} (k∈kl₁ ∷ kl₂'⊆kl₁)
+        with ∈k-dec k l₁
+    ...   | no k∉kl₁ = ⊥-elim (k∉kl₁ k∈kl₁)
+    ...   | yes _ rewrite restrict-subset-keys {l₁} {l₂'} kl₂'⊆kl₁ = refl
+
+    restrict-equal-keys : ∀ {l₁ l₂ : List (A × B)} →
+                          keys l₁ ≡ keys l₂ →
+                          keys l₁ ≡ keys (restrict l₁ l₂)
+    restrict-equal-keys {l₁} {l₂} kl₁≡kl₂
+        with subst (λ l → All (λ k → k ∈ l) (keys l₂)) (sym kl₁≡kl₂) (All-x∈xs (keys l₂))
+    ...   | kl₂⊆kl₁ = trans kl₁≡kl₂ (restrict-subset-keys {l₁} {l₂} kl₂⊆kl₁)
+
+    intersect-equal-keys : ∀ {l₁ l₂ : List (A × B)} →
+                           keys l₁ ≡ keys l₂ →
+                           keys l₁ ≡ keys (intersect l₁ l₂)
+    intersect-equal-keys {l₁} {l₂} kl₁≡kl₂
+        rewrite restrict-equal-keys (trans kl₁≡kl₂ (updates-keys {l₁} {l₂}))
+        rewrite updates-keys {l₁} {l₂} = refl
+
     restrict-preserves-∉₁ : ∀ {k : A} {l₁ l₂ : List (A × B)} →
                             ¬ k ∈k l₁ → ¬ k ∈k restrict l₁ l₂
     restrict-preserves-∉₁ {k} {l₁} {l₂} k∉kl₁ k∈kl₁l₂ =
@@ -448,13 +465,16 @@ private module ImplInsert (f : B → B → B) where
 
 
 Map : Set (a ⊔ℓ b)
-Map = Σ (List (A × B)) (λ l → Unique (keys l))
+Map = Σ (List (A × B)) (λ l → Unique (ImplKeys.keys l))
+
+keys : Map → List A
+keys (kvs , _) = ImplKeys.keys kvs
 
 _∈_ : (A × B) → Map → Set (a ⊔ℓ b)
 _∈_ p (kvs , _) = MemProp._∈_ p kvs
 
 _∈k_ : A → Map → Set a
-_∈k_ k (kvs , _) = MemProp._∈_ k (keys kvs)
+_∈k_ k m = MemProp._∈_ k (keys m)
 
 Map-functional : ∀ {k : A} {v v' : B} {m : Map} → (k , v) ∈ m → (k , v') ∈ m → v ≡ v'
 Map-functional {m = (l , ul)} k,v∈m k,v'∈m = ListAB-functional ul k,v∈m k,v'∈m
@@ -492,8 +512,8 @@ data Expr : Set (a ⊔ℓ b) where
     _∪_ : Expr → Expr → Expr
     _∩_ : Expr → Expr → Expr
 
-open ImplInsert _⊔₂_ using (union-preserves-Unique) renaming (insert to insert-impl; union to union-impl)
-open ImplInsert _⊓₂_ using (intersect-preserves-Unique) renaming (intersect to intersect-impl)
+open ImplInsert _⊔₂_ using (union-preserves-Unique; union-equal-keys) renaming (insert to insert-impl; union to union-impl)
+open ImplInsert _⊓₂_ using (intersect-preserves-Unique; intersect-equal-keys) renaming (intersect to intersect-impl)
 
 _⊔_ : Map → Map → Map
 _⊔_ (kvs₁ , _) (kvs₂ , uks₂) = (union-impl kvs₁ kvs₂ , union-preserves-Unique kvs₁ kvs₂ uks₂)
@@ -553,45 +573,46 @@ Expr-Provenance k (e₁ ∩ e₂) k∈ke₁e₂
 ...   | no k∉ke₁ | yes k∈ke₂ = ⊥-elim (intersect-preserves-∉₁ {l₂ = proj₁ ⟦ e₂ ⟧} k∉ke₁ k∈ke₁e₂)
 ...   | no k∉ke₁ | no k∉ke₂ = ⊥-elim (intersect-preserves-∉₂ {l₁ = proj₁ ⟦ e₁ ⟧} k∉ke₂ k∈ke₁e₂)
 
-data SubsetInfo (m₁ m₂ : Map) : Set (a ⊔ℓ b) where
-    extra : (k : A) → k ∈k m₁ → ¬ k ∈k m₂ → SubsetInfo m₁ m₂
-    mismatch : (k : A) (v₁ v₂ : B) → (k , v₁) ∈ m₁ → (k , v₂) ∈ m₂ → ¬ v₁ ≈₂ v₂ → SubsetInfo m₁ m₂
-    fine : m₁ ⊆ m₂ → SubsetInfo m₁ m₂
-
-SubsetInfo-to-dec : ∀ {m₁ m₂ : Map} → SubsetInfo m₁ m₂ → Dec (m₁ ⊆ m₂)
-SubsetInfo-to-dec (extra k k∈km₁ k∉km₂) =
-    let (v , k,v∈m₁) = locate k∈km₁
-    in no (λ m₁⊆m₂ →
-           let (v' , (_ , k,v'∈m₂)) = m₁⊆m₂ k v k,v∈m₁
-           in k∉km₂ (∈-cong proj₁ k,v'∈m₂))
-SubsetInfo-to-dec {m₁} {m₂} (mismatch k v₁ v₂ k,v₁∈m₁ k,v₂∈m₂ v₁̷≈v₂) =
-    no (λ m₁⊆m₂ →
-        let (v' , (v₁≈v' , k,v'∈m₂)) = m₁⊆m₂ k v₁ k,v₁∈m₁
-        in v₁̷≈v₂ (subst (λ v'' → v₁ ≈₂ v'') (Map-functional {k} {v'} {v₂} {m₂} k,v'∈m₂ k,v₂∈m₂) v₁≈v')) -- for some reason, can't just use subst...
-SubsetInfo-to-dec (fine m₁⊆m₂) = yes m₁⊆m₂
-
 module _ (≈₂-dec : ∀ (b₁ b₂ : B) → Dec (b₁ ≈₂ b₂)) where
-    compute-SubsetInfo : ∀ m₁ m₂ → SubsetInfo m₁ m₂
-    compute-SubsetInfo ([] , _) m₂ = fine (λ k v ())
-    compute-SubsetInfo m₁@((k , v) ∷ xs₁ , push k≢xs₁ uxs₁) m₂@(l₂ , u₂)
-        with compute-SubsetInfo (xs₁ , uxs₁) m₂
-    ...   | extra k' k'∈kxs₁ k'∉km₂ = extra k' (there k'∈kxs₁) k'∉km₂
-    ...   | mismatch k' v₁ v₂ k',v₁∈xs₁ k',v₂∈m₂ v₁̷≈v₂ =
-            mismatch k' v₁ v₂ (there k',v₁∈xs₁) k',v₂∈m₂ v₁̷≈v₂
-    ...   | fine xs₁⊆m₂ with ∈k-dec k l₂
-    ...       | no k∉km₂ = extra k (here refl) k∉km₂
-    ...       | yes k∈km₂ with locate k∈km₂
-    ...           | (v' , k,v'∈m₂) with ≈₂-dec v v'
-    ...               | no v̷≈v' = mismatch k v v' (here refl) (k,v'∈m₂) v̷≈v'
-    ...               | yes v≈v' = fine m₁⊆m₂
-                            where
-                                m₁⊆m₂ : m₁ ⊆ m₂
-                                m₁⊆m₂ k' v'' (here k,v≡k',v'')
-                                    rewrite cong proj₁ k,v≡k',v''
-                                    rewrite cong proj₂ k,v≡k',v'' =
-                                    (v' , (v≈v' , k,v'∈m₂))
-                                m₁⊆m₂ k' v'' (there k,v≡k',v'') =
-                                    xs₁⊆m₂ k' v'' k,v≡k',v''
+    private module _ where
+        data SubsetInfo (m₁ m₂ : Map) : Set (a ⊔ℓ b) where
+            extra : (k : A) → k ∈k m₁ → ¬ k ∈k m₂ → SubsetInfo m₁ m₂
+            mismatch : (k : A) (v₁ v₂ : B) → (k , v₁) ∈ m₁ → (k , v₂) ∈ m₂ → ¬ v₁ ≈₂ v₂ → SubsetInfo m₁ m₂
+            fine : m₁ ⊆ m₂ → SubsetInfo m₁ m₂
+
+        SubsetInfo-to-dec : ∀ {m₁ m₂ : Map} → SubsetInfo m₁ m₂ → Dec (m₁ ⊆ m₂)
+        SubsetInfo-to-dec (extra k k∈km₁ k∉km₂) =
+            let (v , k,v∈m₁) = locate k∈km₁
+            in no (λ m₁⊆m₂ →
+                   let (v' , (_ , k,v'∈m₂)) = m₁⊆m₂ k v k,v∈m₁
+                   in k∉km₂ (∈-cong proj₁ k,v'∈m₂))
+        SubsetInfo-to-dec {m₁} {m₂} (mismatch k v₁ v₂ k,v₁∈m₁ k,v₂∈m₂ v₁̷≈v₂) =
+            no (λ m₁⊆m₂ →
+                let (v' , (v₁≈v' , k,v'∈m₂)) = m₁⊆m₂ k v₁ k,v₁∈m₁
+                in v₁̷≈v₂ (subst (λ v'' → v₁ ≈₂ v'') (Map-functional {k} {v'} {v₂} {m₂} k,v'∈m₂ k,v₂∈m₂) v₁≈v')) -- for some reason, can't just use subst...
+        SubsetInfo-to-dec (fine m₁⊆m₂) = yes m₁⊆m₂
+
+        compute-SubsetInfo : ∀ m₁ m₂ → SubsetInfo m₁ m₂
+        compute-SubsetInfo ([] , _) m₂ = fine (λ k v ())
+        compute-SubsetInfo m₁@((k , v) ∷ xs₁ , push k≢xs₁ uxs₁) m₂@(l₂ , u₂)
+            with compute-SubsetInfo (xs₁ , uxs₁) m₂
+        ...   | extra k' k'∈kxs₁ k'∉km₂ = extra k' (there k'∈kxs₁) k'∉km₂
+        ...   | mismatch k' v₁ v₂ k',v₁∈xs₁ k',v₂∈m₂ v₁̷≈v₂ =
+                mismatch k' v₁ v₂ (there k',v₁∈xs₁) k',v₂∈m₂ v₁̷≈v₂
+        ...   | fine xs₁⊆m₂ with ∈k-dec k l₂
+        ...       | no k∉km₂ = extra k (here refl) k∉km₂
+        ...       | yes k∈km₂ with locate k∈km₂
+        ...           | (v' , k,v'∈m₂) with ≈₂-dec v v'
+        ...               | no v̷≈v' = mismatch k v v' (here refl) (k,v'∈m₂) v̷≈v'
+        ...               | yes v≈v' = fine m₁⊆m₂
+                                where
+                                    m₁⊆m₂ : m₁ ⊆ m₂
+                                    m₁⊆m₂ k' v'' (here k,v≡k',v'')
+                                        rewrite cong proj₁ k,v≡k',v''
+                                        rewrite cong proj₂ k,v≡k',v'' =
+                                        (v' , (v≈v' , k,v'∈m₂))
+                                    m₁⊆m₂ k' v'' (there k,v≡k',v'') =
+                                        xs₁⊆m₂ k' v'' k,v≡k',v''
 
     ⊆-dec : ∀ m₁ m₂ → Dec (m₁ ⊆ m₂)
     ⊆-dec m₁ m₂ = SubsetInfo-to-dec (compute-SubsetInfo m₁ m₂)
@@ -860,3 +881,9 @@ isLattice = record
     ; absorb-⊔-⊓ = absorb-⊔-⊓
     ; absorb-⊓-⊔ = absorb-⊓-⊔
     }
+
+⊔-equal-keys : ∀ {m₁ m₂ : Map} → keys m₁ ≡ keys m₂ → keys m₁ ≡ keys (m₁ ⊔ m₂)
+⊔-equal-keys km₁≡km₂ = union-equal-keys km₁≡km₂
+
+⊓-equal-keys : ∀ {m₁ m₂ : Map} → keys m₁ ≡ keys m₂ → keys m₁ ≡ keys (m₁ ⊓ m₂)
+⊓-equal-keys km₁≡km₂ = intersect-equal-keys km₁≡km₂

Lattice/Prod.agda

@@ -94,6 +94,16 @@ isLattice = record
         )
     }
 
+
+module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_) where
+    ≈-dec : IsDecidable _≈_
+    ≈-dec (a₁ , b₁) (a₂ , b₂)
+        with ≈₁-dec a₁ a₂ | ≈₂-dec b₁ b₂
+    ...   | yes a₁≈a₂ | yes b₁≈b₂ = yes (a₁≈a₂ , b₁≈b₂)
+    ...   | no a₁̷≈a₂ | _ = no (λ (a₁≈a₂ , _) → a₁̷≈a₂ a₁≈a₂)
+    ...   | _ | no b₁̷≈b₂ = no (λ (_ , b₁≈b₂) → b₁̷≈b₂ b₁≈b₂)
+
+
 module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
          (h₁ h₂ : ℕ)
          (fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where

Utils.agda

@@ -0,0 +1,41 @@
+module Utils where
+
+open import Data.Nat using (ℕ; suc)
+open import Data.List using (List; []; _∷_; _++_)
+open import Data.List.Membership.Propositional using (_∈_)
+open import Data.List.Relation.Unary.All using (All; []; _∷_; map)
+open import Data.List.Relation.Unary.Any using (Any; here; there) -- TODO: re-export these with nicer names from map
+open import Relation.Binary.PropositionalEquality using (_≡_; sym; refl)
+open import Relation.Nullary using (¬_)
+
+data Unique {c} {C : Set c} : List C → Set c where
+    empty : Unique []
+    push : ∀ {x : C} {xs : List C}
+        → All (λ x' → ¬ x ≡ x') xs
+        → Unique xs
+        → Unique (x ∷ xs)
+
+Unique-append : ∀ {c} {C : Set c} {x : C} {xs : List C} →
+                ¬ x ∈ xs → Unique xs →  Unique (xs ++ (x ∷ []))
+Unique-append {c} {C} {x} {[]} _ _ = push [] empty
+Unique-append {c} {C} {x} {x' ∷ xs'} x∉xs (push x'≢ uxs') =
+    push (help x'≢) (Unique-append (λ x∈xs' → x∉xs (there x∈xs')) uxs')
+    where
+        x'≢x : ¬ x' ≡ x
+        x'≢x x'≡x = x∉xs (here (sym x'≡x))
+
+        help : {l : List C} → All (λ x'' → ¬ x' ≡ x'') l → All (λ x'' → ¬ x' ≡ x'') (l ++ (x ∷ []))
+        help {[]} _ = x'≢x ∷ []
+        help {e ∷ es} (x'≢e ∷ x'≢es) = x'≢e ∷ help x'≢es
+
+All¬-¬Any : ∀ {p c} {C : Set c} {P : C → Set p} {l : List C} → All (λ x → ¬ P x) l → ¬ Any P l
+All¬-¬Any {l = x ∷ xs} (¬Px ∷ _) (here Px) = ¬Px Px
+All¬-¬Any {l = x ∷ xs} (_ ∷ ¬Pxs) (there Pxs) = All¬-¬Any ¬Pxs Pxs
+
+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')
+
+iterate : ∀ {a} {A : Set a} (n : ℕ) → (f : A → A) → A → A
+iterate 0 _ a = a
+iterate (suc n) f a = f (iterate n f a)