Prove multi-key access monotonicity in finite maps

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

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₁))