Add decidability proofs for properties

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

@@ -8,6 +8,7 @@ module Analysis.Forward
     {{≈ˡ-dec : IsDecidable _≈ˡ_}} where
 
 open import Data.Empty using (⊥-elim)
+open import Data.Unit using (⊤)
 open import Data.String using (String)
 open import Data.Product using (_,_)
 open import Data.List using (_∷_; []; foldr; foldl)
@@ -20,7 +21,7 @@ open IsFiniteHeightLattice isFiniteHeightLatticeˡ
     using () renaming (isLattice to isLatticeˡ)
 
 module WithProg (prog : Program) where
-    open import Analysis.Forward.Lattices L prog hiding (≈ᵛ-Decidable) -- to disambiguate instance resolution
+    open import Analysis.Forward.Lattices L prog hiding (≈ᵛ-Decidable; ≈ᵐ-Decidable) -- to disambiguate instance resolution
     open import Analysis.Forward.Evaluation L prog
     open Program prog
 
@@ -65,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 ≈ᵐ-Decidable 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
@@ -77,7 +78,7 @@ module WithProg (prog : Program) where
             updateAll-k∈ks-≡ {l = sv} (states-complete s) s,vs∈usv
 
         module WithValidInterpretation {{latticeInterpretationˡ : LatticeInterpretation isLatticeˡ}}
-                                       {{validEvaluator : ValidStmtEvaluator evaluator latticeInterpretationˡ}} where
+                                       {{validEvaluator : ValidStmtEvaluator evaluator latticeInterpretationˡ}} (dummy : ⊤) where
             open ValidStmtEvaluator validEvaluator
 
             eval-fold-valid : ∀ {s bss vs ρ₁ ρ₂} → ρ₁ , bss ⇒ᵇˢ ρ₂ → ⟦ vs ⟧ᵛ ρ₁ → ⟦ foldl (flip (eval s)) vs bss ⟧ᵛ ρ₂

Analysis/Forward/Lattices.agda

@@ -10,7 +10,6 @@ module Analysis.Forward.Lattices
 
 open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
 open import Data.Product using (proj₁; proj₂; _,_)
-open import Data.Unit using (tt)
 open import Data.Sum using (inj₁; inj₂)
 open import Data.List using (List; _∷_; []; foldr)
 open import Data.List.Membership.Propositional using () renaming (_∈_ to _∈ˡ_)
@@ -38,7 +37,7 @@ instance
 -- 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.WithKeys String L tt vars
+module VariableValuesFiniteMap = Lattice.FiniteMap String L vars
 open VariableValuesFiniteMap
     using ()
     renaming
@@ -55,23 +54,13 @@ open VariableValuesFiniteMap
         ; 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ˡ
+        ; Provenance-union to Provenance-unionᵛ
+        ; ⊔-Monotonicˡ to ⊔ᵛ-Monotonicˡ
         ; ⊔-Monotonicʳ to ⊔ᵛ-Monotonicʳ
         ; ⊔-idemp to ⊔ᵛ-idemp
         )
     public
-open Lattice.FiniteMap.IterProdIsomorphism String L _
-    using ()
-    renaming
-        ( Provenance-union to Provenance-unionᵐ
-        )
-    public
-open Lattice.FiniteMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight String L _ vars-Unique
+open VariableValuesFiniteMap.FixedHeight vars-Unique
     using ()
     renaming
         ( isFiniteHeightLattice to isFiniteHeightLatticeᵛ
@@ -83,7 +72,7 @@ open Lattice.FiniteMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight String L
 ⊥ᵛ = Chain.Height.⊥ fixedHeightᵛ
 
 -- Finally, the map we care about is (state -> (variables -> value)). Bring that in.
-module StateVariablesFiniteMap = Lattice.FiniteMap.WithKeys State VariableValues tt states
+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
@@ -96,20 +85,15 @@ open StateVariablesFiniteMap
         ; _≼_ to _≼ᵐ_
         ; ≈-Decidable to ≈ᵐ-Decidable
         ; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ
+        ; ≈-sym to ≈ᵐ-sym
         )
     public
-open Lattice.FiniteMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight State VariableValues _ states-Unique
+open StateVariablesFiniteMap.FixedHeight states-Unique
     using ()
     renaming
         ( isFiniteHeightLattice to isFiniteHeightLatticeᵐ
         )
     public
-open IsFiniteHeightLattice isFiniteHeightLatticeᵐ
-    using ()
-    renaming
-        ( ≈-sym to ≈ᵐ-sym
-        )
-    public
 
 -- We now have our (state -> (variables -> value)) map.
 -- Define a couple of helpers to retrieve values from it. Specifically,
@@ -197,7 +181,7 @@ module _ {{latticeInterpretationˡ : LatticeInterpretation isLatticeˡ}} where
     ⟦⟧ᵛ-⊔ᵛ-∨ : ∀ {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₁₂
+             ← 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∈ρ))

Analysis/Sign.agda

@@ -16,6 +16,7 @@ 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
@@ -78,10 +79,9 @@ open AB.Plain 0ˢ using ()
         ; _≼_ to _≼ᵍ_
         ; _⊔_ to _⊔ᵍ_
         ; _⊓_ to _⊓ᵍ_
+        ; ≼-trans to ≼ᵍ-trans
         )
 
-open IsLattice isLatticeᵍ using () renaming (≼-trans to ≼ᵍ-trans)
-
 plus : SignLattice → SignLattice → SignLattice
 plus ⊥ᵍ _ = ⊥ᵍ
 plus _ ⊥ᵍ = ⊥ᵍ
@@ -102,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 _ ⊥ᵍ = ⊥ᵍ
@@ -120,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
 ⟦_⟧ᵍ ⊥ᵍ _ = ⊥
 ⟦_⟧ᵍ ⊤ᵍ _ = ⊤
@@ -196,29 +202,13 @@ module WithProg (prog : Program) where
 
     eval-Monoʳ : ∀ (e : Expr) → Monotonic _≼ᵛ_ _≼ᵍ_ (eval e)
     eval-Monoʳ (e₁ + e₂) {vs₁} {vs₂} vs₁≼vs₂ =
-        let
-            -- TODO: 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
-                {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-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₂ =
-        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-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₂ =
@@ -302,4 +292,8 @@ module WithProg (prog : Program) where
     eval-valid (⇒ᵉ-ℕ ρ 0) _ = refl
     eval-valid (⇒ᵉ-ℕ ρ (suc n')) _ = (n' , refl)
 
-    analyze-correct = Analysis.Forward.WithProg.analyze-correct
+    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}
-                  (≈-Decidable : IsDecidable _≈_)
-                  (flA : IsFiniteHeightLattice A h _≈_ _⊔_ _⊓_)
+                  {{ ≈-Decidable : IsDecidable _≈_ }}
+                  {{flA : IsFiniteHeightLattice A h _≈_ _⊔_ _⊓_}}
                   (f : A → A)
                   (Monotonicᶠ : Monotonic (IsFiniteHeightLattice._≼_ flA)
                                           (IsFiniteHeightLattice._≼_ flA) f) where
@@ -28,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
@@ -65,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
@@ -85,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

@@ -68,6 +68,7 @@ module TransportFiniteHeight
         renaming (⊥ to ⊥₁; ⊤ to ⊤₁; bounded to bounded₁; longestChain to c)
 
     instance
+        fixedHeight : IsLattice.FixedHeight lB height
         fixedHeight = record
             { ⊥ = f ⊥₁
             ; ⊤ = f ⊤₁

Language/Graphs.agda

@@ -124,28 +124,6 @@ buildCfg (s₁ then s₂) = buildCfg s₁ ↦ buildCfg s₂
 buildCfg (if _ then s₁ else s₂) = buildCfg s₁ ∙ buildCfg s₂
 buildCfg (while _ repeat s) = loop (buildCfg s)
 
-private
-    z≢sf : ∀ {n : ℕ} (f : Fin n) → ¬ (zero ≡ suc f)
-    z≢sf f ()
-
-    z≢mapsfs : ∀ {n : ℕ} (fs : List (Fin n)) → All (λ sf → ¬ zero ≡ sf) (List.map suc fs)
-    z≢mapsfs [] = []
-    z≢mapsfs (f ∷ fs') = z≢sf f ∷ z≢mapsfs fs'
-
-    finValues : ∀ (n : ℕ) → Σ (List (Fin n)) Unique
-    finValues 0 = ([] , Utils.empty)
-    finValues (suc n') =
-        let
-            (inds' , unids') = finValues n'
-        in
-            ( zero ∷ List.map suc inds'
-            , push (z≢mapsfs inds') (Unique-map suc suc-injective unids')
-            )
-
-    finValues-complete : ∀ (n : ℕ) (f : Fin n) → f ListMem.∈ (proj₁ (finValues n))
-    finValues-complete (suc n') zero = RelAny.here refl
-    finValues-complete (suc n') (suc f') = RelAny.there (x∈xs⇒fx∈fxs suc (finValues-complete n' f'))
-
 module _ (g : Graph) where
     open import Data.Product.Properties as ProdProp using ()
     private _≟_ = ProdProp.≡-dec (FinProp._≟_ {Graph.size g})
@@ -154,13 +132,13 @@ module _ (g : Graph) where
     open import Data.List.Membership.DecPropositional (_≟_) using (_∈?_)
 
     indices : List (Graph.Index g)
-    indices = proj₁ (finValues (Graph.size g))
+    indices = proj₁ (fins (Graph.size g))
 
     indices-complete : ∀ (idx : (Graph.Index g)) → idx ListMem.∈ indices
-    indices-complete = finValues-complete (Graph.size g)
+    indices-complete = fins-complete (Graph.size g)
 
     indices-Unique : Unique indices
-    indices-Unique = proj₂ (finValues (Graph.size g))
+    indices-Unique = proj₂ (fins (Graph.size g))
 
     predecessors : (Graph.Index g) → List (Graph.Index g)
     predecessors idx = List.filter (λ idx' → (idx' , idx) ∈? (Graph.edges g)) indices

Lattice.agda

@@ -4,7 +4,8 @@ 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₂)
@@ -21,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
@@ -224,6 +237,28 @@ record IsFiniteHeightLattice {a} (A : Set a)
     field
         {{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}
     {_⊔₁_ : A → A → A} {_⊔₂_ : B → B → B}

Lattice/AboveBelow.agda

@@ -321,7 +321,7 @@ module Plain (x : A) where
             ; 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 , λ ())

Lattice/Builder.agda

@@ -0,0 +1,381 @@
+module Lattice.Builder where
+
+open import Lattice
+open import Equivalence
+open import Utils using (Unique; push; empty; Unique-append; Unique-++⁻ˡ; Unique-++⁻ʳ; Unique-narrow; All¬-¬Any; ¬Any-map; fins; fins-complete; findUniversal; Decidable-¬)
+open import Data.Nat as Nat using (ℕ)
+open import Data.Fin as Fin using (Fin; suc; zero; _≟_)
+open import Data.Maybe as Maybe using (Maybe; just; nothing; _>>=_; maybe)
+open import Data.Maybe.Properties using (just-injective)
+open import Data.Unit using (⊤; tt)
+open import Data.List.NonEmpty using (List⁺; tail; toList) renaming (_∷_ to _∷⁺_)
+open import Data.List.Membership.Propositional as MemProp using (lose) renaming (_∈_ to _∈ˡ_; mapWith∈ to mapWith∈ˡ)
+open import Data.List.Membership.Propositional.Properties using () renaming (∈-++⁺ʳ to ∈ˡ-++⁺ʳ; ∈-++⁺ˡ to ∈ˡ-++⁺ˡ; ∈-cartesianProductWith⁺ to ∈ˡ-cartesianProductWith⁺)
+open import Data.List.Relation.Unary.Any using (Any; here; there; any?; satisfied)
+open import Data.List.Relation.Unary.Any.Properties using (¬Any[])
+open import Data.List.Relation.Unary.All using (All; []; _∷_; map; lookup; zipWith; tabulate; all?)
+open import Data.List.Relation.Unary.All.Properties using () renaming (++⁺ to ++ˡ⁺; ++⁻ʳ to ++ˡ⁻ʳ)
+open import Data.List using (List; _∷_; []; cartesianProduct; cartesianProductWith; foldr) renaming (_++_ to _++ˡ_)
+open import Data.List.Properties using () renaming (++-conicalʳ to ++ˡ-conicalʳ; ++-identityʳ to ++ˡ-identityʳ; ++-assoc to ++ˡ-assoc)
+open import Data.Sum using (_⊎_; inj₁; inj₂)
+open import Data.Product using (Σ; _,_; _×_; proj₁; proj₂; uncurry)
+open import Data.Empty using (⊥; ⊥-elim)
+open import Relation.Nullary using (¬_; Dec; yes; no; ¬?)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst)
+open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
+open import Relation.Binary using () renaming (Decidable to Decidable²)
+open import Relation.Unary using (Decidable)
+open import Agda.Primitive using (lsuc; Level) renaming (_⊔_ to _⊔ℓ_)
+
+record Graph : Set where
+    constructor mkGraph
+    field
+        size : ℕ
+
+    Node : Set
+    Node = Fin size
+
+    nodes = fins size
+
+    nodes-complete = fins-complete size
+
+    Edge : Set
+    Edge = Node × Node
+
+    field
+        edges : List Edge
+
+    data Path : Node → Node → Set where
+        done : ∀ {n : Node} → Path n n
+        step : ∀ {n₁ n₂ n₃ : Node} →  (n₁ , n₂) ∈ˡ edges → Path n₂ n₃ → Path n₁ n₃
+
+    data IsDone : ∀ {n₁ n₂} → Path n₁ n₂ → Set where
+        isDone : ∀ {n : Node} → IsDone (done {n})
+
+    IsDone? : ∀ {n₁ n₂} → Decidable (IsDone {n₁} {n₂})
+    IsDone? done = yes isDone
+    IsDone? (step _ _) = no (λ {()})
+
+    _++_ : ∀ {n₁ n₂ n₃} → Path n₁ n₂ → Path n₂ n₃ → Path n₁ n₃
+    done ++ p = p
+    (step e p₁) ++ p₂ = step e (p₁ ++ p₂)
+
+    ++-done : ∀ {n₁ n₂} (p : Path n₁ n₂) → p ++ done ≡ p
+    ++-done done = refl
+    ++-done (step e∈edges p) rewrite ++-done p = refl
+
+    ++-assoc : ∀ {n₁ n₂ n₃ n₄} (p₁ : Path n₁ n₂) (p₂ : Path n₂ n₃) (p₃ : Path n₃ n₄) →
+                 (p₁ ++ p₂) ++ p₃ ≡ p₁ ++ (p₂ ++ p₃)
+    ++-assoc done p₂ p₃ = refl
+    ++-assoc (step n₁,n∈edges p₁) p₂ p₃ rewrite ++-assoc p₁ p₂ p₃ = refl
+
+    IsDone-++ˡ : ∀ {n₁ n₂ n₃} (p₁ : Path n₁ n₂) (p₂ : Path n₂ n₃) →
+                 ¬ IsDone p₁ → ¬ IsDone (p₁ ++ p₂)
+    IsDone-++ˡ done _ done≢done = ⊥-elim (done≢done isDone)
+
+    interior : ∀ {n₁ n₂} → Path n₁ n₂ → List Node
+    interior done = []
+    interior (step _ done) = []
+    interior (step {n₂ = n₂} _ p) = n₂ ∷ interior p
+
+    interior-extend : ∀ {n₁ n₂ n₃} → (p : Path n₁ n₂) →  (n₂,n₃∈edges : (n₂ , n₃) ∈ˡ edges) →
+                      let p' = (p ++ (step n₂,n₃∈edges done))
+                      in (interior p' ≡ interior p) ⊎ (interior p' ≡ interior p ++ˡ (n₂ ∷ []))
+    interior-extend done _ = inj₁ refl
+    interior-extend (step n₁,n₂∈edges done) n₂n₃∈edges = inj₂ refl
+    interior-extend {n₂ = n₂} (step {n₂ = n} n₁,n∈edges p@(step _ _)) n₂n₃∈edges
+        with p ++ (step n₂n₃∈edges done) | interior-extend p n₂n₃∈edges
+    ...   | done | inj₁ []≡intp rewrite sym []≡intp = inj₁ refl
+    ...   | done | inj₂ []=intp++[n₂] with () ← ++ˡ-conicalʳ (interior p) (n₂ ∷ []) (sym []=intp++[n₂])
+    ...   | step _ p | inj₁ IH rewrite IH = inj₁ refl
+    ...   | step _ p | inj₂ IH rewrite IH = inj₂ refl
+
+    interior-++ : ∀ {n₁ n₂ n₃} → (p₁ : Path n₁ n₂) →  (p₂ : Path n₂ n₃) →
+                    ¬ IsDone p₁ → ¬ IsDone p₂ →
+                    interior (p₁ ++ p₂) ≡ interior p₁ ++ˡ (n₂ ∷ interior p₂)
+    interior-++ done _ done≢done _ = ⊥-elim (done≢done isDone)
+    interior-++ _ done _ done≢done = ⊥-elim (done≢done isDone)
+    interior-++ (step _ done) (step _ _) _ _ = refl
+    interior-++ (step n₁,n∈edges p@(step n,n'∈edges p')) p₂ _ p₂≢done
+        rewrite interior-++ p p₂ (λ {()}) p₂≢done = refl
+
+    SimpleWalkVia : List Node → Node → Node → Set
+    SimpleWalkVia ns n₁ n₂ = Σ (Path n₁ n₂) (λ p → Unique (interior p) × All (_∈ˡ ns) (interior p))
+
+    SimpleWalk-extend : ∀ {n₁ n₂ n₃ ns} →  (w : SimpleWalkVia ns n₁ n₂) → (n₂ , n₃) ∈ˡ edges →  All (λ nʷ →  ¬ nʷ ≡ n₂) (interior (proj₁ w)) → n₂ ∈ˡ ns → SimpleWalkVia ns n₁ n₃
+    SimpleWalk-extend (p , (Unique-intp , intp⊆ns)) n₂,n₃∈edges w≢n₂ n₂∈ns
+        with p ++ (step n₂,n₃∈edges done) | interior-extend p n₂,n₃∈edges
+    ...   | p' | inj₁ intp'≡intp rewrite sym intp'≡intp = (p' , Unique-intp , intp⊆ns)
+    ...   | p' | inj₂ intp'≡intp++[n₂]
+            with intp++[n₂]⊆ns ←  ++ˡ⁺ intp⊆ns (n₂∈ns ∷ [])
+            rewrite sym intp'≡intp++[n₂] = (p' , (subst Unique (sym intp'≡intp++[n₂]) (Unique-append (¬Any-map sym (All¬-¬Any w≢n₂)) Unique-intp) , intp++[n₂]⊆ns))
+
+    ∈ˡ-narrow : ∀ {x y : Node} {ys : List Node} → x ∈ˡ (y ∷ ys) → ¬ y ≡ x → x ∈ˡ ys
+    ∈ˡ-narrow (here refl) x≢y = ⊥-elim (x≢y refl)
+    ∈ˡ-narrow (there x∈ys) _ = x∈ys
+
+    SplitSimpleWalkViaHelp : ∀ {n n₁ n₂ ns} (nⁱ : Node)
+                                            (w : SimpleWalkVia (n ∷ ns) n₁ n₂)
+                                            (p₁ : Path n₁ nⁱ) (p₂ : Path nⁱ n₂) →
+                                            ¬ IsDone p₁ → ¬ IsDone p₂ →
+                                            All (_∈ˡ ns) (interior p₁) →
+                                            proj₁ w ≡ p₁ ++ p₂ →
+                                            (Σ (SimpleWalkVia ns n₁ n × SimpleWalkVia ns n n₂) λ (w₁ , w₂) → proj₁ w₁ ++ proj₁ w₂ ≡ proj₁ w) ⊎ (Σ (SimpleWalkVia ns n₁ n₂) λ w' → proj₁ w' ≡ proj₁ w)
+    SplitSimpleWalkViaHelp nⁱ w done _ done≢done _ _ _ = ⊥-elim (done≢done isDone)
+    SplitSimpleWalkViaHelp nⁱ w p₁ done _ done≢done _ _ = ⊥-elim (done≢done isDone)
+    SplitSimpleWalkViaHelp {n} {ns = ns} nⁱ w@(p , (Unique-intp , intp⊆ns)) p₁@(step _ _) p₂@(step {n₂ = nⁱ'} nⁱ,nⁱ',∈edges p₂') p₁≢done p₂≢done intp₁⊆ns p≡p₁++p₂
+        with intp≡intp₁++[n]++intp₂ ← trans (cong interior p≡p₁++p₂) (interior-++ p₁ p₂ p₁≢done p₂≢done)
+        with nⁱ∈n∷ns ∷ intp₂⊆n∷ns ← ++ˡ⁻ʳ (interior p₁) (subst (All (_∈ˡ (n ∷ ns))) intp≡intp₁++[n]++intp₂ intp⊆ns)
+        with nⁱ ≟ n
+    ...   | yes refl
+            with Unique-intp₁ ← Unique-++⁻ˡ (interior p₁) (subst Unique intp≡intp₁++[n]++intp₂ Unique-intp)
+            with (push n≢intp₂ Unique-intp₂) ← Unique-++⁻ʳ (interior p₁) (subst Unique intp≡intp₁++[n]++intp₂ Unique-intp)
+            = inj₁ (((p₁ , (Unique-intp₁ , intp₁⊆ns)) , (p₂ , (Unique-intp₂ , zipWith (uncurry ∈ˡ-narrow) (intp₂⊆n∷ns , n≢intp₂)))) , sym p≡p₁++p₂)
+    ...   | no nⁱ≢n
+            with p₂'
+    ...       | done
+                = let
+                      -- note: copied with below branch. can't use with <- to
+                      --       share and re-use because the termination checker loses the thread.
+                      p₁' = (p₁ ++ (step nⁱ,nⁱ',∈edges done))
+                      n≢nⁱ n≡nⁱ = nⁱ≢n (sym n≡nⁱ)
+                      intp₁'=intp₁++[nⁱ] = subst (λ xs → interior p₁' ≡ interior p₁ ++ˡ xs) (++ˡ-identityʳ (nⁱ ∷ [])) (interior-++ p₁ (step nⁱ,nⁱ',∈edges done) p₁≢done (λ {()}))
+                      intp₁++[nⁱ]⊆ns = ++ˡ⁺ intp₁⊆ns (∈ˡ-narrow nⁱ∈n∷ns n≢nⁱ ∷ [])
+                      intp₁'⊆ns = subst (All (_∈ˡ ns)) (sym intp₁'=intp₁++[nⁱ]) intp₁++[nⁱ]⊆ns
+                      -- end shared with below branch.
+                      Unique-intp₁++[nⁱ] = Unique-++⁻ˡ (interior p₁ ++ˡ (nⁱ ∷ [])) (subst Unique (trans intp≡intp₁++[n]++intp₂ (sym (++ˡ-assoc (interior p₁) (nⁱ ∷ []) []))) Unique-intp)
+                  in inj₂ ((p₁ ++ (step nⁱ,nⁱ',∈edges done) , (subst Unique (sym intp₁'=intp₁++[nⁱ]) Unique-intp₁++[nⁱ] , intp₁'⊆ns)) , sym p≡p₁++p₂)
+    ...       | p₂'@(step _ _)
+                = let p₁' = (p₁ ++ (step nⁱ,nⁱ',∈edges done))
+                      n≢nⁱ n≡nⁱ = nⁱ≢n (sym n≡nⁱ)
+                      intp₁'=intp₁++[nⁱ] = subst (λ xs → interior p₁' ≡ interior p₁ ++ˡ xs) (++ˡ-identityʳ (nⁱ ∷ [])) (interior-++ p₁ (step nⁱ,nⁱ',∈edges done) p₁≢done (λ {()}))
+                      intp₁++[nⁱ]⊆ns = ++ˡ⁺ intp₁⊆ns (∈ˡ-narrow nⁱ∈n∷ns n≢nⁱ ∷ [])
+                      intp₁'⊆ns = subst (All (_∈ˡ ns)) (sym intp₁'=intp₁++[nⁱ]) intp₁++[nⁱ]⊆ns
+                      p≡p₁'++p₂' = trans p≡p₁++p₂ (sym (++-assoc p₁ (step nⁱ,nⁱ',∈edges done) p₂'))
+                  in SplitSimpleWalkViaHelp nⁱ' w p₁' p₂' (IsDone-++ˡ _ _ p₁≢done) (λ {()}) intp₁'⊆ns p≡p₁'++p₂'
+
+    SplitSimpleWalkVia : ∀ {n n₁ n₂ ns} (w : SimpleWalkVia (n ∷ ns) n₁ n₂) →  (Σ (SimpleWalkVia ns n₁ n × SimpleWalkVia ns n n₂) λ (w₁ , w₂) → proj₁ w₁ ++ proj₁ w₂ ≡ proj₁ w) ⊎ (Σ (SimpleWalkVia ns n₁ n₂) λ w' → proj₁ w' ≡ proj₁ w)
+    SplitSimpleWalkVia (done , (_ , _)) = inj₂ ((done , (empty , [])) , refl)
+    SplitSimpleWalkVia (step n₁,n₂∈edges done , (_ , _)) = inj₂ ((step n₁,n₂∈edges done , (empty , [])) , refl)
+    SplitSimpleWalkVia w@(step {n₂ = nⁱ} n₁,nⁱ∈edges p@(step  _ _) , (push nⁱ≢intp Unique-intp , nⁱ∈ns ∷ intp⊆ns)) = SplitSimpleWalkViaHelp nⁱ w (step n₁,nⁱ∈edges done) p (λ {()}) (λ {()}) [] refl
+
+    open import Data.List.Membership.DecSetoid (decSetoid {A = Node} _≟_) using () renaming (_∈?_ to _∈ˡ?_)
+
+    splitFromInteriorʳ : ∀ {n₁ n₂ n} (p : Path n₁ n₂) → n ∈ˡ (interior p) →
+                        Σ (Path n n₂) (λ p' → ¬ IsDone p' × (Σ (List Node) λ ns → interior p ≡ ns ++ˡ n ∷ interior p'))
+    splitFromInteriorʳ done ()
+    splitFromInteriorʳ (step _ done) ()
+    splitFromInteriorʳ (step {n₂ = n'} n₁,n'∈edges p'@(step _ _)) (here refl) = (p' , ((λ {()}) , ([] , refl)))
+    splitFromInteriorʳ (step {n₂ = n'} n₁,n'∈edges p'@(step _ _)) (there n∈intp')
+        with (p'' , (¬IsDone-p'' , (ns , intp'≡ns++intp''))) ← splitFromInteriorʳ p' n∈intp'
+        rewrite intp'≡ns++intp'' = (p'' , (¬IsDone-p'' , (n' ∷ ns , refl)))
+
+    splitFromInteriorˡ : ∀ {n₁ n₂ n} (p : Path n₁ n₂) → n ∈ˡ (interior p) →
+                        Σ (Path n₁ n) (λ p' → ¬ IsDone p' × (Σ (List Node) λ ns → interior p ≡ interior p' ++ˡ ns))
+    splitFromInteriorˡ done ()
+    splitFromInteriorˡ (step _ done) ()
+    splitFromInteriorˡ p@(step {n₂ = n'} n₁,n'∈edges p'@(step _ _)) (here refl) = (step n₁,n'∈edges done , ((λ {()}) , (interior p , refl)))
+    splitFromInteriorˡ p@(step {n₂ = n'} n₁,n'∈edges p'@(step _ _)) (there n∈intp')
+        with splitFromInteriorˡ p' n∈intp'
+    ...   | (p''@(step _ _) , (¬IsDone-p'' , (ns , intp'≡intp''++ns)))
+            rewrite intp'≡intp''++ns
+            = (step n₁,n'∈edges p'' , ((λ { () }) , (ns , refl)))
+    ...   | (done , (¬IsDone-Done , _)) = ⊥-elim (¬IsDone-Done isDone)
+
+    findCycleHelp : ∀ {n₁ nⁱ n₂} (p : Path n₁ n₂) (p₁ : Path n₁ nⁱ) (p₂ : Path nⁱ n₂) →
+                      ¬ IsDone p₁ → Unique (interior p₁) →
+                      p ≡ p₁ ++ p₂ →
+                      (Σ (SimpleWalkVia (proj₁ nodes) n₁ n₂) λ w → proj₁ w ≡ p) ⊎ (Σ Node (λ n → Σ (SimpleWalkVia (proj₁ nodes) n n) λ w →  ¬ IsDone (proj₁ w)))
+    findCycleHelp p p₁ done ¬IsDonep₁ Unique-intp₁ p≡p₁++done rewrite ++-done p₁ = inj₁ ((p₁ , (Unique-intp₁ , tabulate (λ {x} _ → nodes-complete x))) , sym p≡p₁++done)
+    findCycleHelp {nⁱ = nⁱ} p p₁ (step nⁱ,nⁱ'∈edges p₂') ¬IsDone-p₁ Unique-intp₁ p≡p₁++p₂
+        with nⁱ ∈ˡ? interior p₁
+    ...   | no nⁱ∉intp₁ =
+            let p₁' = p₁ ++ step nⁱ,nⁱ'∈edges done
+                intp₁'≡intp₁++[nⁱ] = subst (λ xs → interior p₁' ≡ interior p₁ ++ˡ xs) (++ˡ-identityʳ (nⁱ ∷ [])) (interior-++ p₁ (step nⁱ,nⁱ'∈edges done) ¬IsDone-p₁ (λ {()}))
+                ¬IsDone-p₁' = IsDone-++ˡ p₁ (step nⁱ,nⁱ'∈edges done) ¬IsDone-p₁
+                p≡p₁'++p₂' = trans p≡p₁++p₂ (sym (++-assoc p₁ (step nⁱ,nⁱ'∈edges done) p₂'))
+                Unique-intp₁' = subst Unique (sym intp₁'≡intp₁++[nⁱ]) (Unique-append nⁱ∉intp₁ Unique-intp₁)
+            in findCycleHelp p p₁' p₂' ¬IsDone-p₁' Unique-intp₁' p≡p₁'++p₂'
+    ...   | yes nⁱ∈intp₁
+            with (pᶜ , (¬IsDone-pᶜ , (ns , intp₁≡ns++intpᶜ))) ← splitFromInteriorʳ p₁ nⁱ∈intp₁
+            rewrite sym (++ˡ-assoc ns (nⁱ ∷ []) (interior pᶜ)) =
+            let Unique-intp₁' = subst Unique intp₁≡ns++intpᶜ Unique-intp₁
+            in inj₂ (nⁱ , ((pᶜ , (Unique-++⁻ʳ (ns ++ˡ nⁱ ∷ [])  Unique-intp₁' , tabulate (λ {x} _ → nodes-complete x))) , ¬IsDone-pᶜ))
+
+    findCycle : ∀ {n₁ n₂} (p : Path n₁ n₂) →  (Σ (SimpleWalkVia (proj₁ nodes) n₁ n₂) λ w → proj₁ w ≡ p) ⊎ (Σ Node (λ n → Σ (SimpleWalkVia (proj₁ nodes) n n) λ w →  ¬ IsDone (proj₁ w)))
+    findCycle done = inj₁ ((done , (empty , [])) , refl)
+    findCycle (step n₁,n₂∈edges done) = inj₁ ((step n₁,n₂∈edges done , (empty , [])) , refl)
+    findCycle p@(step {n₂ = n'} n₁,n'∈edges p'@(step _ _)) = findCycleHelp p (step n₁,n'∈edges done) p' (λ {()}) empty refl
+
+    toSimpleWalk : ∀ {n₁ n₂} (p : Path n₁ n₂) → SimpleWalkVia (proj₁ nodes) n₁ n₂
+    toSimpleWalk done = (done , (empty , []))
+    toSimpleWalk (step {n₂ = nⁱ} n₁,nⁱ∈edges p')
+        with toSimpleWalk p'
+    ...   | (done , _) = (step n₁,nⁱ∈edges done , (empty , []))
+    ...   | (p''@(step _ _) , (Unique-intp'' , intp''⊆nodes))
+            with nⁱ ∈ˡ? interior p''
+    ...       | no nⁱ∉intp'' = (step n₁,nⁱ∈edges p'' , (push (tabulate (λ { n∈intp'' refl →  nⁱ∉intp'' n∈intp'' })) Unique-intp'' , (nodes-complete nⁱ) ∷ intp''⊆nodes))
+    ...       | yes nⁱ∈intp''
+                with splitFromInteriorʳ p'' nⁱ∈intp''
+    ...           | (done , (¬IsDone=p''ʳ , (ns , intp''≡ns++intp''ʳ))) = ⊥-elim (¬IsDone=p''ʳ isDone)
+    ...           | (p''ʳ@(step _ _) , (¬IsDone=p''ʳ , (ns , intp''≡ns++intp''ʳ))) =
+                    -- no rewrites because then I can't reason about the return value of toSimpleWalk
+                    -- rewrite intp''≡ns++intp''ʳ
+                    -- rewrite sym (++ˡ-assoc ns (nⁱ ∷ []) (interior p''ʳ)) =
+                    let reassoc-intp''≡ns++intp''ʳ = subst (interior p'' ≡_) (sym (++ˡ-assoc ns (nⁱ ∷ []) (interior p''ʳ))) intp''≡ns++intp''ʳ
+                        intp''ʳ⊆nodes = ++ˡ⁻ʳ (ns ++ˡ nⁱ ∷ []) (subst (All (_∈ˡ (proj₁ nodes))) reassoc-intp''≡ns++intp''ʳ intp''⊆nodes)
+                        Unique-ns++intp''ʳ = subst Unique reassoc-intp''≡ns++intp''ʳ Unique-intp''
+                        nⁱ∈p''ˡ = ∈ˡ-++⁺ʳ ns {ys = nⁱ ∷ []} (here refl)
+                    in (step n₁,nⁱ∈edges p''ʳ , (Unique-narrow (ns ++ˡ nⁱ ∷ []) Unique-ns++intp''ʳ nⁱ∈p''ˡ , nodes-complete nⁱ ∷ intp''ʳ⊆nodes ))
+
+    toSimpleWalk-IsDone⁻ : ∀ {n₁ n₂} (p : Path n₁ n₂) →
+                          ¬ IsDone p → ¬ IsDone (proj₁ (toSimpleWalk p))
+    toSimpleWalk-IsDone⁻ done ¬IsDone-p _ = ¬IsDone-p isDone
+    toSimpleWalk-IsDone⁻ (step {n₂ = nⁱ} n₁,nⁱ∈edges p') _ isDone-w
+        with toSimpleWalk p'
+    ...   | (done , _) with () ← isDone-w
+    ...   | (p''@(step _ _) , (Unique-intp'' , intp''⊆nodes))
+            with nⁱ ∈ˡ? interior p''
+    ...       | no nⁱ∉intp'' with () ← isDone-w
+    ...       | yes nⁱ∈intp''
+                with splitFromInteriorʳ p'' nⁱ∈intp''
+    ...           | (done , (¬IsDone=p''ʳ , (ns , intp''≡ns++intp''ʳ))) = ¬IsDone=p''ʳ isDone
+    ...           | (p''ʳ@(step _ _) , (¬IsDone=p''ʳ , (ns , intp''≡ns++intp''ʳ)))
+                    with () ← isDone-w
+
+    Adjacency : Set
+    Adjacency = ∀ (n₁ n₂ : Node) → List (Path n₁ n₂)
+
+    Adjacency-update : ∀ (n₁ n₂ : Node) → (List (Path n₁ n₂) → List (Path n₁ n₂)) → Adjacency → Adjacency
+    Adjacency-update n₁ n₂ f adj n₁' n₂'
+        with n₁ ≟ n₁' | n₂ ≟ n₂'
+    ...  | yes refl | yes refl = f (adj n₁ n₂)
+    ...  | _        | _        = adj n₁' n₂'
+
+    Adjecency-append : ∀ {n₁ n₂ : Node} → List (Path n₁ n₂) → Adjacency → Adjacency
+    Adjecency-append {n₁} {n₂} ps = Adjacency-update n₁ n₂ (ps ++ˡ_)
+
+    Adjacency-append-monotonic : ∀ {adj n₁ n₂ n₁' n₂'} {ps : List (Path n₁ n₂)} {p : Path n₁' n₂'} → p ∈ˡ adj n₁' n₂' → p ∈ˡ Adjecency-append ps adj n₁' n₂'
+    Adjacency-append-monotonic {adj} {n₁} {n₂} {n₁'} {n₂'} {ps} p∈adj
+        with n₁ ≟ n₁' | n₂ ≟ n₂'
+    ...   | yes refl | yes refl = ∈ˡ-++⁺ʳ ps p∈adj
+    ...   | yes refl | no _ = p∈adj
+    ...   | no _ | no _ = p∈adj
+    ...   | no _ | yes _ = p∈adj
+
+    adj⁰ : Adjacency
+    adj⁰ n₁ n₂
+        with n₁ ≟ n₂
+    ... | yes refl = done ∷ []
+    ... | no _ = []
+
+    adj⁰-done : ∀ n →  done ∈ˡ adj⁰ n n
+    adj⁰-done n
+        with n ≟ n
+    ... | yes refl = here refl
+    ... | no n≢n = ⊥-elim (n≢n refl)
+
+    seedWithEdges : ∀ (es : List Edge) →  (∀ {e} → e ∈ˡ es → e ∈ˡ edges) → Adjacency → Adjacency
+    seedWithEdges es e∈es⇒e∈edges adj = foldr (λ ((n₁ , n₂) , n₁n₂∈edges) → Adjacency-update n₁ n₂ ((step n₁n₂∈edges done) ∷_)) adj (mapWith∈ˡ es (λ {e} e∈es →  (e , e∈es⇒e∈edges e∈es)))
+
+    seedWithEdges-monotonic : ∀ {n₁ n₂ es adj} → (e∈es⇒e∈edges : ∀ {e} → e ∈ˡ es → e ∈ˡ edges) → ∀ {p} → p ∈ˡ adj n₁ n₂ → p ∈ˡ seedWithEdges es e∈es⇒e∈edges adj n₁ n₂
+    seedWithEdges-monotonic {es = []} e∈es⇒e∈edges p∈adj = p∈adj
+    seedWithEdges-monotonic {es = (n₁ , n₂) ∷ es} e∈es⇒e∈edges p∈adj = Adjacency-append-monotonic {ps = step (e∈es⇒e∈edges (here refl)) done ∷ []} (seedWithEdges-monotonic (λ e∈es → e∈es⇒e∈edges (there e∈es)) p∈adj)
+
+    e∈seedWithEdges : ∀ {n₁ n₂ es adj} → (e∈es⇒e∈edges : ∀ {e} → e ∈ˡ es → e ∈ˡ edges) → ∀ (n₁n₂∈es : (n₁ , n₂) ∈ˡ es) →  (step (e∈es⇒e∈edges n₁n₂∈es) done) ∈ˡ seedWithEdges es e∈es⇒e∈edges adj n₁ n₂
+    e∈seedWithEdges {es = []} e∈es⇒e∈edges ()
+    e∈seedWithEdges {es = (n₁' , n₂') ∷ es} e∈es⇒e∈edges (here refl)
+        with n₁' ≟ n₁' | n₂' ≟ n₂'
+    ...   | yes refl | yes refl = here refl
+    ...   | no n₁'≢n₁' | _ = ⊥-elim (n₁'≢n₁' refl)
+    ...   | _ | no n₂'≢n₂' = ⊥-elim (n₂'≢n₂' refl)
+    e∈seedWithEdges {n₁} {n₂} {es = (n₁' , n₂') ∷ es} {adj} e∈es⇒e∈edges (there n₁n₂∈es) = Adjacency-append-monotonic {ps = step (e∈es⇒e∈edges (here refl)) done ∷ []} (e∈seedWithEdges (λ e∈es → e∈es⇒e∈edges (there e∈es)) n₁n₂∈es)
+
+    adj¹ : Adjacency
+    adj¹ = seedWithEdges edges (λ x → x) adj⁰
+
+    adj¹-adj⁰ : ∀ {n₁ n₂ p} → p ∈ˡ adj⁰ n₁ n₂ → p ∈ˡ adj¹ n₁ n₂
+    adj¹-adj⁰ p∈adj⁰ = seedWithEdges-monotonic (λ x → x) p∈adj⁰
+
+    edge∈adj¹ : ∀ {n₁ n₂} (n₁n₂∈edges : (n₁ , n₂) ∈ˡ edges) →  (step n₁n₂∈edges done) ∈ˡ adj¹ n₁ n₂
+    edge∈adj¹ = e∈seedWithEdges (λ x → x)
+
+    through : Node → Adjacency → Adjacency
+    through n adj n₁ n₂ = cartesianProductWith _++_ (adj n₁ n) (adj n n₂) ++ˡ adj n₁ n₂
+
+    through-monotonic : ∀ adj n {n₁ n₂ p} → p ∈ˡ adj n₁ n₂ → p ∈ˡ (through n adj) n₁ n₂
+    through-monotonic adj n p∈adjn₁n₂ = ∈ˡ-++⁺ʳ _ p∈adjn₁n₂
+
+    through-++ : ∀ adj n {n₁ n₂} {p₁ : Path n₁ n} {p₂ : Path n n₂} → p₁ ∈ˡ adj n₁ n → p₂ ∈ˡ adj n n₂ → (p₁ ++ p₂) ∈ˡ through n adj n₁ n₂
+    through-++ adj n p₁∈adj p₂∈adj = ∈ˡ-++⁺ˡ (∈ˡ-cartesianProductWith⁺ _++_ p₁∈adj p₂∈adj)
+
+    throughAll : List Node → Adjacency
+    throughAll = foldr through adj¹
+
+    throughAll-adj₁ : ∀ {n₁ n₂ p} ns → p ∈ˡ adj¹ n₁ n₂ → p ∈ˡ throughAll ns n₁ n₂
+    throughAll-adj₁ [] p∈adj¹ = p∈adj¹
+    throughAll-adj₁ (n ∷ ns) p∈adj¹ = through-monotonic (throughAll ns) n (throughAll-adj₁ ns p∈adj¹)
+
+    paths-throughAll : ∀ {n₁ n₂ : Node} (ns : List Node) (w : SimpleWalkVia ns n₁ n₂) →  proj₁ w ∈ˡ throughAll ns n₁ n₂
+    paths-throughAll {n₁} [] (done , (_ , _)) = adj¹-adj⁰ (adj⁰-done n₁)
+    paths-throughAll {n₁} [] (step e∈edges done , (_ , _)) = edge∈adj¹ e∈edges
+    paths-throughAll {n₁} [] (step _ (step _ _) , (_ , (() ∷ _)))
+    paths-throughAll (n ∷ ns) w
+        with SplitSimpleWalkVia w
+    ...  | inj₁ ((w₁ , w₂) , w₁++w₂≡w) rewrite sym w₁++w₂≡w = through-++ (throughAll ns) n (paths-throughAll ns w₁) (paths-throughAll ns w₂)
+    ...  | inj₂ (w' , w'≡w) rewrite sym w'≡w = through-monotonic (throughAll ns) n (paths-throughAll ns w')
+
+    adj : Adjacency
+    adj = throughAll (proj₁ nodes)
+
+    PathExists : Node → Node → Set
+    PathExists n₁ n₂ = Path n₁ n₂
+
+    PathExists? : Decidable² PathExists
+    PathExists? n₁ n₂
+        with allSimplePathsNoted ← paths-throughAll {n₁ = n₁} {n₂ = n₂} (proj₁ nodes)
+        with adj n₁ n₂
+    ...   | [] = no (λ p →  let w = toSimpleWalk p in ¬Any[] (allSimplePathsNoted w))
+    ...   | (p ∷ ps) = yes p
+
+    NoCycles : Set
+    NoCycles = ∀ {n} (p : Path n n) →  IsDone p
+
+    NoCycles? : Dec NoCycles
+    NoCycles? with any? (λ n → any? (Decidable-¬ IsDone?) (adj n n)) (proj₁ nodes)
+    ... | yes existsCycle =
+          no (λ ∀p,IsDonep →  let (n , n,n-cycle) = satisfied existsCycle in
+                              let (p , ¬IsDone-p) = satisfied n,n-cycle in
+                              ¬IsDone-p (∀p,IsDonep p))
+    ... | no noCycles =
+          yes (λ { done →  isDone
+                 ; p@(step {n₁ = n} _ _) →
+                    let w = toSimpleWalk p in
+                    let ¬IsDone-w = toSimpleWalk-IsDone⁻ p (λ {()}) in
+                    let w∈adj = paths-throughAll (proj₁ nodes) w in
+                    ⊥-elim (noCycles (lose (nodes-complete n) (lose w∈adj ¬IsDone-w)))
+                 })
+
+    NoCycles⇒adj-complete : NoCycles → ∀ {n₁ n₂} {p : Path n₁ n₂} →  p ∈ˡ adj n₁ n₂
+    NoCycles⇒adj-complete noCycles {n₁} {n₂} {p}
+        with findCycle p
+    ...   | inj₁ (w , w≡p) rewrite sym w≡p = paths-throughAll (proj₁ nodes) w
+    ...   | inj₂ (nᶜ , (wᶜ , wᶜ≢done)) = ⊥-elim (wᶜ≢done (noCycles (proj₁ wᶜ)))
+
+    Is-⊤ : Node → Set
+    Is-⊤ n = All (PathExists n) (proj₁ nodes)
+
+    Is-⊥ : Node → Set
+    Is-⊥ n = All (λ n' → PathExists n' n) (proj₁ nodes)
+
+    Has-⊤ : Set
+    Has-⊤ = Any Is-⊤ (proj₁ nodes)
+
+    Has-T? : Dec Has-⊤
+    Has-T? = findUniversal (proj₁ nodes) PathExists?
+
+    Has-⊥ : Set
+    Has-⊥ = Any Is-⊥ (proj₁ nodes)
+
+    Has-⊥? : Dec Has-⊥
+    Has-⊥? = findUniversal (proj₁ nodes) (λ n₁ n₂ → PathExists? n₂ n₁)

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

@@ -9,10 +9,10 @@ module Lattice.FiniteMap (A : Set) (B : Set)
     {_≈₂_ : B → B → Set}
     {_⊔₂_ : B → B → B} {_⊓₂_ : B → B → B}
     {{≡-Decidable-A : IsDecidable {_} {A} _≡_}}
-    {{lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_}} (dummy : ⊤) where
+    {{lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_}} (ks : List A) where
 
 open IsLattice lB using () renaming (_≼_ to _≼₂_)
-open import Lattice.Map A B dummy as Map
+open import Lattice.Map A B _ as Map
     using
         ( Map
         ; ⊔-equal-keys
@@ -74,7 +74,7 @@ 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
     FiniteMap = Σ Map (λ m → Map.keys m ≡ ks)
 
@@ -131,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
@@ -143,6 +143,7 @@ module WithKeys (ks : List A) where
             λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} →
                 IsEquivalence.≈-trans ≈ᵐ-equiv {m₁} {m₂} {m₃}
         }
+    open IsEquivalence ≈-equiv public
 
     instance
         isUnionSemilattice : IsSemilattice FiniteMap _≈_ _⊔_
@@ -183,7 +184,7 @@ module WithKeys (ks : List A) where
             ; isLattice = isLattice
             }
 
-    open IsLattice isLattice using (_≼_; ⊔-Monotonicˡ; ⊔-Monotonicʳ) public
+    open IsLattice isLattice using (_≼_; ⊔-idemp; ⊔-Monotonicˡ; ⊔-Monotonicʳ) public
 
     m₁≼m₂⇒m₁[k]≼m₂[k] : ∀ (fm₁ fm₂ : FiniteMap) {k : A} {v₁ v₂ : B} →
                         fm₁ ≼ fm₂ → (k , v₁) ∈ fm₁ → (k , v₂) ∈ fm₂ → v₁ ≼₂ v₂
@@ -253,9 +254,35 @@ 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₂))
 
-module IterProdIsomorphism where
+    _∈ᵐ_ : ∀ {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
@@ -267,7 +294,7 @@ module IterProdIsomorphism where
             ; ≈-equiv to ≈ᵘ-equiv
             ; fixedHeight to fixedHeightᵘ
             )
-    open import Lattice.IterProd B ⊤ dummy
+    open import Lattice.IterProd B ⊤ _
         as IP
         using (IterProd)
     open IsLattice lB using ()
@@ -296,20 +323,12 @@ module IterProdIsomorphism where
         in
             (((k , v) ∷ fm' , push k≢fm' ufm') , kvs≡ks)
 
+    _≈ⁱᵖ_ : ∀ {n : ℕ} → IterProd n → IterProd n → Set
+    _≈ⁱᵖ_ {n} = IP._≈_ {n}
 
-    private
-        _⊆ᵐ_ : ∀ {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
+    _⊔ⁱᵖ_ : ∀ {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))
@@ -368,26 +387,6 @@ module IterProdIsomorphism where
                                 fm'₂⊆fm'₁ k' v' k',v'∈fm'₂
                         in (v'' , (v'≈v'' , there k',v''∈fm'₁))
 
-    FromBothMaps : ∀ (k : A) (v : B) {ks : List A} (fm₁ fm₂ : FiniteMap ks) → Set
-    FromBothMaps k v fm₁ fm₂ =
-        Σ (B × B)
-          (λ (v₁ , v₂) → ( (v ≡ v₁ ⊔₂ v₂) × ((k , v₁) ∈ᵐ fm₁ × (k , v₂) ∈ᵐ fm₂)))
-
-    Provenance-union : ∀ {ks : List A} (fm₁ fm₂ : FiniteMap ks) {k : A} {v : B} →
-                       (k , v) ∈ᵐ (_⊔_ 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₁ ← (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)
@@ -613,7 +612,7 @@ module IterProdIsomorphism where
                         in
                             (v' , (v₁⊔v₂≈v' , there v'∈fm'))
 
-    module WithUniqueKeysAndFixedHeight {ks : List A} (uks : Unique ks) {{≈₂-Decidable : IsDecidable _≈₂_}} {h₂ : ℕ} {{fhB : FixedHeight₂ h₂}} where
+    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)
@@ -631,3 +630,6 @@ module IterProdIsomorphism where
         ⊥-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/Prod.agda

@@ -106,6 +106,8 @@ instance
         ; isLattice = isLattice
         }
 
+open IsLattice isLattice using (_≼_; _≺_; ≺-cong) public
+
 module _ {{≈₁-Decidable : IsDecidable _≈₁_}} {{≈₂-Decidable : IsDecidable _≈₂_}} where
     open IsDecidable ≈₁-Decidable using () renaming (R-dec to ≈₁-dec)
     open IsDecidable ≈₂-Decidable using () renaming (R-dec to ≈₂-dec)
@@ -125,7 +127,6 @@ module _ {{≈₁-Decidable : IsDecidable _≈₁_}} {{≈₂-Decidable : IsDeci
              {{fhA : FixedHeight₁ h₁}} {{fhB : FixedHeight₂ h₂}} where
 
         open import Data.Nat.Properties
-        open IsLattice isLattice using (_≼_; _≺_; ≺-cong)
 
         module ChainMapping₁ = ChainMapping joinSemilattice₁ isJoinSemilattice
         module ChainMapping₂ = ChainMapping joinSemilattice₂ isJoinSemilattice

Main.agda

@@ -1,11 +1,13 @@
 {-# OPTIONS --guardedness #-}
 module Main where
 
-open import Language
-open import Analysis.Sign
+open import Language hiding (_++_)
 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

@@ -1,19 +1,31 @@
 module Utils where
 
 open import Agda.Primitive using () renaming (_⊔_ to _⊔ℓ_)
-open import Data.Product as Prod using (_×_)
+open import Data.Product as Prod using (Σ; _×_; _,_; proj₁; proj₂)
 open import Data.Nat using (ℕ; suc)
+open import Data.Fin as Fin using (Fin; suc; zero)
+open import Data.Fin.Properties using (suc-injective)
 open import Data.List using (List; cartesianProduct; []; _∷_; _++_; foldr; filter) renaming (map to mapˡ)
-open import Data.List.Membership.Propositional using (_∈_)
+open import Data.List.Membership.Propositional using (_∈_; lose)
 open import Data.List.Membership.Propositional.Properties as ListMemProp using ()
-open import Data.List.Relation.Unary.All using (All; []; _∷_; map)
-open import Data.List.Relation.Unary.Any using (Any; here; there) -- TODO: re-export these with nicer names from map
+open import Data.List.Relation.Unary.All using (All; []; _∷_; map; all?; lookup)
+open import Data.List.Relation.Unary.All.Properties using (++⁻ˡ; ++⁻ʳ)
+open import Data.List.Relation.Unary.Any as Any using (Any; here; there; any?) -- TODO: re-export these with nicer names from map
 open import Data.Sum using (_⊎_)
 open import Function.Definitions using (Injective)
+open import Relation.Binary using (Antisymmetric) renaming (Decidable to Decidable²)
 open import Relation.Binary.PropositionalEquality using (_≡_; sym; refl; cong)
-open import Relation.Nullary using (¬_; yes; no)
+open import Relation.Nullary using (¬_; yes; no; Dec)
+open import Relation.Nullary.Decidable using (¬?)
 open import Relation.Unary using (Decidable)
 
+All¬-¬Any : ∀ {p c} {C : Set c} {P : C → Set p} {l : List C} → All (λ x → ¬ P x) l → ¬ Any P l
+All¬-¬Any {l = x ∷ xs} (¬Px ∷ _) (here Px) = ¬Px Px
+All¬-¬Any {l = x ∷ xs} (_ ∷ ¬Pxs) (there Pxs) = All¬-¬Any ¬Pxs Pxs
+
+Decidable-¬ : ∀ {p c} {C : Set c} {P : C → Set p} → Decidable P → Decidable (λ x → ¬ P x)
+Decidable-¬ Decidable-P x = ¬? (Decidable-P x)
+
 data Unique {c} {C : Set c} : List C → Set c where
     empty : Unique []
     push : ∀ {x : C} {xs : List C}
@@ -34,6 +46,24 @@ Unique-append {c} {C} {x} {x' ∷ xs'} x∉xs (push x'≢ uxs') =
         help {[]} _ = x'≢x ∷ []
         help {e ∷ es} (x'≢e ∷ x'≢es) = x'≢e ∷ help x'≢es
 
+Unique-++⁻ˡ : ∀ {c} {C : Set c} (xs : List C) {ys : List C} → Unique (xs ++ ys) → Unique xs
+Unique-++⁻ˡ [] Unique-ys = empty
+Unique-++⁻ˡ (x ∷ xs) {ys} (push x≢xs++ys Unique-xs++ys) = push (++⁻ˡ xs {ys = ys} x≢xs++ys) (Unique-++⁻ˡ xs Unique-xs++ys)
+
+Unique-++⁻ʳ : ∀ {c} {C : Set c} (xs : List C) {ys : List C} → Unique (xs ++ ys) → Unique ys
+Unique-++⁻ʳ [] Unique-ys = Unique-ys
+Unique-++⁻ʳ (x ∷ xs) {ys} (push x≢xs++ys Unique-xs++ys) = Unique-++⁻ʳ xs Unique-xs++ys
+
+Unique-∈-++ˡ : ∀ {c} {C : Set c} {x : C} (xs : List C) {ys : List C} →  Unique (xs ++ ys) → x ∈ xs → ¬ x ∈ ys
+Unique-∈-++ˡ [] _ ()
+Unique-∈-++ˡ {x = x} (x' ∷ xs) (push x≢xs++ys _) (here refl) = All¬-¬Any (++⁻ʳ xs x≢xs++ys)
+Unique-∈-++ˡ {x = x} (x' ∷ xs) (push _ Unique-xs++ys) (there x̷∈xs) = Unique-∈-++ˡ xs Unique-xs++ys x̷∈xs
+
+Unique-narrow : ∀ {c} {C : Set c} {x : C} (xs : List C) {ys : List C} →  Unique (xs ++ ys) → x ∈ xs →  Unique (x ∷ ys)
+Unique-narrow [] _ ()
+Unique-narrow {x = x} (x' ∷ xs) (push x≢xs++ys Unique-xs++ys) (here refl) = push (++⁻ʳ xs x≢xs++ys) (Unique-++⁻ʳ xs Unique-xs++ys)
+Unique-narrow {x = x} (x' ∷ xs) (push _ Unique-xs++ys) (there x̷∈xs) = Unique-narrow xs Unique-xs++ys x̷∈xs
+
 All-≢-map : ∀ {c d} {C : Set c} {D : Set d} (x : C) {xs : List C} (f : C → D) →
             Injective (_≡_ {_} {C}) (_≡_ {_} {D}) f →
             All (λ x' → ¬ x ≡ x') xs → All (λ y' → ¬ (f x) ≡ y') (mapˡ f xs)
@@ -46,9 +76,8 @@ Unique-map : ∀ {c d} {C : Set c} {D : Set d} {l : List C} (f : C → D) →
 Unique-map {l = []} _ _ _ = empty
 Unique-map {l = x ∷ xs} f f-Injecitve (push x≢xs uxs) = push (All-≢-map x f f-Injecitve x≢xs) (Unique-map f f-Injecitve uxs)
 
-All¬-¬Any : ∀ {p c} {C : Set c} {P : C → Set p} {l : List C} → All (λ x → ¬ P x) l → ¬ Any P l
-All¬-¬Any {l = x ∷ xs} (¬Px ∷ _) (here Px) = ¬Px Px
-All¬-¬Any {l = x ∷ xs} (_ ∷ ¬Pxs) (there Pxs) = All¬-¬Any ¬Pxs Pxs
+¬Any-map : ∀ {p₁ p₂ c} {C : Set c} {P₁ : C → Set p₁} {P₂ : C → Set p₂} {l : List C} → (∀ {x} → P₁ x → P₂ x) → ¬ Any P₂ l → ¬ Any P₁ l
+¬Any-map f ¬Any-P₂ Any-P₁ = ¬Any-P₂ (Any.map f Any-P₁)
 
 All-single : ∀ {p c} {C : Set c} {P : C → Set p} {c : C} {l : List C} → All P l → c ∈ l → P c
 All-single {c = c} {l = x ∷ xs} (p ∷ ps) (here refl) = p
@@ -106,3 +135,34 @@ _∧_ P Q a = P a × Q a
 
 it : ∀ {a} {A : Set a} {{_ : A}} → A
 it {{x}} = x
+
+z≢sf : ∀ {n : ℕ} (f : Fin n) → ¬ (Fin.zero ≡ Fin.suc f)
+z≢sf f ()
+
+z≢mapsfs : ∀ {n : ℕ} (fs : List (Fin n)) → All (λ sf → ¬ zero ≡ sf) (mapˡ suc fs)
+z≢mapsfs [] = []
+z≢mapsfs (f ∷ fs') = z≢sf f ∷ z≢mapsfs fs'
+
+fins : ∀ (n : ℕ) → Σ (List (Fin n)) Unique
+fins 0 = ([] , empty)
+fins (suc n') =
+    let
+        (inds' , unids') = fins n'
+    in
+        ( zero ∷ mapˡ suc inds'
+        , push (z≢mapsfs inds') (Unique-map suc suc-injective unids')
+        )
+
+fins-complete : ∀ (n : ℕ) (f : Fin n) → f ∈ (proj₁ (fins n))
+fins-complete (suc n') zero = here refl
+fins-complete (suc n') (suc f') = there (x∈xs⇒fx∈fxs suc (fins-complete n' f'))
+
+findUniversal : ∀ {p c} {C : Set c} {R : C → C → Set p} (l : List C) →  Decidable² R →
+                Dec (Any (λ x → All (R x) l) l)
+findUniversal l Rdec = any? (λ x → all? (Rdec x) l) l
+
+findUniversal-unique : ∀ {p c} {C : Set c} (R : C → C → Set p) (l : List C) →
+                       Antisymmetric _≡_ R →
+                       ∀ x₁ x₂ → x₁ ∈ l → x₂ ∈ l → All (R x₁) l → All (R x₂) l →
+                       x₁ ≡ x₂
+findUniversal-unique R l Rantisym x₁ x₂ x₁∈l x₂∈l Allx₁ Allx₂ = Rantisym (lookup Allx₁ x₂∈l) (lookup Allx₂ x₁∈l)