Add a lattice instance for Map

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

Lattice.agda

@@ -42,7 +42,7 @@ record IsLattice {a} (A : Set a)
         absorb-⊓-⊔ : (x y : A) → (x ⊓ (x ⊔ y)) ≈ x
 
     open IsSemilattice joinSemilattice public
-    open IsSemilattice meetSemilattice public renaming
+    open IsSemilattice meetSemilattice public hiding (≈-equiv; ≈-refl; ≈-sym; ≈-trans) renaming
         ( ⊔-assoc to ⊓-assoc
         ; ⊔-comm to ⊓-comm
         ; ⊔-idemp to ⊓-idemp
@@ -350,3 +350,41 @@ module IsLatticeInstances where
             ; absorb-⊔-⊓ = absorb-⊔-⊓
             ; absorb-⊓-⊔ = absorb-⊓-⊔
             }
+
+    module ForMap {a} {A B : Set a}
+        (≡-dec-A : Decidable (_≡_ {a} {A}))
+        (_≈₂_ : B → B → Set a)
+        (_⊔₂_ : B → B → B)
+        (_⊓₂_ : B → B → B)
+        (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
+
+        open import Map A B ≡-dec-A
+        open IsLattice lB renaming
+            ( ≈-refl to ≈₂-refl; ≈-sym to ≈₂-sym
+            ; ⊔-idemp to ⊔₂-idemp; ⊓-idemp to ⊓₂-idemp
+            ; absorb-⊔-⊓ to absorb-⊔₂-⊓₂; absorb-⊓-⊔ to absorb-⊓₂-⊔₂
+            )
+
+        private
+            module MapJoin = IsSemilatticeInstances.ForMap ≡-dec-A _≈₂_ _⊔₂_ (IsLattice.joinSemilattice lB)
+            module MapMeet = IsSemilatticeInstances.ForMap ≡-dec-A _≈₂_ _⊓₂_ (IsLattice.meetSemilattice lB)
+
+            infix 4 _≈_
+            infixl 20 _⊔_
+
+            _≈_ : Map → Map → Set a
+            _≈_ = lift (_≈₂_)
+
+            _⊔_ : Map → Map → Map
+            m₁ ⊔ m₂ = union _⊔₂_ m₁ m₂
+
+            _⊓_ : Map → Map → Map
+            m₁ ⊓ m₂ = intersect _⊓₂_ m₁ m₂
+
+        MapIsLattice : IsLattice Map _≈_ _⊔_ _⊓_
+        MapIsLattice = record
+            { joinSemilattice = MapJoin.MapIsUnionSemilattice
+            ; meetSemilattice = MapMeet.MapIsIntersectSemilattice
+            ; absorb-⊔-⊓ = union-intersect-absorb _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ _⊓₂_ ⊔₂-idemp ⊓₂-idemp absorb-⊔₂-⊓₂ absorb-⊓₂-⊔₂
+            ; absorb-⊓-⊔ = intersect-union-absorb _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ _⊓₂_ ⊔₂-idemp ⊓₂-idemp absorb-⊔₂-⊓₂ absorb-⊓₂-⊔₂
+            }

Map.agda

@@ -682,8 +682,8 @@ module _ (_≈_ : B → B → Set b) where
              (_⊔₂_ : B → B → B) (_⊓₂_ : B → B → B)
              (⊔₂-idemp :  ∀ (b : B) → (b ⊔₂ b) ≈ b)
              (⊓₂-idemp :  ∀ (b : B) → (b ⊓₂ b) ≈ b)
-             (⊔₂-⊓₂-absorb : ∀ {b₁ b₂ : B} → (b₁ ⊔₂ (b₁ ⊓₂ b₂)) ≈ b₁)
+             (⊔₂-⊓₂-absorb : ∀ (b₁ b₂ : B) → (b₁ ⊔₂ (b₁ ⊓₂ b₂)) ≈ b₁)
-             (⊓₂-⊔₂-absorb : ∀ {b₁ b₂ : B} → (b₁ ⊓₂ (b₁ ⊔₂ b₂)) ≈ b₁)
+             (⊓₂-⊔₂-absorb : ∀ (b₁ b₂ : B) → (b₁ ⊓₂ (b₁ ⊔₂ b₂)) ≈ b₁)
              where
         private module I⊔ = ImplInsert _⊔₂_
         private module I⊓ = ImplInsert _⊓₂_
@@ -703,7 +703,7 @@ module _ (_≈_ : B → B → Set b) where
                                            (single {v₂} v₂∈m₂)) , v₁v₁'v₂∈m₁m₁₂))
                         rewrite Map-functional {m = m₁} k,v₁∈m₁ k,v₁'∈m₁
                         rewrite Map-functional {m = m₁ ⊓ (m₁ ⊔ m₂)} k,v∈m₁m₁₂ v₁v₁'v₂∈m₁m₁₂ =
-                        (v₁' , (⊓₂-⊔₂-absorb , k,v₁'∈m₁))
+                        (v₁' , (⊓₂-⊔₂-absorb v₁' v₂ , k,v₁'∈m₁))
                 ...   | (_ , (bothⁱ (single {v₁} k,v₁∈m₁)
                                     (in₁ (single {v₁'} k,v₁'∈m₁) _) , v₁v₁'∈m₁m₁₂))
                         rewrite Map-functional {m = m₁} k,v₁∈m₁ k,v₁'∈m₁
@@ -717,7 +717,7 @@ module _ (_≈_ : B → B → Set b) where
                     with ∈k-dec k l₂
                 ...   | yes k∈km₂ =
                         let (v₂ , k,v₂∈m₂) = locate k∈km₂
-                        in (v ⊓₂ (v ⊔₂ v₂) , (≈-sym ⊓₂-⊔₂-absorb , I⊓.intersect-combines u₁ (I⊔.union-preserves-Unique l₁ l₂ u₂) k,v∈m₁ (I⊔.union-combines u₁ u₂ k,v∈m₁ k,v₂∈m₂)))
+                        in (v ⊓₂ (v ⊔₂ v₂) , (≈-sym (⊓₂-⊔₂-absorb v v₂) , I⊓.intersect-combines u₁ (I⊔.union-preserves-Unique l₁ l₂ u₂) k,v∈m₁ (I⊔.union-combines u₁ u₂ k,v∈m₁ k,v₂∈m₂)))
                 ...   | no k∉km₂ = (v ⊓₂ v , (≈-sym (⊓₂-idemp v) , I⊓.intersect-combines u₁ (I⊔.union-preserves-Unique l₁ l₂ u₂) k,v∈m₁ (I⊔.union-preserves-∈₁ u₁ k,v∈m₁ k∉km₂)))
 
         union-intersect-absorb : ∀ (m₁ m₂ : Map) →  lift (m₁ ⊔ (m₁ ⊓ m₂)) m₁
@@ -731,7 +731,7 @@ module _ (_≈_ : B → B → Set b) where
                                            (single {v₂} k,v₂∈m₂)) , v₁v₁'v₂∈m₁m₁₂))
                         rewrite Map-functional {m = m₁} k,v₁∈m₁ k,v₁'∈m₁
                         rewrite Map-functional {m = m₁ ⊔ (m₁ ⊓ m₂)} k,v∈m₁m₁₂ v₁v₁'v₂∈m₁m₁₂ =
-                        (v₁' , (⊔₂-⊓₂-absorb , k,v₁'∈m₁))
+                        (v₁' , (⊔₂-⊓₂-absorb v₁' v₂ , k,v₁'∈m₁))
                 ...   | (_ , (in₁ (single {v₁} k,v₁∈m₁) k∉km₁₂ , k,v₁∈m₁m₁₂))
                         rewrite Map-functional {m = m₁ ⊔ (m₁ ⊓ m₂)} k,v∈m₁m₁₂ k,v₁∈m₁m₁₂ =
                         (v₁ , (≈-refl , k,v₁∈m₁))
@@ -744,5 +744,5 @@ module _ (_≈_ : B → B → Set b) where
                     with ∈k-dec k l₂
                 ...   | yes k∈km₂ =
                         let (v₂ , k,v₂∈m₂) = locate k∈km₂
-                        in (v ⊔₂ (v ⊓₂ v₂) , (≈-sym ⊔₂-⊓₂-absorb , I⊔.union-combines u₁ (I⊓.intersect-preserves-Unique {l₁} {l₂} u₂) k,v∈m₁ (I⊓.intersect-combines u₁ u₂ k,v∈m₁ k,v₂∈m₂)))
+                        in (v ⊔₂ (v ⊓₂ v₂) , (≈-sym (⊔₂-⊓₂-absorb v v₂) , I⊔.union-combines u₁ (I⊓.intersect-preserves-Unique {l₁} {l₂} u₂) k,v∈m₁ (I⊓.intersect-combines u₁ u₂ k,v∈m₁ k,v₂∈m₂)))
                 ...   | no k∉km₂ = (v , (≈-refl , I⊔.union-preserves-∈₁ u₁ k,v∈m₁ (I⊓.intersect-preserves-∉₂ {k} {l₁} {l₂} k∉km₂)))