Library GraphBasics.Digraphs

Require Export Arcs.

Section DIGRAPH.

Inductive Digraph : V_set -> A_set -> Set :=
  | D_empty : Digraph V_empty A_empty
  | D_vertex :
      forall (v : V_set) (a : A_set) (d : Digraph v a) (x : Vertex),
      ~ v x -> Digraph (V_union (V_single x) v) a
  | D_arc :
      forall (v : V_set) (a : A_set) (d : Digraph v a) (x y : Vertex),
      v x ->
      v y ->
      ~ a (A_ends x y) -> Digraph v (A_union (A_single (A_ends x y)) a)
  | D_eq :
      forall (v v' : V_set) (a a' : A_set),
      v = v' -> a = a' -> Digraph v a -> Digraph v' a'.

Fixpoint DV_list (v : V_set) (a : A_set) (d : Digraph v a) {struct d} :
 V_list :=
  match d with
  | D_empty => V_nil
  | D_vertex v' a' d' x _ => x :: DV_list v' a' d'
  | D_arc v' a' d' x y _ _ _ => DV_list v' a' d'
  | D_eq v v' a a' _ _ d => DV_list v a d
  end.

Fixpoint DA_list (v : V_set) (a : A_set) (d : Digraph v a) {struct d} :
 A_list :=
  match d with
  | D_empty => A_nil
  | D_vertex v' a' d' x _ => DA_list v' a' d'
  | D_arc v' a' d' x y _ _ _ => A_ends x y :: DA_list v' a' d'
  | D_eq v v' a a' _ _ d => DA_list v a d
  end.

Definition D_order (v : V_set) (a : A_set) (d : Digraph v a) :=
  length (DV_list v a d).

Definition D_size (v : V_set) (a : A_set) (d : Digraph v a) :=
  length (DA_list v a d).

Lemma D_v_dec :
 forall (v : V_set) (a : A_set) (d : Digraph v a) (x : Vertex),
 {v x} + {~ v x}.
Proof.
        intros v a d; elim d; intros.
        right; apply V_empty_nothing.

        case (H x0); intros.
        left; apply V_in_right; trivial.

        case (V_eq_dec x x0); intros.
        left; apply V_in_left; rewrite e; apply V_in_single.

        right; red in |- *; intros; inversion H0.
        elim n1; inversion H1; trivial.

        elim n0; trivial.

        auto.

        case (H x); intros.
        left; elim e; trivial.

        right; elim e; trivial.
Qed.

Lemma D_a_dec :
 forall (v : V_set) (a : A_set) (d : Digraph v a) (x : Arc), {a x} + {~ a x}.
Proof.
        intros v a d; elim d; intros.
        right; apply A_empty_nothing.

        auto.

        case (H x0); intros.
        left; apply A_in_right; trivial.

        case (A_eq_dec (A_ends x y) x0); intros.
        left; apply A_in_left; rewrite e; apply A_in_single.

        right; red in |- *; intros; inversion H0.
        elim n1; inversion H1; trivial.

        elim n0; trivial.

        case (H x); intros.
        left; elim e0; trivial.

        right; elim e0; trivial.
Qed.

End DIGRAPH.

Section UNION_DIGRAPHS.

Lemma D_union :
 forall (v1 v2 : V_set) (a1 a2 : A_set),
 Digraph v1 a1 -> Digraph v2 a2 -> Digraph (V_union v1 v2) (A_union a1 a2).
Proof.
        intros; elim H; intros.
        apply D_eq with (v := v2) (a := a2).
        symmetry in |- *; apply V_union_neutral.

        symmetry in |- *; apply A_union_neutral.

        trivial.

        case (D_v_dec v2 a2 H0 x); intros.
        apply D_eq with (v := V_union v v2) (a := A_union a a2).
        rewrite V_union_assoc; rewrite (V_union_absorb (V_single x)); trivial.
        apply V_included_single; apply V_in_right; trivial.

        trivial.

        trivial.

        apply
         D_eq
          with (v := V_union (V_single x) (V_union v v2)) (a := A_union a a2).
        symmetry in |- *; apply V_union_assoc.

        trivial.

        apply D_vertex.
        trivial.

        apply V_not_union; trivial.

        case (D_a_dec v2 a2 H0 (A_ends x y)); intros.
        apply D_eq with (v := V_union v v2) (a := A_union a a2).
        trivial.

        rewrite A_union_assoc;
         rewrite (A_union_absorb (A_single (A_ends x y)));
         trivial.
        apply A_included_single; apply A_in_right; trivial.

        trivial.

        apply
         D_eq
          with
            (v := V_union v v2)
            (a := A_union (A_single (A_ends x y)) (A_union a a2)).
        trivial.

        symmetry in |- *; apply A_union_assoc.

        apply D_arc.
        trivial.

        apply V_in_left; trivial.

        apply V_in_left; trivial.

        apply A_not_union; trivial.

        apply D_eq with (v := V_union v v2) (a := A_union a a2).
        elim e; trivial.

        elim e0; trivial.

        trivial.
Qed.

End UNION_DIGRAPHS.