Prove monotonicity of eval

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

Analysis/Sign.agda

@@ -56,6 +56,11 @@ open AB.Plain 0ˢ using ()
         ; _⊔_ to _⊔ᵍ_
         )
 
+open IsLattice isLatticeᵍ using ()
+    renaming
+        ( ≼-trans to ≼ᵍ-trans
+        )
+
 plus : SignLattice → SignLattice → SignLattice
 plus ⊥ᵍ _ = ⊥ᵍ
 plus _ ⊥ᵍ = ⊥ᵍ
@@ -99,7 +104,7 @@ 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 Lattice.FiniteValueMap.WithKeys _≟ˢ_ isLatticeᵍ vars
-        using ()
+        using (m₁≼m₂⇒m₁[k]≼m₂[k])
         renaming
             ( FiniteMap to VariableSigns
             ; isLattice to isLatticeᵛ
@@ -193,6 +198,43 @@ module _ (prog : Program) where
     eval (# 0) _ _ = [ 0ˢ ]ᵍ
     eval (# (suc n')) _ _ = [ + ]ᵍ
 
+    eval-Mono : ∀ (e : Expr) (k∈e⇒k∈vars : ∀ k → k ∈ᵉ e → k ∈ˡ vars) → Monotonic _≼ᵛ_ _≼ᵍ_ (eval e k∈e⇒k∈vars)
+    eval-Mono (e₁ + e₂) k∈e⇒k∈vars {vs₁} {vs₂} vs₁≼vs₂ =
+        let
+            k∈e₁⇒k∈vars = λ k k∈e₁ → k∈e⇒k∈vars k (in⁺₁ k∈e₁)
+            k∈e₂⇒k∈vars = λ k k∈e₂ → k∈e⇒k∈vars k (in⁺₂ k∈e₂)
+            g₁vs₁ = eval e₁ k∈e₁⇒k∈vars vs₁
+            g₂vs₁ = eval e₂ k∈e₂⇒k∈vars vs₁
+            g₁vs₂ = eval e₁ k∈e₁⇒k∈vars vs₂
+            g₂vs₂ = eval e₂ k∈e₂⇒k∈vars vs₂
+        in
+            ≼ᵍ-trans
+                {plus g₁vs₁ g₂vs₁} {plus g₁vs₂ g₂vs₁} {plus g₁vs₂ g₂vs₂}
+                (plus-Monoˡ g₂vs₁ {g₁vs₁} {g₁vs₂} (eval-Mono e₁ k∈e₁⇒k∈vars {vs₁} {vs₂} vs₁≼vs₂))
+                (plus-Monoʳ g₁vs₂ {g₂vs₁} {g₂vs₂} (eval-Mono e₂ k∈e₂⇒k∈vars {vs₁} {vs₂} vs₁≼vs₂))
+    eval-Mono (e₁ - e₂) k∈e⇒k∈vars {vs₁} {vs₂} vs₁≼vs₂ =
+        let
+            k∈e₁⇒k∈vars = λ k k∈e₁ → k∈e⇒k∈vars k (in⁻₁ k∈e₁)
+            k∈e₂⇒k∈vars = λ k k∈e₂ → k∈e⇒k∈vars k (in⁻₂ k∈e₂)
+            g₁vs₁ = eval e₁ k∈e₁⇒k∈vars vs₁
+            g₂vs₁ = eval e₂ k∈e₂⇒k∈vars vs₁
+            g₁vs₂ = eval e₁ k∈e₁⇒k∈vars vs₂
+            g₂vs₂ = eval e₂ k∈e₂⇒k∈vars vs₂
+        in
+            ≼ᵍ-trans
+                {minus g₁vs₁ g₂vs₁} {minus g₁vs₂ g₂vs₁} {minus g₁vs₂ g₂vs₂}
+                (minus-Monoˡ g₂vs₁ {g₁vs₁} {g₁vs₂} (eval-Mono e₁ k∈e₁⇒k∈vars {vs₁} {vs₂} vs₁≼vs₂))
+                (minus-Monoʳ g₁vs₂ {g₂vs₁} {g₂vs₂} (eval-Mono e₂ k∈e₂⇒k∈vars {vs₁} {vs₂} vs₁≼vs₂))
+    eval-Mono (` k) k∈e⇒k∈vars {vs₁} {vs₂} vs₁≼vs₂ =
+        let
+            (v₁ , k,v₁∈vs₁) = locateᵛ {k} {vs₁} (vars-in-Map k vs₁ (k∈e⇒k∈vars k here))
+            (v₂ , k,v₂∈vs₂) = locateᵛ {k} {vs₂} (vars-in-Map k vs₂ (k∈e⇒k∈vars k here))
+        in
+            m₁≼m₂⇒m₁[k]≼m₂[k] vs₁ vs₂ vs₁≼vs₂ k,v₁∈vs₁ k,v₂∈vs₂
+    eval-Mono (# 0) _ _ = ≈ᵍ-refl
+    eval-Mono (# (suc n')) _ _ = ≈ᵍ-refl
+
+
     updateForState : State → StateVariables → VariableSigns
     updateForState s sv
         with code s in p

Lattice/FiniteMap.agda

@@ -12,7 +12,7 @@ module Lattice.FiniteMap {a b : Level} {A : Set a} {B : Set b}
 
 open IsLattice lB using () renaming (_≼_ to _≼₂_)
 open import Lattice.Map ≡-dec-A lB as Map
-    using (Map; ⊔-equal-keys; ⊓-equal-keys; ∈k-dec; m₁≼m₂⇒m₁[k]≼m₂[k])
+    using (Map; ⊔-equal-keys; ⊓-equal-keys; ∈k-dec)
     renaming
         ( _≈_ to _≈ᵐ_
         ; _⊔_ to _⊔ᵐ_
@@ -30,6 +30,7 @@ open import Lattice.Map ≡-dec-A lB as Map
         ; absorb-⊓-⊔ to absorb-⊓ᵐ-⊔ᵐ
         ; ≈-dec to ≈ᵐ-dec
         ; _[_] to _[_]ᵐ
+        ; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ
         ; locate to locateᵐ
         ; keys to keysᵐ
         ; _updating_via_ to _updatingᵐ_via_
@@ -138,6 +139,10 @@ module WithKeys (ks : List A) where
         ; isLattice = isLattice
         }
 
+    m₁≼m₂⇒m₁[k]≼m₂[k] : ∀ (fm₁ fm₂ : FiniteMap) {k : A} {v₁ v₂ : B} →
+                        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₂
+
     module GeneralizedUpdate
              {l} {L : Set l}
              {_≈ˡ_ : L → L → Set l} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L}
@@ -177,7 +182,7 @@ module WithKeys (ks : List A) where
                 (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₂
+                (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₁))