(** {1 Random DFS in graph} The graph is represented by a pair ([vertices], [successor]) {h 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 whiteaccess (r: set vertex) (z: vertex) (v: set vertex) = exists x l. mem x r /\ whitepath x l 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)) predicate nodeflip_whitepath (roots v1 v2: set vertex) = forall z. nodeflip z v1 v2 -> whiteaccess roots z v1 predicate whitepath_nodeflip (roots v1 v2: set vertex) = forall x l z. mem x roots -> whitepath x l z v1 -> nodeflip z v1 v2 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 (** {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 {nodeflip_whitepath roots visited 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 begin let r' = dfs (successors x) (add x visited) in let r = dfs roots' r' in (*-------- nodeflip_whitepath ----------------------------*) assert {forall z. nodeflip z visited r -> nodeflip z visited r' \/ nodeflip z r' r}; (*-------- case 1 ----------*) assert {forall z. nodeflip z visited r' -> z = x \/ nodeflip z (add x visited) r' }; (* case 1-1: nodeflip z visited r' /\ z = x *) assert {whitepath x Nil x visited}; (* case 1-2: nodeflip z visited r' /\ z <> x *) assert {forall z. nodeflip z (add x visited) r' -> whiteaccess (successors x) z (add x visited)}; assert {forall x' l z. whitepath x' l z (add x visited) -> whitepath x' l z visited}; assert {forall z x' l. edge x x' -> whitepath x' l z visited -> whitepath x (Cons x l) z visited}; assert {forall z. nodeflip z (add x visited) r' -> whiteaccess roots z visited}; (*-------- case 2 ------------*) assert {forall z. nodeflip z r' r -> whiteaccess roots' z r'}; assert {forall z x' l. whitepath x' l z r' -> whitepath x' l z visited}; r end let dfs_main (roots: set vertex) : set vertex = requires {subset roots vertices} dfs roots empty end