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

Switch to a path definition that allows trivial self-loops

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

18
Lattice/Builder.agda
View File

@ -40,16 +40,12 @@ record Graph : Set where
edges : List Edge
data Path : Node → Node → Set where
last : ∀ {n₁ n₂ : Node} → (n₁ , n₂) ∈ˡ edges → Path n₁ n₂
done : ∀ {n : Node} → 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')
done ++ p = p
(step e p₁) ++ p₂ = step e (p₁ ++ p₂)
Adjacency : Set
Adjacency = ∀ (n₁ n₂ : Node) → List (Path n₁ n₂)
@ -70,9 +66,9 @@ record Graph : Set where
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)))
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)))
e∈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₂
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 {es = []} e∈es⇒e∈edges ()
e∈seedWithEdges {es = (n₁' , n₂') ∷ es} e∈es⇒e∈edges (here refl)
with n₁' ≟ n₁' | n₂' ≟ n₂'
@ -89,7 +85,7 @@ record Graph : Set where
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¹ : ∀ {n₁ n₂} (n₁n₂∈edges : (n₁ , n₂) ∈ˡ edges) → (step n₁n₂∈edges done) ∈ˡ adj¹ n₁ n₂
edge∈adj¹ = e∈seedWithEdges (λ x → x)
throughAll : List Node → Adjacency
@ -106,4 +102,4 @@ record Graph : Set where
adj = throughAll (proj₁ nodes)
NoCycles : Set
NoCycles = ∀ (n : Node) → adj n n ≡ []
NoCycles = ∀ (n : Node) → All (_≡ done) (adj n n)