Library DigraphMapImp

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

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

Import Lab.

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


Close Scope nat_scope.

Definition maptype :=
VertexMap.t (option NodeLabel *
                    (VertexMap.t (option EdgeLabel) *
                    (VertexMap.t (option EdgeLabel)))).

Definition adj_map (x : Vertex.t) (m : maptype)
                               :=
match (VertexMap.find x m) with
| None => let empty_m := VertexMap.empty (option EdgeLabel) in
                 (None, (empty_m, empty_m))
| Some wmaps => wmaps
end.

Definition succ x m := fst (snd (adj_map x m)).
Definition pred x m := snd (snd (adj_map x m)).

Definition is_succ y x m := VertexMap.In y (succ x m).
Definition is_pred y x m := VertexMap.In y (pred x m).

Definition is_labeled_succ y x m w := VertexMap.MapsTo y w (succ x m).
Definition is_labeled_pred y x m w := VertexMap.MapsTo y w (pred x m).

Record tt : Type := Make_Graph {
map : maptype;

pred_succ : forall x y w, is_labeled_succ y x map w <-> is_labeled_pred x y map w
}.

Definition successors v g := succ v (map g).
Definition predecessors v g := pred v (map g).

Lemma unw_pred_succ : forall g x y, is_succ y x (map g) <-> is_pred x y (map g).

Proof.
intros. generalize (pred_succ g); intro.
unfold is_labeled_succ, is_labeled_pred, is_succ, is_pred in *.
do 2 rewrite Mapsto_In.
split; intro; destruct H0; exists x0; apply H; assumption.
Qed.

Definition t := tt.


Definition V g := VertexMap.map (fun wsp => fst wsp) (map g).

Definition vertex_label v g := match VertexMap.find v (map g) with
                                                  | None => None
                                                  | Some wsp => Some (fst wsp)
                                                end.

Definition add_neighborhood x
                                               (wsp : option NodeLabel * (VertexMap.t (option EdgeLabel) * VertexMap.t (option EdgeLabel))) (s : EdgeMap.t (option EdgeLabel)) :=
let (w,sp) := wsp in let (su,pr) := sp in
(VertexMap.fold (fun y v s' => EdgeMap.add (x,y) v s') su s).

Definition E (g : t) :=
VertexMap.fold (fun x wsp s => add_neighborhood x wsp s)
                         (map g)
                         (EdgeMap.empty (option EdgeLabel)).

Definition edge_label e g := VertexMap.find (snd_end e) (successors (fst_end e) g).

Definition link g v1 v2 := VertexMap.find v2 (successors v1 g).

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

Proof.
unfold vertex_label. intros.
case_eq (VertexMap.find v (map g)); intros.
destruct p. simpl in *.
unfold V.
set (f := (fun
        wsp : option NodeLabel *
              (VertexMap.t (option EdgeLabel) *
               VertexMap.t (option EdgeLabel)) => fst wsp)) in *.
case_eq (VertexMap.find v (VertexMap.map f (map g))); intros.
generalize (VertexMap.find_2 H0). clear H0. intro.
rewrite MapFacts.map_mapsto_iff in H0. destruct H0. destruct H0.
unfold f in H0. generalize (VertexMap.find_2 H). clear H. intro.
destruct x. simpl in *. generalize (MapsTo_fun H H1). intro.
inversion H2. subst. auto.
generalize (VertexMap.find_2 H). clear H. intro.
generalize (MapsTo_In _ _ _ _ H). clear H. intro.
rewrite <-MapFacts.map_in_iff with (f:= f) in H.
rewrite MapFacts.in_find_iff in H. congruence.
set (f := (fun
        wsp : option NodeLabel *
              (VertexMap.t (option EdgeLabel) *
               VertexMap.t (option EdgeLabel)) => fst wsp)) in *.
case_eq (VertexMap.find v (VertexMap.map f (map g))); intros.
generalize (VertexMap.find_2 H0). clear H0. intro.
generalize (MapsTo_In _ _ _ _ H0). clear H0. intro.
rewrite MapFacts.map_in_iff in H0. rewrite MapFacts.in_find_iff in H0. congruence.
unfold V. unfold f in H0. rewrite H0. auto.
Qed.

Definition In_graph_vertex v g := VertexMap.In v (map g).

Definition In_graph_labeled_vertex v g w :=
                exists m, VertexMap.find v (map g) = Some (w,m).

Definition In_graph_edge (e : Edge.t) g :=
is_succ (snd_end e) (fst_end e) (map g).

Definition In_graph_labeled_edge e g w :=
is_labeled_succ (snd_end e) (fst_end e) (map g) w.

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


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

Proof.
unfold In_graph_vertex, V. intros.
rewrite MapFacts.map_in_iff. reflexivity.
Qed.

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

Proof.
unfold In_graph_labeled_vertex, V. intros.
set (f := (fun
        wsp : option NodeLabel *
              (VertexMap.t (option EdgeLabel) *
               VertexMap.t (option EdgeLabel)) => fst wsp)) in *.
split; intros.
destruct H. replace l with (f (l,x)).
apply VertexMap.map_1. apply VertexMap.find_2. auto.
auto.
rewrite MapFacts.map_mapsto_iff in H. destruct H. destruct H.
destruct x. simpl in H. subst. exists p.
apply VertexMap.find_1. auto.
Qed.

Add Morphism In_graph_vertex : In_graph_vertex_m.

Proof.
unfold In_graph_vertex; intros.
do 2 rewrite MapFacts.in_find_iff. rewrite (MapFacts.find_o _ H). reflexivity.
Qed.

Add Morphism In_graph_labeled_vertex : In_graph_labeled_vertex_m.

Proof.
unfold In_graph_labeled_vertex; intros.
split; intros; destruct H0; exists x0.
rewrite (MapFacts.find_o _ H) in H0; auto.
rewrite (MapFacts.find_o _ H); auto.
Qed.

Ltac eq_key_simpl :=
unfold VertexMap.eq_key, VertexMap.Raw.Proofs.PX.eqk in *; simpl in *; auto.

Ltac eq_key_elt_simpl :=
unfold VertexMap.eq_key_elt, VertexMap.Raw.Proofs.PX.eqke in *; simpl in *; auto.

Ltac eq_key_solve := eq_key_simpl; eq_key_elt_simpl.

Lemma add_neighborhood_spec : forall x wsp s v a b,
(forall v1 v2, EdgeMap.In (v1,v2) s -> ~Vertex.eq x v1) ->
(EdgeMap.MapsTo (a,b) v (add_neighborhood x wsp s) <->
(~Vertex.eq x a /\ EdgeMap.MapsTo (a,b) v s) \/ (Vertex.eq x a /\ VertexMap.MapsTo b v (fst (snd wsp)))).

Proof.
unfold add_neighborhood; intros x wsp s v a b HH.
destruct wsp. destruct p. simpl.
rewrite VertexMap.fold_1.
set (f := (fun (a0 : EdgeMap.t (option EdgeLabel))
        (p : VertexMap.key * option EdgeLabel) =>
      EdgeMap.add (x, fst p) (snd p) a0)) in *.
split; intros.
generalize VertexMap.elements_2. intro.
generalize (H0 _ t0). clear H0. intro Helt.
generalize VertexMap.elements_3w. intro.
generalize (H0 _ t0). clear H0. intro HND.
induction (VertexMap.elements t0).
simpl in H. left. split.
apply HH with (v2 := b). apply (EMapFacts.MapsTo_In _ _ _ _ H). auto.
rewrite fold_left_assoc_map_find_nodup in H. set (m := fold_left f l s) in *.
unfold f in H. rewrite EMapFacts.add_mapsto_iff in H. simpl in H.
destruct H. destruct H. destruct H. subst.
right. split. auto. apply Helt. left. eq_key_solve.
apply IHl. destruct H. auto.
intros. apply Helt. right. auto.
inversion HND; auto.
intros. apply EMapFacts.Equal_refl.
intros. eapply EMapFacts.Equal_trans; eauto.
eauto.
unfold f. intros. apply EMapFacts.add_add_Eq. simpl. intro.
elim H0. destruct H1. eq_key_solve.
unfold f. intros. apply EMapFacts.add_m. split; eq_key_solve.
auto.
auto.
generalize VertexMap.elements_1.
intro. generalize (H0 _ t0 b v). clear H0. intro.
generalize VertexMap.elements_3w. intro.
generalize (H1 _ t0). clear H1. intro HND.
induction (VertexMap.elements t0).
simpl. destruct H. auto. destruct H. auto.
destruct H. generalize (H0 H1). intro. inversion H2.
rewrite fold_left_assoc_map_find_nodup. set (m := fold_left f l s) in *.
unfold f. rewrite EMapFacts.add_mapsto_iff. simpl.
destruct H.
destruct H.
right. split. intro. destruct H2. elim H. auto.
unfold m. apply fold_invariant. auto.
intros. unfold f. rewrite EMapFacts.add_mapsto_iff. simpl.
right. split. intro. destruct H4. elim H. auto. auto.
destruct H. generalize (H0 H1). intro.
inversion H2; subst.
left. split. split; auto. inversion H4; auto. inversion H4; auto.
right. split. intro. destruct H3.
generalize (H0 H1). intro.
inversion HND. subst. elim H9.
rewrite <-H5 in H4.
rewrite InA_alt. rewrite InA_alt in H4. destruct H4. destruct H4.
exists x0. split. inversion H4;eq_key_solve. auto.
apply IHl. intro. auto.
inversion HND; auto.
inversion HND; auto.
intros. apply EMapFacts.Equal_refl.
intros. eapply EMapFacts.Equal_trans; eauto.
eauto.
unfold f. intros. apply EMapFacts.add_add_Eq. simpl. intro.
elim H1. destruct H2. eq_key_solve.
unfold f. intros. apply EMapFacts.add_m. split; eq_key_solve.
auto.
auto.
Qed.

Lemma add_neighborhood_diff : forall v1 v2 v3 s v m,
~Vertex.eq v1 v3 ->
(EdgeMap.MapsTo (v1,v2) v (add_neighborhood v3 s m) <->
 EdgeMap.MapsTo (v1,v2) v m).

Proof.
unfold add_neighborhood; intros x wsp s v a b HH.
destruct v. destruct p. simpl.
rewrite VertexMap.fold_1.
set (f := (fun (a0 : EdgeMap.t (option EdgeLabel))
        (p : VertexMap.key * option EdgeLabel) =>
      EdgeMap.add (s, fst p) (snd p) a0)) in *.
apply fold_invariant. reflexivity.
intros. unfold f. rewrite EMapFacts.add_mapsto_iff. simpl.
split; intros.
destruct H1.
destruct H1. destruct H1. elim HH. auto.
destruct H1. rewrite <-H0. auto.
right. split.
intro. elim HH. destruct H2. auto. rewrite H0. auto.
Qed.

Lemma add_neighborhood_eq : forall x wsp s a b v,
Vertex.eq x a ->
(EdgeMap.MapsTo (a,b) v (add_neighborhood x wsp s) <->
((forall val, ~VertexMap.MapsTo b val (fst (snd wsp))) /\ EdgeMap.MapsTo (a,b) v s)
 \/ VertexMap.MapsTo b v (fst (snd wsp))).

Proof.
unfold add_neighborhood; intros x wsp s v a b.
destruct wsp. destruct p. simpl.
rewrite VertexMap.fold_1.
set (f := (fun (a0 : EdgeMap.t (option EdgeLabel))
        (p : VertexMap.key * option EdgeLabel) =>
      EdgeMap.add (x, fst p) (snd p) a0)) in *.
intro HH.
split; intros.
generalize VertexMap.elements_2. intro.
generalize (H0 _ t0 a). clear H0. intro Helt.
generalize VertexMap.elements_1. intro.
generalize (H0 _ t0 a). clear H0. intro Helt2.
generalize VertexMap.elements_3w. intro.
generalize (H0 _ t0). clear H0. intro HND.
induction (VertexMap.elements t0).
simpl in H. left. split.
intro. intro. generalize (Helt2 _ H0). intro. inversion H1.
auto.
rewrite fold_left_assoc_map_find_nodup in H. set (m := fold_left f l s) in *.
unfold f in H. rewrite EMapFacts.add_mapsto_iff in H. simpl in H.
destruct H. destruct H. destruct H. subst.
right. apply Helt. left. eq_key_solve.
apply IHl. destruct H. auto.
intros. apply Helt. right. auto.
intros. generalize (Helt2 _ H0). intro.
inversion H1; subst.
destruct H. elim H.
split. auto.
inversion H3; auto.
auto.
inversion HND; auto.
intros. apply EMapFacts.Equal_refl.
intros. eapply EMapFacts.Equal_trans; eauto.
eauto.
unfold f. intros. apply EMapFacts.add_add_Eq. simpl. intro.
elim H0. destruct H1. eq_key_solve.
unfold f. intros. apply EMapFacts.add_m. split; eq_key_solve.
auto.
auto.
destruct H. destruct H.
apply fold_invariant. auto.
unfold f; intros.
rewrite EMapFacts.add_mapsto_iff. simpl.
assert (VertexMap.MapsTo (fst x0) (snd x0) t0).
apply VertexMap.elements_2. rewrite InA_alt. exists x0.
split. eq_key_solve. auto.
destruct (Vertex.eq_dec (fst x0) a).
elim (H (snd x0)).
rewrite <-e. auto.
right. split. intro. elim n. destruct H4. auto.
auto.

generalize VertexMap.elements_2. intro.
generalize (H0 _ t0 a b). clear H0. intro Helt.
generalize VertexMap.elements_1. intro.
generalize (H0 _ t0 a b). clear H0. intro H0.
generalize VertexMap.elements_3w. intro.
generalize (H1 _ t0). clear H1. intro HND.
induction (VertexMap.elements t0).
simpl. generalize (H0 H). intro. inversion H1.
rewrite fold_left_assoc_map_find_nodup. set (m := fold_left f l s) in *.
unfold f. rewrite EMapFacts.add_mapsto_iff. simpl.
generalize (H0 H). intro.
inversion H1; subst.
left. split. split. auto. inversion H3; auto. inversion H3; auto.
right. split. intro. destruct H2. inversion HND; subst.
elim H7. rewrite InA_alt in H3. destruct H3. destruct H3.
rewrite InA_alt. exists x0. split. inversion H3; subst.
simpl in *. rewrite H6 in H4. eq_key_solve. auto.
apply IHl. intro. auto.
intro. auto.
inversion HND; auto.
intros. apply EMapFacts.Equal_refl.
intros. eapply EMapFacts.Equal_trans; eauto.
eauto.
unfold f. intros. apply EMapFacts.add_add_Eq. simpl. intro.
elim H1. destruct H2. eq_key_solve.
unfold f. intros. apply EMapFacts.add_m. split; eq_key_solve.
auto.
auto.
Qed.

Lemma add_neighborhood_comm : forall y z s,
~ VertexMap.eq_key y z ->
EdgeMap.Equal
  (add_neighborhood (fst z) (snd z) (add_neighborhood (fst y) (snd y) s))
  (add_neighborhood (fst y) (snd y) (add_neighborhood (fst z) (snd z) s)).

Proof.
intros. intro. destruct y0.
case_eq (EdgeMap.find (t0,t1) (add_neighborhood (fst z) (snd z)
                                                (add_neighborhood (fst y) (snd y) s))); intros.
assert (EdgeMap.MapsTo (t0,t1) o (add_neighborhood (fst y) (snd y)
                                                           (add_neighborhood (fst z) (snd z) s))).
generalize (EdgeMap.find_2 H0). clear H0. intros.
destruct (Vertex.eq_dec t0 (fst z)).
rewrite add_neighborhood_eq in H0. rewrite add_neighborhood_diff in H0.
rewrite add_neighborhood_diff. rewrite add_neighborhood_eq.
destruct H0. destruct H0.
left. split; auto.
right; auto.
auto.
intro. elim H. rewrite e in H1. eq_key_solve.
intro. elim H. rewrite e in H1. eq_key_solve.
auto.
rewrite add_neighborhood_diff in H0.
destruct (Vertex.eq_dec t0 (fst y)).
rewrite add_neighborhood_eq in H0.
rewrite add_neighborhood_eq. rewrite add_neighborhood_diff.
destruct H0. destruct H0.
left. split; auto.
right. auto.
intro. elim H. rewrite e in H1. eq_key_solve.
auto.
auto.
rewrite add_neighborhood_diff in H0. rewrite add_neighborhood_diff.
rewrite add_neighborhood_diff.
auto.
auto.
auto.
auto.
auto.
rewrite (EdgeMap.find_1 H1). auto.

case_eq (EdgeMap.find (t0,t1) (add_neighborhood (fst y) (snd y)
                                                (add_neighborhood (fst z) (snd z) s))); intros.
assert (EdgeMap.MapsTo (t0,t1) o (add_neighborhood (fst z) (snd z)
                                                           (add_neighborhood (fst y) (snd y) s))).
generalize (EdgeMap.find_2 H1). clear H1. intros.
destruct (Vertex.eq_dec t0 (fst y)).
rewrite add_neighborhood_eq in H1. rewrite add_neighborhood_diff in H1.
rewrite add_neighborhood_diff. rewrite add_neighborhood_eq.
destruct H1. destruct H1.
left. split; auto.
right; auto.
auto.
intro. elim H. rewrite e in H2. eq_key_solve.
intro. elim H. rewrite e in H2. eq_key_solve.
auto.
rewrite add_neighborhood_diff in H1.
destruct (Vertex.eq_dec t0 (fst z)).
rewrite add_neighborhood_eq in H1.
rewrite add_neighborhood_eq. rewrite add_neighborhood_diff.
destruct H1. destruct H1.
left. split; auto.
right. auto.
auto.
auto.
auto.
rewrite add_neighborhood_diff in H1.
rewrite add_neighborhood_diff. rewrite add_neighborhood_diff. auto.
auto.
auto.
auto.
auto.

rewrite (EdgeMap.find_1 H2) in H0. congruence.
auto.
Qed.

Lemma add_neighborhood_compat : forall a e1 e2,
EdgeMap.Equal e1 e2 ->
EdgeMap.Equal (add_neighborhood (fst a) (snd a) e1)
  (add_neighborhood (fst a) (snd a) e2).

Proof.
intros. intro.
case_eq (EdgeMap.find y (add_neighborhood (fst a) (snd a) e1)); intros.
generalize (EdgeMap.find_2 H0). intro.
assert (EdgeMap.MapsTo y o (add_neighborhood (fst a) (snd a) e2)).
destruct y. destruct (Vertex.eq_dec t0 (fst a)).
rewrite add_neighborhood_eq. rewrite add_neighborhood_eq in H1.
destruct H1. destruct H1.
left. split; auto.
apply EdgeMap.find_2. rewrite <-H. apply EdgeMap.find_1. auto.
right. auto.
auto.
auto.
rewrite add_neighborhood_diff in H1. rewrite add_neighborhood_diff.
apply EdgeMap.find_2. rewrite <-H. apply EdgeMap.find_1. auto.
auto.
auto.
rewrite (EdgeMap.find_1 H2). auto.

case_eq (EdgeMap.find y (add_neighborhood (fst a) (snd a) e2)); intros.
generalize (EdgeMap.find_2 H1). intro.
assert (EdgeMap.MapsTo y o (add_neighborhood (fst a) (snd a) e1)).
destruct y. destruct (Vertex.eq_dec t0 (fst a)).
rewrite add_neighborhood_eq. rewrite add_neighborhood_eq in H2.
destruct H2. destruct H2.
left. split; auto.
apply EdgeMap.find_2. rewrite H. apply EdgeMap.find_1. auto.
right. auto.
auto.
auto.
rewrite add_neighborhood_diff in H2. rewrite add_neighborhood_diff.
apply EdgeMap.find_2. rewrite H. apply EdgeMap.find_1. auto.
auto.
auto.
rewrite (EdgeMap.find_1 H3) in H0. auto.
auto.
Qed.

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

Proof.
unfold E. intros.
rewrite VertexMap.fold_1.
assert (forall a, InA (@VertexMap.eq_key_elt (option NodeLabel*(VertexMap.t (option EdgeLabel)*VertexMap.t (option EdgeLabel))))
                               a (VertexMap.elements (map g)) ->
            fst (snd (snd a)) = succ (fst a) (map g)) as HH.
intros. destruct a.
generalize (VertexMap.elements_2 H). simpl. intro.
unfold succ, adj_map.
rewrite (VertexMap.find_1 H0). auto.
split; intros.
assert (exists z, VertexMap.MapsTo (fst_end e) z (map g)).
case_eq (VertexMap.find (fst_end e) (map g)); intros.
exists p. apply VertexMap.find_2. auto.
unfold In_graph_labeled_edge, is_labeled_succ, succ, adj_map in H.
rewrite H0 in H. simpl in H. rewrite MapFacts.empty_mapsto_iff in H. inversion H.
destruct H0. generalize VertexMap.elements_1. intro.
generalize (H1 _ _ _ _ H0). clear H0 H1. intro Hfst.
generalize VertexMap.elements_3w. intro.
generalize (H0 _ (map g)). clear H0. intro HND.
induction (VertexMap.elements (map g)).
simpl. inversion Hfst.
set (f := (fun (a0 : EdgeMap.t (option EdgeLabel))
        (p : VertexMap.key *
             (option NodeLabel *
              (VertexMap.t (option EdgeLabel) *
               VertexMap.t (option EdgeLabel)))) =>
      add_neighborhood (fst p) (snd p) a0)) in *.
rewrite fold_left_assoc_map_find_nodup.
set (m := (fold_left f l0 (EdgeMap.empty (option EdgeLabel)))) in *.
unfold f. rewrite (edge_eq e). rewrite add_neighborhood_spec.
inversion Hfst; subst.
right. split. inversion H1; auto.
rewrite HH.
unfold In_graph_labeled_edge, is_labeled_succ in *. simpl.
unfold succ, adj_map in *. inversion H1. simpl in H0.
rewrite (MapFacts.find_o _ H0) in H. auto.
left. eq_key_elt_simpl.
left. rewrite <-(edge_eq e). split.
intro. inversion HND. subst. elim H4.
rewrite InA_alt in H1. destruct H1. destruct H1. rewrite InA_alt. exists x0.
split. inversion H1. simpl in *. subst. rewrite <-H0 in H3. eq_key_solve. auto.
apply IHl0.
intros. apply HH. right. auto.
auto.
inversion HND; auto.

clear IHl0 Hfst HH H.
unfold m. apply fold_invariant. intros.
rewrite EMapFacts.empty_in_iff in H. inversion H.
intros.
unfold f in H1. rewrite EMapFacts.Mapsto_In in H1. destruct H1.
destruct (Vertex.eq_dec v1 (fst x0)).
intro. inversion HND. subst. elim H5.
rewrite InA_alt. exists x0. split.
rewrite e0 in H2. eq_key_solve. auto.
rewrite add_neighborhood_diff in H1. apply H0 with (v2 := v2).
apply EMapFacts.MapsTo_In with (e := x1). auto. auto.
intros. apply EMapFacts.Equal_refl.
intros. eapply EMapFacts.Equal_trans; eauto.
eauto.
unfold f.
apply add_neighborhood_comm.
intros. apply add_neighborhood_compat. auto.

generalize VertexMap.elements_3w. intro.
generalize (H0 _ (map g)). clear H0. intro HND.
induction (VertexMap.elements (map g)).
simpl in H. rewrite EMapFacts.empty_mapsto_iff in H. inversion H.
set (f := (fun (a0 : EdgeMap.t (option EdgeLabel))
        (p : VertexMap.key *
             (option NodeLabel *
              (VertexMap.t (option EdgeLabel) *
               VertexMap.t (option EdgeLabel)))) =>
      add_neighborhood (fst p) (snd p) a0)) in *.
rewrite fold_left_assoc_map_find_nodup in H.
set (m := (fold_left f l0 (EdgeMap.empty (option EdgeLabel)))) in *.
unfold f in H. rewrite (edge_eq e) in H. rewrite add_neighborhood_spec in H.
destruct H.
unfold In_graph_labeled_edge, is_labeled_succ in *. simpl.
apply IHl0.
intros. apply HH. right. auto.
rewrite (edge_eq e). destruct H. auto.
inversion HND; auto.
destruct H.
unfold In_graph_labeled_edge, is_labeled_succ in *. simpl.
rewrite HH in H0.
unfold succ, adj_map in *.
rewrite (MapFacts.find_o _ H) in H0. auto.
left. eq_key_elt_simpl.

clear IHl0 HH H.
unfold m. apply fold_invariant. intros.
rewrite EMapFacts.empty_in_iff in H. inversion H.
intros.
unfold f in H1. rewrite EMapFacts.Mapsto_In in H1. destruct H1.
destruct (Vertex.eq_dec v1 (fst x)).
intro. inversion HND. subst. elim H5.
rewrite InA_alt. exists x. split.
rewrite e0 in H2. eq_key_solve. auto.
rewrite add_neighborhood_diff in H1. apply H0 with (v2 := v2).
apply EMapFacts.MapsTo_In with (e := x0). auto. auto.
intros. apply EMapFacts.Equal_refl.
intros. eapply EMapFacts.Equal_trans; eauto.
eauto.
unfold f. intros. apply add_neighborhood_comm; auto.
intros. apply add_neighborhood_compat. auto.
Qed.

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

Proof.
intros.
unfold edge_label, successors.
case_eq (EdgeMap.find e (E g)); intros.
generalize (EdgeMap.find_2 H). clear H. intro.
rewrite <-In_graph_labeled_edge_spec in H.
unfold In_graph_labeled_edge, is_labeled_succ in H.
apply (VertexMap.find_1 H).
unfold edge_label.
case_eq (VertexMap.find (snd_end e) (succ (fst_end e) (map g))); intros.
generalize (VertexMap.find_2 H0). intro.
fold (is_labeled_succ (snd_end e) (fst_end e) (map g) o) in H1.
fold (In_graph_labeled_edge e g o) in H1.
rewrite In_graph_labeled_edge_spec in H1.
rewrite EMapFacts.find_mapsto_iff in H1. congruence.
auto.
Qed.

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

Proof.
intros. rewrite EMapFacts.Mapsto_In. unfold In_graph_edge, is_succ.
split; intros.
generalize (In_MapsTo _ _ _ H). intro. destruct H0.
exists x. rewrite <-In_graph_labeled_edge_spec.
unfold In_graph_labeled_edge, is_labeled_succ. auto.
destruct H. rewrite Mapsto_In. exists x.
rewrite <-In_graph_labeled_edge_spec in H.
unfold In_graph_labeled_edge, is_labeled_succ in H. auto.
Qed.

Opaque Edge.t.

Add Morphism In_graph_edge : In_graph_edge_m.

Proof.
intros. do 2 rewrite In_graph_edge_spec.
do 2 rewrite EMapFacts.in_find_iff.
rewrite (EMapFacts.find_o _ H). reflexivity.
Qed.

Add Morphism In_graph_labeled_edge : In_graph_labeled_edge_m.

Proof.
intros. do 2 rewrite In_graph_labeled_edge_spec.
rewrite EMapFacts.MapsTo_iff. reflexivity. auto.
Qed.

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

Proof.
unfold link, successors, In_graph_labeled_edge, is_labeled_succ,
           succ, adj_map, In_graph_labeled_edge. intros. simpl.
split; intros.
apply VertexMap.find_2. auto.
apply VertexMap.find_1. auto.
Qed.

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

Proof.
intros. rewrite <-link_edge_equiv. unfold link.
split; intros.
apply VertexMap.find_1. auto.
apply VertexMap.find_2. auto.
Qed.

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

Proof.
intros. rewrite <-link_edge_equiv. unfold link.
unfold predecessors. fold (is_labeled_pred v1 v2 (map g) l).
rewrite <-pred_succ. fold (In_graph_labeled_edge (v1,v2) g l).
assert (is_labeled_succ v2 v1 (map g) l <-> In_graph_labeled_edge (v1,v2) g l).
unfold In_graph_labeled_edge. simpl. reflexivity.
rewrite H. clear H.
split; intros.
apply VertexMap.find_1. auto.
apply VertexMap.find_2. auto.
Qed.


Definition fold_vertices (A : Type) f g (a : A) := VertexMap.fold (f g) (V g) a.

Definition fold_edges (A : Type) f g (a : A) := EdgeMap.fold (f g) (E g) a.

Definition fold_succ (A : Type) f v g (a : A) :=
VertexMap.fold (f g v) (successors v g) a.

Definition fold_pred (A : Type) f v g (a : A) :=
VertexMap.fold (f g v) (predecessors v g) a.

Definition fold_succ_ne (A : Type) f v g (a : A) :=
VertexMap.fold (f g v) (VertexMap.remove v (successors v g)) a.

Definition fold_pred_ne (A : Type) f v g (a : A) :=
VertexMap.fold (f g v) (VertexMap.remove v (predecessors v g)) 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].

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

Proof.
auto.
Qed.

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

Proof.
auto.
Qed.

Lemma 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.

Proof.
auto.
Qed.

Lemma 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.

Proof.
auto.
Qed.

Lemma 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.

Proof.
auto.
Qed.

Lemma 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.

Proof.
auto.
Qed.

Definition empty_map : maptype :=
VertexMap.empty (option NodeLabel* (VertexMap.t (option EdgeLabel) * VertexMap.t (option EdgeLabel))).

Lemma pred_succ_empty : forall x y w,
is_labeled_succ y x empty_map w <-> is_labeled_pred x y empty_map w.

Proof.
intros. unfold is_labeled_succ, is_labeled_pred. do 2 rewrite MapFacts.empty_mapsto_iff. reflexivity.
Qed.

Definition empty_graph := Make_Graph empty_map (pred_succ_empty).

Lemma empty_graph_empty : forall v, ~In_graph_vertex v empty_graph.

Proof.
unfold In_graph_vertex. simpl.
unfold empty_map. intros. rewrite MapFacts.empty_in_iff. intuition.
Qed.


Lemma In_graph_edge_in_ext : forall e g,
In_graph_edge e g -> In_ext e g.

Proof.
unfold In_graph_edge, In_ext, In_graph_vertex.
split.
unfold is_succ, succ, adj_map in H. rewrite MapFacts.in_find_iff in *.
case_eq (VertexMap.find (fst_end e) (map g)); intros; rewrite H0 in H.
congruence.
simpl in H. rewrite MapFacts.empty_o in H. congruence.
rewrite unw_pred_succ in H.
unfold is_pred, pred, adj_map in H. rewrite MapFacts.in_find_iff in *.
case_eq (VertexMap.find (snd_end e) (map g)); intros.
congruence.
rewrite H0 in H.
simpl in H. rewrite MapFacts.empty_o in H. congruence.
Qed.



Definition add_vertex_map (m : maptype) x w :=
match VertexMap.find x m with
| None => let empty_m := VertexMap.empty (option EdgeLabel) in
                                           VertexMap.add x (w,(empty_m,empty_m)) m
| Some _ => m
end.

Lemma pred_succ_add_vertex : forall g v w x y w',
is_labeled_succ y x (add_vertex_map (map g) v w) w' <-> is_labeled_pred x y (add_vertex_map (map g) v w) w'.

Proof.
unfold add_vertex_map; intros.
case_eq (VertexMap.find v (map g)); intros.
apply pred_succ.
unfold is_labeled_succ, succ, adj_map.
destruct (Vertex.eq_dec x v).
rewrite MapFacts.add_eq_o. simpl.
unfold is_labeled_pred, pred, adj_map.
destruct (Vertex.eq_dec y v).
rewrite MapFacts.add_eq_o. simpl.
do 2 rewrite MapFacts.empty_mapsto_iff. reflexivity.
auto.
rewrite MapFacts.add_neq_o.
case_eq (VertexMap.find y (map g)); intros.
split; intros.
rewrite MapFacts.empty_mapsto_iff in H1. inversion H1.
destruct p.
assert (is_labeled_pred x y (map g) w').
unfold is_labeled_pred, pred, adj_map.
rewrite H0. assumption.
rewrite <-pred_succ in H2.
unfold is_labeled_succ, succ, adj_map in H2.
rewrite (MapFacts.find_o _ (Vertex.eq_sym e)) in H.
rewrite H in H2. simpl in H2. rewrite MapFacts.empty_mapsto_iff in H2. inversion H2.
simpl. do 2 rewrite MapFacts.empty_mapsto_iff. reflexivity.
auto.
auto.
rewrite MapFacts.add_neq_o.
unfold is_labeled_pred, pred, adj_map.
destruct (Vertex.eq_dec y v).
rewrite MapFacts.add_eq_o. simpl.
case_eq (VertexMap.find x (map g)); intros.
split; intros.
destruct p.
assert (is_labeled_succ y x (map g) w').
unfold is_labeled_succ, succ, adj_map.
rewrite H0. assumption.
rewrite pred_succ in H2.
unfold is_labeled_pred, pred, adj_map in H2.
rewrite (MapFacts.find_o _ (Vertex.eq_sym e)) in H.
rewrite H in H2. simpl in H2. rewrite MapFacts.empty_mapsto_iff in H2. inversion H2.
rewrite MapFacts.empty_mapsto_iff in H1. inversion H1.
simpl. do 2 rewrite MapFacts.empty_mapsto_iff. reflexivity.
auto.
auto.
rewrite MapFacts.add_neq_o.
apply pred_succ.
auto.
auto.
Qed.

Definition add_vertex v g w :=
Make_Graph (add_vertex_map (map g) v w)
                     (pred_succ_add_vertex g v w).

Lemma 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'.

Proof.
unfold In_graph_labeled_vertex, add_vertex, add_vertex_map. intros. simpl.
split; intros.
destruct H.
case_eq (VertexMap.find v (map g)); intros; rewrite H0 in H.
right.
exists x0. assumption.
destruct (Vertex.eq_dec x v).
left.
rewrite MapFacts.add_eq_o in H.
split.
unfold In_graph_vertex. rewrite MapFacts.in_find_iff. rewrite H0. congruence.
split;[auto| inversion H; auto].
auto.
right.
rewrite MapFacts.add_neq_o in H.
exists x0. auto.
auto.

do 2 destruct H. destruct H0.
unfold In_graph_vertex in H. rewrite MapFacts.in_find_iff in H.
case_eq (VertexMap.find v (map g)); intros; rewrite H2 in H; try congruence.
elim H. congruence.
rewrite MapFacts.add_eq_o.
exists ((VertexMap.empty (option EdgeLabel), VertexMap.empty (option EdgeLabel))).
rewrite H1. reflexivity.
auto.
case_eq (VertexMap.find v (map g)); intros.
exists x0. assumption.
rewrite MapFacts.add_neq_o.
exists x0. assumption.
intro. rewrite (MapFacts.find_o _ H1) in H0. congruence.
Qed.

Lemma 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'.

Proof.
unfold In_graph_labeled_edge, add_vertex, add_vertex_map. intros. simpl.
split; intros.
case_eq (VertexMap.find v (map g)); intros; rewrite H0 in H.
assumption.
unfold is_labeled_succ, succ, adj_map in *.
destruct (Vertex.eq_dec (fst_end e) v).
rewrite MapFacts.add_eq_o in H. simpl in H.
rewrite MapFacts.empty_mapsto_iff in H. inversion H.
auto.
rewrite MapFacts.add_neq_o in H.
assumption.
auto.
case_eq (VertexMap.find v (map g)); intros.
assumption.
unfold is_labeled_succ, succ, adj_map in *.
destruct (Vertex.eq_dec (fst_end e) v).
rewrite (MapFacts.find_o _ (Vertex.eq_sym e0)) in H0.
rewrite H0 in H. simpl in H. rewrite MapFacts.empty_mapsto_iff in H. inversion H.
rewrite MapFacts.add_neq_o. simpl. assumption.
auto.
Qed.


Definition remove_neighbor x (wsp : (option NodeLabel) *
                                                       (VertexMap.t (option EdgeLabel) *
                                                        VertexMap.t (option EdgeLabel)))
                                              :=
let (w,sp) := wsp in
let (s,p) := sp in
(w, (VertexMap.remove x s, VertexMap.remove x p)).

Definition remove_map (m : maptype) x : maptype :=
VertexMap.map (remove_neighbor x) (VertexMap.remove x m).

Lemma remove_neighbor_spec : forall v wsp w s p,
remove_neighbor v wsp = (w,(s,p)) ->
~VertexMap.In v s /\ ~VertexMap.In v p.

Proof.
intros.
unfold remove_neighbor. destruct wsp. destruct p0. simpl in *.
inversion H. subst.
split; rewrite MapFacts.remove_in_iff; intro; destruct H0; elim H0; auto.
Qed.

Lemma remove_map_mapsto : forall x v g,
VertexMap.In x (map g) ->
~Vertex.eq x v ->
VertexMap.MapsTo x (remove_neighbor v (adj_map x (map g))) (remove_map (map g) v).

Proof.
intros.
apply VertexMap.map_1. apply VertexMap.remove_2. auto.
unfold adj_map. case_eq (VertexMap.find x (map g)); intros.
apply VertexMap.find_2. auto.
rewrite MapFacts.in_find_iff in H. congruence.
Qed.

Lemma Equal_remove_empty : forall v,
VertexMap.Equal (VertexMap.remove v (VertexMap.empty (option EdgeLabel)))
                            (VertexMap.empty (option EdgeLabel)).

Proof.
split.
Qed.

Lemma remove_map_succ : forall x v g,
~Vertex.eq x v ->
VertexMap.Equal (succ x (remove_map (map g) v))
                            (VertexMap.remove v (succ x (map g))).

Proof.
unfold succ; intros.
unfold adj_map. case_eq (VertexMap.find x (remove_map (map g) v)); intros.
unfold remove_map in H0.
generalize (VertexMap.find_2 H0). clear H0. intro.
rewrite MapFacts.map_mapsto_iff in H0. destruct H0. destruct H0.
rewrite MapFacts.remove_mapsto_iff in H1. destruct H1.
generalize (VertexMap.find_1 H2). intro. rewrite H3.
rewrite H0. unfold remove_neighbor. destruct x0. destruct p0. simpl. reflexivity.
simpl. unfold remove_map in H0.
assert (~VertexMap.In x (VertexMap.remove v (map g))).
intro. rewrite MapFacts.in_find_iff in H1.
case_eq (VertexMap.find
       (elt:=option NodeLabel *
             (VertexMap.t (option EdgeLabel) * VertexMap.t (option EdgeLabel)))
       x
       (VertexMap.remove
          (elt:=option NodeLabel *
                (VertexMap.t (option EdgeLabel) *
                 VertexMap.t (option EdgeLabel))) v (map g))); intros.
generalize (VertexMap.find_2 H2). clear H2. intro.
generalize (VertexMap.map_1 (remove_neighbor v) H2). intro.
generalize (VertexMap.find_1 H3). clear H3. intro.
rewrite H3 in *. congruence.
congruence.
clear H0. rewrite MapFacts.in_find_iff in H1.
rewrite MapFacts.remove_neq_o in H1.
case_eq (VertexMap.find x (map g)); intros.
rewrite H0 in *. elim H1. congruence.
simpl in *.
rewrite Equal_remove_empty. apply MapFacts.Equal_refl.
auto.
Qed.

Lemma remove_map_pred : forall x v g,
~Vertex.eq x v ->
VertexMap.Equal (pred x (remove_map (map g) v))
                            (VertexMap.remove v (pred x (map g))).

Proof.
unfold pred; intros.
unfold adj_map. case_eq (VertexMap.find x (remove_map (map g) v)); intros.
unfold remove_map in H0.
generalize (VertexMap.find_2 H0). clear H0. intro.
rewrite MapFacts.map_mapsto_iff in H0. destruct H0. destruct H0.
rewrite MapFacts.remove_mapsto_iff in H1. destruct H1.
generalize (VertexMap.find_1 H2). intro. rewrite H3.
rewrite H0. unfold remove_neighbor. destruct x0. destruct p0. simpl. reflexivity.
simpl. unfold remove_map in H0.
assert (~VertexMap.In x (VertexMap.remove v (map g))).
intro. rewrite MapFacts.in_find_iff in H1.
case_eq (VertexMap.find
       (elt:=option NodeLabel *
             (VertexMap.t (option EdgeLabel) * VertexMap.t (option EdgeLabel)))
       x
       (VertexMap.remove
          (elt:=option NodeLabel *
                (VertexMap.t (option EdgeLabel) *
                 VertexMap.t (option EdgeLabel))) v (map g))); intros.
generalize (VertexMap.find_2 H2). clear H2. intro.
generalize (VertexMap.map_1 (remove_neighbor v) H2). intro.
generalize (VertexMap.find_1 H3). clear H3. intro.
rewrite H3 in *. congruence.
congruence.
clear H0. rewrite MapFacts.in_find_iff in H1.
rewrite MapFacts.remove_neq_o in H1.
case_eq (VertexMap.find x (map g)); intros.
rewrite H0 in *. elim H1. congruence.
simpl in *.
rewrite Equal_remove_empty. apply MapFacts.Equal_refl.
auto.
Qed.

Lemma remove_map_succ_eq : forall x v g,
Vertex.eq x v ->
succ x (remove_map (map g) v) = VertexMap.empty (option EdgeLabel).

Proof.
intros.
unfold succ, adj_map.
case_eq (VertexMap.find x (remove_map (map g) v)); intros.
unfold remove_map in H0. generalize (VertexMap.find_2 H0). clear H0. intro.
rewrite MapFacts.map_mapsto_iff in H0. destruct H0. destruct H0.
rewrite MapFacts.remove_mapsto_iff in H1. destruct H1.
elim H1. auto.
simpl. reflexivity.
Qed.

Lemma remove_map_pred_eq : forall x v g,
Vertex.eq x v ->
pred x (remove_map (map g) v) = VertexMap.empty (option EdgeLabel).

Proof.
intros.
unfold pred, adj_map.
case_eq (VertexMap.find x (remove_map (map g) v)); intros.
unfold remove_map in H0. generalize (VertexMap.find_2 H0). clear H0. intro.
rewrite MapFacts.map_mapsto_iff in H0. destruct H0. destruct H0.
rewrite MapFacts.remove_mapsto_iff in H1. destruct H1.
elim H1. auto.
simpl. reflexivity.
Qed.

Lemma pred_succ_remove_vertex : forall g v x y w,
is_labeled_succ y x (remove_map (map g) v) w <->
is_labeled_pred x y (remove_map (map g) v) w.

Proof.
intros.
unfold is_labeled_succ, is_labeled_pred.
destruct (Vertex.eq_dec x v).
rewrite remove_map_succ_eq.
split; intro.
rewrite MapFacts.empty_mapsto_iff in H. inversion H.
unfold pred, adj_map in H.
case_eq (VertexMap.find y (remove_map (map g) v)); intros.
rewrite H0 in H.
unfold remove_map in H0. generalize (VertexMap.find_2 H0). clear H0. intro.
rewrite MapFacts.map_mapsto_iff in H0.
destruct H0. destruct H0.
rewrite MapFacts.remove_mapsto_iff in H1. destruct H1.
rewrite H0 in H.
unfold remove_neighbor in H. destruct x0. destruct p0. simpl in H.
rewrite MapFacts.remove_mapsto_iff in H. destruct H. elim H. auto.
rewrite H0 in H. simpl in H. rewrite MapFacts.empty_mapsto_iff in H. inversion H.
auto.
destruct (Vertex.eq_dec y v).
rewrite remove_map_pred_eq.
split; intro.
unfold succ, adj_map in H.
case_eq (VertexMap.find x (remove_map (map g) v)); intros.
rewrite H0 in H.
unfold remove_map in H0. generalize (VertexMap.find_2 H0). clear H0. intro.
rewrite MapFacts.map_mapsto_iff in H0.
destruct H0. destruct H0.
rewrite MapFacts.remove_mapsto_iff in H1. destruct H1.
rewrite H0 in H.
unfold remove_neighbor in H. destruct x0. destruct p0. simpl in H.
rewrite MapFacts.remove_mapsto_iff in H. destruct H. elim H. auto.
rewrite H0 in H. simpl in H. rewrite MapFacts.empty_mapsto_iff in H. inversion H.
rewrite MapFacts.empty_mapsto_iff in H. inversion H.
auto.

rewrite remove_map_pred. rewrite remove_map_succ.
do 2 rewrite MapFacts.remove_mapsto_iff.
split; intros; destruct H; split.
auto.
fold (is_labeled_pred x y (map g) w). rewrite <-pred_succ.
unfold is_labeled_succ. auto.
auto.
fold (is_labeled_succ y x (map g) w). rewrite pred_succ.
unfold is_labeled_pred. auto.
auto.
auto.
Qed.

Definition remove_vertex v g :=
Make_Graph (remove_map (map g) v)
                     (pred_succ_remove_vertex g v).

Lemma 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).

Proof.
unfold In_graph_labeled_vertex; intros.
split; intros.
destruct H.
destruct x0.
generalize (VertexMap.find_2 H). clear H. intro.
unfold remove_vertex in H. simpl in H. unfold remove_map in H.
rewrite MapFacts.map_mapsto_iff in H. destruct H. destruct H.
rewrite MapFacts.remove_mapsto_iff in H0. destruct H0.
split.
destruct x0. exists p.
unfold remove_neighbor in H. destruct p. inversion H. subst.
apply VertexMap.find_1. auto.
auto.
destruct H. destruct H. destruct x0.
exists (VertexMap.remove r t0, VertexMap.remove r t1).
unfold remove_vertex in *. simpl in *.
case_eq (VertexMap.find x (remove_map (map g) r)); intros.
generalize (VertexMap.find_2 H1). clear H1. intro.
unfold remove_map in H1. rewrite MapFacts.map_mapsto_iff in H1.
destruct H1. destruct H1.
rewrite MapFacts.remove_mapsto_iff in H2. destruct H2.
rewrite H1. unfold remove_neighbor. destruct x0.
destruct p0. generalize (VertexMap.find_2 H). clear H. intro H.
generalize (MapsTo_fun H H3). intro. inversion H4. subst. reflexivity.

unfold remove_map in H1.
assert (~VertexMap.In x (VertexMap.remove r (map g))).
intro. rewrite MapFacts.in_find_iff in H2.
case_eq (VertexMap.find
       (elt:=option NodeLabel *
             (VertexMap.t (option EdgeLabel) * VertexMap.t (option EdgeLabel)))
       x
       (VertexMap.remove
          (elt:=option NodeLabel *
                (VertexMap.t (option EdgeLabel) *
                 VertexMap.t (option EdgeLabel))) r (map g))); intros.
generalize (VertexMap.find_2 H3). clear H3. intro.
generalize (VertexMap.map_1 (remove_neighbor r) H3). intro.
generalize (VertexMap.find_1 H4). clear H4. intro.
rewrite H4 in *. congruence.
congruence.
elim H2. rewrite MapFacts.in_find_iff. rewrite MapFacts.remove_neq_o. congruence.
auto.
Qed.

Lemma 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).

Proof.
unfold In_graph_labeled_edge, is_labeled_succ. intros.
split; intros.
destruct (Vertex.eq_dec (fst_end e) r).
simpl in H. rewrite remove_map_succ_eq in H.
rewrite MapFacts.empty_mapsto_iff in H. inversion H. auto.
simpl in H. rewrite remove_map_succ in H.
rewrite MapFacts.remove_mapsto_iff in H. destruct H.
split.
auto.
unfold incident. intro. destruct H1; [elim n|elim H]; auto.
auto.
destruct H.
simpl. rewrite remove_map_succ. rewrite MapFacts.remove_mapsto_iff. split.
intro. elim H0. right. auto.
auto.
intro. elim H0. left. auto.
Qed.


Definition add_edge_map e (map : maptype) w :=
let v1 := fst_end e in
let v2 := snd_end e in
match VertexMap.find v1 map with
| None => map
| Some wsp1 => match Vertex.eq_dec v1 v2 with
                | left _ => let (w1, sp1) := wsp1 in let (s1,p1) := sp1 in
                                 let succ1 := VertexMap.add v2 w s1 in
                                 let pred1 := VertexMap.add v1 w p1 in
                                 VertexMap.add v1 (w1, (succ1,pred1)) map
                | right _ => match VertexMap.find v2 map with
                             | None => map
                             | Some wsp2 => let (w1, sp1) := wsp1 in let (s1,p1) := sp1 in
                                                         let (w2, sp2) := wsp2 in let (s2,p2) := sp2 in
                                                         let succ1 := VertexMap.add v2 w s1 in
                                                         let pred2 := VertexMap.add v1 w p2 in
                                VertexMap.add v2 (w2,(s2,pred2))
                                            (VertexMap.add v1 (w1,(succ1,p1)) map)
                            end
               end
end.

Lemma add_edge_succ : forall e g w x,
In_ext e g ->
~Vertex.eq x (fst_end e) ->
VertexMap.Equal (succ x (add_edge_map e (map g) w)) (succ x (map g)).

Proof.
unfold add_edge_map, succ, adj_map. intros.
case_eq (VertexMap.find (fst_end e) (map g)); intros.
destruct (Vertex.eq_dec (fst_end e) (snd_end e)).
destruct p. destruct p.
rewrite MapFacts.add_neq_o. simpl.
apply MapFacts.Equal_refl.
auto.
case_eq (VertexMap.find (snd_end e) (map g)); intros.
destruct p. destruct p. destruct p0. destruct p.
destruct (Vertex.eq_dec x (snd_end e)).
rewrite MapFacts.add_eq_o.
rewrite (MapFacts.find_o _ e0). rewrite H2. simpl. apply MapFacts.Equal_refl. auto.
rewrite MapFacts.add_neq_o. rewrite MapFacts.add_neq_o. apply MapFacts.Equal_refl.
auto.
auto.
apply MapFacts.Equal_refl.
apply MapFacts.Equal_refl.
Qed.

Lemma add_edge_succ_fst : forall g e w x,
In_ext e g ->
Vertex.eq x (fst_end e) ->
VertexMap.Equal (succ x (add_edge_map e (map g) w))
                            (VertexMap.add (snd_end e) w (succ x (map g))).

Proof.
unfold add_edge_map, succ, adj_map. intros.
case_eq (VertexMap.find (fst_end e) (map g)); intros.
destruct (Vertex.eq_dec (fst_end e) (snd_end e)).
destruct p. destruct p.
rewrite MapFacts.add_eq_o. simpl.
rewrite (MapFacts.find_o _ H0). rewrite H1. simpl.
apply MapFacts.Equal_refl.
auto.
rewrite (MapFacts.find_o _ H0).
case_eq (VertexMap.find (snd_end e) (map g)); intros.
destruct p. destruct p. destruct p0. destruct p.
rewrite MapFacts.add_neq_o.
rewrite MapFacts.add_eq_o.
rewrite (MapFacts.find_o _ H0). rewrite H1. simpl. apply MapFacts.Equal_refl.
auto.
auto.

unfold In_ext, In_graph_vertex in H.
do 2 rewrite MapFacts.in_find_iff in H. destruct H. congruence.

unfold In_ext, In_graph_vertex in H.
do 2 rewrite MapFacts.in_find_iff in H. destruct H. congruence.
Qed.

Lemma add_edge_succ_notin : forall e g w x,
~In_ext e g ->
VertexMap.Equal (succ x (add_edge_map e (map g) w)) (succ x (map g)).

Proof.
unfold add_edge_map, succ, adj_map. intros.
case_eq (VertexMap.find (fst_end e) (map g)); intros.
destruct (Vertex.eq_dec (fst_end e) (snd_end e)).
elim H. unfold In_ext, In_graph_vertex.
do 2 rewrite MapFacts.in_find_iff. rewrite (MapFacts.find_o _ (Vertex.eq_sym e0)).
rewrite H0. split; congruence.
destruct p. destruct p.
case_eq (VertexMap.find (snd_end e) (map g)); intros.
elim H. unfold In_ext, In_graph_vertex.
do 2 rewrite MapFacts.in_find_iff. split; congruence.
apply MapFacts.Equal_refl.
apply MapFacts.Equal_refl.
Qed.

Lemma add_edge_pred : forall e g w x,
In_ext e g ->
~Vertex.eq x (snd_end e) ->
VertexMap.Equal (pred x (add_edge_map e (map g) w)) (pred x (map g)).

Proof.
unfold add_edge_map, pred, adj_map. intros.
case_eq (VertexMap.find (fst_end e) (map g)); intros.
destruct (Vertex.eq_dec (fst_end e) (snd_end e)).
destruct p. destruct p.
rewrite MapFacts.add_neq_o. simpl.
apply MapFacts.Equal_refl.
auto.
intro. elim H0. rewrite <-e0. auto.
case_eq (VertexMap.find (snd_end e) (map g)); intros.
destruct p. destruct p. destruct p0. destruct p.
rewrite MapFacts.add_neq_o.
destruct (Vertex.eq_dec x (fst_end e)).
rewrite MapFacts.add_eq_o.
rewrite (MapFacts.find_o _ e0). rewrite H1. simpl. apply MapFacts.Equal_refl.
auto.
rewrite MapFacts.add_neq_o. apply MapFacts.Equal_refl.
auto.
auto.
apply MapFacts.Equal_refl.
apply MapFacts.Equal_refl.
Qed.

Lemma add_edge_pred_snd : forall g e w x,
In_ext e g ->
Vertex.eq x (snd_end e) ->
VertexMap.Equal (pred x (add_edge_map e (map g) w))
                            (VertexMap.add (fst_end e) w (pred x (map g))).

Proof.
unfold add_edge_map, pred, adj_map. intros.
case_eq (VertexMap.find (fst_end e) (map g)); intros.
destruct (Vertex.eq_dec (fst_end e) (snd_end e)).
destruct p. destruct p.
rewrite MapFacts.add_eq_o. simpl.
rewrite (MapFacts.find_o _ H0). rewrite (MapFacts.find_o _ (Vertex.eq_sym e0)). simpl.
rewrite H1. simpl. apply MapFacts.Equal_refl.
rewrite e0. auto.
case_eq (VertexMap.find (snd_end e) (map g)); intros.
destruct p. destruct p. destruct p0. destruct p.
rewrite MapFacts.add_eq_o.
rewrite (MapFacts.find_o _ H0). rewrite H2. simpl. apply MapFacts.Equal_refl.
auto.

unfold In_ext, In_graph_vertex in H.
do 2 rewrite MapFacts.in_find_iff in H. destruct H. congruence.

unfold In_ext, In_graph_vertex in H.
do 2 rewrite MapFacts.in_find_iff in H. destruct H. congruence.
Qed.

Lemma add_edge_pred_notin : forall e g w x,
~In_ext e g ->
VertexMap.Equal (pred x (add_edge_map e (map g) w)) (pred x (map g)).

Proof.
unfold add_edge_map, pred, adj_map. intros.
case_eq (VertexMap.find (fst_end e) (map g)); intros.
destruct (Vertex.eq_dec (fst_end e) (snd_end e)).
elim H. unfold In_ext, In_graph_vertex.
do 2 rewrite MapFacts.in_find_iff. rewrite (MapFacts.find_o _ (Vertex.eq_sym e0)).
rewrite H0. split; congruence.
destruct p. destruct p.
case_eq (VertexMap.find (snd_end e) (map g)); intros.
elim H. unfold In_ext, In_graph_vertex.
do 2 rewrite MapFacts.in_find_iff. split; congruence.
apply MapFacts.Equal_refl.
apply MapFacts.Equal_refl.
Qed.

Lemma In_ext_dec : forall e g, {In_ext e g}+{~In_ext e g}.

Proof.
unfold In_ext, In_graph_vertex. intros.
destruct (MapFacts.In_dec (map g) (fst_end e));
destruct (MapFacts.In_dec (map g) (snd_end e)).
left; split; auto.
right. intro. destruct H. elim n. auto.
right. intro. destruct H. elim n. auto.
right. intro. destruct H. elim n. auto.
Qed.

Lemma pred_succ_add_edge : forall g e w' x y w,
is_labeled_succ y x (add_edge_map e (map g) w') w <->
is_labeled_pred x y (add_edge_map e (map g) w') w.

Proof.
unfold is_labeled_succ, is_labeled_pred; intros.
destruct (In_ext_dec e g).
destruct (Vertex.eq_dec x (fst_end e)).
rewrite add_edge_succ_fst.
rewrite MapFacts.add_mapsto_iff.
destruct (Vertex.eq_dec y (snd_end e)).
rewrite add_edge_pred_snd.
rewrite MapFacts.add_mapsto_iff.
split; intros; destruct H; destruct H; subst.
left. split; auto.
right. split. auto.
fold (is_labeled_succ y x (map g) w) in H0. rewrite pred_succ in H0.
unfold is_labeled_pred in H0. auto.
left. split; auto.
elim H. auto.
auto.
auto.
rewrite add_edge_pred.
split; intros.
destruct H; destruct H; subst.
elim n. auto.
fold (is_labeled_succ y x (map g) w) in H0. rewrite pred_succ in H0.
unfold is_labeled_pred in H0. auto.
right. split. auto.
fold (is_labeled_succ y x (map g) w). rewrite pred_succ.
unfold is_labeled_pred. auto.
auto.
auto.
auto.
auto.

rewrite add_edge_succ.
destruct (Vertex.eq_dec y (snd_end e)).
rewrite add_edge_pred_snd.
split; intros.
rewrite MapFacts.add_mapsto_iff.
right. split. auto.
fold (is_labeled_succ y x (map g) w) in H. rewrite pred_succ in H.
unfold is_labeled_pred in H. auto.
rewrite MapFacts.add_mapsto_iff in H.
destruct H; destruct H; subst.
elim n. auto.
fold (is_labeled_succ y x (map g) w). rewrite pred_succ.
unfold is_labeled_pred. auto.
auto.
auto.

rewrite add_edge_pred.
fold (is_labeled_succ y x (map g) w). fold (is_labeled_pred x y (map g) w).
apply pred_succ.
auto.
auto.
auto.
auto.

rewrite add_edge_succ_notin. rewrite add_edge_pred_notin.
fold (is_labeled_succ y x (map g) w). fold (is_labeled_pred x y (map g) w).
apply pred_succ.
auto.
auto.
Qed.

Definition add_edge e g w :=
Make_Graph (add_edge_map e (map g) w)
                     (pred_succ_add_edge g e w).

Lemma 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'.

Proof.
unfold In_graph_labeled_vertex, add_edge. intros. simpl.
unfold add_edge_map.
case_eq (VertexMap.find (fst_end e) (map g)); intros.
destruct (Vertex.eq_dec (fst_end e) (snd_end e)).
destruct p. destruct p.
destruct (Vertex.eq_dec v (fst_end e)).
rewrite MapFacts.add_eq_o.
rewrite (MapFacts.find_o _ e1). rewrite H.
split; intros.
destruct H0. inversion H0. subst. exists (t0,t1). reflexivity.
destruct H0. inversion H0. subst.
exists (VertexMap.add (snd_end e) w t0, VertexMap.add (fst_end e) w t1). reflexivity.
auto.
rewrite MapFacts.add_neq_o. reflexivity.
auto.
case_eq (VertexMap.find (snd_end e) (map g)); intros.
destruct p. destruct p. destruct p0. destruct p.
destruct (Vertex.eq_dec v (snd_end e)).
rewrite MapFacts.add_eq_o.
rewrite (MapFacts.find_o _ e0). rewrite H0.
split; intros.
destruct H1. inversion H1. exists (t2,t3). auto.
destruct H1. inversion H1. exists (t2, VertexMap.add (fst_end e) w t3). auto.
auto.
rewrite MapFacts.add_neq_o.
destruct (Vertex.eq_dec v (fst_end e)).
rewrite MapFacts.add_eq_o.
rewrite (MapFacts.find_o _ e0). rewrite H.
split; intros.
destruct H1. inversion H1. subst. exists (t0,t1). auto.
destruct H1. inversion H1. subst. exists (VertexMap.add (snd_end e) w t0, t1). auto.
auto.
rewrite MapFacts.add_neq_o. reflexivity.
auto.
auto.
reflexivity.
reflexivity.
Qed.

Lemma 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.

Proof.
unfold In_graph_labeled_edge, is_labeled_succ. intros.
simpl. destruct (In_ext_dec e g).
destruct (Vertex.eq_dec (fst_end e') (fst_end e)).
rewrite add_edge_succ_fst. rewrite MapFacts.add_mapsto_iff.
destruct (Vertex.eq_dec (snd_end e) (snd_end e')).
elim H0. split; auto.
right. split; auto.
auto.
auto.
rewrite add_edge_succ; auto.
rewrite add_edge_succ_notin; auto.
Qed.

Lemma 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.

Proof.
intros. unfold In_graph_labeled_edge, is_labeled_succ.
simpl. rewrite add_edge_succ_fst. rewrite MapFacts.add_mapsto_iff.
left. split; auto.
auto.
auto.
Qed.

Lemma 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'.

Proof.
unfold In_graph_labeled_edge, is_labeled_succ in *. intros.
destruct (Vertex.eq_dec (fst_end e') (fst_end e)).
simpl in H0. rewrite add_edge_succ_fst in H0.
rewrite MapFacts.add_mapsto_iff in H0.
destruct H0; destruct H0; subst.
elim H1. split; auto.
auto.
auto.
auto.
simpl in H0. rewrite add_edge_succ in H0.
auto.
auto.
auto.
Qed.

Lemma 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').

Proof.
unfold In_graph_labeled_vertex, add_edge. intros. simpl.
unfold add_edge_map.
case_eq (VertexMap.find (fst_end e) (map g)); intros.
destruct (Vertex.eq_dec (fst_end e) (snd_end e)).
elim H. unfold In_ext, In_graph_vertex. do 2 rewrite MapFacts.in_find_iff.
rewrite (MapFacts.find_o _ (Vertex.eq_sym e0)). rewrite H0. split; congruence.
case_eq (VertexMap.find (snd_end e) (map g)); intros.
elim H. unfold In_ext, In_graph_vertex. do 2 rewrite MapFacts.in_find_iff.
split; congruence.
reflexivity.
reflexivity.
Qed.

Lemma 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').

Proof.
unfold In_graph_labeled_edge, add_edge. intros. simpl.
unfold add_edge_map.
case_eq (VertexMap.find (fst_end e) (map g)); intros.
destruct (Vertex.eq_dec (fst_end e) (snd_end e)).
elim H. unfold In_ext, In_graph_vertex. do 2 rewrite MapFacts.in_find_iff.
rewrite (MapFacts.find_o _ (Vertex.eq_sym e0)). rewrite H0. split; congruence.
case_eq (VertexMap.find (snd_end e) (map g)); intros.
elim H. unfold In_ext, In_graph_vertex. do 2 rewrite MapFacts.in_find_iff.
split; congruence.
reflexivity.
reflexivity.
Qed.

Definition add_edge_w e g w :=
match VertexMap.find (fst_end e) (map g) with
| Some _ => (match VertexMap.find (snd_end e) (map g) with
                 | Some _ => add_edge e g w
                 | None => add_edge e (add_vertex (snd_end e) g None) w
                 end)
| None => (match VertexMap.find (snd_end e) (map g) with
                 | Some _ => add_edge e (add_vertex (fst_end e) g None) w
                 | None => add_edge e (add_vertex (fst_end e) (add_vertex (snd_end e) g None) None) w
                 end)
end.

Lemma 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).

Proof.
unfold add_edge_w; intros.
case_eq (VertexMap.find (fst_end e) (map g));
case_eq (VertexMap.find (snd_end e) (map g)); intros.
rewrite In_graph_add_edge_vertex.
split; intros.
left. auto.
destruct H1. auto.
destruct H1. destruct H2.
elim H3. destruct H1.
unfold In_graph_vertex. rewrite MapFacts.in_find_iff. rewrite (MapFacts.find_o _ H1). congruence.
unfold In_graph_vertex. rewrite MapFacts.in_find_iff. rewrite (MapFacts.find_o _ H1). congruence.
rewrite In_graph_add_edge_vertex. rewrite In_add_vertex.
split; intros.
destruct H1. destruct H1.
destruct H2. right. split. right. auto.
split. auto.
unfold In_graph_vertex. rewrite MapFacts.in_find_iff. rewrite (MapFacts.find_o _ H2).
rewrite H. congruence.
left. auto.
destruct H1.
right. auto.
destruct H1. destruct H2.
left.
unfold In_graph_vertex in *. rewrite MapFacts.in_find_iff in H3.
destruct H1; rewrite (MapFacts.find_o _ H1) in H3.
rewrite H0 in H3. elim H3. congruence.
split.
unfold In_graph_vertex. rewrite MapFacts.in_find_iff. auto.
split; auto.

rewrite In_graph_add_edge_vertex. rewrite In_add_vertex.
split; intros.
destruct H1. destruct H1.
destruct H2. right. split. left. auto.
split. auto.
unfold In_graph_vertex in *. rewrite MapFacts.in_find_iff. rewrite (MapFacts.find_o _ H2).
rewrite H0. congruence.
left. auto.
destruct H1.
right. auto.
destruct H1. destruct H2.
left.
unfold In_graph_vertex in *. rewrite MapFacts.in_find_iff in H3.
destruct H1; rewrite (MapFacts.find_o _ H1) in H3.
split.
unfold In_graph_vertex. rewrite MapFacts.in_find_iff. auto.
split; auto.
rewrite H in H3. elim H3. congruence.

rewrite In_graph_add_edge_vertex. rewrite In_add_vertex. rewrite In_add_vertex.
split; intros.
destruct H1; destruct H1. destruct H2.
right. split.
left. auto.
split. auto.
unfold In_graph_vertex in *. rewrite MapFacts.in_find_iff. rewrite (MapFacts.find_o _ H2). rewrite H0. auto.
destruct H1. destruct H2.
right.
split. right. auto.
split. auto.
unfold In_graph_vertex in *. rewrite MapFacts.in_find_iff. rewrite (MapFacts.find_o _ H2). rewrite H. auto.
left. auto.

destruct H1. right. right. auto.
destruct H1. destruct H2. destruct H1.
destruct (Vertex.eq_dec (fst_end e) (snd_end e)).
right. left. split.
unfold In_graph_vertex in *. rewrite MapFacts.in_find_iff in *.
rewrite (MapFacts.find_o _ H1) in H3. rewrite H. congruence.
split. rewrite H1. auto.
auto.
left. split.
unfold In_graph_vertex. rewrite MapFacts.in_find_iff. simpl.
unfold add_vertex_map. rewrite H. rewrite MapFacts.add_neq_o.
rewrite H0. congruence. auto.
split; auto.

right. left.
split. unfold In_graph_vertex in *. rewrite MapFacts.in_find_iff in *.
rewrite (MapFacts.find_o _ H1) in H3. rewrite H. congruence.
split; 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_add_edge_weak_edge_2 : forall e g w,
In_graph_labeled_edge e (add_edge_w e g w) w.

Proof.
unfold add_edge_w; intros.
case_eq (VertexMap.find (fst_end e) (map g));
case_eq (VertexMap.find (snd_end e) (map g)); intros.
apply In_graph_edge_add_edge_2.
unfold In_ext, In_graph_vertex. do 2 rewrite MapFacts.in_find_iff.
split; congruence.
apply In_graph_edge_add_edge_2.
unfold In_ext, In_graph_vertex. do 2 rewrite MapFacts.in_find_iff.
split; try congruence.
simpl. unfold add_vertex_map. rewrite H.
destruct (Vertex.eq_dec (fst_end e) (snd_end e)).
rewrite MapFacts.add_eq_o. congruence. auto.
rewrite MapFacts.add_neq_o. congruence.
auto.
simpl. unfold add_vertex_map. rewrite H.
rewrite MapFacts.add_eq_o. congruence.
auto.
apply In_graph_edge_add_edge_2.
unfold In_ext, In_graph_vertex. do 2 rewrite MapFacts.in_find_iff.
split; try congruence.
simpl. unfold add_vertex_map. rewrite H0.
rewrite MapFacts.add_eq_o. congruence.
auto.
simpl. unfold add_vertex_map. rewrite H0.
destruct (Vertex.eq_dec (snd_end e) (fst_end e)).
rewrite MapFacts.add_eq_o. congruence.
auto.
rewrite MapFacts.add_neq_o. congruence.
auto.
apply In_graph_edge_add_edge_2.
unfold In_ext, In_graph_vertex. do 2 rewrite MapFacts.in_find_iff.
split; try congruence.
simpl. unfold add_vertex_map. rewrite H.
destruct (Vertex.eq_dec (fst_end e) (snd_end e)).
rewrite MapFacts.add_eq_o. rewrite MapFacts.add_eq_o. congruence.
auto.
auto.
rewrite MapFacts.add_neq_o. rewrite H0.
rewrite MapFacts.add_eq_o. congruence.
auto.
auto.
simpl. unfold add_vertex_map. rewrite H.
destruct (Vertex.eq_dec (snd_end e) (fst_end e)).
rewrite MapFacts.add_eq_o. rewrite MapFacts.add_eq_o. congruence.
auto.
auto.
rewrite MapFacts.add_neq_o. rewrite H0. rewrite MapFacts.add_neq_o.
rewrite MapFacts.add_eq_o. congruence.
auto.
auto.
auto.
Qed.

Lemma 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').

Proof.
split; intros.
destruct (Edge.eq_dec e e').
left. split. auto.
unfold add_edge_w in H.
case_eq (VertexMap.find (fst_end e) (map g)); intros; rewrite H0 in H.
case_eq (VertexMap.find (snd_end e) (map g)); intros; rewrite H1 in H.
assert (In_graph_labeled_edge e (add_edge e g w) w).
apply In_graph_edge_add_edge_2.
split; unfold In_graph_vertex; rewrite MapFacts.in_find_iff; congruence.
rewrite In_graph_labeled_edge_spec in H. rewrite <-e0 in H.
rewrite In_graph_labeled_edge_spec in H2.
apply (EMapFacts.MapsTo_fun H2 H).
assert (In_graph_labeled_edge e (add_edge e (add_vertex (snd_end e) g None) w) w).
apply In_graph_edge_add_edge_2.
split. unfold In_graph_vertex. unfold add_vertex, add_vertex_map. simpl.
rewrite H1. rewrite MapFacts.in_find_iff. rewrite MapFacts.add_neq_o. congruence.
intro. rewrite (find_o _ H2) in H1. congruence.
unfold In_graph_vertex, add_vertex, add_vertex_map. simpl.
rewrite H1. rewrite MapFacts.in_find_iff. rewrite MapFacts.add_eq_o. congruence.
auto.
rewrite In_graph_labeled_edge_spec in H. rewrite In_graph_labeled_edge_spec in H2.
rewrite <-e0 in H. apply (EMapFacts.MapsTo_fun H2 H).
case_eq (VertexMap.find (snd_end e) (map g)); intros; rewrite H1 in H.
assert (In_graph_labeled_edge e (add_edge e (add_vertex (fst_end e) g None) w) w).
apply In_graph_edge_add_edge_2.
split. unfold In_graph_vertex, add_vertex, add_vertex_map. simpl.
rewrite H0. rewrite MapFacts.in_find_iff. rewrite MapFacts.add_eq_o. congruence.
auto.
unfold In_graph_vertex. unfold add_vertex, add_vertex_map. simpl.
rewrite H0. rewrite MapFacts.in_find_iff. rewrite MapFacts.add_neq_o. congruence.
intro. rewrite (find_o _ H2) in H0. congruence.
rewrite In_graph_labeled_edge_spec in H. rewrite In_graph_labeled_edge_spec in H2.
rewrite <-e0 in H. apply (EMapFacts.MapsTo_fun H2 H).
assert (In_graph_labeled_edge e (add_edge e (add_vertex (fst_end e) (add_vertex (snd_end e) g None) None) w) w).
apply In_graph_edge_add_edge_2.
split; unfold In_graph_vertex, add_vertex, add_vertex_map; simpl; rewrite MapFacts.in_find_iff.
rewrite H1.
destruct (Vertex.eq_dec (fst_end e) (snd_end e)).
rewrite MapFacts.add_eq_o;auto. rewrite MapFacts.add_eq_o; auto. congruence.
rewrite MapFacts.add_neq_o; auto. rewrite H0. rewrite MapFacts.add_eq_o; auto. congruence.
rewrite H1.
destruct (Vertex.eq_dec (fst_end e) (snd_end e)).
rewrite MapFacts.add_eq_o;auto. rewrite MapFacts.add_eq_o; auto. congruence.
rewrite MapFacts.add_neq_o; auto. rewrite H0. rewrite MapFacts.add_neq_o; auto.
rewrite MapFacts.add_eq_o; auto. congruence.
rewrite In_graph_labeled_edge_spec in H. rewrite In_graph_labeled_edge_spec in H2.
rewrite <-e0 in H. apply (EMapFacts.MapsTo_fun H2 H).
right. split. auto.
unfold add_edge_w in H.
case_eq (VertexMap.find (fst_end e) (map g));
case_eq (VertexMap.find (snd_end e) (map g)); intros; rewrite H0 in *; rewrite H1 in *.
apply In_graph_add_edge_edge with (e := e) (w := w).
unfold In_ext, In_graph_vertex. do 2 rewrite MapFacts.in_find_iff.
split; congruence.
auto.
auto.
assert (In_graph_labeled_edge e' (add_vertex (snd_end e) g None) w').
apply In_graph_add_edge_edge with (e := e) (w := w).
unfold In_ext, In_graph_vertex. do 2 rewrite MapFacts.in_find_iff.
split.
simpl. unfold add_vertex_map. rewrite H0. rewrite MapFacts.add_neq_o. congruence.
intro. rewrite (MapFacts.find_o _ H2) in H0. congruence.
simpl. unfold add_vertex_map. rewrite H0. rewrite MapFacts.add_eq_o. congruence.
auto.
auto.
auto.
rewrite In_add_vertex_edge in H2. auto.

assert (In_graph_labeled_edge e' (add_vertex (fst_end e) g None) w').
apply In_graph_add_edge_edge with (e := e) (w := w).
unfold In_ext, In_graph_vertex. do 2 rewrite MapFacts.in_find_iff.
split.
simpl. unfold add_vertex_map. rewrite H1. rewrite MapFacts.add_eq_o. congruence.
auto.
simpl. unfold add_vertex_map. rewrite H1. rewrite MapFacts.add_neq_o. congruence.
intro. rewrite (MapFacts.find_o _ H2) in H1. congruence.
auto.
auto.
rewrite In_add_vertex_edge in H2. auto.

assert (In_graph_labeled_edge e' (add_vertex (fst_end e) (add_vertex (snd_end e) g None) None) w').
apply In_graph_add_edge_edge with (e := e) (w := w).
unfold In_ext, In_graph_vertex. do 2 rewrite MapFacts.in_find_iff.
split.
simpl. unfold add_vertex_map. rewrite H0.
destruct (Vertex.eq_dec (fst_end e) (snd_end e)).
rewrite MapFacts.add_eq_o. rewrite MapFacts.add_eq_o. congruence.
auto.
auto.
rewrite MapFacts.add_neq_o. rewrite H1. rewrite MapFacts.add_eq_o. congruence.
auto.
auto.
simpl. unfold add_vertex_map. rewrite H0.
destruct (Vertex.eq_dec (fst_end e) (snd_end e)).
rewrite MapFacts.add_eq_o. rewrite MapFacts.add_eq_o. congruence.
auto.
auto.
rewrite MapFacts.add_neq_o. rewrite H1. rewrite MapFacts.add_neq_o.
rewrite MapFacts.add_eq_o. congruence.
auto.
auto.
auto.
auto.
auto.
rewrite In_add_vertex_edge in H2. rewrite In_add_vertex_edge in H2. auto.

destruct H. destruct H.
rewrite In_graph_labeled_edge_spec. rewrite <-H. rewrite H0.
rewrite <-In_graph_labeled_edge_spec. apply In_graph_add_edge_weak_edge_2.
destruct H.
unfold add_edge_w.
case_eq (VertexMap.find (fst_end e) (map g)); intros.
case_eq (VertexMap.find (snd_end e) (map g)); intros.
apply In_graph_edge_add_edge. auto. auto.
apply In_graph_edge_add_edge.
rewrite In_add_vertex_edge. auto. auto.
case_eq (VertexMap.find (snd_end e) (map g)); intros.
apply In_graph_edge_add_edge. rewrite In_add_vertex_edge. auto. auto.
apply In_graph_edge_add_edge. rewrite In_add_vertex_edge. rewrite In_add_vertex_edge. auto. auto.
Qed.


Definition remove_edge_map e (map : maptype) :=
let v1 := fst_end e in
let v2 := snd_end e in
match VertexMap.find v1 map with
| None => map
| Some wsp1 => match Vertex.eq_dec v1 v2 with
                | left _ => let (w1, sp1) := wsp1 in let (s1,p1) := sp1 in
                                 let succ1 := VertexMap.remove v2 s1 in
                                 let pred1 := VertexMap.remove v1 p1 in
                                 VertexMap.add v1 (w1, (succ1,pred1)) map
                | right _ => match VertexMap.find v2 map with
                             | None => map
                             | Some wsp2 => let (w1, sp1) := wsp1 in let (s1,p1) := sp1 in
                                                         let (w2, sp2) := wsp2 in let (s2,p2) := sp2 in
                                                         let succ1 := VertexMap.remove v2 s1 in
                                                         let pred2 := VertexMap.remove v1 p2 in
                                VertexMap.add v2 (w2,(s2,pred2))
                                            (VertexMap.add v1 (w1,(succ1,p1)) map)
                            end
               end
end.

Lemma succ_remove_edge : forall g e x,
~Vertex.eq x (fst_end e) ->
succ x (remove_edge_map e (map g)) = succ x (map g).

Proof.
unfold remove_edge_map, succ, adj_map; intros.
case_eq (VertexMap.find (fst_end e) (map g)); intros.
destruct (Vertex.eq_dec (fst_end e) (snd_end e)).
destruct p. destruct p.
rewrite MapFacts.add_neq_o. auto.
auto.
case_eq (VertexMap.find (snd_end e) (map g)); intros.
destruct p. destruct p. destruct p0. destruct p.
destruct (Vertex.eq_dec x (snd_end e)).
rewrite MapFacts.add_eq_o.
rewrite (MapFacts.find_o _ e0). rewrite H1. simpl. auto.
auto.
rewrite MapFacts.add_neq_o. rewrite MapFacts.add_neq_o. auto.
auto.
auto.
auto.
auto.
Qed.

Lemma succ_remove_edge_fst : forall g e x,
In_ext e g ->
Vertex.eq x (fst_end e) ->
succ x (remove_edge_map e (map g)) = VertexMap.remove (snd_end e) (succ x (map g)).

Proof.
unfold remove_edge_map, succ, adj_map; intros.
case_eq (VertexMap.find (fst_end e) (map g)); intros.
destruct (Vertex.eq_dec (fst_end e) (snd_end e)).
destruct p. destruct p.
rewrite MapFacts.add_eq_o.
rewrite (MapFacts.find_o _ H0). rewrite H1. auto.
auto.
case_eq (VertexMap.find (snd_end e) (map g)); intros.
destruct p. destruct p. destruct p0. destruct p.
rewrite MapFacts.add_neq_o. rewrite MapFacts.add_eq_o.
rewrite (MapFacts.find_o _ H0). rewrite H1.
auto.
auto.
intro. elim n. rewrite <-H0. auto.

unfold In_ext, In_graph_vertex in H.
do 2 rewrite MapFacts.in_find_iff in H. destruct H. congruence.

unfold In_ext, In_graph_vertex in H.
do 2 rewrite MapFacts.in_find_iff in H. destruct H. congruence.
Qed.

Lemma pred_remove_edge : forall g e x,
~Vertex.eq x (snd_end e) ->
pred x (remove_edge_map e (map g)) = pred x (map g).

Proof.
unfold remove_edge_map, pred, adj_map; intros.
case_eq (VertexMap.find (fst_end e) (map g)); intros.
destruct (Vertex.eq_dec (fst_end e) (snd_end e)).
destruct p. destruct p.
rewrite MapFacts.add_neq_o. auto.
intro. elim H. rewrite <-e0. auto.
case_eq (VertexMap.find (snd_end e) (map g)); intros.
destruct p. destruct p. destruct p0. destruct p.
rewrite MapFacts.add_neq_o.
destruct (Vertex.eq_dec x (fst_end e)).
rewrite MapFacts.add_eq_o.
rewrite (MapFacts.find_o _ e0). rewrite H0. simpl. auto.
auto.
rewrite MapFacts.add_neq_o. auto.
auto.
auto.
auto.
auto.
Qed.

Lemma pred_remove_edge_snd : forall g e x,
In_ext e g ->
Vertex.eq x (snd_end e) ->
pred x (remove_edge_map e (map g)) = VertexMap.remove (fst_end e) (pred x (map g)).

Proof.
unfold remove_edge_map, pred, adj_map; intros.
case_eq (VertexMap.find (fst_end e) (map g)); intros.
destruct (Vertex.eq_dec (fst_end e) (snd_end e)).
destruct p. destruct p.
rewrite MapFacts.add_eq_o.
rewrite (MapFacts.find_o _ H0). rewrite (MapFacts.find_o _ (Vertex.eq_sym e0)).
rewrite H1. auto.
rewrite e0. auto.
case_eq (VertexMap.find (snd_end e) (map g)); intros.
destruct p. destruct p. destruct p0. destruct p.
rewrite MapFacts.add_eq_o. rewrite (MapFacts.find_o _ H0). rewrite H2.
auto.
auto.

unfold In_ext, In_graph_vertex in H.
do 2 rewrite MapFacts.in_find_iff in H. destruct H. congruence.

unfold In_ext, In_graph_vertex in H.
do 2 rewrite MapFacts.in_find_iff in H. destruct H. congruence.
Qed.

Lemma succ_remove_edge_notin : forall g e x,
~In_ext e g ->
succ x (remove_edge_map e (map g)) = succ x (map g).

Proof.
unfold remove_edge_map, succ, adj_map; intros.
case_eq (VertexMap.find (fst_end e) (map g)); intros.
destruct (Vertex.eq_dec (fst_end e) (snd_end e)).
elim H. unfold In_ext, In_graph_vertex. do 2 rewrite MapFacts.in_find_iff.
rewrite (MapFacts.find_o _ (Vertex.eq_sym e0)). split; congruence.
case_eq (VertexMap.find (snd_end e) (map g)); intros.
elim H. unfold In_ext, In_graph_vertex. do 2 rewrite MapFacts.in_find_iff.
split; congruence.
auto.
auto.
Qed.

Lemma pred_remove_edge_notin : forall g e x,
~In_ext e g ->
pred x (remove_edge_map e (map g)) = pred x (map g).

Proof.
unfold remove_edge_map, pred, adj_map; intros.
case_eq (VertexMap.find (fst_end e) (map g)); intros.
destruct (Vertex.eq_dec (fst_end e) (snd_end e)).
elim H. unfold In_ext, In_graph_vertex. do 2 rewrite MapFacts.in_find_iff.
rewrite (MapFacts.find_o _ (Vertex.eq_sym e0)). split; congruence.
case_eq (VertexMap.find (snd_end e) (map g)); intros.
elim H. unfold In_ext, In_graph_vertex. do 2 rewrite MapFacts.in_find_iff.
split; congruence.
auto.
auto.
Qed.

Lemma pred_succ_remove_edge : forall g e x y w,
is_labeled_succ y x (remove_edge_map e (map g)) w <->
is_labeled_pred x y (remove_edge_map e (map g)) w.

Proof.
intros. destruct (In_ext_dec e g).
unfold is_labeled_succ, is_labeled_pred, is_succ. intros.
destruct (Vertex.eq_dec x (fst_end e)).
rewrite succ_remove_edge_fst.
destruct (Vertex.eq_dec y (snd_end e)).
rewrite pred_remove_edge_snd.
rewrite MapFacts.remove_mapsto_iff. rewrite MapFacts.remove_mapsto_iff.
split; intros.
destruct H. elim H. auto.
destruct H. elim H. auto.
auto.
auto.
rewrite pred_remove_edge.
rewrite MapFacts.remove_mapsto_iff.
split; intros.
destruct H.
fold (is_labeled_succ y x (map g) w) in H0. fold (is_labeled_pred x y (map g) w).
apply pred_succ. auto.
split. auto.
fold (is_labeled_succ y x (map g) w). fold (is_labeled_pred x y (map g) w) in H.
apply pred_succ. auto.
auto.
auto.
auto.
rewrite succ_remove_edge.
destruct (Vertex.eq_dec y (snd_end e)).
rewrite pred_remove_edge_snd.
rewrite MapFacts.remove_mapsto_iff.
split; intros.
split. auto.
fold (is_labeled_succ y x (map g) w) in H. fold (is_labeled_pred x y (map g) w).
apply pred_succ. auto.
destruct H.
fold (is_labeled_succ y x (map g) w). fold (is_labeled_pred x y (map g) w) in H0.
apply pred_succ. auto. auto.
auto.
rewrite pred_remove_edge.
fold (is_labeled_succ y x (map g) w). fold (is_labeled_pred x y (map g) w).
apply pred_succ.
auto.
auto.

unfold is_labeled_succ, is_labeled_pred.
rewrite succ_remove_edge_notin. rewrite pred_remove_edge_notin.
fold (is_labeled_succ y x (map g) w). fold (is_labeled_pred x y (map g) w).
apply pred_succ.
auto.
auto.
Qed.

Definition remove_edge e g :=
Make_Graph (remove_edge_map e (map g))
                     (pred_succ_remove_edge g e).

Lemma 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).

Proof.
unfold In_graph_labeled_vertex. simpl. intros.
unfold remove_edge_map. case_eq (VertexMap.find (fst_end e) (map g)); intros.
destruct (Vertex.eq_dec (fst_end e) (snd_end e)).
destruct p. destruct p.
destruct (Vertex.eq_dec v (fst_end e)).
rewrite MapFacts.add_eq_o.
rewrite (MapFacts.find_o _ e1). rewrite H.
split; intros.
destruct H0. inversion H0. subst. exists (t0,t1). auto.
destruct H0. inversion H0. subst.
exists (VertexMap.remove (snd_end e) t0, VertexMap.remove (fst_end e) t1). auto.
auto.
rewrite MapFacts.add_neq_o. reflexivity.
auto.
case_eq (VertexMap.find (snd_end e) (map g)); intros.
destruct p. destruct p. destruct p0. destruct p.
destruct (Vertex.eq_dec v (snd_end e)).
rewrite MapFacts.add_eq_o.
rewrite (MapFacts.find_o _ e0). rewrite H0.
split; intros.
destruct H1. inversion H1. subst. exists (t2,t3). auto.
destruct H1. inversion H1. subst. exists (t2,VertexMap.remove (fst_end e) t3). auto.
auto.
rewrite MapFacts.add_neq_o.
destruct (Vertex.eq_dec v (fst_end e)).
rewrite MapFacts.add_eq_o.
rewrite (MapFacts.find_o _ e0). rewrite H.
split; intros.
destruct H1. inversion H1. subst. exists (t0,t1). auto.
destruct H1. inversion H1. subst. exists (VertexMap.remove (snd_end e) t0,t1). auto.
auto.
rewrite MapFacts.add_neq_o. reflexivity.
auto.
auto.
reflexivity.
reflexivity.
Qed.

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

Proof.
unfold successors. intros. simpl.
destruct (In_ext_dec e g).
rewrite succ_remove_edge_fst.
apply VertexMap.remove_1. auto.
auto.
auto.
rewrite succ_remove_edge_notin.
intro. elim n.
split.
unfold In_graph_vertex, succ, adj_map in *. rewrite MapFacts.in_find_iff.
case_eq (VertexMap.find (fst_end e) (map g)); intros; rewrite H0 in H.
congruence.
simpl in H. rewrite MapFacts.empty_in_iff in H. inversion H.
fold (is_succ (snd_end e) (fst_end e) (map g)) in H. rewrite unw_pred_succ in H.
unfold In_graph_vertex, is_pred, pred, adj_map in *. rewrite MapFacts.in_find_iff.
case_eq (VertexMap.find (snd_end e) (map g)); intros; rewrite H0 in H.
congruence.
simpl in H. rewrite MapFacts.empty_in_iff in H. inversion H.
auto.
Qed.

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

Proof.
unfold predecessors. intros. simpl.
destruct (In_ext_dec e g).
rewrite pred_remove_edge_snd.
apply VertexMap.remove_1. auto.
auto.
auto.
rewrite pred_remove_edge_notin.
intro. elim n.
split.
fold (is_pred (fst_end e) (snd_end e) (map g)) in H. rewrite <-unw_pred_succ in H.
unfold In_graph_vertex, is_succ, succ, adj_map in *. rewrite MapFacts.in_find_iff.
case_eq (VertexMap.find (fst_end e) (map g)); intros; rewrite H0 in H.
congruence.
simpl in H. rewrite MapFacts.empty_in_iff in H. inversion H.
unfold In_graph_vertex, pred, adj_map in *. rewrite MapFacts.in_find_iff.
case_eq (VertexMap.find (snd_end e) (map g)); intros; rewrite H0 in H.
congruence.
simpl in H. rewrite MapFacts.empty_in_iff in H. inversion H.
auto.
Qed.

End Directed_GraphMap.