Random DFS in graph

The graph is represented by a pair (vertices, successor)

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


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 {whitepath_nodeflip roots visited result}
  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
        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};

        (*-------- whitepath_NODEFLIP -------------------------------------------*)
          (* case 1: x = z *)
            assert {mem x r'};
	  
	  (* case 2: whitepath x l z /\ x <> z *)
            (* using lemma whitepath_whitepath_fst_not_twice *)
            assert {forall l z. whitepath x l z visited -> x <> z -> 
              whiteaccess (successors x) z (add x visited) };
            assert {forall l z. whitepath x l z visited -> x <> z -> nodeflip z (add x visited) r'}; 
	  assert {forall l z. whitepath x l z visited -> nodeflip z visited r'};  
	  
	  (* case 3: whiteaccess roots' z visited *)
            (* case 3-1: not (whiteaccess roots' z r') *)
              assert {forall x' l z. whitepath x' l z visited -> not whitepath x' l z r' ->
                exists y. (L.mem y l \/ y = z) /\ nodeflip y visited r' }; 
              assert {forall x' l z. whitepath x' l z visited -> not whitepath x' l z r' ->
                exists y. (L.mem y l \/ y = z) /\ (y = x  \/ whiteaccess (successors x) y (add x visited)) };
              assert {forall y. whiteaccess (successors x) y (add x visited) ->
                exists l'. whitepath x l' y visited }; 
              assert {forall x' l z. whitepath x' l z visited -> not whitepath x' l z r' ->
                exists y l'. (L.mem y l \/ y = z) /\ whitepath x l' y visited };
              assert {forall x' l z. whitepath x' l z visited -> not whitepath x' l z r' ->
                exists l'. whitepath x l' z visited }; 
              (* goto cases 1-2 *)
              assert {forall x' l z. whitepath x' l z visited -> not whitepath x' l z r' ->
                 nodeflip z visited r }; 
            (* case 3-2: whiteaccess roots' z r' *)
              assert {forall x' l z. mem x' roots' -> whitepath x' l z r' ->
                 nodeflip z visited r};  
	r


let dfs_main (roots: set vertex) : set vertex =
   requires {subset roots vertices}
   dfs roots empty

end

Generated by why3doc 0.86.1