Properly state all-paths property using simple walks
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
14214ab5e7
commit
eb2d64f3b5
@ -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ᶜ)))
|
||||
|
||||
Loading…
Reference in New Issue
Block a user