Library Paths

Require Import DigraphInterface.
Require Import OrderedType.
Require Import ZArith.
Require Import OrderedTypeEx.
Require Import Graph_Properties.
Require Import Labels.

Module Path (Vertex : OrderedType) (Lab : Labels with Definition EdgeLabel := nat)
                    (G : Directed_Graph Vertex Lab).

Import G Edge.

Module Import P := GraphProps Vertex Lab G.


Definition eval o := match o with
| None => 1
| Some w => w
end.

Inductive path : list Edge.t -> Vertex.t -> Vertex.t -> G.t -> nat -> Prop :=
| path_self : forall v1 v2 g, Vertex.eq v1 v2 -> path nil v1 v2 g 0
| path_post : forall p v1 v2 v3 val w g e , path p v1 v2 g val ->
                                                             In_graph_labeled_edge (v2,v3) g w ->
                                                             Edge.eq e (v2,v3) ->
                                                             path (p++ e :: nil) v1 v3 g (val + eval w).

Lemma path_nil_eq_end : forall v v' g val,
path nil v v' g val -> Vertex.eq v v' /\ val = 0.

Proof.
  intros.
  inversion H; subst.
    intuition.
    eelim app_cons_not_nil; eauto.
Qed.

Lemma path_snd_ext : forall p x y g val,
path p x y g val ->
forall z, Vertex.eq y z ->
path p x z g val.

Proof.
intros p x y g val H z H0. rewrite <-(rev_involutive p) in *. induction (rev p). simpl in *.
inversion H. subst. constructor. rewrite <-H0. auto. auto.
eelim app_cons_not_nil. eauto.
simpl. simpl in H. inversion H; subst. eelim app_cons_not_nil. eauto.

intros. apply path_post with (v2 := v2) (val := val0) (w := w). auto.
assert (Edge.eq (v2,z) (v2,y)).
split; auto.
rewrite H5; auto.
rewrite H4. split; auto.
Qed.

Lemma path_trans : forall v1 v2 v3 g p1 p2 val1 val2,
path p1 v1 v2 g val1 ->
path p2 v2 v3 g val2 ->
path (p1 ++ p2) v1 v3 g (val1 + val2).

Proof.
  induction 2; intros.
    rewrite app_nil_r.
    rewrite plus_0_r.
    apply path_snd_ext with (y := v0); assumption.
    rewrite app_assoc. replace (val1 + (val + eval w)) with (val1 + val + eval w).
      apply path_post with (v2 := v2).
        apply IHpath; auto.
        auto.
      auto.
    intuition.
Qed.

Lemma decompose_app : forall l l' (x x' : Edge.t),
l ++ x :: nil = l' ++ x' :: nil ->
l = l' /\ x = x'.

Proof.
  induction l; intros. simpl in H.
  induction l'.
    inversion H; subst; intuition.
    inversion H; subst. eelim app_cons_not_nil; eauto.
  induction l'. simpl in H.
    inversion H. eelim app_cons_not_nil; eauto.
    simpl in H. inversion H. subst.
    destruct (IHl _ _ _ H2). subst. intuition.
Qed.

Lemma path_edge_charac : forall e p v v' g val,
path (e :: p) v v' g val ->
exists v'', exists w, Edge.eq e (v, v'') /\ In_graph_labeled_edge e g w.

Proof.
  intros. rewrite <-(rev_involutive (e :: p)) in H. simpl in H.
  generalize v v' g val H. clear H.
  induction (rev p). intros.
    inversion H. subst.
    rewrite <-app_nil_l in H0.
    generalize (decompose_app _ _ _ _ H0). intro. destruct H4 as [H5 HH4]. subst.
    generalize (path_nil_eq_end _ _ _ _ H1). intro. destruct H4. subst.
    exists v'0. exists w. split.
      eapply Edge.eq_trans. eassumption.
      split; auto.
      rewrite H3. assumption.
  intros. inversion H; subst.
    eelim app_cons_not_nil; eauto.
    cut (p0 = rev (l ++ e :: nil)).
      intro. subst. apply (IHl _ _ _ _ H1).
      eapply decompose_app. eassumption.
Qed.

Lemma path_eqlistA : forall p r v g val,
path p r v g val ->
forall p',
(eqlistA Edge.eq p' p ->
path p' r v g val).

Proof.
  intros p r v g val H. induction H.
    intros. inversion H0. subst. constructor. auto.
    intros. replace (p ++ e :: nil) with (rev (e :: rev p)) in H2.
      rewrite <-(rev_involutive p') in H2.
      generalize (eqlistA_rev H2). intro.
      do 2 rewrite rev_involutive in H3.
      rewrite <-(rev_involutive p').
      induction (rev p').
        inversion H3.
        inversion H3. subst.
        generalize (eqlistA_rev H9). rewrite rev_involutive. intro.
        generalize (IHpath _ H4). intro. simpl.
        apply path_post with (v2 := v2) (val := val) (w := w); auto.
        apply Edge.eq_trans with (y := e); auto.
      simpl. rewrite rev_involutive. reflexivity.
Qed.

Lemma pos_edge_pos_path : forall p v v' g val,
path p v v' g val ->
(forall a b c, In_graph_labeled_edge (a,b) g (Some c) -> 0 <= c) ->
0 <= val.

Proof.
  induction 1.
    intros. left.
  intros. apply le_trans with (m := val).
    apply IHpath. auto.
    intuition.
Qed.

Lemma In_graph_edge_equiv : forall e g l,
In_graph_labeled_edge e g l -> In_graph_edge e g.

Proof.
 intros.
 rewrite In_graph_labeled_edge_spec in H.
 rewrite In_graph_edge_spec.
 apply EMapFacts.MapsTo_In with (e := l). assumption.
Qed.

Add Morphism edge_label : edge_label_m.

Proof.
  intros. do 2 rewrite edge_label_spec.
  rewrite EMapFacts.find_o with (y := y);[reflexivity | assumption].
Qed.

Add Morphism vertex_label : vertex_label_m.

Proof.
  intros. do 2 rewrite vertex_label_spec.
  rewrite MapFacts.find_o with (y := y);[reflexivity | assumption].
Qed.

Lemma in_path_in_graph : forall p e v v' g val,
InA Edge.eq e p ->
path p v v' g val ->
In_graph_edge e g.

Proof.
intros.
rewrite <-(rev_involutive p) in *.
generalize v v' val H H0. clear v v' val H H0.
induction (rev p); intros. inversion H.
simpl in H0. inversion H0; subst.
eelim app_cons_not_nil. eauto.
generalize (decompose_app _ _ _ _ H1). clear H1. intro. inversion H1; subst.
simpl in H. generalize (InA_app _ H). intro.
destruct H5. eapply IHl. auto. eauto.
inversion H5; subst.
rewrite H7. rewrite H4. eapply In_graph_edge_equiv. eassumption.
inversion H7.
Qed.

Lemma path_ends_in_graph : forall p v v' g val,
path p v v' g val ->
p <> nil ->
In_graph_vertex v g /\ In_graph_vertex v' g.

Proof.
intros. induction H.
congruence.
destruct p. inversion H. subst.
split. rewrite H3.
assert (In_graph_edge (v2,v3) g).
eapply In_graph_labeled_edge_weak; eauto.
destruct (In_graph_edge_in_ext _ _ H4); simpl in *; auto.
assert (In_graph_edge (v2,v3) g).
eapply In_graph_labeled_edge_weak; eauto.
destruct (In_graph_edge_in_ext _ _ H4); simpl in *; auto.
elim (app_cons_not_nil _ _ _ (sym_eq H3)).
assert (In_graph_vertex v1 g /\ In_graph_vertex v2 g).
apply IHpath. congruence.
split. intuition.
assert (In_graph_edge (v2,v3) g).
eapply In_graph_labeled_edge_weak; eauto.
destruct (In_graph_edge_in_ext _ _ H4); simpl in *; auto.
Qed.

Lemma path_value_ge_edge : forall p v v' g val,
path p v v' g val ->
forall v1 v2 w,
In (v1,v2) p ->
edge_label (v1,v2) g = Some w ->
eval w <= val.

Proof.
intros. induction H. inversion H0.
destruct (in_app_or _ _ _ H0).
eapply le_trans. apply IHpath. auto. auto. intuition.
rewrite <-H3 in H2. apply le_trans with (m := eval w0).
inversion H4. subst.
rewrite (labeled_edge_edge_label (v1,v2) g w0 w); auto.
inversion H5.
intuition.
Qed.

Lemma minus_plus_plus_minus : forall x y z,
y <= x ->
x - y + z = x + z - y.

Proof.
induction x; intros. simpl.
inversion H; subst. intuition.
destruct y. simpl. auto.
apply IHx. intuition.
Qed.

Lemma path_end : forall p v1 v2 v w g val,
path ((v1,v2) :: p) v1 v g val ->
edge_label (v1,v2) g = Some w ->
path p v2 v g (val - eval w).

Proof.
intros p v1 v2 v w g val H HH. rewrite <-(rev_involutive p) in *.
generalize v1 v2 w v val H HH. clear v v1 v2 w val H HH.
induction (rev p); intros. simpl in *.
inversion H; subst.
replace ((v1,v2) :: nil) with (nil ++ (v1,v2) :: nil) in H0.
generalize (decompose_app _ _ _ _ H0); intros. destruct H4; subst. clear H0.
generalize (path_nil_eq_end _ _ _ _ H1). intro. destruct H0; subst.
simpl. rewrite <-H3 in *. rewrite (labeled_edge_edge_label (v1,v2) g _ _ H2 HH) in *; auto.
simpl in *. rewrite minus_diag.
constructor. inversion H3; auto.
auto.

simpl in H. inversion H; subst.
rewrite app_comm_cons in H0. generalize (decompose_app _ _ _ _ H0); intros.
destruct H4; subst; clear H0.
simpl.
cut (path (rev l ++ (v3,v) :: nil) v2 v g (val0+ eval w0-eval w)). intro.
eapply path_eqlistA. eapply H0.
apply eqlistA_app. intuition. intuition.
constructor. auto. constructor.
generalize (IHl _ _ w _ _ H1). intro.
replace (val0 + eval w0 - eval w) with (val0 - eval w + eval w0).
eapply path_post. eauto. auto. apply Edge.eq_refl.
apply minus_plus_plus_minus.
eapply (path_value_ge_edge ((v1,v2) :: rev l) v1 v3 g val0); auto.
constructor. auto. auto.
Qed.

Lemma path_shorten_1 : forall p1 p2 v1 v2 v3 v4 g val,
path (p1 ++ (v3,v4) :: p2) v1 v2 g val ->
exists val', path (p1 ++ (v3, v4) :: nil) v1 v4 g val' /\ val' <= val.

Proof.
intros.
rewrite <-(rev_involutive p2) in H.
generalize v1 v2 val H. clear v1 v2 val H.
induction (rev p2); intros. simpl in H. exists val.
inversion H; subst.
eelim app_cons_not_nil. eauto.
generalize (decompose_app _ _ _ _ H0). intro. destruct H4; subst.
split.
inversion H3; simpl in *; destruct H0.
eapply path_snd_ext. eauto. auto. auto.

simpl in H; inversion H; subst.
eelim app_cons_not_nil. eauto.
rewrite app_comm_cons in H0. rewrite ass_app in H0.
generalize (decompose_app _ _ _ _ H0). clear H0. intro. destruct H0; subst.
destruct (IHl _ _ _ H1). destruct H0.
exists x. split. auto. intuition.
Qed.

Lemma path_shorten_2 : forall p1 p2 v1 v2 v3 v4 g val,
path (p1 ++ (v3,v4) :: p2) v1 v2 g val ->
exists val', path p1 v1 v3 g val' /\ val' <= val.

Proof.
intros.
generalize (path_shorten_1 _ _ _ _ _ _ _ _ H). intro. do 2 destruct H0.
inversion H0; subst.
eelim app_cons_not_nil. eauto.
generalize (decompose_app _ _ _ _ H2). clear H2. intros. destruct H2; subst.
exists val0. split. eapply path_snd_ext. eassumption.
inversion H5; intuition.
intuition.
Qed.

Lemma path_value_eq : forall p v1 v2 v1' v2' g val val',
path p v1 v2 g val ->
path p v1' v2' g val' ->
val = val'.

Proof.
intros. rewrite <-(rev_involutive p) in *.
generalize v1 v2 v1' v2' val val' H H0. clear v1 v2 v1' v2' val val' H H0.
induction (rev p); intros. simpl in *.
inversion H; subst.
inversion H0; subst. auto.
eelim app_cons_not_nil. eauto.
eelim app_cons_not_nil. eauto.
simpl in H. simpl in H0.
inversion H. inversion H0. auto. subst.
eelim app_cons_not_nil. eauto.
generalize (decompose_app _ _ _ _ H1). intro. destruct H9; subst; clear H1.
inversion H0; subst.
eelim app_cons_not_nil. eauto.
generalize (decompose_app _ _ _ _ H1). intro. destruct H8; subst; clear H1.
replace val with val0.
generalize (Edge.eq_trans (Edge.eq_sym H4) H7). intro.
rewrite H1 in *.
rewrite (In_graph_labeled_edge_eq (v4,v2') g w w0); auto.
eapply IHl. eauto. eauto.
Qed.

Lemma cut_path_aux : forall p' v0 v1 g v,
path p' v0 v1 g v ->
forall p vopt,
path p v0 v1 g vopt ->
forall v2 v3 w val,
vopt <= v ->
path (p' ++ (v1,v2) :: nil) v0 v3 g val ->
edge_label (v1,v2) g = Some w ->
vopt + eval w <= val.

Proof.
intros. inversion H2; subst.
eelim app_cons_not_nil. eauto.
generalize (decompose_app _ _ _ _ H4). clear H4. intro. destruct H4; subst.
generalize (path_value_eq _ _ _ _ _ _ _ _ H H5). intro. subst.
rewrite <-H7 in *. rewrite (labeled_edge_edge_label _ _ _ _ H6 H3).
inversion H3; subst; auto. intuition.
Qed.

Lemma cut_path : forall p' v0 v1 g v,
path p' v0 v1 g v ->
forall p vopt,
path p v0 v1 g vopt ->
forall p1 v2 v3 w val,
vopt <= v ->
path (p' ++ (v1,v2) :: p1) v0 v3 g val ->
edge_label (v1,v2) g = Some w ->
vopt + eval w <= val.

Proof.
intros. generalize (path_shorten_1 _ _ _ _ _ _ _ _ H2). intro.
destruct H4. destruct H4.
apply le_trans with (m := x).
eapply cut_path_aux;[eapply H|eapply H0|eauto|eauto|eauto].
auto.
Qed.

End Path.