Library UniMath.Combinatorics.GraphPaths

Author: Floris van Doorn, december 2017
  • paths in a graph (called gpaths to disambiguate from the identity type)
  • operations on paths
In this file we consider graphs with a type of vertices and a type of edges between any pair of vertices. We could restrict to sets, but there is no reason to do that here.

Definition issymmetric {V : UU} (E : V V UU) : UU :=
  u v, E u v E v u.

Definition gpaths_of_length {V : UU} (E : V V UU) (v w : V) (n : nat) : UU.
  revert v. induction n as [|n IH].
  - intro v. exact (v = w).
  - intro v. exact (u, E v u × IH u).

Definition gpaths {V : UU} (E : V V UU) (v w : V) : UU :=
  n, gpaths_of_length E v w n.

Definition nil {V : UU} {E : V V UU} (v : V) : gpaths E v v :=
  (0,, idpath v).

Definition cons {V : UU} {E : V V UU} {w u v : V} (e : E u v) (p : gpaths E v w) : gpaths E u w :=
  (S (pr1 p),, (v,, (e,, pr2 p))).

Local Notation "[]" := (nil _) (at level 0, format "[]").
Local Infix "::" := cons.

Lemma gpaths_ind {V : UU} {E : V V UU} {w : V} (P : {u}, gpaths E u w UU)
      (H1 : P []) (H2 : {u v} (e : E u v) (p : gpaths E v w), P p P (e :: p))
      {u : V} (p : gpaths E u w) : P p.
  induction p as [n p]. revert u p. induction n as [|n IH].
  - induction p. exact H1.
  - induction p as [v x]. induction x as [e p]. apply (H2 _ _ _ (n,, p)).
    apply IH.

Definition foldr {V : UU} {E : V V UU} {w : V} {B : V UU} (f : {u v}, E u v B v B u)
           (b : B w) : ∏{u : V}, gpaths E u w B u.
Proof. apply gpaths_ind. exact b. exact (λ u v e _ b, f u v e b). Defined.

Definition concat {V : UU} {E : V V UU} {u v w : V} (p : gpaths E u v) (q : gpaths E v w) :
  gpaths E u w :=
  foldr (λ _ _ , cons) q p.

Local Infix "++" := concat.

Definition append {V : UU} {E : V V UU} {u v w : V} (p : gpaths E u v) (e : E v w) :
  gpaths E u w :=
  p ++ e::[].

Definition reverse {V : UU} {E : V V UU} (H : issymmetric E) {u v : V} (p : gpaths E u v) :
  gpaths E v u.
  revert u p. apply gpaths_ind.
  - exact [].
  - intros u u' e p q. exact (append q (invmap (H u' u) e)).

Definition symmetric_closure {V : UU} (E : V V UU) (u v : V) : UU :=
E u v ⨿ E v u.

Definition issymmetric_symmetric_closure {V : UU} (E : V V UU) :
  issymmetric (symmetric_closure E) :=
  λ u v, weqcoprodcomm (E u v) (E v u).

Definition reverse_in_closure {V : UU} {E : V V UU} {u v : V}
           (p : gpaths (symmetric_closure E) u v) : gpaths (symmetric_closure E) v u :=
  reverse (issymmetric_symmetric_closure E) p.