why3doc index index
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
module GraphSetSuccPath
Properties of paths (aka Why3 path library)
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
module GraphSetSuccPathColored
Properties of colored paths
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.2