Analysis/Forward.agda

@@ -10,18 +10,16 @@ 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₁; proj₂; _,_)
+open import Data.Product using (_×_; 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; cong; sym; trans; subst)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; 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ˡ
@@ -64,32 +62,25 @@ 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ᵛ
-    ⊥ᵛ = Chain.Height.⊥ fixedHeightᵛ
+    ⊥ᵛ = proj₁ (proj₁ (proj₁ 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]; m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂)
+        using (_[_]; m₁≼m₂⇒m₁[ks]≼m₂[ks])
         renaming
             ( FiniteMap to StateVariables
             ; isLattice to isLatticeᵐ
             ; _≈_ to _≈ᵐ_
-            ; _∈_ to _∈ᵐ_
             ; _∈k_ to _∈kᵐ_
             ; locate to locateᵐ
             ; _≼_ to _≼ᵐ_
@@ -122,13 +113,8 @@ 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-≈ s sv₁ sv₂ sv₁≈sv₂ =
+    variablesAt-≈ = {!!}
-        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
     --
@@ -246,17 +232,11 @@ module WithProg (prog : Program) where
         module WithInterpretation (latticeInterpretationˡ : LatticeInterpretation isLatticeˡ) where
             open LatticeInterpretation latticeInterpretationˡ
                 using ()
-                renaming
+                renaming (⟦_⟧ to ⟦_⟧ˡ; ⟦⟧-respects-≈ to ⟦⟧ˡ-respects-≈ˡ)
-                    ( ⟦_⟧ 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₂ , _}
@@ -267,21 +247,9 @@ 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 {vs} {vs ∷ vss'} {ρ = ρ} ⟦vs⟧ρ (Any.here refl) =
+            ⟦⟧ᵛ-foldr = {!!}
-                ⟦⟧ᵛ-⊔ᵛ-∨ {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
@@ -307,17 +275,13 @@ 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
+                    updateVariablesFromStmt-fold-matches {bss'} {updateVariablesFromStmt bs vs} ρ,bss'⇒ρ₂ (updateVariablesFromStmt-matches ρ₁,bs⇒ρ ⟦vs⟧ρ₁)
-                        {bss'} {updateVariablesFromStmt bs vs} ρ,bss'⇒ρ₂
-                        (updateVariablesFromStmt-matches ρ₁,bs⇒ρ ⟦vs⟧ρ₁)
 
                 updateVariablesForState-matches : ∀ {s sv ρ₁ ρ₂} → ρ₁ , (code s) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s sv ⟧ᵛ ρ₁ → ⟦ updateVariablesForState s sv ⟧ᵛ ρ₂
-                updateVariablesForState-matches =
+                updateVariablesForState-matches = updateVariablesFromStmt-fold-matches
-                    updateVariablesFromStmt-fold-matches
 
                 updateAll-matches : ∀ {s sv ρ₁ ρ₂} → ρ₁ , (code s) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s sv ⟧ᵛ ρ₁ → ⟦ variablesAt s (updateAll sv) ⟧ᵛ ρ₂
-                updateAll-matches {s} {sv} ρ₁,bss⇒ρ₂ ⟦vs⟧ρ₁
+                updateAll-matches {s} {sv} ρ₁,bss⇒ρ₂ ⟦vs⟧ρ₁ rewrite variablesAt-updateAll s sv =
-                    rewrite variablesAt-updateAll s sv =
                     updateVariablesForState-matches {s} {sv} ρ₁,bss⇒ρ₂ ⟦vs⟧ρ₁
 
 
@@ -325,44 +289,12 @@ module WithProg (prog : Program) where
                 stepTrace {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ ρ₁,bss⇒ρ₂ =
                         let
                             -- I'd use rewrite, but Agda gets a memory overflow (?!).
-                            ⟦joinAll-result⟧ρ₁ =
+                            ⟦joinAll-result⟧ρ₁ = subst (λ vs → ⟦ vs ⟧ᵛ ρ₁) (sym (variablesAt-joinAll s₁ result)) ⟦joinForKey-s₁⟧ρ₁ 
-                                subst (λ vs → ⟦ vs ⟧ᵛ ρ₁)
+                            ⟦analyze-result⟧ρ₂ = updateAll-matches {sv = joinAll result} ρ₁,bss⇒ρ₂ ⟦joinAll-result⟧ρ₁
-                                      (sym (variablesAt-joinAll s₁ result))
+                            analyze-result≈result = ≈ᵐ-sym {result} {updateAll (joinAll result)} result≈analyze-result
-                                      ⟦joinForKey-s₁⟧ρ₁
+                            analyze-s₁≈s₁ = variablesAt-≈ s₁ (updateAll (joinAll result)) result (analyze-result≈result)
-                            ⟦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⇒ρ₂) =
+                walkTrace {s₁} {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ (Trace-single ρ₁,bss⇒ρ₂) = stepTrace {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ ρ₁,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 as Empty using ()
+open import Data.Empty using (⊥)
 
 open IsEquivalence ≈-equiv
 
@@ -38,16 +38,11 @@ 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) → Empty.⊥
+    Bounded-suc-n : ∀ {a₁ a₂ : A} {n : ℕ} → Bounded n → Chain a₁ a₂ (suc n) → ⊥
     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
 
-    record Height (height : ℕ) : Set a where
+    Height : ℕ → Set a
-        field
+    Height height = (Σ (A × A) (λ (a₁ , a₂) → Chain a₁ a₂ height) × Bounded height)
-            ⊥ : A
-            ⊤ : A
-
-            longestChain : Chain ⊥ ⊤ height
-            bounded : Bounded height

Fixedpoint.agda

@@ -23,21 +23,15 @@ import Chain
 module ChainA = Chain _≈_ ≈-equiv _≺_ ≺-cong
 
 private
-    open ChainA.Height fixedHeight
+    ⊥ᴬ : A
-        using ()
+    ⊥ᴬ = proj₁ (proj₁ (proj₁ fixedHeight))
-        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 boundedᴬ (ChainA.step x≺⊥ᴬ ≈-refl longestChainᴬ))
+    ...         | no ⊥ᴬ̷≈a⊓⊥ᴬ = ⊥-elim (ChainA.Bounded-suc-n (proj₂ fixedHeight) (ChainA.step x≺⊥ᴬ ≈-refl (proj₂ (proj₁ fixedHeight))))
                     where
                         ⊥ᴬ⊓a̷≈⊥ᴬ : ¬ (⊥ᴬ ⊓ a) ≈ ⊥ᴬ
                         ⊥ᴬ⊓a̷≈⊥ᴬ = λ ⊥ᴬ⊓a≈⊥ᴬ → ⊥ᴬ̷≈a⊓⊥ᴬ (≈-trans (≈-sym ⊥ᴬ⊓a≈⊥ᴬ) (⊓-comm _ _))
@@ -51,7 +45,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 boundedᴬ c)
+    doStep 0 hᶜ a₁ a₂ c g+hᶜ≡sh a₂≼fa₂ rewrite g+hᶜ≡sh = ⊥-elim (ChainA.Bounded-suc-n (proj₂ fixedHeight) 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₂)
@@ -77,7 +71,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 boundedᴬ c)
+    stepPreservesLess 0 _ _ _ _ _ _ c g+hᶜ≡sh _ rewrite g+hᶜ≡sh = ⊥-elim (ChainA.Bounded-suc-n (proj₂ fixedHeight) 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,9 +38,8 @@ module TransportFiniteHeight
     open IsEquivalence ≈₁-equiv using () renaming (≈-sym to ≈₁-sym; ≈-trans to ≈₁-trans)
     open IsEquivalence ≈₂-equiv using () renaming (≈-sym to ≈₂-sym; ≈-trans to ≈₂-trans)
 
-    import Chain
+    open import 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₁)
+    open import 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
@@ -66,17 +65,10 @@ module TransportFiniteHeight
     isFiniteHeightLattice : IsFiniteHeightLattice B height _≈₂_ _⊔₂_ _⊓₂_
     isFiniteHeightLattice =
         let
-            open Chain.Height (IsFiniteHeightLattice.fixedHeight fhlA)
+            (((a₁ , a₂) , c) , bounded₁) = IsFiniteHeightLattice.fixedHeight fhlA
-                using ()
-                renaming (⊥ to ⊥₁; ⊤ to ⊤₁; bounded to bounded₁; longestChain to c)
         in record
             { isLattice = lB
-            ; fixedHeight = record
+            ; fixedHeight = (((f a₁ , f a₂), portChain₁ c) , λ c' → bounded₁ (portChain₂ c'))
-                { ⊥ = 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.Membership.Propositional.Properties as ListMemProp using (∈-filter⁺)
+open import Data.List.Relation.Unary.All using (All; []; _∷_)
 open import Data.List.Relation.Unary.Any as RelAny using ()
 open import Data.Nat using (ℕ; suc)
 open import Data.Product using (_,_; Σ; proj₁; proj₂)
@@ -27,26 +27,43 @@ 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 = wrap (buildCfg rootStmt)
+    graph = buildCfg rootStmt
 
     State : Set
     State = Graph.Index graph
 
     initialState : State
-    initialState = proj₁ (wrap-input (buildCfg rootStmt))
+    initialState = proj₁ (buildCfg-input rootStmt)
 
     finalState : State
-    finalState = proj₁ (wrap-output (buildCfg rootStmt))
+    finalState = proj₁ (buildCfg-output 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
@@ -59,13 +76,13 @@ record Program : Set where
     vars-Unique = proj₂ vars-Set
 
     states : List State
-    states = indices graph
+    states = proj₁ (indices (Graph.size graph))
 
     states-complete : ∀ (s : State) → s ListMem.∈ states
-    states-complete = indices-complete graph
+    states-complete = indices-complete (Graph.size graph)
 
     states-Unique : Unique states
-    states-Unique = indices-Unique graph
+    states-Unique = proj₂ (indices (Graph.size graph))
 
     code : State → List BasicStmt
     code st = graph [ st ]
@@ -82,10 +99,4 @@ record Program : Set where
     open import Data.List.Membership.DecPropositional _≟ᵉ_ using (_∈?_)
 
     incoming : State → List State
-    incoming = predecessors graph
+    incoming idx = List.filter (λ idx' → (idx' , idx) ∈? (Graph.edges graph)) states
-
-    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,19 +7,15 @@ 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 (_×_; Σ; _,_; proj₁; proj₂)
+open import Data.Product using (_×_; Σ; _,_)
-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 (Unique; push; Unique-map; x∈xs⇒fx∈fxs; ∈-cartesianProduct)
+open import Utils using (x∈xs⇒fx∈fxs; ∈-cartesianProduct)
 
 record Graph : Set where
     constructor MkGraph
@@ -116,48 +112,8 @@ 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,11 +18,22 @@ 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)
 
-wrap-output : ∀ (g : Graph) → Σ (Graph.Index (wrap g)) (λ idx → Graph.outputs (wrap g) ≡ idx ∷ [])
+buildCfg-input : ∀ (s : Stmt) → let g = buildCfg s in Σ (Graph.Index g) (λ idx → Graph.inputs g ≡ idx ∷ [])
-wrap-output g = (_ , refl)
+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)
 
 Trace-∙ˡ : ∀ {g₁ g₂ : Graph} {idx₁ idx₂ : Graph.Index g₁} {ρ₁ ρ₂ : Env} →
            Trace {g₁} idx₁ idx₂ ρ₁ ρ₂ →
@@ -213,10 +224,6 @@ 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,12 +355,7 @@ module Plain (x : A) where
         rewrite [x]≺y⇒y≡⊤ _ _ [x]≺y with ≈-⊤-⊤ ← y≈z = ⊥-elim (¬-Chain-⊤ c)
 
     fixedHeight : IsLattice.FixedHeight isLattice 2
-    fixedHeight = record
+    fixedHeight = (((⊥ , ⊤) , longestChain) , isLongest)
-        { ⊥ = ⊥
-        ; ⊤ = ⊤
-        ; longestChain = longestChain
-        ; bounded = isLongest
-        }
 
     isFiniteHeightLattice : IsFiniteHeightLattice AboveBelow 2 _≈_ _⊔_ _⊓_
     isFiniteHeightLattice = record

Lattice/FiniteMap.agda

@@ -30,9 +30,7 @@ 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_
@@ -106,10 +104,6 @@ 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 =
@@ -165,11 +159,6 @@ 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,7 +28,6 @@ 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
@@ -105,14 +104,6 @@ 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})
@@ -162,26 +153,6 @@ 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)
@@ -233,6 +204,26 @@ 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₂ , _) =
@@ -416,12 +407,3 @@ 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,11 +11,9 @@ 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 (ℕ; zero; suc; _+_)
+open import Data.Nat using (ℕ; suc; _+_)
-open import Data.Product using (_×_; _,_; proj₁; proj₂)
+open import Data.Product using (_×_)
-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₂)
@@ -32,50 +30,31 @@ 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
+         field
             ≈₁-dec : IsDecidable _≈₁_
             ≈₂-dec : IsDecidable _≈₂_
             h₁ h₂ : ℕ
             fhA : FixedHeight₁ h₁
             fhB : FixedHeight₂ h₂
 
-        ⊥₁ : A
+    record IsFiniteHeightAndDecEq {A : Set a} {_≈_ : A → A → Set a} {_⊔_ : A → A → A} {_⊓_ : A → A → A} (isLattice : IsLattice A _≈_ _⊔_ _⊓_) : Set (lsuc a) where
-        ⊥₁ = 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 _≈_
 
-            ⊥-correct : Height.⊥ fixedHeight ≡ ⊥
+    record Everything (A : Set a) : Set (lsuc a) where
-
-    record Everything (k : ℕ) : Set (lsuc a) where
-        T = IterProd k
-
         field
-            _≈_ : T → T → Set a
+            _≈_ : A → A → Set a
-            _⊔_ : T → T → T
+            _⊔_ : A → A → A
-            _⊓_ : T → T → T
+            _⊓_ : A → A → A
 
-            isLattice : IsLattice T _≈_ _⊔_ _⊓_
+            isLattice : IsLattice A _≈_ _⊔_ _⊓_
-            isFiniteHeightIfSupported :
+            isFiniteHeightIfSupported : RequiredForFixedHeight → IsFiniteHeightAndDecEq isLattice
-                ∀ (req : RequiredForFixedHeight) →
-                IsFiniteHeightWithBotAndDecEq isLattice (RequiredForFixedHeight.⊥k req k)
 
-    everything : ∀ (k : ℕ) → Everything k
+    everything : ∀ (k : ℕ) → Everything (IterProd k)
     everything 0 = record
         { _≈_ = _≈₂_
         ; _⊔_ = _⊔₂_
@@ -85,7 +64,6 @@ private
             { height = RequiredForFixedHeight.h₂ req
             ; fixedHeight = RequiredForFixedHeight.fhB req
             ; ≈-dec = RequiredForFixedHeight.≈₂-dec req
-            ; ⊥-correct = refl
             }
         }
     everything (suc k') = record
@@ -98,16 +76,13 @@ private
                 fhlRest = Everything.isFiniteHeightIfSupported everythingRest req
             in
                 record
-                    { height = (RequiredForFixedHeight.h₁ req) + IsFiniteHeightWithBotAndDecEq.height fhlRest
+                    { height = (RequiredForFixedHeight.h₁ req) + IsFiniteHeightAndDecEq.height fhlRest
                     ; fixedHeight =
                         P.fixedHeight
-                        (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightWithBotAndDecEq.≈-dec fhlRest)
+                        (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightAndDecEq.≈-dec fhlRest)
-                        (RequiredForFixedHeight.h₁ req) (IsFiniteHeightWithBotAndDecEq.height fhlRest)
+                        (RequiredForFixedHeight.h₁ req) (IsFiniteHeightAndDecEq.height fhlRest)
-                        (RequiredForFixedHeight.fhA req) (IsFiniteHeightWithBotAndDecEq.fixedHeight fhlRest)
+                        (RequiredForFixedHeight.fhA req) (IsFiniteHeightAndDecEq.fixedHeight fhlRest)
-                    ; ≈-dec = P.≈-dec (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightWithBotAndDecEq.≈-dec fhlRest)
+                    ; ≈-dec = P.≈-dec (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightAndDecEq.≈-dec fhlRest)
-                    ; ⊥-correct =
-                        cong ((Height.⊥ (RequiredForFixedHeight.fhA req)) ,_)
-                             (IsFiniteHeightWithBotAndDecEq.⊥-correct fhlRest)
                     }
         }
         where
@@ -146,22 +121,16 @@ module _ (k : ℕ) where
                 ; fhB = fhB
                 }
 
-        fixedHeight = IsFiniteHeightWithBotAndDecEq.fixedHeight (Everything.isFiniteHeightIfSupported (everything k) required)
-
         isFiniteHeightLattice = record
             { isLattice = isLattice
-            ; fixedHeight = fixedHeight
+            ; fixedHeight = IsFiniteHeightAndDecEq.fixedHeight (Everything.isFiniteHeightIfSupported (everything k) required)
             }
 
         finiteHeightLattice : FiniteHeightLattice (IterProd k)
         finiteHeightLattice = record
-            { height = IsFiniteHeightWithBotAndDecEq.height (Everything.isFiniteHeightIfSupported (everything k) required)
+            { height = IsFiniteHeightAndDecEq.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,19 +1112,6 @@ _[_] 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₂
@@ -1142,12 +1129,3 @@ 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,8 +143,17 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
         ∙,b-Preserves-≈₁ : ∀ (b : B) → (λ a → (a , b)) Preserves _≈₁_ ⟶  _≈_
         ∙,b-Preserves-≈₁ b {a₁} {a₂} a₁≈a₂ = (a₁≈a₂ , ≈₂-refl)
 
-        open ChainA.Height fhA using () renaming (⊥ to ⊥₁; ⊤ to ⊤₁; longestChain to longestChain₁; bounded to bounded₁)
+        amin : A
-        open ChainB.Height fhB using () renaming (⊥ to ⊥₂; ⊤ to ⊤₂; longestChain to longestChain₂; bounded to bounded₂)
+        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))
 
         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))
@@ -163,16 +172,15 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
                                      ))
 
     fixedHeight : IsLattice.FixedHeight isLattice (h₁ + h₂)
-    fixedHeight = record
+    fixedHeight =
-      { ⊥ = (⊥₁ , ⊥₂)
+      ( ( ((amin , bmin) , (amax , bmax))
-      ; ⊤ = (⊤₁ , ⊤₂)
+        , concat
-      ; longestChain = concat
+            (ChainMapping₁.Chain-map (λ a → (a , bmin)) (∙,b-Monotonic _) proj₁ (∙,b-Preserves-≈₁ _) (proj₂ (proj₁ fhA)))
-            (ChainMapping₁.Chain-map (λ a → (a , ⊥₂)) (∙,b-Monotonic _) proj₁ (∙,b-Preserves-≈₁ _) longestChain₁)
+            (ChainMapping₂.Chain-map (λ b → (amax , b)) (a,∙-Monotonic _) proj₂ (a,∙-Preserves-≈₂ _) (proj₂ (proj₁ fhB)))
-            (ChainMapping₂.Chain-map (λ b → (⊤₁ , b)) (a,∙-Monotonic _) proj₂ (a,∙-Preserves-≈₂ _) longestChain₂)
+        )
-      ; bounded = λ a₁b₁a₂b₂ →
+      , λ a₁b₁a₂b₂ → let ((n₁ , n₂) , ((a₁a₂ , b₁b₂) , n≤n₁+n₂)) = unzip 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₂))
-            in ≤-trans n≤n₁+n₂ (+-mono-≤ (bounded₁ a₁a₂) (bounded₂ b₁b₂))
+      )
-      }
 
     isFiniteHeightLattice : IsFiniteHeightLattice (A × B) (h₁ + h₂) _≈_ _⊔_ _⊓_
     isFiniteHeightLattice = record

Lattice/Unit.agda

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