Delete unused homomorphism proof that was broken by an Agda update.

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

Analysis/Sign.agda

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

@@ -1,149 +0,0 @@
-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,10 +1,93 @@
 module Language where
 
-open import Data.String using (String)
-open import Data.Nat using (ℕ)
+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)
 
 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,8 +19,10 @@ 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
+        FiniteHeightType = FVM.FiniteMap ks
+
+        finiteHeightLattice = FVM.IterProdIsomorphism.finiteHeightLattice uks ≈₂-dec height₂ fixedHeight₂
+        open FiniteHeightLattice finiteHeightLattice public
 
         ≈-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,8 +10,9 @@ 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)
+    using (Map; ⊔-equal-keys; ⊓-equal-keys; ∈k-dec; m₁≼m₂⇒m₁[k]≼m₂[k])
     renaming
         ( _≈_ to _≈ᵐ_
         ; _⊔_ to _⊔ᵐ_
@@ -28,9 +29,21 @@ 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)
@@ -56,6 +69,18 @@ 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 =
@@ -97,6 +122,8 @@ module _ (ks : List A) where
         ; absorb-⊓-⊔ = λ (m₁ , _) (m₂ , _) → absorb-⊓ᵐ-⊔ᵐ m₁ m₂
         }
 
+    open IsLattice isLattice using (_≼_) public
+
     lattice : Lattice FiniteMap
     lattice = record
         { _≈_ = _≈_
@@ -104,3 +131,46 @@ 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; empty; Unique-append; All¬-¬Any; All-x∈xs)
+open import Utils using (Unique; push; Unique-append; All¬-¬Any; All-x∈xs)
 
 open IsLattice lB using () renaming
     ( ≈-refl to ≈₂-refl; ≈-sym to ≈₂-sym; ≈-trans to ≈₂-trans
@@ -34,6 +34,21 @@ 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
@@ -65,19 +80,6 @@ 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')
@@ -340,7 +342,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₁} {[]} _ = empty
+    restrict-preserves-Unique {l₁} {[]} _ = Utils.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)
@@ -476,6 +478,9 @@ 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
 
@@ -488,8 +493,9 @@ _∈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
 
--- 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` 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.
 forget : ∀ {k : A} {v : B} {l : List (A × B)} → (k , v) ∈ˡ l → k ∈ˡ (ImplKeys.keys l)
 forget = ∈-cong proj₁
 
@@ -529,9 +535,12 @@ 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; union-equal-keys; insert-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)
 
+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₂)
 
@@ -878,6 +887,8 @@ isLattice = record
     ; absorb-⊓-⊔ = absorb-⊓-⊔
     }
 
+open IsLattice isLattice using (_≼_) public
+
 lattice : Lattice Map
 lattice = record
     { _≈_ = _≈_
@@ -958,6 +969,10 @@ _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
@@ -995,7 +1010,6 @@ 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)
@@ -1072,3 +1086,29 @@ 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,15 +5,25 @@ open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
 
 module Lattice.MapSet {a : Level} (A : Set a) (≡-dec-A : Decidable (_≡_ {a} {A})) where
 
-open import Lattice.Unit using (⊤) renaming (_≈_ to _≈₂_; _⊔_ to _⊔₂_; _⊓_ to _⊓₂_; isLattice to ⊤-isLattice)
+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)
 import Lattice.Map
 
 private module UnitMap = Lattice.Map A ⊤ _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A ⊤-isLattice
 open UnitMap using (Map)
 open UnitMap using
-    ( _⊆_; _≈_; ≈-equiv; _⊔_; _⊓_
+    ( _⊆_; _≈_; ≈-equiv; _⊔_; _⊓_; empty
     ; 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 _≟ˢ_ renaming (finiteHeightLattice to finiteHeightLatticeᵐ; FiniteHeightType to FiniteHeightTypeᵐ; ≈-dec to ≈-dec)
+open import Lattice.Bundles.FiniteValueMap String AB.AboveBelow _≟ˢ_ using () 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 : ∀ {ks : List String} → FiniteHeightMap ks → String
+showMap : FiniteHeightMap → 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 xyzw
+dumb : FiniteHeightMap
 dumb = ((("x" , AB.[_] tt) ∷ ("y" , AB.⊥) ∷ ("z" , AB.⊥) ∷ ("w" , AB.⊥) ∷ [] , xyzw-Unique) , refl)
 
-dumbFunction : FiniteHeightMap xyzw → FiniteHeightMap xyzw
+dumbFunction : FiniteHeightMap → FiniteHeightMap
 dumbFunction = _⊔_ dumb
 
 dumbFunction-Monotonic : Monotonic _≼_ _≼_ dumbFunction
 dumbFunction-Monotonic {m₁} {m₂} m₁≼m₂ = ⊔-Monotonicˡ dumb {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₂)
+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₂)
 
 main = run {0ℓ} (putStrLn (showMap aᶠ))

Utils.agda

@@ -2,10 +2,11 @@ module Utils where
 
 open import Agda.Primitive using () renaming (_⊔_ to _⊔ℓ_)
 open import Data.Nat using (ℕ; suc)
-open import Data.List using (List; []; _∷_; _++_)
+open import Data.List using (List; []; _∷_; _++_) renaming (map to mapˡ)
 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 (¬_)
 
@@ -29,6 +30,18 @@ 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