# Library GraphBasics.Edges

Require Export Arcs.

Section EDGE.

Inductive E_set (x y : Vertex) : A_set :=
| E_right : E_set x y (A_ends x y)
| E_left : E_set x y (A_ends y x).

Lemma E_set_eq : x y : Vertex, E_set x y = E_set y x.
Proof.
intros; apply A_set_eq.
split; intros.
inversion H; [ apply E_left | apply E_right ].

inversion H; [ apply E_left | apply E_right ].
Qed.

Lemma E_set_diff1 :
x x' y y' : Vertex, x x' x y' E_set x y E_set x' y'.
Proof.
intros; red in |- *; intros.
absurd (E_set x y (A_ends x' y')).
red in |- *; intros; inversion H2.
elim H; trivial.

elim H0; trivial.

rewrite H1; apply E_right.
Qed.

Lemma E_set_diff2 :
x x' y y' : Vertex, y x' y y' E_set x y E_set x' y'.
Proof.
intros; rewrite (E_set_eq x y); apply E_set_diff1; auto.
Qed.

Lemma E_set_diff3 :
x x' y y' : Vertex, x' x x' y E_set x y E_set x' y'.
Proof.
intros; apply A_set_diff_commut; apply E_set_diff1; trivial.
Qed.

Lemma E_set_diff4 :
x x' y y' : Vertex, y' x y' y E_set x y E_set x' y'.
Proof.
intros; apply A_set_diff_commut; apply E_set_diff2; trivial.
Qed.

Lemma E_set_eq_diff :
x x' y y' : Vertex, x = x' y y' E_set x y E_set x' y'.
Proof.
intros; red in |- *; intros.
absurd (E_set x y (A_ends x' y')).
red in |- *; intros; inversion H2.
elim H0; trivial.

elim H0; rewrite H4; rewrite <- H5; auto.

rewrite H1; apply E_right.
Qed.

Lemma E_set_diff_eq :
x x' y y' : Vertex, x x' y = y' E_set x y E_set x' y'.
Proof.
intros; rewrite (E_set_eq x y); rewrite (E_set_eq x' y');
apply E_set_eq_diff; trivial.
Qed.

Lemma E_set_eq_dec :
x x' y y' : Vertex,
{E_set x y = E_set x' y'} + {E_set x y E_set x' y'}.
Proof.
intros; case (V_eq_dec x x'); intros.
case (V_eq_dec y y'); intros.
left; rewrite e; rewrite e0; trivial.

right; apply E_set_eq_diff; trivial.

case (V_eq_dec x y'); intros.
case (V_eq_dec y x'); intros.
left; rewrite e; rewrite e0; apply E_set_eq.

right; rewrite (E_set_eq x y); apply E_set_diff_eq; trivial.

right; apply E_set_diff1; trivial.
Qed.

Lemma E_not_set_eq123 :
x y z t : Vertex, x z y z ¬ E_set x y (A_ends z t).
Proof.
red in |- *; intros.
inversion H1.
elim H; trivial.

elim H0; trivial.
Qed.

Lemma E_not_set_eq14 :
x y z : Vertex, x z ¬ E_set x y (A_ends y z).
Proof.
red in |- *; intros.
inversion H0.
elim H; rewrite H2; trivial.

elim H; trivial.
Qed.

Lemma E_not_set_eq24 :
x y z : Vertex, y z ¬ E_set x y (A_ends x z).
Proof.
red in |- *; intros.
inversion H0.
elim H; trivial.

elim H; rewrite H2; trivial.
Qed.

End EDGE.

Section LIST_OF_EDGES.

Inductive Edge : Set :=
E_ends : Vertex Vertex Edge.

Inductive E_eq : Edge Edge Prop :=
| E_refl : u : Edge, E_eq u u
| E_rev : x y : Vertex, E_eq (E_ends x y) (E_ends y x).

Definition E_list := list Edge.

Definition E_nil := nil (A:=Edge).

Lemma E_eq_dec : u v : Edge, {E_eq u v} + {¬ E_eq u v}.
Proof.
simple destruct u; intros a b; simple destruct v; intros c d.
case (V_eq_dec a c); intros.
case (V_eq_dec b d); intros.
left; rewrite e; rewrite e0; apply E_refl.

right; red in |- *; intros; inversion H.
elim n; trivial.

elim n; rewrite H3; rewrite <- H4; auto.

case (V_eq_dec a d); intros.
case (V_eq_dec b c); intros.
left; rewrite e; rewrite e0; apply E_rev.

right; red in |- *; intros; inversion H.
elim n; trivial.

elim n0; trivial.

right; red in |- *; intros; inversion H.
elim n; trivial.

elim n0; trivial.
Qed.

Fixpoint E_in (u : Edge) (l : E_list) {struct l} : Prop :=
match l with
| nilFalse
| v :: l'if E_eq_dec u v then True else E_in u l'
end.

(a : A_set) (x y : Vertex),
A_union (E_set x y) a =
A_union (A_single (A_ends x y)) (A_union (A_single (A_ends y x)) a).
Proof.
intros; apply A_set_eq.
split; intros.
inversion_clear H.
inversion_clear H0.
apply A_in_left; apply A_in_single.

apply A_in_right; apply A_in_left; apply A_in_single.

do 2 apply A_in_right; trivial.

inversion_clear H.
inversion_clear H0.
apply A_in_left; apply E_right.

inversion_clear H0.
inversion_clear H.
apply A_in_left; apply E_left.

apply A_in_right; trivial.
Qed.

End LIST_OF_EDGES.

Section E_PROPERTIES.

Lemma E_inclusion :
(a : A_set) (x y : Vertex),
a (A_ends x y) a (A_ends y x) A_included (E_set x y) a.
Proof.
unfold A_included, Included in |- *; intros.
inversion H1; auto.
Qed.

Lemma E_union_absorb :
(a : A_set) (x y : Vertex),
a (A_ends x y) a (A_ends y x) A_union (E_set x y) a = a.
Proof.
intros; apply A_union_absorb.
apply E_inclusion; auto.
Qed.

Lemma E_inter_empty :
x x' y y' : Vertex,
E_set x y E_set x' y' A_inter (E_set x y) (E_set x' y') = A_empty.
Proof.
intros; apply A_set_eq; split; intros.
inversion H0.
elim H; generalize H2; inversion H1; intros.
inversion H5.
trivial.

apply E_set_eq.

inversion H5.
apply E_set_eq.

trivial.

inversion H0.
Qed.

Lemma E_set_disjoint :
(x y : Vertex) (a : A_set),
¬ a (A_ends x y) ¬ a (A_ends y x) A_inter (E_set x y) a = A_empty.
Proof.
intros; apply A_set_eq; split; intros.
inversion H1.
generalize H3; inversion H2; intros.
absurd (a (A_ends x y)); trivial.

absurd (a (A_ends y x)); trivial.

inversion H1.
Qed.

Lemma A_in_union_edge :
(x y x' y' : Vertex) (a : A_set),
A_union (E_set x y) a (A_ends x' y')
¬ E_set x y (A_ends x' y') a (A_ends x' y').
Proof.
intros; inversion H.
absurd (E_set x y (A_ends x' y')); trivial.

trivial.
Qed.

Lemma A_union_edge_edge :
(a a' : A_set) (x y : Vertex),
¬ a' (A_ends x y)
¬ a' (A_ends y x)
a = A_empty
A_union (E_set x y) a = A_union (E_set x y) a' A_empty = a'.
Proof.
intros; apply A_union_inversion with (E := E_set x y).
apply A_inter_empty.

apply E_set_disjoint; trivial.

rewrite <- H1; trivial.
Qed.

Lemma E_eq_not_in :
(a : A_set) (x y x' y' : Vertex),
¬ a (A_ends x y)
¬ a (A_ends y x) E_set x y = E_set x' y' ¬ a (A_ends x' y').
Proof.
intros.
generalize (A_eq_set _ _ H1 (A_ends x y) (E_right x y)); intros.
inversion H2; trivial.
Qed.

Lemma E_eq_not_in' :
(a : A_set) (x y x' y' : Vertex),
¬ a (A_ends x y)
¬ a (A_ends y x) E_set x y = E_set x' y' ¬ a (A_ends y' x').
Proof.
intros.
generalize (A_eq_set _ _ H1 (A_ends x y) (E_right x y)); intros.
inversion H2; trivial.
Qed.

End E_PROPERTIES.