Move proof of least element into FiniteHeightLattice

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

Analysis/Constant.agda

@@ -0,0 +1,223 @@
+
+module Analysis.Constant where
+
+open import Data.Integer as Int using (ℤ; +_; -[1+_]; _≟_)
+open import Data.Integer.Show as IntShow using ()
+open import Data.Nat as Nat using (ℕ; suc; zero)
+open import Data.Product using (Σ; proj₁; proj₂; _,_)
+open import Data.Sum using (inj₁; inj₂)
+open import Data.Empty using (⊥; ⊥-elim)
+open import Data.Unit using (⊤; tt)
+open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; subst)
+open import Relation.Nullary using (¬_; yes; no)
+
+open import Equivalence
+open import Language
+open import Lattice
+open import Showable using (Showable; show)
+open import Utils using (_⇒_; _∧_; _∨_)
+open import Analysis.Utils using (eval-combine₂)
+import Analysis.Forward
+
+instance
+    showable : Showable ℤ
+    showable = record
+        { show = IntShow.show
+        }
+
+instance
+    ≡-equiv : IsEquivalence ℤ _≡_
+    ≡-equiv = record
+        { ≈-refl = refl
+        ; ≈-sym = sym
+        ; ≈-trans = trans
+        }
+
+    ≡-Decidable-ℤ : IsDecidable {_} {ℤ} _≡_
+    ≡-Decidable-ℤ = record { R-dec = _≟_ }
+
+-- embelish 'ℕ' with a top and bottom element.
+open import Lattice.AboveBelow ℤ _ as AB
+    using ()
+    renaming
+        ( AboveBelow to ConstLattice
+        ; ≈-dec to ≈ᶜ-dec
+        ; ⊥ to ⊥ᶜ
+        ; ⊤ to ⊤ᶜ
+        ; [_] to [_]ᶜ
+        ; _≈_ to _≈ᶜ_
+        ; ≈-⊥-⊥ to ≈ᶜ-⊥ᶜ-⊥ᶜ
+        ; ≈-⊤-⊤ to ≈ᶜ-⊤ᶜ-⊤ᶜ
+        ; ≈-lift to ≈ᶜ-lift
+        ; ≈-refl to ≈ᶜ-refl
+        )
+-- 'ℕ''s structure is not finite, so just use a 'plain' above-below Lattice.
+open AB.Plain (+ 0) using ()
+    renaming
+        ( isLattice to isLatticeᶜ
+        ; isFiniteHeightLattice to isFiniteHeightLatticeᵍ
+        ; _≼_ to _≼ᶜ_
+        ; _⊔_ to _⊔ᶜ_
+        ; _⊓_ to _⊓ᶜ_
+        ; ≼-trans to ≼ᶜ-trans
+        ; ≼-refl to ≼ᶜ-refl
+        )
+
+plus : ConstLattice → ConstLattice → ConstLattice
+plus ⊥ᶜ _ = ⊥ᶜ
+plus _ ⊥ᶜ = ⊥ᶜ
+plus ⊤ᶜ _ = ⊤ᶜ
+plus _ ⊤ᶜ = ⊤ᶜ
+plus [ z₁ ]ᶜ [ z₂ ]ᶜ = [ z₁ Int.+ z₂ ]ᶜ
+
+-- this is incredibly tedious: 125 cases per monotonicity proof, and tactics
+-- are hard. postulate for now.
+postulate plus-Monoˡ : ∀ (s₂ : ConstLattice) → Monotonic _≼ᶜ_ _≼ᶜ_ (λ s₁ → plus s₁ s₂)
+postulate plus-Monoʳ : ∀ (s₁ : ConstLattice) → Monotonic _≼ᶜ_ _≼ᶜ_ (plus s₁)
+
+plus-Mono₂ : Monotonic₂ _≼ᶜ_ _≼ᶜ_ _≼ᶜ_ plus
+plus-Mono₂ = (plus-Monoˡ , plus-Monoʳ)
+
+minus : ConstLattice → ConstLattice → ConstLattice
+minus ⊥ᶜ _ = ⊥ᶜ
+minus _ ⊥ᶜ = ⊥ᶜ
+minus ⊤ᶜ _ = ⊤ᶜ
+minus _ ⊤ᶜ = ⊤ᶜ
+minus [ z₁ ]ᶜ [ z₂ ]ᶜ = [ z₁ Int.- z₂ ]ᶜ
+
+postulate minus-Monoˡ : ∀ (s₂ : ConstLattice) → Monotonic _≼ᶜ_ _≼ᶜ_ (λ s₁ → minus s₁ s₂)
+postulate minus-Monoʳ : ∀ (s₁ : ConstLattice) → Monotonic _≼ᶜ_ _≼ᶜ_ (minus s₁)
+
+minus-Mono₂ : Monotonic₂ _≼ᶜ_ _≼ᶜ_ _≼ᶜ_ minus
+minus-Mono₂ = (minus-Monoˡ , minus-Monoʳ)
+
+⟦_⟧ᶜ : ConstLattice → Value → Set
+⟦_⟧ᶜ ⊥ᶜ _ = ⊥
+⟦_⟧ᶜ ⊤ᶜ _ = ⊤
+⟦_⟧ᶜ [ z ]ᶜ v = v ≡ ↑ᶻ z
+
+⟦⟧ᶜ-respects-≈ᶜ : ∀ {s₁ s₂ : ConstLattice} → s₁ ≈ᶜ s₂ → ⟦ s₁ ⟧ᶜ ⇒ ⟦ s₂ ⟧ᶜ
+⟦⟧ᶜ-respects-≈ᶜ ≈ᶜ-⊥ᶜ-⊥ᶜ v bot = bot
+⟦⟧ᶜ-respects-≈ᶜ ≈ᶜ-⊤ᶜ-⊤ᶜ v top = top
+⟦⟧ᶜ-respects-≈ᶜ (≈ᶜ-lift { z } { z } refl) v proof = proof
+
+⟦⟧ᶜ-⊔ᶜ-∨ : ∀ {s₁ s₂ : ConstLattice} → (⟦ s₁ ⟧ᶜ ∨ ⟦ s₂ ⟧ᶜ) ⇒ ⟦ s₁ ⊔ᶜ s₂ ⟧ᶜ
+⟦⟧ᶜ-⊔ᶜ-∨ {⊥ᶜ} x (inj₂ px₂) = px₂
+⟦⟧ᶜ-⊔ᶜ-∨ {⊤ᶜ} x _ = tt
+⟦⟧ᶜ-⊔ᶜ-∨ {[ s₁ ]ᶜ} {[ s₂ ]ᶜ} x px
+    with s₁ ≟ s₂
+...   | no _ = tt
+...   | yes refl
+        with px
+...       | inj₁ px₁ = px₁
+...       | inj₂ px₂ = px₂
+⟦⟧ᶜ-⊔ᶜ-∨ {[ s₁ ]ᶜ} {⊥ᶜ} x (inj₁ px₁) = px₁
+⟦⟧ᶜ-⊔ᶜ-∨ {[ s₁ ]ᶜ} {⊤ᶜ} x _ = tt
+
+s₁≢s₂⇒¬s₁∧s₂ : ∀ {z₁ z₂ : ℤ} → ¬ z₁ ≡ z₂ → ∀ {v} → ¬ ((⟦ [ z₁ ]ᶜ ⟧ᶜ ∧ ⟦ [ z₂ ]ᶜ ⟧ᶜ) v)
+s₁≢s₂⇒¬s₁∧s₂ { z₁ } { z₂ } z₁≢z₂ {v} (v≡z₁ , v≡z₂)
+    with refl ← trans (sym v≡z₁) v≡z₂ = z₁≢z₂ refl
+
+⟦⟧ᶜ-⊓ᶜ-∧ : ∀ {s₁ s₂ : ConstLattice} → (⟦ s₁ ⟧ᶜ ∧ ⟦ s₂ ⟧ᶜ) ⇒ ⟦ s₁ ⊓ᶜ s₂ ⟧ᶜ
+⟦⟧ᶜ-⊓ᶜ-∧ {⊥ᶜ} x (bot , _) = bot
+⟦⟧ᶜ-⊓ᶜ-∧ {⊤ᶜ} x (_ , px₂) = px₂
+⟦⟧ᶜ-⊓ᶜ-∧ {[ s₁ ]ᶜ} {[ s₂ ]ᶜ} x (px₁ , px₂)
+    with s₁ ≟ s₂
+...   | no s₁≢s₂ = s₁≢s₂⇒¬s₁∧s₂ s₁≢s₂ (px₁ , px₂)
+...   | yes refl = px₁
+⟦⟧ᶜ-⊓ᶜ-∧ {[ g₁ ]ᶜ} {⊥ᶜ} x (_ , bot) = bot
+⟦⟧ᶜ-⊓ᶜ-∧ {[ g₁ ]ᶜ} {⊤ᶜ} x (px₁ , _) = px₁
+
+instance
+    latticeInterpretationᶜ : LatticeInterpretation isLatticeᶜ
+    latticeInterpretationᶜ = record
+        { ⟦_⟧ = ⟦_⟧ᶜ
+        ; ⟦⟧-respects-≈ = ⟦⟧ᶜ-respects-≈ᶜ
+        ; ⟦⟧-⊔-∨ = ⟦⟧ᶜ-⊔ᶜ-∨
+        ; ⟦⟧-⊓-∧ = ⟦⟧ᶜ-⊓ᶜ-∧
+        }
+
+module WithProg (prog : Program) where
+    open Program prog
+
+    open import Analysis.Forward.Lattices ConstLattice prog
+    open import Analysis.Forward.Evaluation ConstLattice prog
+    open import Analysis.Forward.Adapters ConstLattice prog
+
+    eval : ∀ (e : Expr) → VariableValues → ConstLattice
+    eval (e₁ + e₂) vs = plus (eval e₁ vs) (eval e₂ vs)
+    eval (e₁ - e₂) vs = minus (eval e₁ vs) (eval e₂ vs)
+    eval (` k) vs
+        with ∈k-decᵛ k (proj₁ (proj₁ vs))
+    ...   | yes k∈vs = proj₁ (locateᵛ {k} {vs} k∈vs)
+    ...   | no _ = ⊤ᶜ
+    eval (# n) _ = [ + n ]ᶜ
+
+    eval-Monoʳ : ∀ (e : Expr) → Monotonic _≼ᵛ_ _≼ᶜ_ (eval e)
+    eval-Monoʳ (e₁ + e₂) {vs₁} {vs₂} vs₁≼vs₂ =
+        eval-combine₂ (λ {x} {y} {z} →  ≼ᶜ-trans {x} {y} {z})
+                      plus plus-Mono₂ {o₁ = eval e₁ vs₁}
+                      (eval-Monoʳ e₁ vs₁≼vs₂) (eval-Monoʳ e₂ vs₁≼vs₂)
+    eval-Monoʳ (e₁ - e₂) {vs₁} {vs₂} vs₁≼vs₂ =
+        eval-combine₂ (λ {x} {y} {z} →  ≼ᶜ-trans {x} {y} {z})
+                      minus minus-Mono₂ {o₁ = eval e₁ vs₁}
+                      (eval-Monoʳ e₁ vs₁≼vs₂) (eval-Monoʳ e₂ vs₁≼vs₂)
+    eval-Monoʳ (` k) {vs₁@((kvs₁ , _) , _)} {vs₂@((kvs₂ , _), _)} vs₁≼vs₂
+        with ∈k-decᵛ k kvs₁ | ∈k-decᵛ k kvs₂
+    ...   | yes k∈kvs₁ | yes k∈kvs₂ =
+            let
+                (v₁ , k,v₁∈vs₁) = locateᵛ {k} {vs₁} k∈kvs₁
+                (v₂ , k,v₂∈vs₂) = locateᵛ {k} {vs₂} k∈kvs₂
+            in
+                m₁≼m₂⇒m₁[k]ᵛ≼m₂[k]ᵛ vs₁ vs₂ vs₁≼vs₂ k,v₁∈vs₁ k,v₂∈vs₂
+    ...   | yes k∈kvs₁ | no k∉kvs₂ = ⊥-elim (k∉kvs₂ (subst (λ l → k ∈ˡ l) (all-equal-keysᵛ vs₁ vs₂) k∈kvs₁))
+    ...   | no k∉kvs₁ | yes k∈kvs₂ = ⊥-elim (k∉kvs₁ (subst (λ l → k ∈ˡ l) (all-equal-keysᵛ vs₂ vs₁) k∈kvs₂))
+    ...   | no k∉kvs₁ | no k∉kvs₂ = IsLattice.≈-refl isLatticeᶜ
+    eval-Monoʳ (# n) _ = ≼ᶜ-refl ([ + n ]ᶜ)
+
+    instance
+        ConstEval : ExprEvaluator
+        ConstEval = record { eval = eval; eval-Monoʳ = eval-Monoʳ }
+
+    -- For debugging purposes, print out the result.
+    output = show (Analysis.Forward.WithProg.result ConstLattice prog)
+
+    -- This should have fewer cases -- the same number as the actual 'plus' above.
+    -- But agda only simplifies on first argument, apparently, so we are stuck
+    -- listing them all.
+    plus-valid : ∀ {g₁ g₂} {z₁ z₂} → ⟦ g₁ ⟧ᶜ (↑ᶻ z₁) → ⟦ g₂ ⟧ᶜ (↑ᶻ z₂) → ⟦ plus g₁ g₂ ⟧ᶜ (↑ᶻ (z₁ Int.+ z₂))
+    plus-valid {⊥ᶜ} {_} ⊥ _ = ⊥
+    plus-valid {[ z ]ᶜ} {⊥ᶜ} _ ⊥ = ⊥
+    plus-valid {⊤ᶜ} {⊥ᶜ} _ ⊥ = ⊥
+    plus-valid {⊤ᶜ} {[ z ]ᶜ} _ _ = tt
+    plus-valid {⊤ᶜ} {⊤ᶜ} _ _ = tt
+    plus-valid {[ z₁ ]ᶜ} {[ z₂ ]ᶜ} refl refl = refl
+    plus-valid {[ z ]ᶜ} {⊤ᶜ} _ _ = tt
+    --
+    -- Same for this one. It should be easier, but Agda won't simplify.
+    minus-valid : ∀ {g₁ g₂} {z₁ z₂} → ⟦ g₁ ⟧ᶜ (↑ᶻ z₁) → ⟦ g₂ ⟧ᶜ (↑ᶻ z₂) → ⟦ minus g₁ g₂ ⟧ᶜ (↑ᶻ (z₁ Int.- z₂))
+    minus-valid {⊥ᶜ} {_} ⊥ _ = ⊥
+    minus-valid {[ z ]ᶜ} {⊥ᶜ} _ ⊥ = ⊥
+    minus-valid {⊤ᶜ} {⊥ᶜ} _ ⊥ = ⊥
+    minus-valid {⊤ᶜ} {[ z ]ᶜ} _ _ = tt
+    minus-valid {⊤ᶜ} {⊤ᶜ} _ _ = tt
+    minus-valid {[ z₁ ]ᶜ} {[ z₂ ]ᶜ} refl refl = refl
+    minus-valid {[ z ]ᶜ} {⊤ᶜ} _ _ = tt
+
+    eval-valid : IsValidExprEvaluator
+    eval-valid (⇒ᵉ-+ ρ e₁ e₂ z₁ z₂ ρ,e₁⇒z₁ ρ,e₂⇒z₂) ⟦vs⟧ρ =
+        plus-valid (eval-valid ρ,e₁⇒z₁ ⟦vs⟧ρ) (eval-valid ρ,e₂⇒z₂ ⟦vs⟧ρ)
+    eval-valid (⇒ᵉ-- ρ e₁ e₂ z₁ z₂ ρ,e₁⇒z₁ ρ,e₂⇒z₂) ⟦vs⟧ρ =
+        minus-valid (eval-valid ρ,e₁⇒z₁ ⟦vs⟧ρ) (eval-valid ρ,e₂⇒z₂ ⟦vs⟧ρ)
+    eval-valid {vs} (⇒ᵉ-Var ρ x v x,v∈ρ) ⟦vs⟧ρ
+        with ∈k-decᵛ x (proj₁ (proj₁ vs))
+    ...   | yes x∈kvs = ⟦vs⟧ρ (proj₂ (locateᵛ {x} {vs} x∈kvs)) x,v∈ρ
+    ...   | no x∉kvs = tt
+    eval-valid (⇒ᵉ-ℕ ρ n) _ = refl
+
+    instance
+        ConstEvalValid : ValidExprEvaluator ConstEval latticeInterpretationᶜ
+        ConstEvalValid = record { valid = eval-valid }
+
+    analyze-correct = Analysis.Forward.WithProg.analyze-correct ConstLattice prog tt

Analysis/Forward.agda

@@ -2,203 +2,35 @@ open import Language hiding (_[_])
 open import Lattice
 
 module Analysis.Forward
-    {L : Set} {h}
+    (L : Set) {h}
     {_≈ˡ_ : L → L → Set} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L}
-    (isFiniteHeightLatticeˡ : IsFiniteHeightLattice L h _≈ˡ_ _⊔ˡ_ _⊓ˡ_)
+    {{isFiniteHeightLatticeˡ : IsFiniteHeightLattice L h _≈ˡ_ _⊔ˡ_ _⊓ˡ_}}
-    (≈ˡ-dec : IsDecidable _≈ˡ_) where
+    {{≈ˡ-dec : IsDecidable _≈ˡ_}} where
 
 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.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.Nullary using (¬_; Dec; yes; no)
 open import Data.Unit using (⊤)
+open import Data.String using (String)
+open import Data.Product using (_,_)
+open import Data.List using (_∷_; []; foldr; foldl)
+open import Data.List.Relation.Unary.Any as Any using ()
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym; subst)
+open import Relation.Nullary using (yes; no)
 open import Function using (_∘_; flip)
-import Chain
-
-open import Utils using (Pairwise; _⇒_; _∨_)
-import Lattice.FiniteValueMap
 
 open IsFiniteHeightLattice isFiniteHeightLatticeˡ
-    using ()
+    using () renaming (isLattice to isLatticeˡ)
-    renaming
-        ( isLattice to isLatticeˡ
-        ; fixedHeight to fixedHeightˡ
-        ; _≼_ to _≼ˡ_
-        ; ≈-sym to ≈ˡ-sym
-        )
 
 module WithProg (prog : Program) where
+    open import Analysis.Forward.Lattices L prog hiding (≈ᵛ-Decidable; ≈ᵐ-Decidable) -- to disambiguate instance resolution
+    open import Analysis.Forward.Evaluation L prog
     open Program prog
 
-    -- The variable -> abstract value (e.g. sign) map is a finite value-map
+    private module WithStmtEvaluator {{evaluator : StmtEvaluator}} where
-    -- with keys strings. Use a bundle to avoid explicitly specifying operators.
+        open StmtEvaluator evaluator
-    module VariableValuesFiniteMap = Lattice.FiniteValueMap.WithKeys _≟ˢ_ isLatticeˡ vars
-    open VariableValuesFiniteMap
-        using ()
-        renaming
-            ( FiniteMap to VariableValues
-            ; isLattice to isLatticeᵛ
-            ; _≈_ to _≈ᵛ_
-            ; _⊔_ to _⊔ᵛ_
-            ; _≼_ to _≼ᵛ_
-            ; ≈₂-dec⇒≈-dec to ≈ˡ-dec⇒≈ᵛ-dec
-            ; _∈_ to _∈ᵛ_
-            ; _∈k_ to _∈kᵛ_
-            ; _updating_via_ to _updatingᵛ_via_
-            ; locate to locateᵛ
-            ; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵛ≼m₂[k]ᵛ
-            ; ∈k-dec to ∈k-decᵛ
-            ; all-equal-keys to all-equal-keysᵛ
-            )
-        public
-    open IsLattice isLatticeᵛ
-        using ()
-        renaming
-            ( ⊔-Monotonicˡ to ⊔ᵛ-Monotonicˡ
-            ; ⊔-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ᵛ
-
-    -- 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₂)
-        renaming
-            ( FiniteMap to StateVariables
-            ; isLattice to isLatticeᵐ
-            ; _≈_ to _≈ᵐ_
-            ; _∈_ to _∈ᵐ_
-            ; _∈k_ to _∈kᵐ_
-            ; locate to locateᵐ
-            ; _≼_ to _≼ᵐ_
-            ; ≈₂-dec⇒≈-dec to ≈ᵛ-dec⇒≈ᵐ-dec
-            ; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ
-            )
-        public
-    open Lattice.FiniteValueMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight _≟_ isLatticeᵛ states-Unique ≈ᵛ-dec _ fixedHeightᵛ
-        using ()
-        renaming
-            ( isFiniteHeightLattice to isFiniteHeightLatticeᵐ
-            )
-    open IsFiniteHeightLattice isFiniteHeightLatticeᵐ
-        using ()
-        renaming
-            ( ≈-sym to ≈ᵐ-sym
-            )
-
-    ≈ᵐ-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))
-
-    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₂ =
-        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
-    --
-    --    L₁ → (A → L₂)
-    --
-    -- Construction, with L₁ = (A → L₂), and f = id
-
-    joinForKey : State → StateVariables → VariableValues
-    joinForKey k states = foldr _⊔ᵛ_ ⊥ᵛ (states [ incoming k ])
-
-    -- The per-key join is made up of map key accesses (which are monotonic)
-    -- and folds using the join operation (also monotonic)
-
-    joinForKey-Mono : ∀ (k : State) → Monotonic _≼ᵐ_ _≼ᵛ_ (joinForKey k)
-    joinForKey-Mono k {fm₁} {fm₂} fm₁≼fm₂ =
-        foldr-Mono joinSemilatticeᵛ joinSemilatticeᵛ (fm₁ [ incoming k ]) (fm₂ [ incoming k ]) _⊔ᵛ_ ⊥ᵛ ⊥ᵛ
-                   (m₁≼m₂⇒m₁[ks]≼m₂[ks] fm₁ fm₂ (incoming k) fm₁≼fm₂)
-                   (⊔ᵛ-idemp ⊥ᵛ) ⊔ᵛ-Monotonicʳ ⊔ᵛ-Monotonicˡ
-
-    -- The name f' comes from the formulation of Exercise 4.26.
-    open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) joinForKey joinForKey-Mono states
-        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
-
-        -- For a particular evaluation function, we need to perform an evaluation
-        -- for an assignment, and update the corresponding key. Use Exercise 4.26's
-        -- generalized update to set the single key's value.
-
-        private module _ (k : String) (e : Expr) where
-            open VariableValuesFiniteMap.GeneralizedUpdate vars isLatticeᵛ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) (λ _ → eval e) (λ _ {vs₁} {vs₂} vs₁≼vs₂ → eval-Mono e {vs₁} {vs₂} vs₁≼vs₂) (k ∷ [])
-                renaming
-                    ( f' to updateVariablesFromExpression
-                    ; f'-Monotonic to updateVariablesFromExpression-Mono
-                    ; f'-k∈ks-≡ to updateVariablesFromExpression-k∈ks-≡
-                    ; f'-k∉ks-backward to updateVariablesFromExpression-k∉ks-backward
-                    )
-                public
-
-        -- The per-state update function makes use of the single-key setter,
-        -- updateVariablesFromExpression, for the case where the statement
-        -- is an assignment.
-        --
-        -- This per-state function adjusts the variables in that state,
-        -- also monotonically; we derive the for-each-state update from
-        -- the Exercise 4.26 again.
-
-        updateVariablesFromStmt : BasicStmt → VariableValues → VariableValues
-        updateVariablesFromStmt (k ← e) vs = updateVariablesFromExpression k e vs
-        updateVariablesFromStmt noop vs = vs
-
-        updateVariablesFromStmt-Monoʳ : ∀ (bs : BasicStmt) → Monotonic _≼ᵛ_ _≼ᵛ_ (updateVariablesFromStmt bs)
-        updateVariablesFromStmt-Monoʳ (k ← e) {vs₁} {vs₂} vs₁≼vs₂ = updateVariablesFromExpression-Mono k e {vs₁} {vs₂} vs₁≼vs₂
-        updateVariablesFromStmt-Monoʳ noop vs₁≼vs₂ = vs₁≼vs₂
 
         updateVariablesForState : State → StateVariables → VariableValues
         updateVariablesForState s sv =
-            foldl (flip updateVariablesFromStmt) (variablesAt s sv) (code s)
+            foldl (flip (eval s)) (variablesAt s sv) (code s)
 
         updateVariablesForState-Monoʳ : ∀ (s : State) → Monotonic _≼ᵐ_ _≼ᵛ_ (updateVariablesForState s)
         updateVariablesForState-Monoʳ s {sv₁} {sv₂} sv₁≼sv₂ =
@@ -209,15 +41,17 @@ module WithProg (prog : Program) where
                 vs₁≼vs₂ = m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ sv₁ sv₂ sv₁≼sv₂ s,vs₁∈sv₁ s,vs₂∈sv₂
             in
                 foldl-Mono' (IsLattice.joinSemilattice isLatticeᵛ) bss
-                            (flip updateVariablesFromStmt) updateVariablesFromStmt-Monoʳ
+                            (flip (eval s)) (eval-Monoʳ s)
                             vs₁≼vs₂
 
-        open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) updateVariablesForState updateVariablesForState-Monoʳ states
+        open StateVariablesFiniteMap.GeneralizedUpdate {{isLatticeᵐ}} (λ x → x) (λ a₁≼a₂ → a₁≼a₂) updateVariablesForState updateVariablesForState-Monoʳ states
+            using ()
             renaming
                 ( f' to updateAll
                 ; f'-Monotonic to updateAll-Mono
                 ; f'-k∈ks-≡ to updateAll-k∈ks-≡
                 )
+            public
 
         -- Finally, the whole analysis consists of getting the 'join'
         -- of all incoming states, then applying the per-state evaluation
@@ -232,7 +66,7 @@ module WithProg (prog : Program) where
                            (joinAll-Mono {sv₁} {sv₂} sv₁≼sv₂)
 
         -- 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₂)
+        open import Fixedpoint analyze (λ {m₁} {m₂} m₁≼m₂ → analyze-Mono {m₁} {m₂} m₁≼m₂)
             using ()
             renaming (aᶠ to result; aᶠ≈faᶠ to result≈analyze-result)
             public
@@ -243,124 +77,68 @@ module WithProg (prog : Program) where
             with (vs , s,vs∈usv) ← locateᵐ {s} {updateAll sv} (states-in-Map s (updateAll sv)) =
             updateAll-k∈ks-≡ {l = sv} (states-complete s) s,vs∈usv
 
-        module WithInterpretation (latticeInterpretationˡ : LatticeInterpretation isLatticeˡ) where
+        module WithValidInterpretation {{latticeInterpretationˡ : LatticeInterpretation isLatticeˡ}}
-            open LatticeInterpretation latticeInterpretationˡ
+                                       {{validEvaluator : ValidStmtEvaluator evaluator latticeInterpretationˡ}} (dummy : ⊤) where
-                using ()
+            open ValidStmtEvaluator validEvaluator
-                renaming
-                    ( ⟦_⟧ to ⟦_⟧ˡ
-                    ; ⟦⟧-respects-≈ to ⟦⟧ˡ-respects-≈ˡ
-                    ; ⟦⟧-⊔-∨ to ⟦⟧ˡ-⊔ˡ-∨
-                    )
 
-            ⟦_⟧ᵛ : VariableValues → Env → Set
+            eval-fold-valid : ∀ {s bss vs ρ₁ ρ₂} → ρ₁ , bss ⇒ᵇˢ ρ₂ → ⟦ vs ⟧ᵛ ρ₁ → ⟦ foldl (flip (eval s)) vs bss ⟧ᵛ ρ₂
-            ⟦_⟧ᵛ vs ρ = ∀ {k l} → (k , l) ∈ᵛ vs → ∀ {v} → (k , v) Language.∈ ρ → ⟦ l ⟧ˡ v
+            eval-fold-valid {_} [] ⟦vs⟧ρ = ⟦vs⟧ρ
+            eval-fold-valid {s} {bs ∷ bss'} {vs} {ρ₁} {ρ₂} (ρ₁,bs⇒ρ ∷ ρ,bss'⇒ρ₂) ⟦vs⟧ρ₁ =
+                eval-fold-valid
+                    {bss = bss'} {eval s bs vs} ρ,bss'⇒ρ₂
+                    (valid ρ₁,bs⇒ρ ⟦vs⟧ρ₁)
 
-            ⟦⊥ᵛ⟧ᵛ∅ : ⟦ ⊥ᵛ ⟧ᵛ []
+            updateVariablesForState-matches : ∀ {s sv ρ₁ ρ₂} → ρ₁ , (code s) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s sv ⟧ᵛ ρ₁ → ⟦ updateVariablesForState s sv ⟧ᵛ ρ₂
-            ⟦⊥ᵛ⟧ᵛ∅ _ ()
+            updateVariablesForState-matches = eval-fold-valid
 
-            ⟦⟧ᵛ-respects-≈ᵛ : ∀ {vs₁ vs₂ : VariableValues} → vs₁ ≈ᵛ vs₂ → ⟦ vs₁ ⟧ᵛ ⇒ ⟦ vs₂ ⟧ᵛ
+            updateAll-matches : ∀ {s sv ρ₁ ρ₂} → ρ₁ , (code s) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s sv ⟧ᵛ ρ₁ → ⟦ variablesAt s (updateAll sv) ⟧ᵛ ρ₂
-            ⟦⟧ᵛ-respects-≈ᵛ {m₁ , _} {m₂ , _}
+            updateAll-matches {s} {sv} ρ₁,bss⇒ρ₂ ⟦vs⟧ρ₁
-                            (m₁⊆m₂ , m₂⊆m₁) ρ ⟦vs₁⟧ρ {k} {l} k,l∈m₂ {v} k,v∈ρ =
+                rewrite variablesAt-updateAll s sv =
-                let
+                updateVariablesForState-matches {s} {sv} ρ₁,bss⇒ρ₂ ⟦vs⟧ρ₁
-                    (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
 
-            ⟦⟧ᵛ-⊔ᵛ-∨ : ∀ {vs₁ vs₂ : VariableValues} → (⟦ vs₁ ⟧ᵛ ∨ ⟦ vs₂ ⟧ᵛ) ⇒ ⟦ vs₁ ⊔ᵛ vs₂ ⟧ᵛ
+            stepTrace : ∀ {s₁ ρ₁ ρ₂} → ⟦ joinForKey s₁ result ⟧ᵛ ρ₁ → ρ₁ , (code s₁) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s₁ result ⟧ᵛ ρ₂
-            ⟦⟧ᵛ-⊔ᵛ-∨ {vs₁} {vs₂} ρ ⟦vs₁⟧ρ∨⟦vs₂⟧ρ {k} {l} k,l∈vs₁₂ {v} k,v∈ρ
+            stepTrace {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ ρ₁,bss⇒ρ₂ =
-                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) =
-                ⟦⟧ᵛ-⊔ᵛ-∨ {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
-
-            module WithValidity (interpretationValidˡ : InterpretationValid) where
-
-                updateVariablesFromStmt-matches : ∀ {bs vs ρ₁ ρ₂} → ρ₁ , bs ⇒ᵇ ρ₂ → ⟦ vs ⟧ᵛ ρ₁ → ⟦ updateVariablesFromStmt bs vs ⟧ᵛ ρ₂
-                updateVariablesFromStmt-matches {_} {vs} {ρ₁} {ρ₁} (⇒ᵇ-noop ρ₁) ⟦vs⟧ρ₁ = ⟦vs⟧ρ₁
-                updateVariablesFromStmt-matches {_} {vs} {ρ₁} {_} (⇒ᵇ-← ρ₁ k e v ρ,e⇒v) ⟦vs⟧ρ₁ {k'} {l} k',l∈vs' {v'} k',v'∈ρ₂
-                    with k ≟ˢ k' | k',v'∈ρ₂
-                ...   | yes refl | here _ v _
-                        rewrite updateVariablesFromExpression-k∈ks-≡ k e {l = vs} (Any.here refl) k',l∈vs' =
-                        interpretationValidˡ ρ,e⇒v ⟦vs⟧ρ₁
-                ...   | yes k≡k' | there _ _ _ _ _ k'≢k _ = ⊥-elim (k'≢k (sym k≡k'))
-                ...   | no k≢k' | here _ _ _ = ⊥-elim (k≢k' refl)
-                ...   | no k≢k'  | there _ _ _ _ _ _ k',v'∈ρ₁ =
-                        let
-                            k'∉[k] = (λ { (Any.here refl) → k≢k' refl })
-                            k',l∈vs = updateVariablesFromExpression-k∉ks-backward k e {l = vs} k'∉[k] k',l∈vs'
-                        in
-                            ⟦vs⟧ρ₁ k',l∈vs k',v'∈ρ₁
-
-                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⟧ρ₁)
-
-                updateVariablesForState-matches : ∀ {s sv ρ₁ ρ₂} → ρ₁ , (code s) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s sv ⟧ᵛ ρ₁ → ⟦ updateVariablesForState s sv ⟧ᵛ ρ₂
-                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 =
-                    updateVariablesForState-matches {s} {sv} ρ₁,bss⇒ρ₂ ⟦vs⟧ρ₁
-
-
-                stepTrace : ∀ {s₁ ρ₁ ρ₂} → ⟦ joinForKey s₁ result ⟧ᵛ ρ₁ → ρ₁ , (code s₁) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s₁ result ⟧ᵛ ρ₂
-                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)
-                        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-edge {ρ₂ = ρ} {idx₂ = s} ρ₁,bss⇒ρ s₁→s₂ tr) =
                     let
-                        ⟦result-s₁⟧ρ =
+                        -- I'd use rewrite, but Agda gets a memory overflow (?!).
-                            stepTrace {s₁} {ρ₁} {ρ} ⟦joinForKey-s₁⟧ρ₁ ρ₁,bss⇒ρ
+                        ⟦joinAll-result⟧ρ₁ =
-                        s₁∈incomingStates =
+                            subst (λ vs → ⟦ vs ⟧ᵛ ρ₁)
-                            []-∈ result (edge⇒incoming s₁→s₂)
+                                  (sym (variablesAt-joinAll s₁ result))
-                                        (variablesAt-∈ s₁ result)
+                                  ⟦joinForKey-s₁⟧ρ₁
-                        ⟦joinForKey-s⟧ρ =
+                        ⟦analyze-result⟧ρ₂ =
-                            ⟦⟧ᵛ-foldr ⟦result-s₁⟧ρ s₁∈incomingStates
+                            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
-                        walkTrace ⟦joinForKey-s⟧ρ tr
+                        ⟦⟧ᵛ-respects-≈ᵛ {variablesAt s₁ (updateAll (joinAll result))} {variablesAt s₁ result} (analyze-s₁≈s₁) ρ₂ ⟦analyze-result⟧ρ₂
 
-                joinForKey-initialState-⊥ᵛ : joinForKey initialState result ≡ ⊥ᵛ
+            walkTrace : ∀ {s₁ s₂ ρ₁ ρ₂} → ⟦ joinForKey s₁ result ⟧ᵛ ρ₁ → Trace {graph} s₁ s₂ ρ₁ ρ₂ → ⟦ variablesAt s₂ result ⟧ᵛ ρ₂
-                joinForKey-initialState-⊥ᵛ = cong (λ ins → foldr _⊔ᵛ_ ⊥ᵛ (result [ ins ])) initialState-pred-∅
+            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
 
-                ⟦joinAll-initialState⟧ᵛ∅ : ⟦ joinForKey initialState result ⟧ᵛ []
+            joinForKey-initialState-⊥ᵛ : joinForKey initialState result ≡ ⊥ᵛ
-                ⟦joinAll-initialState⟧ᵛ∅ = subst (λ vs → ⟦ vs ⟧ᵛ []) (sym joinForKey-initialState-⊥ᵛ) ⟦⊥ᵛ⟧ᵛ∅
+            joinForKey-initialState-⊥ᵛ = cong (λ ins → foldr _⊔ᵛ_ ⊥ᵛ (result [ ins ])) initialState-pred-∅
 
-                analyze-correct : ∀ {ρ : Env} → [] , rootStmt ⇒ˢ ρ → ⟦ variablesAt finalState result ⟧ᵛ ρ
+            ⟦joinAll-initialState⟧ᵛ∅ : ⟦ joinForKey initialState result ⟧ᵛ []
-                analyze-correct {ρ} ∅,s⇒ρ = walkTrace {initialState} {finalState} {[]} {ρ} ⟦joinAll-initialState⟧ᵛ∅ (trace ∅,s⇒ρ)
+            ⟦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⇒ρ)
+
+    open WithStmtEvaluator using (result; analyze; result≈analyze-result) public
+    open WithStmtEvaluator.WithValidInterpretation using (analyze-correct) public

Analysis/Forward/Adapters.agda

@@ -0,0 +1,100 @@
+open import Language hiding (_[_])
+open import Lattice
+
+module Analysis.Forward.Adapters
+    (L : Set) {h}
+    {_≈ˡ_ : L → L → Set} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L}
+    {{isFiniteHeightLatticeˡ : IsFiniteHeightLattice L h _≈ˡ_ _⊔ˡ_ _⊓ˡ_}}
+    {{≈ˡ-dec : IsDecidable _≈ˡ_}}
+    (prog : Program) where
+
+open import Analysis.Forward.Lattices L prog
+open import Analysis.Forward.Evaluation L prog
+
+open import Data.Empty using (⊥-elim)
+open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
+open import Data.Product using (_,_)
+open import Data.List using (_∷_; []; foldr; foldl)
+open import Data.List.Relation.Unary.Any as Any using ()
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym; subst)
+open import Relation.Nullary using (yes; no)
+open import Function using (_∘_; flip)
+
+open IsFiniteHeightLattice isFiniteHeightLatticeˡ
+    using ()
+    renaming
+        ( isLattice to isLatticeˡ
+        ; _≼_ to _≼ˡ_
+        )
+open Program prog
+
+-- Now, allow StmtEvaluators to be auto-constructed from ExprEvaluators.
+module ExprToStmtAdapter {{ exprEvaluator : ExprEvaluator }} where
+    open ExprEvaluator exprEvaluator
+        using ()
+        renaming
+            ( eval to evalᵉ
+            ; eval-Monoʳ to evalᵉ-Monoʳ
+            )
+
+    -- For a particular evaluation function, we need to perform an evaluation
+    -- for an assignment, and update the corresponding key. Use Exercise 4.26's
+    -- generalized update to set the single key's value.
+    private module _ (k : String) (e : Expr) where
+        open VariableValuesFiniteMap.GeneralizedUpdate {{isLatticeᵛ}} (λ x → x) (λ a₁≼a₂ → a₁≼a₂) (λ _ → evalᵉ e) (λ _ {vs₁} {vs₂} vs₁≼vs₂ → evalᵉ-Monoʳ e {vs₁} {vs₂} vs₁≼vs₂) (k ∷ [])
+            using ()
+            renaming
+                ( f' to updateVariablesFromExpression
+                ; f'-Monotonic to updateVariablesFromExpression-Mono
+                ; f'-k∈ks-≡ to updateVariablesFromExpression-k∈ks-≡
+                ; f'-k∉ks-backward to updateVariablesFromExpression-k∉ks-backward
+                )
+            public
+
+    -- The per-state update function makes use of the single-key setter,
+    -- updateVariablesFromExpression, for the case where the statement
+    -- is an assignment.
+    --
+    -- This per-state function adjusts the variables in that state,
+    -- also monotonically; we derive the for-each-state update from
+    -- the Exercise 4.26 again.
+
+    evalᵇ : State → BasicStmt → VariableValues → VariableValues
+    evalᵇ _ (k ← e) vs = updateVariablesFromExpression k e vs
+    evalᵇ _ noop vs = vs
+
+    evalᵇ-Monoʳ : ∀ (s : State) (bs : BasicStmt) → Monotonic _≼ᵛ_ _≼ᵛ_ (evalᵇ s bs)
+    evalᵇ-Monoʳ _ (k ← e) {vs₁} {vs₂} vs₁≼vs₂ = updateVariablesFromExpression-Mono k e {vs₁} {vs₂} vs₁≼vs₂
+    evalᵇ-Monoʳ _ noop vs₁≼vs₂ = vs₁≼vs₂
+
+    instance
+        stmtEvaluator : StmtEvaluator
+        stmtEvaluator = record { eval = evalᵇ ; eval-Monoʳ = evalᵇ-Monoʳ }
+
+    -- Moreover, correct StmtEvaluators can be constructed from correct
+    -- ExprEvaluators.
+    module _ {{latticeInterpretationˡ : LatticeInterpretation isLatticeˡ}}
+             {{isValid : ValidExprEvaluator exprEvaluator latticeInterpretationˡ}} where
+        open ValidExprEvaluator isValid using () renaming (valid to validᵉ)
+
+        evalᵇ-valid : ∀ {s vs ρ₁ ρ₂ bs} → ρ₁ , bs ⇒ᵇ ρ₂ → ⟦ vs ⟧ᵛ ρ₁ → ⟦ evalᵇ s bs vs ⟧ᵛ ρ₂
+        evalᵇ-valid {_} {vs} {ρ₁} {ρ₁} {_} (⇒ᵇ-noop ρ₁) ⟦vs⟧ρ₁ = ⟦vs⟧ρ₁
+        evalᵇ-valid {_} {vs} {ρ₁} {_} {_} (⇒ᵇ-← ρ₁ k e v ρ,e⇒v) ⟦vs⟧ρ₁ {k'} {l} k',l∈vs' {v'} k',v'∈ρ₂
+            with k ≟ˢ k' | k',v'∈ρ₂
+        ...   | yes refl | here _ v _
+                rewrite updateVariablesFromExpression-k∈ks-≡ k e {l = vs} (Any.here refl) k',l∈vs' =
+                validᵉ ρ,e⇒v ⟦vs⟧ρ₁
+        ...   | yes k≡k' | there _ _ _ _ _ k'≢k _ = ⊥-elim (k'≢k (sym k≡k'))
+        ...   | no k≢k' | here _ _ _ = ⊥-elim (k≢k' refl)
+        ...   | no k≢k'  | there _ _ _ _ _ _ k',v'∈ρ₁ =
+                let
+                    k'∉[k] = (λ { (Any.here refl) → k≢k' refl })
+                    k',l∈vs = updateVariablesFromExpression-k∉ks-backward k e {l = vs} k'∉[k] k',l∈vs'
+                in
+                    ⟦vs⟧ρ₁ k',l∈vs k',v'∈ρ₁
+
+        instance
+            validStmtEvaluator : ValidStmtEvaluator stmtEvaluator latticeInterpretationˡ
+            validStmtEvaluator = record
+                { valid = λ {a} {b} {c} {d} →  evalᵇ-valid {a} {b} {c} {d}
+                }

Analysis/Forward/Evaluation.agda

@@ -0,0 +1,66 @@
+open import Language hiding (_[_])
+open import Lattice
+
+module Analysis.Forward.Evaluation
+    (L : Set) {h}
+    {_≈ˡ_ : L → L → Set} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L}
+    {{isFiniteHeightLatticeˡ : IsFiniteHeightLattice L h _≈ˡ_ _⊔ˡ_ _⊓ˡ_}}
+    {{≈ˡ-dec : IsDecidable _≈ˡ_}}
+    (prog : Program) where
+
+open import Analysis.Forward.Lattices L prog
+open import Data.Product using (_,_)
+
+open IsFiniteHeightLattice isFiniteHeightLatticeˡ
+    using ()
+    renaming
+        ( isLattice to isLatticeˡ
+        ; _≼_ to _≼ˡ_
+        )
+open Program prog
+
+-- The "full" version of the analysis ought to define a function
+-- that analyzes each basic statement. For some analyses, the state ID
+-- is used as part of the lattice, so include it here.
+record StmtEvaluator : Set where
+    field
+        eval : State → BasicStmt → VariableValues → VariableValues
+        eval-Monoʳ : ∀ (s : State) (bs : BasicStmt) → Monotonic _≼ᵛ_ _≼ᵛ_ (eval s bs)
+
+-- For some "simpler" analyes, all we need to do is analyze the expressions.
+-- For that purpose, provide a simpler evaluator type.
+record ExprEvaluator : Set where
+    field
+        eval : Expr → VariableValues → L
+        eval-Monoʳ : ∀ (e : Expr) → Monotonic _≼ᵛ_ _≼ˡ_ (eval e)
+
+-- Evaluators have a notion of being "valid", in which the (symbolic)
+-- manipulations on lattice elements they perform match up with
+-- the semantics. Define what it means to be valid for statement and
+-- expression-based evaluators. Define "IsValidExprEvaluator"
+-- and "IsValidStmtEvaluator" standalone so that users can use them
+-- in their type expressions.
+
+module _ {{evaluator : ExprEvaluator}} {{interpretation : LatticeInterpretation isLatticeˡ}} where
+    open ExprEvaluator evaluator
+    open LatticeInterpretation interpretation
+
+    IsValidExprEvaluator : Set
+    IsValidExprEvaluator = ∀ {vs ρ e v} → ρ , e ⇒ᵉ v → ⟦ vs ⟧ᵛ ρ → ⟦ eval e vs ⟧ˡ v
+
+record ValidExprEvaluator (evaluator : ExprEvaluator)
+                          (interpretation : LatticeInterpretation isLatticeˡ) : Set₁ where
+    field
+        valid : IsValidExprEvaluator {{evaluator}} {{interpretation}}
+
+module _ {{evaluator : StmtEvaluator}} {{interpretation : LatticeInterpretation isLatticeˡ}} where
+    open StmtEvaluator evaluator
+    open LatticeInterpretation interpretation
+
+    IsValidStmtEvaluator : Set
+    IsValidStmtEvaluator = ∀ {s vs ρ₁ ρ₂ bs} → ρ₁ , bs ⇒ᵇ ρ₂ → ⟦ vs ⟧ᵛ ρ₁ → ⟦ eval s bs vs ⟧ᵛ ρ₂
+
+record ValidStmtEvaluator (evaluator : StmtEvaluator)
+                           (interpretation : LatticeInterpretation isLatticeˡ) : Set₁ where
+    field
+        valid : IsValidStmtEvaluator {{evaluator}} {{interpretation}}

Analysis/Forward/Lattices.agda

@@ -0,0 +1,195 @@
+open import Language hiding (_[_])
+open import Lattice
+
+module Analysis.Forward.Lattices
+    (L : Set) {h}
+    {_≈ˡ_ : L → L → Set} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L}
+    {{isFiniteHeightLatticeˡ : IsFiniteHeightLattice L h _≈ˡ_ _⊔ˡ_ _⊓ˡ_}}
+    {{≈ˡ-Decidable : IsDecidable _≈ˡ_}}
+    (prog : Program) where
+
+open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
+open import Data.Product using (proj₁; proj₂; _,_)
+open import Data.Sum using (inj₁; inj₂)
+open import Data.List using (List; _∷_; []; foldr)
+open import Data.List.Membership.Propositional using () renaming (_∈_ to _∈ˡ_)
+open import Data.List.Relation.Unary.Any as Any using ()
+open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+open import Utils using (Pairwise; _⇒_; _∨_; it)
+
+open IsFiniteHeightLattice isFiniteHeightLatticeˡ
+    using ()
+    renaming
+        ( isLattice to isLatticeˡ
+        ; fixedHeight to fixedHeightˡ
+        ; ≈-sym to ≈ˡ-sym
+        )
+open Program prog
+
+import Lattice.FiniteMap
+import Chain
+
+instance
+    ≡-Decidable-String = record { R-dec = _≟ˢ_ }
+    ≡-Decidable-State = record { R-dec = _≟_ }
+
+-- The variable -> abstract value (e.g. sign) map is a finite value-map
+-- with keys strings. Use a bundle to avoid explicitly specifying operators.
+-- It's helpful to export these via 'public' since consumers tend to
+-- use various variable lattice operations.
+module VariableValuesFiniteMap = Lattice.FiniteMap String L vars
+open VariableValuesFiniteMap
+    using ()
+    renaming
+        ( FiniteMap to VariableValues
+        ; isLattice to isLatticeᵛ
+        ; _≈_ to _≈ᵛ_
+        ; _⊔_ to _⊔ᵛ_
+        ; _≼_ to _≼ᵛ_
+        ; ≈-Decidable to ≈ᵛ-Decidable
+        ; _∈_ to _∈ᵛ_
+        ; _∈k_ to _∈kᵛ_
+        ; _updating_via_ to _updatingᵛ_via_
+        ; locate to locateᵛ
+        ; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵛ≼m₂[k]ᵛ
+        ; ∈k-dec to ∈k-decᵛ
+        ; all-equal-keys to all-equal-keysᵛ
+        ; Provenance-union to Provenance-unionᵛ
+        ; ⊔-Monotonicˡ to ⊔ᵛ-Monotonicˡ
+        ; ⊔-Monotonicʳ to ⊔ᵛ-Monotonicʳ
+        ; ⊔-idemp to ⊔ᵛ-idemp
+        )
+    public
+open VariableValuesFiniteMap.FixedHeight vars-Unique
+    using ()
+    renaming
+        ( isFiniteHeightLattice to isFiniteHeightLatticeᵛ
+        ; fixedHeight to fixedHeightᵛ
+        ; ⊥-contains-bottoms to ⊥ᵛ-contains-bottoms
+        )
+    public
+
+⊥ᵛ = Chain.Height.⊥ fixedHeightᵛ
+
+-- Finally, the map we care about is (state -> (variables -> value)). Bring that in.
+module StateVariablesFiniteMap = Lattice.FiniteMap State VariableValues states
+open StateVariablesFiniteMap
+    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 _≼ᵐ_
+        ; ≈-Decidable to ≈ᵐ-Decidable
+        ; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ
+        ; ≈-sym to ≈ᵐ-sym
+        )
+    public
+open StateVariablesFiniteMap.FixedHeight states-Unique
+    using ()
+    renaming
+        ( isFiniteHeightLattice to isFiniteHeightLatticeᵐ
+        )
+    public
+
+-- 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))
+
+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₂ =
+    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
+--
+--    L₁ → (A → L₂)
+--
+-- Construction, with L₁ = (A → L₂), and f = id
+
+joinForKey : State → StateVariables → VariableValues
+joinForKey k states = foldr _⊔ᵛ_ ⊥ᵛ (states [ incoming k ])
+
+-- The per-key join is made up of map key accesses (which are monotonic)
+-- and folds using the join operation (also monotonic)
+
+joinForKey-Mono : ∀ (k : State) → Monotonic _≼ᵐ_ _≼ᵛ_ (joinForKey k)
+joinForKey-Mono k {fm₁} {fm₂} fm₁≼fm₂ =
+    foldr-Mono it it (fm₁ [ incoming k ]) (fm₂ [ incoming k ]) _⊔ᵛ_ ⊥ᵛ ⊥ᵛ
+               (m₁≼m₂⇒m₁[ks]≼m₂[ks] fm₁ fm₂ (incoming k) fm₁≼fm₂)
+               (⊔ᵛ-idemp ⊥ᵛ) ⊔ᵛ-Monotonicʳ ⊔ᵛ-Monotonicˡ
+
+-- The name f' comes from the formulation of Exercise 4.26.
+open StateVariablesFiniteMap.GeneralizedUpdate {{isLatticeᵐ}} (λ x → x) (λ a₁≼a₂ → a₁≼a₂) joinForKey joinForKey-Mono states
+    using ()
+    renaming
+        ( f' to joinAll
+        ; f'-Monotonic to joinAll-Mono
+        ; f'-k∈ks-≡ to joinAll-k∈ks-≡
+        )
+    public
+
+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
+
+-- Elements of the lattice type L describe individual variables. What
+-- exactly each lattice element says about the variable is defined
+-- by a LatticeInterpretation element. We've now constructed the
+-- (Variable → L) lattice, which describes states, and we need to lift
+-- the "meaning" of the element lattice to a descriptions of states.
+module _ {{latticeInterpretationˡ : LatticeInterpretation isLatticeˡ}} where
+    open LatticeInterpretation latticeInterpretationˡ
+        using ()
+        renaming
+            ( ⟦_⟧ to ⟦_⟧ˡ
+            ; ⟦⟧-respects-≈ to ⟦⟧ˡ-respects-≈ˡ
+            ; ⟦⟧-⊔-∨ to ⟦⟧ˡ-⊔ˡ-∨
+            )
+        public
+
+    ⟦_⟧ᵛ : 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
+
+    ⟦⟧ᵛ-⊔ᵛ-∨ : ∀ {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) =
+        ⟦⟧ᵛ-⊔ᵛ-∨ {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'))

Analysis/Sign.agda

@@ -7,13 +7,16 @@ open import Data.Sum using (inj₁; inj₂)
 open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Unit using (⊤; tt)
 open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_)
+open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; subst)
 open import Relation.Nullary using (¬_; yes; no)
 
 open import Language
 open import Lattice
+open import Equivalence
 open import Showable using (Showable; show)
 open import Utils using (_⇒_; _∧_; _∨_)
+open import Analysis.Utils using (eval-combine₂)
 import Analysis.Forward
 
 data Sign : Set where
@@ -32,7 +35,7 @@ instance
         }
 
 -- g for siGn; s is used for strings and i is not very descriptive.
-_≟ᵍ_ : IsDecidable (_≡_ {_} {Sign})
+_≟ᵍ_ : Decidable (_≡_ {_} {Sign})
 _≟ᵍ_ + + = yes refl
 _≟ᵍ_ + - = no (λ ())
 _≟ᵍ_ + 0ˢ = no (λ ())
@@ -43,12 +46,22 @@ _≟ᵍ_ 0ˢ + = no (λ ())
 _≟ᵍ_ 0ˢ - = no (λ ())
 _≟ᵍ_ 0ˢ 0ˢ = yes refl
 
+instance
+    ≡-equiv : IsEquivalence Sign _≡_
+    ≡-equiv = record
+        { ≈-refl = refl
+        ; ≈-sym = sym
+        ; ≈-trans = trans
+        }
+
+    ≡-Decidable-Sign : IsDecidable {_} {Sign} _≡_
+    ≡-Decidable-Sign = record { R-dec = _≟ᵍ_ }
+
 -- embelish 'sign' with a top and bottom element.
-open import Lattice.AboveBelow Sign _≡_ (record { ≈-refl = refl; ≈-sym = sym; ≈-trans = trans }) _≟ᵍ_ as AB
+open import Lattice.AboveBelow Sign _ as AB
     using ()
     renaming
         ( AboveBelow to SignLattice
-        ; ≈-dec to ≈ᵍ-dec
         ; ⊥ to ⊥ᵍ
         ; ⊤ to ⊤ᵍ
         ; [_] to [_]ᵍ
@@ -62,15 +75,11 @@ open import Lattice.AboveBelow Sign _≡_ (record { ≈-refl = refl; ≈-sym = s
 open AB.Plain 0ˢ using ()
     renaming
         ( isLattice to isLatticeᵍ
-        ; fixedHeight to fixedHeightᵍ
+        ; isFiniteHeightLattice to isFiniteHeightLatticeᵍ
         ; _≼_ to _≼ᵍ_
         ; _⊔_ to _⊔ᵍ_
         ; _⊓_ to _⊓ᵍ_
-        )
+        ; ≼-trans to ≼ᵍ-trans
-
-open IsLattice isLatticeᵍ using ()
-    renaming
-        ( ≼-trans to ≼ᵍ-trans
         )
 
 plus : SignLattice → SignLattice → SignLattice
@@ -93,6 +102,9 @@ plus [ 0ˢ ]ᵍ [ 0ˢ ]ᵍ = [ 0ˢ ]ᵍ
 postulate plus-Monoˡ : ∀ (s₂ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ_ (λ s₁ → plus s₁ s₂)
 postulate plus-Monoʳ : ∀ (s₁ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ_ (plus s₁)
 
+plus-Mono₂ : Monotonic₂ _≼ᵍ_ _≼ᵍ_ _≼ᵍ_ plus
+plus-Mono₂ = (plus-Monoˡ , plus-Monoʳ)
+
 minus : SignLattice → SignLattice → SignLattice
 minus ⊥ᵍ _ = ⊥ᵍ
 minus _ ⊥ᵍ = ⊥ᵍ
@@ -111,6 +123,9 @@ minus [ 0ˢ ]ᵍ [ 0ˢ ]ᵍ = [ 0ˢ ]ᵍ
 postulate minus-Monoˡ : ∀ (s₂ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ_ (λ s₁ → minus s₁ s₂)
 postulate minus-Monoʳ : ∀ (s₁ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ_ (minus s₁)
 
+minus-Mono₂ : Monotonic₂ _≼ᵍ_ _≼ᵍ_ _≼ᵍ_ minus
+minus-Mono₂ = (minus-Monoˡ , minus-Monoʳ)
+
 ⟦_⟧ᵍ : SignLattice → Value → Set
 ⟦_⟧ᵍ ⊥ᵍ _ = ⊥
 ⟦_⟧ᵍ ⊤ᵍ _ = ⊤
@@ -159,19 +174,21 @@ s₁≢s₂⇒¬s₁∧s₂ { - } { - } +≢+ _ = ⊥-elim (+≢+ refl)
 ⟦⟧ᵍ-⊓ᵍ-∧ {[ g₁ ]ᵍ} {⊥ᵍ} x (_ , bot) = bot
 ⟦⟧ᵍ-⊓ᵍ-∧ {[ g₁ ]ᵍ} {⊤ᵍ} x (px₁ , _) = px₁
 
-latticeInterpretationᵍ : LatticeInterpretation isLatticeᵍ
+instance
-latticeInterpretationᵍ = record
+    latticeInterpretationᵍ : LatticeInterpretation isLatticeᵍ
-    { ⟦_⟧ = ⟦_⟧ᵍ
+    latticeInterpretationᵍ = record
-    ; ⟦⟧-respects-≈ = ⟦⟧ᵍ-respects-≈ᵍ
+        { ⟦_⟧ = ⟦_⟧ᵍ
-    ; ⟦⟧-⊔-∨ = ⟦⟧ᵍ-⊔ᵍ-∨
+        ; ⟦⟧-respects-≈ = ⟦⟧ᵍ-respects-≈ᵍ
-    ; ⟦⟧-⊓-∧ = ⟦⟧ᵍ-⊓ᵍ-∧
+        ; ⟦⟧-⊔-∨ = ⟦⟧ᵍ-⊔ᵍ-∨
-    }
+        ; ⟦⟧-⊓-∧ = ⟦⟧ᵍ-⊓ᵍ-∧
+        }
 
 module WithProg (prog : Program) where
     open Program prog
 
-    module ForwardWithProg = Analysis.Forward.WithProg (record { isLattice = isLatticeᵍ; fixedHeight = fixedHeightᵍ }) ≈ᵍ-dec prog
+    open import Analysis.Forward.Lattices SignLattice prog
-    open ForwardWithProg
+    open import Analysis.Forward.Evaluation SignLattice prog
+    open import Analysis.Forward.Adapters SignLattice prog
 
     eval : ∀ (e : Expr) → VariableValues → SignLattice
     eval (e₁ + e₂) vs = plus (eval e₁ vs) (eval e₂ vs)
@@ -183,32 +200,16 @@ module WithProg (prog : Program) where
     eval (# 0) _ = [ 0ˢ ]ᵍ
     eval (# (suc n')) _ = [ + ]ᵍ
 
-    eval-Mono : ∀ (e : Expr) → Monotonic _≼ᵛ_ _≼ᵍ_ (eval e)
+    eval-Monoʳ : ∀ (e : Expr) → Monotonic _≼ᵛ_ _≼ᵍ_ (eval e)
-    eval-Mono (e₁ + e₂) {vs₁} {vs₂} vs₁≼vs₂ =
+    eval-Monoʳ (e₁ + e₂) {vs₁} {vs₂} vs₁≼vs₂ =
-        let
+        eval-combine₂ (λ {x} {y} {z} →  ≼ᵍ-trans {x} {y} {z})
-            -- TODO: can this be done with less boilerplate?
+                      plus plus-Mono₂ {o₁ = eval e₁ vs₁}
-            g₁vs₁ = eval e₁ vs₁
+                      (eval-Monoʳ e₁ vs₁≼vs₂) (eval-Monoʳ e₂ vs₁≼vs₂)
-            g₂vs₁ = eval e₂ vs₁
+    eval-Monoʳ (e₁ - e₂) {vs₁} {vs₂} vs₁≼vs₂ =
-            g₁vs₂ = eval e₁ vs₂
+        eval-combine₂ (λ {x} {y} {z} →  ≼ᵍ-trans {x} {y} {z})
-            g₂vs₂ = eval e₂ vs₂
+                      minus minus-Mono₂ {o₁ = eval e₁ vs₁}
-        in
+                      (eval-Monoʳ e₁ vs₁≼vs₂) (eval-Monoʳ e₂ vs₁≼vs₂)
-            ≼ᵍ-trans
+    eval-Monoʳ (` k) {vs₁@((kvs₁ , _) , _)} {vs₂@((kvs₂ , _), _)} vs₁≼vs₂
-                {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₁ {vs₁} {vs₂} vs₁≼vs₂))
-                (plus-Monoʳ g₁vs₂ {g₂vs₁} {g₂vs₂} (eval-Mono e₂ {vs₁} {vs₂} vs₁≼vs₂))
-    eval-Mono (e₁ - e₂) {vs₁} {vs₂} vs₁≼vs₂ =
-        let
-            -- TODO: here too -- can this be done with less boilerplate?
-            g₁vs₁ = eval e₁ vs₁
-            g₂vs₁ = eval e₂ vs₁
-            g₁vs₂ = eval e₁ vs₂
-            g₂vs₂ = eval e₂ 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₁ {vs₁} {vs₂} vs₁≼vs₂))
-                (minus-Monoʳ g₁vs₂ {g₂vs₁} {g₂vs₂} (eval-Mono e₂ {vs₁} {vs₂} vs₁≼vs₂))
-    eval-Mono (` k) {vs₁@((kvs₁ , _) , _)} {vs₂@((kvs₂ , _), _)} vs₁≼vs₂
         with ∈k-decᵛ k kvs₁ | ∈k-decᵛ k kvs₂
     ...   | yes k∈kvs₁ | yes k∈kvs₂ =
             let
@@ -219,17 +220,15 @@ module WithProg (prog : Program) where
     ...   | yes k∈kvs₁ | no k∉kvs₂ = ⊥-elim (k∉kvs₂ (subst (λ l → k ∈ˡ l) (all-equal-keysᵛ vs₁ vs₂) k∈kvs₁))
     ...   | no k∉kvs₁ | yes k∈kvs₂ = ⊥-elim (k∉kvs₁ (subst (λ l → k ∈ˡ l) (all-equal-keysᵛ vs₂ vs₁) k∈kvs₂))
     ...   | no k∉kvs₁ | no k∉kvs₂ = IsLattice.≈-refl isLatticeᵍ
-    eval-Mono (# 0) _ = ≈ᵍ-refl
+    eval-Monoʳ (# 0) _ = ≈ᵍ-refl
-    eval-Mono (# (suc n')) _ = ≈ᵍ-refl
+    eval-Monoʳ (# (suc n')) _ = ≈ᵍ-refl
 
-    module ForwardWithEval = ForwardWithProg.WithEvaluator eval eval-Mono
+    instance
-    open ForwardWithEval using (result)
+        SignEval : ExprEvaluator
+        SignEval = record { eval = eval; eval-Monoʳ = eval-Monoʳ }
 
     -- For debugging purposes, print out the result.
-    output = show result
+    output = show (Analysis.Forward.WithProg.result SignLattice prog)
-
-    module ForwardWithInterp = ForwardWithEval.WithInterpretation latticeInterpretationᵍ
-    open ForwardWithInterp using (⟦_⟧ᵛ; InterpretationValid)
 
     -- This should have fewer cases -- the same number as the actual 'plus' above.
     -- But agda only simplifies on first argument, apparently, so we are stuck
@@ -281,16 +280,20 @@ module WithProg (prog : Program) where
     minus-valid {[ 0ˢ ]ᵍ} {[ 0ˢ ]ᵍ} refl refl = refl
     minus-valid {[ 0ˢ ]ᵍ} {⊤ᵍ} _ _ = tt
 
-    eval-Valid : InterpretationValid
+    eval-valid : IsValidExprEvaluator
-    eval-Valid (⇒ᵉ-+ ρ e₁ e₂ z₁ z₂ ρ,e₁⇒z₁ ρ,e₂⇒z₂) ⟦vs⟧ρ =
+    eval-valid (⇒ᵉ-+ ρ e₁ e₂ z₁ z₂ ρ,e₁⇒z₁ ρ,e₂⇒z₂) ⟦vs⟧ρ =
-        plus-valid (eval-Valid ρ,e₁⇒z₁ ⟦vs⟧ρ) (eval-Valid ρ,e₂⇒z₂ ⟦vs⟧ρ)
+        plus-valid (eval-valid ρ,e₁⇒z₁ ⟦vs⟧ρ) (eval-valid ρ,e₂⇒z₂ ⟦vs⟧ρ)
-    eval-Valid (⇒ᵉ-- ρ e₁ e₂ z₁ z₂ ρ,e₁⇒z₁ ρ,e₂⇒z₂) ⟦vs⟧ρ =
+    eval-valid (⇒ᵉ-- ρ e₁ e₂ z₁ z₂ ρ,e₁⇒z₁ ρ,e₂⇒z₂) ⟦vs⟧ρ =
-        minus-valid (eval-Valid ρ,e₁⇒z₁ ⟦vs⟧ρ) (eval-Valid ρ,e₂⇒z₂ ⟦vs⟧ρ)
+        minus-valid (eval-valid ρ,e₁⇒z₁ ⟦vs⟧ρ) (eval-valid ρ,e₂⇒z₂ ⟦vs⟧ρ)
-    eval-Valid {vs} (⇒ᵉ-Var ρ x v x,v∈ρ) ⟦vs⟧ρ
+    eval-valid {vs} (⇒ᵉ-Var ρ x v x,v∈ρ) ⟦vs⟧ρ
         with ∈k-decᵛ x (proj₁ (proj₁ vs))
     ...   | yes x∈kvs = ⟦vs⟧ρ (proj₂ (locateᵛ {x} {vs} x∈kvs)) x,v∈ρ
     ...   | no x∉kvs = tt
-    eval-Valid (⇒ᵉ-ℕ ρ 0) _ = refl
+    eval-valid (⇒ᵉ-ℕ ρ 0) _ = refl
-    eval-Valid (⇒ᵉ-ℕ ρ (suc n')) _ = (n' , refl)
+    eval-valid (⇒ᵉ-ℕ ρ (suc n')) _ = (n' , refl)
 
-    open ForwardWithInterp.WithValidity eval-Valid using (analyze-correct) public
+    instance
+        SignEvalValid : ValidExprEvaluator SignEval latticeInterpretationᵍ
+        SignEvalValid = record { valid = eval-valid }
+
+    analyze-correct = Analysis.Forward.WithProg.analyze-correct SignLattice prog tt

Analysis/Utils.agda

@@ -0,0 +1,15 @@
+module Analysis.Utils where
+
+open import Data.Product using (_,_)
+open import Lattice
+
+module _ {o} {O : Set o} {_≼ᴼ_ : O → O → Set o}
+         (≼ᴼ-trans : ∀ {o₁ o₂ o₃} → o₁ ≼ᴼ o₂ → o₂ ≼ᴼ o₃ → o₁ ≼ᴼ o₃)
+         (combine : O → O → O) (combine-Mono₂ : Monotonic₂ _≼ᴼ_ _≼ᴼ_ _≼ᴼ_ combine) where
+
+    eval-combine₂ : {o₁ o₂ o₃ o₄ : O} → o₁ ≼ᴼ o₃ → o₂ ≼ᴼ o₄ →
+                    combine o₁ o₂ ≼ᴼ combine o₃ o₄
+    eval-combine₂ {o₁} {o₂} {o₃} {o₄} o₁≼o₃ o₂≼o₄ =
+        let (combine-Monoˡ , combine-Monoʳ) = combine-Mono₂
+        in ≼ᴼ-trans (combine-Monoˡ o₂ o₁≼o₃)
+                    (combine-Monoʳ o₃ o₂≼o₄)

Fixedpoint.agda

@@ -5,8 +5,8 @@ module Fixedpoint {a} {A : Set a}
                   {h : ℕ}
                   {_≈_ : A → A → Set a}
                   {_⊔_ : A → A → A} {_⊓_ : A → A → A}
-                  (≈-dec : IsDecidable _≈_)
+                  {{ ≈-Decidable : IsDecidable _≈_ }}
-                  (flA : IsFiniteHeightLattice A h _≈_ _⊔_ _⊓_)
+                  {{flA : IsFiniteHeightLattice A h _≈_ _⊔_ _⊓_}}
                   (f : A → A)
                   (Monotonicᶠ : Monotonic (IsFiniteHeightLattice._≼_ flA)
                                           (IsFiniteHeightLattice._≼_ flA) f) where
@@ -17,6 +17,7 @@ open import Data.Empty using (⊥-elim)
 open import Relation.Binary.PropositionalEquality using (_≡_; sym)
 open import Relation.Nullary using (Dec; ¬_; yes; no)
 
+open IsDecidable ≈-Decidable using () renaming (R-dec to ≈-dec)
 open IsFiniteHeightLattice flA
 
 import Chain
@@ -27,24 +28,9 @@ private
         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 boundedᴬ (ChainA.step x≺⊥ᴬ ≈-refl longestChainᴬ))
-                    where
-                        ⊥ᴬ⊓a̷≈⊥ᴬ : ¬ (⊥ᴬ ⊓ a) ≈ ⊥ᴬ
-                        ⊥ᴬ⊓a̷≈⊥ᴬ = λ ⊥ᴬ⊓a≈⊥ᴬ → ⊥ᴬ̷≈a⊓⊥ᴬ (≈-trans (≈-sym ⊥ᴬ⊓a≈⊥ᴬ) (⊓-comm _ _))
-
-                        x≺⊥ᴬ : (⊥ᴬ ⊓ a) ≺ ⊥ᴬ
-                        x≺⊥ᴬ = (≈-trans (⊔-comm _ _) (≈-trans (≈-refl {⊥ᴬ ⊔ (⊥ᴬ ⊓ a)}) (absorb-⊔-⊓ ⊥ᴬ a)) , ⊥ᴬ⊓a̷≈⊥ᴬ)
-
     -- using 'g', for gas, here helps make sure the function terminates.
     -- since A forms a fixed-height lattice, we must find a solution after
     -- 'h' steps at most. Gas is set up such that as soon as it runs
@@ -64,7 +50,7 @@ private
                     c' rewrite +-comm 1 hᶜ = ChainA.concat c (ChainA.step a₂≺fa₂ ≈-refl (ChainA.done (≈-refl {f a₂})))
 
     fix : Σ A (λ a → a ≈ f a)
-    fix = doStep (suc h) 0 ⊥ᴬ ⊥ᴬ (ChainA.done ≈-refl) (+-comm (suc h) 0) (⊥ᴬ≼ (f ⊥ᴬ))
+    fix = doStep (suc h) 0 ⊥ᴬ ⊥ᴬ (ChainA.done ≈-refl) (+-comm (suc h) 0) (⊥≼ (f ⊥ᴬ))
 
 aᶠ : A
 aᶠ = proj₁ fix
@@ -84,4 +70,4 @@ private
     ...   | no  _ = stepPreservesLess g' _ _ _ b b≈fb (≼-cong ≈-refl (≈-sym b≈fb) (Monotonicᶠ a₂≼b)) _ _ _
 
 aᶠ≼ : ∀ (a : A) → a ≈ f a → aᶠ ≼ a
-aᶠ≼ a a≈fa = stepPreservesLess (suc h) 0 ⊥ᴬ ⊥ᴬ a a≈fa (⊥ᴬ≼ a) (ChainA.done ≈-refl) (+-comm (suc h) 0) (⊥ᴬ≼ (f ⊥ᴬ))
+aᶠ≼ a a≈fa = stepPreservesLess (suc h) 0 ⊥ᴬ ⊥ᴬ a a≈fa (⊥≼ a) (ChainA.done ≈-refl) (+-comm (suc h) 0) (⊥≼ (f ⊥ᴬ))

Isomorphism.agda

@@ -63,27 +63,30 @@ module TransportFiniteHeight
         portChain₂ (done₂ a₂≈a₁) = done₁ (g-preserves-≈₂ a₂≈a₁)
         portChain₂ (step₂ {b₁} {b₂} (b₁≼b₂ , b₁̷≈b₂) b₂≈b₂' c) = step₁ (≈₁-trans (≈₁-sym (g-⊔-distr b₁ b₂)) (g-preserves-≈₂ b₁≼b₂) , g-preserves-̷≈ b₁̷≈b₂) (g-preserves-≈₂ b₂≈b₂') (portChain₂ c)
 
-    isFiniteHeightLattice : IsFiniteHeightLattice B height _≈₂_ _⊔₂_ _⊓₂_
+    open Chain.Height (IsFiniteHeightLattice.fixedHeight fhlA)
-    isFiniteHeightLattice =
+        using ()
-        let
+        renaming (⊥ to ⊥₁; ⊤ to ⊤₁; bounded to bounded₁; longestChain to c)
-            open Chain.Height (IsFiniteHeightLattice.fixedHeight fhlA)
+
-                using ()
+    instance
-                renaming (⊥ to ⊥₁; ⊤ to ⊤₁; bounded to bounded₁; longestChain to c)
+        fixedHeight : IsLattice.FixedHeight lB height
-        in record
+        fixedHeight = record
-            { isLattice = lB
+            { ⊥ = f ⊥₁
-            ; fixedHeight = record
+            ; ⊤ = f ⊤₁
-                { ⊥ = f ⊥₁
+            ; longestChain = portChain₁ c
-                ; ⊤ = f ⊤₁
+            ; bounded = λ c' → bounded₁ (portChain₂ c')
-                ; longestChain = portChain₁ c
-                ; bounded = λ c' → bounded₁ (portChain₂ c')
-                }
             }
 
-    finiteHeightLattice : FiniteHeightLattice B
+        isFiniteHeightLattice : IsFiniteHeightLattice B height _≈₂_ _⊔₂_ _⊓₂_
-    finiteHeightLattice = record
+        isFiniteHeightLattice = record
-        { height = height
+            { isLattice = lB
-        ; _≈_ = _≈₂_
+            ; fixedHeight = fixedHeight
-        ; _⊔_ = _⊔₂_
+            }
-        ; _⊓_ = _⊓₂_
+
-        ; isFiniteHeightLattice = isFiniteHeightLattice
+        finiteHeightLattice : FiniteHeightLattice B
-        }
+        finiteHeightLattice = record
+            { height = height
+            ; _≈_ = _≈₂_
+            ; _⊔_ = _⊔₂_
+            ; _⊓_ = _⊓₂_
+            ; isFiniteHeightLattice = isFiniteHeightLattice
+            }

Language.agda

@@ -16,12 +16,13 @@ open import Data.Nat using (ℕ; suc)
 open import Data.Product using (_,_; Σ; proj₁; proj₂)
 open import Data.Product.Properties as ProdProp using ()
 open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
+open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl)
 open import Relation.Nullary using (¬_)
 
 open import Lattice
 open import Utils using (Unique; push; Unique-map; x∈xs⇒fx∈fxs)
-open import Lattice.MapSet _≟ˢ_ using ()
+open import Lattice.MapSet String {{record { R-dec = _≟ˢ_ }}} _ using ()
     renaming
         ( MapSet to StringSet
         ; to-List to to-Listˢ
@@ -73,10 +74,10 @@ record Program : Set where
     -- vars-complete : ∀ {k : String} (s : State) → k ∈ᵇ (code s) → k ListMem.∈ vars
     -- vars-complete {k} s = ∈⇒∈-Stmts-vars {length} {k} {stmts} {s}
 
-    _≟_ : IsDecidable (_≡_ {_} {State})
+    _≟_ : Decidable (_≡_ {_} {State})
     _≟_ = FinProp._≟_
 
-    _≟ᵉ_ : IsDecidable (_≡_ {_} {Graph.Edge graph})
+    _≟ᵉ_ : Decidable (_≡_ {_} {Graph.Edge graph})
     _≟ᵉ_ = ProdProp.≡-dec _≟_ _≟_
 
     open import Data.List.Membership.DecPropositional _≟ᵉ_ using (_∈?_)

Language/Base.agda

@@ -39,7 +39,7 @@ data _∈ᵇ_ : String → BasicStmt → Set where
     in←₁ : ∀ {k : String} {e : Expr} → k ∈ᵇ (k ← e)
     in←₂ : ∀ {k k' : String} {e : Expr} → k ∈ᵉ e → k ∈ᵇ (k' ← e)
 
-open import Lattice.MapSet (String._≟_)
+open import Lattice.MapSet String {{record { R-dec = String._≟_ }}} _
     renaming
         ( MapSet to StringSet
         ; insert to insertˢ

Language/Graphs.agda

@@ -12,7 +12,6 @@ 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.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)
@@ -122,7 +121,7 @@ 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 (if _ then s₁ else s₂) = buildCfg s₁ ∙ buildCfg s₂
 buildCfg (while _ repeat s) = loop (buildCfg s)
 
 private
@@ -148,7 +147,11 @@ private
     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 (_∈?_)
+    open import Data.Product.Properties as ProdProp using ()
+    private _≟_ = ProdProp.≡-dec (FinProp._≟_ {Graph.size g})
+                                 (FinProp._≟_ {Graph.size g})
+
+    open import Data.List.Membership.DecPropositional (_≟_) using (_∈?_)
 
     indices : List (Graph.Index g)
     indices = proj₁ (finValues (Graph.size g))

Language/Properties.agda

@@ -285,13 +285,9 @@ buildCfg-sufficient (⇒ˢ-⟨⟩ ρ₁ ρ₂ bs ρ₁,bs⇒ρ₂) =
 buildCfg-sufficient (⇒ˢ-then ρ₁ ρ₂ ρ₃ s₁ s₂ ρ₁,s₁⇒ρ₂ ρ₂,s₂⇒ρ₃) =
     buildCfg-sufficient ρ₁,s₁⇒ρ₂ ++ buildCfg-sufficient ρ₂,s₂⇒ρ₃
 buildCfg-sufficient (⇒ˢ-if-true ρ₁ ρ₂ _ _ s₁ s₂ _ _ ρ₁,s₁⇒ρ₂) =
-    EndToEndTrace-singleton[] ρ₁ ++
+    EndToEndTrace-∙ˡ (buildCfg-sufficient ρ₁,s₁⇒ρ₂)
-    (EndToEndTrace-∙ˡ (buildCfg-sufficient ρ₁,s₁⇒ρ₂)) ++
-    EndToEndTrace-singleton[] ρ₂
 buildCfg-sufficient (⇒ˢ-if-false ρ₁ ρ₂ _ s₁ s₂ _ ρ₁,s₂⇒ρ₂) =
-    EndToEndTrace-singleton[] ρ₁ ++
+    EndToEndTrace-∙ʳ {buildCfg s₁} (buildCfg-sufficient ρ₁,s₂⇒ρ₂)
-    (EndToEndTrace-∙ʳ {buildCfg s₁} (buildCfg-sufficient ρ₁,s₂⇒ρ₂)) ++
-    EndToEndTrace-singleton[] ρ₂
 buildCfg-sufficient (⇒ˢ-while-true ρ₁ ρ₂ ρ₃ _ _ s _ _ ρ₁,s⇒ρ₂ ρ₂,ws⇒ρ₃) =
     EndToEndTrace-loop² {buildCfg s}
                         (EndToEndTrace-loop {buildCfg s} (buildCfg-sufficient ρ₁,s⇒ρ₂))

Lattice.agda

@@ -4,15 +4,17 @@ open import Equivalence
 import Chain
 
 open import Relation.Binary.Core using (_Preserves_⟶_ )
-open import Relation.Nullary using (Dec; ¬_)
+open import Relation.Nullary using (Dec; ¬_; yes; no)
+open import Data.Empty using (⊥-elim)
 open import Data.Nat as Nat using (ℕ)
 open import Data.Product using (_×_; Σ; _,_)
 open import Data.Sum using (_⊎_; inj₁; inj₂)
 open import Agda.Primitive using (lsuc; Level) renaming (_⊔_ to _⊔ℓ_)
 open import Function.Definitions using (Injective)
 
-IsDecidable : ∀ {a} {A : Set a} (R : A → A → Set a) → Set a
+record IsDecidable {a} {A : Set a} (R : A → A → Set a) : Set a where
-IsDecidable {a} {A} R = ∀ (a₁ a₂ : A) → Dec (R a₁ a₂)
+    field
+        R-dec : ∀ (a₁ a₂ : A) → Dec (R a₁ a₂)
 
 module _ {a b} {A : Set a} {B : Set b}
     (_≼₁_ : A → A → Set a) (_≼₂_ : B → B → Set b) where
@@ -20,6 +22,18 @@ module _ {a b} {A : Set a} {B : Set b}
     Monotonic : (A → B) → Set (a ⊔ℓ b)
     Monotonic f = ∀ {a₁ a₂ : A} → a₁ ≼₁ a₂ → f a₁ ≼₂ f a₂
 
+    Monotonicˡ : ∀ {c} {C : Set c} → (A → C → B) →  Set (a ⊔ℓ b ⊔ℓ c)
+    Monotonicˡ f = ∀ c →  Monotonic (λ a → f a c)
+
+    Monotonicʳ : ∀ {c} {C : Set c} → (C → A → B) →  Set (a ⊔ℓ b ⊔ℓ c)
+    Monotonicʳ f = ∀ a → Monotonic (f a)
+
+module _ {a b c} {A : Set a} {B : Set b} {C : Set c}
+    (_≼₁_ : A → A → Set a) (_≼₂_ : B → B → Set b) (_≼₃_ : C → C → Set c) where
+
+    Monotonic₂ : (A → B → C) → Set (a ⊔ℓ b ⊔ℓ c)
+    Monotonic₂ f = Monotonicˡ _≼₁_ _≼₃_ f × Monotonicʳ _≼₂_ _≼₃_ f
+
 record IsSemilattice {a} (A : Set a)
     (_≈_ : A → A → Set a)
     (_⊔_ : A → A → A) : Set a where
@@ -186,8 +200,8 @@ record IsLattice {a} (A : Set a)
     (_⊓_ : A → A → A) : Set a where
 
     field
-        joinSemilattice : IsSemilattice A _≈_ _⊔_
+        {{joinSemilattice}} : IsSemilattice A _≈_ _⊔_
-        meetSemilattice : IsSemilattice A _≈_ _⊓_
+        {{meetSemilattice}} : IsSemilattice A _≈_ _⊓_
 
         absorb-⊔-⊓ : (x y : A) → (x ⊔ (x ⊓ y)) ≈ x
         absorb-⊓-⊔ : (x y : A) → (x ⊓ (x ⊔ y)) ≈ x
@@ -216,12 +230,34 @@ record IsFiniteHeightLattice {a} (A : Set a)
     (_⊓_ : A → A → A) : Set (lsuc a) where
 
     field
-        isLattice : IsLattice A _≈_ _⊔_ _⊓_
+        {{isLattice}} : IsLattice A _≈_ _⊔_ _⊓_
 
     open IsLattice isLattice public
 
     field
-        fixedHeight : FixedHeight h
+        {{fixedHeight}} : FixedHeight h
+
+    -- If the equality is decidable, we can prove that the top and bottom
+    -- elements of the chain are least and greatest elements of the lattice
+    module _ {{≈-Decidable : IsDecidable _≈_}} where
+        open IsDecidable ≈-Decidable using () renaming (R-dec to ≈-dec)
+
+        module MyChain = Chain _≈_ ≈-equiv _≺_ ≺-cong
+        open MyChain.Height fixedHeight using (⊥; ⊤) public
+        open MyChain.Height fixedHeight using (bounded; longestChain)
+
+        ⊥≼ : ∀ (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 (MyChain.Bounded-suc-n bounded (MyChain.step x≺⊥ ≈-refl longestChain))
+                        where
+                            ⊥⊓a̷≈⊥ : ¬ (⊥ ⊓ a) ≈ ⊥
+                            ⊥⊓a̷≈⊥ = λ ⊥⊓a≈⊥ → ⊥ᴬ̷≈a⊓⊥ (≈-trans (≈-sym ⊥⊓a≈⊥) (⊓-comm _ _))
+
+                            x≺⊥ : (⊥ ⊓ a) ≺ ⊥
+                            x≺⊥ = (≈-trans (⊔-comm _ _) (≈-trans (≈-refl {⊥ ⊔ (⊥ ⊓ a)}) (absorb-⊔-⊓ ⊥ a)) , ⊥⊓a̷≈⊥)
 
 module ChainMapping {a b} {A : Set a} {B : Set b}
     {_≈₁_ : A → A → Set a} {_≈₂_ : B → B → Set b}
@@ -251,7 +287,7 @@ record Semilattice {a} (A : Set a) : Set (lsuc a) where
         _≈_ : A → A → Set a
         _⊔_ : A → A → A
 
-        isSemilattice : IsSemilattice A _≈_ _⊔_
+        {{isSemilattice}} : IsSemilattice A _≈_ _⊔_
 
     open IsSemilattice isSemilattice public
 
@@ -262,7 +298,7 @@ record Lattice {a} (A : Set a) : Set (lsuc a) where
         _⊔_ : A → A → A
         _⊓_ : A → A → A
 
-        isLattice : IsLattice A _≈_ _⊔_ _⊓_
+        {{isLattice}} : IsLattice A _≈_ _⊔_ _⊓_
 
     open IsLattice isLattice public
 
@@ -273,6 +309,6 @@ record FiniteHeightLattice {a} (A : Set a) : Set (lsuc a) where
         _⊔_ : A → A → A
         _⊓_ : A → A → A
 
-        isFiniteHeightLattice : IsFiniteHeightLattice A height _≈_ _⊔_ _⊓_
+        {{isFiniteHeightLattice}} : IsFiniteHeightLattice A height _≈_ _⊔_ _⊓_
 
     open IsFiniteHeightLattice isFiniteHeightLattice public

Lattice/AboveBelow.agda

@@ -1,17 +1,19 @@
 open import Lattice
 open import Equivalence
 open import Relation.Nullary using (Dec; ¬_; yes; no)
+open import Data.Unit using () renaming (⊤ to ⊤ᵘ)
 
 module Lattice.AboveBelow {a} (A : Set a)
-                          (_≈₁_ : A → A → Set a)
+                          {_≈₁_ : A → A → Set a}
-                          (≈₁-equiv : IsEquivalence A _≈₁_)
+                          {{≈₁-equiv : IsEquivalence A _≈₁_}}
-                          (≈₁-dec : IsDecidable _≈₁_) where
+                          {{≈₁-Decidable : IsDecidable _≈₁_}} (dummy : ⊤ᵘ) where
 
 open import Data.Empty using (⊥-elim)
 open import Data.Product using (_,_)
 open import Data.Nat using (_≤_; ℕ; z≤n; s≤s; suc)
 open import Function using (_∘_)
 open import Showable using (Showable; show)
+open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Binary.PropositionalEquality as Eq
     using (_≡_; sym; subst; refl)
 
@@ -20,6 +22,8 @@ import Chain
 open IsEquivalence ≈₁-equiv using ()
     renaming (≈-refl to ≈₁-refl; ≈-sym to ≈₁-sym; ≈-trans to ≈₁-trans)
 
+open IsDecidable ≈₁-Decidable using () renaming (R-dec to ≈₁-dec)
+
 data AboveBelow : Set a where
     ⊥ : AboveBelow
     ⊤ : AboveBelow
@@ -62,7 +66,7 @@ data _≈_ : AboveBelow → AboveBelow → Set a where
     ; ≈-trans = ≈-trans
     }
 
-≈-dec : IsDecidable _≈_
+≈-dec : Decidable _≈_
 ≈-dec ⊥ ⊥ = yes ≈-⊥-⊥
 ≈-dec ⊤ ⊤ = yes ≈-⊤-⊤
 ≈-dec [ x ] [ y ]
@@ -76,6 +80,10 @@ data _≈_ : AboveBelow → AboveBelow → Set a where
 ≈-dec [ x ] ⊥ = no λ ()
 ≈-dec [ x ] ⊤ = no λ ()
 
+instance
+    ≈-Decidable : IsDecidable _≈_
+    ≈-Decidable = record { R-dec = ≈-dec }
+
 -- Any object can be wrapped in an 'above below' to make it a lattice,
 -- since ⊤ and ⊥ are the largest and least elements, and the rest are left
 -- unordered. That's what this module does.
@@ -169,14 +177,15 @@ module Plain (x : A) where
     ⊔-idemp ⊥ = ≈-⊥-⊥
     ⊔-idemp [ x ] rewrite x≈y⇒[x]⊔[y]≡[x] (≈₁-refl {x}) = ≈-refl
 
-    isJoinSemilattice : IsSemilattice AboveBelow _≈_ _⊔_
+    instance
-    isJoinSemilattice = record
+        isJoinSemilattice : IsSemilattice AboveBelow _≈_ _⊔_
-        { ≈-equiv = ≈-equiv
+        isJoinSemilattice = record
-        ; ≈-⊔-cong = ≈-⊔-cong
+            { ≈-equiv = ≈-equiv
-        ; ⊔-assoc = ⊔-assoc
+            ; ≈-⊔-cong = ≈-⊔-cong
-        ; ⊔-comm = ⊔-comm
+            ; ⊔-assoc = ⊔-assoc
-        ; ⊔-idemp = ⊔-idemp
+            ; ⊔-comm = ⊔-comm
-        }
+            ; ⊔-idemp = ⊔-idemp
+            }
 
     _⊓_ : AboveBelow → AboveBelow → AboveBelow
     ⊥ ⊓ x = ⊥
@@ -262,14 +271,15 @@ module Plain (x : A) where
     ⊓-idemp ⊤ = ≈-⊤-⊤
     ⊓-idemp [ x ] rewrite x≈y⇒[x]⊓[y]≡[x] (≈₁-refl {x}) = ≈-refl
 
-    isMeetSemilattice : IsSemilattice AboveBelow _≈_ _⊓_
+    instance
-    isMeetSemilattice = record
+        isMeetSemilattice : IsSemilattice AboveBelow _≈_ _⊓_
-        { ≈-equiv = ≈-equiv
+        isMeetSemilattice = record
-        ; ≈-⊔-cong = ≈-⊓-cong
+            { ≈-equiv = ≈-equiv
-        ; ⊔-assoc = ⊓-assoc
+            ; ≈-⊔-cong = ≈-⊓-cong
-        ; ⊔-comm = ⊓-comm
+            ; ⊔-assoc = ⊓-assoc
-        ; ⊔-idemp = ⊓-idemp
+            ; ⊔-comm = ⊓-comm
-        }
+            ; ⊔-idemp = ⊓-idemp
+            }
 
     absorb-⊔-⊓ : ∀ (ab₁ ab₂ : AboveBelow) → (ab₁ ⊔ (ab₁ ⊓ ab₂)) ≈ ab₁
     absorb-⊔-⊓ ⊥ ab₂ rewrite ⊥⊓x≡⊥ ab₂ = ≈-⊥-⊥
@@ -294,23 +304,24 @@ module Plain (x : A) where
     ...   | no x̷≈y rewrite x̷≈y⇒[x]⊔[y]≡⊤ x̷≈y rewrite x⊓⊤≡x [ x ] = ≈-refl
 
 
-    isLattice : IsLattice AboveBelow _≈_ _⊔_ _⊓_
+    instance
-    isLattice = record
+        isLattice : IsLattice AboveBelow _≈_ _⊔_ _⊓_
-        { joinSemilattice = isJoinSemilattice
+        isLattice = record
-        ; meetSemilattice = isMeetSemilattice
+            { joinSemilattice = isJoinSemilattice
-        ; absorb-⊔-⊓ = absorb-⊔-⊓
+            ; meetSemilattice = isMeetSemilattice
-        ; absorb-⊓-⊔ = absorb-⊓-⊔
+            ; absorb-⊔-⊓ = absorb-⊔-⊓
-        }
+            ; absorb-⊓-⊔ = absorb-⊓-⊔
+            }
 
-    lattice : Lattice AboveBelow
+        lattice : Lattice AboveBelow
-    lattice = record
+        lattice = record
-        { _≈_ = _≈_
+            { _≈_ = _≈_
-        ; _⊔_ = _⊔_
+            ; _⊔_ = _⊔_
-        ; _⊓_ = _⊓_
+            ; _⊓_ = _⊓_
-        ; isLattice = isLattice
+            ; isLattice = isLattice
-        }
+            }
 
-    open IsLattice isLattice using (_≼_; _≺_; ⊔-Monotonicˡ; ⊔-Monotonicʳ) public
+    open IsLattice isLattice using (_≼_; _≺_; ≼-trans; ≼-refl; ⊔-Monotonicˡ; ⊔-Monotonicʳ) public
 
     ⊥≺[x] : ∀ (x : A) → ⊥ ≺ [ x ]
     ⊥≺[x] x = (≈-refl , λ ())
@@ -354,25 +365,26 @@ module Plain (x : A) where
     isLongest {⊥} (step {_} {[ x ]} _ (≈-lift _) (step [x]≺y y≈z c@(step _ _ _)))
         rewrite [x]≺y⇒y≡⊤ _ _ [x]≺y with ≈-⊤-⊤ ← y≈z = ⊥-elim (¬-Chain-⊤ c)
 
-    fixedHeight : IsLattice.FixedHeight isLattice 2
+    instance
-    fixedHeight = record
+        fixedHeight : IsLattice.FixedHeight isLattice 2
-        { ⊥ = ⊥
+        fixedHeight = record
-        ; ⊤ = ⊤
+            { ⊥ = ⊥
-        ; longestChain = longestChain
+            ; ⊤ = ⊤
-        ; bounded = isLongest
+            ; longestChain = longestChain
-        }
+            ; bounded = isLongest
+            }
 
-    isFiniteHeightLattice : IsFiniteHeightLattice AboveBelow 2 _≈_ _⊔_ _⊓_
+        isFiniteHeightLattice : IsFiniteHeightLattice AboveBelow 2 _≈_ _⊔_ _⊓_
-    isFiniteHeightLattice = record
+        isFiniteHeightLattice = record
-        { isLattice = isLattice
+            { isLattice = isLattice
-        ; fixedHeight = fixedHeight
+            ; fixedHeight = fixedHeight
-        }
+            }
 
-    finiteHeightLattice : FiniteHeightLattice AboveBelow
+        finiteHeightLattice : FiniteHeightLattice AboveBelow
-    finiteHeightLattice = record
+        finiteHeightLattice = record
-        { height = 2
+            { height = 2
-        ; _≈_ = _≈_
+            ; _≈_ = _≈_
-        ; _⊔_ = _⊔_
+            ; _⊔_ = _⊔_
-        ; _⊓_ = _⊓_
+            ; _⊓_ = _⊓_
-        ; isFiniteHeightLattice = isFiniteHeightLattice
+            ; isFiniteHeightLattice = isFiniteHeightLattice
-        }
+            }

Lattice/ExtendBelow.agda

@@ -0,0 +1,169 @@
+open import Lattice
+
+module Lattice.ExtendBelow {a} (A : Set a)
+    {_≈₁_ : A → A → Set a} {_⊔₁_ : A → A → A} {_⊓₁_ : A → A → A}
+    {{lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_}} where
+
+open import Equivalence
+open import Showable using (Showable; show)
+open import Relation.Binary.Definitions using (Decidable)
+open import Relation.Binary.PropositionalEquality using (refl)
+open import Relation.Nullary using (Dec; ¬_; yes; no)
+
+open IsLattice lA using ()
+    renaming ( ≈-equiv to ≈₁-equiv
+             ; ≈-⊔-cong to ≈₁-⊔₁-cong
+             ; ⊔-assoc to ⊔₁-assoc; ⊔-comm to ⊔₁-comm; ⊔-idemp to ⊔₁-idemp
+             ; ≈-⊓-cong to ≈₁-⊓₁-cong
+             ; ⊓-assoc to ⊓₁-assoc; ⊓-comm to ⊓₁-comm; ⊓-idemp to ⊓₁-idemp
+             ; absorb-⊔-⊓ to absorb-⊔₁-⊓₁; absorb-⊓-⊔ to absorb-⊓₁-⊔₁
+             )
+
+open IsEquivalence ≈₁-equiv using ()
+    renaming (≈-refl to ≈₁-refl; ≈-sym to ≈₁-sym; ≈-trans to ≈₁-trans)
+
+data ExtendBelow : Set a where
+    [_] : A → ExtendBelow
+    ⊥ : ExtendBelow
+
+instance
+    showable : {{ showableA : Showable A }} → Showable ExtendBelow
+    showable = record
+        { show = (λ
+            { ⊥ → "⊥"
+            ; [ a ] → show a
+            })
+        }
+
+data _≈_ : ExtendBelow → ExtendBelow → Set a where
+    ≈-⊥-⊥ : ⊥ ≈ ⊥
+    ≈-lift : ∀ {x y : A} → x ≈₁ y → [ x ] ≈ [ y ]
+
+≈-refl : ∀ {ab : ExtendBelow} → ab ≈ ab
+≈-refl {⊥} = ≈-⊥-⊥
+≈-refl {[ x ]} = ≈-lift ≈₁-refl
+
+≈-sym : ∀ {ab₁ ab₂ : ExtendBelow} → ab₁ ≈ ab₂ → ab₂ ≈ ab₁
+≈-sym ≈-⊥-⊥ = ≈-⊥-⊥
+≈-sym (≈-lift x≈₁y) = ≈-lift (≈₁-sym x≈₁y)
+
+≈-trans : ∀ {ab₁ ab₂ ab₃ : ExtendBelow} → ab₁ ≈ ab₂ → ab₂ ≈ ab₃ → ab₁ ≈ ab₃
+≈-trans ≈-⊥-⊥ ≈-⊥-⊥ = ≈-⊥-⊥
+≈-trans (≈-lift a₁≈a₂) (≈-lift a₂≈a₃) = ≈-lift (≈₁-trans a₁≈a₂ a₂≈a₃)
+
+instance
+    ≈-equiv : IsEquivalence ExtendBelow _≈_
+    ≈-equiv = record
+        { ≈-refl = ≈-refl
+        ; ≈-sym = ≈-sym
+        ; ≈-trans = ≈-trans
+        }
+
+_⊔_ : ExtendBelow → ExtendBelow → ExtendBelow
+_⊔_ ⊥ x = x
+_⊔_ [ a₁ ] ⊥ = [ a₁ ]
+_⊔_ [ a₁ ] [ a₂ ] = [ a₁ ⊔₁ a₂ ]
+
+_⊓_ : ExtendBelow → ExtendBelow → ExtendBelow
+_⊓_ ⊥ x = ⊥
+_⊓_ [ _ ] ⊥ = ⊥
+_⊓_ [ a₁ ] [ a₂ ] = [ a₁ ⊓₁ a₂ ]
+
+≈-⊔-cong : ∀ {x₁ x₂ x₃ x₄} → x₁ ≈ x₂ → x₃ ≈ x₄ →
+           (x₁ ⊔ x₃) ≈ (x₂ ⊔ x₄)
+≈-⊔-cong .{⊥} .{⊥} {x₃} {x₄} ≈-⊥-⊥ [a₃]≈[a₄] = [a₃]≈[a₄]
+≈-⊔-cong {x₁ = [ a₁ ]} {x₂ = [ a₂ ]} .{⊥} .{⊥} [a₁]≈[a₂] ≈-⊥-⊥ = [a₁]≈[a₂]
+≈-⊔-cong {x₁ = [ a₁ ]} {x₂ = [ a₂ ]} {x₃ = [ a₃ ]} {x₄ = [ a₄ ]} (≈-lift a₁≈a₂) (≈-lift a₃≈a₄) = ≈-lift (≈₁-⊔₁-cong a₁≈a₂ a₃≈a₄)
+
+⊔-assoc : ∀ (x₁ x₂ x₃ : ExtendBelow) →  ((x₁ ⊔ x₂) ⊔ x₃) ≈ (x₁ ⊔ (x₂ ⊔ x₃))
+⊔-assoc ⊥ x₁ x₂ = ≈-refl
+⊔-assoc [ a₁ ] ⊥ x₂ = ≈-refl
+⊔-assoc [ a₁ ] [ a₂ ] ⊥ = ≈-refl
+⊔-assoc [ a₁ ] [ a₂ ] [ a₃ ] = ≈-lift (⊔₁-assoc a₁ a₂ a₃)
+
+⊔-comm : ∀ (x₁ x₂ : ExtendBelow) →  (x₁ ⊔ x₂) ≈ (x₂ ⊔ x₁)
+⊔-comm ⊥ ⊥ = ≈-refl
+⊔-comm ⊥ [ a₂ ] = ≈-refl
+⊔-comm [ a₁ ] ⊥ = ≈-refl
+⊔-comm [ a₁ ] [ a₂ ] = ≈-lift (⊔₁-comm a₁ a₂)
+
+⊔-idemp : ∀ (x : ExtendBelow) →  (x ⊔ x) ≈ x
+⊔-idemp ⊥ = ≈-refl
+⊔-idemp [ a ] = ≈-lift (⊔₁-idemp a)
+
+≈-⊓-cong : ∀ {x₁ x₂ x₃ x₄} → x₁ ≈ x₂ → x₃ ≈ x₄ →
+           (x₁ ⊓ x₃) ≈ (x₂ ⊓ x₄)
+≈-⊓-cong .{⊥} .{⊥} {x₃} {x₄} ≈-⊥-⊥ [a₃]≈[a₄] = ≈-⊥-⊥
+≈-⊓-cong {x₁ = [ a₁ ]} {x₂ = [ a₂ ]} .{⊥} .{⊥} [a₁]≈[a₂] ≈-⊥-⊥ = ≈-⊥-⊥
+≈-⊓-cong {x₁ = [ a₁ ]} {x₂ = [ a₂ ]} {x₃ = [ a₃ ]} {x₄ = [ a₄ ]} (≈-lift a₁≈a₂) (≈-lift a₃≈a₄) = ≈-lift (≈₁-⊓₁-cong a₁≈a₂ a₃≈a₄)
+
+⊓-assoc : ∀ (x₁ x₂ x₃ : ExtendBelow) →  ((x₁ ⊓ x₂) ⊓ x₃) ≈ (x₁ ⊓ (x₂ ⊓ x₃))
+⊓-assoc ⊥ x₁ x₂ = ≈-refl
+⊓-assoc [ a₁ ] ⊥ x₂ = ≈-refl
+⊓-assoc [ a₁ ] [ a₂ ] ⊥ = ≈-refl
+⊓-assoc [ a₁ ] [ a₂ ] [ a₃ ] = ≈-lift (⊓₁-assoc a₁ a₂ a₃)
+
+⊓-comm : ∀ (x₁ x₂ : ExtendBelow) →  (x₁ ⊓ x₂) ≈ (x₂ ⊓ x₁)
+⊓-comm ⊥ ⊥ = ≈-refl
+⊓-comm ⊥ [ a₂ ] = ≈-refl
+⊓-comm [ a₁ ] ⊥ = ≈-refl
+⊓-comm [ a₁ ] [ a₂ ] = ≈-lift (⊓₁-comm a₁ a₂)
+
+⊓-idemp : ∀ (x : ExtendBelow) →  (x ⊓ x) ≈ x
+⊓-idemp ⊥ = ≈-refl
+⊓-idemp [ a ] = ≈-lift (⊓₁-idemp a)
+
+absorb-⊔-⊓ : (x₁ x₂ : ExtendBelow) → (x₁ ⊔ (x₁ ⊓ x₂)) ≈ x₁
+absorb-⊔-⊓ ⊥ ⊥ = ≈-refl
+absorb-⊔-⊓ ⊥ [ a₂ ] = ≈-refl
+absorb-⊔-⊓ [ a₁ ] ⊥ = ≈-refl
+absorb-⊔-⊓ [ a₁ ] [ a₂ ] = ≈-lift (absorb-⊔₁-⊓₁ a₁ a₂)
+
+absorb-⊓-⊔ : (x₁ x₂ : ExtendBelow) → (x₁ ⊓ (x₁ ⊔ x₂)) ≈ x₁
+absorb-⊓-⊔ ⊥ ⊥ = ≈-refl
+absorb-⊓-⊔ ⊥ [ a₂ ] = ≈-refl
+absorb-⊓-⊔ [ a₁ ] ⊥ = ⊓-idemp [ a₁ ]
+absorb-⊓-⊔ [ a₁ ] [ a₂ ] = ≈-lift (absorb-⊓₁-⊔₁ a₁ a₂)
+
+instance
+    isJoinSemilattice : IsSemilattice ExtendBelow _≈_ _⊔_
+    isJoinSemilattice = record
+        { ≈-equiv = ≈-equiv
+        ; ≈-⊔-cong = ≈-⊔-cong
+        ; ⊔-assoc = ⊔-assoc
+        ; ⊔-comm = ⊔-comm
+        ; ⊔-idemp = ⊔-idemp
+        }
+
+    isMeetSemilattice : IsSemilattice ExtendBelow _≈_ _⊓_
+    isMeetSemilattice = record
+        { ≈-equiv = ≈-equiv
+        ; ≈-⊔-cong = ≈-⊓-cong
+        ; ⊔-assoc = ⊓-assoc
+        ; ⊔-comm = ⊓-comm
+        ; ⊔-idemp = ⊓-idemp
+        }
+
+    isLattice : IsLattice ExtendBelow _≈_ _⊔_ _⊓_
+    isLattice = record
+        { joinSemilattice = isJoinSemilattice
+        ; meetSemilattice = isMeetSemilattice
+        ; absorb-⊔-⊓ = absorb-⊔-⊓
+        ; absorb-⊓-⊔ = absorb-⊓-⊔
+        }
+
+module _ {{≈₁-Decidable : IsDecidable _≈₁_}} where
+    open IsDecidable ≈₁-Decidable using () renaming (R-dec to ≈₁-dec)
+
+    ≈-dec : Decidable _≈_
+    ≈-dec ⊥ ⊥ = yes ≈-⊥-⊥
+    ≈-dec [ a₁ ] [ a₂ ]
+        with ≈₁-dec a₁ a₂
+    ...   | yes a₁≈a₂ = yes (≈-lift a₁≈a₂)
+    ...   | no a₁̷≈a₂ = no (λ { (≈-lift a₁≈a₂) → a₁̷≈a₂ a₁≈a₂ })
+    ≈-dec ⊥ [ _ ] = no (λ ())
+    ≈-dec [ _ ] ⊥ = no (λ ())
+
+    instance
+        ≈-Decidable : IsDecidable _≈_
+        ≈-Decidable = record { R-dec = ≈-dec }

Lattice/FiniteMap.agda

@@ -3,16 +3,28 @@ open import Relation.Binary.PropositionalEquality as Eq
     using (_≡_;refl; sym; trans; cong; subst)
 open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
 open import Data.List using (List; _∷_; [])
+open import Data.Unit using (⊤)
 
-module Lattice.FiniteMap {a b : Level} {A : Set a} {B : Set b}
+module Lattice.FiniteMap (A : Set) (B : Set)
-    {_≈₂_ : B → B → Set b}
+    {_≈₂_ : B → B → Set}
     {_⊔₂_ : B → B → B} {_⊓₂_ : B → B → B}
-    (≡-dec-A : IsDecidable (_≡_ {a} {A}))
+    {{≡-Decidable-A : IsDecidable {_} {A} _≡_}}
-    (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
+    {{lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_}} (ks : List A) where
 
 open IsLattice lB using () renaming (_≼_ to _≼₂_)
-open import Lattice.Map ≡-dec-A lB as Map
+open import Lattice.Map A B _ as Map
-    using (Map; ⊔-equal-keys; ⊓-equal-keys)
+    using
+        ( Map
+        ; ⊔-equal-keys
+        ; ⊓-equal-keys
+        ; subset-impl
+        ; Map-functional
+        ; Expr-Provenance
+        ; Expr-Provenance-≡
+        ; `_; _∪_; _∩_
+        ; in₁; in₂; bothᵘ; single
+        ; ⊔-combines
+        )
     renaming
         ( _≈_ to _≈ᵐ_
         ; _⊔_ to _⊔ᵐ_
@@ -28,7 +40,7 @@ open import Lattice.Map ≡-dec-A lB as Map
         ; ⊓-idemp to ⊓ᵐ-idemp
         ; absorb-⊔-⊓ to absorb-⊔ᵐ-⊓ᵐ
         ; absorb-⊓-⊔ to absorb-⊓ᵐ-⊔ᵐ
-        ; ≈-dec to ≈ᵐ-dec
+        ; ≈-Decidable to ≈ᵐ-Decidable
         ; _[_] to _[_]ᵐ
         ; []-∈ to []ᵐ-∈
         ; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ
@@ -46,17 +58,24 @@ open import Lattice.Map ≡-dec-A lB as Map
         ; _≼_ to _≼ᵐ_
         ; ∈k-dec to ∈k-decᵐ
         )
+open import Data.Empty using (⊥-elim)
+open import Data.List using (List; length; []; _∷_; map)
 open import Data.List.Membership.Propositional using () renaming (_∈_ to _∈ˡ_)
-open import Data.Product using (_×_; _,_; Σ; proj₁ ; proj₂)
+open import Data.List.Properties using (∷-injectiveʳ)
+open import Data.List.Relation.Unary.All using (All)
+open import Data.List.Relation.Unary.Any using (Any; here; there)
+open import Data.Nat using (ℕ)
+open import Data.Product using (_×_; _,_; Σ; proj₁; proj₂)
 open import Equivalence
 open import Function using (_∘_)
 open import Relation.Nullary using (¬_; Dec; yes; no)
-open import Utils using (Pairwise; _∷_; [])
+open import Utils using (Pairwise; _∷_; []; Unique; push; empty; All¬-¬Any)
-open import Data.Empty using (⊥-elim)
 open import Showable using (Showable; show)
+open import Isomorphism using (IsInverseˡ; IsInverseʳ)
+open import Chain using (Height)
 
-module WithKeys (ks : List A) where
+private module WithKeys (ks : List A) where
-    FiniteMap : Set (a ⊔ℓ b)
+    FiniteMap : Set
     FiniteMap = Σ Map (λ m → Map.keys m ≡ ks)
 
     instance
@@ -64,11 +83,15 @@ module WithKeys (ks : List A) where
                    Showable FiniteMap
         showable = record { show = λ (m₁ , _) → show m₁ }
 
-    _≈_ : FiniteMap → FiniteMap → Set (a ⊔ℓ b)
+    _≈_ : FiniteMap → FiniteMap → Set
     _≈_ (m₁ , _) (m₂ , _) = m₁ ≈ᵐ m₂
 
-    ≈₂-dec⇒≈-dec : IsDecidable _≈₂_ → IsDecidable _≈_
+    instance
-    ≈₂-dec⇒≈-dec ≈₂-dec fm₁ fm₂ = ≈ᵐ-dec ≈₂-dec (proj₁ fm₁) (proj₁ fm₂)
+        ≈-Decidable : {{ IsDecidable _≈₂_ }} → IsDecidable _≈_
+        ≈-Decidable {{≈₂-Decidable}} = record
+            { R-dec = λ fm₁ fm₂ →  IsDecidable.R-dec (≈ᵐ-Decidable {{≈₂-Decidable}})
+                                                     (proj₁ fm₁) (proj₁ fm₂)
+            }
 
     _⊔_ : FiniteMap → FiniteMap → FiniteMap
     _⊔_ (m₁ , km₁≡ks) (m₂ , km₂≡ks) =
@@ -84,10 +107,10 @@ module WithKeys (ks : List A) where
                 km₁≡ks
         )
 
-    _∈_ : A × B → FiniteMap → Set (a ⊔ℓ b)
+    _∈_ : A × B → FiniteMap → Set
     _∈_ k,v (m₁ , _) = k,v ∈ˡ (proj₁ m₁)
 
-    _∈k_ : A → FiniteMap → Set a
+    _∈k_ : A → FiniteMap → Set
     _∈k_ k (m₁ , _) = k ∈ˡ (keysᵐ m₁)
 
     open Map using (forget) public
@@ -108,7 +131,7 @@ module WithKeys (ks : List A) where
 
     []-∈ : ∀ {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' 
+    []-∈ {k} {v} {ks'} (m , _) k∈ks' k,v∈fm = []ᵐ-∈ m k,v∈fm k∈ks'
 
     ≈-equiv : IsEquivalence FiniteMap _≈_
     ≈-equiv = record
@@ -120,46 +143,48 @@ module WithKeys (ks : List A) where
             λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} →
                 IsEquivalence.≈-trans ≈ᵐ-equiv {m₁} {m₂} {m₃}
         }
+    open IsEquivalence ≈-equiv public
 
-    isUnionSemilattice : IsSemilattice FiniteMap _≈_ _⊔_
+    instance
-    isUnionSemilattice = record
+        isUnionSemilattice : IsSemilattice FiniteMap _≈_ _⊔_
-        { ≈-equiv = ≈-equiv
+        isUnionSemilattice = record
-        ; ≈-⊔-cong =
+            { ≈-equiv = ≈-equiv
-            λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} {(m₄ , _)} m₁≈m₂ m₃≈m₄ →
+            ; ≈-⊔-cong =
-                ≈ᵐ-⊔ᵐ-cong {m₁} {m₂} {m₃} {m₄} m₁≈m₂ m₃≈m₄
+                λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} {(m₄ , _)} m₁≈m₂ m₃≈m₄ →
-        ; ⊔-assoc = λ (m₁ , _) (m₂ , _) (m₃ , _) → ⊔ᵐ-assoc m₁ m₂ m₃
+                    ≈ᵐ-⊔ᵐ-cong {m₁} {m₂} {m₃} {m₄} m₁≈m₂ m₃≈m₄
-        ; ⊔-comm = λ (m₁ , _) (m₂ , _) → ⊔ᵐ-comm m₁ m₂
+            ; ⊔-assoc = λ (m₁ , _) (m₂ , _) (m₃ , _) → ⊔ᵐ-assoc m₁ m₂ m₃
-        ; ⊔-idemp = λ (m , _) → ⊔ᵐ-idemp m
+            ; ⊔-comm = λ (m₁ , _) (m₂ , _) → ⊔ᵐ-comm m₁ m₂
-        }
+            ; ⊔-idemp = λ (m , _) → ⊔ᵐ-idemp m
+            }
 
-    isIntersectSemilattice : IsSemilattice FiniteMap _≈_ _⊓_
+        isIntersectSemilattice : IsSemilattice FiniteMap _≈_ _⊓_
-    isIntersectSemilattice = record
+        isIntersectSemilattice = record
-        { ≈-equiv = ≈-equiv
+            { ≈-equiv = ≈-equiv
-        ; ≈-⊔-cong =
+            ; ≈-⊔-cong =
-            λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} {(m₄ , _)} m₁≈m₂ m₃≈m₄ →
+                λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} {(m₄ , _)} m₁≈m₂ m₃≈m₄ →
-                ≈ᵐ-⊓ᵐ-cong {m₁} {m₂} {m₃} {m₄} m₁≈m₂ m₃≈m₄
+                    ≈ᵐ-⊓ᵐ-cong {m₁} {m₂} {m₃} {m₄} m₁≈m₂ m₃≈m₄
-        ; ⊔-assoc = λ (m₁ , _) (m₂ , _) (m₃ , _) → ⊓ᵐ-assoc m₁ m₂ m₃
+            ; ⊔-assoc = λ (m₁ , _) (m₂ , _) (m₃ , _) → ⊓ᵐ-assoc m₁ m₂ m₃
-        ; ⊔-comm = λ (m₁ , _) (m₂ , _) → ⊓ᵐ-comm m₁ m₂
+            ; ⊔-comm = λ (m₁ , _) (m₂ , _) → ⊓ᵐ-comm m₁ m₂
-        ; ⊔-idemp = λ (m , _) → ⊓ᵐ-idemp m
+            ; ⊔-idemp = λ (m , _) → ⊓ᵐ-idemp m
-        }
+            }
 
-    isLattice : IsLattice FiniteMap _≈_ _⊔_ _⊓_
+        isLattice : IsLattice FiniteMap _≈_ _⊔_ _⊓_
-    isLattice = record
+        isLattice = record
-        { joinSemilattice = isUnionSemilattice
+            { joinSemilattice = isUnionSemilattice
-        ; meetSemilattice = isIntersectSemilattice
+            ; meetSemilattice = isIntersectSemilattice
-        ; absorb-⊔-⊓ = λ (m₁ , _) (m₂ , _) → absorb-⊔ᵐ-⊓ᵐ m₁ m₂
+            ; absorb-⊔-⊓ = λ (m₁ , _) (m₂ , _) → absorb-⊔ᵐ-⊓ᵐ m₁ m₂
-        ; absorb-⊓-⊔ = λ (m₁ , _) (m₂ , _) → absorb-⊓ᵐ-⊔ᵐ m₁ m₂
+            ; absorb-⊓-⊔ = λ (m₁ , _) (m₂ , _) → absorb-⊓ᵐ-⊔ᵐ m₁ m₂
-        }
+            }
 
-    open IsLattice isLattice using (_≼_; ⊔-Monotonicˡ; ⊔-Monotonicʳ) public
+        lattice : Lattice FiniteMap
+        lattice = record
+            { _≈_ = _≈_
+            ; _⊔_ = _⊔_
+            ; _⊓_ = _⊓_
+            ; isLattice = isLattice
+            }
 
-    lattice : Lattice FiniteMap
+    open IsLattice isLattice using (_≼_; ⊔-idemp; ⊔-Monotonicˡ; ⊔-Monotonicʳ) public
-    lattice = record
-        { _≈_ = _≈_
-        ; _⊔_ = _⊔_
-        ; _⊓_ = _⊓_
-        ; 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₂
@@ -173,7 +198,7 @@ module WithKeys (ks : List A) where
     module GeneralizedUpdate
              {l} {L : Set l}
              {_≈ˡ_ : L → L → Set l} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L}
-             (lL : IsLattice L _≈ˡ_ _⊔ˡ_ _⊓ˡ_)
+             {{lL : IsLattice L _≈ˡ_ _⊔ˡ_ _⊓ˡ_}}
              (f : L → FiniteMap) (f-Monotonic : Monotonic (IsLattice._≼_ lL) _≼_ f)
              (g : A → L → B) (g-Monotonicʳ : ∀ k → Monotonic (IsLattice._≼_ lL) _≼₂_ (g k))
              (ks : List A) where
@@ -187,7 +212,7 @@ module WithKeys (ks : List A) where
         f' l = (f l) updating ks via (updater l)
 
         f'-Monotonic : Monotonic _≼ˡ_ _≼_ f'
-        f'-Monotonic {l₁} {l₂} l₁≼l₂ = f'-Monotonicᵐ lL (proj₁ ∘ f) f-Monotonic g g-Monotonicʳ ks l₁≼l₂
+        f'-Monotonic {l₁} {l₂} l₁≼l₂ = f'-Monotonicᵐ (proj₁ ∘ f) f-Monotonic g g-Monotonicʳ ks l₁≼l₂
 
         f'-∈k-forward : ∀ {k l} → k ∈k (f l) → k ∈k (f' l)
         f'-∈k-forward {k} {l} = updatingᵐ-via-∈k-forward (proj₁ (f l)) ks (updater l)
@@ -229,4 +254,382 @@ module WithKeys (ks : List A) where
     ...   | 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₁))
 
-open WithKeys public
+private
+    _⊆ᵐ_ : ∀ {ks₁ ks₂ : List A} → WithKeys.FiniteMap ks₁ → WithKeys.FiniteMap ks₂ → Set
+    _⊆ᵐ_ fm₁ fm₂ = subset-impl (proj₁ (proj₁ fm₁)) (proj₁ (proj₁ fm₂))
+
+    _∈ᵐ_ : ∀ {ks : List A} → A × B → WithKeys.FiniteMap ks → Set
+    _∈ᵐ_ {ks} = WithKeys._∈_ ks
+
+FromBothMaps : ∀ (k : A) (v : B) {ks : List A} (fm₁ fm₂ : WithKeys.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₂ : WithKeys.FiniteMap ks) {k : A} {v : B} →
+                   (k , v) ∈ᵐ (WithKeys._⊔_ ks 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₁ ← (WithKeys.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₂ ← (WithKeys.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 module IterProdIsomorphism where
+    open WithKeys
+    open import Data.Unit using (tt)
+    open import Lattice.Unit using ()
+        renaming
+            ( _≈_ to _≈ᵘ_
+            ; _⊔_ to _⊔ᵘ_
+            ; _⊓_ to _⊓ᵘ_
+            ; ≈-Decidable to ≈ᵘ-Decidable
+            ; isLattice to isLatticeᵘ
+            ; ≈-equiv to ≈ᵘ-equiv
+            ; fixedHeight to fixedHeightᵘ
+            )
+    open import Lattice.IterProd B ⊤ _
+        as IP
+        using (IterProd)
+    open IsLattice lB using ()
+        renaming
+            ( ≈-trans to ≈₂-trans
+            ; ≈-sym to ≈₂-sym
+            ; FixedHeight to FixedHeight₂
+            )
+
+    from : ∀ {ks : List A} → FiniteMap ks → IterProd (length ks)
+    from {[]} (([] , _) , _) = tt
+    from {k ∷ ks'} (((k' , v) ∷ fm' , push _ uks') , refl) =
+        (v , from ((fm' , uks'), refl))
+
+    to : ∀ {ks : List A} → Unique ks → IterProd (length ks) → FiniteMap ks
+    to {[]} _ ⊤ = (([] , empty) , refl)
+    to {k ∷ ks'} (push k≢ks' uks') (v , rest) =
+        let
+            ((fm' , ufm') , fm'≡ks') = to uks' rest
+
+            -- This would be easier if we pattern matched on the equiality proof
+            -- to get refl, but that makes it harder to reason about 'to' when
+            -- the arguments are not known to be refl.
+            k≢fm' = subst (λ ks → All (λ k' → ¬ k ≡ k') ks) (sym fm'≡ks') k≢ks'
+            kvs≡ks = cong (k ∷_) fm'≡ks'
+        in
+            (((k , v) ∷ fm' , push k≢fm' ufm') , kvs≡ks)
+
+    _≈ⁱᵖ_ : ∀ {n : ℕ} → IterProd n → IterProd n → Set
+    _≈ⁱᵖ_ {n} = IP._≈_ {n}
+
+    _⊔ⁱᵖ_ : ∀ {ks : List A} →
+            IterProd (length ks) → IterProd (length ks) → IterProd (length ks)
+    _⊔ⁱᵖ_ {ks} = IP._⊔_ {length 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})
+                                 (from {ks}) (to {ks} uks)
+    from-to-inverseˡ {[]} _ _ = IsEquivalence.≈-refl (IP.≈-equiv {0})
+    from-to-inverseˡ {k ∷ ks'} (push k≢ks' uks') (v , rest)
+        with ((fm' , ufm') , refl) ← to uks' rest in p rewrite sym p =
+            (IsLattice.≈-refl lB , from-to-inverseˡ {ks'} uks' rest)
+            -- the rewrite here is needed because the IH is in terms of `to uks' rest`,
+            -- but we end up with the 'unpacked' form (fm', ...). So, put it back
+            -- in the 'packed' form after we've performed enough inspection
+            -- to know we take the cons branch of `to`.
+
+    -- The map has its own uniqueness proof, but the call to 'to' needs a standalone
+    -- uniqueness proof too. Work with both proofs as needed to thread things through.
+    --
+    -- The right inverse is: to (from x) = x
+    from-to-inverseʳ : ∀ {ks : List A} (uks : Unique ks) →
+                       IsInverseʳ (_≈_ ks) (_≈ⁱᵖ_ {length ks})
+                                  (from {ks}) (to {ks} uks)
+    from-to-inverseʳ {[]} _ (([] , empty) , kvs≡ks) rewrite kvs≡ks =
+        ( (λ k v ())
+        , (λ k v ())
+        )
+    from-to-inverseʳ {k ∷ ks'} uks@(push _ uks'₁) fm₁@(((k , v) ∷ fm'₁ , push _ uks'₂) , refl)
+        with to uks'₁ (from ((fm'₁ , uks'₂) , refl))
+          | from-to-inverseʳ {ks'} uks'₁ ((fm'₁ , uks'₂) , refl)
+    ...   | ((fm'₂ , ufm'₂) , _)
+          | (fm'₂⊆fm'₁ , fm'₁⊆fm'₂) = (m₂⊆m₁ , m₁⊆m₂)
+                where
+                    kvs₁ = (k , v) ∷ fm'₁
+                    kvs₂ = (k , v) ∷ fm'₂
+
+                    m₁⊆m₂ : subset-impl kvs₁ kvs₂
+                    m₁⊆m₂ k' v' (here refl) =
+                        (v' , (IsLattice.≈-refl lB , here refl))
+                    m₁⊆m₂ k' v' (there k',v'∈fm'₁) =
+                        let (v'' , (v'≈v'' , k',v''∈fm'₂)) =
+                                fm'₁⊆fm'₂ k' v' k',v'∈fm'₁
+                        in (v'' , (v'≈v'' , there k',v''∈fm'₂))
+
+                    m₂⊆m₁ : subset-impl kvs₂ kvs₁
+                    m₂⊆m₁ k' v' (here refl) =
+                        (v' , (IsLattice.≈-refl lB , here refl))
+                    m₂⊆m₁ k' v' (there k',v'∈fm'₂) =
+                        let (v'' , (v'≈v'' , k',v''∈fm'₁)) =
+                                fm'₂⊆fm'₁ k' v' k',v'∈fm'₂
+                        in (v'' , (v'≈v'' , there k',v''∈fm'₁))
+
+    private
+        first-key-in-map : ∀ {k : A} {ks : List A} (fm : FiniteMap (k ∷ ks)) →
+                           Σ B (λ v → (k , v) ∈ᵐ fm)
+        first-key-in-map (((k , v) ∷ _ , _) , refl) = (v , here refl)
+
+        from-first-value : ∀ {k : A} {ks : List A} (fm : FiniteMap (k ∷ ks)) →
+                           proj₁ (from fm) ≡ proj₁ (first-key-in-map fm)
+        from-first-value {k} {ks} (((k , v) ∷ _ , push _ _) , refl) = refl
+
+        -- We need pop because reasoning about two distinct 'refl' pattern
+        -- matches is giving us unification errors. So, stash the 'refl' pattern
+        -- matching into a helper functions, and write solutions in terms
+        -- of that.
+        pop : ∀ {k : A} {ks : List A} → FiniteMap (k ∷ ks) → FiniteMap ks
+        pop (((_ ∷ fm') , push _ ufm') , refl) = ((fm' , ufm') , refl)
+
+        pop-≈ : ∀ {k : A} {ks : List A} (fm₁ fm₂ : FiniteMap (k ∷ ks)) →
+                _≈_ _ fm₁ fm₂ →  _≈_ _ (pop fm₁) (pop fm₂)
+        pop-≈ {k} {ks} fm₁ fm₂ (fm₁⊆fm₂ , fm₂⊆fm₁) =
+            (narrow fm₁⊆fm₂ , narrow fm₂⊆fm₁)
+            where
+                narrow₁ : ∀ {fm₁ fm₂ : FiniteMap (k ∷ ks)} →
+                         fm₁ ⊆ᵐ fm₂ → pop fm₁ ⊆ᵐ fm₂
+                narrow₁ {(_ ∷ _ , push _ _) , refl} kvs₁⊆kvs₂ k' v' k',v'∈fm'₁ =
+                    kvs₁⊆kvs₂ k' v' (there k',v'∈fm'₁)
+
+                narrow₂ : ∀ {fm₁ : FiniteMap ks} {fm₂ : FiniteMap (k ∷ ks)} →
+                          fm₁ ⊆ᵐ fm₂  → fm₁ ⊆ᵐ pop fm₂
+                narrow₂ {fm₁} {fm₂ = (_ ∷ fm'₂ , push k≢ks _) , kvs≡ks@refl} kvs₁⊆kvs₂ k' v' k',v'∈fm'₁
+                    with kvs₁⊆kvs₂ k' v' k',v'∈fm'₁
+                ...   | (v'' , (v'≈v'' , here refl)) rewrite sym (proj₂ fm₁) =
+                        ⊥-elim (All¬-¬Any k≢ks (forget k',v'∈fm'₁))
+                ...   | (v'' , (v'≈v'' , there k',v'∈fm'₂)) =
+                        (v'' , (v'≈v'' , k',v'∈fm'₂))
+
+                narrow : ∀ {fm₁ fm₂ : FiniteMap (k ∷ ks)} →
+                         fm₁ ⊆ᵐ fm₂ → pop fm₁ ⊆ᵐ pop fm₂
+                narrow {fm₁} {fm₂} x = narrow₂ {pop fm₁} (narrow₁ {fm₂ = fm₂} x)
+
+        k,v∈pop⇒k,v∈ : ∀ {k : A} {ks : List A} {k' : A} {v : B} (fm : FiniteMap (k ∷ ks)) →
+                       (k' , v) ∈ᵐ pop fm → (¬ k ≡ k' × ((k' , v) ∈ᵐ fm))
+        k,v∈pop⇒k,v∈ {k} {ks} {k'} {v} (m@((k , _) ∷ fm' , push k≢ks uks') , refl) k',v∈fm =
+            ( (λ { refl → All¬-¬Any k≢ks (forget k',v∈fm) })
+            , there k',v∈fm
+            )
+
+        k,v∈⇒k,v∈pop : ∀ {k : A} {ks : List A} {k' : A} {v : B} (fm : FiniteMap (k ∷ ks)) →
+                       ¬ k ≡ k' → (k' , v) ∈ᵐ fm → (k' , v) ∈ᵐ pop fm
+        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'
+
+        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₂ , _) =
+            (pfm₁fm₂⊆pfm₁pfm₂ , pfm₁pfm₂⊆pfm₁fm₂)
+            where
+                -- pfm₁fm₂⊆pfm₁pfm₂ = {!!}
+                pfm₁fm₂⊆pfm₁pfm₂ : pop (_⊔_ _ fm₁ fm₂) ⊆ᵐ (_⊔_ _ (pop fm₁) (pop fm₂))
+                pfm₁fm₂⊆pfm₁pfm₂ k' v' k',v'∈pfm₁fm₂
+                    with (k≢k' , k',v'∈fm₁fm₂) ← k,v∈pop⇒k,v∈ (_⊔_ _ fm₁ fm₂) k',v'∈pfm₁fm₂
+                    with ((v₁ , v₂) , (refl , (k,v₁∈fm₁ , k,v₂∈fm₂)))
+                         ← Provenance-union fm₁ fm₂ k',v'∈fm₁fm₂
+                    with k',v₁∈pfm₁ ← k,v∈⇒k,v∈pop fm₁ k≢k' k,v₁∈fm₁
+                    with k',v₂∈pfm₂ ← k,v∈⇒k,v∈pop fm₂ k≢k' k,v₂∈fm₂
+                    =
+                        ( v₁ ⊔₂ v₂
+                        , (IsLattice.≈-refl lB
+                          , ⊔-combines {m₁ = proj₁ (pop fm₁)}
+                                       {m₂ = proj₁ (pop fm₂)}
+                                       k',v₁∈pfm₁ k',v₂∈pfm₂
+                          )
+                        )
+
+                pfm₁pfm₂⊆pfm₁fm₂ : (_⊔_ _ (pop fm₁) (pop fm₂)) ⊆ᵐ pop (_⊔_ _ fm₁ fm₂)
+                pfm₁pfm₂⊆pfm₁fm₂ k' v' k',v'∈pfm₁pfm₂
+                    with ((v₁ , v₂) , (refl , (k,v₁∈pfm₁ , k,v₂∈pfm₂)))
+                         ← Provenance-union (pop fm₁) (pop fm₂) k',v'∈pfm₁pfm₂
+                    with (k≢k' , k',v₁∈fm₁) ← k,v∈pop⇒k,v∈ fm₁ k,v₁∈pfm₁
+                    with (_    , k',v₂∈fm₂) ← k,v∈pop⇒k,v∈ fm₂ k,v₂∈pfm₂
+                    =
+                        ( v₁ ⊔₂ v₂
+                        , ( IsLattice.≈-refl lB
+                          , k,v∈⇒k,v∈pop (_⊔_ _ fm₁ fm₂) k≢k'
+                                         (⊔-combines {m₁ = m₁} {m₂ = m₂}
+                                                     k',v₁∈fm₁ k',v₂∈fm₂)
+                          )
+                        )
+
+        from-rest : ∀ {k : A} {ks : List A} (fm : FiniteMap (k ∷ ks)) →
+                    proj₂ (from fm) ≡ from (pop fm)
+        from-rest (((_ ∷ fm') , push _ ufm') , refl) = refl
+
+    from-preserves-≈ : ∀ {ks : List A} → {fm₁ fm₂ : FiniteMap ks} →
+                       _≈_ _ fm₁ fm₂ → (_≈ⁱᵖ_ {length ks}) (from fm₁) (from fm₂)
+    from-preserves-≈ {[]} {_} {_} _ = IsEquivalence.≈-refl ≈ᵘ-equiv
+    from-preserves-≈ {k ∷ ks'} {fm₁@(m₁ , _)} {fm₂@(m₂ , _)} fm₁≈fm₂@(kvs₁⊆kvs₂ , kvs₂⊆kvs₁)
+        with first-key-in-map fm₁
+          | first-key-in-map fm₂
+          | from-first-value fm₁
+          | from-first-value fm₂
+    ...   | (v₁ , k,v₁∈fm₁) | (v₂ , k,v₂∈fm₂) | refl | refl
+            with kvs₁⊆kvs₂ _ _ k,v₁∈fm₁
+    ...       | (v₁' , (v₁≈v₁' , k,v₁'∈fm₂))
+                rewrite Map-functional {m = m₂} k,v₂∈fm₂ k,v₁'∈fm₂
+                rewrite from-rest fm₁ rewrite from-rest fm₂
+                =
+                    ( v₁≈v₁'
+                    , from-preserves-≈ {ks'} {pop fm₁} {pop fm₂}
+                                       (pop-≈ fm₁ fm₂ fm₁≈fm₂)
+                    )
+
+    to-preserves-≈ : ∀ {ks : List A} (uks : Unique ks) {ip₁ ip₂ : IterProd (length ks)} →
+                     _≈ⁱᵖ_ {length ks} ip₁ ip₂ → _≈_ _ (to uks ip₁) (to uks ip₂)
+    to-preserves-≈ {[]} empty {tt} {tt} _ = ((λ k v ()), (λ k v ()))
+    to-preserves-≈ {k ∷ ks'} uks@(push k≢ks' uks') {ip₁@(v₁ , rest₁)} {ip₂@(v₂ , rest₂)} (v₁≈v₂ , rest₁≈rest₂) = (fm₁⊆fm₂ , fm₂⊆fm₁)
+        where
+            inductive-step : ∀ {v₁ v₂ : B} {rest₁ rest₂ : IterProd (length ks')} →
+                               v₁ ≈₂ v₂ → _≈ⁱᵖ_ {length ks'} rest₁ rest₂ →
+                               to uks (v₁ , rest₁) ⊆ᵐ to uks (v₂ , rest₂)
+            inductive-step {v₁} {v₂} {rest₁} {rest₂} v₁≈v₂ rest₁≈rest₂ k v k,v∈kvs₁
+                with ((fm'₁ , ufm'₁) , fm'₁≡ks') ← to uks' rest₁ in p₁
+                with ((fm'₂ , ufm'₂) , fm'₂≡ks') ← to uks' rest₂ in p₂
+                with k,v∈kvs₁
+            ...   | here refl = (v₂ , (v₁≈v₂ , here refl))
+            ...   | there k,v∈fm'₁ with refl ← p₁ with refl ← p₂ =
+                    let
+                        (fm'₁⊆fm'₂ , _) = to-preserves-≈ uks' {rest₁} {rest₂}
+                                                         rest₁≈rest₂
+                        (v' , (v≈v' , k,v'∈kvs₁)) = fm'₁⊆fm'₂ k v k,v∈fm'₁
+                    in
+                        (v' , (v≈v' , there k,v'∈kvs₁))
+
+            fm₁⊆fm₂ : to uks ip₁ ⊆ᵐ to uks ip₂
+            fm₁⊆fm₂ = inductive-step v₁≈v₂ rest₁≈rest₂
+
+            fm₂⊆fm₁ : to uks ip₂ ⊆ᵐ to uks ip₁
+            fm₂⊆fm₁ = inductive-step (≈₂-sym v₁≈v₂)
+                                     (IP.≈-sym {length ks'} rest₁≈rest₂)
+
+    from-⊔-distr : ∀ {ks : List A} → (fm₁ fm₂ : FiniteMap ks) →
+                  _≈ⁱᵖ_ {length ks} (from (_⊔_ _ fm₁ fm₂))
+                                    (_⊔ⁱᵖ_ {ks} (from fm₁) (from fm₂))
+    from-⊔-distr {[]} fm₁ fm₂ = IsEquivalence.≈-refl ≈ᵘ-equiv
+    from-⊔-distr {k ∷ ks} fm₁@(m₁ , _) fm₂@(m₂ , _)
+        with first-key-in-map (_⊔_ _ fm₁ fm₂)
+          | first-key-in-map fm₁
+          | first-key-in-map fm₂
+          | from-first-value (_⊔_ _ fm₁ fm₂)
+          | from-first-value fm₁ | from-first-value fm₂
+    ...   | (v , k,v∈fm₁fm₂) | (v₁ , k,v₁∈fm₁) | (v₂ , k,v₂∈fm₂) | refl | refl | refl
+            with Expr-Provenance k ((` m₁) ∪ (` m₂)) (forget k,v∈fm₁fm₂)
+    ...       | (_ , (in₁ _ k∉km₂ , _)) = ⊥-elim (k∉km₂ (forget k,v₂∈fm₂))
+    ...       | (_ , (in₂ k∉km₁ _ , _)) = ⊥-elim (k∉km₁ (forget k,v₁∈fm₁))
+    ...       | (v₁⊔v₂ , (bothᵘ {v₁'} {v₂'} (single k,v₁'∈m₁) (single k,v₂'∈m₂) , k,v₁⊔v₂∈m₁m₂))
+                rewrite Map-functional {m = m₁} k,v₁∈fm₁ k,v₁'∈m₁
+                rewrite Map-functional {m = m₂} k,v₂∈fm₂ k,v₂'∈m₂
+                rewrite Map-functional {m = proj₁ (_⊔_ _ fm₁ fm₂)} k,v∈fm₁fm₂ k,v₁⊔v₂∈m₁m₂
+                rewrite from-rest (_⊔_ _ fm₁ fm₂) rewrite from-rest fm₁ rewrite from-rest fm₂
+                = ( IsLattice.≈-refl lB
+                  , IsEquivalence.≈-trans
+                        (IP.≈-equiv {length ks})
+                        (from-preserves-≈ {_} {pop (_⊔_ _ fm₁ fm₂)}
+                                              {_⊔_ _ (pop fm₁) (pop fm₂)}
+                                              (pop-⊔-distr fm₁ fm₂))
+                        ((from-⊔-distr (pop fm₁) (pop fm₂)))
+                  )
+
+
+    to-⊔-distr : ∀ {ks : List A} (uks : Unique ks) → (ip₁ ip₂ : IterProd (length ks)) →
+                 _≈_ _ (to uks (_⊔ⁱᵖ_ {ks} ip₁ ip₂)) ((_⊔_ _ (to uks ip₁) (to uks ip₂)))
+    to-⊔-distr {[]} empty tt tt = ((λ k v ()), (λ k v ()))
+    to-⊔-distr {ks@(k ∷ ks')} uks@(push k≢ks' uks') ip₁@(v₁ , rest₁) ip₂@(v₂ , rest₂) = (fm⊆fm₁fm₂ , fm₁fm₂⊆fm)
+        where
+            fm₁ = to uks ip₁
+            fm₁' = to uks' rest₁
+            fm₂ = to uks ip₂
+            fm₂' = to uks' rest₂
+            fm = to uks (_⊔ⁱᵖ_ {k ∷ ks'} ip₁ ip₂)
+
+            fm⊆fm₁fm₂ : fm ⊆ᵐ (_⊔_ _ fm₁ fm₂)
+            fm⊆fm₁fm₂ k v (here refl) =
+                (v₁ ⊔₂ v₂
+                , (IsLattice.≈-refl lB
+                  , ⊔-combines {k} {v₁} {v₂} {proj₁ fm₁} {proj₁ fm₂}
+                               (here refl) (here refl)
+                  )
+                )
+            fm⊆fm₁fm₂ k' v (there k',v∈fm')
+                with (fm'⊆fm'₁fm'₂ , _) ← to-⊔-distr uks' rest₁ rest₂
+                with (v' , (v₁⊔v₂≈v' , k',v'∈fm'₁fm'₂))
+                     ← fm'⊆fm'₁fm'₂ k' v k',v∈fm'
+                with (_ , (refl , (v₁∈fm'₁ , v₂∈fm'₂)))
+                     ← Provenance-union fm₁' fm₂' k',v'∈fm'₁fm'₂ =
+                ( v'
+                , ( v₁⊔v₂≈v'
+                  , ⊔-combines {m₁ = proj₁ fm₁} {m₂ = proj₁ fm₂}
+                               (there v₁∈fm'₁) (there v₂∈fm'₂)
+                  )
+                )
+
+            fm₁fm₂⊆fm : (_⊔_ _ fm₁ fm₂) ⊆ᵐ fm
+            fm₁fm₂⊆fm k' v k',v∈fm₁fm₂
+                with (_ , fm'₁fm'₂⊆fm')
+                     ← to-⊔-distr uks' rest₁ rest₂
+                with (_ , (refl , (v₁∈fm₁ , v₂∈fm₂)))
+                     ← Provenance-union fm₁ fm₂ k',v∈fm₁fm₂
+                with v₁∈fm₁ | v₂∈fm₂
+            ...   | here refl | here refl =
+                    (v , (IsLattice.≈-refl lB , here refl))
+            ...   | here refl | there k',v₂∈fm₂' =
+                    ⊥-elim (All¬-¬Any k≢ks' (subst (k' ∈ˡ_) (proj₂ fm₂')
+                                                   (forget k',v₂∈fm₂')))
+            ...   | there k',v₁∈fm₁' | here refl =
+                    ⊥-elim (All¬-¬Any k≢ks' (subst (k' ∈ˡ_) (proj₂ fm₁')
+                                                   (forget k',v₁∈fm₁')))
+            ...   | there k',v₁∈fm₁' | there k',v₂∈fm₂' =
+                        let
+                            k',v₁v₂∈fm₁'fm₂' =
+                                ⊔-combines {m₁ = proj₁ fm₁'} {m₂ = proj₁ fm₂'}
+                                           k',v₁∈fm₁' k',v₂∈fm₂'
+                            (v' , (v₁⊔v₂≈v' , v'∈fm')) =
+                                fm'₁fm'₂⊆fm' _ _ k',v₁v₂∈fm₁'fm₂'
+                        in
+                            (v' , (v₁⊔v₂≈v' , there v'∈fm'))
+
+    module FixedHeight {ks : List A} {{≈₂-Decidable : IsDecidable _≈₂_}} {h₂ : ℕ} {{fhB : FixedHeight₂ h₂}} (uks : Unique ks) where
+        import Isomorphism
+        open Isomorphism.TransportFiniteHeight
+            (IP.isFiniteHeightLattice {k = length ks} {{fhB = fixedHeightᵘ}}) (isLattice ks)
+            {f = to uks} {g = from {ks}}
+            (to-preserves-≈ uks) (from-preserves-≈ {ks})
+            (to-⊔-distr uks) (from-⊔-distr {ks})
+            (from-to-inverseʳ uks) (from-to-inverseˡ uks)
+            using (isFiniteHeightLattice; finiteHeightLattice; fixedHeight) 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} {{fhB = fixedHeightᵘ}} =
+            to-build uks k v k,v∈⊥
+
+open WithKeys ks public
+module FixedHeight = IterProdIsomorphism.FixedHeight

Lattice/FiniteValueMap.agda

@@ -1,427 +0,0 @@
--- Because iterated products currently require both A and B to be of the same
--- universe, and the FiniteMap is written in a universe-polymorphic way,
--- specialize the FiniteMap module with Set-typed types only.
-
-open import Lattice
-open import Equivalence
-open import Relation.Binary.PropositionalEquality as Eq
-    using (_≡_; refl; sym; trans; cong; subst)
-open import Relation.Binary.Definitions using (Decidable)
-open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
-open import Function.Definitions using (Inverseˡ; Inverseʳ)
-
-module Lattice.FiniteValueMap {A : Set} {B : Set}
-    {_≈₂_ : B → B → Set}
-    {_⊔₂_ : B → B → B} {_⊓₂_ : B → B → B}
-    (≡-dec-A : Decidable (_≡_ {_} {A}))
-    (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
-
-open import Data.List using (List; length; []; _∷_; map)
-open import Data.List.Membership.Propositional using () renaming (_∈_ to _∈ˡ_)
-open import Data.Nat using (ℕ)
-open import Data.Product using (Σ; proj₁; proj₂; _×_)
-open import Data.Empty using (⊥-elim)
-open import Utils using (Unique; push; empty; All¬-¬Any)
-open import Data.Product using (_,_)
-open import Data.List.Properties using (∷-injectiveʳ)
-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
-        ( subset-impl
-        ; locate
-        ; Map-functional
-        ; Expr-Provenance
-        ; Expr-Provenance-≡
-        ; _∩_; _∪_; `_
-        ; in₁; in₂; bothᵘ; single
-        ; ⊔-combines
-        )
-open import Lattice.FiniteMap ≡-dec-A lB public
-
-module IterProdIsomorphism where
-    open import Data.Unit using (⊤; tt)
-    open import Lattice.Unit using ()
-        renaming
-            ( _≈_ to _≈ᵘ_
-            ; _⊔_ to _⊔ᵘ_
-            ; _⊓_ to _⊓ᵘ_
-            ; ≈-dec to ≈ᵘ-dec
-            ; isLattice to isLatticeᵘ
-            ; ≈-equiv to ≈ᵘ-equiv
-            ; fixedHeight to fixedHeightᵘ
-            )
-    open import Lattice.IterProd _≈₂_ _≈ᵘ_ _⊔₂_ _⊔ᵘ_ _⊓₂_ _⊓ᵘ_ lB isLatticeᵘ
-        as IP
-        using (IterProd)
-    open IsLattice lB using ()
-        renaming
-            ( ≈-trans to ≈₂-trans
-            ; ≈-sym to ≈₂-sym
-            ; FixedHeight to FixedHeight₂
-            )
-
-    from : ∀ {ks : List A} → FiniteMap ks → IterProd (length ks)
-    from {[]} (([] , _) , _) = tt
-    from {k ∷ ks'} (((k' , v) ∷ fm' , push _ uks') , refl) =
-        (v , from ((fm' , uks'), refl))
-
-    to : ∀ {ks : List A} → Unique ks → IterProd (length ks) → FiniteMap ks
-    to {[]} _ ⊤ = (([] , empty) , refl)
-    to {k ∷ ks'} (push k≢ks' uks') (v , rest) =
-        let
-            ((fm' , ufm') , fm'≡ks') = to uks' rest
-
-            -- This would be easier if we pattern matched on the equiality proof
-            -- to get refl, but that makes it harder to reason about 'to' when
-            -- the arguments are not known to be refl.
-            k≢fm' = subst (λ ks → All (λ k' → ¬ k ≡ k') ks) (sym fm'≡ks') k≢ks'
-            kvs≡ks = cong (k ∷_) fm'≡ks'
-        in
-            (((k , v) ∷ fm' , push k≢fm' ufm') , kvs≡ks)
-
-
-    private
-        _≈ᵐ_ : ∀ {ks : List A} → FiniteMap ks → FiniteMap ks → Set
-        _≈ᵐ_ {ks} = _≈_ ks
-
-        _⊔ᵐ_ : ∀ {ks : List A} → FiniteMap ks → FiniteMap ks → FiniteMap ks
-        _⊔ᵐ_ {ks} = _⊔_ ks
-
-        _⊆ᵐ_ : ∀ {ks₁ ks₂ : List A} → FiniteMap ks₁ → FiniteMap ks₂ → Set
-        _⊆ᵐ_ fm₁ fm₂ = subset-impl (proj₁ (proj₁ fm₁)) (proj₁ (proj₁ fm₂))
-
-        _≈ⁱᵖ_ : ∀ {n : ℕ} → IterProd n → IterProd n → Set
-        _≈ⁱᵖ_ {n} = IP._≈_ n
-
-        _⊔ⁱᵖ_ : ∀ {ks : List A} →
-                IterProd (length ks) → IterProd (length ks) → IterProd (length ks)
-        _⊔ⁱᵖ_ {ks} = IP._⊔_ (length ks)
-
-        _∈ᵐ_ : ∀ {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})
-                                 (from {ks}) (to {ks} uks)
-    from-to-inverseˡ {[]} _ _ = IsEquivalence.≈-refl (IP.≈-equiv 0)
-    from-to-inverseˡ {k ∷ ks'} (push k≢ks' uks') (v , rest)
-        with ((fm' , ufm') , refl) ← to uks' rest in p rewrite sym p =
-            (IsLattice.≈-refl lB , from-to-inverseˡ {ks'} uks' rest)
-            -- the rewrite here is needed because the IH is in terms of `to uks' rest`,
-            -- but we end up with the 'unpacked' form (fm', ...). So, put it back
-            -- in the 'packed' form after we've performed enough inspection
-            -- to know we take the cons branch of `to`.
-
-    -- The map has its own uniqueness proof, but the call to 'to' needs a standalone
-    -- uniqueness proof too. Work with both proofs as needed to thread things through.
-    --
-    -- The right inverse is: to (from x) = x
-    from-to-inverseʳ : ∀ {ks : List A} (uks : Unique ks) →
-                       IsInverseʳ (_≈ᵐ_ {ks}) (_≈ⁱᵖ_ {length ks})
-                                  (from {ks}) (to {ks} uks)
-    from-to-inverseʳ {[]} _ (([] , empty) , kvs≡ks) rewrite kvs≡ks =
-        ( (λ k v ())
-        , (λ k v ())
-        )
-    from-to-inverseʳ {k ∷ ks'} uks@(push _ uks'₁) fm₁@(((k , v) ∷ fm'₁ , push _ uks'₂) , refl)
-        with to uks'₁ (from ((fm'₁ , uks'₂) , refl))
-          | from-to-inverseʳ {ks'} uks'₁ ((fm'₁ , uks'₂) , refl)
-    ...   | ((fm'₂ , ufm'₂) , _)
-          | (fm'₂⊆fm'₁ , fm'₁⊆fm'₂) = (m₂⊆m₁ , m₁⊆m₂)
-                where
-                    kvs₁ = (k , v) ∷ fm'₁
-                    kvs₂ = (k , v) ∷ fm'₂
-
-                    m₁⊆m₂ : subset-impl kvs₁ kvs₂
-                    m₁⊆m₂ k' v' (here refl) =
-                        (v' , (IsLattice.≈-refl lB , here refl))
-                    m₁⊆m₂ k' v' (there k',v'∈fm'₁) =
-                        let (v'' , (v'≈v'' , k',v''∈fm'₂)) =
-                                fm'₁⊆fm'₂ k' v' k',v'∈fm'₁
-                        in (v'' , (v'≈v'' , there k',v''∈fm'₂))
-
-                    m₂⊆m₁ : subset-impl kvs₂ kvs₁
-                    m₂⊆m₁ k' v' (here refl) =
-                        (v' , (IsLattice.≈-refl lB , here refl))
-                    m₂⊆m₁ k' v' (there k',v'∈fm'₂) =
-                        let (v'' , (v'≈v'' , k',v''∈fm'₁)) =
-                                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)
-        first-key-in-map (((k , v) ∷ _ , _) , refl) = (v , here refl)
-
-        from-first-value : ∀ {k : A} {ks : List A} (fm : FiniteMap (k ∷ ks)) →
-                           proj₁ (from fm) ≡ proj₁ (first-key-in-map fm)
-        from-first-value {k} {ks} (((k , v) ∷ _ , push _ _) , refl) = refl
-
-        -- We need pop because reasoning about two distinct 'refl' pattern
-        -- matches is giving us unification errors. So, stash the 'refl' pattern
-        -- matching into a helper functions, and write solutions in terms
-        -- of that.
-        pop : ∀ {k : A} {ks : List A} → FiniteMap (k ∷ ks) → FiniteMap ks
-        pop (((_ ∷ fm') , push _ ufm') , refl) = ((fm' , ufm') , refl)
-
-        pop-≈ : ∀ {k : A} {ks : List A} (fm₁ fm₂ : FiniteMap (k ∷ ks)) →
-                fm₁ ≈ᵐ fm₂ → pop fm₁ ≈ᵐ pop fm₂
-        pop-≈ {k} {ks} fm₁ fm₂ (fm₁⊆fm₂ , fm₂⊆fm₁) =
-            (narrow fm₁⊆fm₂ , narrow fm₂⊆fm₁)
-            where
-                narrow₁ : ∀ {fm₁ fm₂ : FiniteMap (k ∷ ks)} →
-                         fm₁ ⊆ᵐ fm₂ → pop fm₁ ⊆ᵐ fm₂
-                narrow₁ {(_ ∷ _ , push _ _) , refl} kvs₁⊆kvs₂ k' v' k',v'∈fm'₁ =
-                    kvs₁⊆kvs₂ k' v' (there k',v'∈fm'₁)
-
-                narrow₂ : ∀ {fm₁ : FiniteMap ks} {fm₂ : FiniteMap (k ∷ ks)} →
-                          fm₁ ⊆ᵐ fm₂  → fm₁ ⊆ᵐ pop fm₂
-                narrow₂ {fm₁} {fm₂ = (_ ∷ fm'₂ , push k≢ks _) , kvs≡ks@refl} kvs₁⊆kvs₂ k' v' k',v'∈fm'₁
-                    with kvs₁⊆kvs₂ k' v' k',v'∈fm'₁
-                ...   | (v'' , (v'≈v'' , here refl)) rewrite sym (proj₂ fm₁) =
-                        ⊥-elim (All¬-¬Any k≢ks (forget k',v'∈fm'₁))
-                ...   | (v'' , (v'≈v'' , there k',v'∈fm'₂)) =
-                        (v'' , (v'≈v'' , k',v'∈fm'₂))
-
-                narrow : ∀ {fm₁ fm₂ : FiniteMap (k ∷ ks)} →
-                         fm₁ ⊆ᵐ fm₂ → pop fm₁ ⊆ᵐ pop fm₂
-                narrow {fm₁} {fm₂} x = narrow₂ {pop fm₁} (narrow₁ {fm₂ = fm₂} x)
-
-        k,v∈pop⇒k,v∈ : ∀ {k : A} {ks : List A} {k' : A} {v : B} (fm : FiniteMap (k ∷ ks)) →
-                       (k' , v) ∈ᵐ pop fm → (¬ k ≡ k' × ((k' , v) ∈ᵐ fm))
-        k,v∈pop⇒k,v∈ {k} {ks} {k'} {v} (m@((k , _) ∷ fm' , push k≢ks uks') , refl) k',v∈fm =
-            ( (λ { refl → All¬-¬Any k≢ks (forget k',v∈fm) })
-            , there k',v∈fm
-            )
-
-        k,v∈⇒k,v∈pop : ∀ {k : A} {ks : List A} {k' : A} {v : B} (fm : FiniteMap (k ∷ ks)) →
-                       ¬ k ≡ k' → (k' , v) ∈ᵐ fm → (k' , v) ∈ᵐ pop fm
-        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'
-
-        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₂ , _) =
-            (pfm₁fm₂⊆pfm₁pfm₂ , pfm₁pfm₂⊆pfm₁fm₂)
-            where
-                -- pfm₁fm₂⊆pfm₁pfm₂ = {!!}
-                pfm₁fm₂⊆pfm₁pfm₂ : pop (fm₁ ⊔ᵐ fm₂) ⊆ᵐ (pop fm₁ ⊔ᵐ pop fm₂)
-                pfm₁fm₂⊆pfm₁pfm₂ k' v' k',v'∈pfm₁fm₂
-                    with (k≢k' , k',v'∈fm₁fm₂) ← k,v∈pop⇒k,v∈ (fm₁ ⊔ᵐ fm₂) k',v'∈pfm₁fm₂
-                    with ((v₁ , v₂) , (refl , (k,v₁∈fm₁ , k,v₂∈fm₂)))
-                         ← Provenance-union fm₁ fm₂ k',v'∈fm₁fm₂
-                    with k',v₁∈pfm₁ ← k,v∈⇒k,v∈pop fm₁ k≢k' k,v₁∈fm₁
-                    with k',v₂∈pfm₂ ← k,v∈⇒k,v∈pop fm₂ k≢k' k,v₂∈fm₂
-                    =
-                        ( v₁ ⊔₂ v₂
-                        , (IsLattice.≈-refl lB
-                          , ⊔-combines {m₁ = proj₁ (pop fm₁)}
-                                       {m₂ = proj₁ (pop fm₂)}
-                                       k',v₁∈pfm₁ k',v₂∈pfm₂
-                          )
-                        )
-
-                pfm₁pfm₂⊆pfm₁fm₂ : (pop fm₁ ⊔ᵐ pop fm₂) ⊆ᵐ pop (fm₁ ⊔ᵐ fm₂)
-                pfm₁pfm₂⊆pfm₁fm₂ k' v' k',v'∈pfm₁pfm₂
-                    with ((v₁ , v₂) , (refl , (k,v₁∈pfm₁ , k,v₂∈pfm₂)))
-                         ← Provenance-union (pop fm₁) (pop fm₂) k',v'∈pfm₁pfm₂
-                    with (k≢k' , k',v₁∈fm₁) ← k,v∈pop⇒k,v∈ fm₁ k,v₁∈pfm₁
-                    with (_    , k',v₂∈fm₂) ← k,v∈pop⇒k,v∈ fm₂ k,v₂∈pfm₂
-                    =
-                        ( v₁ ⊔₂ v₂
-                        , ( IsLattice.≈-refl lB
-                          , k,v∈⇒k,v∈pop (fm₁ ⊔ᵐ fm₂) k≢k'
-                                         (⊔-combines {m₁ = m₁} {m₂ = m₂}
-                                                     k',v₁∈fm₁ k',v₂∈fm₂)
-                          )
-                        )
-
-        from-rest : ∀ {k : A} {ks : List A} (fm : FiniteMap (k ∷ ks)) →
-                    proj₂ (from fm) ≡ from (pop fm)
-        from-rest (((_ ∷ fm') , push _ ufm') , refl) = refl
-
-    from-preserves-≈ : ∀ {ks : List A} → {fm₁ fm₂ : FiniteMap ks} →
-                       fm₁ ≈ᵐ fm₂ → (_≈ⁱᵖ_ {length ks}) (from fm₁) (from fm₂)
-    from-preserves-≈ {[]} {_} {_} _ = IsEquivalence.≈-refl ≈ᵘ-equiv
-    from-preserves-≈ {k ∷ ks'} {fm₁@(m₁ , _)} {fm₂@(m₂ , _)} fm₁≈fm₂@(kvs₁⊆kvs₂ , kvs₂⊆kvs₁)
-        with first-key-in-map fm₁
-          | first-key-in-map fm₂
-          | from-first-value fm₁
-          | from-first-value fm₂
-    ...   | (v₁ , k,v₁∈fm₁) | (v₂ , k,v₂∈fm₂) | refl | refl
-            with kvs₁⊆kvs₂ _ _ k,v₁∈fm₁
-    ...       | (v₁' , (v₁≈v₁' , k,v₁'∈fm₂))
-                rewrite Map-functional {m = m₂} k,v₂∈fm₂ k,v₁'∈fm₂
-                rewrite from-rest fm₁ rewrite from-rest fm₂
-                =
-                    ( v₁≈v₁'
-                    , from-preserves-≈ {ks'} {pop fm₁} {pop fm₂}
-                                       (pop-≈ fm₁ fm₂ fm₁≈fm₂)
-                    )
-
-    to-preserves-≈ : ∀ {ks : List A} (uks : Unique ks) {ip₁ ip₂ : IterProd (length ks)} →
-                     _≈ⁱᵖ_ {length ks} ip₁ ip₂ → to uks ip₁ ≈ᵐ to uks ip₂
-    to-preserves-≈ {[]} empty {tt} {tt} _ = ((λ k v ()), (λ k v ()))
-    to-preserves-≈ {k ∷ ks'} uks@(push k≢ks' uks') {ip₁@(v₁ , rest₁)} {ip₂@(v₂ , rest₂)} (v₁≈v₂ , rest₁≈rest₂) = (fm₁⊆fm₂ , fm₂⊆fm₁)
-        where
-            inductive-step : ∀ {v₁ v₂ : B} {rest₁ rest₂ : IterProd (length ks')} →
-                               v₁ ≈₂ v₂ → _≈ⁱᵖ_ {length ks'} rest₁ rest₂ →
-                               to uks (v₁ , rest₁) ⊆ᵐ to uks (v₂ , rest₂)
-            inductive-step {v₁} {v₂} {rest₁} {rest₂} v₁≈v₂ rest₁≈rest₂ k v k,v∈kvs₁
-                with ((fm'₁ , ufm'₁) , fm'₁≡ks') ← to uks' rest₁ in p₁
-                with ((fm'₂ , ufm'₂) , fm'₂≡ks') ← to uks' rest₂ in p₂
-                with k,v∈kvs₁
-            ...   | here refl = (v₂ , (v₁≈v₂ , here refl))
-            ...   | there k,v∈fm'₁ with refl ← p₁ with refl ← p₂ =
-                    let
-                        (fm'₁⊆fm'₂ , _) = to-preserves-≈ uks' {rest₁} {rest₂}
-                                                         rest₁≈rest₂
-                        (v' , (v≈v' , k,v'∈kvs₁)) = fm'₁⊆fm'₂ k v k,v∈fm'₁
-                    in
-                        (v' , (v≈v' , there k,v'∈kvs₁))
-
-            fm₁⊆fm₂ : to uks ip₁ ⊆ᵐ to uks ip₂
-            fm₁⊆fm₂ = inductive-step v₁≈v₂ rest₁≈rest₂
-
-            fm₂⊆fm₁ : to uks ip₂ ⊆ᵐ to uks ip₁
-            fm₂⊆fm₁ = inductive-step (≈₂-sym v₁≈v₂)
-                                     (IP.≈-sym (length ks') rest₁≈rest₂)
-
-    from-⊔-distr : ∀ {ks : List A} → (fm₁ fm₂ : FiniteMap ks) →
-                  _≈ⁱᵖ_ {length ks} (from (fm₁ ⊔ᵐ fm₂))
-                                    (_⊔ⁱᵖ_ {ks} (from fm₁) (from fm₂))
-    from-⊔-distr {[]} fm₁ fm₂ = IsEquivalence.≈-refl ≈ᵘ-equiv
-    from-⊔-distr {k ∷ ks} fm₁@(m₁ , _) fm₂@(m₂ , _)
-        with first-key-in-map (fm₁ ⊔ᵐ fm₂)
-          | first-key-in-map fm₁
-          | first-key-in-map fm₂
-          | from-first-value (fm₁ ⊔ᵐ fm₂)
-          | from-first-value fm₁ | from-first-value fm₂
-    ...   | (v , k,v∈fm₁fm₂) | (v₁ , k,v₁∈fm₁) | (v₂ , k,v₂∈fm₂) | refl | refl | refl
-            with Expr-Provenance k ((` m₁) ∪ (` m₂)) (forget k,v∈fm₁fm₂)
-    ...       | (_ , (in₁ _ k∉km₂ , _)) = ⊥-elim (k∉km₂ (forget k,v₂∈fm₂))
-    ...       | (_ , (in₂ k∉km₁ _ , _)) = ⊥-elim (k∉km₁ (forget k,v₁∈fm₁))
-    ...       | (v₁⊔v₂ , (bothᵘ {v₁'} {v₂'} (single k,v₁'∈m₁) (single k,v₂'∈m₂) , k,v₁⊔v₂∈m₁m₂))
-                rewrite Map-functional {m = m₁} k,v₁∈fm₁ k,v₁'∈m₁
-                rewrite Map-functional {m = m₂} k,v₂∈fm₂ k,v₂'∈m₂
-                rewrite Map-functional {m = proj₁ (fm₁ ⊔ᵐ fm₂)} k,v∈fm₁fm₂ k,v₁⊔v₂∈m₁m₂
-                rewrite from-rest (fm₁ ⊔ᵐ fm₂) rewrite from-rest fm₁ rewrite from-rest fm₂
-                = ( IsLattice.≈-refl lB
-                  , IsEquivalence.≈-trans
-                        (IP.≈-equiv (length ks))
-                        (from-preserves-≈ {_} {pop (fm₁ ⊔ᵐ fm₂)}
-                                              {pop fm₁ ⊔ᵐ pop fm₂}
-                                              (pop-⊔-distr fm₁ fm₂))
-                        ((from-⊔-distr (pop fm₁) (pop fm₂)))
-                  )
-
-
-    to-⊔-distr : ∀ {ks : List A} (uks : Unique ks) → (ip₁ ip₂ : IterProd (length ks)) →
-                 to uks (_⊔ⁱᵖ_ {ks} ip₁ ip₂) ≈ᵐ (to uks ip₁ ⊔ᵐ to uks ip₂)
-    to-⊔-distr {[]} empty tt tt = ((λ k v ()), (λ k v ()))
-    to-⊔-distr {ks@(k ∷ ks')} uks@(push k≢ks' uks') ip₁@(v₁ , rest₁) ip₂@(v₂ , rest₂) = (fm⊆fm₁fm₂ , fm₁fm₂⊆fm)
-        where
-            fm₁ = to uks ip₁
-            fm₁' = to uks' rest₁
-            fm₂ = to uks ip₂
-            fm₂' = to uks' rest₂
-            fm = to uks (_⊔ⁱᵖ_ {k ∷ ks'} ip₁ ip₂)
-
-            fm⊆fm₁fm₂ : fm ⊆ᵐ (fm₁ ⊔ᵐ fm₂)
-            fm⊆fm₁fm₂ k v (here refl) =
-                (v₁ ⊔₂ v₂
-                , (IsLattice.≈-refl lB
-                  , ⊔-combines {k} {v₁} {v₂} {proj₁ fm₁} {proj₁ fm₂}
-                               (here refl) (here refl)
-                  )
-                )
-            fm⊆fm₁fm₂ k' v (there k',v∈fm')
-                with (fm'⊆fm'₁fm'₂ , _) ← to-⊔-distr uks' rest₁ rest₂
-                with (v' , (v₁⊔v₂≈v' , k',v'∈fm'₁fm'₂))
-                     ← fm'⊆fm'₁fm'₂ k' v k',v∈fm'
-                with (_ , (refl , (v₁∈fm'₁ , v₂∈fm'₂)))
-                     ← Provenance-union fm₁' fm₂' k',v'∈fm'₁fm'₂ =
-                ( v'
-                , ( v₁⊔v₂≈v'
-                  , ⊔-combines {m₁ = proj₁ fm₁} {m₂ = proj₁ fm₂}
-                               (there v₁∈fm'₁) (there v₂∈fm'₂)
-                  )
-                )
-
-            fm₁fm₂⊆fm : (fm₁ ⊔ᵐ fm₂) ⊆ᵐ fm
-            fm₁fm₂⊆fm k' v k',v∈fm₁fm₂
-                with (_ , fm'₁fm'₂⊆fm')
-                     ← to-⊔-distr uks' rest₁ rest₂
-                with (_ , (refl , (v₁∈fm₁ , v₂∈fm₂)))
-                     ← Provenance-union fm₁ fm₂ k',v∈fm₁fm₂
-                with v₁∈fm₁ | v₂∈fm₂
-            ...   | here refl | here refl =
-                    (v , (IsLattice.≈-refl lB , here refl))
-            ...   | here refl | there k',v₂∈fm₂' =
-                    ⊥-elim (All¬-¬Any k≢ks' (subst (k' ∈ˡ_) (proj₂ fm₂')
-                                                   (forget k',v₂∈fm₂')))
-            ...   | there k',v₁∈fm₁' | here refl =
-                    ⊥-elim (All¬-¬Any k≢ks' (subst (k' ∈ˡ_) (proj₂ fm₁')
-                                                   (forget k',v₁∈fm₁')))
-            ...   | there k',v₁∈fm₁' | there k',v₂∈fm₂' =
-                        let
-                            k',v₁v₂∈fm₁'fm₂' =
-                                ⊔-combines {m₁ = proj₁ fm₁'} {m₂ = proj₁ fm₂'}
-                                           k',v₁∈fm₁' k',v₂∈fm₂'
-                            (v' , (v₁⊔v₂≈v' , v'∈fm')) =
-                                fm'₁fm'₂⊆fm' _ _ k',v₁v₂∈fm₁'fm₂'
-                        in
-                            (v' , (v₁⊔v₂≈v' , there v'∈fm'))
-
-    module WithUniqueKeysAndFixedHeight {ks : List A} (uks : Unique ks) (≈₂-dec : Decidable _≈₂_) (h₂ : ℕ) (fhB : FixedHeight₂ h₂) where
-        import Isomorphism
-        open Isomorphism.TransportFiniteHeight
-            (IP.isFiniteHeightLattice (length ks) ≈₂-dec ≈ᵘ-dec h₂ 0 fhB fixedHeightᵘ) (isLattice ks)
-            {f = to uks} {g = from {ks}}
-            (to-preserves-≈ uks) (from-preserves-≈ {ks})
-            (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

@@ -1,14 +1,15 @@
 open import Lattice
+open import Data.Unit using (⊤)
 
 -- Due to universe levels, it becomes relatively annoying to handle the case
 -- where the levels of A and B are not the same. For the time being, constrain
 -- them to be the same.
 
-module Lattice.IterProd {a} {A B : Set a}
+module Lattice.IterProd {a} (A B : Set a)
-    (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a)
+    {_≈₁_ : A → A → Set a} {_≈₂_ : B → B → Set a}
-    (_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B)
+    {_⊔₁_ : A → A → A} {_⊔₂_ : B → B → B}
-    (_⊓₁_ : A → A → A) (_⊓₂_ : B → B → B)
+    {_⊓₁_ : A → A → A} {_⊓₂_ : B → B → B}
-    (lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_) (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
+    {{lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_}} {{lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_}} (dummy : ⊤) where
 
 open import Agda.Primitive using (lsuc)
 open import Data.Nat using (ℕ; zero; suc; _+_)
@@ -39,11 +40,11 @@ build a b (suc s) = (a , build a b s)
 private
     record RequiredForFixedHeight : Set (lsuc a) where
         field
-            ≈₁-dec : IsDecidable _≈₁_
+            {{≈₁-Decidable}} : IsDecidable _≈₁_
-            ≈₂-dec : IsDecidable _≈₂_
+            {{≈₂-Decidable}} : IsDecidable _≈₂_
             h₁ h₂ : ℕ
-            fhA : FixedHeight₁ h₁
+            {{fhA}} : FixedHeight₁ h₁
-            fhB : FixedHeight₂ h₂
+            {{fhB}} : FixedHeight₂ h₂
 
         ⊥₁ : A
         ⊥₁ = Height.⊥ fhA
@@ -58,7 +59,7 @@ private
         field
             height : ℕ
             fixedHeight : IsLattice.FixedHeight isLattice height
-            ≈-dec : IsDecidable _≈_
+            ≈-Decidable : IsDecidable _≈_
 
             ⊥-correct : Height.⊥ fixedHeight ≡ ⊥
 
@@ -84,7 +85,7 @@ private
         ; isFiniteHeightIfSupported = λ req → record
             { height = RequiredForFixedHeight.h₂ req
             ; fixedHeight = RequiredForFixedHeight.fhB req
-            ; ≈-dec = RequiredForFixedHeight.≈₂-dec req
+            ; ≈-Decidable = RequiredForFixedHeight.≈₂-Decidable req
             ; ⊥-correct = refl
             }
         }
@@ -101,10 +102,9 @@ private
                     { height = (RequiredForFixedHeight.h₁ req) + IsFiniteHeightWithBotAndDecEq.height fhlRest
                     ; fixedHeight =
                         P.fixedHeight
-                        (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightWithBotAndDecEq.≈-dec fhlRest)
+                            {{≈₂-Decidable = IsFiniteHeightWithBotAndDecEq.≈-Decidable fhlRest}}
-                        (RequiredForFixedHeight.h₁ req) (IsFiniteHeightWithBotAndDecEq.height fhlRest)
+                            {{fhB = IsFiniteHeightWithBotAndDecEq.fixedHeight fhlRest}}
-                        (RequiredForFixedHeight.fhA req) (IsFiniteHeightWithBotAndDecEq.fixedHeight fhlRest)
+                    ; ≈-Decidable = P.≈-Decidable {{≈₂-Decidable = IsFiniteHeightWithBotAndDecEq.≈-Decidable fhlRest}}
-                    ; ≈-dec = P.≈-dec (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightWithBotAndDecEq.≈-dec fhlRest)
                     ; ⊥-correct =
                         cong ((Height.⊥ (RequiredForFixedHeight.fhA req)) ,_)
                              (IsFiniteHeightWithBotAndDecEq.⊥-correct fhlRest)
@@ -112,56 +112,57 @@ private
         }
         where
             everythingRest = everything k'
+            import Lattice.Prod A (IterProd k') {{lB = Everything.isLattice everythingRest}} as P
 
-            import Lattice.Prod
+module _ {k : ℕ} where
-                _≈₁_ (Everything._≈_ everythingRest)
+    open Everything (everything k) using (_≈_; _⊔_; _⊓_) public
-                _⊔₁_ (Everything._⊔_ everythingRest)
+    open Lattice.IsLattice (Everything.isLattice (everything k)) public
-                _⊓₁_ (Everything._⊓_ everythingRest)
-                lA  (Everything.isLattice everythingRest) as P
 
-module _ (k : ℕ) where
+    instance
-    open Everything (everything k) using (_≈_; _⊔_; _⊓_; isLattice) public
+        isLattice = Everything.isLattice (everything k)
-    open Lattice.IsLattice isLattice public
 
-    lattice : Lattice (IterProd k)
+        lattice : Lattice (IterProd k)
-    lattice = record
+        lattice = record
-        { _≈_ = _≈_
+            { _≈_ = _≈_
-        ; _⊔_ = _⊔_
-        ; _⊓_ = _⊓_
-        ; isLattice = isLattice
-        }
-
-    module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
-             (h₁ h₂ : ℕ)
-             (fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where
-
-        private
-            required : RequiredForFixedHeight
-            required = record
-                { ≈₁-dec = ≈₁-dec
-                ; ≈₂-dec = ≈₂-dec
-                ; h₁ = h₁
-                ; h₂ = h₂
-                ; fhA = fhA
-                ; fhB = fhB
-                }
-
-        fixedHeight = IsFiniteHeightWithBotAndDecEq.fixedHeight (Everything.isFiniteHeightIfSupported (everything k) required)
-
-        isFiniteHeightLattice = record
-            { isLattice = isLattice
-            ; fixedHeight = fixedHeight
-            }
-
-        finiteHeightLattice : FiniteHeightLattice (IterProd k)
-        finiteHeightLattice = record
-            { height = IsFiniteHeightWithBotAndDecEq.height (Everything.isFiniteHeightIfSupported (everything k) required)
-            ; _≈_ = _≈_
             ; _⊔_ = _⊔_
             ; _⊓_ = _⊓_
-            ; isFiniteHeightLattice = isFiniteHeightLattice
+            ; isLattice = isLattice
             }
 
-        ⊥-built : Height.⊥ fixedHeight ≡ (build (Height.⊥ fhA) (Height.⊥ fhB) k)
+    module _ {{≈₁-Decidable : IsDecidable _≈₁_}} {{≈₂-Decidable : IsDecidable _≈₂_}}
-        ⊥-built = IsFiniteHeightWithBotAndDecEq.⊥-correct (Everything.isFiniteHeightIfSupported (everything k) required)
+             {h₁ h₂ : ℕ}
+             {{fhA : FixedHeight₁ h₁}} {{fhB : FixedHeight₂ h₂}} where
+
+        private
+            isFiniteHeightWithBotAndDecEq =
+                Everything.isFiniteHeightIfSupported (everything k)
+                    record
+                        { ≈₁-Decidable = ≈₁-Decidable
+                        ; ≈₂-Decidable = ≈₂-Decidable
+                        ; h₁ = h₁
+                        ; h₂ = h₂
+                        ; fhA = fhA
+                        ; fhB = fhB
+                        }
+        open IsFiniteHeightWithBotAndDecEq isFiniteHeightWithBotAndDecEq using (height; ⊥-correct)
+
+        instance
+            fixedHeight = IsFiniteHeightWithBotAndDecEq.fixedHeight isFiniteHeightWithBotAndDecEq
+
+            isFiniteHeightLattice = record
+                { isLattice = isLattice
+                ; fixedHeight = fixedHeight
+                }
+
+            finiteHeightLattice : FiniteHeightLattice (IterProd k)
+            finiteHeightLattice = record
+                { height = height
+                ; _≈_ = _≈_
+                ; _⊔_ = _⊔_
+                ; _⊓_ = _⊓_
+                ; isFiniteHeightLattice = isFiniteHeightLattice
+                }
+
+        ⊥-built : Height.⊥ fixedHeight ≡ (build (Height.⊥ fhA) (Height.⊥ fhB) k)
+        ⊥-built = ⊥-correct
 

Lattice/Map.agda

@@ -1,13 +1,14 @@
 open import Lattice
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst)
-open import Relation.Binary.Definitions using (Decidable)
 open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
+open import Data.Unit using (⊤)
 
-module Lattice.Map {a b : Level} {A : Set a} {B : Set b}
+module Lattice.Map {a b : Level} (A : Set a) (B : Set b)
     {_≈₂_ : B → B → Set b}
     {_⊔₂_ : B → B → B} {_⊓₂_ : B → B → B}
-    (≡-dec-A : Decidable (_≡_ {a} {A}))
+    {{≡-Decidable-A : IsDecidable {a} {A} _≡_}}
-    (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
+    {{lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_}}
+    (dummy : ⊤) where
 
 open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_)
 
@@ -23,6 +24,8 @@ open import Utils using (Unique; push; Unique-append; All¬-¬Any; All-x∈xs)
 open import Data.String using () renaming (_++_ to _++ˢ_)
 open import Showable using (Showable; show)
 
+open IsDecidable ≡-Decidable-A using () renaming (R-dec to _≟ᴬ_)
+
 open IsLattice lB using () renaming
     ( ≈-refl to ≈₂-refl; ≈-sym to ≈₂-sym; ≈-trans to ≈₂-trans
     ; ≈-⊔-cong to ≈₂-⊔₂-cong; ≈-⊓-cong to ≈₂-⊓₂-cong
@@ -41,7 +44,7 @@ private module ImplKeys where
 ∈k-dec : ∀ (k : A) (l : List (A × B)) → Dec (k ∈ˡ (ImplKeys.keys l))
 ∈k-dec k [] = no (λ ())
 ∈k-dec k ((k' , v) ∷ xs)
-    with (≡-dec-A k k')
+    with (k ≟ᴬ k')
 ...   | yes k≡k' = yes (here k≡k')
 ...   | no k≢k' with (∈k-dec k xs)
 ...       | yes k∈kxs = yes (there k∈kxs)
@@ -76,7 +79,7 @@ private module _ where
     k∈-dec : ∀ (k : A) (l : List A) → Dec (k ∈ l)
     k∈-dec k [] = no (λ ())
     k∈-dec k (x ∷ xs)
-        with (≡-dec-A k x)
+        with (k ≟ᴬ x)
     ...   | yes refl = yes (here refl)
     ...   | no k≢x with (k∈-dec k xs)
     ...       | yes k∈xs = yes (there k∈xs)
@@ -113,7 +116,7 @@ private module ImplInsert (f : B → B → B) where
 
     insert : A → B → List (A × B) → List (A × B)
     insert k v [] = (k , v) ∷ []
-    insert k v (x@(k' , v') ∷ xs) with ≡-dec-A k k'
+    insert k v (x@(k' , v') ∷ xs) with k ≟ᴬ k'
     ...                             | yes _ = (k' , f v v') ∷ xs
     ...                             | no _ = x ∷ insert k v xs
 
@@ -123,11 +126,11 @@ private module ImplInsert (f : B → B → B) where
     insert-keys-∈ : ∀ {k : A} {v : B} {l : List (A × B)} →
                     k ∈k l → keys l ≡ keys (insert k v l)
     insert-keys-∈ {k} {v} {(k' , v') ∷ xs} (here k≡k')
-        with (≡-dec-A k k')
+        with (k ≟ᴬ k')
     ...   | yes _ = refl
     ...   | no k≢k' = ⊥-elim (k≢k' k≡k')
     insert-keys-∈ {k} {v} {(k' , _) ∷ xs} (there k∈kxs)
-        with (≡-dec-A k k')
+        with (k ≟ᴬ k')
     ...   | yes _ = refl
     ...   | no _ = cong (λ xs' → k' ∷ xs') (insert-keys-∈ k∈kxs)
 
@@ -135,7 +138,7 @@ private module ImplInsert (f : B → B → B) where
                     ¬ (k ∈k l) → (keys l ++ (k ∷ [])) ≡ keys (insert k v l)
     insert-keys-∉ {k} {v} {[]} _ = refl
     insert-keys-∉ {k} {v} {(k' , v') ∷ xs} k∉kl
-        with (≡-dec-A k k')
+        with (k ≟ᴬ k')
     ...   | yes k≡k' = ⊥-elim (k∉kl (here k≡k'))
     ...   | no _ = cong (λ xs' → k' ∷ xs')
                         (insert-keys-∉ (λ k∈kxs → k∉kl (there k∈kxs)))
@@ -171,7 +174,7 @@ private module ImplInsert (f : B → B → B) where
                                  ¬ k ∈k l → (k , v) ∈ insert k v l
     insert-fresh {l = []} k∉kl = here refl
     insert-fresh {k} {l = (k' , v') ∷ xs} k∉kl
-        with ≡-dec-A k k'
+        with k ≟ᴬ k'
     ...   | yes k≡k' = ⊥-elim (k∉kl (here k≡k'))
     ...   | no _ = there (insert-fresh (λ k∈kxs → k∉kl (there k∈kxs)))
 
@@ -180,9 +183,9 @@ private module ImplInsert (f : B → B → B) where
     insert-preserves-∉k {l = []} k≢k' k∉kl (here k≡k') = k≢k' k≡k'
     insert-preserves-∉k {l = []} k≢k' k∉kl (there ())
     insert-preserves-∉k {k} {k'} {v'} {(k'' , v'') ∷ xs} k≢k' k∉kl k∈kil
-        with ≡-dec-A k k''
+        with k ≟ᴬ k''
     ...   | yes k≡k'' = k∉kl (here k≡k'')
-    ...   | no k≢k'' with ≡-dec-A k' k'' | k∈kil
+    ...   | no k≢k'' with k' ≟ᴬ k'' | k∈kil
     ...       | yes k'≡k'' | here k≡k'' = k≢k'' k≡k''
     ...       | yes k'≡k'' | there k∈kxs = k∉kl (there k∈kxs)
     ...       | no k'≢k''  | here k≡k'' = k∉kl (here k≡k'')
@@ -193,18 +196,18 @@ private module ImplInsert (f : B → B → B) where
                         ¬ k ∈k l₁ → ¬ k ∈k l₂ → ¬ k ∈k union l₁ l₂
     union-preserves-∉ {l₁ = []} _ k∉kl₂ = k∉kl₂
     union-preserves-∉ {k} {(k' , v') ∷ xs₁} k∉kl₁ k∉kl₂
-        with ≡-dec-A k k'
+        with k ≟ᴬ k'
     ...   | yes k≡k' = ⊥-elim (k∉kl₁ (here k≡k'))
     ...   | no k≢k' = insert-preserves-∉k k≢k' (union-preserves-∉ (λ k∈kxs₁ → k∉kl₁ (there k∈kxs₁)) k∉kl₂)
 
     insert-preserves-∈k : ∀ {k k' : A} {v' : B} {l : List (A × B)} →
                           k ∈k l → k ∈k insert k' v' l
     insert-preserves-∈k {k} {k'} {v'} {(k'' , v'') ∷ xs} (here k≡k'')
-        with (≡-dec-A k' k'')
+        with k' ≟ᴬ k''
     ...   | yes _ = here k≡k''
     ...   | no _ = here k≡k''
     insert-preserves-∈k {k} {k'} {v'} {(k'' , v'') ∷ xs} (there k∈kxs)
-        with (≡-dec-A k' k'')
+        with k' ≟ᴬ k''
     ...   | yes _ = there k∈kxs
     ...   | no _ = there (insert-preserves-∈k k∈kxs)
 
@@ -236,11 +239,11 @@ private module ImplInsert (f : B → B → B) where
     insert-preserves-∈ : ∀ {k k' : A} {v v' : B} {l : List (A × B)} →
                          ¬ k ≡ k' → (k , v) ∈ l → (k , v) ∈ insert k' v' l
     insert-preserves-∈ {k} {k'} {l = x ∷ xs} k≢k' (here k,v=x)
-        rewrite sym k,v=x with ≡-dec-A k' k
+        rewrite sym k,v=x with k' ≟ᴬ k
     ...   | yes k'≡k = ⊥-elim (k≢k' (sym k'≡k))
     ...   | no _ = here refl
     insert-preserves-∈ {k} {k'} {l = (k'' , _) ∷ xs} k≢k' (there k,v∈xs)
-        with ≡-dec-A k' k''
+        with k' ≟ᴬ k''
     ...   | yes _ = there k,v∈xs
     ...   | no _ = there (insert-preserves-∈ k≢k' k,v∈xs)
 
@@ -259,7 +262,7 @@ private module ImplInsert (f : B → B → B) where
             k,v∈mxs₁l = union-preserves-∈₁ uxs₁ k,v∈xs₁ k∉kl₂
 
             k≢k' : ¬ k ≡ k'
-            k≢k' with ≡-dec-A k k'
+            k≢k' with k ≟ᴬ k'
             ...    | yes k≡k' rewrite k≡k' = ⊥-elim (All¬-¬Any k'≢xs₁ (∈-cong proj₁ k,v∈xs₁))
             ...    | no  k≢k' = k≢k'
     union-preserves-∈₁ {l₁ = (k' , v') ∷ xs₁} (push k'≢xs₁ uxs₁) (here k,v≡k',v') k∉kl₂
@@ -270,11 +273,11 @@ private module ImplInsert (f : B → B → B) where
                       Unique (keys l) → (k , v') ∈ l → (k , f v v') ∈ (insert k v l)
     insert-combines {l = (k' , v'') ∷ xs} _ (here k,v'≡k',v'')
         rewrite cong proj₁ k,v'≡k',v'' rewrite cong proj₂ k,v'≡k',v''
-        with ≡-dec-A k' k'
+        with k' ≟ᴬ k'
     ...   | yes _ = here refl
     ...   | no k≢k' = ⊥-elim (k≢k' refl)
     insert-combines {k} {l = (k' , v'') ∷ xs} (push k'≢xs uxs) (there k,v'∈xs)
-        with ≡-dec-A k k'
+        with k ≟ᴬ k'
     ...   | yes k≡k' rewrite k≡k' = ⊥-elim (All¬-¬Any k'≢xs (∈-cong proj₁ k,v'∈xs))
     ...   | no k≢k' = there (insert-combines uxs k,v'∈xs)
 
@@ -288,13 +291,13 @@ private module ImplInsert (f : B → B → B) where
         insert-preserves-∈ k≢k' (union-combines uxs₁ ul₂ k,v₁∈xs₁ k,v₂∈l₂)
         where
             k≢k' : ¬ k ≡ k'
-            k≢k' with ≡-dec-A k k'
+            k≢k' with k ≟ᴬ k'
             ...    | yes k≡k' rewrite k≡k' = ⊥-elim (All¬-¬Any k'≢xs₁ (∈-cong proj₁ k,v₁∈xs₁))
             ...    | no  k≢k' = k≢k'
 
     update : A → B → List (A × B) → List (A × B)
     update k v [] = []
-    update k v ((k' , v') ∷ xs) with ≡-dec-A k k'
+    update k v ((k' , v') ∷ xs) with k ≟ᴬ k'
     ...                            | yes _ = (k' , f v v') ∷ xs
     ...                            | no _ = (k' , v') ∷ update k v xs
 
@@ -314,7 +317,7 @@ private module ImplInsert (f : B → B → B) where
                   keys l ≡ keys (update k v l)
     update-keys {l = []} = refl
     update-keys {k} {v} {l = (k' , v') ∷ xs}
-        with ≡-dec-A k k'
+        with k ≟ᴬ k'
     ...   | yes _ = refl
     ...   | no _ rewrite update-keys {k} {v} {xs} = refl
 
@@ -431,11 +434,11 @@ private module ImplInsert (f : B → B → B) where
                          ¬ k ≡ k' → (k , v) ∈ l → (k , v) ∈ update k' v' l
     update-preserves-∈ {k} {k'} {v} {v'} {(k'' , v'') ∷ xs} k≢k' (here k,v≡k'',v'')
         rewrite cong proj₁ k,v≡k'',v'' rewrite cong proj₂ k,v≡k'',v''
-        with ≡-dec-A k' k''
+        with k' ≟ᴬ k''
     ...   | yes k'≡k'' = ⊥-elim (k≢k' (sym k'≡k''))
     ...   | no _ = here refl
     update-preserves-∈ {k} {k'} {v} {v'} {(k'' , v'') ∷ xs} k≢k' (there k,v∈xs)
-        with ≡-dec-A k' k''
+        with k' ≟ᴬ k''
     ...   | yes _ = there k,v∈xs
     ...   | no _ = there (update-preserves-∈ k≢k' k,v∈xs)
 
@@ -449,11 +452,11 @@ private module ImplInsert (f : B → B → B) where
                       Unique (keys l) → (k , v) ∈ l → (k , f v' v) ∈ update k v' l
     update-combines {k} {v} {v'} {(k' , v'') ∷ xs} _ (here k,v=k',v'')
         rewrite cong proj₁ k,v=k',v'' rewrite cong proj₂ k,v=k',v''
-        with ≡-dec-A k' k'
+        with k' ≟ᴬ k'
     ...   | yes _ = here refl
     ...   | no k'≢k' = ⊥-elim (k'≢k' refl)
     update-combines {k} {v} {v'} {(k' , v'') ∷ xs} (push k'≢xs uxs) (there k,v∈xs)
-        with ≡-dec-A k k'
+        with k ≟ᴬ k'
     ...   | yes k≡k' rewrite k≡k' = ⊥-elim (All¬-¬Any k'≢xs (∈-cong proj₁ k,v∈xs))
     ...   | no _ = there (update-combines uxs k,v∈xs)
 
@@ -467,7 +470,7 @@ private module ImplInsert (f : B → B → B) where
         update-preserves-∈ k≢k' (updates-combine uxs₁ u₂ k,v₁∈xs k,v₂∈l₂)
         where
             k≢k' : ¬ k ≡ k'
-            k≢k' with ≡-dec-A k k'
+            k≢k' with k ≟ᴬ k'
             ...    | yes k≡k' rewrite k≡k' = ⊥-elim (All¬-¬Any k'≢xs (∈-cong proj₁ k,v₁∈xs))
             ...    | no  k≢k' = k≢k'
 
@@ -625,7 +628,8 @@ Expr-Provenance-≡ {k} {v} e k,v∈e
     with (v' , (p , k,v'∈e)) ← Expr-Provenance k e (forget k,v∈e)
     rewrite Map-functional {m = ⟦ e ⟧} k,v∈e k,v'∈e = p
 
-module _ (≈₂-dec : IsDecidable _≈₂_) where
+module _ {{≈₂-Decidable : IsDecidable _≈₂_}} where
+    open IsDecidable ≈₂-Decidable using () renaming (R-dec to ≈₂-dec)
     private module _ where
         data SubsetInfo (m₁ m₂ : Map) : Set (a ⊔ℓ b) where
             extra : (k : A) → k ∈k m₁ → ¬ k ∈k m₂ → SubsetInfo m₁ m₂
@@ -676,6 +680,9 @@ module _ (≈₂-dec : IsDecidable _≈₂_) where
     ...   | _         | no  m₂̷⊆m₁ = no (λ (_ , m₂⊆m₁) → m₂̷⊆m₁ m₂⊆m₁)
     ...   | no  m₁̷⊆m₂ | _         = no (λ (m₁⊆m₂ , _) → m₁̷⊆m₂ m₁⊆m₂)
 
+    ≈-Decidable : IsDecidable _≈_
+    ≈-Decidable = record { R-dec = ≈-dec }
+
 private module I⊔ = ImplInsert _⊔₂_
 private module I⊓ = ImplInsert _⊓₂_
 
@@ -1026,7 +1033,7 @@ updating-via-k∉ks-backward m = transform-k∉ks-backward
 
 module _ {l} {L : Set l}
          {_≈ˡ_ : L → L → Set l} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L}
-         (lL : IsLattice L _≈ˡ_ _⊔ˡ_ _⊓ˡ_) where
+         {{lL : IsLattice L _≈ˡ_ _⊔ˡ_ _⊓ˡ_}} where
     open IsLattice lL using () renaming (_≼_ to _≼ˡ_)
 
     module _ (f : L → Map) (f-Monotonic : Monotonic _≼ˡ_ _≼_ f)

Lattice/MapSet.agda

@@ -1,9 +1,9 @@
 open import Lattice
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst)
-open import Relation.Binary.Definitions using (Decidable)
 open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
+open import Data.Unit using (⊤)
 
-module Lattice.MapSet {a : Level} {A : Set a} (≡-dec-A : Decidable (_≡_ {a} {A})) where
+module Lattice.MapSet {a : Level} (A : Set a) {{≡-Decidable-A : IsDecidable (_≡_ {a} {A})}} (dummy : ⊤) where
 
 open import Data.List using (List; map)
 open import Data.Product using (_,_; proj₁)
@@ -12,7 +12,7 @@ open import Function using (_∘_)
 open import Lattice.Unit using (⊤; tt) renaming (_≈_ to _≈₂_; _⊔_ to _⊔₂_; _⊓_ to _⊓₂_; isLattice to ⊤-isLattice)
 import Lattice.Map
 
-private module UnitMap = Lattice.Map ≡-dec-A ⊤-isLattice
+private module UnitMap = Lattice.Map A ⊤ dummy
 open UnitMap
     using (Map; Expr; ⟦_⟧)
     renaming

Lattice/Nat.agda

@@ -18,31 +18,32 @@ private
     ≡-⊓-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≡ a₂ → a₃ ≡ a₄ → (a₁ ⊓ a₃) ≡ (a₂ ⊓ a₄)
     ≡-⊓-cong a₁≡a₂ a₃≡a₄ rewrite a₁≡a₂ rewrite a₃≡a₄ = refl
 
-isMaxSemilattice : IsSemilattice ℕ _≡_ _⊔_
+instance
-isMaxSemilattice = record
+    isMaxSemilattice : IsSemilattice ℕ _≡_ _⊔_
-    { ≈-equiv = record
+    isMaxSemilattice = record
-        { ≈-refl = refl
+        { ≈-equiv = record
-        ; ≈-sym = sym
+            { ≈-refl = refl
-        ; ≈-trans = trans
+            ; ≈-sym = sym
+            ; ≈-trans = trans
+            }
+        ; ≈-⊔-cong = ≡-⊔-cong
+        ; ⊔-assoc = ⊔-assoc
+        ; ⊔-comm = ⊔-comm
+        ; ⊔-idemp = ⊔-idem
         }
-    ; ≈-⊔-cong = ≡-⊔-cong
-    ; ⊔-assoc = ⊔-assoc
-    ; ⊔-comm = ⊔-comm
-    ; ⊔-idemp = ⊔-idem
-    }
 
-isMinSemilattice : IsSemilattice ℕ _≡_ _⊓_
+    isMinSemilattice : IsSemilattice ℕ _≡_ _⊓_
-isMinSemilattice = record
+    isMinSemilattice = record
-    { ≈-equiv = record
+        { ≈-equiv = record
-        { ≈-refl = refl
+            { ≈-refl = refl
-        ; ≈-sym = sym
+            ; ≈-sym = sym
-        ; ≈-trans = trans
+            ; ≈-trans = trans
+            }
+        ; ≈-⊔-cong = ≡-⊓-cong
+        ; ⊔-assoc = ⊓-assoc
+        ; ⊔-comm = ⊓-comm
+        ; ⊔-idemp = ⊓-idem
         }
-    ; ≈-⊔-cong = ≡-⊓-cong
-    ; ⊔-assoc = ⊓-assoc
-    ; ⊔-comm = ⊓-comm
-    ; ⊔-idemp = ⊓-idem
-    }
 
 private
     max-bound₁ : {x y z : ℕ} → x ⊔ y ≡ z → x ≤ z
@@ -74,18 +75,19 @@ private
             helper : x ⊔ (x ⊓ y) ≤ x ⊔ x  → x ⊔ x ≡ x → x ⊔ (x ⊓ y) ≤ x
             helper x⊔x⊓y≤x⊔x x⊔x≡x rewrite x⊔x≡x = x⊔x⊓y≤x⊔x
 
-isLattice : IsLattice ℕ _≡_ _⊔_ _⊓_
+instance
-isLattice = record
+    isLattice : IsLattice ℕ _≡_ _⊔_ _⊓_
-    { joinSemilattice = isMaxSemilattice
+    isLattice = record
-    ; meetSemilattice = isMinSemilattice
+        { joinSemilattice = isMaxSemilattice
-    ; absorb-⊔-⊓ = λ x y → maxmin-absorb {x} {y}
+        ; meetSemilattice = isMinSemilattice
-    ; absorb-⊓-⊔ = λ x y → minmax-absorb {x} {y}
+        ; absorb-⊔-⊓ = λ x y → maxmin-absorb {x} {y}
-    }
+        ; absorb-⊓-⊔ = λ x y → minmax-absorb {x} {y}
+        }
 
-lattice : Lattice ℕ
+    lattice : Lattice ℕ
-lattice = record
+    lattice = record
-    { _≈_ = _≡_
+        { _≈_ = _≡_
-    ; _⊔_ = _⊔_
+        ; _⊔_ = _⊔_
-    ; _⊓_ = _⊓_
+        ; _⊓_ = _⊓_
-    ; isLattice = isLattice
+        ; isLattice = isLattice
-    }
+        }

Lattice/Prod.agda

@@ -1,10 +1,10 @@
 open import Lattice
 
-module Lattice.Prod {a b} {A : Set a} {B : Set b}
+module Lattice.Prod {a b} (A : Set a) (B : Set b)
-    (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set b)
+    {_≈₁_ : A → A → Set a} {_≈₂_ : B → B → Set b}
-    (_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B)
+    {_⊔₁_ : A → A → A} {_⊔₂_ : B → B → B}
-    (_⊓₁_ : A → A → A) (_⊓₂_ : B → B → B)
+    {_⊓₁_ : A → A → A} {_⊓₂_ : B → B → B}
-    (lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_) (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
+    {{lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_}} {{lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_}} where
 
 open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
 open import Data.Nat using (ℕ; _≤_; _+_; suc)
@@ -12,6 +12,7 @@ open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
 open import Data.Empty using (⊥-elim)
 open import Relation.Binary.Core using (_Preserves_⟶_ )
 open import Relation.Binary.PropositionalEquality using (sym; subst)
+open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Nullary using (¬_; yes; no)
 open import Equivalence
 import Chain
@@ -39,13 +40,14 @@ open IsLattice lB using () renaming
 _≈_ : A × B → A × B → Set (a ⊔ℓ b)
 (a₁ , b₁) ≈ (a₂ , b₂) = (a₁ ≈₁ a₂) × (b₁ ≈₂ b₂)
 
-≈-equiv : IsEquivalence (A × B) _≈_
+instance
-≈-equiv = record
+    ≈-equiv : IsEquivalence (A × B) _≈_
-    { ≈-refl = λ {p} → (≈₁-refl , ≈₂-refl)
+    ≈-equiv = record
-    ; ≈-sym = λ {p₁} {p₂} (a₁≈a₂ , b₁≈b₂) → (≈₁-sym a₁≈a₂ , ≈₂-sym b₁≈b₂)
+        { ≈-refl = λ {p} → (≈₁-refl , ≈₂-refl)
-    ; ≈-trans = λ {p₁} {p₂} {p₃} (a₁≈a₂ , b₁≈b₂) (a₂≈a₃ , b₂≈b₃) →
+        ; ≈-sym = λ {p₁} {p₂} (a₁≈a₂ , b₁≈b₂) → (≈₁-sym a₁≈a₂ , ≈₂-sym b₁≈b₂)
-        ( ≈₁-trans a₁≈a₂ a₂≈a₃ , ≈₂-trans b₁≈b₂ b₂≈b₃ )
+        ; ≈-trans = λ {p₁} {p₂} {p₃} (a₁≈a₂ , b₁≈b₂) (a₂≈a₃ , b₂≈b₃) →
-    }
+            ( ≈₁-trans a₁≈a₂ a₂≈a₃ , ≈₂-trans b₁≈b₂ b₂≈b₃ )
+        }
 
 _⊔_ : A × B → A × B → A × B
 (a₁ , b₁) ⊔ (a₂ , b₂) = (a₁ ⊔₁ a₂ , b₁ ⊔₂ b₂)
@@ -75,116 +77,124 @@ private module ProdIsSemilattice (f₁ : A → A → A) (f₂ : B → B → B) (
             )
         }
 
-isJoinSemilattice : IsSemilattice (A × B) _≈_ _⊔_
+instance
-isJoinSemilattice = ProdIsSemilattice.isSemilattice _⊔₁_ _⊔₂_ joinSemilattice₁ joinSemilattice₂
+    isJoinSemilattice : IsSemilattice (A × B) _≈_ _⊔_
+    isJoinSemilattice = ProdIsSemilattice.isSemilattice _⊔₁_ _⊔₂_ joinSemilattice₁ joinSemilattice₂
 
-isMeetSemilattice : IsSemilattice (A × B) _≈_ _⊓_
+    isMeetSemilattice : IsSemilattice (A × B) _≈_ _⊓_
-isMeetSemilattice = ProdIsSemilattice.isSemilattice _⊓₁_ _⊓₂_ meetSemilattice₁ meetSemilattice₂
+    isMeetSemilattice = ProdIsSemilattice.isSemilattice _⊓₁_ _⊓₂_ meetSemilattice₁ meetSemilattice₂
 
-isLattice : IsLattice (A × B) _≈_ _⊔_ _⊓_
+    isLattice : IsLattice (A × B) _≈_ _⊔_ _⊓_
-isLattice = record
+    isLattice = record
-    { joinSemilattice = isJoinSemilattice
+        { joinSemilattice = isJoinSemilattice
-    ; meetSemilattice = isMeetSemilattice
+        ; meetSemilattice = isMeetSemilattice
-    ; absorb-⊔-⊓ = λ (a₁ , b₁) (a₂ , b₂) →
+        ; absorb-⊔-⊓ = λ (a₁ , b₁) (a₂ , b₂) →
-        ( IsLattice.absorb-⊔-⊓ lA a₁ a₂
+            ( IsLattice.absorb-⊔-⊓ lA a₁ a₂
-        , IsLattice.absorb-⊔-⊓ lB b₁ b₂
+            , IsLattice.absorb-⊔-⊓ lB b₁ b₂
-        )
+            )
-    ; absorb-⊓-⊔ = λ (a₁ , b₁) (a₂ , b₂) →
+        ; absorb-⊓-⊔ = λ (a₁ , b₁) (a₂ , b₂) →
-        ( IsLattice.absorb-⊓-⊔ lA a₁ a₂
+            ( IsLattice.absorb-⊓-⊔ lA a₁ a₂
-        , IsLattice.absorb-⊓-⊔ lB b₁ b₂
+            , IsLattice.absorb-⊓-⊔ lB b₁ b₂
-        )
+            )
-    }
+        }
 
-lattice : Lattice (A × B)
+    lattice : Lattice (A × B)
-lattice = record
+    lattice = record
-    { _≈_ = _≈_
+        { _≈_ = _≈_
-    ; _⊔_ = _⊔_
+        ; _⊔_ = _⊔_
-    ; _⊓_ = _⊓_
+        ; _⊓_ = _⊓_
-    ; isLattice = isLattice
+        ; isLattice = isLattice
-    }
+        }
 
-module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_) where
+open IsLattice isLattice using (_≼_; _≺_; ≺-cong) public
-    ≈-dec : IsDecidable _≈_
+
+module _ {{≈₁-Decidable : IsDecidable _≈₁_}} {{≈₂-Decidable : IsDecidable _≈₂_}} where
+    open IsDecidable ≈₁-Decidable using () renaming (R-dec to ≈₁-dec)
+    open IsDecidable ≈₂-Decidable using () renaming (R-dec to ≈₂-dec)
+
+    ≈-dec : Decidable _≈_
     ≈-dec (a₁ , b₁) (a₂ , b₂)
         with ≈₁-dec a₁ a₂ | ≈₂-dec b₁ b₂
     ...   | yes a₁≈a₂ | yes b₁≈b₂ = yes (a₁≈a₂ , b₁≈b₂)
     ...   | no a₁̷≈a₂ | _ = no (λ (a₁≈a₂ , _) → a₁̷≈a₂ a₁≈a₂)
     ...   | _ | no b₁̷≈b₂ = no (λ (_ , b₁≈b₂) → b₁̷≈b₂ b₁≈b₂)
 
+    instance
+        ≈-Decidable : IsDecidable _≈_
+        ≈-Decidable = record { R-dec = ≈-dec }
 
-module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
+    module _ {h₁ h₂ : ℕ}
-         (h₁ h₂ : ℕ)
+             {{fhA : FixedHeight₁ h₁}} {{fhB : FixedHeight₂ h₂}} where
-         (fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where
 
-    open import Data.Nat.Properties
+        open import Data.Nat.Properties
-    open IsLattice isLattice using (_≼_; _≺_; ≺-cong)
 
-    module ChainMapping₁ = ChainMapping joinSemilattice₁ isJoinSemilattice
+        module ChainMapping₁ = ChainMapping joinSemilattice₁ isJoinSemilattice
-    module ChainMapping₂ = ChainMapping joinSemilattice₂ isJoinSemilattice
+        module ChainMapping₂ = ChainMapping joinSemilattice₂ isJoinSemilattice
 
-    module ChainA = Chain _≈₁_ ≈₁-equiv _≺₁_ ≺₁-cong
+        module ChainA = Chain _≈₁_ ≈₁-equiv _≺₁_ ≺₁-cong
-    module ChainB = Chain _≈₂_ ≈₂-equiv _≺₂_ ≺₂-cong
+        module ChainB = Chain _≈₂_ ≈₂-equiv _≺₂_ ≺₂-cong
-    module ProdChain = Chain _≈_ ≈-equiv _≺_ ≺-cong
+        module ProdChain = Chain _≈_ ≈-equiv _≺_ ≺-cong
 
-    open ChainA using () renaming (Chain to Chain₁; done to done₁; step to step₁; Chain-≈-cong₁ to Chain₁-≈-cong₁)
+        open ChainA using () renaming (Chain to Chain₁; done to done₁; step to step₁; Chain-≈-cong₁ to Chain₁-≈-cong₁)
-    open ChainB using () renaming (Chain to Chain₂; done to done₂; step to step₂; Chain-≈-cong₁ to Chain₂-≈-cong₁)
+        open ChainB using () renaming (Chain to Chain₂; done to done₂; step to step₂; Chain-≈-cong₁ to Chain₂-≈-cong₁)
-    open ProdChain using (Chain; concat; done; step)
+        open ProdChain using (Chain; concat; done; step)
 
-    private
+        private
-        a,∙-Monotonic : ∀ (a : A) → Monotonic _≼₂_ _≼_ (λ b → (a , b))
+            a,∙-Monotonic : ∀ (a : A) → Monotonic _≼₂_ _≼_ (λ b → (a , b))
-        a,∙-Monotonic a {b₁} {b₂} b₁⊔b₂≈b₂ = (⊔₁-idemp a , b₁⊔b₂≈b₂)
+            a,∙-Monotonic a {b₁} {b₂} b₁⊔b₂≈b₂ = (⊔₁-idemp a , b₁⊔b₂≈b₂)
 
-        a,∙-Preserves-≈₂ : ∀ (a : A) → (λ b → (a , b)) Preserves _≈₂_ ⟶  _≈_
+            a,∙-Preserves-≈₂ : ∀ (a : A) → (λ b → (a , b)) Preserves _≈₂_ ⟶  _≈_
-        a,∙-Preserves-≈₂ a {b₁} {b₂} b₁≈b₂ = (≈₁-refl , b₁≈b₂)
+            a,∙-Preserves-≈₂ a {b₁} {b₂} b₁≈b₂ = (≈₁-refl , b₁≈b₂)
 
-        ∙,b-Monotonic : ∀ (b : B) → Monotonic _≼₁_ _≼_ (λ a → (a , b))
+            ∙,b-Monotonic : ∀ (b : B) → Monotonic _≼₁_ _≼_ (λ a → (a , b))
-        ∙,b-Monotonic b {a₁} {a₂} a₁⊔a₂≈a₂ = (a₁⊔a₂≈a₂ , ⊔₂-idemp b)
+            ∙,b-Monotonic b {a₁} {a₂} a₁⊔a₂≈a₂ = (a₁⊔a₂≈a₂ , ⊔₂-idemp b)
 
-        ∙,b-Preserves-≈₁ : ∀ (b : B) → (λ a → (a , b)) Preserves _≈₁_ ⟶  _≈_
+            ∙,b-Preserves-≈₁ : ∀ (b : B) → (λ a → (a , b)) Preserves _≈₁_ ⟶  _≈_
-        ∙,b-Preserves-≈₁ b {a₁} {a₂} a₁≈a₂ = (a₁≈a₂ , ≈₂-refl)
+            ∙,b-Preserves-≈₁ b {a₁} {a₂} a₁≈a₂ = (a₁≈a₂ , ≈₂-refl)
 
-        open ChainA.Height fhA using () renaming (⊥ to ⊥₁; ⊤ to ⊤₁; longestChain to longestChain₁; bounded to bounded₁)
+            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₂)
+            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 : ∀ {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))
+            unzip (done (a₁≈a₂ , b₁≈b₂)) = ((0 , 0) , ((done₁ a₁≈a₂ , done₂ b₁≈b₂) , ≤-refl))
-        unzip {a₁} {a₂} {b₁} {b₂} {n} (step {(a₁ , b₁)} {(a , b)} ((a₁≼a , b₁≼b) , a₁b₁̷≈ab) (a≈a' , b≈b') a'b'a₂b₂)
+            unzip {a₁} {a₂} {b₁} {b₂} {n} (step {(a₁ , b₁)} {(a , b)} ((a₁≼a , b₁≼b) , a₁b₁̷≈ab) (a≈a' , b≈b') a'b'a₂b₂)
-            with ≈₁-dec a₁ a | ≈₂-dec b₁ b | unzip a'b'a₂b₂
+                with ≈₁-dec a₁ a | ≈₂-dec b₁ b | unzip a'b'a₂b₂
-        ...   | yes a₁≈a | yes b₁≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) = ⊥-elim (a₁b₁̷≈ab (a₁≈a , b₁≈b))
+            ...   | yes a₁≈a | yes b₁≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) = ⊥-elim (a₁b₁̷≈ab (a₁≈a , b₁≈b))
-        ...   | no a₁̷≈a  | yes b₁≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) =
+            ...   | no a₁̷≈a  | yes b₁≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) =
-                ((suc n₁ , n₂) , ((step₁ (a₁≼a , a₁̷≈a) a≈a' c₁ , Chain₂-≈-cong₁ (≈₂-sym (≈₂-trans b₁≈b b≈b')) c₂), +-monoʳ-≤ 1 (n≤n₁+n₂)))
+                    ((suc n₁ , n₂) , ((step₁ (a₁≼a , a₁̷≈a) a≈a' c₁ , Chain₂-≈-cong₁ (≈₂-sym (≈₂-trans b₁≈b b≈b')) c₂), +-monoʳ-≤ 1 (n≤n₁+n₂)))
-        ...   | yes a₁≈a | no b₁̷≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) =
+            ...   | yes a₁≈a | no b₁̷≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) =
-                ((n₁ , suc n₂) , ( (Chain₁-≈-cong₁ (≈₁-sym (≈₁-trans a₁≈a a≈a')) c₁ , step₂ (b₁≼b , b₁̷≈b) b≈b' c₂)
+                    ((n₁ , suc n₂) , ( (Chain₁-≈-cong₁ (≈₁-sym (≈₁-trans a₁≈a a≈a')) c₁ , step₂ (b₁≼b , b₁̷≈b) b≈b' c₂)
-                                 , subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂)
+                                     , subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂)
-                                 ))
-        ...   | no a₁̷≈a  | no b₁̷≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) =
-                ((suc n₁ , suc n₂) , ( (step₁ (a₁≼a , a₁̷≈a) a≈a' c₁ , step₂ (b₁≼b , b₁̷≈b) b≈b' c₂)
-                                     , m≤n⇒m≤o+n 1 (subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂))
                                      ))
+            ...   | no a₁̷≈a  | no b₁̷≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) =
+                    ((suc n₁ , suc n₂) , ( (step₁ (a₁≼a , a₁̷≈a) a≈a' c₁ , step₂ (b₁≼b , b₁̷≈b) b≈b' c₂)
+                                         , m≤n⇒m≤o+n 1 (subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂))
+                                         ))
 
-    fixedHeight : IsLattice.FixedHeight isLattice (h₁ + h₂)
+        instance
-    fixedHeight = record
+            fixedHeight : IsLattice.FixedHeight isLattice (h₁ + h₂)
-      { ⊥ = (⊥₁ , ⊥₂)
+            fixedHeight = record
-      ; ⊤ = (⊤₁ , ⊤₂)
+              { ⊥ = (⊥₁ , ⊥₂)
-      ; longestChain = concat
+              ; ⊤ = (⊤₁ , ⊤₂)
-            (ChainMapping₁.Chain-map (λ a → (a , ⊥₂)) (∙,b-Monotonic _) proj₁ (∙,b-Preserves-≈₁ _) longestChain₁)
+              ; longestChain = concat
-            (ChainMapping₂.Chain-map (λ b → (⊤₁ , b)) (a,∙-Monotonic _) proj₂ (a,∙-Preserves-≈₂ _) longestChain₂)
+                    (ChainMapping₁.Chain-map (λ a → (a , ⊥₂)) (∙,b-Monotonic _) proj₁ (∙,b-Preserves-≈₁ _) longestChain₁)
-      ; bounded = λ a₁b₁a₂b₂ →
+                    (ChainMapping₂.Chain-map (λ b → (⊤₁ , b)) (a,∙-Monotonic _) proj₂ (a,∙-Preserves-≈₂ _) longestChain₂)
-            let ((n₁ , n₂) , ((a₁a₂ , b₁b₂) , n≤n₁+n₂)) = unzip a₁b₁a₂b₂
+              ; bounded = λ a₁b₁a₂b₂ →
-            in ≤-trans n≤n₁+n₂ (+-mono-≤ (bounded₁ a₁a₂) (bounded₂ b₁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 : IsFiniteHeightLattice (A × B) (h₁ + h₂) _≈_ _⊔_ _⊓_
-    isFiniteHeightLattice = record
+            isFiniteHeightLattice = record
-        { isLattice = isLattice
+                { isLattice = isLattice
-        ; fixedHeight = fixedHeight
+                ; fixedHeight = fixedHeight
-        }
+                }
 
-    finiteHeightLattice : FiniteHeightLattice (A × B)
+            finiteHeightLattice : FiniteHeightLattice (A × B)
-    finiteHeightLattice = record
+            finiteHeightLattice = record
-        { height = h₁ + h₂
+                { height = h₁ + h₂
-        ; _≈_ = _≈_
+                ; _≈_ = _≈_
-        ; _⊔_ = _⊔_
+                ; _⊔_ = _⊔_
-        ; _⊓_ = _⊓_
+                ; _⊓_ = _⊓_
-        ; isFiniteHeightLattice = isFiniteHeightLattice
+                ; isFiniteHeightLattice = isFiniteHeightLattice
-        }
+                }

Lattice/Unit.agda

@@ -7,6 +7,7 @@ open import Data.Unit using (⊤; tt) public
 open import Data.Unit.Properties using (_≟_; ≡-setoid)
 open import Relation.Binary using (Setoid)
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_)
+open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Nullary using (Dec; ¬_; yes; no)
 open import Equivalence
 open import Lattice
@@ -24,9 +25,13 @@ _≈_ = _≡_
     ; ≈-trans = trans
     }
 
-≈-dec : IsDecidable _≈_
+≈-dec : Decidable _≈_
 ≈-dec = _≟_
 
+instance
+    ≈-Decidable : IsDecidable _≈_
+    ≈-Decidable = record { R-dec = ≈-dec }
+
 _⊔_ : ⊤ → ⊤ → ⊤
 tt ⊔ tt = tt
 
@@ -45,14 +50,15 @@ tt ⊓ tt = tt
 ⊔-idemp : (x : ⊤) → (x ⊔ x) ≈ x
 ⊔-idemp tt = Eq.refl
 
-isJoinSemilattice : IsSemilattice ⊤ _≈_ _⊔_
+instance
-isJoinSemilattice = record
+    isJoinSemilattice : IsSemilattice ⊤ _≈_ _⊔_
-    { ≈-equiv = ≈-equiv
+    isJoinSemilattice = record
-    ; ≈-⊔-cong = ≈-⊔-cong
+        { ≈-equiv = ≈-equiv
-    ; ⊔-assoc = ⊔-assoc
+        ; ≈-⊔-cong = ≈-⊔-cong
-    ; ⊔-comm  = ⊔-comm
+        ; ⊔-assoc = ⊔-assoc
-    ; ⊔-idemp = ⊔-idemp
+        ; ⊔-comm  = ⊔-comm
-    }
+        ; ⊔-idemp = ⊔-idemp
+        }
 
 ≈-⊓-cong : ∀ {ab₁ ab₂ ab₃ ab₄} → ab₁ ≈ ab₂ → ab₃ ≈ ab₄ → (ab₁ ⊓ ab₃) ≈ (ab₂ ⊓ ab₄)
 ≈-⊓-cong {tt} {tt} {tt} {tt} _ _ = Eq.refl
@@ -66,36 +72,32 @@ isJoinSemilattice = record
 ⊓-idemp : (x : ⊤) → (x ⊓ x) ≈ x
 ⊓-idemp tt = Eq.refl
 
-isMeetSemilattice : IsSemilattice ⊤ _≈_ _⊓_
+instance
-isMeetSemilattice = record
+    isMeetSemilattice : IsSemilattice ⊤ _≈_ _⊓_
-    { ≈-equiv = ≈-equiv
+    isMeetSemilattice = record
-    ; ≈-⊔-cong = ≈-⊓-cong
+        { ≈-equiv = ≈-equiv
-    ; ⊔-assoc = ⊓-assoc
+        ; ≈-⊔-cong = ≈-⊓-cong
-    ; ⊔-comm  = ⊓-comm
+        ; ⊔-assoc = ⊓-assoc
-    ; ⊔-idemp = ⊓-idemp
+        ; ⊔-comm  = ⊓-comm
-    }
+        ; ⊔-idemp = ⊓-idemp
+        }
 
-absorb-⊔-⊓ : (x y : ⊤) → (x ⊔ (x ⊓ y)) ≈ x
+instance
-absorb-⊔-⊓ tt tt = Eq.refl
+    isLattice : IsLattice ⊤ _≈_ _⊔_ _⊓_
+    isLattice = record
+        { joinSemilattice = isJoinSemilattice
+        ; meetSemilattice = isMeetSemilattice
+        ; absorb-⊔-⊓ = λ { tt tt → Eq.refl }
+        ; absorb-⊓-⊔ = λ { tt tt → Eq.refl }
+        }
 
-absorb-⊓-⊔ : (x y : ⊤) → (x ⊓ (x ⊔ y)) ≈ x
+    lattice : Lattice ⊤
-absorb-⊓-⊔ tt tt = Eq.refl
+    lattice = record
-
+        { _≈_ = _≈_
-isLattice : IsLattice ⊤ _≈_ _⊔_ _⊓_
+        ; _⊔_ = _⊔_
-isLattice = record
+        ; _⊓_ = _⊓_
-    { joinSemilattice = isJoinSemilattice
+        ; isLattice = isLattice
-    ; meetSemilattice = isMeetSemilattice
+        }
-    ; absorb-⊔-⊓ = absorb-⊔-⊓
-    ; absorb-⊓-⊔ = absorb-⊓-⊔
-    }
-
-lattice : Lattice ⊤
-lattice = record
-    { _≈_ = _≈_
-    ; _⊔_ = _⊔_
-    ; _⊓_ = _⊓_
-    ; isLattice = isLattice
-    }
 
 open Chain _≈_ ≈-equiv (IsLattice._≺_ isLattice) (IsLattice.≺-cong isLattice)
 
@@ -107,25 +109,26 @@ private
     isLongest {tt} {tt} (step (tt⊔tt≈tt , tt̷≈tt) _ _) = ⊥-elim (tt̷≈tt refl)
     isLongest (done _) = z≤n
 
-fixedHeight : IsLattice.FixedHeight isLattice 0
+instance
-fixedHeight = record
+    fixedHeight : IsLattice.FixedHeight isLattice 0
-    { ⊥ = tt
+    fixedHeight = record
-    ; ⊤ = tt
+        { ⊥ = tt
-    ; longestChain = longestChain
+        ; ⊤ = tt
-    ; bounded = isLongest
+        ; longestChain = longestChain
-    }
+        ; bounded = isLongest
+        }
 
-isFiniteHeightLattice : IsFiniteHeightLattice ⊤ 0 _≈_ _⊔_ _⊓_
+    isFiniteHeightLattice : IsFiniteHeightLattice ⊤ 0 _≈_ _⊔_ _⊓_
-isFiniteHeightLattice = record
+    isFiniteHeightLattice = record
-    { isLattice = isLattice
+        { isLattice = isLattice
-    ; fixedHeight = fixedHeight
+        ; fixedHeight = fixedHeight
-    }
+        }
 
-finiteHeightLattice : FiniteHeightLattice ⊤
+    finiteHeightLattice : FiniteHeightLattice ⊤
-finiteHeightLattice = record
+    finiteHeightLattice = record
-    { height = 0
+        { height = 0
-    ; _≈_ = _≈_
+        ; _≈_ = _≈_
-    ; _⊔_ = _⊔_
+        ; _⊔_ = _⊔_
-    ; _⊓_ = _⊓_
+        ; _⊓_ = _⊓_
-    ; isFiniteHeightLattice = isFiniteHeightLattice
+        ; isFiniteHeightLattice = isFiniteHeightLattice
-    }
+        }

Main.agda

@@ -1,11 +1,13 @@
 {-# OPTIONS --guardedness #-}
 module Main where
 
-open import Language
+open import Language hiding (_++_)
-open import Analysis.Sign
 open import Data.Vec using (Vec; _∷_; [])
 open import IO
 open import Level using (0ℓ)
+open import Data.String using (_++_)
+import Analysis.Constant as ConstantAnalysis
+import Analysis.Sign as SignAnalysis
 
 testCode : Stmt
 testCode =
@@ -38,6 +40,7 @@ testProgram = record
     { rootStmt = testCode
     }
 
-open WithProg testProgram using (output; analyze-correct)
+open SignAnalysis.WithProg testProgram using (analyze-correct) renaming (output to output-Sign)
+open ConstantAnalysis.WithProg testProgram using (analyze-correct) renaming (output to output-Const)
 
-main = run {0ℓ} (putStrLn output)
+main = run {0ℓ} (putStrLn (output-Const ++ "\n" ++ output-Sign))

Utils.agda

@@ -103,3 +103,6 @@ _∨_ P Q a = P a ⊎ Q a
 _∧_ : ∀ {a p₁ p₂} {A : Set a} (P : A → Set p₁) (Q : A → Set p₂) →
       A → Set (p₁ ⊔ℓ p₂)
 _∧_ P Q a = P a × Q a
+
+it : ∀ {a} {A : Set a} {{_ : A}} → A
+it {{x}} = x