From 3f5551d70c4078d2c38184ccca24cb35d73d8063 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Wed, 8 May 2024 22:34:02 -0700
Subject: [PATCH] Add a lemma about the effect of joinAll

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Analysis/Forward.agda | 24 ++++++++++++++++++------
 1 file changed, 18 insertions(+), 6 deletions(-)

diff --git a/Analysis/Forward.agda b/Analysis/Forward.agda
index be5e944..45c51e2 100644
--- a/Analysis/Forward.agda
+++ b/Analysis/Forward.agda
@@ -95,6 +95,17 @@ module WithProg (prog : Program) where
     ≈ᵐ-dec = ≈ᵛ-dec⇒≈ᵐ-dec ≈ᵛ-dec
     fixedHeightᵐ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵐ
 
+    -- We now have our (state -> (variables -> value)) map.
+    -- Define a couple of helpers to retrieve values from it. Specifically,
+    -- since the State type is as specific as possible, it's always possible to
+    -- retrieve the variable values at each state.
+
+    states-in-Map : ∀ (s : State) (sv : StateVariables) → s ∈kᵐ sv
+    states-in-Map s sv@(m , ksv≡states) rewrite ksv≡states = states-complete s
+
+    variablesAt : State → StateVariables → VariableValues
+    variablesAt s sv = proj₁ (locateᵐ {s} {sv} (states-in-Map s sv))
+
     -- build up the 'join' function, which follows from Exercise 4.26's
     --
     --    L₁ → (A → L₂)
@@ -118,8 +129,15 @@ module WithProg (prog : Program) where
         renaming
             ( f' to joinAll
             ; f'-Monotonic to joinAll-Mono
+            ; f'-k∈ks-≡ to joinAll-k∈ks-≡
             )
 
+    variablesAt-joinAll : ∀ (s : State) (sv : StateVariables) →
+                          variablesAt s (joinAll sv) ≡ joinForKey s sv
+    variablesAt-joinAll s sv
+        with (vs , s,vs∈usv) ← locateᵐ {s} {joinAll sv} (states-in-Map s (joinAll sv)) =
+        joinAll-k∈ks-≡ {l = sv} (states-complete s) s,vs∈usv
+
     -- With 'join' in hand, we need to perform abstract evaluation.
     module WithEvaluator (eval : Expr → VariableValues → L)
                          (eval-Mono : ∀ (e : Expr) → Monotonic _≼ᵛ_ _≼ˡ_ (eval e)) where
@@ -138,9 +156,6 @@ module WithProg (prog : Program) where
                     )
                 public
 
-        states-in-Map : ∀ (s : State) (sv : StateVariables) → s ∈kᵐ sv
-        states-in-Map s sv@(m , ksv≡states) rewrite ksv≡states = states-complete s
-
         -- The per-state update function makes use of the single-key setter,
         -- updateVariablesFromExpression, for the case where the statement
         -- is an assignment.
@@ -157,9 +172,6 @@ module WithProg (prog : Program) where
         updateVariablesFromStmt-Monoʳ (k ← e) {vs₁} {vs₂} vs₁≼vs₂ = updateVariablesFromExpression-Mono k e {vs₁} {vs₂} vs₁≼vs₂
         updateVariablesFromStmt-Monoʳ noop vs₁≼vs₂ = vs₁≼vs₂
 
-        variablesAt : State → StateVariables → VariableValues
-        variablesAt s sv = proj₁ (locateᵐ {s} {sv} (states-in-Map s sv))
-
         updateVariablesForState : State → StateVariables → VariableValues
         updateVariablesForState s sv =
             foldl (flip updateVariablesFromStmt) (variablesAt s sv) (code s)