Graph theory

module Path

  use list.List
  use list.Append

  type vertex

  predicate edge vertex vertex

  inductive path vertex (list vertex) vertex =
  | Path_empty:
      forall x: vertex. path x Nil x
  | Path_cons:
      forall x y z: vertex, l: list vertex.
      edge x y -> path y l z -> path x (Cons x l) z

path v0 [v0; v1; ...; vn-1] vn means a path from v0 to vn composed of n edges (vi,vi+1).

  lemma path_right_extension:
    forall x y z: vertex, l: list vertex.
    path x l y -> edge y z -> path x (l ++ Cons y Nil) z

  lemma path_right_inversion:
    forall x z: vertex, l: list vertex. path x l z ->
       (x = z /\ l = Nil)
    \/ (exists y: vertex, l': list vertex.
        path x l' y /\ edge y z /\ l = l' ++ Cons y Nil)

  lemma path_trans:
    forall x y z: vertex, l1 l2: list vertex.
    path x l1 y -> path y l2 z -> path x (l1 ++ l2) z

  lemma empty_path:
    forall x y: vertex. path x Nil y -> x = y

  lemma path_decomposition:
    forall x y z: vertex, l1 l2: list vertex.
    path x (l1 ++ Cons y l2) z -> path x l1 y /\ path y (Cons y l2) z

end

module IntPathWeight

  clone export Path
  use int.Int
  use list.List
  use list.Append

  val function weight vertex vertex : int

  function path_weight (l: list vertex) (dst: vertex) : int = match l with
    | Nil -> 0
    | Cons x Nil -> weight x dst
    | Cons x ((Cons y _) as r) -> weight x y + path_weight r dst
  end

the total weight of a path path _ l dst

  lemma path_weight_right_extension:
    forall x y: vertex, l: list vertex.
    path_weight (l ++ Cons x Nil) y = path_weight l x + weight x y

  lemma path_weight_decomposition:
    forall y z: vertex, l1 l2: list vertex.
    path_weight (l1 ++ Cons y l2) z =
    path_weight l1 y + path_weight (Cons y l2) z

end