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.
The 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 list.Elements as E
  use import init_graph.GraphSetSucc
  use import init_graph.GraphSetSuccPath

  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 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 ++ (Cons z Nil)) -> 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 abc :
    forall z x:'a, r v. mem z (diff r v) -> z = x \/ mem z (diff r  (add x v))

  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

(*  lemma assert_proof :
    forall x v r roots'. mem x vertices -> not (mem x v) -> 
    whiteaccess (union roots' (successors x)) (diff r (add x v)) (add x v) ->
    whiteaccess (add x roots') (diff r v) v
*)

let rec random_search roots visited
  variant {(cardinal vertices - cardinal visited), (cardinal roots)} = 
  requires {subset roots vertices }
  requires {subset visited vertices }
  ensures {subset visited result}
  ensures {forall z. mem z (diff result visited) -> exists x l. mem x roots /\ whitepath x l z visited }

  if is_empty roots then
     visited
  else
    let x = choose roots in
    let roots' = remove x roots in
     if mem x visited then
       random_search roots' visited
     else
       let r = random_search (union roots' (successors x)) (add x visited) in
       (*----------- nodeflip_whitepath -----------*)
       (* case 1: nodeflip z visited r /\ z = x *)
          assert {forall z. z = x -> whitepath x Nil z visited};
       (* case 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)) };
       r

end