Library UndigraphMapImp

Require Import FMaps.
Require Import FSets.
Require Import UndigraphInterface.
Require Import Constructive_UndigraphInterface.
Require Import FMapAVL.
Require Import Directed_edges.
Require Import MapFacts.
Require Import Labels.

Module Undirected_GraphMap (Vertex : OrderedType) (Lab : Labels)
       <: Undirected_Graph Vertex Lab
       <: Constructive_Undirected_Graph Vertex Lab.

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

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

Definition adj x m := snd (adj_map x m).

Definition succ := adj.
Definition pred := adj.

Definition is_adj y x m := VertexMap.In y (adj x m).

Definition is_labeled_adj y x m w := VertexMap.MapsTo y w (adj x m).

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

adjacency : forall x y w, is_labeled_adj y x map w <-> is_labeled_adj x y map w
}.

Definition adjacent v g := adj v (map g).

Definition successors v g := adjacent v g.
Definition predecessors v g := adjacent v g.

Lemma Mapsto_In : forall (A : Type) v (m : VertexMap.t A),
VertexMap.In v m <-> exists x, VertexMap.MapsTo v x m.

Proof.
intros. rewrite MapFacts.in_find_iff.
case_eq (VertexMap.find v m); intros.
split; intros.
exists a. rewrite MapFacts.find_mapsto_iff. auto.
congruence.
split; intros.
congruence.
destruct H0. rewrite MapFacts.find_mapsto_iff in H0. congruence.
Qed.

Lemma EMapsto_In : forall (A : Type) v (m : EdgeMap.t A),
EdgeMap.In v m <-> exists x, EdgeMap.MapsTo v x m.

Proof.
intros. rewrite EMapFacts.in_find_iff.
case_eq (EdgeMap.find v m); intros.
split; intros.
exists a. rewrite EMapFacts.find_mapsto_iff. auto.
congruence.
split; intros.
congruence.
destruct H0. rewrite EMapFacts.find_mapsto_iff in H0. congruence.
Qed.

Lemma unw_adjacency : forall g x y, is_adj y x (map g) <-> is_adj x y (map g).

Proof.
intros. generalize (adjacency g); intro.
unfold is_labeled_adj, is_labeled_adj, is_adj, is_adj 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))
                                               (s : EdgeMap.t (option EdgeLabel)) :=
let (w,sp) := wsp in (VertexMap.fold (fun y v s' => EdgeMap.add (x,y) v s') sp 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) (adjacent (fst_end e) g).

Definition link g v1 v2 := VertexMap.find v2 (adjacent 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)) => 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)) => 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_adj (snd_end e) (fst_end e) (map g).

Definition In_graph_labeled_edge e g w :=
is_labeled_adj (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)) => 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 t0.
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 (snd wsp))).

Proof.
unfold add_neighborhood; intros x wsp s v a b HH.
destruct wsp. 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. 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 (snd wsp)) /\ EdgeMap.MapsTo (a,b) v s)
 \/ VertexMap.MapsTo b v (snd wsp)).

Proof.
unfold add_neighborhood; intros x wsp s v a b.
destruct wsp. 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))))
                               a (VertexMap.elements (map g)) ->
            snd (snd a) = adj (fst a) (map g)) as HH.
intros. destruct a.
generalize (VertexMap.elements_2 H). simpl. intro.
unfold adj, 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_adj, adj, 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)))) =>
      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_adj in *. simpl.
unfold adj, 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 EMapsto_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)))) =>
      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_adj 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_adj in *. simpl.
rewrite HH in H0.
unfold adj, 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 EMapsto_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, adjacent.
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_adj in H.
apply (VertexMap.find_1 H).
unfold edge_label.
case_eq (VertexMap.find (snd_end e) (adj (fst_end e) (map g))); intros.
generalize (VertexMap.find_2 H0). intro.
fold (is_labeled_adj (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 EMapsto_In. unfold In_graph_edge, is_adj.
split; intros.
generalize (In_MapsTo _ _ _ H). intro. destruct H0.
exists x. rewrite <-In_graph_labeled_edge_spec.
unfold In_graph_labeled_edge, is_labeled_adj. auto.
destruct H. rewrite Mapsto_In. exists x.
rewrite <-In_graph_labeled_edge_spec in H.
unfold In_graph_labeled_edge, is_labeled_adj 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, adjacent, In_graph_labeled_edge, is_labeled_adj,
           adj, 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, adjacent. fold (is_labeled_adj v1 v2 (map g) l).
rewrite <-adjacency. fold (In_graph_labeled_edge (v1,v2) g l).
assert (is_labeled_adj 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.


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_adj, adj, 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_adjacency in H.
unfold is_adj, adj, 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 empty_map : maptype :=
VertexMap.empty (option NodeLabel* VertexMap.t (option EdgeLabel)).

Lemma adjacency_empty : forall x y w,
is_labeled_adj y x empty_map w <-> is_labeled_adj x y empty_map w.

Proof.
intros. unfold is_labeled_adj. do 2 rewrite MapFacts.empty_mapsto_iff. reflexivity.
Qed.

Definition empty_graph := Make_Graph empty_map (adjacency_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.



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) m
| Some _ => m
end.

Lemma adjacency_add_vertex : forall g v w x y w',
is_labeled_adj y x (add_vertex_map (map g) v w) w' <-> is_labeled_adj 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 adjacency.
unfold is_labeled_adj, adj, adj_map.
destruct (Vertex.eq_dec x v).
rewrite MapFacts.add_eq_o. simpl.
unfold is_labeled_adj, adj, 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_adj x y (map g) w').
unfold is_labeled_adj, adj, adj_map.
rewrite H0. assumption.
rewrite <-adjacency in H2.
unfold is_labeled_adj, adj, 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_adj, adj, 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_adj y x (map g) w').
unfold is_labeled_adj, adj, adj_map.
rewrite H0. assumption.
rewrite adjacency in H2.
unfold is_labeled_adj, adj, 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 adjacency.
auto.
auto.
Qed.

Definition add_vertex v g w :=
Make_Graph (add_vertex_map (map g) v w)
                     (adjacency_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)).
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_adj, adj, 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_adj, adj, 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)))
                                              :=
let (w,sp) := wsp in (w, VertexMap.remove x sp).

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,
remove_neighbor v wsp = (w,s) ->
~VertexMap.In v s.

Proof.
intros.
unfold remove_neighbor. destruct wsp. simpl in *.
inversion H. subst.
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_adj : forall x v g,
~Vertex.eq x v ->
VertexMap.Equal (adj x (remove_map (map g) v))
                            (VertexMap.remove v (adj x (map g))).

Proof.
unfold adj; 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. 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)))
       x
       (VertexMap.remove
          (elt:=option NodeLabel *
                (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_adj_eq : forall x v g,
Vertex.eq x v ->
adj x (remove_map (map g) v) = VertexMap.empty (option EdgeLabel).

Proof.
intros.
unfold adj, 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 adjacency_remove_vertex : forall g v x y w,
is_labeled_adj y x (remove_map (map g) v) w <->
is_labeled_adj x y (remove_map (map g) v) w.

Proof.
intros.
unfold is_labeled_adj.
destruct (Vertex.eq_dec x v).
rewrite remove_map_adj_eq.
split; intro.
rewrite MapFacts.empty_mapsto_iff in H. inversion H.
unfold adj, 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. 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_adj_eq y v g).
split; intro.
unfold adj, 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. 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_adj. rewrite remove_map_adj.
do 2 rewrite MapFacts.remove_mapsto_iff.
split; intros; destruct H; split.
auto.
fold (is_labeled_adj x y (map g) w). rewrite <-adjacency.
unfold is_labeled_adj. auto.
auto.
fold (is_labeled_adj y x (map g) w). rewrite adjacency.
unfold is_labeled_adj. auto.
auto.
auto.
Qed.

Definition remove_vertex v g :=
Make_Graph (remove_map (map g) v)
                     (adjacency_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.
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.
unfold remove_neighbor in H. destruct x1. inversion H. subst.
exists t0. apply VertexMap.find_1. auto.
auto.
destruct H. destruct H.
exists (VertexMap.remove r x0).
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.
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)))
       x
       (VertexMap.remove
          (elt:=option NodeLabel *
                (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_adj. intros.
split; intros.
destruct (Vertex.eq_dec (fst_end e) r).
simpl in H. rewrite remove_map_adj_eq in H.
rewrite MapFacts.empty_mapsto_iff in H. inversion H. auto.
simpl in H. rewrite remove_map_adj 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_adj. 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 adj1 := VertexMap.add v2 w sp1 in
                                 VertexMap.add v1 (w1, adj1) map
                | right _ => match VertexMap.find v2 map with
                             | None => map
                             | Some wsp2 => let (w1, sp1) := wsp1 in
                                                         let (w2, sp2) := wsp2 in
                                                         let adj1 := VertexMap.add v2 w sp1 in
                                                         let adj2 := VertexMap.add v1 w sp2 in
                                VertexMap.add v2 (w2,adj2)
                                            (VertexMap.add v1 (w1,adj1) map)
                            end
               end
end.

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

Proof.
unfold add_edge_map, adj, 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.
rewrite MapFacts.add_neq_o. simpl.
apply MapFacts.Equal_refl.
auto.
case_eq (VertexMap.find (snd_end e) (map g)); intros.
destruct p. destruct p0.
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_adj_fst : forall g e w x,
In_ext e g ->
Vertex.eq x (fst_end e) ->
VertexMap.Equal (adj x (add_edge_map e (map g) w))
                            (VertexMap.add (snd_end e) w (adj x (map g))).

Proof.
unfold add_edge_map, adj, 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.
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 p0.
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_adj_notin : forall e g w x,
~In_ext e g ->
VertexMap.Equal (adj x (add_edge_map e (map g) w)) (adj x (map g)).

Proof.
unfold add_edge_map, adj, 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.
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_adj_snd : forall g e w x,
In_ext e g ->
Vertex.eq x (snd_end e) ->
VertexMap.Equal (adj x (add_edge_map e (map g) w))
                            (VertexMap.add (fst_end e) w (adj x (map g))).

Proof.
unfold add_edge_map, adj, 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.
rewrite MapFacts.add_eq_o. simpl.
rewrite (MapFacts.find_o _ H0). rewrite (MapFacts.find_o _ (Vertex.eq_sym e0)). rewrite H1. simpl.
apply MapFacts.add_m; auto. apply MapFacts.Equal_refl.
rewrite H0. auto.
case_eq (VertexMap.find (snd_end e) (map g)); intros.
destruct p. destruct p0.
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 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 adjacency_add_edge : forall g e w' x y w,
is_labeled_adj y x (add_edge_map e (map g) w') w <->
is_labeled_adj x y (add_edge_map e (map g) w') w.

Proof.
unfold is_labeled_adj, is_labeled_adj; intros.
destruct (In_ext_dec e g).
destruct (Vertex.eq_dec x (fst_end e)).
rewrite add_edge_adj_fst with (x:=x).
rewrite MapFacts.add_mapsto_iff.
destruct (Vertex.eq_dec y (fst_end e)).
rewrite add_edge_adj_fst.
rewrite MapFacts.add_mapsto_iff.
split; intros.
destruct H. destruct H. left. split. rewrite H. rewrite e0. auto. auto.
destruct H. right. split. intro. elim H. rewrite H1. rewrite e0. auto.
apply adjacency. auto.
destruct H. destruct H. left. split. rewrite H. rewrite e0. auto. auto.
destruct H. right. split. intro. elim H. rewrite H1. rewrite e0. auto.
apply adjacency. auto.
auto.
auto.
destruct (Vertex.eq_dec y (snd_end e)).
rewrite add_edge_adj_snd. rewrite MapFacts.add_mapsto_iff.
split; intros.
destruct H. destruct H. left. split. auto. auto.
destruct H. elim H. auto.
destruct H. destruct H. left. split. auto. auto.
destruct H. elim H. auto.
auto.
auto.
rewrite add_edge_adj.
split; intros.
destruct H. destruct H. elim n0. auto. destruct H. apply adjacency. auto.
right. split. auto. apply adjacency. auto.
auto.
auto.
auto.
auto.
auto.

destruct (Vertex.eq_dec x (snd_end e)).
rewrite add_edge_adj_snd with (x:=x).
rewrite MapFacts.add_mapsto_iff.
destruct (Vertex.eq_dec y (fst_end e)).
rewrite add_edge_adj_fst.
rewrite MapFacts.add_mapsto_iff.
split; intros.
destruct H. destruct H. left. split. auto. auto.
destruct H. elim H. auto.
destruct H. destruct H. left. split. auto. auto.
destruct H. elim H. auto.
auto.
auto.
destruct (Vertex.eq_dec y (snd_end e)).
rewrite add_edge_adj_snd. rewrite MapFacts.add_mapsto_iff.
split; intros.
destruct H. destruct H. elim n0. auto.
destruct H. right. split. auto. apply adjacency. auto.
destruct H. destruct H. elim n. auto.
destruct H. right. split. auto. apply adjacency. auto.
auto.
auto.
rewrite add_edge_adj.
split; intros.
destruct H. destruct H. elim n0. auto.
destruct H. apply adjacency. auto.
right. split. auto. apply adjacency. auto.
auto.
auto.
auto.
auto.
auto.

rewrite add_edge_adj.
destruct (Vertex.eq_dec y (fst_end e)).
rewrite add_edge_adj_fst.
rewrite MapFacts.add_mapsto_iff.
split; intros.
right. split. auto. apply adjacency. auto.
destruct H. destruct H. elim n0. auto.
destruct H. apply adjacency. auto.
auto.
auto.
destruct (Vertex.eq_dec y (snd_end e)).
rewrite add_edge_adj_snd. rewrite MapFacts.add_mapsto_iff.
split; intros.
right. split. auto. apply adjacency. auto.
destruct H. destruct H. elim n. auto.
destruct H. apply adjacency. auto.
auto.
auto.
rewrite add_edge_adj.
apply adjacency.
auto.
auto.
auto.
auto.
auto.
auto.

rewrite add_edge_adj_notin. rewrite add_edge_adj_notin. apply adjacency.
auto.
auto.
Qed.

Definition add_edge e g w :=
Make_Graph (add_edge_map e (map g) w)
                     (adjacency_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 (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). reflexivity.
destruct H0. inversion H0. subst.
exists (VertexMap.add (snd_end e) w x). reflexivity.
auto.
rewrite MapFacts.add_neq_o. reflexivity.
auto.
case_eq (VertexMap.find (snd_end e) (map g)); intros.
destruct p. destruct p0.
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 t1. auto.
destruct H1. inversion H1. exists (VertexMap.add (fst_end e) w x). 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). auto.
destruct H1. inversion H1. subst. exists (VertexMap.add (snd_end e) w x). 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' ->
~Edge.eq (permute e) e' ->
In_graph_labeled_edge e' (add_edge e g w') w.

Proof.
unfold In_graph_labeled_edge, is_labeled_adj. intros.
simpl. destruct (In_ext_dec e g).
destruct (Vertex.eq_dec (fst_end e') (fst_end e)).
rewrite add_edge_adj_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.
destruct (Vertex.eq_dec (fst_end e') (snd_end e)).
rewrite add_edge_adj_snd. rewrite MapFacts.add_mapsto_iff.
destruct (Vertex.eq_dec (fst_end e) (snd_end e')).
elim H1. destruct e. simpl. reduce_edge. split; auto.
right. split; auto.
auto.
auto.
rewrite add_edge_adj; auto.
rewrite add_edge_adj_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_adj.
simpl. rewrite add_edge_adj_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' ->
~Edge.eq (permute e) e' ->
In_graph_labeled_edge e' g w'.

Proof.
unfold In_graph_labeled_edge, is_labeled_adj in *. intros.
destruct (Vertex.eq_dec (fst_end e') (fst_end e)).
simpl in H0. rewrite add_edge_adj_fst in H0.
rewrite MapFacts.add_mapsto_iff in H0.
destruct H0; destruct H0; subst.
elim H1. split; auto.
auto.
auto.
auto.
destruct (Vertex.eq_dec (fst_end e') (snd_end e)).
simpl in H0. rewrite add_edge_adj_snd in H0.
rewrite MapFacts.add_mapsto_iff in H0.
destruct H0; destruct H0; subst.
elim H2. destruct e. reduce_edge. simpl. split; auto.
auto.
auto.
auto.
simpl in H0. rewrite add_edge_adj in H0.
auto.
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 permute_edge_in : forall e g w,
In_graph_labeled_edge e g w <-> In_graph_labeled_edge (permute e) g w.

Proof.
unfold In_graph_labeled_edge. intros.
unfold permute. destruct e. simpl. apply adjacency.
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' \/ eq (permute e) e') /\ w = w') \/ (~eq e e' /\ ~eq (permute 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).

destruct (Edge.eq_dec (permute e) e').
left. split. right. 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 (permute e) (add_edge e g w) w).
rewrite <-permute_edge_in. 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 permute_edge_in in H2.
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 (permute e) (add_edge e (add_vertex (fst_end e) g None) w) w).
rewrite <-permute_edge_in. 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 permute_edge_in in H2.
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.
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.
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.
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.
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.
auto.
rewrite In_add_vertex_edge in H2. rewrite In_add_vertex_edge in H2. auto.

destruct H. 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.
rewrite In_graph_labeled_edge_spec. rewrite <-H. rewrite H0.
rewrite <-In_graph_labeled_edge_spec. rewrite <-permute_edge_in. apply In_graph_add_edge_weak_edge_2.
destruct H. destruct H0.
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.
apply In_graph_edge_add_edge.
rewrite In_add_vertex_edge. auto. 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. auto.
apply In_graph_edge_add_edge. rewrite In_add_vertex_edge. rewrite In_add_vertex_edge. auto. 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 adj1 := VertexMap.remove v2 sp1 in
                                 VertexMap.add v1 (w1, adj1) map
                | right _ => match VertexMap.find v2 map with
                             | None => map
                             | Some wsp2 => let (w1, sp1) := wsp1 in
                                                         let (w2, sp2) := wsp2 in
                                                         let adj1 := VertexMap.remove v2 sp1 in
                                                         let adj2 := VertexMap.remove v1 sp2 in
                                VertexMap.add v2 (w2,adj2)
                                            (VertexMap.add v1 (w1,adj1) map)
                            end
               end
end.

Lemma adj_remove_edge : forall g e x,
~Vertex.eq x (fst_end e) ->
~Vertex.eq x (snd_end e) ->
adj x (remove_edge_map e (map g)) = adj x (map g).

Proof.
unfold remove_edge_map, adj, 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.
rewrite MapFacts.add_neq_o. auto.
auto.
case_eq (VertexMap.find (snd_end e) (map g)); intros.
destruct p. destruct p0.
rewrite MapFacts.add_neq_o. rewrite MapFacts.add_neq_o. auto.
auto.
auto.
auto.
auto.
Qed.

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

Proof.
unfold remove_edge_map, adj, 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.
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 p0.
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 adj_remove_edge_snd : forall g e x,
In_ext e g ->
Vertex.eq x (snd_end e) ->
VertexMap.Equal (adj x (remove_edge_map e (map g)))
                            (VertexMap.remove (fst_end e) (adj x (map g))).

Proof.
unfold remove_edge_map, adj, 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.
rewrite MapFacts.add_eq_o.
rewrite (MapFacts.find_o _ H0). rewrite (MapFacts.find_o _ (Vertex.eq_sym e0)).
rewrite H1. simpl.
rewrite e0. apply MapFacts.Equal_refl.
rewrite H0. auto.
rewrite H0. auto.
case_eq (VertexMap.find (snd_end e) (map g)); intros.
destruct p. destruct p0.
rewrite MapFacts.add_eq_o. simpl.
apply MapFacts.Equal_refl.
auto.
rewrite H2. simpl. rewrite Equal_remove_empty. apply MapFacts.Equal_refl.

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

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

Proof.
unfold remove_edge_map, adj, 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 adjacency_remove_edge : forall g e x y w,
is_labeled_adj y x (remove_edge_map e (map g)) w <->
is_labeled_adj x y (remove_edge_map e (map g)) w.

Proof.
intros. destruct (In_ext_dec e g).
unfold is_labeled_adj, is_labeled_adj, is_adj. intros.
destruct (Vertex.eq_dec x (fst_end e)).
rewrite adj_remove_edge_fst. rewrite MapFacts.remove_mapsto_iff.
destruct (Vertex.eq_dec y (fst_end e)).
rewrite adj_remove_edge_fst. rewrite MapFacts.remove_mapsto_iff.
split; intros.
destruct H. split. intro. elim H. rewrite H1. rewrite e0. auto. apply adjacency. auto.
destruct H. split. intro. elim H. rewrite H1. rewrite e0. auto. apply adjacency. auto.
auto.
auto.
destruct (Vertex.eq_dec y (snd_end e)).
rewrite adj_remove_edge_snd. rewrite MapFacts.remove_mapsto_iff.
split; intros.
destruct H. elim H. auto.
destruct H. elim H. auto.
auto.
auto.
rewrite adj_remove_edge.
split; intros.
destruct H. apply adjacency. auto.
split. auto. apply adjacency. auto.
auto.
auto.
auto.
auto.
destruct (Vertex.eq_dec x (snd_end e)).
rewrite adj_remove_edge_snd. rewrite MapFacts.remove_mapsto_iff.
destruct (Vertex.eq_dec y (fst_end e)).
rewrite adj_remove_edge_fst. rewrite MapFacts.remove_mapsto_iff.
split; intros.
destruct H. elim H. auto.
destruct H. elim H. auto.
auto.
auto.
destruct (Vertex.eq_dec y (snd_end e)).
rewrite adj_remove_edge_snd. rewrite MapFacts.remove_mapsto_iff.
split; intros.
destruct H. split. auto. apply adjacency. auto.
destruct H. split. auto. apply adjacency. auto.
auto.
auto.
rewrite adj_remove_edge.
split; intros.
destruct H. apply adjacency. auto.
split. auto. apply adjacency. auto.
auto.
auto.
auto.
auto.

rewrite adj_remove_edge.
destruct (Vertex.eq_dec y (fst_end e)).
rewrite adj_remove_edge_fst. rewrite MapFacts.remove_mapsto_iff.
split; intros.
split. auto. apply adjacency. auto.
destruct H. apply adjacency. auto.
auto.
auto.
destruct (Vertex.eq_dec y (snd_end e)).
rewrite adj_remove_edge_snd. rewrite MapFacts.remove_mapsto_iff.
split; intros.
split. auto. apply adjacency. auto.
destruct H. apply adjacency. auto.
auto.
auto.
rewrite adj_remove_edge.
split; intros.
apply adjacency. auto.
apply adjacency. auto.
auto.
auto.
auto.
auto.

unfold is_labeled_adj.
rewrite adj_remove_edge_notin. rewrite adj_remove_edge_notin.
apply adjacency.
auto.
auto.
Qed.

Definition remove_edge e g :=
Make_Graph (remove_edge_map e (map g))
                     (adjacency_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 (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). auto.
destruct H0. inversion H0. subst.
exists (VertexMap.remove (snd_end e) x). auto.
auto.
rewrite MapFacts.add_neq_o. reflexivity.
auto.
case_eq (VertexMap.find (snd_end e) (map g)); intros.
destruct p. destruct p0.
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 (t1). auto.
destruct H1. inversion H1. subst. exists (VertexMap.remove (fst_end e) x). 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). auto.
destruct H1. inversion H1. subst. exists (VertexMap.remove (snd_end e) x). 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, adjacent. intros. simpl.
destruct (In_ext_dec e g).
rewrite adj_remove_edge_fst.
apply VertexMap.remove_1. auto.
auto.
auto.
rewrite adj_remove_edge_notin.
intro. elim n.
split.
unfold In_graph_vertex, adj, 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_adj (snd_end e) (fst_end e) (map g)) in H. rewrite unw_adjacency in H.
unfold In_graph_vertex, is_adj, adj, 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, adjacent. intros. simpl.
destruct (In_ext_dec e g).
rewrite adj_remove_edge_snd.
apply VertexMap.remove_1. auto.
auto.
auto.
rewrite adj_remove_edge_notin.
intro. elim n.
split.
fold (is_adj (fst_end e) (snd_end e) (map g)) in H. rewrite <-unw_adjacency in H.
unfold In_graph_vertex, is_adj, adj, 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, adj, 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 Undirected_GraphMap.