Library Directed_edges

Require Import OrderedTypeEx.
Require Import OrderedType.


Module Directed_Edge (Vertex : OrderedType) <: OrderedType.

Module VertexPair := PairOrderedType Vertex Vertex.
Include VertexPair.

Module Import OTFacts := OrderedTypeFacts Vertex.
Module OTPairFacts := OrderedTypeFacts VertexPair.

Definition fst_end : t -> Vertex.t := fun x => fst x.
Definition snd_end : t -> Vertex.t := fun x => snd x.

Lemma edge_eq : forall e,
e = (fst_end e, snd_end e).

Proof.
 intro e; destruct e; unfold fst_end, snd_end; reflexivity.
Qed.

Lemma change_fst : forall x y,
fst_end (x,y) = x.

Proof.
auto.
Qed.

Lemma change_snd : forall x y,
snd_end (x,y) = y.

Proof.
auto.
Qed.

Ltac reduce_edge :=
repeat (try rewrite change_fst in *;try rewrite change_snd in *).

Definition incident e x := Vertex.eq x (fst_end e) \/ Vertex.eq x (snd_end e).

Lemma incident_dec : forall e x,
incident e x \/ ~incident e x.

Proof.
  intros e x.
  destruct (eq_dec x (fst_end e)).
    left;unfold incident;left;assumption.
    destruct (eq_dec x (snd_end e)).
    left;unfold incident;right;assumption.
  right;unfold incident;intro Heq; destruct Heq as [H|H];[elim (n H)|elim (n0 H)].
Qed.

Definition permute (e : t) :=
match e with |(x,y) => (y,x) end.

End Directed_Edge.