GraphSetSucc

 module GraphSetSucc

A 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

  use export set.Fset

  type vertex

  constant vertices: set vertex

  function successors vertex : set vertex

  axiom successors_vertices:
    forall x. mem x vertices -> subset (successors x) vertices

  predicate edge (x y: vertex) = mem x vertices /\ mem y (successors x)

  clone export graph.Path with type vertex = vertex, predicate edge = edge

end

GraphSetSuccPath

module GraphSetSuccPath

Properties of paths (aka Why3 path library)

• automatic proofs
• only path_vertex_last_occ proved in Coq

  use import int.Int
  use import list.List
  use import list.Mem as L
  use import list.Append
  use import list.NumOcc
  use import GraphSetSucc

  predicate path_fst_not_twice (x: vertex) (l: list vertex) (z: vertex) =
    path x (Cons x l) z /\ (not L.mem x l)

  lemma mem_decidable:
    forall x: 'a, lv: list 'a. L.mem x lv \/ not L.mem x lv

  predicate spl (lv: list 'a) = forall x. L.mem x lv -> num_occ x lv = 1

  lemma spl_single:
    forall x: 'a. spl (Cons x Nil)

  lemma spl_expansion:
    forall x: 'a, lv: list 'a. spl lv -> not (L.mem x lv) -> spl (lv ++ (Cons x Nil))

  lemma spl_sub:
    forall lv lv1 lv2: list 'a. lv = lv1 ++ lv2 -> spl lv -> spl lv1 /\ spl lv2

  lemma numocc_nonneg:
    forall x: 'a, lv "induction": list 'a.  0 <= NumOcc.num_occ x lv

  lemma path_edge:
    forall x z. path x (Cons x Nil) z -> edge x z

  lemma path_hd:
    forall x y z l. path x (Cons y l) z -> x = y

  lemma path_vertex_l :
    forall x y z l. path x l z -> L.mem y l -> mem y vertices

  lemma path_vertex_r :
    forall x z l. path x l z -> l <> Nil -> mem z vertices

  lemma path_vertex_last_occ :
    forall x y z l. path x l z -> L.mem y l ->
    (exists l1 l2. l = l1 ++ (Cons y l2) /\ (path_fst_not_twice y l2 z))
end

GraphSetSuccPathColored

module GraphSetSuccPathColored

Properties of colored paths

• automatic proofs
• whitepath_whitepostfix, path_vertex_last_occ proved in Coq

  use import map.Map
  use import list.List
  use import list.Mem as L
  use import list.Append
  use import GraphSetSucc
  use import GraphSetSuccPath

  type color = WHITE | GRAY | BLACK

  predicate whitepath (x: vertex) (l: list vertex) (z: vertex) (c: map vertex color) =
    path x l z /\ c[x] = WHITE /\ c[z] = WHITE /\ (forall y. L.mem y l -> c[y] = WHITE)

  predicate node_flip (x: vertex) (c1 c2: map vertex color) =
    c1[x] = WHITE /\ c2[x] <> WHITE

  predicate whitepath_flip (x: vertex) (l: list vertex) (z: vertex) (c1 c2: map vertex color) =
    whitepath x l z c1 /\ not whitepath x l z c2

  lemma whitepath_trans:
    forall x y z l1 l2 c. whitepath x l1 y c -> whitepath y l2 z c -> whitepath x (l1 ++ l2) z c

  lemma whitepath_mem_decomp:
    forall x y z l1 l2 c. whitepath x (l1 ++ (Cons y l2)) z c -> whitepath x l1 y c /\ whitepath y (Cons y l2) z c

  lemma whitepath_mem_decomp_right:
    forall x y z l c. whitepath x l z c -> L.mem y (l ++ (Cons z Nil)) -> exists l'. whitepath y l' z c

  lemma whitepath_vertex_l:
    forall x y z l c. whitepath x l z c -> L.mem y l -> mem y vertices

  lemma whitepath_vertex_r:
    forall x z l c. whitepath x l z c -> l <> Nil -> mem z vertices

  lemma whitepathflip_contains_node_flip:
    forall x z l c1 c2. whitepath_flip x l z c1 c2 -> exists y. L.mem y (l ++ (Cons z Nil)) /\ node_flip y c1 c2

  lemma whitepathflip_contains_node_flip_whitepath:
    forall x z l c1 c2. whitepath_flip x l z c1 c2 -> exists y l'. L.mem y (l ++ (Cons z Nil)) /\ node_flip y c1 c2 /\ whitepath y l' z c1

  lemma whitepath_whitepostfix :
    forall x z l c. whitepath x l z c -> x <> z -> (exists y l'. edge x y /\ whitepath y l' z (set c x GRAY))

end