Lattice.agda

@@ -145,14 +145,3 @@ 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

@@ -1,78 +0,0 @@
-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

@@ -1,107 +0,0 @@
-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,7 +19,6 @@ 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
@@ -29,13 +28,35 @@ open IsLattice lB using () renaming
     ; absorb-⊔-⊓ to absorb-⊔₂-⊓₂; absorb-⊓-⊔ to absorb-⊓₂-⊔₂
     )
 
-private module ImplKeys where
+keys : List (A × B) → List A
-    keys : List (A × B) → List A
+keys = map proj₁
-    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 _ 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)
@@ -87,7 +108,6 @@ 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
@@ -133,20 +153,6 @@ 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₂
@@ -360,29 +366,6 @@ 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₂ =
@@ -465,16 +448,13 @@ private module ImplInsert (f : B → B → B) where
 
 
 Map : Set (a ⊔ℓ b)
-Map = Σ (List (A × B)) (λ l → Unique (ImplKeys.keys l))
+Map = Σ (List (A × B)) (λ l → Unique (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 m = MemProp._∈_ k (keys m)
+_∈k_ k (kvs , _) = MemProp._∈_ k (keys kvs)
 
 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
@@ -512,8 +492,8 @@ data Expr : Set (a ⊔ℓ b) where
     _∪_ : Expr → Expr → Expr
     _∩_ : Expr → Expr → Expr
 
-open ImplInsert _⊔₂_ using (union-preserves-Unique; union-equal-keys) renaming (insert to insert-impl; union to union-impl)
+open ImplInsert _⊔₂_ using (union-preserves-Unique) renaming (insert to insert-impl; union to union-impl)
-open ImplInsert _⊓₂_ using (intersect-preserves-Unique; intersect-equal-keys) renaming (intersect to intersect-impl)
+open ImplInsert _⊓₂_ using (intersect-preserves-Unique) renaming (intersect to intersect-impl)
 
 _⊔_ : Map → Map → Map
 _⊔_ (kvs₁ , _) (kvs₂ , uks₂) = (union-impl kvs₁ kvs₂ , union-preserves-Unique kvs₁ kvs₂ uks₂)
@@ -573,46 +553,45 @@ 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
-    private module _ where
+    compute-SubsetInfo : ∀ m₁ m₂ → SubsetInfo m₁ m₂
-        data SubsetInfo (m₁ m₂ : Map) : Set (a ⊔ℓ b) where
+    compute-SubsetInfo ([] , _) m₂ = fine (λ k v ())
-            extra : (k : A) → k ∈k m₁ → ¬ k ∈k m₂ → SubsetInfo m₁ m₂
+    compute-SubsetInfo m₁@((k , v) ∷ xs₁ , push k≢xs₁ uxs₁) m₂@(l₂ , u₂)
-            mismatch : (k : A) (v₁ v₂ : B) → (k , v₁) ∈ m₁ → (k , v₂) ∈ m₂ → ¬ v₁ ≈₂ v₂ → SubsetInfo m₁ m₂
+        with compute-SubsetInfo (xs₁ , uxs₁) m₂
-            fine : m₁ ⊆ m₂ → SubsetInfo m₁ 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₂ =
-        SubsetInfo-to-dec : ∀ {m₁ m₂ : Map} → SubsetInfo m₁ m₂ → Dec (m₁ ⊆ m₂)
+            mismatch k' v₁ v₂ (there k',v₁∈xs₁) k',v₂∈m₂ v₁̷≈v₂
-        SubsetInfo-to-dec (extra k k∈km₁ k∉km₂) =
+    ...   | fine xs₁⊆m₂ with ∈k-dec k l₂
-            let (v , k,v∈m₁) = locate k∈km₁
+    ...       | no k∉km₂ = extra k (here refl) k∉km₂
-            in no (λ m₁⊆m₂ →
+    ...       | yes k∈km₂ with locate k∈km₂
-                   let (v' , (_ , k,v'∈m₂)) = m₁⊆m₂ k v k,v∈m₁
+    ...           | (v' , k,v'∈m₂) with ≈₂-dec v v'
-                   in k∉km₂ (∈-cong proj₁ k,v'∈m₂))
+    ...               | no v̷≈v' = mismatch k v v' (here refl) (k,v'∈m₂) v̷≈v'
-        SubsetInfo-to-dec {m₁} {m₂} (mismatch k v₁ v₂ k,v₁∈m₁ k,v₂∈m₂ v₁̷≈v₂) =
+    ...               | yes v≈v' = fine m₁⊆m₂
-            no (λ m₁⊆m₂ →
+                            where
-                let (v' , (v₁≈v' , k,v'∈m₂)) = m₁⊆m₂ k v₁ k,v₁∈m₁
+                                m₁⊆m₂ : m₁ ⊆ 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...
+                                m₁⊆m₂ k' v'' (here k,v≡k',v'')
-        SubsetInfo-to-dec (fine m₁⊆m₂) = yes m₁⊆m₂
+                                    rewrite cong proj₁ k,v≡k',v''
-
+                                    rewrite cong proj₂ k,v≡k',v'' =
-        compute-SubsetInfo : ∀ m₁ m₂ → SubsetInfo m₁ m₂
+                                    (v' , (v≈v' , k,v'∈m₂))
-        compute-SubsetInfo ([] , _) m₂ = fine (λ k v ())
+                                m₁⊆m₂ k' v'' (there k,v≡k',v'') =
-        compute-SubsetInfo m₁@((k , v) ∷ xs₁ , push k≢xs₁ uxs₁) m₂@(l₂ , u₂)
+                                    xs₁⊆m₂ k' v'' k,v≡k',v''
-            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₂)
@@ -881,9 +860,3 @@ 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,16 +94,6 @@ 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

@@ -1,41 +0,0 @@
-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)