mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
100 lines
2.5 KiB
Plaintext
100 lines
2.5 KiB
Plaintext
|
|
(** {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
|
|
*)
|