DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Put self-paths into the adjacency graph

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2025-11-28 17:08:56 -08:00
parent 25fa0140f0
commit 6f642d85e0
1 changed files with 10 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
Lattice/Builder.agda
View File

@ -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 {n₁ n₂ p} → p ∈ˡ adj n₁ n₂ → p ∈ˡ (through n adj) n₁ n₂
through-monotonic adj n p∈adjn₁n₂ = ∈ˡ-++⁺ʳ _ p∈adjn₁n₂ through-monotonic adj n p∈adjn₁n₂ = ∈ˡ-++⁺ʳ _ p∈adjn₁n₂
seedWithEdges : ∀ (es : List Edge) → (∀ {e} → e ∈ˡ es → e ∈ˡ edges) → Adjacency seedWithEdges : ∀ (es : List Edge) → (∀ {e} → e ∈ˡ es → e ∈ˡ edges) → Adjacency → 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 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 = []} e∈es⇒e∈edges ()
e∈seedWithEdges {es = (n₁' , n₂') ∷ es} e∈es⇒e∈edges (here refl) e∈seedWithEdges {es = (n₁' , n₂') ∷ es} e∈es⇒e∈edges (here refl)
with n₁' ≟ n₁' | n₂' ≟ n₂' 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 ... | 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 ... | 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¹ : 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¹ : ∀ {n₁ n₂} (n₁n₂∈edges : (n₁ , n₂) ∈ˡ edges) → (step n₁n₂∈edges done) ∈ˡ adj¹ n₁ n₂
edge∈adj¹ = e∈seedWithEdges (λ x → x) edge∈adj¹ = e∈seedWithEdges (λ x → x)