Walks in undirected graphs

Content created by Egbert Rijke, Fredrik Bakke and Jonathan Prieto-Cubides.

Created on 2022-08-07.
Last modified on 2024-10-16.

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.action-on-identifications-functions
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.function-types
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.torsorial-type-families
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-torsorial-Id 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-coproduct
      ( compute-vertex-on-walk-Undirected-Graph w)
      ( equiv-is-contr
        ( is-torsorial-Id (other-element-unordered-pair p y))
        ( is-contr-unit))) ∘e
    ( left-distributive-Σ-coproduct
      ( 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-coproduct
      ( compute-edge-on-walk-Undirected-Graph w)
      ( equiv-is-contr
        ( is-torsorial-Id (pair p e))
        ( is-contr-unit))) ∘e
    ( left-distributive-Σ-coproduct
      ( 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-coproduct 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-torsorial-constant-walk-Undirected-Graph :
    is-torsorial constant-walk-Undirected-Graph
  pr1 (pr1 is-torsorial-constant-walk-Undirected-Graph) = x
  pr2 (pr1 is-torsorial-constant-walk-Undirected-Graph) =
    refl-constant-walk-Undirected-Graph
  pr2 is-torsorial-constant-walk-Undirected-Graph
    (v , refl-walk-Undirected-Graph , refl) =
    refl
  pr2 is-torsorial-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-torsorial-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)

Recent changes