agda-spa/Lattice/Builder.agda

module Lattice.Builder where

open import Lattice
open import Equivalence
open import Utils using (Unique; push; empty; Unique-append; Unique-++⁻ˡ; Unique-++⁻ʳ; All¬-¬Any; ¬Any-map; fins; fins-complete)
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 () 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)
open import Data.List.Relation.Unary.All using (All; []; _∷_; map; lookup; zipWith; tabulate)
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 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})

    _++_ : ∀ {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 ++ˡ interior p'))
    splitFromInterior done ()
    splitFromInterior (step _ done) ()
    splitFromInterior (step {n₂ = n'} n₁,n'∈edges p'@(step _ _)) (here refl) = (p' , ((λ {()}) , (n' ∷ [] , 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)))


    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₂'))
            in findCycleHelp p p₁' p₂' ¬IsDone-p₁' (subst Unique (sym intp₁'≡intp₁++[nⁱ]) (Unique-append nⁱ∉intp₁ Unique-intp₁)) p≡p₁'++p₂'
    ...   | yes nⁱ∈intp₁
            with (pᶜ , (¬IsDone-pᶜ , (ns , intp₁≡ns++intpᶜ))) ← splitFromInterior p₁ nⁱ∈intp₁ =
            let Unique-intp₁' = subst Unique intp₁≡ns++intpᶜ Unique-intp₁
            in inj₂ (nⁱ , ((pᶜ , (Unique-++⁻ʳ ns  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

    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)

    NoCycles : Set
    NoCycles = ∀ (n : Node) →  All IsDone (adj n n)

    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 (lookup (noCycles nᶜ) (paths-throughAll (proj₁ nodes) wᶜ)))