why3doc index index

# 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

Generated by why3doc 0.88.3