Library Constructive_DigraphInterface

Require Import FMaps.
Require Import Directed_edges.
Require Import FMapAVL.
Require Import MapFacts.
Require Import DigraphInterface.
Require Import Labels.

Module Type Constructive_Directed_Graph (Vertex : OrderedType) (Lab : Labels)
                                                                     <: Directed_Graph Vertex Lab.

Import Lab.

Module VertexMap := FMapAVL.Make Vertex.
Module Export VMapFacts := MyMapFacts VertexMap.
Module Import Edge := Directed_Edge Vertex.
Module EdgeMap := FMapAVL.Make Edge.
Module Import EMapFacts := MyMapFacts EdgeMap.

Parameter t : Type.
Parameter V : t -> VertexMap.t (option NodeLabel).
Parameter vertex_label : Vertex.t -> t -> option (option NodeLabel).
Parameter E : t -> EdgeMap.t (option EdgeLabel).
Parameter edge_label : Edge.t -> t -> option (option EdgeLabel).
Parameter successors : Vertex.t -> t -> VertexMap.t (option EdgeLabel).
Parameter predecessors : Vertex.t -> t -> VertexMap.t (option EdgeLabel).
Parameter link : t -> Vertex.t -> Vertex.t -> option (option EdgeLabel).

Parameter vertex_label_spec : forall v g,
vertex_label v g = VertexMap.find v (V g).

Parameter edge_label_spec : forall e g,
edge_label e g = EdgeMap.find e (E g).

Parameter In_graph_vertex : Vertex.t -> t -> Prop.
Parameter In_graph_labeled_vertex : Vertex.t -> t -> option NodeLabel -> Prop.
Parameter In_graph_edge : Edge.t -> t -> Prop.
Parameter In_graph_labeled_edge : Edge.t -> t -> option EdgeLabel -> Prop.

Parameter In_graph_vertex_spec : forall v g,
In_graph_vertex v g <-> VertexMap.In v (V g).

Parameter In_graph_labeled_vertex_spec : forall v g l,
In_graph_labeled_vertex v g l <-> VertexMap.MapsTo v l (V g).

Add Morphism In_graph_vertex : In_graph_vertex_m.
Add Morphism In_graph_labeled_vertex : In_graph_labeled_vertex_m.

Parameter In_graph_edge_spec : forall e g,
In_graph_edge e g <-> EdgeMap.In e (E g).

Opaque Edge.t.

Parameter In_graph_labeled_edge_spec : forall e g l,
In_graph_labeled_edge e g l <-> EdgeMap.MapsTo e l (E g).

Add Morphism In_graph_edge : In_graph_edge_m.
Add Morphism In_graph_labeled_edge : In_graph_labeled_edge_m.

Parameter link_edge_equiv : forall v1 v2 g l,
link g v1 v2 = Some l <-> In_graph_labeled_edge (v1,v2) g l.

Parameter mapsto_edge_equiv_succ : forall v1 v2 g l,
VertexMap.MapsTo v2 l (successors v1 g) <-> In_graph_labeled_edge (v1,v2) g l.

Parameter mapsto_edge_equiv_pred : forall v1 v2 g l,
VertexMap.MapsTo v1 l (predecessors v2 g) <-> In_graph_labeled_edge (v1,v2) g l.


Parameter In_graph_edge_in_ext : forall e g,
In_graph_edge e g -> In_graph_vertex (fst_end e) g /\
                                   In_graph_vertex (snd_end e) g.

Parameter fold_edges : forall (A : Type), (t -> Edge.t -> (option EdgeLabel) -> A -> A) -> t -> A -> A.
Parameter fold_vertices : forall (A : Type), (t -> Vertex.t -> (option NodeLabel) -> A -> A) -> t -> A -> A.
Parameter fold_succ : forall (A : Type), (t -> Vertex.t -> Vertex.t -> (option EdgeLabel) -> A -> A) -> Vertex.t -> t -> A -> A.
Parameter fold_pred : forall (A : Type), (t -> Vertex.t -> Vertex.t -> (option EdgeLabel) -> A -> A) -> Vertex.t -> t -> A -> A.
Parameter fold_succ_ne : forall (A : Type), (t -> Vertex.t -> Vertex.t -> (option EdgeLabel) -> A -> A) -> Vertex.t -> t -> A -> A.
Parameter fold_pred_ne : forall (A : Type), (t -> Vertex.t -> Vertex.t -> (option EdgeLabel) -> A -> A) -> Vertex.t -> t -> A -> A.

Implicit Arguments fold_edges [A].
Implicit Arguments fold_vertices [A].
Implicit Arguments fold_succ [A].
Implicit Arguments fold_pred [A].
Implicit Arguments fold_succ_ne [A].
Implicit Arguments fold_pred_ne [A].

Parameter fold_vertices_spec : forall (A : Type) f g (a : A),
fold_vertices f g a = VertexMap.fold (f g) (V g) a.

Parameter fold_edges_spec : forall (A : Type) f g (a : A),
fold_edges f g a = EdgeMap.fold (f g) (E g) a.

Parameter fold_succ_spec : forall (A : Type) f v g (a : A),
fold_succ f v g a = VertexMap.fold (f g v) (successors v g) a.

Parameter fold_pred_spec : forall (A : Type) f v g (a : A),
fold_pred f v g a = VertexMap.fold (f g v) (predecessors v g) a.

Parameter fold_succ_ne_spec : forall (A : Type) f v g (a : A),
fold_succ_ne f v g a = VertexMap.fold (f g v) (VertexMap.remove v (successors v g)) a.

Parameter fold_pred_ne_spec : forall (A : Type) f v g (a : A),
fold_pred_ne f v g a = VertexMap.fold (f g v) (VertexMap.remove v (predecessors v g)) a.

Parameter empty_graph : t.
Parameter add_vertex : Vertex.t -> t -> option NodeLabel -> t.
Parameter add_edge : Edge.t -> t -> option EdgeLabel -> t.
Parameter add_edge_w : Edge.t -> t -> option EdgeLabel -> t.
Parameter remove_vertex : Vertex.t -> t -> t.
Parameter remove_edge : Edge.t -> t -> t.


Parameter In_remove_vertex : forall x r g w,
In_graph_labeled_vertex x (remove_vertex r g) w <->
(In_graph_labeled_vertex x g w /\ ~Vertex.eq x r).

Parameter In_remove_edge : forall e r g w,
In_graph_labeled_edge e (remove_vertex r g) w <->
(In_graph_labeled_edge e g w /\ ~incident e r).


Parameter In_add_vertex : forall v g x w w',
In_graph_labeled_vertex x (add_vertex v g w) w' <->
(~In_graph_vertex v g /\ Vertex.eq x v /\ w = w') \/ In_graph_labeled_vertex x g w'.

Parameter In_add_vertex_edge : forall v g e w w',
In_graph_labeled_edge e (add_vertex v g w) w' <-> In_graph_labeled_edge e g w'.

Definition In_ext e g := In_graph_vertex (fst_end e) g /\ In_graph_vertex (snd_end e) g.


Parameter In_graph_add_edge_vertex : forall v g e w w',
(In_graph_labeled_vertex v (add_edge e g w) w' <-> In_graph_labeled_vertex v g w').

Parameter In_graph_edge_add_edge : forall e e' g w w',
In_graph_labeled_edge e' g w->
~Edge.eq e e' ->
In_graph_labeled_edge e' (add_edge e g w') w.

Parameter In_graph_edge_add_edge_2 : forall e g w,
In_ext e g ->
In_graph_labeled_edge e (add_edge e g w) w.

Parameter In_graph_add_edge_edge : forall g e e' w w',
In_ext e g ->
In_graph_labeled_edge e' (add_edge e g w) w' ->
~Edge.eq e e' ->
In_graph_labeled_edge e' g w'.

Parameter Add_edge_fail_vertex : forall e g w v w',
~In_ext e g ->
(In_graph_labeled_vertex v g w' <->
In_graph_labeled_vertex v (add_edge e g w) w').

Parameter Add_edge_fail_edge : forall e g w e' w',
~In_ext e g ->
(In_graph_labeled_edge e' g w' <->
In_graph_labeled_edge e' (add_edge e g w) w').


Parameter In_graph_add_edge_weak_vertex : forall v g e w w',
In_graph_labeled_vertex v (add_edge_w e g w) w' <->
In_graph_labeled_vertex v g w' \/ (incident e v /\ w' = None /\ ~In_graph_vertex v g).

Parameter In_graph_add_edge_weak_edge : forall g e e' w w',
In_graph_labeled_edge e' (add_edge_w e g w) w' <->
(eq e e' /\ w = w') \/ (~eq e e' /\ In_graph_labeled_edge e' g w').


Parameter In_graph_remove_edge_vertex : forall v e g w,
(In_graph_labeled_vertex v (remove_edge e g) w <->
In_graph_labeled_vertex v g w).

Parameter In_graph_remove_edge_edge_succ : forall e g,
~VertexMap.In (snd_end e) (successors (fst_end e) (remove_edge e g)).

Parameter In_graph_remove_edge_edge_pred : forall e g,
~VertexMap.In (fst_end e) (predecessors (snd_end e) (remove_edge e g)).

End Constructive_Directed_Graph.