Analysis/Sign.agda

@@ -1,50 +0,0 @@
-module Analysis.Sign where
-
-open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
-open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans)
-open import Relation.Nullary using (¬_; Dec; yes; no)
-
-open import Language
-open import Lattice
-
-data Sign : Set where
-    + : Sign
-    - : Sign
-    0ˢ : Sign
-
--- g for siGn; s is used for strings and i is not very descriptive.
-_≟ᵍ_ : IsDecidable (_≡_ {_} {Sign})
-_≟ᵍ_ + + = yes refl
-_≟ᵍ_ + - = no (λ ())
-_≟ᵍ_ + 0ˢ = no (λ ())
-_≟ᵍ_ - + = no (λ ())
-_≟ᵍ_ - - = yes refl
-_≟ᵍ_ - 0ˢ = no (λ ())
-_≟ᵍ_ 0ˢ + = no (λ ())
-_≟ᵍ_ 0ˢ - = no (λ ())
-_≟ᵍ_ 0ˢ 0ˢ = yes refl
-
-module _ (prog : Program) where
-    open Program prog
-
-    -- embelish 'sign' with a top and bottom element.
-    open import Lattice.AboveBelow Sign _≡_ (record { ≈-refl = refl; ≈-sym = sym; ≈-trans = trans }) _≟ᵍ_ as AB renaming (AboveBelow to SignLattice; ≈-dec to ≈ᵍ-dec)
-    -- 'sign' has no underlying lattice structure, so use the 'plain' above-below lattice.
-    open AB.Plain using () renaming (finiteHeightLattice to finiteHeightLatticeᵍ-if-inhabited)
-
-
-    finiteHeightLatticeᵍ = finiteHeightLatticeᵍ-if-inhabited 0ˢ
-
-    -- The variable -> sign map is a finite value-map with keys strings. Use a bundle to avoid explicitly specifying operators.
-    open import Lattice.Bundles.FiniteValueMap String SignLattice _≟ˢ_ renaming (finiteHeightLattice to finiteHeightLatticeᵛ-if-B-finite; FiniteHeightType to FiniteHeightTypeᵛ; _≈_ to _≈ᵛ_; ≈-dec to ≈ᵛ-dec-if-≈ᵍ-dec)
-
-
-    VariableSigns = FiniteHeightTypeᵛ finiteHeightLatticeᵍ vars-Unique ≈ᵍ-dec
-    finiteHeightLatticeᵛ = finiteHeightLatticeᵛ-if-B-finite finiteHeightLatticeᵍ vars-Unique ≈ᵍ-dec
-    ≈ᵛ-dec = ≈ᵛ-dec-if-≈ᵍ-dec finiteHeightLatticeᵍ vars-Unique ≈ᵍ-dec
-
-    -- Finally, the map we care about is (state -> (variables -> sign)). Bring that in.
-    open import Lattice.Bundles.FiniteValueMap State VariableSigns _≟_ renaming (finiteHeightLattice to finiteHeightLatticeᵐ-if-B-finite; FiniteHeightType to FiniteHeightTypeᵐ)
-
-    StateVariables = FiniteHeightTypeᵐ finiteHeightLatticeᵛ states-Unique ≈ᵛ-dec
-    finiteHeightLatticeᵐ = finiteHeightLatticeᵐ-if-B-finite finiteHeightLatticeᵛ states-Unique ≈ᵛ-dec

Homomorphism.agda

@@ -0,0 +1,149 @@
+open import Equivalence
+
+module Homomorphism {a b} (A : Set a) (B : Set b)
+    (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set b)
+    (≈₂-equiv : IsEquivalence B _≈₂_)
+    (f : A → B) where
+
+open import Agda.Primitive using (lsuc; Level) renaming (_⊔_ to _⊔ℓ_)
+open import Function.Definitions using (Surjective)
+open import Relation.Binary.Core using (_Preserves_⟶_ )
+open import Data.Product using (_,_)
+open import Lattice
+
+open IsEquivalence ≈₂-equiv using () renaming (≈-trans to ≈₂-trans; ≈-sym to ≈₂-sym; ≈-refl to ≈₂-refl)
+open import Relation.Binary.Reasoning.Base.Single _≈₂_ ≈₂-refl ≈₂-trans
+
+infixl 20 _∙₂_
+_∙₂_ = ≈₂-trans
+
+record SemilatticeHomomorphism (_⊔₁_ : A → A → A)
+                               (_⊔₂_ : B → B → B) : Set (a ⊔ℓ b) where
+    field
+        f-preserves-≈ : f Preserves _≈₁_ ⟶  _≈₂_
+        f-⊔-distr : ∀ (a₁ a₂ : A) → f (a₁ ⊔₁ a₂) ≈₂ ((f a₁) ⊔₂ (f a₂))
+
+module _ (_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B)
+         (sh : SemilatticeHomomorphism _⊔₁_ _⊔₂_)
+         (≈₂-⊔₂-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≈₂ a₂ → a₃ ≈₂ a₄ → (a₁ ⊔₂ a₃) ≈₂ (a₂ ⊔₂ a₄))
+         (surF : Surjective _≈₁_ _≈₂_ f) where
+
+    open SemilatticeHomomorphism sh
+
+    transportSemilattice : IsSemilattice A _≈₁_ _⊔₁_ → IsSemilattice B _≈₂_ _⊔₂_
+    transportSemilattice sA = record
+        { ≈-equiv = ≈₂-equiv
+        ; ≈-⊔-cong = ≈₂-⊔₂-cong
+        ; ⊔-assoc = λ b₁ b₂ b₃ →
+            let (a₁ , fa₁≈b₁) = surF b₁
+                (a₂ , fa₂≈b₂) = surF b₂
+                (a₃ , fa₃≈b₃) = surF b₃
+            in
+               begin
+                   (b₁ ⊔₂ b₂) ⊔₂ b₃
+               ∼⟨ ≈₂-⊔₂-cong (≈₂-⊔₂-cong (≈₂-sym fa₁≈b₁) (≈₂-sym fa₂≈b₂)) (≈₂-sym fa₃≈b₃) ⟩
+                   (f a₁ ⊔₂ f a₂) ⊔₂ f a₃
+               ∼⟨ ≈₂-⊔₂-cong (≈₂-sym (f-⊔-distr a₁ a₂)) ≈₂-refl ⟩
+                   f (a₁ ⊔₁ a₂) ⊔₂ f a₃
+               ∼⟨ ≈₂-sym (f-⊔-distr (a₁ ⊔₁ a₂) a₃) ⟩
+                   f ((a₁ ⊔₁ a₂) ⊔₁ a₃)
+               ∼⟨ f-preserves-≈ (IsSemilattice.⊔-assoc sA a₁ a₂ a₃) ⟩
+                   f (a₁ ⊔₁ (a₂ ⊔₁ a₃))
+               ∼⟨ f-⊔-distr a₁ (a₂ ⊔₁ a₃) ⟩
+                   f a₁ ⊔₂ f (a₂ ⊔₁ a₃)
+               ∼⟨ ≈₂-⊔₂-cong ≈₂-refl (f-⊔-distr a₂ a₃) ⟩
+                   f a₁ ⊔₂ (f a₂ ⊔₂ f a₃)
+               ∼⟨ ≈₂-⊔₂-cong fa₁≈b₁ (≈₂-⊔₂-cong fa₂≈b₂ fa₃≈b₃) ⟩
+                   b₁ ⊔₂ (b₂ ⊔₂ b₃)
+               ∎
+        ; ⊔-comm = λ b₁ b₂ →
+            let (a₁ , fa₁≈b₁) = surF b₁
+                (a₂ , fa₂≈b₂) = surF b₂
+            in
+               begin
+                   b₁ ⊔₂ b₂
+               ∼⟨ ≈₂-⊔₂-cong (≈₂-sym fa₁≈b₁) (≈₂-sym fa₂≈b₂) ⟩
+                   f a₁ ⊔₂ f a₂
+               ∼⟨ ≈₂-sym (f-⊔-distr a₁ a₂) ⟩
+                   f (a₁ ⊔₁ a₂)
+               ∼⟨ f-preserves-≈ (IsSemilattice.⊔-comm sA a₁ a₂) ⟩
+                   f (a₂ ⊔₁ a₁)
+               ∼⟨ f-⊔-distr a₂ a₁ ⟩
+                   f a₂ ⊔₂ f a₁
+               ∼⟨ ≈₂-⊔₂-cong fa₂≈b₂ fa₁≈b₁ ⟩
+                   b₂ ⊔₂ b₁
+               ∎
+        ; ⊔-idemp = λ b →
+            let (a , fa≈b) = surF b
+            in
+               begin
+                   b ⊔₂ b
+               ∼⟨ ≈₂-⊔₂-cong (≈₂-sym fa≈b) (≈₂-sym fa≈b) ⟩
+                   f a ⊔₂ f a
+               ∼⟨ ≈₂-sym (f-⊔-distr a a) ⟩
+                   f (a ⊔₁ a)
+               ∼⟨ f-preserves-≈ (IsSemilattice.⊔-idemp sA a) ⟩
+                   f a
+               ∼⟨ fa≈b ⟩
+                   b
+               ∎
+        }
+
+
+record LatticeHomomorphism (_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B)
+                           (_⊓₁_ : A → A → A) (_⊓₂_ : B → B → B) : Set (a ⊔ℓ b) where
+    field
+        ⊔-homomorphism : SemilatticeHomomorphism _⊔₁_ _⊔₂_
+        ⊓-homomorphism : SemilatticeHomomorphism _⊓₁_ _⊓₂_
+
+    open SemilatticeHomomorphism ⊔-homomorphism using (f-⊔-distr; f-preserves-≈) public
+    open SemilatticeHomomorphism ⊓-homomorphism using () renaming (f-⊔-distr to f-⊓-distr) public
+
+module _ (_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B)
+         (_⊓₁_ : A → A → A) (_⊓₂_ : B → B → B)
+         (lh : LatticeHomomorphism _⊔₁_ _⊔₂_ _⊓₁_ _⊓₂_)
+         (≈₂-⊔₂-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≈₂ a₂ → a₃ ≈₂ a₄ → (a₁ ⊔₂ a₃) ≈₂ (a₂ ⊔₂ a₄))
+         (≈₂-⊓₂-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≈₂ a₂ → a₃ ≈₂ a₄ → (a₁ ⊓₂ a₃) ≈₂ (a₂ ⊓₂ a₄))
+         (surF : Surjective _≈₁_ _≈₂_ f) where
+
+    open LatticeHomomorphism lh
+
+    transportLattice : IsLattice A _≈₁_ _⊔₁_ _⊓₁_ → IsLattice B _≈₂_ _⊔₂_ _⊓₂_
+    transportLattice lA = record
+        { joinSemilattice = transportSemilattice _⊔₁_ _⊔₂_ (LatticeHomomorphism.⊔-homomorphism lh) ≈₂-⊔₂-cong surF (IsLattice.joinSemilattice lA)
+        ; meetSemilattice = transportSemilattice _⊓₁_ _⊓₂_ (LatticeHomomorphism.⊓-homomorphism lh) ≈₂-⊓₂-cong surF (IsLattice.meetSemilattice lA)
+        ; absorb-⊔-⊓ = λ b₁ b₂ →
+            let (a₁ , fa₁≈b₁) = surF b₁
+                (a₂ , fa₂≈b₂) = surF b₂
+            in
+               begin
+                   b₁ ⊔₂ (b₁ ⊓₂ b₂)
+               ∼⟨ ≈₂-⊔₂-cong (≈₂-sym fa₁≈b₁) (≈₂-⊓₂-cong (≈₂-sym fa₁≈b₁) (≈₂-sym fa₂≈b₂)) ⟩
+                   f a₁ ⊔₂ (f a₁ ⊓₂ f a₂)
+               ∼⟨ ≈₂-⊔₂-cong ≈₂-refl (≈₂-sym (f-⊓-distr a₁ a₂)) ⟩
+                   f a₁ ⊔₂ f (a₁ ⊓₁ a₂)
+               ∼⟨ ≈₂-sym (f-⊔-distr a₁ (a₁ ⊓₁ a₂)) ⟩
+                   f (a₁ ⊔₁ (a₁ ⊓₁ a₂))
+               ∼⟨ f-preserves-≈ (IsLattice.absorb-⊔-⊓ lA a₁ a₂) ⟩
+                   f a₁
+               ∼⟨ fa₁≈b₁ ⟩
+                   b₁
+               ∎
+        ; absorb-⊓-⊔ = λ b₁ b₂ →
+            let (a₁ , fa₁≈b₁) = surF b₁
+                (a₂ , fa₂≈b₂) = surF b₂
+            in
+               begin
+                   b₁ ⊓₂ (b₁ ⊔₂ b₂)
+               ∼⟨ ≈₂-⊓₂-cong (≈₂-sym fa₁≈b₁) (≈₂-⊔₂-cong (≈₂-sym fa₁≈b₁) (≈₂-sym fa₂≈b₂)) ⟩
+                   f a₁ ⊓₂ (f a₁ ⊔₂ f a₂)
+               ∼⟨ ≈₂-⊓₂-cong ≈₂-refl (≈₂-sym (f-⊔-distr a₁ a₂)) ⟩
+                   f a₁ ⊓₂ f (a₁ ⊔₁ a₂)
+               ∼⟨ ≈₂-sym (f-⊓-distr a₁ (a₁ ⊔₁ a₂)) ⟩
+                   f (a₁ ⊓₁ (a₁ ⊔₁ a₂))
+               ∼⟨ f-preserves-≈ (IsLattice.absorb-⊓-⊔ lA a₁ a₂) ⟩
+                   f a₁
+               ∼⟨ fa₁≈b₁ ⟩
+                   b₁
+               ∎
+        }

Language.agda

@@ -1,93 +1,10 @@
 module Language where
 
-open import Data.Nat using (ℕ; suc; pred)
-open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
-open import Data.Product using (Σ; _,_; proj₁; proj₂)
-open import Data.Vec using (Vec; foldr)
-open import Data.List using ([]; _∷_; List) renaming (foldr to foldrˡ; map to mapˡ)
-open import Data.List.Relation.Unary.All using (All; []; _∷_)
-open import Data.Fin using (Fin; suc; zero; fromℕ; inject₁) renaming (_≟_ to _≟ᶠ_)
-open import Data.Fin.Properties using (suc-injective)
-open import Relation.Binary.PropositionalEquality using (cong; _≡_)
-open import Relation.Nullary using (¬_)
-open import Function using (_∘_)
-
-open import Lattice
-open import Utils using (Unique; Unique-map; empty; push)
+open import Data.String using (String)
+open import Data.Nat using (ℕ)
 
 data Expr : Set where
     _+_ : Expr → Expr → Expr
     _-_ : Expr → Expr → Expr
     `_ : String → Expr
     #_ : ℕ → Expr
-
-data Stmt : Set where
-    _←_ : String → Expr → Stmt
-
-open import Lattice.MapSet String _≟ˢ_
-    renaming
-        ( MapSet to StringSet
-        ; insert to insertˢ
-        ; to-List to to-Listˢ
-        ; empty to emptyˢ
-        ; _⊔_ to _⊔ˢ_
-        )
-
-private
-    Expr-vars : Expr → StringSet
-    Expr-vars (l + r) = Expr-vars l ⊔ˢ Expr-vars r
-    Expr-vars (l - r) = Expr-vars l ⊔ˢ Expr-vars r
-    Expr-vars (` s) = insertˢ s emptyˢ
-    Expr-vars (# _) = emptyˢ
-
-    Stmt-vars : Stmt → StringSet
-    Stmt-vars (x ← e) = insertˢ x (Expr-vars e)
-
-    -- Creating a new number from a natural number can never create one
-    -- equal to one you get from weakening the bounds on another number.
-    z≢sf : ∀ {n : ℕ} (f : Fin n) → ¬ (zero ≡ suc f)
-    z≢sf f ()
-
-    z≢mapsfs : ∀ {n : ℕ} (fs : List (Fin n)) → All (λ sf → ¬ zero ≡ sf) (mapˡ suc fs)
-    z≢mapsfs [] = []
-    z≢mapsfs (f ∷ fs') = z≢sf f ∷ z≢mapsfs fs'
-
-    indices : ∀ (n : ℕ) → Σ (List (Fin n)) Unique
-    indices 0 = ([] , empty)
-    indices (suc n') =
-        let
-            (inds' , unids') = indices n'
-        in
-            ( zero ∷ mapˡ suc inds'
-            , push (z≢mapsfs inds') (Unique-map suc suc-injective unids')
-            )
-
-
--- For now, just represent the program and CFG as one type, without branching.
-record Program : Set where
-    field
-        length : ℕ
-        stmts : Vec Stmt length
-
-    private
-        vars-Set : StringSet
-        vars-Set = foldr (λ n → StringSet)
-                         (λ {k} stmt acc → (Stmt-vars stmt) ⊔ˢ acc) emptyˢ stmts
-
-    vars : List String
-    vars = to-Listˢ vars-Set
-
-    vars-Unique : Unique vars
-    vars-Unique = proj₂ vars-Set
-
-    State : Set
-    State = Fin length
-
-    states : List State
-    states = proj₁ (indices length)
-
-    states-Unique : Unique states
-    states-Unique = proj₂ (indices length)
-
-    _≟_ : IsDecidable (_≡_ {_} {State})
-    _≟_ = _≟ᶠ_

Lattice/Bundles/FiniteValueMap.agda

@@ -19,10 +19,8 @@ module _ (fhB : FiniteHeightLattice B) where
     module _ {ks : List A} (uks : Unique ks) (≈₂-dec : Decidable _≈₂_) where
         import Lattice.FiniteValueMap A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A isLattice₂ as FVM
 
-        FiniteHeightType = FVM.FiniteMap ks
-
-        finiteHeightLattice = FVM.IterProdIsomorphism.finiteHeightLattice uks ≈₂-dec height₂ fixedHeight₂
-        open FiniteHeightLattice finiteHeightLattice public
+        FiniteHeightType = FVM.FiniteMap
 
         ≈-dec = FVM.≈-dec ks ≈₂-dec
 
+        finiteHeightLattice = FVM.IterProdIsomorphism.finiteHeightLattice uks ≈₂-dec height₂ fixedHeight₂

Lattice/FiniteMap.agda

@@ -2,7 +2,7 @@ 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; _∷_; [])
+open import Data.List using (List)
 
 module Lattice.FiniteMap {a b : Level} (A : Set a) (B : Set b)
     (_≈₂_ : B → B → Set b)
@@ -10,9 +10,8 @@ module Lattice.FiniteMap {a b : Level} (A : Set a) (B : Set b)
     (≡-dec-A : IsDecidable (_≡_ {a} {A}))
     (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
 
-open IsLattice lB using () renaming (_≼_ to _≼₂_)
 open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB as Map
-    using (Map; ⊔-equal-keys; ⊓-equal-keys; ∈k-dec; m₁≼m₂⇒m₁[k]≼m₂[k])
+    using (Map; ⊔-equal-keys; ⊓-equal-keys)
     renaming
         ( _≈_ to _≈ᵐ_
         ; _⊔_ to _⊔ᵐ_
@@ -29,21 +28,9 @@ open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB as Map
         ; absorb-⊔-⊓ to absorb-⊔ᵐ-⊓ᵐ
         ; absorb-⊓-⊔ to absorb-⊓ᵐ-⊔ᵐ
         ; ≈-dec to ≈ᵐ-dec
-        ; _[_] to _[_]ᵐ
-        ; locate to locateᵐ
-        ; keys to keysᵐ
-        ; _updating_via_ to _updatingᵐ_via_
-        ; updating-via-keys-≡ to updatingᵐ-via-keys-≡
-        ; f'-Monotonic to f'-Monotonicᵐ
-        ; _≼_ to _≼ᵐ_
         )
-open import Data.List.Membership.Propositional using () renaming (_∈_ to _∈ˡ_)
 open import Data.Product using (_×_; _,_; Σ; proj₁ ; proj₂)
 open import Equivalence
-open import Function using (_∘_)
-open import Relation.Nullary using (¬_; Dec; yes; no)
-open import Utils using (Pairwise; _∷_; [])
-open import Data.Empty using (⊥-elim)
 
 module _ (ks : List A) where
     FiniteMap : Set (a ⊔ℓ b)
@@ -69,18 +56,6 @@ module _ (ks : List A) where
                 km₁≡ks
         )
 
-    _∈k_ : A → FiniteMap → Set a
-    _∈k_ k (m₁ , _) = k ∈ˡ (keysᵐ m₁)
-
-    _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 ]ᵐ
-
     ≈-equiv : IsEquivalence FiniteMap _≈_
     ≈-equiv = record
         { ≈-refl =
@@ -122,8 +97,6 @@ module _ (ks : List A) where
         ; absorb-⊓-⊔ = λ (m₁ , _) (m₂ , _) → absorb-⊓ᵐ-⊔ᵐ m₁ m₂
         }
 
-    open IsLattice isLattice using (_≼_) public
-
     lattice : Lattice FiniteMap
     lattice = record
         { _≈_ = _≈_
@@ -131,46 +104,3 @@ module _ (ks : List A) where
         ; _⊓_ = _⊓_
         ; isLattice = isLattice
         }
-
-    module _ {l} {L : Set l}
-             {_≈ˡ_ : L → L → Set l} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L}
-             (lL : IsLattice L _≈ˡ_ _⊔ˡ_ _⊓ˡ_) where
-        open IsLattice lL using () renaming (_≼_ to _≼ˡ_)
-
-        module _ (f : L → FiniteMap) (f-Monotonic : Monotonic _≼ˡ_ _≼_ f)
-                 (g : A → L → B) (g-Monotonicʳ : ∀ k → Monotonic _≼ˡ_ _≼₂_ (g k))
-                 (ks : List A) where
-
-            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₂
-
-    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₁))

Lattice/Map.agda

@@ -19,7 +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; Unique-append; All¬-¬Any; All-x∈xs)
+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
@@ -34,21 +34,6 @@ private module ImplKeys where
     keys : List (A × B) → List A
     keys = map proj₁
 
--- See note on `forget` for why this is defined in global scope even though
--- it operates on lists.
-∈k-dec : ∀ (k : A) (l : List (A × B)) → Dec (k ∈ˡ (ImplKeys.keys l))
-∈k-dec k [] = no (λ ())
-∈k-dec k ((k' , v) ∷ xs)
-    with (≡-dec-A k k')
-...   | yes k≡k' = yes (here k≡k')
-...   | no k≢k' with (∈k-dec k xs)
-...       | yes k∈kxs = yes (there k∈kxs)
-...       | no k∉kxs = no witness
-              where
-                  witness : ¬ k ∈ˡ (ImplKeys.keys ((k' , v) ∷ xs))
-                  witness (here k≡k') = k≢k' k≡k'
-                  witness (there k∈kxs) = k∉kxs k∈kxs
-
 private module _ where
     open MemProp using (_∈_)
     open ImplKeys
@@ -80,6 +65,19 @@ private module _ where
     ...       | yes k∈xs = yes (there k∈xs)
     ...       | no k∉xs = no (λ { (here k≡x) → k≢x k≡x; (there k∈xs) → k∉xs k∈xs })
 
+    ∈k-dec : ∀ (k : A) (l : List (A × B)) → Dec (k ∈ keys l)
+    ∈k-dec k [] = no (λ ())
+    ∈k-dec k ((k' , v) ∷ xs)
+        with (≡-dec-A k k')
+    ...   | yes k≡k' = yes (here k≡k')
+    ...   | no k≢k' with (∈k-dec k xs)
+    ...       | yes k∈kxs = yes (there k∈kxs)
+    ...       | no k∉kxs = no witness
+                  where
+                      witness : ¬ k ∈ keys ((k' , v) ∷ xs)
+                      witness (here k≡k') = k≢k' k≡k'
+                      witness (there k∈kxs) = k∉kxs k∈kxs
+
     ∈-cong : ∀ {c d} {C : Set c} {D : Set d} {c : C} {l : List C} →
              (f : C → D) → c ∈ l → f c ∈ map f l
     ∈-cong f (here c≡c') = here (cong f c≡c')
@@ -342,7 +340,7 @@ private module ImplInsert (f : B → B → B) where
 
     restrict-preserves-Unique : ∀ {l₁ l₂ : List (A × B)} →
                                 Unique (keys l₂) → Unique (keys (restrict l₁ l₂))
-    restrict-preserves-Unique {l₁} {[]} _ = Utils.empty
+    restrict-preserves-Unique {l₁} {[]} _ = empty
     restrict-preserves-Unique {l₁} {(k , v) ∷ xs} (push k≢xs uxs)
         with ∈k-dec k l₁
     ...   | yes _ = push (restrict-preserves-k≢ k≢xs) (restrict-preserves-Unique uxs)
@@ -478,9 +476,6 @@ private module ImplInsert (f : B → B → B) where
 Map : Set (a ⊔ℓ b)
 Map = Σ (List (A × B)) (λ l → Unique (ImplKeys.keys l))
 
-empty : Map
-empty = ([] , Utils.empty)
-
 keys : Map → List A
 keys (kvs , _) = ImplKeys.keys kvs
 
@@ -493,9 +488,8 @@ _∈k_ k m = MemProp._∈_ k (keys m)
 locate : ∀ {k : A} {m : Map} → k ∈k m → Σ B (λ v → (k , v) ∈ m)
 locate k∈km = locate-impl k∈km
 
--- `forget` and `∈k-dec` are defined this way because ∈ for maps uses
--- projection, so the full map can't be guessed. On the other hand, list can
--- be guessed.
+-- defined this way because ∈ for maps uses projection, so the full map can't be guessed.
+-- On the other hand, list can be guessed.
 forget : ∀ {k : A} {v : B} {l : List (A × B)} → (k , v) ∈ˡ l → k ∈ˡ (ImplKeys.keys l)
 forget = ∈-cong proj₁
 
@@ -535,12 +529,9 @@ data Expr : Set (a ⊔ℓ b) where
     _∪_ : Expr → Expr → Expr
     _∩_ : Expr → Expr → Expr
 
-open ImplInsert _⊔₂_ using (union-preserves-Unique; union-equal-keys; insert-preserves-Unique) renaming (insert to insert-impl; union to union-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)
 
-insert : A → B → Map → Map
-insert k v (l , uks) = (insert-impl k v l , insert-preserves-Unique uks)
-
 _⊔_ : Map → Map → Map
 _⊔_ (kvs₁ , _) (kvs₂ , uks₂) = (union-impl kvs₁ kvs₂ , union-preserves-Unique kvs₁ kvs₂ uks₂)
 
@@ -887,8 +878,6 @@ isLattice = record
     ; absorb-⊓-⊔ = absorb-⊓-⊔
     }
 
-open IsLattice isLattice using (_≼_) public
-
 lattice : Lattice Map
 lattice = record
     { _≈_ = _≈_
@@ -969,10 +958,6 @@ _updating_via_ (kvs , uks) ks f =
     , subst Unique (transform-keys-≡ kvs ks f) uks
     )
 
-updating-via-keys-≡ : ∀ (m : Map) (ks : List A) (f : A → B) →
-                  keys m ≡ keys (m updating ks via f)
-updating-via-keys-≡ (l , _) = transform-keys-≡ l
-
 updating-via-∉k-forward : ∀ (m : Map) (ks : List A) (f : A → B) {k : A} →
                           ¬ k ∈k m → ¬ k ∈k (m updating ks via f)
 updating-via-∉k-forward m = transform-∉k-forward
@@ -1010,6 +995,7 @@ updating-via-k∉ks-backward m = transform-k∉ks-backward
 module _ {l} {L : Set l}
          {_≈ˡ_ : L → L → Set l} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L}
          (lL : IsLattice L _≈ˡ_ _⊔ˡ_ _⊓ˡ_) where
+    open IsLattice isLattice using (_≼_)
     open IsLattice lL using () renaming (_≼_ to _≼ˡ_)
 
     module _ (f : L → Map) (f-Monotonic : Monotonic _≼ˡ_ _≼_ f)
@@ -1086,29 +1072,3 @@ module _ {l} {L : Set l}
                             with refl ← Map-functional {m = f' l₂} k,v∈f'l₂ k,v₂∈f'l₂
                             with refl ← Map-functional {m = f l₂} k,v'∈fl₂ k,v₂∈fl₂ =
                             (v₁ ⊔₂ v , (v'≈v'' , k,v₁v₂∈f'l₁f'l₂))
-
-
-_[_] : Map → List A → List B
-_[_] m [] = []
-_[_] m (k ∷ ks)
-    with ∈k-dec k (proj₁ m)
-...   | yes k∈km = proj₁ (locate {m = m} k∈km) ∷ (m [ ks ])
-...   | no _ = m [ ks ]
-
-m₁≼m₂⇒m₁[k]≼m₂[k] : ∀ (m₁ m₂ : Map) {k : A} {v₁ v₂ : B} →
-                    m₁ ≼ m₂ → (k , v₁) ∈ m₁ → (k , v₂) ∈ m₂ → v₁ ≼₂ v₂
-m₁≼m₂⇒m₁[k]≼m₂[k] m₁ m₂ m₁≼m₂ k,v₁∈m₁ k,v₂∈m₂
-    with k,v₁v₂∈m₁m₂ ← ⊔-combines {m₁ = m₁} {m₂ = m₂} k,v₁∈m₁ k,v₂∈m₂
-    with (v' , (v₁v₂≈v' , k,v'∈m₂)) ← (proj₁ m₁≼m₂) _ _ k,v₁v₂∈m₁m₂
-    with refl ← Map-functional {m = m₂} k,v₂∈m₂ k,v'∈m₂
-    = v₁v₂≈v'
-
-m₁≼m₂⇒k∈km₁⇒k∈km₂ : ∀ (m₁ m₂ : Map) {k : A} →
-                    m₁ ≼ m₂ → k ∈k m₁ → k ∈k m₂
-m₁≼m₂⇒k∈km₁⇒k∈km₂ m₁ m₂ m₁≼m₂ k∈km₁ =
-    let
-        k∈km₁m₂ = union-preserves-∈k₁ {l₁ = proj₁ m₁} {l₂ = proj₁ m₂} k∈km₁
-        (v , k,v∈m₁m₂) = locate {m = m₁ ⊔ m₂} k∈km₁m₂
-        (v' , (v≈v' , k,v'∈m₂)) = (proj₁ m₁≼m₂) _ _ k,v∈m₁m₂
-    in
-        forget k,v'∈m₂

Lattice/MapSet.agda

@@ -5,25 +5,15 @@ open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
 
 module Lattice.MapSet {a : Level} (A : Set a) (≡-dec-A : Decidable (_≡_ {a} {A})) where
 
-open import Data.List using (List; map)
-open import Data.Product using (proj₁)
-open import Function using (_∘_)
-
-open import Lattice.Unit using (⊤; tt) renaming (_≈_ to _≈₂_; _⊔_ to _⊔₂_; _⊓_ to _⊓₂_; isLattice to ⊤-isLattice)
+open import Lattice.Unit using (⊤) renaming (_≈_ to _≈₂_; _⊔_ to _⊔₂_; _⊓_ to _⊓₂_; isLattice to ⊤-isLattice)
 import Lattice.Map
 
 private module UnitMap = Lattice.Map A ⊤ _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A ⊤-isLattice
 open UnitMap using (Map)
 open UnitMap using
-    ( _⊆_; _≈_; ≈-equiv; _⊔_; _⊓_; empty
+    ( _⊆_; _≈_; ≈-equiv; _⊔_; _⊓_
     ; isUnionSemilattice; isIntersectSemilattice; isLattice; lattice
     ) public
 
 MapSet : Set a
 MapSet = Map
-
-to-List : MapSet → List A
-to-List = map proj₁ ∘ proj₁
-
-insert : A → MapSet → MapSet
-insert k = UnitMap.insert k tt

Main.agda

@@ -22,7 +22,7 @@ xyzw-Unique = push ((λ ()) ∷ (λ ()) ∷ (λ ()) ∷ []) (push ((λ ()) ∷ (
 open import Lattice using (IsFiniteHeightLattice; FiniteHeightLattice; Monotonic)
 open import Lattice.AboveBelow ⊤ _≡_ (record { ≈-refl = refl; ≈-sym = sym; ≈-trans = trans }) _≟ᵘ_  as AB using () renaming (≈-dec to ≈ᵘ-dec)
 open AB.Plain using () renaming (finiteHeightLattice to finiteHeightLatticeᵘ)
-open import Lattice.Bundles.FiniteValueMap String AB.AboveBelow _≟ˢ_ using () renaming (finiteHeightLattice to finiteHeightLatticeᵐ; FiniteHeightType to FiniteHeightTypeᵐ; ≈-dec to ≈-dec)
+open import Lattice.Bundles.FiniteValueMap String AB.AboveBelow _≟ˢ_ renaming (finiteHeightLattice to finiteHeightLatticeᵐ; FiniteHeightType to FiniteHeightTypeᵐ; ≈-dec to ≈-dec)
 
 fhlᵘ = finiteHeightLatticeᵘ (Data.Unit.tt)
 
@@ -33,7 +33,7 @@ showAboveBelow AB.⊤ = "⊤"
 showAboveBelow AB.⊥ = "⊥"
 showAboveBelow (AB.[_] tt) = "()"
 
-showMap : FiniteHeightMap → String
+showMap : ∀ {ks : List String} → FiniteHeightMap ks → String
 showMap ((kvs , _) , _) = "{" ++ foldr (λ (x , y) rest → x ++ " ↦ " ++ showAboveBelow y ++ ", " ++ rest) "" kvs ++ "}"
 
 fhlⁱᵖ = finiteHeightLatticeᵐ fhlᵘ xyzw-Unique ≈ᵘ-dec
@@ -44,16 +44,16 @@ open import Relation.Binary.Reasoning.Base.Single _≈_ (λ {m} → ≈-refl {m}
 smallestMap = proj₁ (proj₁ (proj₁ (FiniteHeightLattice.fixedHeight fhlⁱᵖ)))
 largestMap = proj₂ (proj₁ (proj₁ (FiniteHeightLattice.fixedHeight fhlⁱᵖ)))
 
-dumb : FiniteHeightMap
+dumb : FiniteHeightMap xyzw
 dumb = ((("x" , AB.[_] tt) ∷ ("y" , AB.⊥) ∷ ("z" , AB.⊥) ∷ ("w" , AB.⊥) ∷ [] , xyzw-Unique) , refl)
 
-dumbFunction : FiniteHeightMap → FiniteHeightMap
+dumbFunction : FiniteHeightMap xyzw → FiniteHeightMap xyzw
 dumbFunction = _⊔_ dumb
 
 dumbFunction-Monotonic : Monotonic _≼_ _≼_ dumbFunction
 dumbFunction-Monotonic {m₁} {m₂} m₁≼m₂ = ⊔-Monotonicˡ dumb {m₁} {m₂} m₁≼m₂
 
 
-open import Fixedpoint {0ℓ} {FiniteHeightMap} {8} {_≈_} {_⊔_} {_⊓_} (≈-dec fhlᵘ xyzw-Unique ≈ᵘ-dec) (FiniteHeightLattice.isFiniteHeightLattice fhlⁱᵖ) dumbFunction (λ {m₁} {m₂} m₁≼m₂ → dumbFunction-Monotonic {m₁} {m₂} m₁≼m₂)
+open import Fixedpoint {0ℓ} {FiniteHeightMap xyzw} {8} {_≈_} {_⊔_} {_⊓_} (≈-dec fhlᵘ xyzw-Unique ≈ᵘ-dec) (FiniteHeightLattice.isFiniteHeightLattice fhlⁱᵖ) dumbFunction (λ {m₁} {m₂} m₁≼m₂ → dumbFunction-Monotonic {m₁} {m₂} m₁≼m₂)
 
 main = run {0ℓ} (putStrLn (showMap aᶠ))

Utils.agda

@@ -2,11 +2,10 @@ module Utils where
 
 open import Agda.Primitive using () renaming (_⊔_ to _⊔ℓ_)
 open import Data.Nat using (ℕ; suc)
-open import Data.List using (List; []; _∷_; _++_) renaming (map to mapˡ)
+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 Function.Definitions using (Injective)
 open import Relation.Binary.PropositionalEquality using (_≡_; sym; refl)
 open import Relation.Nullary using (¬_)
 
@@ -30,18 +29,6 @@ Unique-append {c} {C} {x} {x' ∷ xs'} x∉xs (push x'≢ uxs') =
         help {[]} _ = x'≢x ∷ []
         help {e ∷ es} (x'≢e ∷ x'≢es) = x'≢e ∷ help x'≢es
 
-All-≢-map : ∀ {c d} {C : Set c} {D : Set d} (x : C) {xs : List C} (f : C → D) →
-            Injective (_≡_ {_} {C}) (_≡_ {_} {D}) f →
-            All (λ x' → ¬ x ≡ x') xs → All (λ y' → ¬ (f x) ≡ y') (mapˡ f xs)
-All-≢-map x f f-Injecitve [] = []
-All-≢-map x {x' ∷ xs'} f f-Injecitve (x≢x' ∷ x≢xs') = (λ fx≡fx' → x≢x' (f-Injecitve fx≡fx')) ∷ All-≢-map x f f-Injecitve x≢xs'
-
-Unique-map : ∀ {c d} {C : Set c} {D : Set d} {l : List C} (f : C → D) →
-             Injective (_≡_ {_} {C}) (_≡_ {_} {D}) f →
-             Unique l → Unique (mapˡ f l)
-Unique-map {l = []} _ _ _ = empty
-Unique-map {l = x ∷ xs} f f-Injecitve (push x≢xs uxs) = push (All-≢-map x f f-Injecitve x≢xs) (Unique-map f f-Injecitve uxs)
-
 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