From ec31333e9a853ee65e44860da1221d109d4cc773 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sun, 11 Feb 2024 13:19:46 -0800
Subject: [PATCH] Add a 'Finite Map' lattice

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Lattice/FiniteMap.agda | 78 ++++++++++++++++++++++++++++++++++++++++++
 Lattice/Map.agda       | 14 +++++---
 2 files changed, 88 insertions(+), 4 deletions(-)
 create mode 100644 Lattice/FiniteMap.agda

diff --git a/Lattice/FiniteMap.agda b/Lattice/FiniteMap.agda
new file mode 100644
index 0000000..c2342a9
--- /dev/null
+++ b/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₂
+        }
diff --git a/Lattice/Map.agda b/Lattice/Map.agda
index fa6935e..980fe4e 100644
--- a/Lattice/Map.agda
+++ b/Lattice/Map.agda
@@ -141,9 +141,9 @@ private module ImplInsert (f : B → B → B) where
         rewrite union-subset-keys kl₁'⊆kl₂ =
         insert-keys-∈ k∈kl₂
 
-    union-equal-keys : ∀ (l₁ l₂ : List (A × B)) →
+    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₂
+    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₂)
 
@@ -512,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₂)
@@ -881,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₂