(** {1 Random DFS in graph}
The graph is represented by a pair ([vertices], [successor])
{h
-
vertices
: this constant is the set of graph vertices
-
successor
: this function gives for each vertex the set of vertices directly joinable from it
The algorithm is depth-first-search in the graph. It picks randomly the son on which recursive call is done.
The proof is mutually recursive on pre and post conditions. Fully automatic proof.
}
*)
module DfsRandomSearch
use import int.Int
use import list.List
use import list.Append
use import list.Mem as L
use import list.Elements as E
use import init_graph.GraphSetSucc
lemma mem_decidable:
forall x: 'a, l: list 'a. L.mem x l \/ not L.mem x l
lemma list_suffix_fst_not_twice:
forall x, l "induction" : list vertex. L.mem x l -> exists l1 l2. l = l1 ++ (Cons x l2) /\ not L.mem x l2
predicate white_vertex (x: vertex) (v: set vertex) =
not (mem x v)
predicate nodeflip (x: vertex) (v1 v2: set vertex) =
white_vertex x v1 /\ not (white_vertex x v2)
predicate whitepath (x: vertex) (l: list vertex) (z: vertex) (v: set vertex) =
path x l z /\ (forall y. L.mem y l -> white_vertex y v) /\ white_vertex z v
predicate whitereachable (x z: vertex) (v: set vertex) =
exists l. whitepath x l z v
predicate whitereached (x: vertex) (s: set vertex) (v: set vertex) =
forall z. mem z s -> exists l. whitepath x l z v
predicate whiteaccessfrom (r: set vertex) (z: vertex) (v: set vertex) =
exists x. mem x r /\ whitereachable x z v
predicate whiteaccess (r s: set vertex) (v: set vertex) =
forall z. mem z s -> exists x. mem x r /\ whitereachable x z v
predicate path_fst_not_twice (x: vertex) (l: list vertex) (z: vertex) =
path x l z /\
match l with
| Nil -> true
| Cons _ l' -> x <> z /\ not (L.mem x l')
end
lemma path_suffix_fst_not_twice:
forall x z l "induction". path x l z ->
exists l1 l2. l = l1 ++ l2 /\ path_fst_not_twice x l2 z
lemma path_path_fst_not_twice:
forall x z l. path x l z ->
exists l'. path_fst_not_twice x l' z /\ subset (E.elements l') (E.elements l)
predicate whitepath_fst_not_twice (x: vertex) (l: list vertex) (z: vertex) (v: set vertex) =
whitepath x l z v /\ path_fst_not_twice x l z
lemma whitepath_decomposition:
forall x l1 l2 z y v. whitepath x (l1 ++ (Cons y l2)) z v -> whitepath x l1 y v /\ whitepath y (Cons y l2) z v
lemma whitepath_mem_decomposition_r:
forall x l z y v. whitepath x l z v -> (L.mem y l \/ y = z) -> exists l': list vertex. whitepath y l' z v
lemma whitepath_whitepath_fst_not_twice:
forall x z l v. whitepath x l z v -> exists l'. whitepath_fst_not_twice x l' z v
lemma path_cons_inversion:
forall x z l. path x (Cons x l) z -> exists y. edge x y /\ path y l z
lemma whitepath_cons_inversion:
forall x z l v. whitepath x (Cons x l) z v -> exists y. edge x y /\ whitepath y l z v
lemma whitepath_cons_fst_not_twice_inversion:
forall x z l v. whitepath_fst_not_twice x (Cons x l) z v -> x <> z ->
(exists y. edge x y /\ whitepath y l z (add x v))
lemma whitepath_fst_not_twice_inversion :
forall x z l v. whitepath_fst_not_twice x l z v -> x <> z ->
(exists y l'. edge x y /\ whitepath y l' z (add x v))
lemma whitepath_trans:
forall x l1 y l2 z v. whitepath x l1 y v -> whitepath y l2 z v -> whitepath x (l1 ++ l2) z v
lemma whitepath_Y:
forall x l z y x' l' v. whitepath x l z v -> (L.mem y l \/ y = z) -> whitepath x' l' y v -> exists l0. whitepath x' l0 z v
lemma abc :
forall z x:'a, r v. mem z (diff r v) -> z = x \/ mem z (diff r (add x v))
lemma abcd :
forall z:'a, r1 r2 r3. mem z (diff r1 r3) -> mem z (diff r1 r2) \/ mem z (diff r2 r3)
lemma whitereachable1 :
forall x y l z v. whitepath y l z (add x v) -> whitepath y l z v
lemma whitereachable2 :
forall x y l z v. not (mem x v) -> whitepath y l z v -> edge x y -> whitepath x (Cons x l) z v
(** {3 program} *)
let rec dfs (roots: set vertex) (visited: set vertex): set vertex
variant {(cardinal vertices - cardinal visited), (cardinal roots)} =
requires {subset roots vertices }
requires {subset visited vertices }
ensures {subset visited result}
ensures {subset result vertices}
ensures {forall z. mem z (diff result visited) -> exists x l. mem x roots /\ whitepath x l z visited}
ensures {forall x l z. mem x roots -> whitepath x l z visited -> mem z result }
if is_empty roots then visited
else
let x = choose roots in
let roots' = remove x roots in
if mem x visited then
dfs roots' visited
else
let r' = dfs (successors x) (add x visited) in
let r = dfs roots' r' in
(*-------- nodeflip_whitepath ----------------------------*)
assert {forall z. mem z (diff r visited) -> mem z (diff r' visited) \/ mem z (diff r r')};
(*-------- case 1 ----------*)
assert {forall z. mem z (diff r' visited) -> z = x \/ mem z (diff r' (add x visited)) };
(* case 1-1: nodeflip z visited r' /\ z = x *)
assert {forall z. z = x -> whitepath x Nil z visited};
(* case 1-2: nodeflip z visited r' /\ z <> x *)
assert {forall z. mem z (diff r' (add x visited)) ->
(exists y l. mem y roots' /\ whitepath y l z (add x visited))
\/
(exists y l. edge x y /\ whitepath y l z (add x visited)) };
(*-------- case 2 ------------*)
assert {forall z. mem z (diff r r') -> exists y l. mem y roots' /\ whitepath y l z r'};
assert {forall z y l. whitepath y l z r' -> whitepath y l z (add x visited)};
(*-------- whitepath_nodeflip -------------------------------------------*)
(* case 1: whiteaccessfrom roots' z r' *)
assert {forall y l z. mem y roots' -> whitepath y l z r' -> mem z r };
(* case 2: not (whiteaccessfrom roots' z r') *)
assert {forall y l z. whitepath y l z visited -> not whitepath y l z r' ->
exists y'. (L.mem y' l \/ y' = z) /\ mem y' (diff r' visited) };
assert {forall y l z. whitepath y l z visited -> not whitepath y l z r' ->
exists y'. (L.mem y' l \/ y' = z) /\
(y' = x \/ whiteaccessfrom (successors x) y' (add x visited)) };
(**) assert {forall y'. whiteaccessfrom (successors x) y' (add x visited) ->
exists l'. whitepath x l' y' visited };
assert {forall y l z. whitepath y l z visited -> not whitepath y l z r' ->
exists y' l'. (L.mem y' l \/ y' = z) /\ whitepath x l' y' visited };
assert {forall y l z. whitepath y l z visited -> not whitepath y l z r' ->
exists l'. whitepath x l' z visited };
(* case 3-1: whitepath x l z /\ z = x *)
assert {mem x r'};
(* case 3-2: whitepath x l z /\ z <> x *)
(* using lemma whitepath_whitepath_fst_not_twice *)
assert {forall l z. z <> x -> whitepath x l z visited
-> exists x' l'. edge x x' /\ whitepath x' l' z (add x visited) };
r
let dfs_main (roots: set vertex) : set vertex =
requires {subset roots vertices}
dfs roots empty
end