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
*)
|
