Require Export Paths.

Section ACYCLIC.

Inductive Acyclic : V_set → A_set → Set :=
  | AC_empty : Acyclic V_empty A_empty
  | AC_vertex :
      ∀ (v : V_set) (a : A_set) (ac : Acyclic v a) (x : Vertex),
      ¬ v x → Acyclic (V_union (V_single x) v) a
  | AC_leaf :
      ∀ (v : V_set) (a : A_set) (ac : Acyclic v a) (x y : Vertex),
      v x →
      ¬ v y → Acyclic (V_union (V_single y) v) (A_union (E_set x y) a)
  | AC_eq :
      ∀ (v v' : V_set) (a a' : A_set),
      v = v' → a = a' → Acyclic v a → Acyclic v' a'.

Lemma Acyclic_Isa_Graph :
 ∀ (v : V_set) (a : A_set), Acyclic v a → Graph v a.
Proof.
        intros a v ac; elim ac; intros.
        apply G_empty.

        apply G_vertex; trivial.

        apply G_edge.
        apply G_vertex; trivial.

        apply V_in_right; trivial.

        apply V_in_left; apply V_in_single.

        red in |- *; intros Heq; elim n; rewrite <- Heq; trivial.

        red in |- *; intros; elim n; apply (G_ina_inv2 v0 a0 H x y); trivial.

        red in |- *; intros; elim n; apply (G_ina_inv1 v0 a0 H y x); trivial.

        apply G_eq with (v := v0) (a := a0); trivial.
Defined.

Lemma AC_ina_inv1 :
 ∀ (v : V_set) (a : A_set) (x y : Vertex),
 Acyclic v a → a (A_ends x y) → v x.
Proof.
        intros v a x y ac H;
         apply (G_ina_inv1 v a (Acyclic_Isa_Graph v a ac) x y);
         trivial.
Qed.

Lemma AC_ina_inv2 :
 ∀ (v : V_set) (a : A_set) (x y : Vertex),
 Acyclic v a → a (A_ends x y) → v y.
Proof.
        intros v a x y ac H;
         apply (G_ina_inv2 v a (Acyclic_Isa_Graph v a ac) x y);
         trivial.
Qed.

End ACYCLIC.

Section ACYCLIC_AND_DEGREES.

Remark AC_vertex_isolated :
 ∀ (v : V_set) (a : A_set) (x : Vertex),
 Acyclic v a →
 ¬ v x →
 Acyclic (V_union (V_single x) v) a → ∀ y : Vertex, ¬ a (A_ends x y).
Proof.
        intros; red in |- *; intros.
        elim H0; apply (AC_ina_inv1 v a x y); trivial.
Qed.

Lemma AC_vertex_degree_zero :
 ∀ (v : V_set) (a : A_set) (ac : Acyclic v a) (x : Vertex) (Hn : ¬ v x),
 degree x (V_union (V_single x) v) a
   (Acyclic_Isa_Graph (V_union (V_single x) v) a (AC_vertex v a ac x Hn)) = 0.
Proof.
        intros; apply Degree_isolated; unfold isolated in |- ×.
        red in |- *; intros; elim Hn.
        apply AC_ina_inv1 with (a := a) (y := y); trivial.
Qed.

Remark AC_edge_pendant :
 ∀ (v : V_set) (a : A_set) (x y : Vertex),
 Acyclic v a →
 v x →
 ¬ v y →
 Acyclic (V_union (V_single y) v) (A_union (E_set x y) a) →
 ∀ z : Vertex, A_union (E_set x y) a (A_ends z y) → z = x.
Proof.
        intros; inversion H3.
        inversion H4; trivial.

        absurd (v y).
        trivial.

        apply (AC_ina_inv2 v a z y); trivial.
Qed.

Lemma AC_edge_degree_one :
 ∀ (v : V_set) (a : A_set) (ac : Acyclic v a)
   (x y : Vertex) (Hp : v x) (Hn : ¬ v y),
 degree y (V_union (V_single y) v) (A_union (E_set x y) a)
   (Acyclic_Isa_Graph (V_union (V_single y) v) (A_union (E_set x y) a)
      (AC_leaf v a ac x y Hp Hn)) = 1.
Proof.
        intros; apply Degree_pendant; unfold pendant in |- ×.
        split with x.
        apply A_in_left; apply E_left.

        intros; inversion H.
        inversion H0; trivial.

        absurd (v y).
        trivial.

        apply AC_ina_inv1 with (a := a) (y := z); trivial.
Qed.

Remark one_le_one : ∀ n : nat, n = 1 → n ≤ 1.
Proof.
        intros; omega.
Qed.

Lemma Acyclic_no_cycle :
 ∀ (v : V_set) (a : A_set) (Ac : Acyclic v a)
   (x y : Vertex) (vl : V_list) (el : E_list) (p : Path v a x y vl el),
 Cycle v a x y vl el p → vl = V_nil.
Proof.
        intros v a Ac; elim Ac; intros.
        inversion p.
        trivial.

        inversion H2.

        case (V_in_dec x (x0 :: vl)); intros.
        apply
         (Path_degree_zero_nil (V_union (V_single x) v0) a0
            (Acyclic_Isa_Graph (V_union (V_single x) v0) a0
               (AC_vertex v0 a0 ac x n)) x0 y vl el p).
        split with x.
        trivial.

        apply AC_vertex_degree_zero.

        cut (Path v0 a0 x0 y vl el); intros.
        apply (H _ _ _ _ H1); intros.
        apply H0.

        apply Path_supergraph_cons_vertex with (z := x).
        trivial.

        red in |- *; intros; elim n0; simpl in |- *; auto.

        red in |- *; intros; elim n0; simpl in |- *; auto.

        case (V_in_dec y (x0 :: vl)); intros.
        apply
         (Cycle_degree_one_nil (V_union (V_single y) v0)
            (A_union (E_set x y) a0)
            (Acyclic_Isa_Graph (V_union (V_single y) v0)
               (A_union (E_set x y) a0) (AC_leaf v0 a0 ac x y v1 n)) x0 y0 vl
            el p H0).
        split with y.
        trivial.

        apply one_le_one.
        apply AC_edge_degree_one.

        cut (Path v0 a0 x0 y0 vl el); intros.
        apply (H _ _ _ _ H1).
        apply H0.

        apply Path_supergraph_cons_arc with (x' := x) (y' := y).
        apply Path_supergraph_cons_vertex with (z := y).
        trivial.

        red in |- *; intros; elim n0; simpl in |- *; auto.

        red in |- *; intros; elim n0; simpl in |- *; auto.

        red in |- *; intros; elim n0;
         apply (P_inxyel_inyvl _ _ _ _ _ _ p x y);
         trivial.

        red in |- *; intros; elim n0;
         apply (P_inxyel_inxvl _ _ _ _ _ _ p y x);
         trivial.

        generalize H; rewrite e; rewrite e0; intros.
        apply (H1 _ _ _ _ p H0).
Qed.

End ACYCLIC_AND_DEGREES.