stdlib/graph.mlw

   1
   2 (** {1 Graph theory} *)
   3
   4 module Path
   5
   6   use list.List
   7   use list.Append
   8
   9   type vertex
  10
  11   predicate edge vertex vertex
  12
  13   inductive path vertex (list vertex) vertex =
  14   | Path_empty:
  15       forall x: vertex. path x Nil x
  16   | Path_cons:
  17       forall x y z: vertex, l: list vertex.
  18       edge x y -> path y l z -> path x (Cons x l) z
  19   (** `path v0 [v0; v1; ...; vn-1] vn`
  20      means a path from `v0` to `vn` composed of `n` edges `(vi,vi+1)`. *)
  21
  22   lemma path_right_extension:
  23     forall x y z: vertex, l: list vertex.
  24     path x l y -> edge y z -> path x (l ++ Cons y Nil) z
  25
  26   lemma path_right_inversion:
  27     forall x z: vertex, l: list vertex. path x l z ->
  28        (x = z /\ l = Nil)
  29     \/ (exists y: vertex, l': list vertex.
  30         path x l' y /\ edge y z /\ l = l' ++ Cons y Nil)
  31
  32   lemma path_trans:
  33     forall x y z: vertex, l1 l2: list vertex.
  34     path x l1 y -> path y l2 z -> path x (l1 ++ l2) z
  35
  36   lemma empty_path:
  37     forall x y: vertex. path x Nil y -> x = y
  38
  39   lemma path_decomposition:
  40     forall x y z: vertex, l1 l2: list vertex.
  41     path x (l1 ++ Cons y l2) z -> path x l1 y /\ path y (Cons y l2) z
  42
  43 end
  44
  45 module IntPathWeight
  46
  47   clone export Path
  48   use int.Int
  49   use list.List
  50   use list.Append
  51
  52   val function weight vertex vertex : int
  53
  54   function path_weight (l: list vertex) (dst: vertex) : int = match l with
  55     | Nil -> 0
  56     | Cons x Nil -> weight x dst
  57     | Cons x ((Cons y _) as r) -> weight x y + path_weight r dst
  58   end
  59   (** the total weight of a path `path _ l dst` *)
  60
  61   lemma path_weight_right_extension:
  62     forall x y: vertex, l: list vertex.
  63     path_weight (l ++ Cons x Nil) y = path_weight l x + weight x y
  64
  65   lemma path_weight_decomposition:
  66     forall y z: vertex, l1 l2: list vertex.
  67     path_weight (l1 ++ Cons y l2) z =
  68     path_weight l1 y + path_weight (Cons y l2) z
  69
  70 end
  71
  72 (***
  73 module SimplePath
  74
  75   use list.List
  76   use list.Mem
  77
  78   type graph
  79
  80   type vertex
  81
  82   predicate edge graph vertex vertex
  83
  84   (** `simple_path g src [x1;...;xn] dst` is a path
  85      src --> x1 --> x2 --> ... --> xn --> dst without repetition. *)
  86   inductive simple_path graph vertex (list vertex) vertex =
  87   | Path_empty :
  88       forall g:graph, v:vertex. simple_path g v (Nil : list vertex) v
  89   | Path_cons  :
  90       forall g:graph, src v dst : vertex, l : list vertex.
  91       edge g src v -> src <> v ->
  92       simple_path g v l dst -> not mem src l ->
  93       simple_path g src (Cons v l) dst
  94
  95   predicate simple_cycle (g : graph) (v : vertex) =
  96     exists l : list vertex. l <> Nil /\ simple_path g v l v
  97
  98 end
  99 *)