why3/stdlib/graph.mlw at master · EasyCrypt/why3 · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99

(** {1 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

(***
module SimplePath

  use list.List
  use list.Mem

  type graph

  type vertex

  predicate edge graph vertex vertex

  (** `simple_path g src [x1;...;xn] dst` is a path
     src --> x1 --> x2 --> ... --> xn --> dst without repetition. *)
  inductive simple_path graph vertex (list vertex) vertex =
  | Path_empty :
      forall g:graph, v:vertex. simple_path g v (Nil : list vertex) v
  | Path_cons  :
      forall g:graph, src v dst : vertex, l : list vertex.
      edge g src v -> src <> v ->
      simple_path g v l dst -> not mem src l ->
      simple_path g src (Cons v l) dst

  predicate simple_cycle (g : graph) (v : vertex) =
    exists l : list vertex. l <> Nil /\ simple_path g v l v

end
*)