Finish the last proof obligation for trace walking

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

Analysis/Forward.agda

@@ -82,7 +82,7 @@ module WithProg (prog : Program) where
     -- Finally, the map we care about is (state -> (variables -> value)). Bring that in.
     module StateVariablesFiniteMap = Lattice.FiniteValueMap.WithKeys _≟_ isLatticeᵛ states
     open StateVariablesFiniteMap
-        using (_[_]; []-∈; m₁≼m₂⇒m₁[ks]≼m₂[ks])
+        using (_[_]; []-∈; m₁≼m₂⇒m₁[ks]≼m₂[ks]; m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂)
         renaming
             ( FiniteMap to StateVariables
             ; isLattice to isLatticeᵐ
@@ -124,7 +124,9 @@ module WithProg (prog : Program) where
     variablesAt-∈ s sv = proj₂ (locateᵐ {s} {sv} (states-in-Map s sv))
 
     variablesAt-≈ : ∀ s sv₁ sv₂ → sv₁ ≈ᵐ sv₂ → variablesAt s sv₁ ≈ᵛ variablesAt s sv₂
-    variablesAt-≈ = {!!}
+    variablesAt-≈ s sv₁ sv₂ sv₁≈sv₂ =
+        m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ sv₁ sv₂ sv₁≈sv₂
+                               (states-in-Map s sv₁) (states-in-Map s sv₂)
 
     -- build up the 'join' function, which follows from Exercise 4.26's
     --

Lattice/FiniteMap.agda

@@ -32,6 +32,7 @@ open import Lattice.Map ≡-dec-A lB as Map
         ; _[_] to _[_]ᵐ
         ; []-∈ to []ᵐ-∈
         ; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ
+        ; m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ to m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ᵐ
         ; locate to locateᵐ
         ; keys to keysᵐ
         ; _updating_via_ to _updatingᵐ_via_
@@ -164,6 +165,11 @@ module WithKeys (ks : List A) where
                         fm₁ ≼ fm₂ → (k , v₁) ∈ fm₁ → (k , v₂) ∈ fm₂ → v₁ ≼₂ v₂
     m₁≼m₂⇒m₁[k]≼m₂[k] (m₁ , _) (m₂ , _) m₁≼m₂ k,v₁∈m₁ k,v₂∈m₂ = m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ m₁ m₂ m₁≼m₂ k,v₁∈m₁ k,v₂∈m₂
 
+    m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ : ∀ (fm₁ fm₂ : FiniteMap) {k : A} →
+                             fm₁ ≈ fm₂ → ∀ (k∈kfm₁ : k ∈k fm₁) (k∈kfm₂ : k ∈k fm₂) →
+                             proj₁ (locate {fm = fm₁} k∈kfm₁) ≈₂ proj₁ (locate {fm = fm₂} k∈kfm₂)
+    m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ (m₁ , _) (m₂ , _) = m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ᵐ m₁ m₂
+
     module GeneralizedUpdate
              {l} {L : Set l}
              {_≈ˡ_ : L → L → Set l} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L}

Lattice/Map.agda

@@ -1142,3 +1142,12 @@ m₁≼m₂⇒k∈km₁⇒k∈km₂ m₁ m₂ m₁≼m₂ k∈km₁ =
         (v' , (v≈v' , k,v'∈m₂)) = (proj₁ m₁≼m₂) _ _ k,v∈m₁m₂
     in
         forget k,v'∈m₂
+
+m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ : ∀ (m₁ m₂ : Map) {k : A} →
+                         m₁ ≈ m₂ → ∀ (k∈km₁ : k ∈k m₁) (k∈km₂ : k ∈k m₂) →
+                         proj₁ (locate {m = m₁} k∈km₁) ≈₂ proj₁ (locate {m = m₂} k∈km₂)
+m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ m₁ m₂ {k} (m₁⊆m₂ , m₂⊆m₁) k∈km₁ k∈km₂
+    with (v₁ , k,v₁∈m₁) ← locate {m = m₁} k∈km₁
+    with (v₂ , k,v₂∈m₂) ← locate {m = m₂} k∈km₂
+    with (v₂' , (v₁≈v₂' , k,v₂'∈m₂)) ← m₁⊆m₂ k v₁ k,v₁∈m₁
+    rewrite Map-functional {m = m₂} k,v₂∈m₂ k,v₂'∈m₂ = v₁≈v₂'