Random search in graph

{c vertices} Proof adapted from Dowek and Munoz

  • graph represented by pair vertices, successor:
          [vertices] constant: set of graph vertices
          [successor] function: for each vertex x, this function gives the set or vertices directly joinable from x
  • fully automatic proof

    
    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
    
      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
        
     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
    
      predicate nodeflip_whitepath (roots v1 v2: set vertex) =
        forall z. nodeflip z v1 v2 -> exists x l. mem x roots /\ whitepath x l 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 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))
    
      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
              (* using lemma whitepath_whitepath_fst_not_twice *)
    
         	  let r = random_search (union roots' (successors x)) (add x visited) in
    	  (*-------------- whitepath_nodeflip -------------*)
    	  (* case 1: whitepath x l z /\ x = z *)
                (* assert {mem x r}; *)
    	  
    	  (* case 2: whitepath x l z /\ x <> z *)
                (* assert {forall l z. whitepath x l z visited -> x <> z 
                   -> exists y l'. edge x y /\ whitepath y 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 /\ mem x l *)
                  (* assert {forall x' l z. mem x' roots' -> whitepath x' l z visited -> L.mem x (l ++ Cons z Nil) 
                     -> exists l'. whitepath x l' z visited}; *)
                  (* goto cases 1-2 *)
                (* case 3-2: whitepath roots' l z /\ not mem x l *)
                  assert {forall x' l z. mem x' roots' -> whitepath x' l z visited -> not L.mem x (l ++ Cons z Nil) 
                     -> whitepath x' l z (add x visited)};  
    
              (*----------- nodeflip_whitepath -----------*)
              assert {forall z. nodeflip z visited r -> nodeflip z (add x visited) r \/ z = x};  
    
              (* case 1: nodeflip z visited r /\ z = x *)
                assert {whitepath x Nil x visited};  
              (* case 2: nodeflip z visited r /\ z <> x *)
                assert {forall x' l z. edge x x' -> whitepath x' l z (add x visited) -> 
                    whitepath x (Cons x l) z visited};  
              r
          end
    
    let random_search_main (roots: set vertex) =
       requires {subset roots vertices}
       random_search roots (empty) 
    
    end
    

  • Generated by why3doc 0.86.1