# Library Path

Require Import Utf8.
Require Export Graph.
Require Import Common.

Set Implicit Arguments.

Generalizable All Variables.

# Paths

We use the dependently typed formulation of graphs
Section path.
Variable V : Type.
Variable E : VVType.

Inductive path (s : V) : VType :=
| NoEdges : path s s
| AddEdge : d d', path s dE d d'path s d'.

Fixpoint prepend s d (p : path s d) : s', E s' spath s' d :=
match p with
| NoEdgesfun _ E'AddEdge (NoEdges _) E'
| AddEdge _ _ p' Efun _ E'AddEdge (prepend p' E') E
end.

Fixpoint concatenate s d d' (p : path s d) (p' : path d d') : path s d' :=
match p' with
| NoEdgesp
| AddEdge _ _ p' EAddEdge (concatenate p p') E
end.

Fixpoint concatenate' s d (p : path s d) : d', path d d'path s d' :=
match p with
| NoEdgesfun _ p'p'
| AddEdge _ _ p Efun _ p'concatenate' p (prepend p' E)
end.

Variable typeOf : VType.
Variable functionOf : s d, E s dtypeOf stypeOf d.

Fixpoint compose_path s d (p : path s d) : typeOf stypeOf d :=
match p with
| NoEdgesfun xx
| AddEdge _ _ p' Efun xfunctionOf E (compose_path p' x)
end.
End path.

Arguments NoEdges [V E s].
Arguments AddEdge [V E s d d'] _ _.
Arguments prepend [V E s d] p [s'] p'.

Section path_Theorems.
Variable V : Type.
Variable E : VVType.

Lemma concatenate_noedges_p s d (p : path E s d) : concatenate NoEdges p = p.
Proof.
induction p; t.
Qed.

Lemma concatenate_p_noedges s d (p : path E s d) : concatenate p NoEdges = p.
Proof.
t.
Qed.

Lemma concatenate'_p_addedge s d d' d''
(p : path E s d)
(p' : path E d d')
(e : E d' d'') :
concatenate' p (AddEdge p' e) = AddEdge (concatenate' p p') e.
Proof.
induction p; t.
Qed.

Lemma concatenate'_p_noedges s d (p : path E s d) : concatenate' p NoEdges = p.
Proof.
induction p; t.
Qed.

Lemma concatenate'_noedges_p s d (p : path E s d) : concatenate' NoEdges p = p.
Proof.
t.
Qed.

Hint Rewrite concatenate'_p_noedges.

Lemma concatenate_addedge_concatenate'_prepend s d d'0 d'
(p : path E s d)
(e : E d d'0)
(p' : path E d'0 d') :
concatenate (AddEdge p e) p' = concatenate' p (prepend p' e).
Proof.
induction p'; t.
Qed.

Hint Resolve concatenate_noedges_p concatenate_addedge_concatenate'_prepend.

Lemma concatenate_concatenate'_equivalent s d d'
(p : path E s d)
(p' : path E d d') :
concatenate p p' = concatenate' p p'.
Proof.
induction p; t.
Qed.

Hint Rewrite concatenate_noedges_p concatenate_addedge_concatenate'_prepend.
Hint Rewrite <- concatenate_concatenate'_equivalent.

Lemma concatenate_p_addedge s d d' d''
(p : path E s d)
(p' : path E d d')
(e : E d' d'') :
concatenate p (AddEdge p' e) = AddEdge (concatenate p p') e.
Proof.
induction p; t.
Qed.

Lemma concatenate_prepend_p s s' d d'
(p1 : path E s' d)
(p2 : path E d d')
(e : E s s') :
(prepend (concatenate p1 p2) e) = (concatenate (prepend p1 e) p2).
Proof.
induction p1; t.
Qed.

Hint Rewrite concatenate_prepend_p.

Lemma concatenate_associative o1 o2 o3 o4
(p1 : path E o1 o2)
(p2 : path E o2 o3)
(p3 : path E o3 o4) :
(concatenate (concatenate p1 p2) p3) = (concatenate p1 (concatenate p2 p3)).
Proof.
induction p1; t.
Qed.

Lemma compose_path_addedge s d d' (p : path E s d) (e : E _ d') typeOf functionOf
: x,
compose_path typeOf functionOf (AddEdge p e) x
= functionOf _ _ e (compose_path typeOf functionOf p x).
Proof.
induction p; t_with t'.
Qed.

Lemma compose_path_prepend s' s d (p : path E s d) (e : E s' _) typeOf functionOf
: x,
compose_path typeOf functionOf (prepend p e) x
= (compose_path typeOf functionOf p (functionOf _ _ e x)).
Proof.
induction p; t_with t'.
Qed.
End path_Theorems.

Hint Rewrite compose_path_prepend compose_path_addedge.
Hint Rewrite concatenate_p_noedges concatenate_noedges_p.
Hint Resolve concatenate_p_noedges concatenate_noedges_p.

Definition PathsOf (G : Graph)
:= { sd : G × G & @path G (Edge G) (fst sd) (snd sd) }.