Random search in graph

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

• 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 a ministep of a random search in the graph. It is generic to any search strategy.
This completeness proof is adapted from Dowek and Munoz and is fully automatic.

module RandomSearch
  use import int.Int
  use import list.List
  use import list.Append
  use import list.Mem as L
  use import init_graph.GraphSetSucc
  use import list.NumOcc

  lemma path_lst_occ:
    forall x y z l. L.mem x l -> path y l z ->
      exists l1 l2. l = l1 ++ Cons x l2 /\ path x (Cons x l2) z /\ not L.mem x l2

  lemma path_inv:
    forall x z l. path x (Cons x l) z -> exists x'. edge x x' /\ path x' l z 

  predicate white_vertex (x: vertex) (v: set vertex) =
    not (mem x v)

  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

  lemma whitepath_suffix:
    forall x y z v l1 l2. whitepath y (l1 ++ Cons x l2) z v -> whitepath x (Cons x l2) z v

  lemma whitepath_inv:
    forall x z l v. whitepath x (Cons x l) z v -> not L.mem x l -> z <> x -> exists x'. edge x x' /\ whitepath x' l z (add x v)

  lemma whitepath_split_lst_occ:
    forall x y l z v. L.mem x l -> whitepath y l z v -> z <> x ->
      exists x' l'. edge x x' /\ whitepath x' l' z (add x v)

let rec random_search r v = 
  requires {subset r vertices }
  requires {subset v vertices }
  ensures {subset v result}
  ensures {forall z y l. mem y r -> whitepath y l z v -> mem z (diff result v)}

  if is_empty r then v else
  let x = choose r in
  let r' = remove x r in
  if mem x v then random_search r' v else
  let v' = random_search (union r' (successors x)) (add x v) in
   assert {forall z y l. mem y r -> whitepath y l z v -> z <> x ->
      whitepath y l z (add x v) \/
      exists x' l'. edge x x' /\ whitepath x' l' z (add x v) } ;
   v'
      

let random_search_main (roots: set vertex) =
  requires {subset roots vertices}
  ensures {forall z y l. mem y roots -> path y l z -> mem z result}
  random_search roots empty 

end