Require Import Digraphs.

Section DIRECTED_PATHES.

Variable v : V_set.

Variable a : A_set.

Inductive D_walk : Vertex → Vertex → V_list → A_list → Set :=
  | DW_null : ∀ x : Vertex, v x → D_walk x x V_nil A_nil
  | DW_step :
      ∀ (x y z : Vertex) (vl : V_list) (al : A_list),
      D_walk y z vl al →
      a (A_ends x y) → D_walk x z (y :: vl) (A_ends x y :: al).

Definition D_closed_walk :=
  ∀ (x : Vertex) (vl : V_list) (al : A_list), D_walk x x vl al.

Inductive D_trail : Vertex → Vertex → V_list → A_list → Set :=
  | DT_null : ∀ x : Vertex, v x → D_trail x x V_nil A_nil
  | DT_step :
      ∀ (x y z : Vertex) (vl : V_list) (al : A_list),
      D_trail y z vl al →
      a (A_ends x y) →
      ¬ In (A_ends x y) al → D_trail x z (y :: vl) (A_ends x y :: al).

Definition D_closed_trail :=
  ∀ (x : Vertex) (vl : V_list) (al : A_list), D_trail x x vl al.

Inductive D_path : Vertex → Vertex → V_list → A_list → Set :=
  | DP_null : ∀ x : Vertex, v x → D_path x x V_nil A_nil
  | DP_step :
      ∀ (x y z : Vertex) (vl : V_list) (al : A_list),
      D_path y z vl al →
      a (A_ends x y) →
      ¬ In y vl →
      (In x vl → x = z) →
      ¬ In (A_ends x y) al → D_path x z (y :: vl) (A_ends x y :: al).

Definition D_cycle :=
  ∀ (x : Vertex) (vl : V_list) (al : A_list), D_path x x vl al.

Lemma D_trail_isa_walk :
 ∀ (x y : Vertex) (vl : V_list) (al : A_list) (t : D_trail x y vl al),
 D_walk x y vl al.
Proof.
        intros x y vl al t; elim t; intros.
        apply DW_null; trivial.

        apply DW_step; trivial.
Qed.

Lemma D_path_isa_trail :
 ∀ (x y : Vertex) (vl : V_list) (al : A_list) (p : D_path x y vl al),
 D_trail x y vl al.
Proof.
        intros x y vl al p; elim p; intros.
        apply DT_null; trivial.

        apply DT_step; trivial.
Qed.

End DIRECTED_PATHES.