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 white_monotony (v1 v2: set vertex) =
    forall x: vertex. white_vertex x v2 -> white_vertex x v1

  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

  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_mem_decomp: 
    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_decomp_right: 
    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 why_type_decidable:
    forall x y: 'a. x = y \/ x <> y
    
  lemma Lmem_decidable:
    forall x:vertex, l. L.mem x l \/ not (L.mem x l)

  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)

  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_not_nil_inversion:
    forall x z l. path x (Cons x l) z -> exists y. edge x y /\ path y l z

  lemma whitepath_not_nil_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_not_nil_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_inversion : 
    forall x z l v. whitepath x l z v -> x <> z -> 
    (exists y: vertex, l': list vertex. 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 nodeflip_monotony :
    forall x v0 v1 v2. subset v0 v1 -> nodeflip x v1 v2 -> nodeflip x v0 v2

  lemma whitepath_monotony :
    forall x l z v0 v1. subset v0 v1 -> whitepath x l z v1 -> whitepath x l z v0

let rec random_search (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 {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
      	 random_search roots' visited
      else begin
     	  let r = random_search (union roots' (successors x)) (add x visited) in
          (*----------- nodeflip_whitepath -----------*)
          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 roots' z (add x visited) 
                     \/ 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};

	  (*-------------- whitepath_nodeflip -------------*)

	  (* case 1: whitepath x l z visited /\ 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 
               -> exists x' l'. edge x x' /\ whitepath x' l' z (add x visited)};  
               (* same as lemma whitepath_inversion *)
            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: whitepath roots' l z *)
            (* case 3-1: whitepath roots' l z /\ L.mem x l *)
              assert {forall y l z. whitepath y l z visited -> (L.mem x l \/ x = z)
                 -> exists l'. whitepath x l' z visited};
              (* goto cases 1-2 *)
            (* case 3-2: whitepath roots' l z /\ not (L.mem x l) *)
              assert {forall y l z. mem y roots' -> whitepath y l z visited -> not (L.mem x l \/ x = z)
                 -> whitepath y l z (add x visited)};  
          r
      end

let random_search_main (roots: set vertex) =
   requires {subset roots vertices}
   random_search roots (empty) 

end