Walks in undirected graphs
module graph-theory.walks-undirected-graphs where
Imports
open import elementary-number-theory.equality-natural-numbers open import elementary-number-theory.natural-numbers open import foundation.contractible-types open import foundation.coproduct-types open import foundation.decidable-types open import foundation.dependent-pair-types open import foundation.empty-types open import foundation.equivalences open import foundation.functions open import foundation.functoriality-coproduct-types open import foundation.fundamental-theorem-of-identity-types open import foundation.identity-types open import foundation.propositions open import foundation.type-arithmetic-coproduct-types open import foundation.unit-type open import foundation.universe-levels open import foundation.unordered-pairs open import graph-theory.undirected-graphs open import univalent-combinatorics.standard-finite-types
Idea
A walk in an undirected graph consists of a list of edges that connect the starting point with the end point. Walks may repeat edges and pass through the same vertex multiple times.
Definitions
Walks in undirected graphs
module _ {l1 l2 : Level} (G : Undirected-Graph l1 l2) where data walk-Undirected-Graph (x : vertex-Undirected-Graph G) : vertex-Undirected-Graph G → UU (l1 ⊔ l2 ⊔ lsuc lzero) where refl-walk-Undirected-Graph : walk-Undirected-Graph x x cons-walk-Undirected-Graph : (p : unordered-pair (vertex-Undirected-Graph G)) → (e : edge-Undirected-Graph G p) → {y : type-unordered-pair p} → walk-Undirected-Graph x (element-unordered-pair p y) → walk-Undirected-Graph x (other-element-unordered-pair p y)
The vertices on a walk
module _ {l1 l2 : Level} (G : Undirected-Graph l1 l2) {x : vertex-Undirected-Graph G} where is-vertex-on-walk-Undirected-Graph : {y : vertex-Undirected-Graph G} (w : walk-Undirected-Graph G x y) → vertex-Undirected-Graph G → UU l1 is-vertex-on-walk-Undirected-Graph refl-walk-Undirected-Graph v = x ＝ v is-vertex-on-walk-Undirected-Graph (cons-walk-Undirected-Graph p e {y} w) v = ( is-vertex-on-walk-Undirected-Graph w v) + ( other-element-unordered-pair p y ＝ v) vertex-on-walk-Undirected-Graph : {y : vertex-Undirected-Graph G} (w : walk-Undirected-Graph G x y) → UU l1 vertex-on-walk-Undirected-Graph w = Σ (vertex-Undirected-Graph G) (is-vertex-on-walk-Undirected-Graph w) vertex-vertex-on-walk-Undirected-Graph : {y : vertex-Undirected-Graph G} (w : walk-Undirected-Graph G x y) → vertex-on-walk-Undirected-Graph w → vertex-Undirected-Graph G vertex-vertex-on-walk-Undirected-Graph w = pr1
Edges on a walk
module _ {l1 l2 : Level} (G : Undirected-Graph l1 l2) {x : vertex-Undirected-Graph G} where is-edge-on-walk-Undirected-Graph' : {y : vertex-Undirected-Graph G} (w : walk-Undirected-Graph G x y) → total-edge-Undirected-Graph G → UU (lsuc lzero ⊔ l1 ⊔ l2) is-edge-on-walk-Undirected-Graph' refl-walk-Undirected-Graph e = raise-empty (lsuc lzero ⊔ l1 ⊔ l2) is-edge-on-walk-Undirected-Graph' (cons-walk-Undirected-Graph q f w) e = ( is-edge-on-walk-Undirected-Graph' w e) + ( pair q f ＝ e) is-edge-on-walk-Undirected-Graph : {y : vertex-Undirected-Graph G} (w : walk-Undirected-Graph G x y) → (p : unordered-pair-vertices-Undirected-Graph G) → edge-Undirected-Graph G p → UU (lsuc lzero ⊔ l1 ⊔ l2) is-edge-on-walk-Undirected-Graph w p e = is-edge-on-walk-Undirected-Graph' w (pair p e) edge-on-walk-Undirected-Graph : {y : vertex-Undirected-Graph G} (w : walk-Undirected-Graph G x y) → UU (lsuc lzero ⊔ l1 ⊔ l2) edge-on-walk-Undirected-Graph w = Σ ( total-edge-Undirected-Graph G) ( λ e → is-edge-on-walk-Undirected-Graph' w e) edge-edge-on-walk-Undirected-Graph : {y : vertex-Undirected-Graph G} (w : walk-Undirected-Graph G x y) → edge-on-walk-Undirected-Graph w → total-edge-Undirected-Graph G edge-edge-on-walk-Undirected-Graph w = pr1
Concatenating walks
module _ {l1 l2 : Level} (G : Undirected-Graph l1 l2) {x : vertex-Undirected-Graph G} where concat-walk-Undirected-Graph : {y z : vertex-Undirected-Graph G} → walk-Undirected-Graph G x y → walk-Undirected-Graph G y z → walk-Undirected-Graph G x z concat-walk-Undirected-Graph w refl-walk-Undirected-Graph = w concat-walk-Undirected-Graph w (cons-walk-Undirected-Graph p e v) = cons-walk-Undirected-Graph p e (concat-walk-Undirected-Graph w v)
The length of a walk
module _ {l1 l2 : Level} (G : Undirected-Graph l1 l2) {x : vertex-Undirected-Graph G} where length-walk-Undirected-Graph : {y : vertex-Undirected-Graph G} → walk-Undirected-Graph G x y → ℕ length-walk-Undirected-Graph refl-walk-Undirected-Graph = 0 length-walk-Undirected-Graph (cons-walk-Undirected-Graph p e w) = succ-ℕ (length-walk-Undirected-Graph w)
Properties
The type of vertices on the constant walk is contractible
module _ {l1 l2 : Level} (G : Undirected-Graph l1 l2) (x : vertex-Undirected-Graph G) where is-contr-vertex-on-walk-refl-walk-Undirected-Graph : is-contr ( vertex-on-walk-Undirected-Graph G (refl-walk-Undirected-Graph {x = x})) is-contr-vertex-on-walk-refl-walk-Undirected-Graph = is-contr-total-path x
The type of vertices on a walk is equivalent to Fin (n + 1) where n is the length of the walk
module _ {l1 l2 : Level} (G : Undirected-Graph l1 l2) {x : vertex-Undirected-Graph G} where compute-vertex-on-walk-Undirected-Graph : {y : vertex-Undirected-Graph G} (w : walk-Undirected-Graph G x y) → vertex-on-walk-Undirected-Graph G w ≃ Fin (succ-ℕ (length-walk-Undirected-Graph G w)) compute-vertex-on-walk-Undirected-Graph refl-walk-Undirected-Graph = equiv-is-contr ( is-contr-vertex-on-walk-refl-walk-Undirected-Graph G x) ( is-contr-Fin-one-ℕ) compute-vertex-on-walk-Undirected-Graph ( cons-walk-Undirected-Graph p e {y} w) = ( equiv-coprod ( compute-vertex-on-walk-Undirected-Graph w) ( equiv-is-contr ( is-contr-total-path (other-element-unordered-pair p y)) ( is-contr-unit))) ∘e ( left-distributive-Σ-coprod ( vertex-Undirected-Graph G) ( is-vertex-on-walk-Undirected-Graph G w) ( λ z → other-element-unordered-pair p y ＝ z))
The type of edges on a constant walk is empty
module _ {l1 l2 : Level} (G : Undirected-Graph l1 l2) (x : vertex-Undirected-Graph G) where is-empty-edge-on-walk-refl-walk-Undirected-Graph : is-empty ( edge-on-walk-Undirected-Graph G (refl-walk-Undirected-Graph {x = x})) is-empty-edge-on-walk-refl-walk-Undirected-Graph = is-empty-raise-empty ∘ pr2
The type of edges on a walk is equivalent to Fin n where n is the length of the walk
module _ {l1 l2 : Level} (G : Undirected-Graph l1 l2) {x : vertex-Undirected-Graph G} where compute-edge-on-walk-Undirected-Graph : {y : vertex-Undirected-Graph G} (w : walk-Undirected-Graph G x y) → edge-on-walk-Undirected-Graph G w ≃ Fin (length-walk-Undirected-Graph G w) compute-edge-on-walk-Undirected-Graph refl-walk-Undirected-Graph = equiv-is-empty ( is-empty-edge-on-walk-refl-walk-Undirected-Graph G x) ( id) compute-edge-on-walk-Undirected-Graph (cons-walk-Undirected-Graph p e w) = ( equiv-coprod ( compute-edge-on-walk-Undirected-Graph w) ( equiv-is-contr ( is-contr-total-path (pair p e)) ( is-contr-unit))) ∘e ( left-distributive-Σ-coprod ( total-edge-Undirected-Graph G) ( is-edge-on-walk-Undirected-Graph' G w) ( λ z → pair p e ＝ z))
Right unit law for concatenation of walks
module _ {l1 l2 : Level} (G : Undirected-Graph l1 l2) {x : vertex-Undirected-Graph G} where right-unit-law-concat-walk-Undirected-Graph : {y : vertex-Undirected-Graph G} (w : walk-Undirected-Graph G x y) → (concat-walk-Undirected-Graph G w refl-walk-Undirected-Graph) ＝ w right-unit-law-concat-walk-Undirected-Graph refl-walk-Undirected-Graph = refl right-unit-law-concat-walk-Undirected-Graph ( cons-walk-Undirected-Graph p e w) = ap ( cons-walk-Undirected-Graph p e) ( right-unit-law-concat-walk-Undirected-Graph w)
For any walk w from x to y and any vertex v on w, we can decompose w into a walk w1 from x to v and a walk w2 from v to y
module _ {l1 l2 : Level} (G : Undirected-Graph l1 l2) {x : vertex-Undirected-Graph G} where first-segment-walk-Undirected-Graph : {y : vertex-Undirected-Graph G} (w : walk-Undirected-Graph G x y) (v : vertex-on-walk-Undirected-Graph G w) → walk-Undirected-Graph G x (vertex-vertex-on-walk-Undirected-Graph G w v) first-segment-walk-Undirected-Graph refl-walk-Undirected-Graph (v , refl) = refl-walk-Undirected-Graph first-segment-walk-Undirected-Graph (cons-walk-Undirected-Graph p e w) (v , inl x) = first-segment-walk-Undirected-Graph w (pair v x) first-segment-walk-Undirected-Graph ( cons-walk-Undirected-Graph p e w) ( .(other-element-unordered-pair p _) , inr refl) = cons-walk-Undirected-Graph p e w second-segment-walk-Undirected-Graph : {y : vertex-Undirected-Graph G} (w : walk-Undirected-Graph G x y) (v : vertex-on-walk-Undirected-Graph G w) → walk-Undirected-Graph G (vertex-vertex-on-walk-Undirected-Graph G w v) y second-segment-walk-Undirected-Graph refl-walk-Undirected-Graph (v , refl) = refl-walk-Undirected-Graph second-segment-walk-Undirected-Graph (cons-walk-Undirected-Graph p e w) (v , inl H) = cons-walk-Undirected-Graph p e ( second-segment-walk-Undirected-Graph w (pair v H)) second-segment-walk-Undirected-Graph ( cons-walk-Undirected-Graph p e w) ( .(other-element-unordered-pair p _) , inr refl) = refl-walk-Undirected-Graph eq-decompose-walk-Undirected-Graph : {y : vertex-Undirected-Graph G} (w : walk-Undirected-Graph G x y) (v : vertex-on-walk-Undirected-Graph G w) → ( concat-walk-Undirected-Graph G ( first-segment-walk-Undirected-Graph w v) ( second-segment-walk-Undirected-Graph w v)) ＝ w eq-decompose-walk-Undirected-Graph refl-walk-Undirected-Graph (v , refl) = refl eq-decompose-walk-Undirected-Graph ( cons-walk-Undirected-Graph p e w) (v , inl H) = ap ( cons-walk-Undirected-Graph p e) ( eq-decompose-walk-Undirected-Graph w (pair v H)) eq-decompose-walk-Undirected-Graph ( cons-walk-Undirected-Graph p e w) ( .(other-element-unordered-pair p _) , inr refl) = right-unit-law-concat-walk-Undirected-Graph G ( cons-walk-Undirected-Graph p e w)
For any edge e on p, if v is a vertex on w then it is a vertex on cons p e w
is-vertex-on-walk-cons-walk-Undirected-Graph : {l1 l2 : Level} (G : Undirected-Graph l1 l2) (p : unordered-pair-vertices-Undirected-Graph G) (e : edge-Undirected-Graph G p) → {x : vertex-Undirected-Graph G} {y : type-unordered-pair p} → (w : walk-Undirected-Graph G x (element-unordered-pair p y)) → {v : vertex-Undirected-Graph G} → is-vertex-on-walk-Undirected-Graph G w v → is-vertex-on-walk-Undirected-Graph G (cons-walk-Undirected-Graph p e w) v is-vertex-on-walk-cons-walk-Undirected-Graph G p e w = inl
For any decomposition of a walk w into w1 followed by w2, any vertex on w is a vertex on w1 or on w2
module _ {l1 l2 : Level} (G : Undirected-Graph l1 l2) {x : vertex-Undirected-Graph G} where is-vertex-on-first-segment-walk-Undirected-Graph : {y : vertex-Undirected-Graph G} (w : walk-Undirected-Graph G x y) → (v : vertex-on-walk-Undirected-Graph G w) → vertex-Undirected-Graph G → UU l1 is-vertex-on-first-segment-walk-Undirected-Graph w v = is-vertex-on-walk-Undirected-Graph G ( first-segment-walk-Undirected-Graph G w v) is-vertex-on-second-segment-walk-Undirected-Graph : {y : vertex-Undirected-Graph G} (w : walk-Undirected-Graph G x y) → (v : vertex-on-walk-Undirected-Graph G w) → vertex-Undirected-Graph G → UU l1 is-vertex-on-second-segment-walk-Undirected-Graph w v = is-vertex-on-walk-Undirected-Graph G ( second-segment-walk-Undirected-Graph G w v) is-vertex-on-first-or-second-segment-walk-Undirected-Graph : {y : vertex-Undirected-Graph G} (w : walk-Undirected-Graph G x y) → (u v : vertex-on-walk-Undirected-Graph G w) → ( is-vertex-on-first-segment-walk-Undirected-Graph w u ( vertex-vertex-on-walk-Undirected-Graph G w v)) + ( is-vertex-on-second-segment-walk-Undirected-Graph w u ( vertex-vertex-on-walk-Undirected-Graph G w v)) is-vertex-on-first-or-second-segment-walk-Undirected-Graph refl-walk-Undirected-Graph (u , refl) (.u , refl) = inl refl is-vertex-on-first-or-second-segment-walk-Undirected-Graph ( cons-walk-Undirected-Graph p e w) (u , inl H) (v , inl K) = map-coprod id ( is-vertex-on-walk-cons-walk-Undirected-Graph G p e ( second-segment-walk-Undirected-Graph G w (u , H))) ( is-vertex-on-first-or-second-segment-walk-Undirected-Graph w ( pair u H) ( pair v K)) is-vertex-on-first-or-second-segment-walk-Undirected-Graph ( cons-walk-Undirected-Graph p e w) ( u , inl H) ( .(other-element-unordered-pair p _) , inr refl) = inr (inr refl) is-vertex-on-first-or-second-segment-walk-Undirected-Graph ( cons-walk-Undirected-Graph p e w) ( .(other-element-unordered-pair p _) , inr refl) ( v , inl x) = inl (is-vertex-on-walk-cons-walk-Undirected-Graph G p e w x) is-vertex-on-first-or-second-segment-walk-Undirected-Graph ( cons-walk-Undirected-Graph p e w) ( .(other-element-unordered-pair p _) , inr refl) ( .(other-element-unordered-pair p _) , inr refl) = inl (inr refl)
For any decomposition of a walk w into w1 followed by w2, any vertex on w1 is a vertex on w
is-vertex-on-walk-is-vertex-on-first-segment-walk-Undirected-Graph : {l1 l2 : Level} (G : Undirected-Graph l1 l2) {x y : vertex-Undirected-Graph G} (w : walk-Undirected-Graph G x y) (v : vertex-on-walk-Undirected-Graph G w) (u : vertex-Undirected-Graph G) → is-vertex-on-first-segment-walk-Undirected-Graph G w v u → is-vertex-on-walk-Undirected-Graph G w u is-vertex-on-walk-is-vertex-on-first-segment-walk-Undirected-Graph G refl-walk-Undirected-Graph (v , refl) .(vertex-vertex-on-walk-Undirected-Graph G refl-walk-Undirected-Graph (v , refl)) refl = refl is-vertex-on-walk-is-vertex-on-first-segment-walk-Undirected-Graph G ( cons-walk-Undirected-Graph p e w) (v , inl K) u H = inl ( is-vertex-on-walk-is-vertex-on-first-segment-walk-Undirected-Graph G w (pair v K) u H) is-vertex-on-walk-is-vertex-on-first-segment-walk-Undirected-Graph G ( cons-walk-Undirected-Graph p e w) (.(other-element-unordered-pair p _) , inr refl) u H = H
For any decomposition of a walk w into w1 followed by w2, any vertex on w2 is a vertex on w
is-vertex-on-walk-is-vertex-on-second-segment-walk-Undirected-Graph : {l1 l2 : Level} (G : Undirected-Graph l1 l2) {x y : vertex-Undirected-Graph G} (w : walk-Undirected-Graph G x y) (v : vertex-on-walk-Undirected-Graph G w) (u : vertex-Undirected-Graph G) → is-vertex-on-second-segment-walk-Undirected-Graph G w v u → is-vertex-on-walk-Undirected-Graph G w u is-vertex-on-walk-is-vertex-on-second-segment-walk-Undirected-Graph G refl-walk-Undirected-Graph (v , refl) .v refl = refl is-vertex-on-walk-is-vertex-on-second-segment-walk-Undirected-Graph G (cons-walk-Undirected-Graph p e w) (v , inl K) u (inl H) = is-vertex-on-walk-cons-walk-Undirected-Graph G p e w ( is-vertex-on-walk-is-vertex-on-second-segment-walk-Undirected-Graph G w (pair v K) u H) is-vertex-on-walk-is-vertex-on-second-segment-walk-Undirected-Graph G ( cons-walk-Undirected-Graph p e w) ( v , inl K) .(other-element-unordered-pair p _) ( inr refl) = inr refl is-vertex-on-walk-is-vertex-on-second-segment-walk-Undirected-Graph G ( cons-walk-Undirected-Graph p e w) ( .(other-element-unordered-pair p _) , inr refl) .(other-element-unordered-pair p _) ( refl) = inr refl
Constant walks are identifications
module _ {l1 l2 : Level} (G : Undirected-Graph l1 l2) {x : vertex-Undirected-Graph G} where is-constant-walk-Undirected-Graph-Prop : {y : vertex-Undirected-Graph G} → walk-Undirected-Graph G x y → Prop lzero is-constant-walk-Undirected-Graph-Prop w = is-zero-ℕ-Prop (length-walk-Undirected-Graph G w) is-constant-walk-Undirected-Graph : {y : vertex-Undirected-Graph G} → walk-Undirected-Graph G x y → UU lzero is-constant-walk-Undirected-Graph w = type-Prop (is-constant-walk-Undirected-Graph-Prop w) constant-walk-Undirected-Graph : (y : vertex-Undirected-Graph G) → UU (lsuc lzero ⊔ l1 ⊔ l2) constant-walk-Undirected-Graph y = Σ (walk-Undirected-Graph G x y) is-constant-walk-Undirected-Graph is-decidable-is-constant-walk-Undirected-Graph : {y : vertex-Undirected-Graph G} (w : walk-Undirected-Graph G x y) → is-decidable (is-constant-walk-Undirected-Graph w) is-decidable-is-constant-walk-Undirected-Graph w = is-decidable-is-zero-ℕ (length-walk-Undirected-Graph G w) refl-constant-walk-Undirected-Graph : constant-walk-Undirected-Graph x pr1 refl-constant-walk-Undirected-Graph = refl-walk-Undirected-Graph pr2 refl-constant-walk-Undirected-Graph = refl is-contr-total-constant-walk-Undirected-Graph : is-contr (Σ (vertex-Undirected-Graph G) constant-walk-Undirected-Graph) pr1 (pr1 is-contr-total-constant-walk-Undirected-Graph) = x pr2 (pr1 is-contr-total-constant-walk-Undirected-Graph) = refl-constant-walk-Undirected-Graph pr2 is-contr-total-constant-walk-Undirected-Graph (v , refl-walk-Undirected-Graph , refl) = refl pr2 is-contr-total-constant-walk-Undirected-Graph (.(other-element-unordered-pair p _) , cons-walk-Undirected-Graph p e w , ()) constant-walk-eq-Undirected-Graph : (y : vertex-Undirected-Graph G) → x ＝ y → constant-walk-Undirected-Graph y constant-walk-eq-Undirected-Graph y refl = refl-constant-walk-Undirected-Graph is-equiv-constant-walk-eq-Undirected-Graph : (y : vertex-Undirected-Graph G) → is-equiv (constant-walk-eq-Undirected-Graph y) is-equiv-constant-walk-eq-Undirected-Graph = fundamental-theorem-id ( is-contr-total-constant-walk-Undirected-Graph) ( constant-walk-eq-Undirected-Graph) equiv-constant-walk-eq-Undirected-Graph : (y : vertex-Undirected-Graph G) → (x ＝ y) ≃ constant-walk-Undirected-Graph y pr1 (equiv-constant-walk-eq-Undirected-Graph y) = constant-walk-eq-Undirected-Graph y pr2 (equiv-constant-walk-eq-Undirected-Graph y) = is-equiv-constant-walk-eq-Undirected-Graph y eq-constant-walk-Undirected-Graph : {y : vertex-Undirected-Graph G} → constant-walk-Undirected-Graph y → x ＝ y eq-constant-walk-Undirected-Graph {y} = map-inv-is-equiv (is-equiv-constant-walk-eq-Undirected-Graph y)