Require Export Graphs.

Section NEIGHBOR.

Variable v : V_set.

Variable a : A_set.

Definition In_neighbor (x y : Vertex) := a (A_ends y x).

Definition Out_neighbor (x y : Vertex) := a (A_ends x y).

Definition Neighbor (x y : Vertex) := A_included (E_set x y) a.

Lemma neighbor_in_neighbor :
 ∀ x y : Vertex, Neighbor x y → In_neighbor x y.
Proof.
        unfold Neighbor, A_included, Included, In_neighbor in |- *; intros.
        apply H; apply E_left.
Qed.

Lemma neighbor_out_neighbor :
 ∀ x y : Vertex, Neighbor x y → Out_neighbor x y.
Proof.
        unfold Neighbor, A_included, Included, Out_neighbor in |- *; intros.
        apply H; apply E_right.
Qed.

Lemma In_and_out_neighbor :
 ∀ x y : Vertex, In_neighbor x y → Out_neighbor x y → Neighbor x y.
Proof.
        unfold Neighbor, A_included, Included, In_neighbor, Out_neighbor
         in |- *; intros.
        inversion H1; auto.
Qed.

End NEIGHBOR.

Section DEGREE.

Fixpoint In_neighborhood (x : Vertex) (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' _ ⇒ In_neighborhood x v' a' d'
  | D_arc v' a' d' x' y' _ _ _ ⇒
      if V_eq_dec x y'
      then x' :: In_neighborhood x v' a' d'
      else In_neighborhood x v' a' d'
  | D_eq v' _ a' _ _ _ d' ⇒ In_neighborhood x v' a' d'
  end.

Fixpoint Out_neighborhood (x : Vertex) (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' _ ⇒ Out_neighborhood x v' a' d'
  | D_arc v' a' d' x' y' _ _ _ ⇒
      if V_eq_dec x x'
      then y' :: Out_neighborhood x v' a' d'
      else Out_neighborhood x v' a' d'
  | D_eq v' _ a' _ _ _ d' ⇒ Out_neighborhood x v' a' d'
  end.

Fixpoint neighborhood (x : Vertex) (v : V_set) (a : A_set)
 (g : Graph v a) {struct g} : V_list :=
  match g with
  | G_empty ⇒ V_nil
  | G_vertex v' a' g' x' _ ⇒ neighborhood x v' a' g'
  | G_edge v' a' g' x' y' _ _ _ _ _ ⇒
      if V_eq_dec x x'
      then y' :: neighborhood x v' a' g'
      else
       if V_eq_dec x y'
       then x' :: neighborhood x v' a' g'
       else neighborhood x v' a' g'
  | G_eq v' _ a' _ _ _ g' ⇒ neighborhood x v' a' g'
  end.

Fixpoint In_degree (x : Vertex) (v : V_set) (a : A_set)
 (d : Digraph v a) {struct d} : nat :=
  match d with
  | D_empty ⇒ 0
  | D_vertex v' a' d' x' _ ⇒ In_degree x v' a' d'
  | D_arc v' a' d' x' y' _ _ _ ⇒
      if V_eq_dec x y'
      then S (In_degree x v' a' d')
      else In_degree x v' a' d'
  | D_eq v' _ a' _ _ _ d' ⇒ In_degree x v' a' d'
  end.

Lemma In_degree_neighborhood :
 ∀ (x : Vertex) (v : V_set) (a : A_set) (d : Digraph v a),
 In_degree x v a d = length (In_neighborhood x v a d).
Proof.
        simple induction d; simpl in |- *; intros.
        trivial.

        trivial.

        case (V_eq_dec x y); rewrite H; auto.

        trivial.
Qed.

Fixpoint Out_degree (x : Vertex) (v : V_set) (a : A_set)
 (d : Digraph v a) {struct d} : nat :=
  match d with
  | D_empty ⇒ 0
  | D_vertex v' a' d' x' _ ⇒ Out_degree x v' a' d'
  | D_arc v' a' d' x' y' _ _ _ ⇒
      if V_eq_dec x x'
      then S (Out_degree x v' a' d')
      else Out_degree x v' a' d'
  | D_eq v' _ a' _ _ _ d' ⇒ Out_degree x v' a' d'
  end.

Lemma Out_degree_neighborhood :
 ∀ (x : Vertex) (v : V_set) (a : A_set) (d : Digraph v a),
 Out_degree x v a d = length (Out_neighborhood x v a d).
Proof.
        simple induction d; simpl in |- *; intros.
        trivial.

        trivial.

        case (V_eq_dec x x0); rewrite H; auto.

        trivial.
Qed.

Fixpoint degree (x : Vertex) (v : V_set) (a : A_set)
 (g : Graph v a) {struct g} : nat :=
  match g with
  | G_empty ⇒ 0
  | G_vertex v' a' g' x' _ ⇒ degree x v' a' g'
  | G_edge v' a' g' x' y' _ _ _ _ _ ⇒
      if V_eq_dec x x'
      then S (degree x v' a' g')
      else
        if V_eq_dec x y'
        then S (degree x v' a' g')
        else degree x v' a' g'
  | G_eq v' _ a' _ _ _ g' ⇒ degree x v' a' g'
  end.

Lemma Degree_neighborhood :
 ∀ (x : Vertex) (v : V_set) (a : A_set) (g : Graph v a),
 degree x v a g = length (neighborhood x v a g).
Proof.
        simple induction g; simpl in |- *; intros.
        trivial.

        trivial.

        case (V_eq_dec x x0); intros.
        rewrite H; auto.

        case (V_eq_dec x y); rewrite H; auto.

        trivial.
Qed.

End DEGREE.

Section REMARKABLE_DEGREE.

Definition isolated (x : Vertex) (v : V_set) (a : A_set)
  (g : Graph v a) := ∀ y : Vertex, ¬ a (A_ends x y).

Lemma Degree_isolated :
 ∀ (v : V_set) (a : A_set) (g : Graph v a) (x : Vertex),
 isolated x v a g → degree x v a g = 0.
Proof.
        unfold isolated in |- *; simple induction g; simpl in |- *; intros.
        trivial.

        auto.

        case (V_eq_dec x0 x); intros.
        absurd (A_union (E_set x y) a0 (A_ends x0 y)).
        auto.

        rewrite e; apply A_in_left; apply E_right.

        case (V_eq_dec x0 y); intros.
        absurd (A_union (E_set x y) a0 (A_ends x0 x)).
        auto.

        rewrite e; apply A_in_left; apply E_left.

        apply (H x0); red in |- *; intros.
        elim (H0 y0); apply A_in_right; trivial.

        apply (H x); rewrite e0; trivial.
Qed.

Definition pendant (x : Vertex) (v : V_set) (a : A_set)
  (g : Graph v a) :=
  exists2 y : Vertex,
    a (A_ends x y) & (∀ z : Vertex, a (A_ends x z) → z = y).

Lemma Degree_pendant :
 ∀ (v : V_set) (a : A_set) (g : Graph v a) (x : Vertex),
 pendant x v a g → degree x v a g = 1.
Proof.
        unfold pendant in |- *; simple induction g; simpl in |- *; intros.
        elim H; intros.
        inversion H0.

        auto.

        case (V_eq_dec x0 x); intros.
        rewrite (Degree_isolated v0 a0 d x0).
        trivial.

        elim H0; rewrite e; intros.
        unfold isolated in |- *; red in |- *; intros.
        absurd (y0 = x1).
        red in |- *; intros.
        absurd (y = x1).
        red in |- *; intros; elim n0.
        rewrite H5; rewrite <- H4; trivial.

        apply H2; apply A_in_left; apply E_right.

        apply H2; apply A_in_right; trivial.

        case (V_eq_dec x0 y); intros.
        rewrite (Degree_isolated v0 a0 d x0).
        trivial.

        elim H0; rewrite e; intros.
        unfold isolated in |- *; red in |- *; intros.
        absurd (y0 = x1).
        red in |- *; intros.
        absurd (x = x1).
        red in |- *; intros; elim n1.
        rewrite H5; rewrite <- H4; trivial.

        apply H2; apply A_in_left; apply E_left.

        apply H2; apply A_in_right; trivial.

        apply H; elim H0; intros.
        split with x1.
        apply (A_in_union_edge _ _ _ _ _ H1).
        apply E_not_set_eq123; auto.

        intros; apply H2; apply A_in_right; trivial.

        apply H; rewrite e0; trivial.
Qed.

Lemma Degree_not_isolated :
 ∀ (v : V_set) (a : A_set) (g : Graph v a) (x : Vertex),
 (∃ y : Vertex, a (A_ends x y)) → degree x v a g > 0.
Proof.
        simple induction g; simpl in |- *; intros.
        elim H; intros.
        inversion H0.

        auto.

        case (V_eq_dec x0 x); intros.
        omega.

        case (V_eq_dec x0 y); intros.
        omega.

        apply H; elim H0; intros.
        split with x1.
        apply (A_in_union_edge _ _ _ _ _ H1).
        apply E_not_set_eq123; auto.

        apply H; rewrite e0; trivial.
Qed.

Lemma Degree_not_pendant :
 ∀ (v : V_set) (a : A_set) (g : Graph v a) (x : Vertex),
 (exists2 y : Vertex,
    a (A_ends x y) & (exists2 z : Vertex, a (A_ends x z) & y ≠ z)) →
 degree x v a g > 1.
Proof.
        simple induction g; simpl in |- *; intros.
        elim H; intros.
        inversion H0.

        auto.

        case (V_eq_dec x0 x); intros.
        apply gt_n_S; apply Degree_not_isolated.
        elim H0; rewrite e; intros.
        case (V_eq_dec x1 y); intros.
        elim H2; rewrite e0; intros.
        split with x2.
        apply (A_in_union_edge _ _ _ _ _ H3).
        apply E_not_set_eq24; auto.

        split with x1.
        apply (A_in_union_edge _ _ _ _ _ H1).
        apply E_not_set_eq24; auto.

        case (V_eq_dec x0 y); intros.
        apply gt_n_S; apply Degree_not_isolated.
        elim H0; rewrite e; intros.
        case (V_eq_dec x x1); intros.
        elim H2; rewrite e0; intros.
        split with x2; apply (A_in_union_edge _ _ _ _ _ H3).
        apply E_not_set_eq14; trivial.

        split with x1; apply (A_in_union_edge _ _ _ _ _ H1).
        apply E_not_set_eq14; trivial.

        apply H; elim H0; intros.
        split with x1.
        apply (A_in_union_edge _ _ _ _ _ H1).
        apply E_not_set_eq123; auto.

        elim H2; intros.
        split with x2.
        apply (A_in_union_edge _ _ _ _ _ H3).
        apply E_not_set_eq123; auto.

        trivial.

        apply H; rewrite e0; trivial.
Qed.

End REMARKABLE_DEGREE.