Library Unlabeled_spec
Require Import Constructive_DigraphInterface.
Require Import Constructive_UndigraphInterface.
Require Import OrderedType.
Require Import Graph_Properties.
Require Import Labels.
Module UDSpec (Vertex : OrderedType) (Lab : Labels)
(G : Constructive_Directed_Graph Vertex Lab).
Module Import Props := GraphProps Vertex Lab G.
Import G Edge.
Lemma In_remove_vertex_u : forall x r g,
In_graph_vertex x (remove_vertex r g) <->
In_graph_vertex x g /\ ~Vertex.eq x r.
Proof.
intros.
split; intros.
destruct (In_graph_vertex_strong _ _ H).
generalize (In_remove_vertex x r g x0). intro. rewrite H1 in H0.
destruct H0. split. apply In_graph_labeled_vertex_weak with (val := x0). auto. auto.
destruct H. destruct (In_graph_vertex_strong x g H).
apply In_graph_labeled_vertex_weak with (val := x0).
rewrite In_remove_vertex. split; auto.
Qed.
Lemma In_remove_edge_u : forall e r g,
In_graph_edge e (remove_vertex r g) <->
(In_graph_edge e g /\ ~incident e r).
Proof.
intros.
split; intros.
destruct (In_graph_edge_strong _ _ H).
generalize (In_remove_edge e r g x). intro. rewrite H1 in H0.
destruct H0. split. apply In_graph_labeled_edge_weak with (val := x). auto. auto.
destruct H. destruct (In_graph_edge_strong e g H).
apply In_graph_labeled_edge_weak with (val := x).
rewrite In_remove_edge. split; auto.
Qed.
Lemma In_add_vertex_u : forall v g x w,
In_graph_vertex x (add_vertex v g w) <->
Vertex.eq x v \/ In_graph_vertex x g.
Proof.
intros.
split; intros.
destruct (In_graph_vertex_strong _ _ H).
generalize (In_add_vertex v g x w x0). intro. rewrite H1 in H0.
destruct H0.
left. intuition.
right. apply In_graph_labeled_vertex_weak with (val := x0). auto.
destruct H.
destruct (In_graph_vertex_dec x g).
destruct (In_graph_vertex_strong x g). auto.
apply In_graph_labeled_vertex_weak with (val := x0).
rewrite In_add_vertex. right. auto.
apply In_graph_labeled_vertex_weak with (val := w).
rewrite In_add_vertex. left. split; [|split]; auto.
rewrite H in n. auto.
destruct (In_graph_vertex_strong x g). auto.
apply In_graph_labeled_vertex_weak with (val := x0).
rewrite In_add_vertex. right. auto.
Qed.
Lemma In_add_vertex_edge_u : forall v g e w,
In_graph_edge e (add_vertex v g w) <-> In_graph_edge e g.
Proof.
intros. split; intros.
destruct (In_graph_edge_strong _ _ H).
rewrite In_add_vertex_edge in H0.
apply In_graph_labeled_edge_weak with (val := x). auto.
destruct (In_graph_edge_strong _ _ H).
apply In_graph_labeled_edge_weak with (val := x).
rewrite In_add_vertex_edge. auto.
Qed.
Lemma In_graph_add_edge_vertex_u : forall v g e w,
In_graph_vertex v (add_edge e g w) <-> In_graph_vertex v g.
Proof.
intros. split; intros.
destruct (In_graph_vertex_strong _ _ H).
rewrite In_graph_add_edge_vertex in H0.
apply In_graph_labeled_vertex_weak with (val := x). auto.
destruct (In_graph_vertex_strong _ _ H).
apply In_graph_labeled_vertex_weak with (val := x).
rewrite In_graph_add_edge_vertex. auto.
Qed.
Lemma In_graph_edge_add_edge_u : forall e e' g w,
In_graph_edge e' g ->
~Edge.eq e e' ->
In_graph_edge e' (add_edge e g w).
Proof.
intros.
destruct (In_graph_edge_strong _ _ H).
apply In_graph_labeled_edge_weak with (val := x).
apply In_graph_edge_add_edge; auto.
Qed.
Lemma In_graph_edge_add_edge_2_u : forall e g w,
In_ext e g ->
In_graph_edge e (add_edge e g w).
Proof.
intros.
apply In_graph_labeled_edge_weak with (val := w).
apply In_graph_edge_add_edge_2. auto.
Qed.
Lemma In_graph_add_edge_edge_u : forall g e e' w,
In_ext e g ->
In_graph_edge e' (add_edge e g w) ->
~Edge.eq e e' ->
In_graph_edge e' g.
Proof.
intros.
destruct (In_graph_edge_strong _ _ H0).
apply In_graph_labeled_edge_weak with (val := x).
apply In_graph_add_edge_edge with (e := e) (w := w); auto.
Qed.
Lemma Add_edge_fail_vertex_u : forall e g w v,
~In_ext e g ->
(In_graph_vertex v g <-> In_graph_vertex v (add_edge e g w)).
Proof.
intros. split; intros.
destruct (In_graph_vertex_strong _ _ H0).
apply In_graph_labeled_vertex_weak with (val := x).
rewrite <-Add_edge_fail_vertex; auto.
destruct (In_graph_vertex_strong _ _ H0).
apply In_graph_labeled_vertex_weak with (val := x).
rewrite <-Add_edge_fail_vertex in H1; auto.
Qed.
Lemma Add_edge_fail_edge_u : forall e g w e',
~In_ext e g ->
(In_graph_edge e' g <-> In_graph_edge e' (add_edge e g w)).
Proof.
intros. split; intros.
destruct (In_graph_edge_strong _ _ H0).
apply In_graph_labeled_edge_weak with (val := x).
rewrite <-Add_edge_fail_edge; auto.
destruct (In_graph_edge_strong _ _ H0).
apply In_graph_labeled_edge_weak with (val := x).
rewrite <-Add_edge_fail_edge in H1; auto.
Qed.
Lemma In_graph_add_edge_weak_vertex_u : forall v g e w,
In_graph_vertex v (add_edge_w e g w) <->
In_graph_vertex v g \/ (incident e v /\ ~In_graph_vertex v g).
Proof.
split; intros.
destruct (In_graph_vertex_strong _ _ H).
rewrite In_graph_add_edge_weak_vertex in H0.
destruct H0. left. apply In_graph_labeled_vertex_weak with (val := x); auto.
right. intuition.
destruct H.
destruct (In_graph_vertex_strong _ _ H).
apply In_graph_labeled_vertex_weak with (val := x).
rewrite In_graph_add_edge_weak_vertex. left. auto.
destruct H.
apply In_graph_labeled_vertex_weak with (val := None).
rewrite In_graph_add_edge_weak_vertex. right. intuition.
Qed.
Lemma In_graph_add_edge_weak_edge_u : forall g e e' w,
In_graph_edge e' (add_edge_w e g w) <->
eq e e' \/ (~eq e e' /\ In_graph_edge e' g).
Proof.
split; intros.
destruct (In_graph_edge_strong _ _ H).
rewrite In_graph_add_edge_weak_edge in H0. destruct H0.
left. intuition.
destruct H0. right. split. auto. apply In_graph_labeled_edge_weak with (val := x); auto.
destruct H.
apply In_graph_labeled_edge_weak with (val := w).
rewrite In_graph_add_edge_weak_edge. left. split; auto.
destruct H. destruct (In_graph_edge_strong _ _ H0).
apply In_graph_labeled_edge_weak with (val := x).
rewrite In_graph_add_edge_weak_edge. right. split; auto.
Qed.
Lemma In_graph_remove_edge_vertex_u : forall v e g,
(In_graph_vertex v (remove_edge e g) <-> In_graph_vertex v g).
Proof.
split; intros.
destruct (In_graph_vertex_strong _ _ H).
rewrite In_graph_remove_edge_vertex in H0.
apply In_graph_labeled_vertex_weak with (val := x); auto.
destruct (In_graph_vertex_strong _ _ H).
apply In_graph_labeled_vertex_weak with (val := x).
rewrite In_graph_remove_edge_vertex. auto.
Qed.
Lemma In_graph_remove_edge_edge_succ_u : forall e g,
~VertexMap.In (snd_end e) (successors (fst_end e) (remove_edge e g)).
Proof.
apply In_graph_remove_edge_edge_succ.
Qed.
Lemma In_graph_remove_edge_edge_pred_u : forall e g,
~VertexMap.In (fst_end e) (predecessors (snd_end e) (remove_edge e g)).
Proof.
apply In_graph_remove_edge_edge_pred.
Qed.
End UDSpec.
Module UUSpec (Vertex : OrderedType) (Lab : Labels)
(G : Constructive_Undirected_Graph Vertex Lab).
Module Import Props := GraphProps Vertex Lab G.
Import G Edge.
Lemma In_remove_vertex_u : forall x r g,
In_graph_vertex x (remove_vertex r g) <->
In_graph_vertex x g /\ ~Vertex.eq x r.
Proof.
intros.
split; intros.
destruct (In_graph_vertex_strong _ _ H).
generalize (In_remove_vertex x r g x0). intro. rewrite H1 in H0.
destruct H0. split. apply In_graph_labeled_vertex_weak with (val := x0). auto. auto.
destruct H. destruct (In_graph_vertex_strong x g H).
apply In_graph_labeled_vertex_weak with (val := x0).
rewrite In_remove_vertex. split; auto.
Qed.
Lemma In_remove_edge_u : forall e r g,
In_graph_edge e (remove_vertex r g) <->
(In_graph_edge e g /\ ~incident e r).
Proof.
intros.
split; intros.
destruct (In_graph_edge_strong _ _ H).
generalize (In_remove_edge e r g x). intro. rewrite H1 in H0.
destruct H0. split. apply In_graph_labeled_edge_weak with (val := x). auto. auto.
destruct H. destruct (In_graph_edge_strong e g H).
apply In_graph_labeled_edge_weak with (val := x).
rewrite In_remove_edge. split; auto.
Qed.
Lemma In_add_vertex_u : forall v g x w,
In_graph_vertex x (add_vertex v g w) <->
Vertex.eq x v \/ In_graph_vertex x g.
Proof.
intros.
split; intros.
destruct (In_graph_vertex_strong _ _ H).
generalize (In_add_vertex v g x w x0). intro. rewrite H1 in H0.
destruct H0.
left. intuition.
right. apply In_graph_labeled_vertex_weak with (val := x0). auto.
destruct H.
destruct (In_graph_vertex_dec x g).
destruct (In_graph_vertex_strong x g). auto.
apply In_graph_labeled_vertex_weak with (val := x0).
rewrite In_add_vertex. right. auto.
apply In_graph_labeled_vertex_weak with (val := w).
rewrite In_add_vertex. left. split; [|split]; auto.
rewrite H in n. auto.
destruct (In_graph_vertex_strong x g). auto.
apply In_graph_labeled_vertex_weak with (val := x0).
rewrite In_add_vertex. right. auto.
Qed.
Lemma In_add_vertex_edge_u : forall v g e w,
In_graph_edge e (add_vertex v g w) <-> In_graph_edge e g.
Proof.
intros. split; intros.
destruct (In_graph_edge_strong _ _ H).
rewrite In_add_vertex_edge in H0.
apply In_graph_labeled_edge_weak with (val := x). auto.
destruct (In_graph_edge_strong _ _ H).
apply In_graph_labeled_edge_weak with (val := x).
rewrite In_add_vertex_edge. auto.
Qed.
Lemma In_graph_add_edge_vertex_u : forall v g e w,
In_graph_vertex v (add_edge e g w) <-> In_graph_vertex v g.
Proof.
intros. split; intros.
destruct (In_graph_vertex_strong _ _ H).
rewrite In_graph_add_edge_vertex in H0.
apply In_graph_labeled_vertex_weak with (val := x). auto.
destruct (In_graph_vertex_strong _ _ H).
apply In_graph_labeled_vertex_weak with (val := x).
rewrite In_graph_add_edge_vertex. auto.
Qed.
Lemma In_graph_edge_add_edge_u : forall e e' g w,
In_graph_edge e' g ->
~Edge.eq e e' ->
~Edge.eq (permute e) e' ->
In_graph_edge e' (add_edge e g w).
Proof.
intros.
destruct (In_graph_edge_strong _ _ H).
apply In_graph_labeled_edge_weak with (val := x).
apply In_graph_edge_add_edge; auto.
Qed.
Lemma In_graph_edge_add_edge_2_u : forall e g w,
In_ext e g ->
In_graph_edge e (add_edge e g w).
Proof.
intros.
apply In_graph_labeled_edge_weak with (val := w).
apply In_graph_edge_add_edge_2. auto.
Qed.
Lemma In_graph_add_edge_edge_u : forall g e e' w,
In_ext e g ->
In_graph_edge e' (add_edge e g w) ->
~Edge.eq e e' ->
~Edge.eq (permute e) e' ->
In_graph_edge e' g.
Proof.
intros.
destruct (In_graph_edge_strong _ _ H0).
apply In_graph_labeled_edge_weak with (val := x).
apply In_graph_add_edge_edge with (e := e) (w := w); auto.
Qed.
Lemma Add_edge_fail_vertex_u : forall e g w v,
~In_ext e g ->
(In_graph_vertex v g <-> In_graph_vertex v (add_edge e g w)).
Proof.
intros. split; intros.
destruct (In_graph_vertex_strong _ _ H0).
apply In_graph_labeled_vertex_weak with (val := x).
rewrite <-Add_edge_fail_vertex; auto.
destruct (In_graph_vertex_strong _ _ H0).
apply In_graph_labeled_vertex_weak with (val := x).
rewrite <-Add_edge_fail_vertex in H1; auto.
Qed.
Lemma Add_edge_fail_edge_u : forall e g w e',
~In_ext e g ->
(In_graph_edge e' g <-> In_graph_edge e' (add_edge e g w)).
Proof.
intros. split; intros.
destruct (In_graph_edge_strong _ _ H0).
apply In_graph_labeled_edge_weak with (val := x).
rewrite <-Add_edge_fail_edge; auto.
destruct (In_graph_edge_strong _ _ H0).
apply In_graph_labeled_edge_weak with (val := x).
rewrite <-Add_edge_fail_edge in H1; auto.
Qed.
Lemma In_graph_add_edge_weak_vertex_u : forall v g e w,
In_graph_vertex v (add_edge_w e g w) <->
In_graph_vertex v g \/ (incident e v /\ ~In_graph_vertex v g).
Proof.
split; intros.
destruct (In_graph_vertex_strong _ _ H).
rewrite In_graph_add_edge_weak_vertex in H0.
destruct H0. left. apply In_graph_labeled_vertex_weak with (val := x); auto.
right. intuition.
destruct H.
destruct (In_graph_vertex_strong _ _ H).
apply In_graph_labeled_vertex_weak with (val := x).
rewrite In_graph_add_edge_weak_vertex. left. auto.
destruct H.
apply In_graph_labeled_vertex_weak with (val := None).
rewrite In_graph_add_edge_weak_vertex. right. intuition.
Qed.
Lemma In_graph_add_edge_weak_edge_u : forall g e e' w,
In_graph_edge e' (add_edge_w e g w) <->
eq e e' \/ eq (permute e) e' \/ (~eq e e' /\ ~eq (permute e) e' /\ In_graph_edge e' g).
Proof.
split; intros.
destruct (In_graph_edge_strong _ _ H).
rewrite In_graph_add_edge_weak_edge in H0. destruct H0. destruct H0. destruct H0.
left. intuition.
right. left. auto.
destruct H0. destruct H1. right. right. split. auto. split. auto.
apply In_graph_labeled_edge_weak with (val := x); auto.
destruct H.
apply In_graph_labeled_edge_weak with (val := w).
rewrite In_graph_add_edge_weak_edge. left. split; auto.
destruct H.
apply In_graph_labeled_edge_weak with (val := w).
rewrite In_graph_add_edge_weak_edge. left. split; auto.
destruct H. destruct H0.
destruct (In_graph_edge_strong _ _ H1).
apply In_graph_labeled_edge_weak with (val := x).
rewrite In_graph_add_edge_weak_edge. right. split; auto.
Qed.
Lemma In_graph_remove_edge_vertex_u : forall v e g,
(In_graph_vertex v (remove_edge e g) <-> In_graph_vertex v g).
Proof.
split; intros.
destruct (In_graph_vertex_strong _ _ H).
rewrite In_graph_remove_edge_vertex in H0.
apply In_graph_labeled_vertex_weak with (val := x); auto.
destruct (In_graph_vertex_strong _ _ H).
apply In_graph_labeled_vertex_weak with (val := x).
rewrite In_graph_remove_edge_vertex. auto.
Qed.
Lemma In_graph_remove_edge_edge_succ_u : forall e g,
~VertexMap.In (snd_end e) (successors (fst_end e) (remove_edge e g)).
Proof.
apply In_graph_remove_edge_edge_succ.
Qed.
Lemma In_graph_remove_edge_edge_pred_u : forall e g,
~VertexMap.In (fst_end e) (predecessors (snd_end e) (remove_edge e g)).
Proof.
apply In_graph_remove_edge_edge_pred.
Qed.
End UUSpec.
Require Import Constructive_UndigraphInterface.
Require Import OrderedType.
Require Import Graph_Properties.
Require Import Labels.
Module UDSpec (Vertex : OrderedType) (Lab : Labels)
(G : Constructive_Directed_Graph Vertex Lab).
Module Import Props := GraphProps Vertex Lab G.
Import G Edge.
Lemma In_remove_vertex_u : forall x r g,
In_graph_vertex x (remove_vertex r g) <->
In_graph_vertex x g /\ ~Vertex.eq x r.
Proof.
intros.
split; intros.
destruct (In_graph_vertex_strong _ _ H).
generalize (In_remove_vertex x r g x0). intro. rewrite H1 in H0.
destruct H0. split. apply In_graph_labeled_vertex_weak with (val := x0). auto. auto.
destruct H. destruct (In_graph_vertex_strong x g H).
apply In_graph_labeled_vertex_weak with (val := x0).
rewrite In_remove_vertex. split; auto.
Qed.
Lemma In_remove_edge_u : forall e r g,
In_graph_edge e (remove_vertex r g) <->
(In_graph_edge e g /\ ~incident e r).
Proof.
intros.
split; intros.
destruct (In_graph_edge_strong _ _ H).
generalize (In_remove_edge e r g x). intro. rewrite H1 in H0.
destruct H0. split. apply In_graph_labeled_edge_weak with (val := x). auto. auto.
destruct H. destruct (In_graph_edge_strong e g H).
apply In_graph_labeled_edge_weak with (val := x).
rewrite In_remove_edge. split; auto.
Qed.
Lemma In_add_vertex_u : forall v g x w,
In_graph_vertex x (add_vertex v g w) <->
Vertex.eq x v \/ In_graph_vertex x g.
Proof.
intros.
split; intros.
destruct (In_graph_vertex_strong _ _ H).
generalize (In_add_vertex v g x w x0). intro. rewrite H1 in H0.
destruct H0.
left. intuition.
right. apply In_graph_labeled_vertex_weak with (val := x0). auto.
destruct H.
destruct (In_graph_vertex_dec x g).
destruct (In_graph_vertex_strong x g). auto.
apply In_graph_labeled_vertex_weak with (val := x0).
rewrite In_add_vertex. right. auto.
apply In_graph_labeled_vertex_weak with (val := w).
rewrite In_add_vertex. left. split; [|split]; auto.
rewrite H in n. auto.
destruct (In_graph_vertex_strong x g). auto.
apply In_graph_labeled_vertex_weak with (val := x0).
rewrite In_add_vertex. right. auto.
Qed.
Lemma In_add_vertex_edge_u : forall v g e w,
In_graph_edge e (add_vertex v g w) <-> In_graph_edge e g.
Proof.
intros. split; intros.
destruct (In_graph_edge_strong _ _ H).
rewrite In_add_vertex_edge in H0.
apply In_graph_labeled_edge_weak with (val := x). auto.
destruct (In_graph_edge_strong _ _ H).
apply In_graph_labeled_edge_weak with (val := x).
rewrite In_add_vertex_edge. auto.
Qed.
Lemma In_graph_add_edge_vertex_u : forall v g e w,
In_graph_vertex v (add_edge e g w) <-> In_graph_vertex v g.
Proof.
intros. split; intros.
destruct (In_graph_vertex_strong _ _ H).
rewrite In_graph_add_edge_vertex in H0.
apply In_graph_labeled_vertex_weak with (val := x). auto.
destruct (In_graph_vertex_strong _ _ H).
apply In_graph_labeled_vertex_weak with (val := x).
rewrite In_graph_add_edge_vertex. auto.
Qed.
Lemma In_graph_edge_add_edge_u : forall e e' g w,
In_graph_edge e' g ->
~Edge.eq e e' ->
In_graph_edge e' (add_edge e g w).
Proof.
intros.
destruct (In_graph_edge_strong _ _ H).
apply In_graph_labeled_edge_weak with (val := x).
apply In_graph_edge_add_edge; auto.
Qed.
Lemma In_graph_edge_add_edge_2_u : forall e g w,
In_ext e g ->
In_graph_edge e (add_edge e g w).
Proof.
intros.
apply In_graph_labeled_edge_weak with (val := w).
apply In_graph_edge_add_edge_2. auto.
Qed.
Lemma In_graph_add_edge_edge_u : forall g e e' w,
In_ext e g ->
In_graph_edge e' (add_edge e g w) ->
~Edge.eq e e' ->
In_graph_edge e' g.
Proof.
intros.
destruct (In_graph_edge_strong _ _ H0).
apply In_graph_labeled_edge_weak with (val := x).
apply In_graph_add_edge_edge with (e := e) (w := w); auto.
Qed.
Lemma Add_edge_fail_vertex_u : forall e g w v,
~In_ext e g ->
(In_graph_vertex v g <-> In_graph_vertex v (add_edge e g w)).
Proof.
intros. split; intros.
destruct (In_graph_vertex_strong _ _ H0).
apply In_graph_labeled_vertex_weak with (val := x).
rewrite <-Add_edge_fail_vertex; auto.
destruct (In_graph_vertex_strong _ _ H0).
apply In_graph_labeled_vertex_weak with (val := x).
rewrite <-Add_edge_fail_vertex in H1; auto.
Qed.
Lemma Add_edge_fail_edge_u : forall e g w e',
~In_ext e g ->
(In_graph_edge e' g <-> In_graph_edge e' (add_edge e g w)).
Proof.
intros. split; intros.
destruct (In_graph_edge_strong _ _ H0).
apply In_graph_labeled_edge_weak with (val := x).
rewrite <-Add_edge_fail_edge; auto.
destruct (In_graph_edge_strong _ _ H0).
apply In_graph_labeled_edge_weak with (val := x).
rewrite <-Add_edge_fail_edge in H1; auto.
Qed.
Lemma In_graph_add_edge_weak_vertex_u : forall v g e w,
In_graph_vertex v (add_edge_w e g w) <->
In_graph_vertex v g \/ (incident e v /\ ~In_graph_vertex v g).
Proof.
split; intros.
destruct (In_graph_vertex_strong _ _ H).
rewrite In_graph_add_edge_weak_vertex in H0.
destruct H0. left. apply In_graph_labeled_vertex_weak with (val := x); auto.
right. intuition.
destruct H.
destruct (In_graph_vertex_strong _ _ H).
apply In_graph_labeled_vertex_weak with (val := x).
rewrite In_graph_add_edge_weak_vertex. left. auto.
destruct H.
apply In_graph_labeled_vertex_weak with (val := None).
rewrite In_graph_add_edge_weak_vertex. right. intuition.
Qed.
Lemma In_graph_add_edge_weak_edge_u : forall g e e' w,
In_graph_edge e' (add_edge_w e g w) <->
eq e e' \/ (~eq e e' /\ In_graph_edge e' g).
Proof.
split; intros.
destruct (In_graph_edge_strong _ _ H).
rewrite In_graph_add_edge_weak_edge in H0. destruct H0.
left. intuition.
destruct H0. right. split. auto. apply In_graph_labeled_edge_weak with (val := x); auto.
destruct H.
apply In_graph_labeled_edge_weak with (val := w).
rewrite In_graph_add_edge_weak_edge. left. split; auto.
destruct H. destruct (In_graph_edge_strong _ _ H0).
apply In_graph_labeled_edge_weak with (val := x).
rewrite In_graph_add_edge_weak_edge. right. split; auto.
Qed.
Lemma In_graph_remove_edge_vertex_u : forall v e g,
(In_graph_vertex v (remove_edge e g) <-> In_graph_vertex v g).
Proof.
split; intros.
destruct (In_graph_vertex_strong _ _ H).
rewrite In_graph_remove_edge_vertex in H0.
apply In_graph_labeled_vertex_weak with (val := x); auto.
destruct (In_graph_vertex_strong _ _ H).
apply In_graph_labeled_vertex_weak with (val := x).
rewrite In_graph_remove_edge_vertex. auto.
Qed.
Lemma In_graph_remove_edge_edge_succ_u : forall e g,
~VertexMap.In (snd_end e) (successors (fst_end e) (remove_edge e g)).
Proof.
apply In_graph_remove_edge_edge_succ.
Qed.
Lemma In_graph_remove_edge_edge_pred_u : forall e g,
~VertexMap.In (fst_end e) (predecessors (snd_end e) (remove_edge e g)).
Proof.
apply In_graph_remove_edge_edge_pred.
Qed.
End UDSpec.
Module UUSpec (Vertex : OrderedType) (Lab : Labels)
(G : Constructive_Undirected_Graph Vertex Lab).
Module Import Props := GraphProps Vertex Lab G.
Import G Edge.
Lemma In_remove_vertex_u : forall x r g,
In_graph_vertex x (remove_vertex r g) <->
In_graph_vertex x g /\ ~Vertex.eq x r.
Proof.
intros.
split; intros.
destruct (In_graph_vertex_strong _ _ H).
generalize (In_remove_vertex x r g x0). intro. rewrite H1 in H0.
destruct H0. split. apply In_graph_labeled_vertex_weak with (val := x0). auto. auto.
destruct H. destruct (In_graph_vertex_strong x g H).
apply In_graph_labeled_vertex_weak with (val := x0).
rewrite In_remove_vertex. split; auto.
Qed.
Lemma In_remove_edge_u : forall e r g,
In_graph_edge e (remove_vertex r g) <->
(In_graph_edge e g /\ ~incident e r).
Proof.
intros.
split; intros.
destruct (In_graph_edge_strong _ _ H).
generalize (In_remove_edge e r g x). intro. rewrite H1 in H0.
destruct H0. split. apply In_graph_labeled_edge_weak with (val := x). auto. auto.
destruct H. destruct (In_graph_edge_strong e g H).
apply In_graph_labeled_edge_weak with (val := x).
rewrite In_remove_edge. split; auto.
Qed.
Lemma In_add_vertex_u : forall v g x w,
In_graph_vertex x (add_vertex v g w) <->
Vertex.eq x v \/ In_graph_vertex x g.
Proof.
intros.
split; intros.
destruct (In_graph_vertex_strong _ _ H).
generalize (In_add_vertex v g x w x0). intro. rewrite H1 in H0.
destruct H0.
left. intuition.
right. apply In_graph_labeled_vertex_weak with (val := x0). auto.
destruct H.
destruct (In_graph_vertex_dec x g).
destruct (In_graph_vertex_strong x g). auto.
apply In_graph_labeled_vertex_weak with (val := x0).
rewrite In_add_vertex. right. auto.
apply In_graph_labeled_vertex_weak with (val := w).
rewrite In_add_vertex. left. split; [|split]; auto.
rewrite H in n. auto.
destruct (In_graph_vertex_strong x g). auto.
apply In_graph_labeled_vertex_weak with (val := x0).
rewrite In_add_vertex. right. auto.
Qed.
Lemma In_add_vertex_edge_u : forall v g e w,
In_graph_edge e (add_vertex v g w) <-> In_graph_edge e g.
Proof.
intros. split; intros.
destruct (In_graph_edge_strong _ _ H).
rewrite In_add_vertex_edge in H0.
apply In_graph_labeled_edge_weak with (val := x). auto.
destruct (In_graph_edge_strong _ _ H).
apply In_graph_labeled_edge_weak with (val := x).
rewrite In_add_vertex_edge. auto.
Qed.
Lemma In_graph_add_edge_vertex_u : forall v g e w,
In_graph_vertex v (add_edge e g w) <-> In_graph_vertex v g.
Proof.
intros. split; intros.
destruct (In_graph_vertex_strong _ _ H).
rewrite In_graph_add_edge_vertex in H0.
apply In_graph_labeled_vertex_weak with (val := x). auto.
destruct (In_graph_vertex_strong _ _ H).
apply In_graph_labeled_vertex_weak with (val := x).
rewrite In_graph_add_edge_vertex. auto.
Qed.
Lemma In_graph_edge_add_edge_u : forall e e' g w,
In_graph_edge e' g ->
~Edge.eq e e' ->
~Edge.eq (permute e) e' ->
In_graph_edge e' (add_edge e g w).
Proof.
intros.
destruct (In_graph_edge_strong _ _ H).
apply In_graph_labeled_edge_weak with (val := x).
apply In_graph_edge_add_edge; auto.
Qed.
Lemma In_graph_edge_add_edge_2_u : forall e g w,
In_ext e g ->
In_graph_edge e (add_edge e g w).
Proof.
intros.
apply In_graph_labeled_edge_weak with (val := w).
apply In_graph_edge_add_edge_2. auto.
Qed.
Lemma In_graph_add_edge_edge_u : forall g e e' w,
In_ext e g ->
In_graph_edge e' (add_edge e g w) ->
~Edge.eq e e' ->
~Edge.eq (permute e) e' ->
In_graph_edge e' g.
Proof.
intros.
destruct (In_graph_edge_strong _ _ H0).
apply In_graph_labeled_edge_weak with (val := x).
apply In_graph_add_edge_edge with (e := e) (w := w); auto.
Qed.
Lemma Add_edge_fail_vertex_u : forall e g w v,
~In_ext e g ->
(In_graph_vertex v g <-> In_graph_vertex v (add_edge e g w)).
Proof.
intros. split; intros.
destruct (In_graph_vertex_strong _ _ H0).
apply In_graph_labeled_vertex_weak with (val := x).
rewrite <-Add_edge_fail_vertex; auto.
destruct (In_graph_vertex_strong _ _ H0).
apply In_graph_labeled_vertex_weak with (val := x).
rewrite <-Add_edge_fail_vertex in H1; auto.
Qed.
Lemma Add_edge_fail_edge_u : forall e g w e',
~In_ext e g ->
(In_graph_edge e' g <-> In_graph_edge e' (add_edge e g w)).
Proof.
intros. split; intros.
destruct (In_graph_edge_strong _ _ H0).
apply In_graph_labeled_edge_weak with (val := x).
rewrite <-Add_edge_fail_edge; auto.
destruct (In_graph_edge_strong _ _ H0).
apply In_graph_labeled_edge_weak with (val := x).
rewrite <-Add_edge_fail_edge in H1; auto.
Qed.
Lemma In_graph_add_edge_weak_vertex_u : forall v g e w,
In_graph_vertex v (add_edge_w e g w) <->
In_graph_vertex v g \/ (incident e v /\ ~In_graph_vertex v g).
Proof.
split; intros.
destruct (In_graph_vertex_strong _ _ H).
rewrite In_graph_add_edge_weak_vertex in H0.
destruct H0. left. apply In_graph_labeled_vertex_weak with (val := x); auto.
right. intuition.
destruct H.
destruct (In_graph_vertex_strong _ _ H).
apply In_graph_labeled_vertex_weak with (val := x).
rewrite In_graph_add_edge_weak_vertex. left. auto.
destruct H.
apply In_graph_labeled_vertex_weak with (val := None).
rewrite In_graph_add_edge_weak_vertex. right. intuition.
Qed.
Lemma In_graph_add_edge_weak_edge_u : forall g e e' w,
In_graph_edge e' (add_edge_w e g w) <->
eq e e' \/ eq (permute e) e' \/ (~eq e e' /\ ~eq (permute e) e' /\ In_graph_edge e' g).
Proof.
split; intros.
destruct (In_graph_edge_strong _ _ H).
rewrite In_graph_add_edge_weak_edge in H0. destruct H0. destruct H0. destruct H0.
left. intuition.
right. left. auto.
destruct H0. destruct H1. right. right. split. auto. split. auto.
apply In_graph_labeled_edge_weak with (val := x); auto.
destruct H.
apply In_graph_labeled_edge_weak with (val := w).
rewrite In_graph_add_edge_weak_edge. left. split; auto.
destruct H.
apply In_graph_labeled_edge_weak with (val := w).
rewrite In_graph_add_edge_weak_edge. left. split; auto.
destruct H. destruct H0.
destruct (In_graph_edge_strong _ _ H1).
apply In_graph_labeled_edge_weak with (val := x).
rewrite In_graph_add_edge_weak_edge. right. split; auto.
Qed.
Lemma In_graph_remove_edge_vertex_u : forall v e g,
(In_graph_vertex v (remove_edge e g) <-> In_graph_vertex v g).
Proof.
split; intros.
destruct (In_graph_vertex_strong _ _ H).
rewrite In_graph_remove_edge_vertex in H0.
apply In_graph_labeled_vertex_weak with (val := x); auto.
destruct (In_graph_vertex_strong _ _ H).
apply In_graph_labeled_vertex_weak with (val := x).
rewrite In_graph_remove_edge_vertex. auto.
Qed.
Lemma In_graph_remove_edge_edge_succ_u : forall e g,
~VertexMap.In (snd_end e) (successors (fst_end e) (remove_edge e g)).
Proof.
apply In_graph_remove_edge_edge_succ.
Qed.
Lemma In_graph_remove_edge_edge_pred_u : forall e g,
~VertexMap.In (fst_end e) (predecessors (snd_end e) (remove_edge e g)).
Proof.
apply In_graph_remove_edge_edge_pred.
Qed.
End UUSpec.