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 : forall x : Vertex, v x -> D_walk x x V_nil A_nil
  | DW_step :
      forall (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 :=
  forall (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 : forall x : Vertex, v x -> D_trail x x V_nil A_nil
  | DT_step :
      forall (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 :=
  forall (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 : forall x : Vertex, v x -> D_path x x V_nil A_nil
  | DP_step :
      forall (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 :=
  forall (x : Vertex) (vl : V_list) (al : A_list), D_path x x vl al.

Lemma D_trail_isa_walk :
 forall (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 :
 forall (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.