Library Graph_Properties

Require Import DigraphInterface.
Require Import OrderedType.
Require Import Labels.

Module GraphProps (Vertex : OrderedType) (Lab : Labels)
                                (G : Directed_Graph Vertex Lab).

Import G.

Lemma In_graph_vertex_dec : forall v g, {In_graph_vertex v g}+{~In_graph_vertex v g}.

Proof.
intros. case_eq (VertexMap.find v (V g));[left|right]; intros.
rewrite In_graph_vertex_spec. rewrite MapFacts.in_find_iff. congruence.
rewrite In_graph_vertex_spec. rewrite MapFacts.in_find_iff. congruence.
Qed.

Lemma In_graph_edge_dec : forall e g, {In_graph_edge e g}+{~In_graph_edge e g}.

Proof.
intros. case_eq (EdgeMap.find e (E g));[left|right]; intros.
rewrite In_graph_edge_spec. rewrite EMapFacts.in_find_iff. congruence.
rewrite In_graph_edge_spec. rewrite EMapFacts.in_find_iff. congruence.
Qed.


Lemma In_graph_labeled_vertex_weak : forall v g val,
In_graph_labeled_vertex v g val ->
In_graph_vertex v g.

Proof.
 intros.
 rewrite In_graph_labeled_vertex_spec in H.
 rewrite In_graph_vertex_spec.
 apply MapsTo_In with (e := val). assumption.
Qed.

Lemma In_graph_vertex_strong : forall v g,
In_graph_vertex v g ->
exists val, In_graph_labeled_vertex v g val.

Proof.
 intros.
 rewrite In_graph_vertex_spec in H. rewrite Mapsto_In in H. destruct H.
 exists x. rewrite In_graph_labeled_vertex_spec. auto.
Qed.

Lemma In_graph_labeled_edge_weak : forall e g val,
In_graph_labeled_edge e g val ->
In_graph_edge e g.

Proof.
 intros.
 rewrite In_graph_labeled_edge_spec in H.
 rewrite In_graph_edge_spec.
 apply EMapFacts.MapsTo_In with (e := val). assumption.
Qed.

Lemma In_graph_edge_strong : forall e g,
In_graph_edge e g ->
exists val, In_graph_labeled_edge e g val.

Proof.
 intros.
 rewrite In_graph_edge_spec in H. rewrite EMapFacts.Mapsto_In in H. destruct H.
 exists x. rewrite In_graph_labeled_edge_spec. auto.
Qed.

Lemma labeled_edge_edge_label : forall e g w w',
In_graph_labeled_edge e g w ->
edge_label e g = Some w' ->
w = w'.

Proof.
intros.
rewrite In_graph_labeled_edge_spec in H.
rewrite edge_label_spec in H0.
apply EMapFacts.MapsTo_fun with (m := (E g)) (x := e).
assumption.
apply EdgeMap.find_2. assumption.
Qed.

Lemma labeled_vertex_vertex_label : forall v g w w',
In_graph_labeled_vertex v g w ->
vertex_label v g = Some w' ->
w = w'.

Proof.
intros.
rewrite In_graph_labeled_vertex_spec in H.
rewrite vertex_label_spec in H0.
apply MapsTo_fun with (m := (V g)) (x := v).
assumption.
apply VertexMap.find_2. assumption.
Qed.

Lemma In_graph_labeled_edge_eq : forall e g w w',
In_graph_labeled_edge e g w ->
In_graph_labeled_edge e g w' ->
w = w'.

Proof.
intros.
rewrite In_graph_labeled_edge_spec in *.
apply EMapFacts.MapsTo_fun with (m := E g) (x := e); assumption.
Qed.

Lemma In_graph_labeled_vertex_eq : forall v g w w',
In_graph_labeled_vertex v g w ->
In_graph_labeled_vertex v g w' ->
w = w'.

Proof.
intros.
rewrite In_graph_labeled_vertex_spec in *.
apply MapsTo_fun with (m := V g) (x := v); assumption.
Qed.



Definition eq g1 g2 := VertexMap.Equal (V g1) (V g2) /\
                                    EdgeMap.Equal (E g1) (E g2).

Notation "g1 =G g2" := (eq g1 g2) (at level 80).

Lemma eq_trans : forall g1 g2 g3, g1 =G g2 -> g2 =G g3 -> g1 =G g3.

Proof.
 unfold eq. intros.
 destruct H. destruct H0.
 split; [eapply MapFacts.Equal_trans| eapply EMapFacts.MapFacts.Equal_trans]; eauto.
Qed.

Lemma eq_refl : forall g, g =G g.

Proof.
 unfold eq. intros.
 split;[apply MapFacts.Equal_refl| apply EMapFacts.MapFacts.Equal_refl].
Qed.

Lemma eq_sym : forall g1 g2, g1 =G g2 -> g2 =G g1.

Proof.
 unfold eq. intros.
 destruct H.
 split; [apply MapFacts.Equal_sym|apply EMapFacts.MapFacts.Equal_sym]; auto.
Qed.

End GraphProps.