From eb2d64f3b585991df9dff5989cfe582be0f48cdb Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Fri, 28 Nov 2025 21:31:54 -0800 Subject: [PATCH] Properly state all-paths property using simple walks Signed-off-by: Danila Fedorin --- Lattice/Builder.agda | 64 +++++++++++++++++++++++++++++++++++--------- 1 file changed, 51 insertions(+), 13 deletions(-) diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda index 6400dd5..33a0242 100644 --- a/Lattice/Builder.agda +++ b/Lattice/Builder.agda @@ -2,7 +2,7 @@ module Lattice.Builder where open import Lattice open import Equivalence -open import Utils using (fins; fins-complete) +open import Utils using (Unique; 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) @@ -10,9 +10,9 @@ 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 ∈ˡ-++⁺ʳ) +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) +open import Data.List.Relation.Unary.All using (All; []; _∷_; map; lookup) open import Data.List using (List; _∷_; []; cartesianProduct; cartesianProductWith; foldr) renaming (_++_ to _++ˡ_) open import Data.Sum using (_⊎_; inj₁; inj₂) open import Data.Product using (Σ; _,_; _×_; proj₁; proj₂) @@ -52,6 +52,13 @@ record Graph : Set where interior (step _ done) = [] interior (step {n₂ = n₂} _ p) = n₂ ∷ interior p + SimpleWalkVia : List Node → Node → Node → Set + SimpleWalkVia ns n₁ n₂ = Σ (Path n₁ n₂) (λ p → Unique (interior p) × All (λ n → n ∈ˡ ns) (interior p)) + + postulate 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) + + postulate findCycle : ∀ {n₁ n₂} (p : Path n₁ n₂) → (Σ (SimpleWalkVia (proj₁ nodes) n₁ n₂) λ w → proj₁ w ≡ p) ⊎ (Σ Node (λ n → Σ (SimpleWalkVia (proj₁ nodes) n n) λ w → ¬ proj₁ w ≡ done)) + Adjacency : Set Adjacency = ∀ (n₁ n₂ : Node) → List (Path n₁ n₂) @@ -61,8 +68,16 @@ record Graph : Set where ... | 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₂ + 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₂ @@ -70,9 +85,19 @@ record Graph : Set where ... | 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) @@ -80,16 +105,14 @@ record Graph : Set where ... | 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} e∈es⇒e∈edges (there n₁n₂∈es) - with n₁' ≟ n₁ | n₂' ≟ n₂ - ... | yes refl | yes refl = there (e∈seedWithEdges (λ e∈es → e∈es⇒e∈edges (there e∈es)) n₁n₂∈es) - ... | no _ | no _ = 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 + 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) @@ -99,6 +122,9 @@ 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₂ + 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¹ @@ -106,11 +132,23 @@ record Graph : Set where 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) + 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 (_≡ done) (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ᶜ)))