Almost prove correctness

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

Analysis/Forward.agda

@@ -10,16 +10,18 @@ module Analysis.Forward
 open import Data.Empty using (⊥-elim)
 open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
 open import Data.Nat using (suc)
-open import Data.Product using (_×_; proj₁; _,_)
+open import Data.Product using (_×_; proj₁; proj₂; _,_)
+open import Data.Sum using (inj₁; inj₂)
 open import Data.List using (List; _∷_; []; foldr; foldl; cartesianProduct; cartesianProductWith)
 open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_)
 open import Data.List.Relation.Unary.Any as Any using ()
-open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; subst)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym; trans; subst)
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Data.Unit using (⊤)
 open import Function using (_∘_; flip)
+import Chain
 
-open import Utils using (Pairwise; _⇒_)
+open import Utils using (Pairwise; _⇒_; _∨_)
 import Lattice.FiniteValueMap
 
 open IsFiniteHeightLattice isFiniteHeightLatticeˡ
@@ -62,25 +64,32 @@ module WithProg (prog : Program) where
             ; ⊔-Monotonicʳ to ⊔ᵛ-Monotonicʳ
             ; ⊔-idemp to ⊔ᵛ-idemp
             )
+    open Lattice.FiniteValueMap.IterProdIsomorphism _≟ˢ_ isLatticeˡ
+        using ()
+        renaming
+            ( Provenance-union to Provenance-unionᵐ
+            )
     open Lattice.FiniteValueMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight _≟ˢ_ isLatticeˡ vars-Unique ≈ˡ-dec _ fixedHeightˡ
         using ()
         renaming
             ( isFiniteHeightLattice to isFiniteHeightLatticeᵛ
+            ; ⊥-contains-bottoms to ⊥ᵛ-contains-bottoms
             )
 
     ≈ᵛ-dec = ≈ˡ-dec⇒≈ᵛ-dec ≈ˡ-dec
     joinSemilatticeᵛ = IsFiniteHeightLattice.joinSemilattice isFiniteHeightLatticeᵛ
     fixedHeightᵛ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵛ
-    ⊥ᵛ = proj₁ (proj₁ (proj₁ fixedHeightᵛ))
+    ⊥ᵛ = Chain.Height.⊥ fixedHeightᵛ
 
     -- 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ᵐ
             ; _≈_ to _≈ᵐ_
+            ; _∈_ to _∈ᵐ_
             ; _∈k_ to _∈kᵐ_
             ; locate to locateᵐ
             ; _≼_ to _≼ᵐ_
@@ -113,8 +122,13 @@ module WithProg (prog : Program) where
     variablesAt : State → StateVariables → VariableValues
     variablesAt s sv = proj₁ (locateᵐ {s} {sv} (states-in-Map s sv))
 
+    variablesAt-∈ : ∀ (s : State) (sv : StateVariables) → (s , variablesAt s sv) ∈ᵐ sv
+    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
     --
@@ -232,11 +246,17 @@ module WithProg (prog : Program) where
         module WithInterpretation (latticeInterpretationˡ : LatticeInterpretation isLatticeˡ) where
             open LatticeInterpretation latticeInterpretationˡ
                 using ()
-                renaming (⟦_⟧ to ⟦_⟧ˡ; ⟦⟧-respects-≈ to ⟦⟧ˡ-respects-≈ˡ)
+                renaming
+                    ( ⟦_⟧ to ⟦_⟧ˡ
+                    ; ⟦⟧-respects-≈ to ⟦⟧ˡ-respects-≈ˡ
+                    ; ⟦⟧-⊔-∨ to ⟦⟧ˡ-⊔ˡ-∨
+                    )
 
             ⟦_⟧ᵛ : 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₂ , _}
@@ -247,9 +267,21 @@ module WithProg (prog : Program) where
                 in
                     ⟦⟧ˡ-respects-≈ˡ (≈ˡ-sym l≈l') v ⟦l'⟧v
 
+            ⟦⟧ᵛ-⊔ᵛ-∨ : ∀ {vs₁ vs₂ : VariableValues} → (⟦ vs₁ ⟧ᵛ ∨ ⟦ vs₂ ⟧ᵛ) ⇒ ⟦ vs₁ ⊔ᵛ vs₂ ⟧ᵛ
+            ⟦⟧ᵛ-⊔ᵛ-∨ {vs₁} {vs₂} ρ ⟦vs₁⟧ρ∨⟦vs₂⟧ρ {k} {l} k,l∈vs₁₂ {v} k,v∈ρ
+                with ((l₁ , l₂) , (refl , (k,l₁∈vs₁ , k,l₂∈vs₂)))
+                     ← Provenance-unionᵐ vs₁ vs₂ k,l∈vs₁₂
+                with ⟦vs₁⟧ρ∨⟦vs₂⟧ρ
+            ...   | inj₁ ⟦vs₁⟧ρ = ⟦⟧ˡ-⊔ˡ-∨ {l₁} {l₂} v (inj₁ (⟦vs₁⟧ρ k,l₁∈vs₁ k,v∈ρ))
+            ...   | inj₂ ⟦vs₂⟧ρ = ⟦⟧ˡ-⊔ˡ-∨ {l₁} {l₂} v (inj₂ (⟦vs₂⟧ρ k,l₂∈vs₂ k,v∈ρ))
+
             ⟦⟧ᵛ-foldr : ∀ {vs : VariableValues} {vss : List VariableValues} {ρ : Env} →
                         ⟦ vs ⟧ᵛ ρ → vs ∈ˡ vss → ⟦ foldr _⊔ᵛ_ ⊥ᵛ vss ⟧ᵛ ρ
-            ⟦⟧ᵛ-foldr = {!!}
+            ⟦⟧ᵛ-foldr {vs} {vs ∷ vss'} {ρ = ρ} ⟦vs⟧ρ (Any.here refl) =
+                ⟦⟧ᵛ-⊔ᵛ-∨ {vs₁ = vs} {vs₂ = foldr _⊔ᵛ_ ⊥ᵛ vss'} ρ (inj₁ ⟦vs⟧ρ)
+            ⟦⟧ᵛ-foldr {vs} {vs' ∷ vss'} {ρ = ρ} ⟦vs⟧ρ (Any.there vs∈vss') =
+                ⟦⟧ᵛ-⊔ᵛ-∨ {vs₁ = vs'} {vs₂ = foldr _⊔ᵛ_ ⊥ᵛ vss'} ρ
+                         (inj₂ (⟦⟧ᵛ-foldr ⟦vs⟧ρ vs∈vss'))
 
             InterpretationValid : Set
             InterpretationValid = ∀ {vs ρ e v} → ρ , e ⇒ᵉ v → ⟦ vs ⟧ᵛ ρ → ⟦ eval e vs ⟧ˡ v
@@ -275,13 +307,17 @@ module WithProg (prog : Program) where
                 updateVariablesFromStmt-fold-matches : ∀ {bss vs ρ₁ ρ₂} → ρ₁ , bss ⇒ᵇˢ ρ₂ → ⟦ vs ⟧ᵛ ρ₁ → ⟦ foldl (flip updateVariablesFromStmt) vs bss ⟧ᵛ ρ₂
                 updateVariablesFromStmt-fold-matches [] ⟦vs⟧ρ = ⟦vs⟧ρ
                 updateVariablesFromStmt-fold-matches {bs ∷ bss'} {vs} {ρ₁} {ρ₂} (ρ₁,bs⇒ρ ∷ ρ,bss'⇒ρ₂) ⟦vs⟧ρ₁ =
-                    updateVariablesFromStmt-fold-matches {bss'} {updateVariablesFromStmt bs vs} ρ,bss'⇒ρ₂ (updateVariablesFromStmt-matches ρ₁,bs⇒ρ ⟦vs⟧ρ₁)
+                    updateVariablesFromStmt-fold-matches
+                        {bss'} {updateVariablesFromStmt bs vs} ρ,bss'⇒ρ₂
+                        (updateVariablesFromStmt-matches ρ₁,bs⇒ρ ⟦vs⟧ρ₁)
 
                 updateVariablesForState-matches : ∀ {s sv ρ₁ ρ₂} → ρ₁ , (code s) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s sv ⟧ᵛ ρ₁ → ⟦ updateVariablesForState s sv ⟧ᵛ ρ₂
-                updateVariablesForState-matches = updateVariablesFromStmt-fold-matches
+                updateVariablesForState-matches =
+                    updateVariablesFromStmt-fold-matches
 
                 updateAll-matches : ∀ {s sv ρ₁ ρ₂} → ρ₁ , (code s) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s sv ⟧ᵛ ρ₁ → ⟦ variablesAt s (updateAll sv) ⟧ᵛ ρ₂
-                updateAll-matches {s} {sv} ρ₁,bss⇒ρ₂ ⟦vs⟧ρ₁ rewrite variablesAt-updateAll s sv =
+                updateAll-matches {s} {sv} ρ₁,bss⇒ρ₂ ⟦vs⟧ρ₁
+                    rewrite variablesAt-updateAll s sv =
                     updateVariablesForState-matches {s} {sv} ρ₁,bss⇒ρ₂ ⟦vs⟧ρ₁
 
 
@@ -289,12 +325,44 @@ module WithProg (prog : Program) where
                 stepTrace {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ ρ₁,bss⇒ρ₂ =
                         let
                             -- I'd use rewrite, but Agda gets a memory overflow (?!).
-                            ⟦joinAll-result⟧ρ₁ = subst (λ vs → ⟦ vs ⟧ᵛ ρ₁) (sym (variablesAt-joinAll s₁ result)) ⟦joinForKey-s₁⟧ρ₁ 
-                            ⟦analyze-result⟧ρ₂ = updateAll-matches {sv = joinAll result} ρ₁,bss⇒ρ₂ ⟦joinAll-result⟧ρ₁
-                            analyze-result≈result = ≈ᵐ-sym {result} {updateAll (joinAll result)} result≈analyze-result
-                            analyze-s₁≈s₁ = variablesAt-≈ s₁ (updateAll (joinAll result)) result (analyze-result≈result)
+                            ⟦joinAll-result⟧ρ₁ =
+                                subst (λ vs → ⟦ vs ⟧ᵛ ρ₁)
+                                      (sym (variablesAt-joinAll s₁ result))
+                                      ⟦joinForKey-s₁⟧ρ₁
+                            ⟦analyze-result⟧ρ₂ =
+                                updateAll-matches {sv = joinAll result}
+                                                  ρ₁,bss⇒ρ₂ ⟦joinAll-result⟧ρ₁
+                            analyze-result≈result =
+                                ≈ᵐ-sym {result} {updateAll (joinAll result)}
+                                       result≈analyze-result
+                            analyze-s₁≈s₁ =
+                                variablesAt-≈ s₁ (updateAll (joinAll result))
+                                                 result (analyze-result≈result)
                         in
                             ⟦⟧ᵛ-respects-≈ᵛ {variablesAt s₁ (updateAll (joinAll result))} {variablesAt s₁ result} (analyze-s₁≈s₁) ρ₂ ⟦analyze-result⟧ρ₂
 
                 walkTrace : ∀ {s₁ s₂ ρ₁ ρ₂} → ⟦ joinForKey s₁ result ⟧ᵛ ρ₁ → Trace {graph} s₁ s₂ ρ₁ ρ₂ → ⟦ variablesAt s₂ result ⟧ᵛ ρ₂
-                walkTrace {s₁} {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ (Trace-single ρ₁,bss⇒ρ₂) = stepTrace {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ ρ₁,bss⇒ρ₂
+                walkTrace {s₁} {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ (Trace-single ρ₁,bss⇒ρ₂) =
+                    stepTrace {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ ρ₁,bss⇒ρ₂
+                walkTrace {s₁} {s₂} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ (Trace-edge {ρ₂ = ρ} {idx₂ = s} ρ₁,bss⇒ρ s₁→s₂ tr) =
+                    let
+                        ⟦result-s₁⟧ρ =
+                            stepTrace {s₁} {ρ₁} {ρ} ⟦joinForKey-s₁⟧ρ₁ ρ₁,bss⇒ρ
+                        s₁∈incomingStates =
+                            []-∈ result (edge⇒incoming s₁→s₂)
+                                        (variablesAt-∈ s₁ result)
+                        ⟦joinForKey-s⟧ρ =
+                            ⟦⟧ᵛ-foldr ⟦result-s₁⟧ρ s₁∈incomingStates
+                    in
+                        walkTrace ⟦joinForKey-s⟧ρ tr
+
+                postulate initialState-pred-∅ : incoming initialState ≡ []
+
+                joinForKey-initialState-⊥ᵛ : joinForKey initialState result ≡ ⊥ᵛ
+                joinForKey-initialState-⊥ᵛ = cong (λ ins → foldr _⊔ᵛ_ ⊥ᵛ (result [ ins ])) initialState-pred-∅
+
+                ⟦joinAll-initialState⟧ᵛ∅ : ⟦ joinForKey initialState result ⟧ᵛ []
+                ⟦joinAll-initialState⟧ᵛ∅ = subst (λ vs → ⟦ vs ⟧ᵛ []) (sym joinForKey-initialState-⊥ᵛ) ⟦⊥ᵛ⟧ᵛ∅
+
+                analyze-correct : ∀ {ρ : Env} → [] , rootStmt ⇒ˢ ρ → ⟦ variablesAt finalState result ⟧ᵛ ρ
+                analyze-correct {ρ} ∅,s⇒ρ = walkTrace {initialState} {finalState} {[]} {ρ} ⟦joinAll-initialState⟧ᵛ∅ (trace ∅,s⇒ρ)

Chain.agda

@@ -10,7 +10,7 @@ open import Data.Nat using (ℕ; suc; _+_; _≤_)
 open import Data.Nat.Properties using (+-comm; m+1+n≰m)
 open import Data.Product using (_×_; Σ; _,_)
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
-open import Data.Empty using (⊥)
+open import Data.Empty as Empty using ()
 
 open IsEquivalence ≈-equiv
 
@@ -38,11 +38,16 @@ module _  where
     Bounded : ℕ → Set a
     Bounded bound = ∀ {a₁ a₂ : A} {n : ℕ} → Chain a₁ a₂ n → n ≤ bound
 
-    Bounded-suc-n : ∀ {a₁ a₂ : A} {n : ℕ} → Bounded n → Chain a₁ a₂ (suc n) → ⊥
+    Bounded-suc-n : ∀ {a₁ a₂ : A} {n : ℕ} → Bounded n → Chain a₁ a₂ (suc n) → Empty.⊥
     Bounded-suc-n {a₁} {a₂} {n} bounded c = (m+1+n≰m n n+1≤n)
         where
             n+1≤n : n + 1 ≤ n
             n+1≤n rewrite (+-comm n 1) = bounded c
 
-    Height : ℕ → Set a
-    Height height = (Σ (A × A) (λ (a₁ , a₂) → Chain a₁ a₂ height) × Bounded height)
+    record Height (height : ℕ) : Set a where
+        field
+            ⊥ : A
+            ⊤ : A
+
+            longestChain : Chain ⊥ ⊤ height
+            bounded : Bounded height

Fixedpoint.agda

@@ -23,15 +23,21 @@ import Chain
 module ChainA = Chain _≈_ ≈-equiv _≺_ ≺-cong
 
 private
-    ⊥ᴬ : A
-    ⊥ᴬ = proj₁ (proj₁ (proj₁ fixedHeight))
+    open ChainA.Height fixedHeight
+        using ()
+        renaming
+            ( ⊥ to ⊥ᴬ
+            ; longestChain to longestChainᴬ
+            ; bounded to boundedᴬ
+            )
+
 
     ⊥ᴬ≼ : ∀ (a : A) → ⊥ᴬ ≼ a
     ⊥ᴬ≼ a with ≈-dec a ⊥ᴬ
     ...   | yes a≈⊥ᴬ = ≼-cong a≈⊥ᴬ ≈-refl (≼-refl a)
     ...   | no a̷≈⊥ᴬ with ≈-dec ⊥ᴬ (a ⊓ ⊥ᴬ)
     ...         | yes ⊥ᴬ≈a⊓⊥ᴬ = ≈-trans (⊔-comm ⊥ᴬ a) (≈-trans (≈-⊔-cong (≈-refl {a}) ⊥ᴬ≈a⊓⊥ᴬ) (absorb-⊔-⊓ a ⊥ᴬ))
-    ...         | no ⊥ᴬ̷≈a⊓⊥ᴬ = ⊥-elim (ChainA.Bounded-suc-n (proj₂ fixedHeight) (ChainA.step x≺⊥ᴬ ≈-refl (proj₂ (proj₁ fixedHeight))))
+    ...         | no ⊥ᴬ̷≈a⊓⊥ᴬ = ⊥-elim (ChainA.Bounded-suc-n boundedᴬ (ChainA.step x≺⊥ᴬ ≈-refl longestChainᴬ))
                     where
                         ⊥ᴬ⊓a̷≈⊥ᴬ : ¬ (⊥ᴬ ⊓ a) ≈ ⊥ᴬ
                         ⊥ᴬ⊓a̷≈⊥ᴬ = λ ⊥ᴬ⊓a≈⊥ᴬ → ⊥ᴬ̷≈a⊓⊥ᴬ (≈-trans (≈-sym ⊥ᴬ⊓a≈⊥ᴬ) (⊓-comm _ _))
@@ -45,7 +51,7 @@ private
     -- out, we have exceeded h steps, which shouldn't be possible.
 
     doStep : ∀ (g hᶜ : ℕ) (a₁ a₂ : A) (c : ChainA.Chain a₁ a₂ hᶜ) (g+hᶜ≡h : g + hᶜ ≡ suc h) (a₂≼fa₂ : a₂ ≼ f a₂) → Σ A (λ a → a ≈ f a)
-    doStep 0 hᶜ a₁ a₂ c g+hᶜ≡sh a₂≼fa₂ rewrite g+hᶜ≡sh = ⊥-elim (ChainA.Bounded-suc-n (proj₂ fixedHeight) c)
+    doStep 0 hᶜ a₁ a₂ c g+hᶜ≡sh a₂≼fa₂ rewrite g+hᶜ≡sh = ⊥-elim (ChainA.Bounded-suc-n boundedᴬ c)
     doStep (suc g') hᶜ a₁ a₂ c g+hᶜ≡sh a₂≼fa₂ rewrite sym (+-suc g' hᶜ)
         with ≈-dec a₂ (f a₂)
     ...   | yes a₂≈fa₂ = (a₂ , a₂≈fa₂)
@@ -71,7 +77,7 @@ private
                      (c : ChainA.Chain a₁ a₂ hᶜ) (g+hᶜ≡h : g + hᶜ ≡ suc h)
                      (a₂≼fa₂ : a₂ ≼ f a₂) →
                      proj₁ (doStep g hᶜ a₁ a₂ c g+hᶜ≡h a₂≼fa₂) ≼ a
-    stepPreservesLess 0 _ _ _ _ _ _ c g+hᶜ≡sh _ rewrite g+hᶜ≡sh = ⊥-elim (ChainA.Bounded-suc-n (proj₂ fixedHeight) c)
+    stepPreservesLess 0 _ _ _ _ _ _ c g+hᶜ≡sh _ rewrite g+hᶜ≡sh = ⊥-elim (ChainA.Bounded-suc-n boundedᴬ c)
     stepPreservesLess (suc g') hᶜ a₁ a₂ a a≈fa a₂≼a c g+hᶜ≡sh a₂≼fa₂ rewrite sym (+-suc g' hᶜ)
         with ≈-dec a₂ (f a₂)
     ...   | yes _ = a₂≼a

Isomorphism.agda

@@ -38,8 +38,9 @@ module TransportFiniteHeight
     open IsEquivalence ≈₁-equiv using () renaming (≈-sym to ≈₁-sym; ≈-trans to ≈₁-trans)
     open IsEquivalence ≈₂-equiv using () renaming (≈-sym to ≈₂-sym; ≈-trans to ≈₂-trans)
 
-    open import Chain _≈₁_ ≈₁-equiv _≺₁_ ≺₁-cong using () renaming (Chain to Chain₁; done to done₁; step to step₁)
-    open import Chain _≈₂_ ≈₂-equiv _≺₂_ ≺₂-cong using () renaming (Chain to Chain₂; done to done₂; step to step₂)
+    import Chain
+    open Chain _≈₁_ ≈₁-equiv _≺₁_ ≺₁-cong using () renaming (Chain to Chain₁; done to done₁; step to step₁)
+    open Chain _≈₂_ ≈₂-equiv _≺₂_ ≺₂-cong using () renaming (Chain to Chain₂; done to done₂; step to step₂)
 
     private
         f-Injective : Injective _≈₁_ _≈₂_ f
@@ -65,10 +66,17 @@ module TransportFiniteHeight
     isFiniteHeightLattice : IsFiniteHeightLattice B height _≈₂_ _⊔₂_ _⊓₂_
     isFiniteHeightLattice =
         let
-            (((a₁ , a₂) , c) , bounded₁) = IsFiniteHeightLattice.fixedHeight fhlA
+            open Chain.Height (IsFiniteHeightLattice.fixedHeight fhlA)
+                using ()
+                renaming (⊥ to ⊥₁; ⊤ to ⊤₁; bounded to bounded₁; longestChain to c)
         in record
             { isLattice = lB
-            ; fixedHeight = (((f a₁ , f a₂), portChain₁ c) , λ c' → bounded₁ (portChain₂ c'))
+            ; fixedHeight = record
+                { ⊥ = f ⊥₁
+                ; ⊤ = f ⊤₁
+                ; longestChain = portChain₁ c
+                ; bounded = λ c' → bounded₁ (portChain₂ c')
+                }
             }
 
     finiteHeightLattice : FiniteHeightLattice B

Language.agda

@@ -10,7 +10,7 @@ open import Data.Fin using (Fin; suc; zero)
 open import Data.Fin.Properties as FinProp using (suc-injective)
 open import Data.List as List using (List; []; _∷_)
 open import Data.List.Membership.Propositional as ListMem using ()
-open import Data.List.Relation.Unary.All using (All; []; _∷_)
+open import Data.List.Membership.Propositional.Properties as ListMemProp using (∈-filter⁺)
 open import Data.List.Relation.Unary.Any as RelAny using ()
 open import Data.Nat using (ℕ; suc)
 open import Data.Product using (_,_; Σ; proj₁; proj₂)
@@ -27,43 +27,26 @@ open import Lattice.MapSet _≟ˢ_ using ()
         ; to-List to to-Listˢ
         )
 
-private
-    z≢sf : ∀ {n : ℕ} (f : Fin n) → ¬ (zero ≡ suc f)
-    z≢sf f ()
-
-    z≢mapsfs : ∀ {n : ℕ} (fs : List (Fin n)) → All (λ sf → ¬ zero ≡ sf) (List.map suc fs)
-    z≢mapsfs [] = []
-    z≢mapsfs (f ∷ fs') = z≢sf f ∷ z≢mapsfs fs'
-
-    indices : ∀ (n : ℕ) → Σ (List (Fin n)) Unique
-    indices 0 = ([] , Utils.empty)
-    indices (suc n') =
-        let
-            (inds' , unids') = indices n'
-        in
-            ( zero ∷ List.map suc inds'
-            , push (z≢mapsfs inds') (Unique-map suc suc-injective unids')
-            )
-
-    indices-complete : ∀ (n : ℕ) (f : Fin n) → f ListMem.∈ (proj₁ (indices n))
-    indices-complete (suc n') zero = RelAny.here refl
-    indices-complete (suc n') (suc f') = RelAny.there (x∈xs⇒fx∈fxs suc (indices-complete n' f'))
-
 record Program : Set where
     field
         rootStmt : Stmt
 
     graph : Graph
-    graph = buildCfg rootStmt
+    graph = wrap (buildCfg rootStmt)
 
     State : Set
     State = Graph.Index graph
 
     initialState : State
-    initialState = proj₁ (buildCfg-input rootStmt)
+    initialState = proj₁ (wrap-input (buildCfg rootStmt))
 
     finalState : State
-    finalState = proj₁ (buildCfg-output rootStmt)
+    finalState = proj₁ (wrap-output (buildCfg rootStmt))
+
+    trace : ∀ {ρ : Env} → [] , rootStmt ⇒ˢ ρ → Trace {graph} initialState finalState [] ρ
+    trace {ρ} ∅,s⇒ρ
+        with MkEndToEndTrace idx₁ (RelAny.here refl) idx₂ (RelAny.here refl) tr
+             ← EndToEndTrace-wrap (buildCfg-sufficient ∅,s⇒ρ) = tr
 
     private
         vars-Set : StringSet
@@ -76,13 +59,13 @@ record Program : Set where
     vars-Unique = proj₂ vars-Set
 
     states : List State
-    states = proj₁ (indices (Graph.size graph))
+    states = indices graph
 
     states-complete : ∀ (s : State) → s ListMem.∈ states
-    states-complete = indices-complete (Graph.size graph)
+    states-complete = indices-complete graph
 
     states-Unique : Unique states
-    states-Unique = proj₂ (indices (Graph.size graph))
+    states-Unique = indices-Unique graph
 
     code : State → List BasicStmt
     code st = graph [ st ]
@@ -99,4 +82,10 @@ record Program : Set where
     open import Data.List.Membership.DecPropositional _≟ᵉ_ using (_∈?_)
 
     incoming : State → List State
-    incoming idx = List.filter (λ idx' → (idx' , idx) ∈? (Graph.edges graph)) states
+    incoming = predecessors graph
+
+    edge⇒incoming : ∀ {s₁ s₂ : State} → (s₁ , s₂) ListMem.∈ (Graph.edges graph) →
+                    s₁ ListMem.∈ (incoming s₂)
+    edge⇒incoming {s₁} {s₂} s₁,s₂∈es =
+        ∈-filter⁺ (λ s' → (s' , s₂) ∈? (Graph.edges graph))
+                  (states-complete s₁) s₁,s₂∈es

Language/Graphs.agda

@@ -7,15 +7,19 @@ open import Data.Fin.Properties as FinProp using (suc-injective)
 open import Data.List as List using (List; []; _∷_)
 open import Data.List.Membership.Propositional as ListMem using ()
 open import Data.List.Membership.Propositional.Properties as ListMemProp using ()
+open import Data.List.Relation.Unary.All using (All; []; _∷_)
+open import Data.List.Relation.Unary.Any as RelAny using ()
 open import Data.Nat as Nat using (ℕ; suc)
 open import Data.Nat.Properties using (+-assoc; +-comm)
-open import Data.Product using (_×_; Σ; _,_)
+open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
+open import Data.Product.Properties as ProdProp using ()
 open import Data.Vec using (Vec; []; _∷_; lookup; cast; _++_)
 open import Data.Vec.Properties using (cast-is-id; ++-assoc; lookup-++ˡ; cast-sym; ++-identityʳ; lookup-++ʳ)
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; refl; subst; trans)
+open import Relation.Nullary using (¬_)
 
 open import Lattice
-open import Utils using (x∈xs⇒fx∈fxs; ∈-cartesianProduct)
+open import Utils using (Unique; push; Unique-map; x∈xs⇒fx∈fxs; ∈-cartesianProduct)
 
 record Graph : Set where
     constructor MkGraph
@@ -112,8 +116,48 @@ singleton bss = record
     ; outputs = zero ∷ []
     }
 
+wrap : Graph → Graph
+wrap g = singleton [] ↦ g ↦ singleton []
+
 buildCfg : Stmt → Graph
 buildCfg ⟨ bs₁ ⟩ = singleton (bs₁ ∷ [])
 buildCfg (s₁ then s₂) = buildCfg s₁ ↦ buildCfg s₂
 buildCfg (if _ then s₁ else s₂) = singleton [] ↦ (buildCfg s₁ ∙ buildCfg s₂) ↦ singleton []
 buildCfg (while _ repeat s) = loop (buildCfg s)
+
+private
+    z≢sf : ∀ {n : ℕ} (f : Fin n) → ¬ (zero ≡ suc f)
+    z≢sf f ()
+
+    z≢mapsfs : ∀ {n : ℕ} (fs : List (Fin n)) → All (λ sf → ¬ zero ≡ sf) (List.map suc fs)
+    z≢mapsfs [] = []
+    z≢mapsfs (f ∷ fs') = z≢sf f ∷ z≢mapsfs fs'
+
+    finValues : ∀ (n : ℕ) → Σ (List (Fin n)) Unique
+    finValues 0 = ([] , Utils.empty)
+    finValues (suc n') =
+        let
+            (inds' , unids') = finValues n'
+        in
+            ( zero ∷ List.map suc inds'
+            , push (z≢mapsfs inds') (Unique-map suc suc-injective unids')
+            )
+
+    finValues-complete : ∀ (n : ℕ) (f : Fin n) → f ListMem.∈ (proj₁ (finValues n))
+    finValues-complete (suc n') zero = RelAny.here refl
+    finValues-complete (suc n') (suc f') = RelAny.there (x∈xs⇒fx∈fxs suc (finValues-complete n' f'))
+
+module _ (g : Graph) where
+    open import Data.List.Membership.DecPropositional (ProdProp.≡-dec (FinProp._≟_ {Graph.size g}) (FinProp._≟_ {Graph.size g})) using (_∈?_)
+
+    indices : List (Graph.Index g)
+    indices = proj₁ (finValues (Graph.size g))
+
+    indices-complete : ∀ (idx : (Graph.Index g)) → idx ListMem.∈ indices
+    indices-complete = finValues-complete (Graph.size g)
+
+    indices-Unique : Unique indices
+    indices-Unique = proj₂ (finValues (Graph.size g))
+
+    predecessors : (Graph.Index g) → List (Graph.Index g)
+    predecessors idx = List.filter (λ idx' → (idx' , idx) ∈? (Graph.edges g)) indices

Language/Properties.agda

@@ -18,22 +18,11 @@ open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym)
 
 open import Utils using (x∈xs⇒fx∈fxs; ∈-cartesianProduct; concat-∈)
 
+wrap-input : ∀ (g : Graph) → Σ (Graph.Index (wrap g)) (λ idx → Graph.inputs (wrap g) ≡ idx ∷ [])
+wrap-input g = (_ , refl)
 
-buildCfg-input : ∀ (s : Stmt) → let g = buildCfg s in Σ (Graph.Index g) (λ idx → Graph.inputs g ≡ idx ∷ [])
-buildCfg-input ⟨ bs₁ ⟩ = (zero , refl)
-buildCfg-input (s₁ then s₂)
-    with (idx , p) ← buildCfg-input s₁ rewrite p = (_ , refl)
-buildCfg-input (if _ then s₁ else s₂) = (zero , refl)
-buildCfg-input (while _ repeat s)
-    with (idx , p) ← buildCfg-input s rewrite p = (_ , refl)
-
-buildCfg-output : ∀ (s : Stmt) → let g = buildCfg s in Σ (Graph.Index g) (λ idx → Graph.outputs g ≡ idx ∷ [])
-buildCfg-output ⟨ bs₁ ⟩ = (zero , refl)
-buildCfg-output (s₁ then s₂)
-    with (idx , p) ← buildCfg-output s₂ rewrite p = (_ , refl)
-buildCfg-output (if _ then s₁ else s₂) = (_ , refl)
-buildCfg-output (while _ repeat s)
-    with (idx , p) ← buildCfg-output s rewrite p = (_ , refl)
+wrap-output : ∀ (g : Graph) → Σ (Graph.Index (wrap g)) (λ idx → Graph.outputs (wrap g) ≡ idx ∷ [])
+wrap-output g = (_ , refl)
 
 Trace-∙ˡ : ∀ {g₁ g₂ : Graph} {idx₁ idx₂ : Graph.Index g₁} {ρ₁ ρ₂ : Env} →
            Trace {g₁} idx₁ idx₂ ρ₁ ρ₂ →
@@ -224,6 +213,10 @@ EndToEndTrace-singleton ρ₁⇒ρ₂ = record
 EndToEndTrace-singleton[] : ∀ (ρ : Env) → EndToEndTrace {singleton []} ρ ρ
 EndToEndTrace-singleton[] env = EndToEndTrace-singleton []
 
+EndToEndTrace-wrap : ∀ {g : Graph} {ρ₁ ρ₂ : Env} →
+                     EndToEndTrace {g} ρ₁ ρ₂ → EndToEndTrace {wrap g} ρ₁ ρ₂
+EndToEndTrace-wrap {g} {ρ₁} {ρ₂} etr = EndToEndTrace-singleton[] ρ₁ ++ etr ++ EndToEndTrace-singleton[] ρ₂
+
 buildCfg-sufficient : ∀ {s : Stmt} {ρ₁ ρ₂ : Env} → ρ₁ , s ⇒ˢ ρ₂ →
                       EndToEndTrace {buildCfg s} ρ₁ ρ₂
 buildCfg-sufficient (⇒ˢ-⟨⟩ ρ₁ ρ₂ bs ρ₁,bs⇒ρ₂) =

Lattice/AboveBelow.agda

@@ -355,7 +355,12 @@ module Plain (x : A) where
         rewrite [x]≺y⇒y≡⊤ _ _ [x]≺y with ≈-⊤-⊤ ← y≈z = ⊥-elim (¬-Chain-⊤ c)
 
     fixedHeight : IsLattice.FixedHeight isLattice 2
-    fixedHeight = (((⊥ , ⊤) , longestChain) , isLongest)
+    fixedHeight = record
+        { ⊥ = ⊥
+        ; ⊤ = ⊤
+        ; longestChain = longestChain
+        ; bounded = isLongest
+        }
 
     isFiniteHeightLattice : IsFiniteHeightLattice AboveBelow 2 _≈_ _⊔_ _⊓_
     isFiniteHeightLattice = record

Lattice/FiniteMap.agda

@@ -30,7 +30,9 @@ open import Lattice.Map ≡-dec-A lB as Map
         ; absorb-⊓-⊔ to absorb-⊓ᵐ-⊔ᵐ
         ; ≈-dec to ≈ᵐ-dec
         ; _[_] 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_
@@ -104,6 +106,10 @@ module WithKeys (ks : List A) where
     _[_] : FiniteMap → List A → List B
     _[_] (m₁ , _) ks = m₁ [ ks ]ᵐ
 
+    []-∈ : ∀ {k : A} {v : B} {ks' : List A} (fm : FiniteMap) →
+           k ∈ˡ ks' → (k , v) ∈ fm → v ∈ˡ (fm [ ks' ])
+    []-∈ {k} {v} {ks'} (m , _) k∈ks' k,v∈fm = []ᵐ-∈ m k,v∈fm k∈ks' 
+
     ≈-equiv : IsEquivalence FiniteMap _≈_
     ≈-equiv = record
         { ≈-refl =
@@ -159,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/FiniteValueMap.agda

@@ -28,6 +28,7 @@ open import Data.List.Relation.Unary.All using (All)
 open import Data.List.Relation.Unary.Any using (Any; here; there)
 open import Relation.Nullary using (¬_)
 open import Isomorphism using (IsInverseˡ; IsInverseʳ)
+open import Chain using (Height)
 
 open import Lattice.Map ≡-dec-A lB
     using
@@ -104,6 +105,14 @@ module IterProdIsomorphism where
         _∈ᵐ_ : ∀ {ks : List A} → A × B → FiniteMap ks → Set
         _∈ᵐ_ {ks} = _∈_ ks
 
+    to-build : ∀ {b : B} {ks : List A} (uks : Unique ks) →
+               let fm = to uks (IP.build b tt (length ks))
+               in ∀ (k : A) (v : B) → (k , v) ∈ᵐ fm → v ≡ b
+    to-build {b} {k ∷ ks'} (push _ uks') k v (here refl) = refl
+    to-build {b} {k ∷ ks'} (push _ uks') k' v (there k',v∈m') =
+        to-build {ks = ks'} uks' k' v k',v∈m'
+
+
     -- The left inverse is: from (to x) = x
     from-to-inverseˡ : ∀ {ks : List A} (uks : Unique ks) →
                       IsInverseˡ (_≈ᵐ_ {ks}) (_≈ⁱᵖ_ {length ks})
@@ -153,6 +162,26 @@ module IterProdIsomorphism where
                                 fm'₂⊆fm'₁ k' v' k',v'∈fm'₂
                         in (v'' , (v'≈v'' , there k',v''∈fm'₁))
 
+    FromBothMaps : ∀ (k : A) (v : B) {ks : List A} (fm₁ fm₂ : FiniteMap ks) → Set
+    FromBothMaps k v fm₁ fm₂ =
+        Σ (B × B)
+          (λ (v₁ , v₂) → ( (v ≡ v₁ ⊔₂ v₂) × ((k , v₁) ∈ᵐ fm₁ × (k , v₂) ∈ᵐ fm₂)))
+
+    Provenance-union : ∀ {ks : List A} (fm₁ fm₂ : FiniteMap ks) {k : A} {v : B} →
+                       (k , v) ∈ᵐ (fm₁ ⊔ᵐ fm₂) → FromBothMaps k v fm₁ fm₂
+    Provenance-union fm₁@(m₁ , ks₁≡ks) fm₂@(m₂ , ks₂≡ks) {k} {v} k,v∈fm₁fm₂
+        with Expr-Provenance-≡ ((` m₁) ∪ (` m₂)) k,v∈fm₁fm₂
+    ...   | in₁ (single k,v∈m₁) k∉km₂
+            with k∈km₁ ← (forget k,v∈m₁)
+            rewrite trans ks₁≡ks (sym ks₂≡ks) =
+            ⊥-elim (k∉km₂ k∈km₁)
+    ...   | in₂ k∉km₁ (single k,v∈m₂)
+            with k∈km₂ ← (forget k,v∈m₂)
+            rewrite trans ks₁≡ks (sym ks₂≡ks) =
+            ⊥-elim (k∉km₁ k∈km₂)
+    ...   | bothᵘ {v₁} {v₂} (single k,v₁∈m₁) (single k,v₂∈m₂) =
+            ((v₁ , v₂) , (refl , (k,v₁∈m₁ , k,v₂∈m₂)))
+
     private
         first-key-in-map : ∀ {k : A} {ks : List A} (fm : FiniteMap (k ∷ ks)) →
                            Σ B (λ v → (k , v) ∈ᵐ fm)
@@ -204,26 +233,6 @@ module IterProdIsomorphism where
         k,v∈⇒k,v∈pop (m@(_ ∷ _ , push k≢ks _) , refl) k≢k' (here refl) = ⊥-elim (k≢k' refl)
         k,v∈⇒k,v∈pop (m@(_ ∷ _ , push k≢ks _) , refl) k≢k' (there k,v'∈fm') = k,v'∈fm'
 
-        FromBothMaps : ∀ (k : A) (v : B) {ks : List A} (fm₁ fm₂ : FiniteMap ks) → Set
-        FromBothMaps k v fm₁ fm₂ =
-            Σ (B × B)
-              (λ (v₁ , v₂) → ( (v ≡ v₁ ⊔₂ v₂) × ((k , v₁) ∈ᵐ fm₁ × (k , v₂) ∈ᵐ fm₂)))
-
-        Provenance-union : ∀ {ks : List A} (fm₁ fm₂ : FiniteMap ks) {k : A} {v : B} →
-                           (k , v) ∈ᵐ (fm₁ ⊔ᵐ fm₂) → FromBothMaps k v fm₁ fm₂
-        Provenance-union fm₁@(m₁ , ks₁≡ks) fm₂@(m₂ , ks₂≡ks) {k} {v} k,v∈fm₁fm₂
-            with Expr-Provenance-≡ ((` m₁) ∪ (` m₂)) k,v∈fm₁fm₂
-        ...   | in₁ (single k,v∈m₁) k∉km₂
-                with k∈km₁ ← (forget k,v∈m₁)
-                rewrite trans ks₁≡ks (sym ks₂≡ks) =
-                ⊥-elim (k∉km₂ k∈km₁)
-        ...   | in₂ k∉km₁ (single k,v∈m₂)
-                with k∈km₂ ← (forget k,v∈m₂)
-                rewrite trans ks₁≡ks (sym ks₂≡ks) =
-                ⊥-elim (k∉km₁ k∈km₂)
-        ...   | bothᵘ {v₁} {v₂} (single k,v₁∈m₁) (single k,v₂∈m₂) =
-                ((v₁ , v₂) , (refl , (k,v₁∈m₁ , k,v₂∈m₂)))
-
         pop-⊔-distr : ∀ {k : A} {ks : List A} (fm₁ fm₂ : FiniteMap (k ∷ ks)) →
                       pop (fm₁ ⊔ᵐ fm₂) ≈ᵐ (pop fm₁ ⊔ᵐ pop fm₂)
         pop-⊔-distr {k} {ks} fm₁@(m₁ , _) fm₂@(m₂ , _) =
@@ -407,3 +416,12 @@ module IterProdIsomorphism where
             (to-⊔-distr uks) (from-⊔-distr {ks})
             (from-to-inverseʳ uks) (from-to-inverseˡ uks)
             using (isFiniteHeightLattice; finiteHeightLattice) public
+
+        -- Helpful lemma: all entries of the 'bottom' map are assigned to bottom.
+
+        open Height (IsFiniteHeightLattice.fixedHeight isFiniteHeightLattice) using (⊥)
+
+        ⊥-contains-bottoms : ∀ {k : A} {v : B} → (k , v) ∈ᵐ ⊥ → v ≡ (Height.⊥ fhB)
+        ⊥-contains-bottoms {k} {v} k,v∈⊥
+            rewrite IP.⊥-built (length ks) ≈₂-dec ≈ᵘ-dec h₂ 0 fhB fixedHeightᵘ =
+            to-build uks k v k,v∈⊥

Lattice/IterProd.agda

@@ -11,9 +11,11 @@ module Lattice.IterProd {a} {A B : Set a}
     (lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_) (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
 
 open import Agda.Primitive using (lsuc)
-open import Data.Nat using (ℕ; suc; _+_)
-open import Data.Product using (_×_)
+open import Data.Nat using (ℕ; zero; suc; _+_)
+open import Data.Product using (_×_; _,_; proj₁; proj₂)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; cong)
 open import Utils using (iterate)
+open import Chain using (Height)
 
 open IsLattice lA renaming (FixedHeight to FixedHeight₁)
 open IsLattice lB renaming (FixedHeight to FixedHeight₂)
@@ -30,6 +32,10 @@ IterProd k = iterate k (λ t → A × t) B
 -- that are built up by the two iterations. So, do everything in one iteration.
 -- This requires some odd code.
 
+build : A → B → (k : ℕ) → IterProd k
+build _ b zero = b
+build a b (suc s) = (a , build a b s)
+
 private
     record RequiredForFixedHeight : Set (lsuc a) where
         field
@@ -39,22 +45,37 @@ private
             fhA : FixedHeight₁ h₁
             fhB : FixedHeight₂ h₂
 
-    record IsFiniteHeightAndDecEq {A : Set a} {_≈_ : A → A → Set a} {_⊔_ : A → A → A} {_⊓_ : A → A → A} (isLattice : IsLattice A _≈_ _⊔_ _⊓_) : Set (lsuc a) where
+        ⊥₁ : A
+        ⊥₁ = Height.⊥ fhA
+
+        ⊥₂ : B
+        ⊥₂ = Height.⊥ fhB
+
+        ⊥k : ∀ (k : ℕ) → IterProd k
+        ⊥k = build ⊥₁ ⊥₂
+
+    record IsFiniteHeightWithBotAndDecEq {A : Set a} {_≈_ : A → A → Set a} {_⊔_ : A → A → A} {_⊓_ : A → A → A} (isLattice : IsLattice A _≈_ _⊔_ _⊓_) (⊥ : A) : Set (lsuc a) where
         field
             height : ℕ
             fixedHeight : IsLattice.FixedHeight isLattice height
             ≈-dec : IsDecidable _≈_
 
-    record Everything (A : Set a) : Set (lsuc a) where
+            ⊥-correct : Height.⊥ fixedHeight ≡ ⊥
+
+    record Everything (k : ℕ) : Set (lsuc a) where
+        T = IterProd k
+
         field
-            _≈_ : A → A → Set a
-            _⊔_ : A → A → A
-            _⊓_ : A → A → A
+            _≈_ : T → T → Set a
+            _⊔_ : T → T → T
+            _⊓_ : T → T → T
 
-            isLattice : IsLattice A _≈_ _⊔_ _⊓_
-            isFiniteHeightIfSupported : RequiredForFixedHeight → IsFiniteHeightAndDecEq isLattice
+            isLattice : IsLattice T _≈_ _⊔_ _⊓_
+            isFiniteHeightIfSupported :
+                ∀ (req : RequiredForFixedHeight) →
+                IsFiniteHeightWithBotAndDecEq isLattice (RequiredForFixedHeight.⊥k req k)
 
-    everything : ∀ (k : ℕ) → Everything (IterProd k)
+    everything : ∀ (k : ℕ) → Everything k
     everything 0 = record
         { _≈_ = _≈₂_
         ; _⊔_ = _⊔₂_
@@ -64,6 +85,7 @@ private
             { height = RequiredForFixedHeight.h₂ req
             ; fixedHeight = RequiredForFixedHeight.fhB req
             ; ≈-dec = RequiredForFixedHeight.≈₂-dec req
+            ; ⊥-correct = refl
             }
         }
     everything (suc k') = record
@@ -76,13 +98,16 @@ private
                 fhlRest = Everything.isFiniteHeightIfSupported everythingRest req
             in
                 record
-                    { height = (RequiredForFixedHeight.h₁ req) + IsFiniteHeightAndDecEq.height fhlRest
+                    { height = (RequiredForFixedHeight.h₁ req) + IsFiniteHeightWithBotAndDecEq.height fhlRest
                     ; fixedHeight =
                         P.fixedHeight
-                        (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightAndDecEq.≈-dec fhlRest)
-                        (RequiredForFixedHeight.h₁ req) (IsFiniteHeightAndDecEq.height fhlRest)
-                        (RequiredForFixedHeight.fhA req) (IsFiniteHeightAndDecEq.fixedHeight fhlRest)
-                    ; ≈-dec = P.≈-dec (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightAndDecEq.≈-dec fhlRest)
+                        (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightWithBotAndDecEq.≈-dec fhlRest)
+                        (RequiredForFixedHeight.h₁ req) (IsFiniteHeightWithBotAndDecEq.height fhlRest)
+                        (RequiredForFixedHeight.fhA req) (IsFiniteHeightWithBotAndDecEq.fixedHeight fhlRest)
+                    ; ≈-dec = P.≈-dec (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightWithBotAndDecEq.≈-dec fhlRest)
+                    ; ⊥-correct =
+                        cong ((Height.⊥ (RequiredForFixedHeight.fhA req)) ,_)
+                             (IsFiniteHeightWithBotAndDecEq.⊥-correct fhlRest)
                     }
         }
         where
@@ -121,16 +146,22 @@ module _ (k : ℕ) where
                 ; fhB = fhB
                 }
 
+        fixedHeight = IsFiniteHeightWithBotAndDecEq.fixedHeight (Everything.isFiniteHeightIfSupported (everything k) required)
+
         isFiniteHeightLattice = record
             { isLattice = isLattice
-            ; fixedHeight = IsFiniteHeightAndDecEq.fixedHeight (Everything.isFiniteHeightIfSupported (everything k) required)
+            ; fixedHeight = fixedHeight
             }
 
         finiteHeightLattice : FiniteHeightLattice (IterProd k)
         finiteHeightLattice = record
-            { height = IsFiniteHeightAndDecEq.height (Everything.isFiniteHeightIfSupported (everything k) required)
+            { height = IsFiniteHeightWithBotAndDecEq.height (Everything.isFiniteHeightIfSupported (everything k) required)
             ; _≈_ = _≈_
             ; _⊔_ = _⊔_
             ; _⊓_ = _⊓_
             ; isFiniteHeightLattice = isFiniteHeightLattice
             }
+
+        ⊥-built : Height.⊥ fixedHeight ≡ (build (Height.⊥ fhA) (Height.⊥ fhB) k)
+        ⊥-built = IsFiniteHeightWithBotAndDecEq.⊥-correct (Everything.isFiniteHeightIfSupported (everything k) required)
+

Lattice/Map.agda

@@ -1112,6 +1112,19 @@ _[_] m (k ∷ ks)
 ...   | yes k∈km = proj₁ (locate {m = m} k∈km) ∷ (m [ ks ])
 ...   | no _ = m [ ks ]
 
+[]-∈ : ∀ {k : A} {v : B} {ks : List A} (m : Map) →
+       (k , v) ∈ m → k ∈ˡ ks → v ∈ˡ (m [ ks ])
+[]-∈ {k} {v} {ks} m k,v∈m (here refl)
+    with ∈k-dec k (proj₁ m)
+...    | no k∉km = ⊥-elim (k∉km (forget k,v∈m))
+...    | yes k∈km
+         with (v' , k,v'∈m) ← locate {m = m} k∈km
+         rewrite Map-functional {m = m} k,v'∈m k,v∈m = here refl
+[]-∈ {k} {v} {k' ∷ ks'} m k,v∈m (there k∈ks')
+    with ∈k-dec k' (proj₁ m)
+...   | no _  = []-∈ m k,v∈m k∈ks'
+...   | yes _ = there ([]-∈ m k,v∈m k∈ks')
+
 m₁≼m₂⇒m₁[k]≼m₂[k] : ∀ (m₁ m₂ : Map) {k : A} {v₁ v₂ : B} →
                     m₁ ≼ m₂ → (k , v₁) ∈ m₁ → (k , v₂) ∈ m₂ → v₁ ≼₂ v₂
 m₁≼m₂⇒m₁[k]≼m₂[k] m₁ m₂ m₁≼m₂ k,v₁∈m₁ k,v₂∈m₂
@@ -1129,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₂'

Lattice/Prod.agda

@@ -143,17 +143,8 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
         ∙,b-Preserves-≈₁ : ∀ (b : B) → (λ a → (a , b)) Preserves _≈₁_ ⟶  _≈_
         ∙,b-Preserves-≈₁ b {a₁} {a₂} a₁≈a₂ = (a₁≈a₂ , ≈₂-refl)
 
-        amin : A
-        amin = proj₁ (proj₁ (proj₁ fhA))
-
-        amax : A
-        amax = proj₂ (proj₁ (proj₁ fhA))
-
-        bmin : B
-        bmin = proj₁ (proj₁ (proj₁ fhB))
-
-        bmax : B
-        bmax = proj₂ (proj₁ (proj₁ fhB))
+        open ChainA.Height fhA using () renaming (⊥ to ⊥₁; ⊤ to ⊤₁; longestChain to longestChain₁; bounded to bounded₁)
+        open ChainB.Height fhB using () renaming (⊥ to ⊥₂; ⊤ to ⊤₂; longestChain to longestChain₂; bounded to bounded₂)
 
         unzip : ∀ {a₁ a₂ : A} {b₁ b₂ : B} {n : ℕ} → Chain (a₁ , b₁) (a₂ , b₂) n → Σ (ℕ × ℕ) (λ (n₁ , n₂) → ((Chain₁ a₁ a₂ n₁ × Chain₂ b₁ b₂ n₂) × (n ≤ n₁ + n₂)))
         unzip (done (a₁≈a₂ , b₁≈b₂)) = ((0 , 0) , ((done₁ a₁≈a₂ , done₂ b₁≈b₂) , ≤-refl))
@@ -172,15 +163,16 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
                                      ))
 
     fixedHeight : IsLattice.FixedHeight isLattice (h₁ + h₂)
-    fixedHeight =
-      ( ( ((amin , bmin) , (amax , bmax))
-        , concat
-            (ChainMapping₁.Chain-map (λ a → (a , bmin)) (∙,b-Monotonic _) proj₁ (∙,b-Preserves-≈₁ _) (proj₂ (proj₁ fhA)))
-            (ChainMapping₂.Chain-map (λ b → (amax , b)) (a,∙-Monotonic _) proj₂ (a,∙-Preserves-≈₂ _) (proj₂ (proj₁ fhB)))
-        )
-      , λ a₁b₁a₂b₂ → let ((n₁ , n₂) , ((a₁a₂ , b₁b₂) , n≤n₁+n₂)) = unzip a₁b₁a₂b₂
-                     in ≤-trans n≤n₁+n₂ (+-mono-≤ (proj₂ fhA a₁a₂) (proj₂ fhB b₁b₂))
-      )
+    fixedHeight = record
+      { ⊥ = (⊥₁ , ⊥₂)
+      ; ⊤ = (⊤₁ , ⊤₂)
+      ; longestChain = concat
+            (ChainMapping₁.Chain-map (λ a → (a , ⊥₂)) (∙,b-Monotonic _) proj₁ (∙,b-Preserves-≈₁ _) longestChain₁)
+            (ChainMapping₂.Chain-map (λ b → (⊤₁ , b)) (a,∙-Monotonic _) proj₂ (a,∙-Preserves-≈₂ _) longestChain₂)
+      ; bounded = λ a₁b₁a₂b₂ →
+            let ((n₁ , n₂) , ((a₁a₂ , b₁b₂) , n≤n₁+n₂)) = unzip a₁b₁a₂b₂
+            in ≤-trans n≤n₁+n₂ (+-mono-≤ (bounded₁ a₁a₂) (bounded₂ b₁b₂))
+      }
 
     isFiniteHeightLattice : IsFiniteHeightLattice (A × B) (h₁ + h₂) _≈_ _⊔_ _⊓_
     isFiniteHeightLattice = record

Lattice/Unit.agda

@@ -108,7 +108,12 @@ private
     isLongest (done _) = z≤n
 
 fixedHeight : IsLattice.FixedHeight isLattice 0
-fixedHeight = (((tt , tt) , longestChain) , isLongest)
+fixedHeight = record
+    { ⊥ = tt
+    ; ⊤ = tt
+    ; longestChain = longestChain
+    ; bounded = isLongest
+    }
 
 isFiniteHeightLattice : IsFiniteHeightLattice ⊤ 0 _≈_ _⊔_ _⊓_
 isFiniteHeightLattice = record