# Library GraphBasics.Dipaths

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.