Prove that the 'join' transformation is monotonic

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

Analysis/Sign.agda

@@ -1,11 +1,14 @@
 module Analysis.Sign where
 
 open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
+open import Data.Product using (proj₁)
+open import Data.List using (foldr)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans)
 open import Relation.Nullary using (¬_; Dec; yes; no)
 
 open import Language
 open import Lattice
+open import Utils using (Pairwise)
 import Lattice.Bundles.FiniteValueMap
 
 private module FixedHeightFiniteMap = Lattice.Bundles.FiniteValueMap.FromFiniteHeightLattice
@@ -31,7 +34,9 @@ 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)
+    open import Lattice.AboveBelow Sign _≡_ (record { ≈-refl = refl; ≈-sym = sym; ≈-trans = trans }) _≟ᵍ_ as AB
+        using ()
+        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)
 
@@ -40,16 +45,61 @@ module _ (prog : Program) where
 
     -- The variable -> sign map is a finite value-map with keys strings. Use a bundle to avoid explicitly specifying operators.
     open FixedHeightFiniteMap String SignLattice _≟ˢ_ finiteHeightLatticeᵍ vars-Unique ≈ᵍ-dec
+        using ()
         renaming
             ( finiteHeightLattice to finiteHeightLatticeᵛ
             ; FiniteMap to VariableSigns
             ; _≈_ to _≈ᵛ_
+            ; _⊔_ to _⊔ᵛ_
             ; ≈-dec to ≈ᵛ-dec
             )
+    open FiniteHeightLattice finiteHeightLatticeᵛ
+        using ()
+        renaming
+            ( ⊔-Monotonicˡ to ⊔ᵛ-Monotonicˡ
+            ; ⊔-Monotonicʳ to ⊔ᵛ-Monotonicʳ
+            ; _≼_ to _≼ᵛ_
+            ; joinSemilattice to joinSemilatticeᵛ
+            ; ⊔-idemp to ⊔ᵛ-idemp
+            )
+
+    ⊥ᵛ = proj₁ (proj₁ (proj₁ (FiniteHeightLattice.fixedHeight finiteHeightLatticeᵛ)))
 
     -- Finally, the map we care about is (state -> (variables -> sign)). Bring that in.
-    open FixedHeightFiniteMap State VariableSigns _≟_ finiteHeightLatticeᵛ states-Unique ≈ᵛ-dec
+    module StateVariablesFiniteMap = FixedHeightFiniteMap State VariableSigns _≟_ finiteHeightLatticeᵛ states-Unique ≈ᵛ-dec
+    open StateVariablesFiniteMap
+        using (_[_]; m₁≼m₂⇒m₁[ks]≼m₂[ks])
         renaming
             ( finiteHeightLattice to finiteHeightLatticeᵐ
             ; FiniteMap to StateVariables
+            ; isLattice to isLatticeᵐ
+            )
+    open FiniteHeightLattice finiteHeightLatticeᵐ
+        using ()
+        renaming (_≼_ to _≼ᵐ_)
+
+    -- build up the 'join' function, which follows from Exercise 4.26's
+    --
+    --    L₁ → (A → L₂)
+    --
+    -- Construction, with L₁ = (A → L₂), and f = id
+
+    joinForKey : State → StateVariables → VariableSigns
+    joinForKey k states = foldr _⊔ᵛ_ ⊥ᵛ (states [ incoming k ])
+
+    -- The per-key join is made up of map key accesses (which are monotonic)
+    -- and folds using the join operation (also monotonic)
+
+    joinForKey-Mono : ∀ (k : State) → Monotonic _≼ᵐ_ _≼ᵛ_ (joinForKey k)
+    joinForKey-Mono k {fm₁} {fm₂} fm₁≼fm₂ =
+        foldr-Mono joinSemilatticeᵛ joinSemilatticeᵛ (fm₁ [ incoming k ]) (fm₂ [ incoming k ]) _⊔ᵛ_ ⊥ᵛ ⊥ᵛ
+                   (m₁≼m₂⇒m₁[ks]≼m₂[ks] fm₁ fm₂ (incoming k) fm₁≼fm₂)
+                   (⊔ᵛ-idemp ⊥ᵛ) ⊔ᵛ-Monotonicʳ ⊔ᵛ-Monotonicˡ
+
+    -- The name f' comes from the formulation of Exercise 4.26.
+
+    open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) joinForKey joinForKey-Mono states
+        renaming
+            ( f' to joinAll
+            ; f'-Monotonic to joinAll-Mono
             )

Language.agda

@@ -91,3 +91,15 @@ record Program : Set where
 
     _≟_ : IsDecidable (_≡_ {_} {State})
     _≟_ = _≟ᶠ_
+
+    -- Computations for incoming and outgoing edged  will have to change too
+    -- when we support branching etc.
+
+    incoming : State → List State
+    incoming
+        with length
+    ...   | 0 = (λ ())
+    ...   | suc n' = (λ
+            { zero → []
+            ; (suc f') → (inject₁ f') ∷ []
+            })

Lattice.agda

@@ -124,7 +124,7 @@ module _ {a} {A : Set a}
     open IsSemilattice lA using (_≼_)
 
     id-Mono : Monotonic _≼_ _≼_ (λ x → x)
-    id-Mono a₁≼a₂ = a₁≼a₂
+    id-Mono {a₁} {a₂} a₁≼a₂ = a₁≼a₂
 
 module _ {a b} {A : Set a} {B : Set b}
          {_≈₁_ : A → A → Set a} {_⊔₁_ : A → A → A}

Lattice/FiniteMap.agda

@@ -132,23 +132,24 @@ module WithKeys (ks : List A) where
         ; isLattice = isLattice
         }
 
-    module _ {l} {L : Set l}
+    module GeneralizedUpdate
+             {l} {L : Set l}
              {_≈ˡ_ : L → L → Set l} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L}
-             (lL : IsLattice L _≈ˡ_ _⊔ˡ_ _⊓ˡ_) where
+             (lL : IsLattice L _≈ˡ_ _⊔ˡ_ _⊓ˡ_)
+             (f : L → FiniteMap) (f-Monotonic : Monotonic (IsLattice._≼_ lL) _≼_ f)
+             (g : A → L → B) (g-Monotonicʳ : ∀ k → Monotonic (IsLattice._≼_ lL) _≼₂_ (g k))
+             (ks : List A) where
+
         open IsLattice lL using () renaming (_≼_ to _≼ˡ_)
 
-        module _ (f : L → FiniteMap) (f-Monotonic : Monotonic _≼ˡ_ _≼_ f)
+        updater : L → A → B
-                 (g : A → L → B) (g-Monotonicʳ : ∀ k → Monotonic _≼ˡ_ _≼₂_ (g k))
+        updater l k = g k l
-                 (ks : List A) where
 
-            updater : L → A → B
+        f' : L → FiniteMap
-            updater l k = g k l
+        f' l = (f l) updating ks via (updater l)
 
-            f' : L → FiniteMap
+        f'-Monotonic : Monotonic _≼ˡ_ _≼_ f'
-            f' l = (f l) updating ks via (updater l)
+        f'-Monotonic {l₁} {l₂} l₁≼l₂ = f'-Monotonicᵐ lL (proj₁ ∘ f) f-Monotonic g g-Monotonicʳ ks l₁≼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)