DFS in graph - completeness of the whitepath theorem

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

This algorithm is depth-first-search in the graph. It picks randomly the son on which recursive call is done.
This theorem refers to the White-path theorem in book by Cormen et al.
The new visited vertices are exactly the ones reachable from roots by a white path w.r.t the previously visited set.
Automatic proof, with inductive definition of white paths and heavy use of the "by" connective.

Notice that this proof relies on the non-black-to-white property for its completeness.
The set of visited vertices is splitted into gray and black sets.
The result differs from previous dfs versions since only black visited set is returned.
Thus, this proof is slightly more complex than with a sole set of visited vertices.

The formula "A && B" means "A /\ A -> B" .
The formula "A by B" means "B /\ B -> A"

module DFSWhitePathGrayCompleteness
  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


predicate white_vertex (x: vertex) (v: set vertex) =
    not (mem x v)
 
  inductive wpath vertex (list vertex) vertex (set vertex) =
  | WPath_empty:
      forall x v. white_vertex x v -> wpath x Nil x v
  | WPath_cons:
      forall x y l z v.
      white_vertex x v -> edge x y -> wpath y l z v -> wpath x (Cons x l) z v

  predicate whiteaccess (r s v: set vertex) =
    forall z. mem z s -> exists x l. mem x r /\ wpath x l z v

  predicate nbtw (b g: set vertex) =
    forall x x'. edge x x' -> mem x b -> mem x' (union b g)

  lemma whiteaccess_var:
    forall r r' s v. subset r r' -> whiteaccess r s v -> whiteaccess r' s v

  lemma whiteaccess_diff:
    forall r s v. whiteaccess r s v -> whiteaccess (diff r v) s v

  lemma nbtw_path:
    forall r v. nbtw (diff r v) v -> 
      forall x l z. mem x (diff r v) -> wpath x l z v -> mem z (diff r v)

  lemma nbtw_whiteaccess:
    forall r s v. nbtw (diff r v) v -> whiteaccess r s v -> subset s (diff r v)

  lemma diff_empty:
    forall b g r: set vertex. inter r g == empty -> diff r (union b g) == diff r b

   lemma whiteaccess_roots_result: 
   forall r r' s v b g. v = union b g -> subset (diff r g) r' -> whiteaccess r s v
     -> whiteaccess (diff r' v) s v
     by whiteaccess r' s v
     by whiteaccess (diff r g) s v
     by whiteaccess (diff r v) s v

	  
let rec dfs r g b 
  variant {(cardinal vertices - cardinal g), (cardinal r)} =
  requires {subset r vertices }
  requires {subset b vertices }
  requires {subset g vertices }
  requires {inter b g == empty}
  ensures {subset result vertices }
  ensures {subset b result }
  ensures {inter result g == empty}
  ensures {subset (diff r g) result &&
           nbtw (diff result (union b g)) (union b g) &&
           forall s. whiteaccess r s (union b g) -> subset s (diff result b) }
  if is_empty r then b else
  let x = choose r in
  let r' = remove x r in
  let v = union b g in
  if mem x v then dfs r' g b else
  let v' = dfs (successors x) (add x g) b in
  assert {diff (add x v') b == add x (diff v' b) };
  let v'' = dfs r' g (add x v') in
  assert {diff v'' b == union (diff v'' (add x v')) (diff (add x v') b) };
  v''

end