Require Export Graphs.
Require Export Degrees.

Section PATH.

Variable v : V_set.
Variable a : A_set.

Inductive Walk : Vertex → Vertex → V_list → E_list → Set :=
  | W_null : ∀ x : Vertex, v x → Walk x x V_nil E_nil
  | W_step :
      ∀ (x y z : Vertex) (vl : V_list) (el : E_list),
      Walk y z vl el →
      v x → a (A_ends x y) → Walk x z (y :: vl) (E_ends x y :: el).

Definition Closed_walk (x y : Vertex) (vl : V_list)
  (el : E_list) (w : Walk x y vl el) := x = y.

Inductive Trail : Vertex → Vertex → V_list → E_list → Set :=
  | T_null : ∀ x : Vertex, v x → Trail x x V_nil E_nil
  | T_step :
      ∀ (x y z : Vertex) (vl : V_list) (el : E_list),
      Trail y z vl el →
      v x →
      a (A_ends x y) →
      (∀ u : Edge, In u el → ¬ E_eq u (E_ends x y)) →
      Trail x z (y :: vl) (E_ends x y :: el).

Definition Closed_trail (x y : Vertex) (vl : V_list)
  (el : E_list) (t : Trail x y vl el) := x = y.

Inductive Path : Vertex → Vertex → V_list → E_list → Set :=
  | P_null : ∀ x : Vertex, v x → Path x x V_nil E_nil
  | P_step :
      ∀ (x y z : Vertex) (vl : V_list) (el : E_list),
      Path y z vl el →
      v x →
      a (A_ends x y) →
      x ≠ y →
      ¬ In y vl →
      (In x vl → x = z) →
      (∀ u : Edge, In u el → ¬ E_eq u (E_ends x y)) →
      Path x z (y :: vl) (E_ends x y :: el).

Definition Cycle (x y : Vertex) (vl : V_list) (el : E_list)
  (p : Path x y vl el) := x = y.

Lemma P_iny_vl :
 ∀ (x y : Vertex) (vl : V_list) (el : E_list),
 Path x y vl el → vl ≠ V_nil → In y vl.
Proof.
        intros x y vl el p; elim p; intros.
        absurd (V_nil = V_nil); auto.

        inversion p0.
        simpl in |- *; auto.

        rewrite H10; simpl in |- *; right.
        apply H; rewrite <- H10; discriminate.
Qed.

Lemma P_endx_inv :
 ∀ (x y : Vertex) (vl : V_list) (el : E_list), Path x y vl el → v x.
Proof.
        intros x y vl el p; elim p; auto.
Qed.

Lemma P_endy_inv :
 ∀ (x y : Vertex) (vl : V_list) (el : E_list), Path x y vl el → v y.
Proof.
        intros x y vl el p; elim p; auto.
Qed.

Lemma P_invl_inv :
 ∀ (x y : Vertex) (vl : V_list) (el : E_list),
 Path x y vl el → ∀ z : Vertex, In z vl → v z.
Proof.
        intros x y vl el p; elim p; intros.
        inversion H.

        inversion H0.
        rewrite <- H1; apply (P_endx_inv _ _ _ _ p0).

        auto.
Qed.

Lemma P_inel_ina :
 ∀ (x y : Vertex) (vl : V_list) (el : E_list),
 Path x y vl el →
 ∀ x' y' : Vertex, In (E_ends x' y') el → a (A_ends x' y').
Proof.
        intros x y vl el p; elim p; intros.
        inversion H.

        inversion H0.
        inversion H1.
        rewrite <- H3; rewrite <- H4; trivial.

        auto.
Qed.

Lemma P_inxyel_inxvl :
 ∀ (x y : Vertex) (vl : V_list) (el : E_list),
 Path x y vl el →
 ∀ x' y' : Vertex, In (E_ends x' y') el → In x' (x :: vl).
Proof.
        intros x y vl el p; elim p; intros.
        inversion H.

        inversion H0.
        inversion H1.
        simpl in |- *; auto.

        simpl in |- *; right.
        apply (H x' y'); auto.
Qed.

Lemma P_inxyel_inyvl :
 ∀ (x y : Vertex) (vl : V_list) (el : E_list),
 Path x y vl el →
 ∀ x' y' : Vertex, In (E_ends x' y') el → In y' (x :: vl).
Proof.
        intros x y vl el p; elim p; intros.
        inversion H.

        inversion H0.
        inversion H1.
        simpl in |- *; auto.

        simpl in |- *; right.
        apply (H x' y'); auto.
Qed.

Lemma P_backstep :
 ∀ (x y z : Vertex) (vl : V_list) (el : E_list),
 Path x z (y :: vl) el → {el' : E_list & Path y z vl el'}.
Proof.
        intros; inversion H.
        split with el0; trivial.
Qed.

Lemma Trail_isa_walk :
 ∀ (x y : Vertex) (vl : V_list) (el : E_list),
 Trail x y vl el → Walk x y vl el.
Proof.
        intros x y vl el t; elim t; intros.
        apply W_null; trivial.

        apply W_step; trivial.
Qed.

Lemma Path_isa_trail :
 ∀ (x y : Vertex) (vl : V_list) (el : E_list),
 Path x y vl el → Trail x y vl el.
Proof.
        intros x y vl el t; elim t; intros.
        apply T_null; trivial.

        apply T_step; trivial.
Qed.

End PATH.

Section EXTRACTED.

Variable v : V_set.
Variable a : A_set.

Fixpoint V_extract (x : Vertex) (vl : V_list) {struct vl} : V_list :=
  match vl with
  | nil ⇒ V_nil
  | y :: vl' ⇒
      if V_in_dec x vl' then V_extract x vl' else vl'
  end.

Lemma P_extract :
 ∀ (x y z : Vertex) (vl : V_list) (el : E_list),
 Path v a y z vl el →
 In x (y :: vl) → {el' : E_list & Path v a x z (V_extract x (y :: vl)) el'}.
Proof.
        intros x y z vl; generalize y; elim vl; simpl in |- *; intros.
        split with el.
        replace x with y0; auto.
        case (V_in_dec y0 nil); auto.

        tauto.

        elim (P_backstep _ _ _ _ _ _ _ H0); intros.
        case (V_in_dec x (a0 :: l)). intros.
        apply (H a0 x0); auto.

        simpl in |- ×. intros. split with el. replace x with y0.
        trivial.

        tauto.
Qed.

Remark P_when_cycle :
 ∀ (x y : Vertex) (vl : V_list) (el : E_list),
 Path v a x y vl el → In x vl → x = y.
Proof.
        intros x y vl el H; inversion H; intros.
        trivial.

        inversion H11.
        absurd (x = y0); auto.

        auto.
Qed.

Lemma Walk_to_path :
 ∀ (x y : Vertex) (vl : V_list) (el : E_list),
 Walk v a x y vl el →
 {vl0 : V_list & {el0 : E_list & Path v a x y vl0 el0}}.
Proof.
        intros x y vl el w; elim w; intros.
        split with V_nil; split with E_nil; apply P_null; trivial.

        elim H; clear H; intros vl' H.
        elim H; clear H; intros el' H.
        case (V_in_dec x0 (y0 :: vl')); intros.
        elim (P_extract _ _ _ _ _ H i); intros.
        split with (V_extract x0 (y0 :: vl')); split with x1; auto.

        case (V_in_dec y0 vl'); intros.
        split with (y0 :: V_nil); split with (E_ends x0 y0 :: E_nil). apply P_step.
        replace z with y0.
        apply P_null; apply (P_endx_inv _ _ _ _ _ _ H).

        apply (P_when_cycle _ _ _ _ H); auto.

        trivial.

        trivial.

        red in |- *; intros; elim n; rewrite H0; simpl in |- *; auto.

        tauto.

        simpl in |- ×. tauto.

        tauto.

        split with (y0 :: vl'); split with (E_ends x0 y0 :: el').
        apply P_step.
        trivial.

        trivial.

        trivial.

        red in |- *; intros; elim n; rewrite H0; simpl in |- *; auto.

        trivial.

        intros; absurd (In x0 vl').
        red in |- *; intros; elim n; simpl in |- *; auto.

        trivial.

        red in |- *; intros.
        elim n; inversion H1.
        apply (P_inxyel_inxvl _ _ _ _ _ _ H x0 y0).
        rewrite <- H3; auto.

        apply (P_inxyel_inyvl _ _ _ _ _ _ H y0 x0).
        rewrite <- H4; rewrite <- H5; rewrite H2; trivial.
Qed.

End EXTRACTED.

Section PATH_AND_DEGREE.

Variable v : V_set.
Variable a : A_set.
Variable g : Graph v a.

Lemma Path_degree_one :
 ∀ (x y : Vertex) (vl : V_list) (el : E_list),
 Path v a x y vl el → ∀ z : Vertex, In z vl → degree z v a g > 0.
Proof.
        intros x y vl el p; elim p; intros.
        inversion H.

        inversion H0.
        rewrite <- H1; apply Degree_not_isolated.
        split with x0; apply (G_non_directed v a g); trivial.

        apply H; auto.
Qed.

Lemma Path_consx_degree_one :
 ∀ (x y : Vertex) (vl : V_list) (el : E_list),
 Path v a x y vl el →
 vl ≠ V_nil → ∀ z : Vertex, In z (x :: vl) → degree z v a g > 0.
Proof.
        simple destruct vl; intros.
        absurd (nil = V_nil); auto.

        inversion H1.
        rewrite <- H2; apply Degree_not_isolated.
        inversion H; split with v0; trivial.

        apply (Path_degree_one x y (v0 :: l) el H); auto.
Qed.

Lemma Path_degree_two :
 ∀ (x y : Vertex) (vl : V_list) (el : E_list),
 Path v a x y vl el →
 ∀ z : Vertex, In z vl → z ≠ y → degree z v a g > 1.
Proof.
        intros x y vl el p; elim p; intros.
        inversion H.

        inversion H0.
        inversion p0.
        absurd (z0 = z).
        trivial.

        rewrite <- H2; auto.

        rewrite <- H2; apply Degree_not_pendant.
        split with x0.
        apply (G_non_directed v a g); trivial.

        split with y1.
        trivial.

        red in |- *; intros.
        elim (n1 (E_ends y0 y1)).
        rewrite <- H13; simpl in |- *; auto.

        rewrite H14; apply E_rev.

        apply H; trivial.
Qed.

Lemma Path_last_step :
 ∀ (x y : Vertex) (vl : V_list) (el : E_list) (p : Path v a x y vl el),
 el ≠ E_nil → ∃ z : Vertex, In (E_ends z y) el.
Proof.
        intros x y vl el p; elim p.
        intros; elim H; trivial.

        simple destruct el0; intros.
        split with x0.
        inversion p0.
        simpl in |- *; left; trivial.

        elim H; intros.
        split with x1.
        simpl in |- *; auto.

        discriminate.
Qed.

Lemma Cycle_degree_two :
 ∀ (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 → ∀ z : Vertex, In z vl → degree z v a g > 1.
Proof.
        intros; case (V_eq_dec z y); intros.
        rewrite e; apply Degree_not_pendant.
        inversion p.
        rewrite <- H4 in H0; inversion H0.

        inversion H.
        split with y0.
        rewrite <- H12; trivial.

        elim (Path_last_step y0 y vl0 el0 H1); intros.
        split with x1.
        apply (G_non_directed v a g); apply (P_inel_ina v a y0 y vl0 el0 H1);
         trivial.

        red in |- *; intros; elim (H7 (E_ends x1 y)).
        trivial.

        rewrite H12; rewrite H14; apply E_rev.

        inversion H1.
        absurd (x = y0).
        trivial.

        rewrite H15; trivial.

        discriminate.

        apply (Path_degree_two x y vl el p); trivial.
Qed.

Lemma Cycle_consx_degree_two :
 ∀ (x y : Vertex) (vl : V_list) (el : E_list) (p : Path v a x y vl el),
 vl ≠ V_nil →
 Cycle v a x y vl el p →
 ∀ z : Vertex, In z (x :: vl) → degree z v a g > 1.
Proof.
        intros; inversion H1.
        rewrite <- H2; inversion H0.
        apply (Cycle_degree_two x y vl el p H0 y).
        apply (P_iny_vl v a x y vl el p); trivial.

        apply (Cycle_degree_two x y vl el p H0); trivial.
Qed.

Lemma Path_degree_zero_nil :
 ∀ (x y : Vertex) (vl : V_list) (el : E_list),
 Path v a x y vl el →
 (exists2 z : Vertex, In z (x :: vl) & degree z v a g = 0) → vl = V_nil.
Proof.
        simple destruct vl; intros.
        trivial.

        elim H0; intros.
        absurd (degree x0 v a g > 0).
        omega.

        apply (Path_consx_degree_one _ _ _ _ H).
        discriminate.

        trivial.
Qed.

Lemma Cycle_degree_one_nil :
 ∀ (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 →
 (exists2 z : Vertex, In z (x :: vl) & degree z v a g ≤ 1) → vl = V_nil.
Proof.
        simple destruct vl; intros.
        trivial.

        elim H0; intros.
        absurd (degree x0 v a g > 1).
        omega.

        apply (Cycle_consx_degree_two _ _ _ _ p).
        discriminate.

        trivial.

        trivial.
Qed.

End PATH_AND_DEGREE.

Section PATH_EQ.

Lemma Walk_eq :
 ∀ (v v' : V_set) (a a' : A_set) (x y : Vertex)
   (vl : V_list) (el : E_list),
 Walk v a x y vl el → v = v' → a = a' → Walk v' a' x y vl el.
Proof.
        intros; elim H; intros.
        apply W_null.
        rewrite <- H0; trivial.

        apply W_step.
        trivial.

        rewrite <- H0; trivial.

        rewrite <- H1; trivial.
Qed.

Lemma Trail_eq :
 ∀ (v v' : V_set) (a a' : A_set) (x y : Vertex)
   (vl : V_list) (el : E_list),
 Trail v a x y vl el → v = v' → a = a' → Trail v' a' x y vl el.
Proof.
        intros; elim H; intros.
        apply T_null.
        rewrite <- H0; trivial.

        intros; apply T_step.
        trivial.

        rewrite <- H0; trivial.

        rewrite <- H1; trivial.

        trivial.
Qed.

Lemma Path_eq :
 ∀ (v v' : V_set) (a a' : A_set) (x y : Vertex)
   (vl : V_list) (el : E_list),
 Path v a x y vl el → v = v' → a = a' → Path v' a' x y vl el.
Proof.
        intros; elim H; intros.
        apply P_null.
        rewrite <- H0; trivial.

        intros; apply P_step.
        trivial.

        rewrite <- H0; trivial.

        rewrite <- H1; trivial.

        trivial.

        trivial.

        trivial.

        trivial.
Qed.

End PATH_EQ.

Section PATH_IN_A_SUBGRAPH.

Lemma Walk_subgraph :
 ∀ (v v' : V_set) (a a' : A_set) (x y : Vertex)
   (vl : V_list) (el : E_list),
 Walk v a x y vl el →
 V_included v v' → A_included a a' → Walk v' a' x y vl el.
Proof.
        intros; elim H; intros.
        apply W_null; apply (H0 x0); trivial.

        apply W_step.
        trivial.

        apply (H0 x0); trivial.

        apply (H1 (A_ends x0 y0)); trivial.
Qed.

Lemma Trail_subgraph :
 ∀ (v v' : V_set) (a a' : A_set) (x y : Vertex)
   (vl : V_list) (el : E_list),
 Trail v a x y vl el →
 V_included v v' → A_included a a' → Trail v' a' x y vl el.
Proof.
        intros; elim H; intros.
        apply T_null; apply (H0 x0); trivial.

        apply T_step.
        trivial.

        apply (H0 x0); trivial.

        apply (H1 (A_ends x0 y0)); trivial.

        trivial.
Qed.

Lemma Path_subgraph :
 ∀ (v v' : V_set) (a a' : A_set) (x y : Vertex)
   (vl : V_list) (el : E_list),
 Path v a x y vl el →
 V_included v v' → A_included a a' → Path v' a' x y vl el.
Proof.
        intros; elim H; intros.
        apply P_null; apply (H0 x0); trivial.

        apply P_step.
        trivial.

        apply (H0 x0); trivial.

        apply (H1 (A_ends x0 y0)); trivial.

        trivial.

        trivial.

        trivial.

        trivial.
Qed.

Lemma Path_supergraph_vertex :
 ∀ (v v' : V_set) (a : A_set) (x y : Vertex) (vl : V_list) (el : E_list),
 Path v a x y vl el →
 v' x → (∀ z : Vertex, In z vl → v' z) → Path v' a x y vl el.
Proof.
        intros v v' a x y vl el p; elim p; intros.
        apply P_null; trivial.

        apply P_step.
        apply H.
        apply H1; simpl in |- *; auto.

        intros; apply H1; simpl in |- *; auto.

        trivial.

        trivial.

        trivial.

        trivial.

        trivial.

        trivial.
Qed.

Lemma Path_supergraph_cons_vertex :
 ∀ (v : V_set) (a : A_set) (x y z : Vertex) (vl : V_list) (el : E_list),
 Path (V_union (V_single z) v) a x y vl el →
 z ≠ x → ¬ In z vl → Path v a x y vl el.
Proof.
        intros v a x y z vl el p; elim p; intros.
        apply P_null.
        inversion v0.
        inversion H1; absurd (z = x0); auto.

        trivial.

        apply P_step.
        apply H.
        red in |- *; intros; elim H1.
        rewrite H2; simpl in |- *; auto.

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

        inversion v0.
        inversion H2; absurd (z = x0); auto.

        trivial.

        trivial.

        trivial.

        trivial.

        trivial.

        trivial.
Qed.

Lemma Path_supergraph_arc :
 ∀ (v v' : V_set) (a a' : A_set) (x y : Vertex)
   (vl : V_list) (el : E_list),
 Path v a x y vl el →
 Graph v' a' →
 v' x →
 (∀ x' y' : Vertex, In (E_ends x' y') el → a' (A_ends x' y')) →
 Path v' a' x y vl el.
Proof.
        intros v v' a a' x y vl el p; elim p; intros.
        apply P_null; trivial.

        apply P_step.
        apply H.
        trivial.

        apply (G_ina_inv2 v' a' H0 x0 y0).
        apply H2; simpl in |- *; auto.

        intros; apply H2; simpl in |- *; auto.

        trivial.

        apply H2; simpl in |- *; auto.

        trivial.

        trivial.

        trivial.

        trivial.
Qed.

Lemma Path_supergraph_cons_arc :
 ∀ (v : V_set) (a : A_set) (x y x' y' : Vertex)
   (vl : V_list) (el : E_list),
 Path v (A_union (E_set x' y') a) x y vl el →
 ¬ In (E_ends x' y') el → ¬ In (E_ends y' x') el → Path v a x y vl el.
Proof.
        intros v a x y x' y' vl el p; elim p; intros.
        apply P_null; trivial.

        apply P_step.
        apply H.
        red in |- *; intros; elim H0.
        simpl in |- *; auto.

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

        trivial.

        inversion a0.
        inversion H2.
        absurd (In (E_ends x' y') (E_ends x0 y0 :: el0)).
        trivial.

        rewrite H5; rewrite H6; simpl in |- *; auto.

        absurd (In (E_ends y' x') (E_ends x0 y0 :: el0)).
        trivial.

        rewrite H5; rewrite H6; simpl in |- *; auto.

        trivial.

        trivial.

        trivial.

        trivial.

        trivial.
Qed.

End PATH_IN_A_SUBGRAPH.

Section APPEND_WALKS.

Variable v : V_set.
Variable a : A_set.

Lemma Walk_append :
 ∀ (x y z : Vertex) (vl vl' : V_list) (el el' : E_list),
 Walk v a x y vl el →
 Walk v a y z vl' el' → Walk v a x z (vl ++ vl') (el ++ el').
Proof.
        intros x y z vl vl' el el' Hw; elim Hw; simpl in |- *; intros.
        trivial.

        apply W_step; auto.
Qed.

End APPEND_WALKS.

Section REVERSE_WALK.

Variable v : V_set.
Variable a : A_set.
Variable g : Graph v a.

Definition cdr (vl : V_list) : V_list :=
  match vl with
  | nil ⇒ V_nil
  | x :: vl' ⇒ vl'
  end.

Lemma cdr_app :
 ∀ vl vl' : V_list, vl ≠ V_nil → cdr (vl ++ vl') = cdr vl ++ vl'.
Proof.
        simple induction vl; simpl in |- *; intros.
        absurd (V_nil = V_nil); auto.

        trivial.
Qed.

Fixpoint E_reverse (el : E_list) : E_list :=
  match el with
  | nil ⇒ E_nil
  | E_ends x y :: el' ⇒ E_reverse el' ++ E_ends y x :: E_nil
  end.

Lemma G_ends_in : ∀ x y : Vertex, a (A_ends x y) → v x.
Proof.
        elim g; intros.
        inversion H.

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

        apply V_in_right; apply (H x0 y); trivial.

        inversion H0.
        inversion H1; rewrite <- H4; trivial.

        apply (H x0 y0); trivial.

        rewrite <- e; apply (H x y); rewrite e0; trivial.
Qed.

Lemma Walk_reverse :
 ∀ (x y : Vertex) (vl : V_list) (el : E_list),
 Walk v a x y vl el → Walk v a y x (cdr (rev (x :: vl))) (E_reverse el).
Proof.
        intros; elim H; simpl in |- *; intros.
        apply W_null; trivial.

        rewrite cdr_app.
        apply (Walk_append v a z y0 x0).
        trivial.

        apply W_step.
        apply W_null; trivial.

        apply (G_ina_inv2 v a g x0 y0); trivial.

        apply (G_non_directed v a g); trivial.

        case (rev vl0); intros; simpl in |- *; discriminate.
Qed.

End REVERSE_WALK.