From 6f642d85e06d63a41183c63e96f4d730f4505743 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Fri, 28 Nov 2025 17:08:56 -0800 Subject: [PATCH] Put self-paths into the adjacency graph Signed-off-by: Danila Fedorin --- Lattice/Builder.agda | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda index 36db51e..16c57b8 100644 --- a/Lattice/Builder.agda +++ b/Lattice/Builder.agda @@ -65,10 +65,10 @@ record Graph : Set where 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₂ ((step n₁n₂∈edges done) ∷_)) (λ n₁ n₂ → []) (mapWith∈ˡ es (λ {e} e∈es → (e , e∈es⇒e∈edges e∈es))) + 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))) - e∈seedWithEdges : ∀ {n₁ n₂ es} → (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 n₁ n₂ + 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₂' @@ -82,8 +82,14 @@ record Graph : Set where ... | no _ | yes _ = e∈seedWithEdges (λ e∈es → e∈es⇒e∈edges (there e∈es)) n₁n₂∈es ... | yes refl | no _ = e∈seedWithEdges (λ e∈es → e∈es⇒e∈edges (there e∈es)) n₁n₂∈es + adj⁰ : Adjacency + adj⁰ n₁ n₂ + with n₁ ≟ n₂ + ... | yes refl = done ∷ [] + ... | no _ = [] + adj¹ : Adjacency - adj¹ = seedWithEdges edges (λ x → x) + adj¹ = seedWithEdges edges (λ x → x) 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)