Iterative breadth search with queue (completeness)

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 iterative depth-first-search with a stack. The proof is quasi similar to random search.
This completeness proof is fully automatic.

module Dfs_stack2
  use import int.Int
  use import ref.Ref
  use import list.List
  use import list.Append
  use import list.Mem as L
  use import list.Elements as E
  use import queue.Queue
  use import list.NumOcc
  use import init_graph.GraphSetSucc

  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 push_set (q: Queue.t vertex) (s: set vertex) 
  variant { cardinal s } =
  ensures {union (elements (old q.elts)) s == elements q.elts }
  if not is_empty s then begin
    let x = choose s in
    Queue.push x q;
    push_set q (remove x s)
  end

let rec bfs r v
  variant {(cardinal vertices - cardinal v), L.length (r.elts)} = 
  requires {subset (elements r.elts) vertices }
  requires {subset v vertices }
  ensures {subset v result }
  ensures {subset result vertices }
  raises {Empty}
  ensures {subset v result}
  ensures {forall z y l. L.mem y (old r).elts -> whitepath y l z v -> mem z (diff result v)}

'L0:
   if Queue.is_empty r then v else
   let x = Queue.pop r in
'L1:
   if mem x v then bfs r v else begin
     push_set r (successors x);
     assert {forall z y l. L.mem y (at r 'L0).elts -> 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) } ;
     bfs r (add x v)
     end

let bfs_main (roots: Queue.t vertex) =
   requires {subset (elements (roots.elts)) vertices}
   raises {Empty}
   ensures {forall z y l. L.mem y (old roots).elts -> path y l z -> mem z result}
   bfs roots empty

end