Prove that the var->lattice maps respect equality

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

Analysis/Forward.agda

@@ -19,7 +19,7 @@ open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Data.Unit using (⊤)
 open import Function using (_∘_; flip)
 
-open import Utils using (Pairwise)
+open import Utils using (Pairwise; _⇒_)
 import Lattice.FiniteValueMap
 
 open IsFiniteHeightLattice isFiniteHeightLatticeˡ
@@ -28,6 +28,7 @@ open IsFiniteHeightLattice isFiniteHeightLatticeˡ
         ( isLattice to isLatticeˡ
         ; fixedHeight to fixedHeightˡ
         ; _≼_ to _≼ˡ_
+        ; ≈-sym to ≈ˡ-sym
         )
 
 module WithProg (prog : Program) where
@@ -210,7 +211,7 @@ module WithProg (prog : Program) where
         -- The fixed point of the 'analyze' function is our final goal.
         open import Fixedpoint ≈ᵐ-dec isFiniteHeightLatticeᵐ analyze (λ {m₁} {m₂} m₁≼m₂ → analyze-Mono {m₁} {m₂} m₁≼m₂)
             using ()
-            renaming (aᶠ to result)
+            renaming (aᶠ to result; aᶠ≈faᶠ to result≈analyze-result)
             public
 
         variablesAt-updateAll : ∀ (s : State) (sv : StateVariables) →
@@ -222,11 +223,21 @@ module WithProg (prog : Program) where
         module WithInterpretation (latticeInterpretationˡ : LatticeInterpretation isLatticeˡ) where
             open LatticeInterpretation latticeInterpretationˡ
                 using ()
-                renaming (⟦_⟧ to ⟦_⟧ˡ)
+                renaming (⟦_⟧ to ⟦_⟧ˡ; ⟦⟧-respects-≈ to ⟦⟧ˡ-respects-≈ˡ)
 
             ⟦_⟧ᵛ : VariableValues → Env → Set
             ⟦_⟧ᵛ vs ρ = ∀ {k l} → (k , l) ∈ᵛ vs → ∀ {v} → (k , v) Language.∈ ρ → ⟦ l ⟧ˡ v
 
+
+            ⟦⟧ᵛ-respects-≈ᵛ : ∀ {vs₁ vs₂ : VariableValues} → vs₁ ≈ᵛ vs₂ → ⟦ vs₁ ⟧ᵛ ⇒ ⟦ vs₂ ⟧ᵛ
+            ⟦⟧ᵛ-respects-≈ᵛ {m₁ , _} {m₂ , _}
+                            (m₁⊆m₂ , m₂⊆m₁) ρ ⟦vs₁⟧ρ {k} {l} k,l∈m₂ {v} k,v∈ρ =
+                let
+                    (l' , (l≈l' , k,l'∈m₁)) = m₂⊆m₁ _ _ k,l∈m₂
+                    ⟦l'⟧v = ⟦vs₁⟧ρ k,l'∈m₁ k,v∈ρ
+                in
+                    ⟦⟧ˡ-respects-≈ˡ (≈ˡ-sym l≈l') v ⟦l'⟧v
+
             InterpretationValid : Set
             InterpretationValid = ∀ {vs ρ e v} → ρ , e ⇒ᵉ v → ⟦ vs ⟧ᵛ ρ → ⟦ eval e vs ⟧ˡ v