From e409cceae52f2dfbc78257b648fdfabd2aa60c02 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Fri, 28 Nov 2025 16:24:48 -0800
Subject: [PATCH] Start on an initial implementation of DAG-based builder

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Lattice/Builder.agda | 87 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 87 insertions(+)

diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda
index 5e8e250..a637609 100644
--- a/Lattice/Builder.agda
+++ b/Lattice/Builder.agda
@@ -20,3 +20,90 @@ 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 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
+        last : ∀ {n₁ n₂ : Node} →  (n₁ , n₂) ∈ˡ edges →  Path n₁ n₂
+        step : ∀ {n₁ n₂ n₃ : Node} →  (n₁ , n₂) ∈ˡ edges → Path n₂ n₃ → Path n₁ n₃
+
+    interior : ∀ {n₁ n₂} → Path n₁ n₂ → List Node
+    interior (last _) = []
+    interior (step {n₂ = n₂} _ p) = n₂ ∷ interior p
+
+    _++_ : ∀ {n₁ n₂ n₃} → Path n₁ n₂ → Path n₂ n₃ → Path n₁ n₃
+    last e ++ p = step e p
+    step e p ++ p' = step e (p ++ p')
+
+    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₂'
+
+    Adjacency-merge : Adjacency → Adjacency → Adjacency
+    Adjacency-merge adj₁ adj₂ n₁ n₂ = adj₁ n₁ n₂ ++ˡ adj₂ n₁ n₂
+
+    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₂
+
+    seedWithEdges : ∀ (es : List Edge) →  (∀ {e} → e ∈ˡ es → e ∈ˡ edges) → Adjacency
+    seedWithEdges es e∈es⇒e∈edges = foldr (λ ((n₁ , n₂) , n₁n₂∈edges) → Adjacency-update n₁ n₂ ((last n₁n₂∈edges) ∷_)) (λ n₁ n₂ → []) (mapWith∈ˡ es (λ {e} e∈es →  (e , e∈es⇒e∈edges e∈es)))
+
+    edge∈seedWithEdges : ∀ {n₁ n₂ es} → (e∈es⇒e∈edges : ∀ {e} → e ∈ˡ es → e ∈ˡ edges) → ∀ (n₁n₂∈es : (n₁ , n₂) ∈ˡ es) →  (last (e∈es⇒e∈edges n₁n₂∈es)) ∈ˡ seedWithEdges es e∈es⇒e∈edges n₁ n₂
+    edge∈seedWithEdges {es = []} e∈es⇒e∈edges ()
+    edge∈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)
+    edge∈seedWithEdges {n₁} {n₂} {es = (n₁' , n₂') ∷ es} e∈es⇒e∈edges (there n₁n₂∈es)
+        with n₁' ≟ n₁ | n₂' ≟ n₂
+    ...   | yes refl | yes refl = there (edge∈seedWithEdges (λ e∈es → e∈es⇒e∈edges (there e∈es)) n₁n₂∈es)
+    ...   | no _ | no _ = edge∈seedWithEdges (λ e∈es → e∈es⇒e∈edges (there e∈es)) n₁n₂∈es
+    ...   | no _ | yes _ = edge∈seedWithEdges (λ e∈es → e∈es⇒e∈edges (there e∈es)) n₁n₂∈es
+    ...   | yes refl | no _ = edge∈seedWithEdges (λ e∈es → e∈es⇒e∈edges (there e∈es)) n₁n₂∈es
+
+    adj¹ : Adjacency
+    adj¹ = seedWithEdges edges (λ x → x)
+
+    edge∈adj¹ : ∀ {n₁ n₂} (n₁n₂∈edges : (n₁ , n₂) ∈ˡ edges) →  (last n₁n₂∈edges) ∈ˡ adj¹ n₁ n₂
+    edge∈adj¹ = edge∈seedWithEdges (λ x → x)
+
+    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} (p : Path n₁ n₂) (ns : List Node) → All (λ n →  n ∈ˡ ns) (interior p) →  p ∈ˡ throughAll ns n₁ n₂
+    -- paths-throughAll (last n₁n₂∈edges) ns _ = throughAll-adj₁ ns (edge∈adj¹ n₁n₂∈edges)
+
+    adj : Adjacency
+    adj = throughAll (proj₁ nodes)
+
+    NoCycles : Set
+    NoCycles = ∀ (n : Node) → adj n n ≡ []