Library Dijkstra

Require Import DigraphInterface.
Require Import OrderedType.
Require Import ZArith.
Require Import OrderedTypeEx.
Require Import Recdef.
Require Import Paths.
Require Import Common.
Require Import FSets.
Require Import Labels.

Close Scope nat_scope.

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

Import G Lab Edge VMapFacts.

Module Import eqlistAF := eqlistAFacts Edge.
Module Import EA := Eadd Vertex Lab G.

Module list_as_OT (O : OrderedType) <: OrderedType.

Import O.

Module Import OP := OrderedTypeFacts O.

Definition t := list O.t.

Definition eq := eqlistA O.eq.

Inductive lt_ : t -> t -> Prop :=
| ltnil : forall a l, lt_ nil (a :: l)
| ltcons : forall a l a' l', O.lt a a' -> lt_ (a :: l) (a' :: l')
| lt_tail : forall a a' l l', O.eq a a' -> lt_ l l' -> lt_ (a :: l) (a' :: l').

Definition lt := lt_.

Lemma eq_dec : forall l l', {eq l l'}+{~eq l l'}.

Proof.
unfold eq; induction l; intros.
destruct l'. left. intuition.
right. intro. inversion H.
destruct l'. right. intro. inversion H.
destruct (IHl l').
destruct (O.eq_dec a t0). left. constructor; auto.
right. intro. elim n. inversion H; auto.
right. intro. elim n. inversion H; auto.
Qed.

Lemma eq_refl : forall x, eq x x.

Proof.
unfold eq; induction x; intros.
auto.
constructor; auto.
Qed.

Lemma eq_sym : forall x y, eq x y -> eq y x.

Proof.
unfold eq; induction x; intros.
inversion H; auto.
destruct y. inversion H.
inversion H. subst.
constructor. auto. auto.
Qed.

Lemma eq_trans : forall x y z, eq x y -> eq y z -> eq x z.

Proof.
induction x; unfold eq; intros.
inversion H. subst. inversion H0. subst. auto.
destruct y. inversion H.
destruct z. inversion H0.
constructor. inversion H; inversion H0; subst.
eapply O.eq_trans; eauto.
eapply IHx; inversion H; inversion H0; subst; eauto.
Qed.

Lemma lt_trans : forall x y z, lt x y -> lt y z -> lt x z.

Proof.
induction x; unfold lt; intros.
inversion H; subst.
inversion H0; subst.
constructor.
constructor.
inversion H; subst.
inversion H0; subst.
constructor. eapply O.lt_trans; eauto.
inversion H0; subst.
constructor.
rewrite <-H3. auto.
constructor.
rewrite <-H3. auto.
inversion H0; subst.
constructor.
rewrite H3. auto.
apply lt_tail. rewrite H3. auto. eapply IHx; eauto.
Qed.

Lemma lt_not_eq : forall x y, lt x y -> ~eq x y.

Proof.
induction x; unfold lt, eq; intros; intro.
inversion H; subst.
inversion H0.
destruct y. inversion H0.
inversion H0; subst.
inversion H; subst.
elim (O.lt_not_eq H2 H4).
eapply IHx; eauto.
Qed.

Lemma compare : forall x y, Compare lt eq x y.

Proof.
induction x; intros.
destruct y.
apply EQ. apply eq_refl.
apply LT. constructor.
destruct y. apply GT. constructor.
destruct (O.compare a t0).
apply LT. constructor. auto.
destruct (IHx y).
apply LT. apply lt_tail; auto.
apply EQ. constructor; auto.
apply GT. apply lt_tail; auto.
apply GT. constructor. auto.
Qed.

End list_as_OT.

Module EdgeList := list_as_OT Edge.
Module Couple_ := PairOrderedType Nat_as_OT Vertex.
Module Couple := PairOrderedType Couple_ EdgeList.

Module CoupleSet := FSetAVL.Make Couple.

Module PS := Properties CoupleSet.
Module PPS := Facts CoupleSet.


Inductive status : Type :=
| Open : status
| Optimal : status.

Inductive vertex_status : Type :=
| Reached : status -> nat -> list t -> vertex_status
| Unreached : vertex_status.

Module Import P := Path Vertex Lab G.

Open Scope nat_scope.

Definition dynamic_prog map graph := forall v v' d (l : list Edge.t) w,
VertexMap.find v map = Some (Reached Optimal d l) ->
In_graph_labeled_edge (v,v') graph w ->
exists s, exists d', exists l',
VertexMap.find v' map = Some (Reached s d' l') /\ d' <= d + (eval w).

Definition shortest_path map graph root := forall p v val d (l : list Edge.t),
path p root v graph val ->
VertexMap.find v map = Some (Reached Optimal d l) ->
d <= val.

Definition correct_path map graph root := forall l (s : status) d v,
VertexMap.find v map = Some (Reached s d l) ->
path (rev l) root v graph d.

Lemma consistant_status : forall map v,
(exists d, exists l, VertexMap.find v map = Some(Reached Optimal d l)) \/
(exists d, exists l, VertexMap.find v map = Some(Reached Open d l)) \/
VertexMap.find v map = Some Unreached \/
VertexMap.find v map = None.

Proof.
intros.
case_eq (VertexMap.find v map); intros.
destruct v0. destruct s.
right. left. exists n. exists l. auto.
left. exists n. exists l. auto.
right. auto.
right. auto.
Qed.

Record pathmap := Make_pathmap {
graph : G.t;
root : Vertex.t;
map : VertexMap.t vertex_status;
is_path : correct_path map graph root;
shortest : shortest_path map graph root;
dynamic : dynamic_prog map graph;
root_find : VertexMap.find root map = Some (Reached Optimal 0 nil);
in_map_in_graph : forall v, In_graph_vertex v graph -> VertexMap.In v map;
set : CoupleSet.t;
set_open : forall d v p, CoupleSet.In (d,v,p) set <-> exists p',
                                    eqlistA Edge.eq p p' /\
                                    VertexMap.MapsTo v (Reached Open d p') map
}.


Definition null_init (g : G.t) :=
VertexMap.map (fun _ => Unreached) (V g).

Lemma null_init_1 : forall g v,
VertexMap.find v (null_init g) = Some Unreached <-> In_graph_vertex v g.

Proof.
unfold null_init.
split; intros.
rewrite In_graph_vertex_spec.
assert (VertexMap.In v (VertexMap.map (fun _ => Unreached) (V g))).
rewrite MapFacts.in_find_iff. congruence. apply (VertexMap.map_2 H0).
apply VertexMap.find_1. rewrite In_graph_vertex_spec in H.
rewrite Mapsto_In in H. destruct H. apply (VertexMap.map_1 _ H).
Qed.

Lemma null_init_2 : forall g v,
VertexMap.find v (null_init g) = None <-> ~In_graph_vertex v g.

Proof.
split; intros. intro.
rewrite <-null_init_1 in H0. congruence.
case_eq (VertexMap.find v (null_init g)); intros.
unfold null_init in H0. generalize (VertexMap.find_2 H0). clear H0. intro.
elim H. rewrite In_graph_vertex_spec.
generalize (MapsTo_In _ _ _ _ H0). intro. apply (VertexMap.map_2 H1).
reflexivity.
Qed.

Lemma null_init_3 : forall g v,
(In_graph_vertex v g /\ VertexMap.find v (null_init g) = Some Unreached) \/
(~In_graph_vertex v g /\ VertexMap.find v (null_init g) = None).

Proof.
intros. destruct (MapFacts.In_dec (V g) v).
left. rewrite <-In_graph_vertex_spec in i. split. auto. rewrite null_init_1. auto.
right. rewrite <-In_graph_vertex_spec in n. split. auto. rewrite null_init_2. auto.
Qed.

Definition first_iter v g init :=
fold_succ_ne
               (fun _ _ x o (ms : (VertexMap.t vertex_status)*CoupleSet.t) =>
                     let (m,s) := ms in
                     (VertexMap.add x (Reached Open (eval o) ((v,x) :: nil)) m,
                      CoupleSet.add (eval o, x, (v,x) :: nil) s)
               )
               v g init.

Definition init_dijkstra (v : Vertex.t) (g : G.t) : VertexMap.t vertex_status * CoupleSet.t :=
let init := (null_init g, CoupleSet.empty) in
let (itermap, iterset) := first_iter v g init
in (VertexMap.add v (Reached Optimal 0 nil) itermap, iterset).

Lemma first_iter_charac : forall r v g s d l,
VertexMap.find v (fst (first_iter r g (null_init g, CoupleSet.empty))) = Some (Reached s d l) ->
(exists w, VertexMap.MapsTo v w (VertexMap.remove r (successors r g)) /\ eval w = d) /\
eqlistA Edge.eq l ((r,v) :: nil).

Proof.
unfold first_iter; intros r v g s d l.
rewrite fold_succ_ne_spec. rewrite VertexMap.fold_1.
apply fold_invariant. intro.
destruct (null_init_3 g v); destruct H0; fold Edge.t in H; simpl in *; congruence.
intros. destruct t0 as [m s'].
destruct x as [x y]. destruct (Vertex.eq_dec v x); simpl in *.
rewrite MapFacts.add_eq_o in H1;[|auto].
split. exists y. split. apply VertexMap.elements_2. rewrite InA_alt. exists (x,y).
split. eq_key_solve. auto. inversion H1; subst; auto.
inversion H1; auto. constructor. split; auto. constructor.
rewrite MapFacts.add_neq_o in H1;[|auto]. auto.
Qed.

Lemma init_finite : forall r g l s d v,
VertexMap.find v (fst (init_dijkstra r g)) = Some (Reached s d l) ->
Vertex.eq v r \/ VertexMap.In v (successors r g).

Proof.
unfold init_dijkstra; intros.
destruct (Vertex.eq_dec v r).
left. auto.
case_eq (first_iter r g (null_init g, CoupleSet.empty)); intros; rewrite H0 in *; simpl in *;
rewrite MapFacts.add_neq_o in H;[|auto].
right. replace t0 with (fst (first_iter r g (null_init g, CoupleSet.empty))) in H.
generalize (first_iter_charac _ _ _ _ _ _ H). intro. destruct H1.
do 2 destruct H1. eapply MapsTo_In; eapply VertexMap.remove_3; eauto.
rewrite H0. auto.
Qed.

Lemma root_find_init : forall r g,
VertexMap.find r (fst (init_dijkstra r g)) = Some (Reached Optimal 0 nil).

Proof.
unfold init_dijkstra; intros.
destruct (first_iter r g (null_init g, CoupleSet.empty)); simpl in *;
rewrite add_eq_o. auto. auto.
Qed.

Lemma path_init : forall r g l s d v,
VertexMap.find v (fst (init_dijkstra r g)) = Some (Reached s d l) ->
path (rev l) r v g d.

Proof.
unfold init_dijkstra. intros.
destruct (Vertex.eq_dec v r).
destruct (first_iter r g (null_init g, CoupleSet.empty)); simpl in *;
rewrite MapFacts.add_eq_o in H;[|auto]. inversion H; subst.
constructor. auto.
case_eq (first_iter r g (null_init g, CoupleSet.empty)); intros v1 v2 HH; rewrite HH in *; simpl in *;
rewrite MapFacts.add_neq_o in H;[|auto].
replace v1 with (fst (first_iter r g (null_init g, CoupleSet.empty))) in H.
destruct (first_iter_charac _ _ _ _ _ _ H).
apply path_eqlistA with (p := (r,v) :: nil). do 2 destruct H0.
replace d with (0 + eval x). change ((r,v) :: nil) with (nil ++ (r,v) :: nil).
apply path_post with (v2 := r). constructor. auto.
rewrite <-mapsto_edge_equiv_succ. eapply VertexMap.remove_3; eauto.
split; auto.
change ((r,v) :: nil) with (rev ((r,v) :: nil)). apply eqlistA_rev. auto.
rewrite HH. auto.
Qed.

Lemma first_iter_not_opt : forall r v g d l,
VertexMap.find v (fst (first_iter r g (null_init g, CoupleSet.empty))) <>
                            Some (Reached Optimal d l).

Proof.
unfold first_iter; intros.
rewrite fold_succ_ne_spec. rewrite VertexMap.fold_1. apply fold_invariant.
destruct (null_init_3 g v); destruct H; unfold Edge.t in *; simpl in *; congruence.
intros. destruct x as (x,y). simpl in *.
destruct (Vertex.eq_dec v x).
destruct t0; simpl in *;
rewrite MapFacts.add_eq_o;[|auto]. congruence.
destruct t0; simpl in *; rewrite MapFacts.add_neq_o;[|auto]. auto.
Qed.

Lemma shortest_init : forall r g,
shortest_path (fst (init_dijkstra r g)) g r.

Proof.
unfold shortest_path. intros.
unfold init_dijkstra in H0. destruct (Vertex.eq_dec v r).
destruct (first_iter r g (null_init g, CoupleSet.empty)); simpl in *;
rewrite add_eq_o in H0. inversion H0. intuition. auto.
case_eq (first_iter r g (null_init g, CoupleSet.empty)); intros x y HH; rewrite HH in *;
simpl in *; rewrite add_neq_o in H0.
replace x with (fst (first_iter r g (null_init g, CoupleSet.empty))) in H0.
elim (first_iter_not_opt _ _ _ _ _ H0).
rewrite HH. auto.
auto.
Qed.

Ltac unfold_data := unfold VertexMap.key, Edge.t in *.

Lemma first_iter_charac_2 : forall r g x v,
VertexMap.MapsTo x v (VertexMap.remove r (successors r g)) ->
exists e, Edge.eq e (r,x) /\
VertexMap.find x (fst (first_iter r g (null_init g, CoupleSet.empty))) =
                             Some (Reached Open (eval v) (e :: nil)).

Proof.
unfold first_iter; intros.
rewrite fold_succ_ne_spec. rewrite VertexMap.fold_1.
generalize VertexMap.elements_1. intro.
generalize (H0 _ _ _ _ H). clear H0. intro.
generalize VertexMap.elements_3w. intro.
generalize (H1 _ (VertexMap.remove r (successors r g))). clear H1. intro HND.
induction (VertexMap.elements (VertexMap.remove r (successors r g))); intros.
inversion H0.
unfold_data.
set (f := (fun (a0 : VertexMap.t vertex_status * CoupleSet.t)
             (p : VertexMap.E.t * option EdgeLabel) =>
           let (m, s) := a0 in
           (VertexMap.add (fst p)
              (Reached Open (eval (snd p)) ((r, fst p) :: nil)) m,
           CoupleSet.add (eval (snd p), fst p, (r,fst p) :: nil) s))) in *.
replace (VertexMap.find x (fst (fold_left f (a :: l) (null_init g, CoupleSet.empty)))) with
             (VertexMap.find x (fst (f (fold_left f l (null_init g, CoupleSet.empty)) a))).
set (m := fold_left f l (null_init g, CoupleSet.empty)) in *.
inversion H0; subst.
unfold f. destruct a. simpl in *.
destruct m; simpl in *;
rewrite MapFacts.add_eq_o;[|auto]. exists (r,t0). split; auto.
split; eq_key_solve. intuition. inversion H2. simpl in H3. subst. auto.
eq_key_solve. intuition.
unfold f. destruct m; simpl in *;
rewrite MapFacts.add_neq_o. apply IHl. auto.
inversion HND; auto.
intro. inversion HND. subst. elim H5.
rewrite InA_alt in H2. destruct H2. destruct H2. rewrite InA_alt. exists x0.
split. inversion H2; subst. simpl in *. rewrite H4 in H1. eq_key_solve. auto.
rewrite fold_left_assoc_map_find_nodup. auto.
constructor. unfold RelationPairs.RelCompFun. apply Equal_refl.
apply PS.equal_refl.
intros. constructor. unfold RelationPairs.RelCompFun.
inversion H1; inversion H2; simpl in *.
apply Equal_trans with (m' := fst y). apply H3. apply H5.
unfold RelationPairs.RelCompFun.
inversion H1; inversion H2; simpl in *.
apply PS.equal_trans with (s2 := snd y).
apply H4. apply H6.
eauto.
intros.
constructor. unfold RelationPairs.RelCompFun.
unfold f. destruct s. simpl. apply add_add_Eq. eq_key_solve.
intros. unfold RelationPairs.RelCompFun.
unfold f. destruct s. simpl.
apply PS.add_add.
intros. constructor. unfold RelationPairs.RelCompFun.
unfold f. destruct e1. destruct e2. simpl.
inversion H1.
apply add_m. auto. auto.
auto.
unfold RelationPairs.RelCompFun. unfold f. destruct e1. destruct e2. simpl.
apply PPS.add_m. simpl. intuition.
inversion H1. auto.
Qed.

Lemma dynamic_init : forall r g,
dynamic_prog (fst (init_dijkstra r g)) g.

Proof.
unfold dynamic_prog. intros.
unfold init_dijkstra in H.
destruct (Vertex.eq_dec v r).
case_eq (first_iter r g (null_init g, CoupleSet.empty));
intros x y HH; rewrite HH in H; simpl in H.
rewrite MapFacts.add_eq_o in H;[|auto]. inversion H; subst.
unfold init_dijkstra. destruct (Vertex.eq_dec v' r).
rewrite HH. simpl.
rewrite MapFacts.add_eq_o;[|auto].
exists Optimal. exists 0. exists nil. split; intuition.
rewrite HH. simpl. rewrite MapFacts.add_neq_o;[|auto].
rewrite e in H0. rewrite <-mapsto_edge_equiv_succ in H0.
assert (VertexMap.MapsTo v' w (VertexMap.remove r (successors r g))) as HH0.
apply VertexMap.remove_2; auto.
generalize (first_iter_charac_2 _ _ _ _ HH0). intro.
destruct H1. destruct H1. rewrite HH in H2. simpl in *. rewrite H2.
exists Open. exists (eval w). exists (x0 :: nil). split; intuition.
case_eq (first_iter r g (null_init g, CoupleSet.empty));
intros x y HH; rewrite HH in H; simpl in H.
rewrite MapFacts.add_neq_o in H;[|auto].
replace x with (fst (first_iter r g (null_init g, CoupleSet.empty))) in H. simpl in H.
elim (first_iter_not_opt _ _ _ _ _ H).
rewrite HH. auto.
Qed.

Lemma in_map_in_graph_init : forall r g,
forall v, In_graph_vertex v g -> VertexMap.In v (fst (init_dijkstra r g)).

Proof.
intros. rewrite MapFacts.in_find_iff.
unfold init_dijkstra, first_iter.
destruct (Vertex.eq_dec v r).
case_eq (fold_succ_ne
            (fun (_ : G.t) (_ x : Vertex.t) (o : option EdgeLabel)
               (ms : VertexMap.t vertex_status * CoupleSet.t) =>
             let (m, s) := ms in
             (VertexMap.add x (Reached Open (eval o) ((r, x) :: nil)) m,
             CoupleSet.add (eval o, x, (r,x) :: nil) s)) r g (null_init g, CoupleSet.empty));
intros x y HH; simpl in *.
rewrite add_eq_o.
congruence. auto.
case_eq (fold_succ_ne
            (fun (_ : G.t) (_ x : Vertex.t) (o : option EdgeLabel)
               (ms : VertexMap.t vertex_status * CoupleSet.t) =>
             let (m, s) := ms in
             (VertexMap.add x (Reached Open (eval o) ((r, x) :: nil)) m,
             CoupleSet.add (eval o, x, (r,x) :: nil) s)) r g (null_init g, CoupleSet.empty));
intros x y HH; simpl in *.
rewrite add_neq_o.
rewrite fold_succ_ne_spec in HH. rewrite VertexMap.fold_1 in HH.
replace x with (fst (fold_left
       (fun (a : VertexMap.t vertex_status * CoupleSet.t)
          (p : VertexMap.key * option EdgeLabel) =>
        let (m, s) := a in
        (VertexMap.add (fst p)
           (Reached Open (eval (snd p)) ((r, fst p) :: nil)) m,
        CoupleSet.add (eval (snd p), fst p, (r,fst p) :: nil) s))
       (VertexMap.elements (elt:=option EdgeLabel) (VertexMap.remove r (successors r g)))
       (null_init g, CoupleSet.empty))).
apply fold_invariant. rewrite <-null_init_1 in H. unfold_data.
simpl. rewrite H. congruence.
intros.
destruct x0 as (x0,x1). simpl.
assert (VertexMap.MapsTo x0 x1 (VertexMap.remove r (successors r g))) as Hadj.
apply VertexMap.elements_2. rewrite InA_alt.
exists (x0,x1). split; auto. intuition.
destruct (Vertex.eq_dec v x0).
destruct t0. simpl. rewrite add_eq_o. congruence. auto.
destruct t0. simpl. rewrite add_neq_o. auto. auto.
unfold VertexMap.key in *. rewrite HH. auto.
auto.
Qed.

Lemma set_open_init : forall r g d v p,
CoupleSet.In (d,v,p) (snd (init_dijkstra r g)) <-> exists p',
eqlistA Edge.eq p p' /\
VertexMap.MapsTo v (Reached Open d p') (fst (init_dijkstra r g)).

Proof.
unfold init_dijkstra; intros.
case_eq (first_iter r g (null_init g, CoupleSet.empty)); intros xxx yyy HHH.
simpl.
replace yyy with (snd (first_iter r g (null_init g, CoupleSet.empty))).
replace xxx with (fst (first_iter r g (null_init g, CoupleSet.empty))).
unfold first_iter.
rewrite fold_succ_ne_spec. rewrite VertexMap.fold_1.
assert (forall x, ~InA (@VertexMap.eq_key_elt (option EdgeLabel)) (r,x) (VertexMap.elements (VertexMap.remove r (successors r g)))).
intro. intro. generalize (VertexMap.elements_2 H). intro.
rewrite remove_mapsto_iff in H0. destruct H0. elim H0. auto.
generalize VertexMap.elements_3w. intro.
generalize (H0 _ (VertexMap.remove r (successors r g))). clear H0. intro HND.
induction (VertexMap.elements (VertexMap.remove r (successors r g))).
simpl.

split; intros.
rewrite PS.Dec.F.empty_iff in H0. inversion H0.
destruct H0. destruct H0. rewrite add_mapsto_iff in H1.
destruct H1. destruct H1. inversion H2.
destruct H1. generalize (null_init_3 g v). intro.
destruct H3. destruct H3.
generalize (VertexMap.find_1 H2). intro. congruence.
destruct H3.
generalize (VertexMap.find_1 H2). intro. congruence.

set (f := (fun (a0 : VertexMap.t vertex_status * CoupleSet.t)
                  (p0 : VertexMap.key * option EdgeLabel) =>
                let (m, s) := a0 in
                (VertexMap.add (fst p0)
                   (Reached Open (eval (snd p0)) ((r, fst p0) :: nil)) m,
                CoupleSet.add (eval (snd p0), fst p0, (r, fst p0) :: nil) s))) in *.
unfold VertexMap.key in *. fold f. fold f in IHl.
assert (CoupleSet.In (d, v, p)
  (snd (f (fold_left f l (null_init g, CoupleSet.empty))a )) <->
(exists p' : list (Vertex.t * Vertex.t),
   eqlistA eq p p' /\
   VertexMap.MapsTo v (Reached Open d p')
     (VertexMap.add r (Reached Optimal 0 nil)
        (fst (f (fold_left f l (null_init g, CoupleSet.empty)) a))))).
cut (forall x p, VertexMap.MapsTo x (Reached Open d p) (fst (fold_left f l (null_init g, CoupleSet.empty)))
                    -> exists y, InA (@VertexMap.eq_key (option EdgeLabel)) (x,y) l). intro Hcut.
destruct (fold_left f l (null_init g, CoupleSet.empty)).
simpl. intros.
split.
rewrite PS.Dec.F.add_iff. simpl. intro.
destruct H0. destruct H0. destruct H0.
exists ((r,fst a) :: nil). split. intuition.
do 2 rewrite add_mapsto_iff.
destruct (Vertex.eq_dec r v).
elim (H (snd a)).
left. rewrite e. destruct H0. rewrite <-H2. destruct a. simpl. intuition.
right. split. auto.
simpl. left. split. auto. subst. auto.
assert ((CoupleSet.In (d, v, p) (snd (t0, t1)) <->
       (exists p' : list (Vertex.t * Vertex.t),
          eqlistA eq p p' /\
          VertexMap.MapsTo v (Reached Open d p')
            (VertexMap.add r (Reached Optimal 0 nil) (fst (t0, t1)))))).
apply IHl.
intros. intro. elim (H x). right. auto.
inversion HND. auto.
rewrite H1 in H0. destruct H0. destruct H0.
destruct (Vertex.eq_dec (fst a) v).
exists p. split. intuition.
rewrite add_mapsto_iff. right.
rewrite add_mapsto_iff in H2. destruct H2. destruct H2. inversion H3.
destruct H2. split. auto.
rewrite add_mapsto_iff. left. split. auto.
simpl in H3. generalize (Hcut _ _ H3). intro.
destruct H4. rewrite <-e in H4. inversion HND. subst.
elim H7. rewrite InA_alt in H4. destruct H4. rewrite InA_alt.
exists x1. split. intuition. intuition.
rewrite add_mapsto_iff in H2. destruct H2. destruct H2. inversion H3.
destruct H2. simpl in H3.
exists x. split. auto.
rewrite add_mapsto_iff. rewrite add_mapsto_iff. right. split. auto.
right. split; auto.

intros. destruct H0. destruct H0.
rewrite add_mapsto_iff in H1. rewrite add_mapsto_iff in H1.
destruct H1. destruct H1. inversion H2.
destruct H1. destruct H2. destruct H2.
rewrite PS.Dec.F.add_iff. simpl.
left. split. split; auto. inversion H3. auto.
inversion H3. subst. intuition.
destruct H2. rewrite PS.Dec.F.add_iff. simpl.
right. rewrite IHl. exists x.
split. auto.
rewrite add_mapsto_iff. right. split. auto. simpl. auto.
intros. intro. elim (H x0). right. auto.
inversion HND. auto.

apply fold_invariant.
simpl. intros.
destruct (null_init_3 g x); destruct H1; generalize (VertexMap.find_1 H0); congruence.
intros.
unfold f in H2. destruct t0. simpl in H2.
rewrite add_mapsto_iff in H2. destruct H2.
destruct H2. exists (snd x).
rewrite InA_alt. exists x. split. eq_key_solve. auto.
destruct H2.
apply (H1 _ p0). simpl. auto.
assert (CoupleSet.eq (snd (fold_left f (a :: l) (null_init g, CoupleSet.empty)))
                                  (snd (f (fold_left f l (null_init g, CoupleSet.empty)) a))).
apply fold_left_assoc.
intuition.
intros. eapply CoupleSet.eq_trans; eauto.
unfold f. destruct s. simpl.
apply PS.add_add.
intros. unfold f. destruct e2. destruct e1. simpl.
apply PPS.add_m.
simpl in *. intuition.
auto.
rewrite (PS.Dec.F.In_m (Couple.eq_refl (d,v,p)) H1).
assert (VertexMap.Equal (fst (f (fold_left f l (null_init g, CoupleSet.empty)) a))
                                        (fst (fold_left f (a :: l) (null_init g, CoupleSet.empty)))).
eapply fold_left_assoc_map_find_nodup.
intuition.
intros. eapply Equal_trans; eauto.
eauto.
unfold f. destruct s. simpl.
apply add_add_Eq.
intros. unfold f. destruct e2. destruct e1. simpl.
apply add_m. auto. auto. auto.

split; intros.
rewrite H0 in H3. destruct H3. exists x. destruct H3. split. auto.
rewrite add_mapsto_iff. rewrite add_mapsto_iff in H4.
destruct H4. left. auto.
destruct H4. right. split. auto.
rewrite <-H2. auto.
rewrite H0. destruct H3. exists x. destruct H3. split. auto.
rewrite add_mapsto_iff. rewrite add_mapsto_iff in H4.
destruct H4. left. auto.
destruct H4. right. split. auto.
rewrite H2. auto.

rewrite HHH. auto.
rewrite HHH. auto.
Qed.

Definition init (g : G.t) (r : Vertex.t) :=
Make_pathmap g
                         r
                         (fst (init_dijkstra r g))
                         (path_init r g)
                         (shortest_init r g)
                         (dynamic_init r g)
                         (root_find_init r g)
                         (in_map_in_graph_init r g)
                         (snd (init_dijkstra r g))
                         (set_open_init r g).

Definition find_min (s : CoupleSet.t) := CoupleSet.min_elt s.

Definition update (v : Vertex.t) (dist : EdgeLabel) (pre : list Edge.t) (m : VertexMap.t vertex_status)
                            (w : option Nat_as_OT.t) (x : Vertex.t) (s : CoupleSet.t) :=
match VertexMap.find x m with
  | None => (m,s)
  | Some (Reached Optimal _ _ ) => (m,s)
  | Some Unreached => let new_dist := dist + eval w in
                                         (VertexMap.add x (Reached Open new_dist ((v,x) :: pre)) m,
                                         CoupleSet.add (new_dist, x, (v,x) :: pre) s)
  | Some (Reached Open n p) => let new_w := dist+eval w in
                                                     if le_lt_dec n new_w
                                                     then (m,s)
                                                     else (VertexMap.add x (Reached Open new_w ((v,x) :: pre)) m,
                                                              CoupleSet.add (new_w,x,(v,x) :: pre) (CoupleSet.remove (n,x,p) s))
end.

Definition iteration pm :=
let d := map pm in
let g := graph pm in
let s := set pm in
match find_min s with
| None => (None, d, s)
| Some (dist, v, p) => let (newd, news) :=
                                        fold_succ_ne (fun _ _ x w (ms : VertexMap.t vertex_status * CoupleSet.t) =>
                                        let (m,s) := ms in update v dist p m w x s) v g (d,s)
                                        in (Some v, VertexMap.add v (Reached Optimal dist p) newd,
                                                            CoupleSet.remove (dist,v,p) news)
end.

Lemma iteration_finite : forall pm s d l v d' l' min,
VertexMap.find v (snd (fst (iteration pm))) = Some (Reached s d l) ->
find_min (set pm) = Some (d', min, l') ->
VertexMap.find v (map pm) = Some (Reached s d l) \/
VertexMap.In v (successors min (graph pm)) \/ Vertex.eq v min.

Proof.
unfold iteration. intros. rewrite H0 in H. simpl in H.
destruct (Vertex.eq_dec v min). right. auto.
case_eq ( fold_succ_ne
                   (fun (_ : G.t) (_ x : Vertex.t) (w : option EdgeLabel)
                      (ms : VertexMap.t vertex_status * CoupleSet.t) =>
                    let (m, s) := ms in update min d' l' m w x s) min
                   (graph pm) (map pm, set pm)); intros x y HH; rewrite HH in *; simpl in *.
rewrite MapFacts.add_neq_o in H.
generalize H. replace x with (fst ( fold_succ_ne
       (fun (_ : G.t) (_ x : Vertex.t) (w : option EdgeLabel)
          (ms : VertexMap.t vertex_status * CoupleSet.t) =>
        let (m, s) := ms in update min d' l' m w x s) min (graph pm)
       (map pm, set pm) )). rewrite fold_succ_ne_spec. rewrite VertexMap.fold_1.
apply fold_invariant. auto.
intros. destruct x0 as (x0,x1). simpl in *.
destruct t0 as [t0 t1]. simpl in *.
unfold update in H3.
case_eq (VertexMap.find x0 t0); intros; rewrite H4 in H3.
destruct v0. destruct s0.
destruct (le_lt_dec n0 (d' + eval x1)).
apply H2. auto.
destruct (Vertex.eq_dec v x0).
right. left. apply MapsTo_In with (e := x1).
eapply VertexMap.remove_3.
apply VertexMap.elements_2. rewrite InA_alt.
exists (x0,x1). split. eq_key_solve. eauto.
simpl in H3. rewrite MapFacts.add_neq_o in H3;[|auto].
apply H2. auto.
apply H2. auto.
destruct (Vertex.eq_dec x0 v).
right. left. apply MapsTo_In with (e := x1).
eapply VertexMap.remove_3.
apply VertexMap.elements_2. rewrite InA_alt.
exists (x0,x1). split. eq_key_solve. eauto.
simpl in H3. rewrite MapFacts.add_neq_o in H3;[|auto].
apply H2. auto.
apply H2. auto.
rewrite HH. auto.
auto.
Qed.

Lemma find_min_1 : forall pm,
forall v dist p, find_min (set pm) = Some (dist, v, p) ->
exists p', eqlistA Edge.eq p p' /\
VertexMap.find v (map pm) = Some (Reached Open dist p') .

Proof.
intros.
assert (exists p', eqlistA Edge.eq p p' /\ VertexMap.MapsTo v (Reached Open dist p') (map pm)).
rewrite <-set_open. apply CoupleSet.min_elt_1. auto.
destruct H0. destruct H0.
exists x. split. auto. apply VertexMap.find_1. auto.
Qed.

Lemma find_min_2 : forall pm,
forall v dist p, find_min (set pm) = Some (dist,v,p) ->
forall v' dist' pred', VertexMap.find v' (map pm) = Some (Reached Open dist' pred') ->
dist <= dist'.

Proof.
unfold find_min; intros.
assert (CoupleSet.In (dist',v',pred') (set pm)).
rewrite set_open. exists pred'. split. intuition.
apply VertexMap.find_2. auto.
generalize CoupleSet.min_elt_2. intro.
generalize (H2 _ _ (dist',v',pred') H H1). intro.
simpl in H3. intuition.
Qed.

Lemma path_iteration : forall pm,
forall l st d v,
VertexMap.find v (snd (fst (iteration pm))) = Some (Reached st d l) ->
path (rev l) (root pm) v (graph pm) d.

Proof.
intro pm. generalize (is_path pm).
unfold iteration; intros H l st d v H0.
case_eq (find_min (set pm)); intros.
rewrite H1 in H0.
destruct e. destruct p.
case_eq (fold_succ_ne
                    (fun (_ : G.t) (_ x : Vertex.t) (w : option EdgeLabel)
                       (ms : VertexMap.t vertex_status * CoupleSet.t) =>
                     let (m, s) := ms in update t0 n l0 m w x s) t0
                    (graph pm) (map pm, set pm));
intros xxx yyy HH; rewrite HH in *; simpl in *.
generalize (find_min_1 _ _ _ _ H1). intro.
destruct H2 as [p' H2]. destruct H2 as [H2 HH2]. subst.
destruct (Vertex.eq_dec v t0).
rewrite add_eq_o in H0.
inversion H0. subst.
apply path_eqlistA with (p := rev p').
eapply H. rewrite (find_o _ e). eauto.
apply eqlistA_rev. auto.
auto.
rewrite add_neq_o in H0.
replace xxx with (fst (fold_succ_ne
       (fun (_ : G.t) (_ x : Vertex.t) (w : option EdgeLabel)
          (ms : VertexMap.t vertex_status * CoupleSet.t) =>
        let (m, s) := ms in update t0 n l0 m w x s) t0 (graph pm)
       (map pm, set pm))) in H0.
rewrite fold_succ_ne_spec in H0.
generalize H0. clear H0. rewrite VertexMap.fold_1. apply fold_invariant.
intros.
eapply H. eauto.
intros.
destruct x as (x,y). simpl in *.
assert (VertexMap.MapsTo x y (VertexMap.remove t0 (successors t0 (graph pm)))) as Hadj.
apply VertexMap.elements_2. rewrite InA_alt.
exists (x,y). split; auto. intuition.
destruct t1. simpl in *.
unfold update in H4.
case_eq (VertexMap.find x t1); intros. simpl in H4. rewrite H5 in H4.
destruct v0. destruct s.
destruct (le_lt_dec n1 (n + eval y)).
eapply H3. eauto.
destruct (Vertex.eq_dec v x).
simpl in H4. rewrite add_eq_o in H4. inversion H4; subst.
simpl. eapply path_snd_ext.
apply path_post with (v2 := t0).
generalize (find_min_1 _ _ _ _ H1). intro.
destruct H6 as [p'' H6]. destruct H6 as [H6 HH6].
apply path_eqlistA with (p := rev p'').
eapply H. eauto.
apply eqlistA_rev. auto.
rewrite <-mapsto_edge_equiv_succ. eapply VertexMap.remove_3; eauto. apply Edge.eq_refl. auto. auto.
simpl in H4. rewrite add_neq_o in H4. eapply H3. eauto. auto.
eapply H3. auto.
destruct (Vertex.eq_dec v x).
simpl in H4. rewrite add_eq_o in H4. inversion H4; subst.
simpl. eapply path_snd_ext. apply path_post with (v2:=t0).
generalize (find_min_1 _ _ _ _ H1). intro.
destruct H6 as [p'' H6]. destruct H6 as [H6 HH6].
apply path_eqlistA with (p := rev p'').
eapply H. eauto.
apply eqlistA_rev. auto.
rewrite <-mapsto_edge_equiv_succ. eapply VertexMap.remove_3; eauto. apply Edge.eq_refl. auto. auto.
simpl in H4. rewrite add_neq_o in H4. eapply H3. eauto. auto.
eapply H3; eauto.
rewrite H5 in H4.
auto.
rewrite HH. auto.
auto.
eapply H; eauto.
rewrite H1 in H0. simpl in H0. eauto.
Qed.

Lemma update_closed_inv : forall pm v d l0 e t0 l,
 VertexMap.find v (fst (fold_succ_ne
       (fun (_ : G.t) (_ x : Vertex.t) (w : option EdgeLabel)
          (ms : VertexMap.t vertex_status * CoupleSet.t) =>
        let (m, s) := ms in update t0 e l0 m w x s) t0 (graph pm)
       (map pm, set pm))) = Some (Reached Optimal d l) ->
VertexMap.find v (map pm) = Some (Reached Optimal d l).

Proof.
intros. rewrite fold_succ_ne_spec in H.
rewrite VertexMap.fold_1 in H. generalize H. apply fold_invariant. auto.
intros.
destruct x as (x,y).
assert (VertexMap.MapsTo x y (VertexMap.remove t0 (successors t0 (graph pm)))) as Hadj.
apply VertexMap.elements_2. rewrite InA_alt.
exists (x,y). split; auto. intuition.
unfold update in H2. destruct t1. simpl in H2.
case_eq (VertexMap.find x t1); intros; rewrite H3 in H2.
destruct v0. destruct s.
destruct (le_lt_dec n (e+eval y)).
apply H1. auto.
destruct (Vertex.eq_dec v x).
simpl in H2. rewrite add_eq_o in H2. inversion H2.
auto.
simpl in H2. rewrite add_neq_o in H2. auto.
auto.
apply H1. auto.
destruct (Vertex.eq_dec v x).
simpl in H2. rewrite add_eq_o in H2. inversion H2. auto.
simpl in H2. rewrite add_neq_o in H2. auto.
auto.
auto.
Qed.

Definition equiv_edge_eq : Equivalence Edge.eq := EMapFacts.KeySetoid.

Lemma path_construction : forall p pm v val r dist pred,
path p r v (graph pm) val ->
VertexMap.find r (map pm) = Some (Reached Optimal dist pred) ->
forall l d,
VertexMap.find v (map pm) = Some (Reached Open d l) ->
exists vc, exists vo,
exists p1, exists p2, eqlistA Edge.eq p (p1 ++ (vc, vo) :: p2) /\
exists do, exists lo, VertexMap.find vo (map pm) = Some (Reached Open do lo) /\
exists dc, exists lc, VertexMap.find vc (map pm) = Some (Reached Optimal dc lc).

Proof.
induction p; intros pm v val r dist pred H HH l d H0.
inversion H; subst.
rewrite (find_o _ (Vertex.eq_sym H1)) in H0.
rewrite H0 in HH. congruence.
eelim app_cons_not_nil. eauto.

inversion H; subst.
destruct p0. simpl in H1. inversion H1; subst. generalize H4. clear H4. intro Heq. clear H1.
generalize (path_nil_eq_end _ _ _ _ H2). intro. destruct H1. subst. simpl in *.
rewrite (find_o _ H1) in HH.
generalize (dynamic _ _ _ _ _ _ HH H3). intro.
exists v2. exists v. exists nil. exists nil. simpl. split.
constructor. auto. auto.
exists d. exists l. split. auto.
exists dist. exists pred. auto.

generalize H4. clear H4. intro Heq.
assert (a = t0 /\ eqlistA Edge.eq p (p0++(v2,v) :: nil)) as Hcut.
inversion H1; subst; split; auto.
apply eqlistA_app.

 apply equiv_edge_eq. intuition. constructor. auto. constructor.
destruct Hcut as [H4 Hcut]. subst. clear H1.

generalize (path_edge_charac _ _ _ _ _ _ H). intro.
do 2 destruct H1. destruct H1 as [H1 Hedge]; subst.
cut (path (p0 ++ (v2,v) :: nil) x v (graph pm) (val0 + eval w - eval x0)). intro.

generalize (consistant_status (map pm) x); intros.
destruct H5. do 2 destruct H5.

assert (path p x v (graph pm) (val0 + eval w - eval x0)) as Hp.
eapply path_eqlistA. eassumption. auto.

generalize (IHp pm v (val0 + eval w - eval x0) x _ _ Hp H5 _ _ H0). clear IHp. intro.
do 5 destruct H6. do 3 destruct H7.
exists x3. exists x4. exists (t0 :: x5). exists x6.
split.
repeat rewrite <-app_comm_cons. constructor. apply Edge.eq_refl.
apply eqlistA_trans with (l' := p0 ++ (v2,v) :: nil).
apply eqlistA_app. apply equiv_edge_eq. apply eqlistA_refl. constructor. auto. constructor.
apply eqlistA_trans with (l' := p). apply eqlistA_sym. auto. auto.
exists x7. exists x8. split. auto. auto.

destruct H5. do 2 destruct H5.
exists r. exists x. exists nil. exists (p0 ++ (v2,v) :: nil).
split. simpl. auto.
constructor. auto. apply eqlistA_app. apply equiv_edge_eq.
apply eqlistA_refl. constructor. auto. constructor.
exists x1. exists x2. split. auto.
exists dist. exists pred. auto.

assert (In_graph_labeled_edge (r,x) (graph pm) x0).
rewrite <-H1. assumption.
generalize (dynamic _ _ x _ _ x0 HH H6). intro.
do 4 destruct H7. destruct H5; congruence.

eapply path_end. eapply path_eqlistA. eassumption. constructor. apply Edge.eq_sym.
destruct x0. simpl. auto. simpl. auto.
apply eqlistA_sym. auto.
rewrite edge_label_spec. apply EdgeMap.find_1.
rewrite <-In_graph_labeled_edge_spec. rewrite H1 in Hedge. assumption.
Qed.

Lemma find_min_opt : forall pm p v e d l val,
find_min (set pm) = Some (d, e, l) ->
path p (root pm) v (graph pm) val ->
Vertex.eq v e ->
d <= val.

Proof.
intros.
generalize (find_min_1 _ _ _ _ H). intro.
rewrite (find_o _ (Vertex.eq_sym H1)) in H2.
destruct H2 as [p' H2]. destruct H2 as [H2 HH2].
generalize (path_construction _ _ _ _ _ _ _ H0 (root_find pm) _ _ HH2). intro.
do 5 destruct H3. do 3 destruct H4. do 2 destruct H5.
assert (d <= x3).
eapply find_min_2. eassumption.
eauto.
eapply le_trans. eassumption.
assert (In_graph_edge (x,x0) (graph pm)).
eapply in_path_in_graph with (p := x1 ++ (x,x0) :: x2).
rewrite InA_app_iff. right. constructor. apply Edge.eq_refl. apply equiv_edge_eq.
eapply path_eqlistA. eassumption. apply eqlistA_sym. auto.
rewrite In_graph_edge_spec in H7. rewrite EMapFacts.in_find_iff in H7.
generalize H7. clear H7. intro HH.
case_eq (edge_label (x,x0) (graph pm)); intros.
cut (x3 <= x5 + eval o). intro.
eapply le_trans. eassumption.

destruct (path_shorten_2 x1 x2 (root pm) v x x0 (graph pm) val).
eapply path_eqlistA. eassumption. apply eqlistA_sym. assumption.
destruct H9. generalize (is_path _ _ _ _ _ H5). intro.
apply (cut_path x1 (root pm) x (graph pm) x7 H9 (rev x6) x5 H11 x2 x0 v).
eapply shortest. eassumption. eassumption.
eapply path_eqlistA. eassumption. apply eqlistA_sym. auto. auto.

destruct (dynamic pm x x0 x5 x6 o). assumption.
rewrite edge_label_spec in H7.
rewrite In_graph_labeled_edge_spec. apply EdgeMap.find_2. assumption.
do 3 destruct H8.
rewrite H4 in H8. inversion H8; subst. auto.

rewrite edge_label_spec in H7. congruence.
Qed.

Lemma shortest_iteration : forall pm p v val d l,
                        path p (root pm) v (graph pm) val ->
                        VertexMap.find v (snd (fst (iteration pm))) = Some (Reached Optimal d l) ->
                        d <= val.

Proof.
intros. generalize H0. intro HH. unfold iteration in H0.
case_eq (find_min (set pm)); intros.
rewrite H1 in H0. destruct e. destruct p0.
generalize (find_min_1 pm t0 n l0 H1).
set (m := fold_succ_ne
                    (fun (_ : G.t) (_ x : Vertex.t) (w : option EdgeLabel)
                       (ms : VertexMap.t vertex_status * CoupleSet.t) =>
                     let (m, s) := ms in update t0 n l0 m w x s) t0
                    (graph pm) (map pm, set pm)) in *.
case_eq m; intros xxx yyy HHH; intros; rewrite HHH in *.
simpl in H0.
destruct (Vertex.eq_dec v t0).
rewrite add_eq_o in H0. simpl in H0. inversion H0.
eapply find_min_opt. rewrite H4 in H1. eauto. eauto.
auto.
auto.
rewrite add_neq_o in H0.
replace xxx with (fst (fold_succ_ne
       (fun (_ : G.t) (_ x : Vertex.t) (w : option EdgeLabel)
          (ms : VertexMap.t vertex_status * CoupleSet.t) =>
        let (m, s) := ms in update t0 n l0 m w x s) t0 (graph pm)
       (map pm, set pm))) in H0.
generalize (update_closed_inv _ _ _ _ _ _ _ H0). clear H0. intro.
eapply shortest. eassumption. eassumption.
unfold m in HHH. rewrite HHH. auto.
auto.
simpl in H0.
eapply shortest. eassumption.
rewrite H1 in H0. simpl in H0. eassumption.
Qed.

Lemma iteration_closed_charac : forall pm v d l,
VertexMap.find v (snd (fst (iteration pm))) = Some (Reached Optimal d l) ->
(exists min, find_min (set pm) = Some (d, min, l) /\ Vertex.eq v min) \/
VertexMap.find v (map pm) = Some (Reached Optimal d l).

Proof.
intros. unfold iteration in H.
case_eq (find_min (set pm)); intros. rewrite H0 in H.
destruct e. destruct p. simpl in H.
case_eq (fold_succ_ne
                   (fun (_ : G.t) (_ x : Vertex.t) (w : option EdgeLabel)
                      (ms : VertexMap.t vertex_status * CoupleSet.t) =>
                    let (m, s) := ms in update t0 n l0 m w x s) t0 (graph pm)
                   (map pm, set pm)); intros xxx yyy HHH; intros; rewrite HHH in *. simpl in H.
destruct (Vertex.eq_dec v t0).
rewrite add_eq_o in H.
generalize (find_min_1 _ _ _ _ H0). intro.
inversion H. subst.
left. exists t0. split; auto.
auto.
rewrite add_neq_o in H.
right.
generalize H. clear H.
replace xxx with (fst (fold_succ_ne
        (fun (_ : G.t) (_ x : Vertex.t) (w : option EdgeLabel)
           (ms : VertexMap.t vertex_status * CoupleSet.t) =>
         let (m, s) := ms in update t0 n l0 m w x s) t0 (graph pm)
        (map pm, set pm))).
rewrite fold_succ_ne_spec. rewrite VertexMap.fold_1.
apply fold_invariant. auto.
intros.
destruct x as (x,y). simpl in *.
unfold update in H2.
assert (VertexMap.MapsTo x y (VertexMap.remove t0 (successors t0 (graph pm)))) as Hadj.
apply VertexMap.elements_2. rewrite InA_alt.
exists (x,y). split; simpl. intuition. auto.
destruct t1. case_eq (VertexMap.find x t1); intros; rewrite H3 in H2.
destruct v0. destruct s.
destruct (le_lt_dec n1 (n + eval y)).
apply H1. auto.
destruct (Vertex.eq_dec v x).
simpl in H2. rewrite add_eq_o in H2. inversion H2.
auto.
simpl in H2. rewrite add_neq_o in H2.
apply H1. auto.
auto.
apply H1. auto.
destruct (Vertex.eq_dec v x).
simpl in H2. rewrite add_eq_o in H2.
inversion H2. auto.
simpl in H2. rewrite add_neq_o in H2.
apply H1. auto.
auto.
apply H1. auto.
rewrite HHH. auto.
auto.
auto.
rewrite H0 in H. simpl in H. right. auto.
Qed.

Definition update_list min d l :=
fun (a : VertexMap.t vertex_status * CoupleSet.t)
       (p : VertexMap.E.t * option nat) =>
     let (m, s0) := a in update min d l m (snd p) (fst p) s0.

Lemma update_list_eq_aux : forall v d l,
forall vl x y m, ~InA (@VertexMap.eq_key (option nat)) (x,y) vl ->
                                 VertexMap.find x (fst (fold_left (update_list v d l) vl m)) =
                                 VertexMap.find x (fst m).

Proof.
intros. apply fold_invariant.
auto.
intros. rewrite <-H1.
destruct x0 as (x0,y0). simpl.

assert (~Vertex.eq x0 x) as Hneq.
intro. elim H. rewrite InA_alt. exists (x0,y0). split; auto. eq_key_simpl.
unfold update_list in *. simpl.
case_eq t0; intros.
unfold update.
case_eq (VertexMap.find x0 t1); intros.
destruct v0. destruct s.
destruct (le_lt_dec n (d + eval y0)).
auto.
simpl. rewrite add_neq_o.
auto.
auto.
auto.
simpl. rewrite add_neq_o.
auto.
auto.
auto.
Qed.

Lemma update_list_eq : forall v d l,
forall vl x y m,
~InA (@VertexMap.eq_key (option nat)) (x,y) vl ->
VertexMap.find x (fst (fold_left (update_list v d l) ((x,y) :: vl) m)) =
VertexMap.find x (fst ((update_list v d l) m (x,y))).

Proof.
intros. apply fold_invariant_cons.
auto.
intros. rewrite <-H1.

destruct x0 as (x0,y0).
assert (~Vertex.eq x0 x) as Hneq.
intro. elim H. rewrite InA_alt. exists (x0,y0). split; auto. eq_key_simpl.
unfold update_list in *. simpl.
destruct t0. simpl. unfold update in *.
case_eq (VertexMap.find x0 t0); intros.
destruct v0. destruct s.
destruct (le_lt_dec n (d + eval y0)).
auto.
simpl. rewrite add_neq_o.
auto.
auto.
auto.
simpl. rewrite add_neq_o.
auto.
auto.
auto.
Qed.

Lemma equivalence_eq_key : Equivalence (@VertexMap.eq_key (option nat)).

Proof.
apply Build_Equivalence.
unfold Reflexive. eq_key_simpl.
unfold Symmetric. eq_key_simpl.
unfold Transitive. eq_key_simpl. intros. eapply Vertex.eq_trans; eauto.
Qed.

Lemma update_list_neq_aux : forall v d l,
forall vl x y x0 y0 m, ~Vertex.eq x y ->
InA (@VertexMap.eq_key (option nat)) (x,x0) vl ->
NoDupA (@VertexMap.eq_key (option nat)) ((y,y0) :: vl) ->
VertexMap.find x (fst (fold_left (update_list v d l) ((y,y0) :: vl) m)) =
VertexMap.find x (fst (fold_left (update_list v d l) vl m)).

Proof.
intros v d l vl x y x0 y0 m H H0 HND. rewrite InA_alt in H0. do 2 destruct H0.
generalize (In_split _ _ H1). intro. do 2 destruct H2.
rewrite H2. do 2 rewrite (find_o _ H0).
rewrite fold_left_app. rewrite app_comm_cons. rewrite fold_left_app.
destruct x1. change (fst (k,o)) with k.
rewrite update_list_eq. rewrite update_list_eq.
set (m1 := (fold_left (update_list v d l) ((y,y0) :: x2) m)) in *.
set (m2 := (fold_left (update_list v d l) x2 m)) in *.
unfold VertexMap.key in *. fold m1. fold m2.
unfold update_list. simpl.
unfold m1, m2.
case_eq m1; intros xxx1 yyy1 HHH1; intros.
case_eq m2; intros xxx2 yyy2 HHH2; intros.
assert (VertexMap.find k xxx1 = VertexMap.find k xxx2).
unfold m1, m2.
replace xxx1 with (fst (fold_left (update_list v d l) ((y, y0) :: x2) m)).
replace xxx2 with (fst (fold_left (update_list v d l) x2 m)).
rewrite update_list_eq_aux with (y := o).
rewrite update_list_eq_aux with (y := o). auto.
rewrite H2 in HND.
change ((y,y0) :: x2 ++ (k,o) :: x3) with ( ((y,y0) :: x2) ++ (k,o) :: x3) in HND.
generalize (NoDupA_swap equivalence_eq_key HND). intro.
inversion H3. subst. intro. elim H6.
right. rewrite InA_app_iff.
left. auto.
apply equivalence_eq_key.
intro. inversion H3; subst.
elim H. eq_key_simpl. rewrite H0. auto.
change ((y,y0) :: x2 ++ (k,o) :: x3) with ( ((y,y0) :: x2) ++ (k,o) :: x3) in HND.
generalize (NoDupA_swap equivalence_eq_key HND). intro.
inversion H2; subst.
elim H7. right. rewrite InA_app_iff. left. auto.
apply equivalence_eq_key.
fold m2. rewrite HHH2. auto.
fold m1. rewrite HHH1. auto.
fold m1. fold m2. rewrite HHH1. rewrite HHH2.
unfold update. rewrite H3.

case_eq (VertexMap.find k xxx2); intros.
destruct v0. destruct s.
destruct (le_lt_dec n (d + eval o)).
auto.
simpl. rewrite add_eq_o. rewrite add_eq_o. auto.
auto.
auto.
auto.
simpl. rewrite add_eq_o. rewrite add_eq_o.
auto.
auto.
auto.
auto.

intro. rewrite H2 in HND.
change ((y,y0) :: x2 ++ (k,o) :: x3) with ( ((y,y0) :: x2) ++ (k,o) :: x3) in HND.
generalize (NoDupA_swap equivalence_eq_key HND). intro.
inversion H4. subst.
elim H7. right. rewrite InA_app_iff. right. auto.
apply equivalence_eq_key.

intro. rewrite H2 in HND.
change ((y,y0) :: x2 ++ (k,o) :: x3) with ( ((y,y0) :: x2) ++ (k,o) :: x3) in HND.
generalize (NoDupA_swap equivalence_eq_key HND). intro.
inversion H4. subst.
elim H7. right. rewrite InA_app_iff. right. auto.
apply equivalence_eq_key.
Qed.

Lemma update_list_neq : forall v d l,
forall vl x y x0 y0 m, InA (@VertexMap.eq_key (option nat)) (x,x0) vl ->
NoDupA (@VertexMap.eq_key (option nat)) ((y,y0) :: vl) ->
VertexMap.find x (fst (fold_left (update_list v d l) ((y,y0) :: vl) m)) =
VertexMap.find x (fst (fold_left (update_list v d l) vl m)).

Proof.
intros. rewrite update_list_neq_aux with (x0 := x0). auto.
intro. inversion H0. subst.
elim H4. rewrite InA_alt in H. destruct H.
rewrite InA_alt. exists x1. split.
destruct H. rewrite <-H. eq_key_simpl. intuition.
auto.
inversion H0. auto.
Qed.

Lemma dynamic_continuation : forall pm v v' w d l,
VertexMap.find v (map pm) = Some (Reached Optimal d l) ->
In_graph_labeled_edge (v, v') (graph pm) w ->
exists s : status,
  exists d' : nat,
    exists l' : list Edge.t,
      VertexMap.find v' (snd (fst (iteration pm))) = Some (Reached s d' l') /\
      d' <= d + eval w.

Proof.
intros. unfold iteration.
generalize (dynamic _ _ _ _ _ _ H H0). intro Hdyn.
case_eq (find_min (set pm)); intros.
destruct e. destruct p.
generalize (find_min_1 _ _ _ _ H1). intro.

case_eq (fold_succ_ne
                     (fun (_ : G.t) (_ x : Vertex.t) (w0 : option EdgeLabel)
                        (ms : VertexMap.t vertex_status * CoupleSet.t) =>
                      let (m, s0) := ms in update t0 n l0 m w0 x s0) t0
                     (graph pm) (map pm, set pm)); intros xxx yyy HHH. simpl.
destruct (Vertex.eq_dec v' t0).
rewrite add_eq_o.
rewrite (find_o _ e) in Hdyn. destruct H2 as [p' H2]. destruct H2 as [H2 HH2].
rewrite HH2 in Hdyn.
exists Optimal. exists n. exists l0. split. auto.
destruct Hdyn. destruct H3. destruct H3. destruct H3. inversion H3; subst. auto.
auto.
rewrite add_neq_o.
replace xxx with (fst (fold_succ_ne
        (fun (_ : G.t) (_ x : Vertex.t) (w0 : option EdgeLabel)
           (ms : VertexMap.t vertex_status * CoupleSet.t) =>
         let (m, s0) := ms in update t0 n l0 m w0 x s0) t0 (graph pm)
        (map pm, set pm))).
rewrite fold_succ_ne_spec. rewrite VertexMap.fold_1.

apply fold_invariant. auto.
intros. destruct x as (x,y). simpl in *.
assert (VertexMap.MapsTo x y (VertexMap.remove t0 (successors t0 (graph pm)))) as Hadj.
apply VertexMap.elements_2. rewrite InA_alt.
exists (x,y). split. intuition. auto.
unfold update. destruct t1. case_eq (VertexMap.find x t1); intros.
destruct v0. destruct s.
destruct (le_lt_dec n1 (n + eval y)).
auto.
simpl. destruct (Vertex.eq_dec v' x).
rewrite add_eq_o.
exists Open. exists (n + eval y). exists ((t0,x) :: l0).
split. auto.
do 4 destruct H4. rewrite (find_o _ e) in H4.
simpl in H4. rewrite H5 in H4. inversion H4. subst.
apply le_trans with (m := x1). intuition. auto.
auto.
rewrite add_neq_o. auto. auto.
auto.
destruct (Vertex.eq_dec v' x).
simpl. rewrite add_eq_o.
exists Open. exists (n + eval y). exists ((t0,x) :: l0).
split. auto.
do 4 destruct H4. rewrite (find_o _ e) in H4.
simpl in H4. rewrite H5 in H4. inversion H4. auto.
simpl. rewrite add_neq_o. auto.
auto.
auto.
rewrite HHH. auto.
auto.
auto.
Qed.

Lemma dynamic_iteration : forall pm,
dynamic_prog (snd (fst (iteration pm))) (graph pm).

Proof.
unfold dynamic_prog. intros.
destruct (iteration_closed_charac _ _ _ _ H).
unfold iteration. destruct H1 as [min H1]. destruct H1 as [H1 HH1].
rewrite H1. simpl.
destruct (Vertex.eq_dec v' v).
case_eq (fold_succ_ne
                     (fun (_ : G.t) (_ x : Vertex.t) (w0 : option EdgeLabel)
                        (ms : VertexMap.t vertex_status * CoupleSet.t) =>
                      let (m, s0) := ms in update min d l m w0 x s0) min
                     (graph pm) (map pm, set pm)); intros xxx yyy HHH; simpl.
rewrite add_eq_o.
exists Optimal. exists d. exists l.
split; intuition.
rewrite e. auto.
case_eq (fold_succ_ne
                     (fun (_ : G.t) (_ x : Vertex.t) (w0 : option EdgeLabel)
                        (ms : VertexMap.t vertex_status * CoupleSet.t) =>
                      let (m, s0) := ms in update min d l m w0 x s0) min
                     (graph pm) (map pm, set pm)); intros xxx yyy HHH; simpl.
rewrite add_neq_o.
replace xxx with (fst (fold_succ_ne
        (fun (_ : G.t) (_ x : Vertex.t) (w0 : option EdgeLabel)
           (ms : VertexMap.t vertex_status * CoupleSet.t) =>
         let (m, s0) := ms in update min d l m w0 x s0) min (graph pm)
        (map pm, set pm))).
rewrite fold_succ_ne_spec. rewrite VertexMap.fold_1.

set (f := (fun (a : VertexMap.t vertex_status * CoupleSet.t)
                 (p : VertexMap.key * option EdgeLabel) =>
               let (m, s0) := a in update min d l m (snd p) (fst p) s0)) in *.

unfold Edge.t, VertexMap.key, Nat_as_OT.t in *. fold f.
generalize VertexMap.elements_1. intro.
generalize (H2 _ (VertexMap.remove min (successors min (graph pm))) v'). clear H2. intro.
assert (VertexMap.MapsTo v' w (VertexMap.remove min (successors min (graph pm)))).
apply VertexMap.remove_2. intro. elim n. rewrite HH1. auto.
rewrite mapsto_edge_equiv_succ.
assert (Edge.eq (min,v') (v,v')).
split; auto. simpl. rewrite H3. assumption.
generalize (H2 _ H3). clear H2 H3. intro.
generalize (VertexMap.elements_3w (VertexMap.remove min (successors min (graph pm)))). intro. unfold EdgeLabel in *.
unfold VertexMap.key, EdgeLabel in *.
induction (VertexMap.elements (elt := option nat) (VertexMap.remove (elt := option nat)
                 min (successors min (graph pm)))).
inversion H2.
inversion H2; subst.
assert (forall l x y m, ~InA (@VertexMap.eq_key (option nat)) (x,y) l ->
                                 VertexMap.find x (fst (fold_left f ((x,y) :: l) m)) =
                                 VertexMap.find x (fst (f m (x,y)))).
apply update_list_eq.

destruct a as (a,x). inversion H5; subst. simpl in H6. simpl in H7. subst.
rewrite (find_o _ H6). rewrite H4.
unfold f, update. simpl.
case_eq (VertexMap.find a (map pm)); intros.
destruct v0. destruct s.
case_eq (le_lt_dec n0 (d + eval x)); intros.
simpl. rewrite H7. exists Open. exists n0. exists l1. split; auto.
simpl. rewrite MapFacts.add_eq_o;[|auto].
exists Open. exists (d + eval x). exists ((min,a) :: l).
split; auto.
simpl. rewrite H7. exists Optimal. exists n0. exists l1. split; auto.
eapply shortest. eapply path_post. eapply path_iteration. eauto. eauto.
apply Edge.eq_refl. inversion H5; subst. simpl in *. subst.
rewrite (find_o _ H8). eauto.
simpl. rewrite MapFacts.add_eq_o;[|auto].
exists Open. exists (d + eval x). exists ((min,a) :: l).
split; auto.
simpl. rewrite H7.

assert (In_graph_vertex a (graph pm)).
rewrite In_graph_vertex_spec. rewrite <-H6. rewrite <-In_graph_vertex_spec.
apply (proj2 (In_graph_edge_in_ext _ _ (In_graph_edge_equiv _ _ _ H0))).
generalize (in_map_in_graph _ _ H8). rewrite MapFacts.in_find_iff. intro. unfold_data. congruence.

inversion H3. subst. auto.
assert (forall m, InA (@VertexMap.eq_key (option nat)) (v',w) l0 ->
                          VertexMap.find v' (fst (fold_left f (a :: l0) m)) =
                          VertexMap.find v' (fst (fold_left f l0 m))).
unfold f. destruct a as (y,y'). intro.
generalize (update_list_neq min d l l0 v' y w y' m).
unfold update_list. intros. apply H4.
auto. auto.

rewrite H4.
apply IHl0. auto.
inversion H3; auto.
rewrite InA_alt. rewrite InA_alt in H5. do 2 destruct H5.
exists x. split. inversion H5. subst. simpl in H7. eq_key_simpl. auto.
rewrite HHH. auto.
intro. elim n. rewrite <-H2. auto.

eapply dynamic_continuation; eauto.
Qed.

Lemma root_find_iter : forall pm,
VertexMap.find (root pm) (snd (fst (iteration pm))) = Some (Reached Optimal 0 nil).

Proof.
unfold iteration; intros.
case_eq (find_min (set pm)); intros.
destruct e. destruct p. simpl.
case_eq (fold_succ_ne
               (fun (_ : G.t) (_ x : Vertex.t) (w : option EdgeLabel)
                  (ms : VertexMap.t vertex_status * CoupleSet.t) =>
                let (m, s) := ms in update t0 n l m w x s) t0 (graph pm)
               (map pm, set pm)); intros xxx yyy HHH; intros.
simpl. replace xxx with (fst (fold_succ_ne
        (fun (_ : G.t) (_ x : Vertex.t) (w : option EdgeLabel)
           (ms : VertexMap.t vertex_status * CoupleSet.t) =>
         let (m, s) := ms in update t0 n l m w x s) t0 (graph pm)
        (map pm, set pm))).
rewrite add_neq_o.
rewrite fold_succ_ne_spec. rewrite VertexMap.fold_1.
apply fold_invariant. intros.
simpl. apply root_find.
intros. destruct x as (x,o). simpl in *.
unfold update. case_eq t1; intros. simpl in *.
case_eq (VertexMap.find x t2); intros.
destruct v. destruct s.
destruct (le_lt_dec n0 (n + eval o)).
auto.
rewrite <-H2. auto.
simpl. rewrite add_neq_o. rewrite H2 in H1. simpl in H1. auto.
intro. rewrite (find_o _ H4) in H3.
unfold Edge.t, Nat_as_OT.t in *.
rewrite H2 in H1. simpl in H1. rewrite H1 in H3. congruence.
auto.
rewrite <-H2. auto.
simpl. rewrite add_neq_o. rewrite H2 in H1. simpl in H1. auto.
intro. rewrite (find_o _ H4) in H3.
unfold Edge.t, Nat_as_OT.t in *.
rewrite H2 in H1. simpl in H1. rewrite H1 in H3. congruence.
simpl. rewrite H2 in H1. simpl in H1. auto.
intro.
generalize (root_find pm). intro.
generalize (find_min_1 _ _ _ _ H). intro.
rewrite (find_o _ H0) in H2. destruct H2. destruct H2. congruence.
rewrite HHH. auto.
simpl. apply root_find.
Qed.

Lemma in_map_in_graph_iter : forall pm v,
In_graph_vertex v (graph pm) -> VertexMap.In v (snd (fst (iteration pm))).

Proof.
intros. unfold iteration. rewrite MapFacts.in_find_iff.
case_eq (find_min (set pm)); intros.
destruct e. destruct p. simpl.
case_eq (fold_succ_ne
               (fun (_ : G.t) (_ x : Vertex.t) (w : option EdgeLabel)
                  (ms : VertexMap.t vertex_status * CoupleSet.t) =>
                let (m, s) := ms in update t0 n l m w x s) t0 (graph pm)
               (map pm, set pm)); intros xxx yyy HHH; intros.
simpl.
replace xxx with (fst (fold_succ_ne
        (fun (_ : G.t) (_ x : Vertex.t) (w : option EdgeLabel)
           (ms : VertexMap.t vertex_status * CoupleSet.t) =>
         let (m, s) := ms in update t0 n l m w x s) t0 (graph pm)
        (map pm, set pm))).
destruct (Vertex.eq_dec v t0).
rewrite add_eq_o.
congruence. auto.
rewrite add_neq_o.
rewrite fold_succ_ne_spec. rewrite VertexMap.fold_1.
apply fold_invariant. rewrite <-MapFacts.in_find_iff. apply in_map_in_graph. auto.

intros.
destruct x as (x,y). simpl.
assert (VertexMap.MapsTo x y (VertexMap.remove t0 (successors t0 (graph pm)))) as Hadj.
apply VertexMap.elements_2. rewrite InA_alt. exists (x,y).
split. intuition. auto.
unfold update. destruct t1. case_eq (VertexMap.find x t1); intros.
destruct v0. destruct s.
destruct (le_lt_dec n1 (n + eval y)).
auto.
simpl. destruct (Vertex.eq_dec v x).
rewrite add_eq_o. congruence. auto.
rewrite add_neq_o. auto. auto.
auto.
simpl. destruct (Vertex.eq_dec v x).
rewrite add_eq_o. congruence. auto.
rewrite add_neq_o. auto. auto.
auto.
auto.
rewrite HHH. auto.
simpl. rewrite <-in_find_iff. apply in_map_in_graph. auto.
Qed.

Lemma add_remove_cp : forall x y s,
~Couple.eq x y ->
CoupleSet.eq (CoupleSet.add x (CoupleSet.remove y s))
                      (CoupleSet.remove y (CoupleSet.add x s)).

Proof.
intros. intro. split; intros.
rewrite PS.Dec.F.add_iff in H0. rewrite PS.Dec.F.remove_iff.
rewrite PS.Dec.F.add_iff. rewrite PS.Dec.F.remove_iff in H0.
fold eq in *. simpl in *.
destruct H0. split. auto.
intro. elim H. do 2 destruct H0. do 2 destruct H1.
unfold Couple.eq. rewrite <-H0 in *. rewrite H1 in *.
split. split. auto. rewrite H3. auto.
eapply eqlistA_trans; eauto. intuition.
destruct H0. split. right. auto.
auto.
rewrite PS.Dec.F.add_iff. rewrite PS.Dec.F.remove_iff in H0.
rewrite PS.Dec.F.add_iff in H0. rewrite PS.Dec.F.remove_iff.
fold eq in *. simpl in *.
destruct H0. destruct H0. destruct H0. destruct H0.
left. split. split; auto. auto. auto.
Qed.

Lemma add_cp : forall x s s',
CoupleSet.eq s s' ->
CoupleSet.eq (CoupleSet.add x s) (CoupleSet.add x s').

Proof.
intros. apply PS.Dec.F.add_m. intuition. auto.
Qed.

Lemma remove_cp : forall x s s',
CoupleSet.eq s s' ->
CoupleSet.eq (CoupleSet.remove x s) (CoupleSet.remove x s').

Proof.
intros. apply PS.Dec.F.remove_m. intuition. auto.
Qed.

Lemma add_add_cp : forall x y s,
~Couple.eq x y ->
CoupleSet.eq (CoupleSet.add x (CoupleSet.add y s))
                      (CoupleSet.add y (CoupleSet.add x s)).

Proof.
intros. apply PS.add_add.
Qed.

Lemma remove_remove_cp : forall x y s,
~Couple.eq x y ->
CoupleSet.eq (CoupleSet.remove x (CoupleSet.remove y s))
                      (CoupleSet.remove y (CoupleSet.remove x s)).

Proof.
intros. intro.
split; intros.
do 2 rewrite PPS.remove_iff in *. fold eq in *.
destruct H0. destruct H0.
intuition.
do 2 rewrite PPS.remove_iff in *. fold eq in *.
destruct H0. destruct H0.
intuition.
Qed.

Lemma set_open_iter : forall pm d v p,
CoupleSet.In (d,v,p) (snd (iteration pm)) <-> exists p',
eqlistA Edge.eq p p' /\
VertexMap.MapsTo v (Reached Open d p') (snd (fst (iteration pm))).

Proof.
unfold iteration. intros. case_eq (find_min (set pm)); intros.
destruct e. destruct p0.
rewrite fold_succ_ne_spec. rewrite VertexMap.fold_1.
generalize VertexMap.elements_3w. intro.
generalize (H0 _ (VertexMap.remove t0 (successors t0 (graph pm)))). clear H0. intro HND.
generalize (set_open pm). intro.
generalize (find_min_1 _ _ _ _ H). intro.
assert (forall y, ~InA (@VertexMap.eq_key_elt (option nat)) (t0,y)
                               (VertexMap.elements (VertexMap.remove t0 (successors t0 (graph pm))))) as Hin.
intro. intro.
generalize (VertexMap.elements_2 H2). intro.
rewrite remove_mapsto_iff in H3. destruct H3. elim H3. auto.
generalize t0 n l (map pm) (set pm) H H0 HND H1 Hin. clear n t0 l H H0 HND H1 Hin. intro t0.
induction (VertexMap.elements (VertexMap.remove t0 (successors t0 (graph pm)))). simpl in *.
split; intros.
rewrite PS.Dec.F.remove_iff in H2. destruct H2. simpl in H3. fold eq in H3.
destruct (Vertex.eq_dec t0 v).
rewrite H0 in H2. destruct H2. destruct H2.
destruct H1. destruct H1.
generalize (VertexMap.find_1 H4). intro.
rewrite (find_o _ e) in H5. rewrite H6 in H5. inversion H5. subst.
elim H3. split. split; auto. rewrite H1. intuition.
rewrite H0 in H2. destruct H2. destruct H2.
exists x. split. intuition.
rewrite add_mapsto_iff. right. split; auto.
destruct H2. destruct H2. rewrite add_mapsto_iff in H3.
destruct H3. destruct H3. inversion H4.
rewrite PS.Dec.F.remove_iff. fold eq. simpl.
split. destruct H1.
rewrite H0. destruct H3. exists x. split; auto.
destruct H3. intuition.
intros.
set (f := (fun (a : VertexMap.t vertex_status * CoupleSet.t)
                            (p : VertexMap.key * option EdgeLabel) =>
                          let (m, s) := a in
                          update t0 n l0 m (snd p) (fst p) s)) in *.
case_eq (fold_left f (a :: l) (t1,t2)); intros. simpl.
replace t3 with (fst (fold_left f (a :: l) (t1, t2))).
replace t4 with (snd (fold_left f (a :: l) (t1, t2))).
cut (CoupleSet.In (d, v, p)
  (CoupleSet.remove (n, t0, l0) (snd (f (fold_left f l (t1,t2)) a))) <->
(exists p' : list (Vertex.t * Vertex.t),
   eqlistA eq p p' /\
   VertexMap.MapsTo v (Reached Open d p')
     (VertexMap.add t0 (Reached Optimal n l0)
        (fst (f (fold_left f l (t1, t2)) a))))); intros.
assert (CoupleSet.eq (snd (fold_left f (a :: l) (t1, t2)))
                                  (snd (f (fold_left f l (t1, t2)) a)) /\
            VertexMap.Equal (fst (fold_left f (a :: l) (t1,t2)))
                                        (fst (f (fold_left f l (t1,t2)) a))).
eapply fold_left_assoc_map_find_nodup.
intuition.
split; intros; destruct H4; destruct H5.
eapply CoupleSet.eq_trans; eauto.
eapply Equal_trans; eauto.
eauto.
unfold f. destruct s. unfold update. simpl. intro.
case_eq (VertexMap.find (fst y) t5); intros. destruct v0.
destruct s. case_eq (le_lt_dec n0 (n + eval (snd y))); intros.
case_eq (VertexMap.find (fst z) t5); intros.
destruct v0. destruct s.
case_eq (le_lt_dec n1 (n + eval (snd z))); intros.
rewrite H5. rewrite H6. intuition.
rewrite add_neq_o.
rewrite H5. rewrite H6. simpl. intuition.
eq_key_solve.
rewrite H5. rewrite H6. intuition.
rewrite add_neq_o.
rewrite H5. rewrite H6. intuition.
eq_key_solve.
rewrite H5. rewrite H6. intuition.
rewrite add_neq_o.
case_eq (VertexMap.find (fst z) t5); intros.
destruct v0. destruct s.
case_eq (le_lt_dec n1 (n + eval (snd z))); intros.
rewrite H5. rewrite H6. intuition.
rewrite add_neq_o. rewrite H5. rewrite H6. simpl.
split.

eapply CoupleSet.eq_trans. apply add_cp.
rewrite <-add_remove_cp. apply CoupleSet.eq_refl.
intro. elim H4. inversion H9. simpl in *. destruct H10. eq_key_solve.
eapply CoupleSet.eq_trans. apply add_add_cp.
intro. inversion H9; destruct H10; simpl in *; elim H4; eq_key_solve.
apply add_cp.
apply CoupleSet.eq_sym.
eapply CoupleSet.eq_trans. rewrite <-add_remove_cp.
apply CoupleSet.eq_refl.
intro. elim H4. inversion H9; destruct H10; simpl in *; eq_key_solve.
apply add_cp.
apply remove_remove_cp.
intro. elim H4; inversion H9; destruct H10; simpl in *; eq_key_solve.
auto.

apply add_add_Eq. eq_key_solve.
eq_key_solve.

rewrite H5. rewrite H6. intuition.
rewrite add_neq_o.
rewrite H5. rewrite H6. simpl. intuition.
eapply CoupleSet.eq_trans. rewrite add_add_cp. apply CoupleSet.eq_refl.
intro. inversion H3. fold eq in H11. simpl in *; elim H4; eq_key_solve. intuition.
apply add_cp. apply add_remove_cp.
intro. inversion H3. fold eq in H11. simpl in *; elim H4; eq_key_solve. intuition.
apply add_add_Eq. eq_key_solve. eq_key_solve.
rewrite H5. rewrite H6. simpl. intuition. eq_key_solve.
case_eq (VertexMap.find (fst z) t5); intros.
destruct v0. destruct s.
case_eq (le_lt_dec n1 (n + eval (snd z))); intros.
rewrite H5. intuition.
rewrite add_neq_o. rewrite H5. simpl. intuition.
eq_key_solve.
rewrite H5. intuition.
rewrite add_neq_o.
rewrite H5. intuition.
eq_key_solve.
simpl. rewrite H5. simpl. intuition.
rewrite add_neq_o.
case_eq (VertexMap.find (fst z) t5); intros.
destruct v0. destruct s.
case_eq (le_lt_dec n0 (n + eval (snd z))); intros.
rewrite H5. intuition.
rewrite add_neq_o. rewrite H5. simpl. intuition.
apply CoupleSet.eq_sym. eapply CoupleSet.eq_trans. rewrite add_add_cp. apply CoupleSet.eq_refl.
intro. inversion H3. fold eq in H11. simpl in *; elim H4; eq_key_solve. intuition.
apply add_cp. apply add_remove_cp.
intro. inversion H3. fold eq in H11. simpl in *; elim H4; eq_key_solve. intuition.
apply add_add_Eq. eq_key_solve. eq_key_solve.
rewrite H5. intuition.
rewrite add_neq_o. rewrite H5. simpl. intuition.
apply add_add_cp.
intro. inversion H3. fold eq in H10. simpl in *; elim H4; eq_key_solve. intuition.
apply add_add_Eq. eq_key_solve.
eq_key_solve.
rewrite H5. intuition.
eq_key_solve.
case_eq (VertexMap.find (fst z) t5); intros.
destruct v0. destruct s.
case_eq (le_lt_dec n0 (n + eval (snd z))); intros.
rewrite H5. intuition.
rewrite add_neq_o. rewrite H5. intuition.
eq_key_solve.
rewrite H5. intuition.
rewrite add_neq_o. rewrite H5. intuition.
eq_key_solve.
rewrite H5. intuition.
unfold f, update; intros.
destruct e2. destruct e1.
destruct H4. simpl in *.
case_eq (VertexMap.find (fst a0) t7); intros.
destruct v0. destruct s.
case_eq (le_lt_dec n0 (n + eval (snd a0))); intros.
rewrite <-(H5 (fst a0)) in *. rewrite H6 in *.
rewrite H7 in *. intuition.
rewrite <-(H5 (fst a0)) in *. rewrite H6 in *.
rewrite H7 in *. intuition.
simpl. apply add_cp. apply remove_cp.
intuition.
simpl. apply add_m. auto. auto. intuition.
rewrite <-(H5 (fst a0)) in *. rewrite H6 in *. intuition.
rewrite <-(H5 (fst a0)) in *. rewrite H6 in *. intuition.
apply add_cp. auto.
simpl. apply add_m. auto. auto. intuition.
rewrite <-(H5 (fst a0)) in *. rewrite H6 in *. intuition.

split; intros.
destruct H4.
assert (CoupleSet.In (d,v,p) (CoupleSet.remove (n,t0,l0) (snd (f (fold_left f l (t1,t2)) a)))).
apply (PPS.remove_m (Couple.eq_refl _) H4). auto.
clear H4 H5.
rewrite H3 in H7. destruct H7. destruct H4.
exists x. split. auto.
rewrite H6. auto.
destruct H5. destruct H5. destruct H4. rewrite H7 in H6.
assert (CoupleSet.In (d,v,p) (CoupleSet.remove (n,t0,l0) (snd (f (fold_left f l (t1,t2)) a)))).
rewrite H3. exists x. split; auto.
apply (PPS.remove_m (Couple.eq_refl _) H4). auto.

unfold f. fold f. inversion HND; subst.
assert (forall y, ~InA (@VertexMap.eq_key_elt (option nat)) (t0,y) l) as Hin2.
intros. intro. eelim Hin. right. eauto.
generalize (IHl n l0 t1 t2 H H0 H6 H1 Hin2). clear IHl. intro IHl.
unfold VertexMap.key, EdgeLabel, Nat_as_OT.t in *. fold f in IHl.
case_eq (fold_left f l (t1,t2)); intros. rewrite H3 in IHl. simpl in IHl.
unfold update.
case_eq (VertexMap.find (fst a) t5); intros.
destruct v0. destruct s.
case_eq (le_lt_dec n0 (n + eval (snd a))); intros.
simpl. auto.
simpl. split; intros.
rewrite PS.Dec.F.remove_iff in H8. fold eq in H8. destruct H8. simpl in H9.
rewrite PS.Dec.F.add_iff in H8. fold eq in H8. simpl in H8. destruct H8.
exists ((t0,fst a) :: l0).
split. intuition. rewrite add_mapsto_iff. right.
split.
intro. elim Hin with (y := snd a).
do 2 destruct H8. rewrite <-H12 in H10.
rewrite H10. left. destruct a. eq_key_solve.
rewrite add_mapsto_iff. left. split. intuition. destruct H8. destruct H8. subst. intuition.
assert (CoupleSet.In (d,v,p) (CoupleSet.remove (n,t0,l0) t6)).
rewrite PS.Dec.F.remove_iff. fold eq. split.
rewrite PS.Dec.F.remove_iff in H8. destruct H8. auto.
simpl. auto.
rewrite IHl in H10. destruct H10. destruct H10.
exists x. split. auto.
rewrite add_mapsto_iff in H11. rewrite add_mapsto_iff.
destruct H11. destruct H11. inversion H12.
right. split. intuition.
destruct H11. rewrite add_mapsto_iff. right.
split. intro.
generalize (VertexMap.find_1 H12). intro.
rewrite (find_o _ H13) in H4. rewrite H4 in H14.
inversion H14; subst.
rewrite PS.Dec.F.remove_iff in H8. destruct H8.
fold eq in H15. simpl in H15. elim H15. intuition.
auto.

rewrite PS.Dec.F.remove_iff. rewrite PS.Dec.F.add_iff. fold eq. simpl.
destruct H8. destruct H8. rewrite add_mapsto_iff in H9.
destruct H9. destruct H9. inversion H10.
destruct H9. rewrite add_mapsto_iff in H10. destruct H10. destruct H10.
inversion H11; subst. split. left. intuition.
intuition.
split. right. destruct H10.
assert (CoupleSet.In (d,v,p) (CoupleSet.remove (n,t0,l0) t6)).
rewrite IHl. exists x. split. auto.
rewrite add_mapsto_iff. right. split; auto.
rewrite PS.Dec.F.remove_iff. fold eq. simpl.
rewrite PS.Dec.F.remove_iff in H12. fold eq in H12. simpl in H12.
destruct H12. split. auto.
intro. destruct H14. destruct H14. elim H10. auto.
destruct H10. intuition.
auto.
simpl.

split; intros.
rewrite PS.Dec.F.remove_iff in H7. fold eq in H7. simpl in H7. destruct H7.
rewrite PS.Dec.F.add_iff in H7. fold eq in H7. simpl in H7. destruct H7.
exists ((t0,fst a) :: l0).
split. intuition.
do 2 destruct H7.
rewrite add_mapsto_iff.
right. split.
intro. elim Hin with (y := snd a).
rewrite <-H10 in H11.
rewrite H11. left. destruct a. eq_key_solve.
rewrite add_mapsto_iff. left. split. auto. rewrite H7. auto.
assert (CoupleSet.In (d,v,p) (CoupleSet.remove (n,t0,l0) t6)).
rewrite PS.Dec.F.remove_iff. fold eq. simpl. split; auto.
rewrite IHl in H9. destruct H9. destruct H9.
rewrite add_mapsto_iff in H10; do 2 destruct H10. inversion H11.
exists x. split. auto.
rewrite add_mapsto_iff. right. split. auto.
rewrite add_mapsto_iff. right. split. intro.
generalize (VertexMap.find_1 H11). intro.
rewrite (find_o _ H12) in H4. rewrite H4 in H13. inversion H13.
auto.

rewrite PS.Dec.F.remove_iff. rewrite PS.Dec.F.add_iff. fold eq. simpl.
do 2 destruct H7. rewrite add_mapsto_iff in H8.
do 2 destruct H8. inversion H9.
rewrite add_mapsto_iff in H9. destruct H9. destruct H9.
inversion H10; subst. split. left. intuition.
intuition.
split. right. destruct H9.
assert (CoupleSet.In (d,v,p) (CoupleSet.remove (n,t0,l0) t6)).
rewrite IHl. exists x. split. auto.
rewrite add_mapsto_iff. right. split; auto.
rewrite PS.Dec.F.remove_iff in H11. fold eq in H11. simpl in H11.
destruct H11. auto.
intuition.
auto.
rewrite H2. auto.
rewrite H2. auto.
simpl. apply set_open.
Qed.

Definition iteration_pathmap pm :=
let g := graph pm in
let r := root pm in
let m := map pm in
(fst (fst (iteration pm)), Make_pathmap g
                                                                r
                                                                (snd (fst (iteration pm)))
                                                                (path_iteration pm)
                                                                (shortest_iteration pm)
                                                                (dynamic_iteration pm)
                                                                (root_find_iter pm)
                                                                (in_map_in_graph_iter pm)
                                                                (snd (iteration pm))
                                                                (set_open_iter pm)).

Definition nonoptimal_vertices_nb (d : VertexMap.t vertex_status) :=
VertexMap.fold (fun x (s : vertex_status) n =>
                                  match s with
                                  | Unreached => S n
                                  | Reached Open _ _ => S n
                                  | _ => n
                                  end)
                        d
                        0.

Lemma open_vertices_nb_eq : forall v d d' m n n',
VertexMap.MapsTo v (Reached Open d n) m ->
nonoptimal_vertices_nb (VertexMap.add v (Reached Optimal d' n') m) <
nonoptimal_vertices_nb m.

Proof.
unfold nonoptimal_vertices_nb; intros.
generalize (add_elements_cons _ m v (Reached Open d n) (Reached Optimal d' n')
                   (VertexMap.find_1 H)). intro.
destruct H0. destruct H0. destruct H0. do 2 rewrite VertexMap.fold_1.
rewrite eqlistA_fold with (l2 := (x ++ (v, (Reached Optimal d' n')) :: x0)).
rewrite eqlistA_fold with (l1 := VertexMap.elements m) (l2 := (x ++ (v, (Reached Open d n)) :: x0)).
set (f := fun (a : nat) (p : VertexMap.key * vertex_status) =>
   match snd p with
   | Reached Open _ _ => S a
   | Reached Optimal _ _ => a
   | Unreached => S a
   end) in *.
rewrite fold_left_app. rewrite fold_left_app.
simpl. unfold f. fold f. simpl.
clear H0 H1.

assert (forall l n, fold_left f l n < fold_left f l (S n)).
induction l. simpl. auto.
simpl. unfold f. fold f.
destruct a. simpl. destruct v0. destruct s.
intros; apply IHl; auto.
intros; apply IHl; auto.
intros; apply IHl; auto.
apply H0.
auto.
intros. inversion H2. destruct x1. destruct y. simpl in *. rewrite H4. auto.
auto.
intros. inversion H2. destruct x1. destruct y. simpl in *. rewrite H4. auto.
Qed.

Lemma nonoptimal_vertices_nb_eq_up : forall v d d' m n n',
VertexMap.MapsTo v (Reached Open d n) m ->
nonoptimal_vertices_nb (VertexMap.add v (Reached Open d' n') m) =
nonoptimal_vertices_nb m.

Proof.
unfold nonoptimal_vertices_nb; intros.
generalize (add_elements_cons _ m v (Reached Open d n) (Reached Open d' n')
                   (VertexMap.find_1 H)). intro.
destruct H0. destruct H0. destruct H0. do 2 rewrite VertexMap.fold_1.
rewrite eqlistA_fold with (l2 := (x ++ (v, (Reached Open d' n')) :: x0)).
rewrite eqlistA_fold with (l1 := VertexMap.elements m) (l2 := (x ++ (v, (Reached Open d n)) :: x0)).
set (f := (fun (a : nat) (p : VertexMap.key * vertex_status) =>
   match snd p with
   | Reached Open _ _ => S a
   | Reached Optimal _ _ => a
   | Unreached => a
   end)) in *.
rewrite fold_left_app. rewrite fold_left_app.
simpl. unfold f. fold f. simpl. auto.
auto.
intros. inversion H2. destruct x1. destruct y. simpl in *. rewrite H4. auto.
auto.
intros. inversion H2. destruct x1. destruct y. simpl in *. rewrite H4. auto.
Qed.

Lemma nonoptimal_vertices_nb_eq_unreached : forall v d m n,
VertexMap.MapsTo v Unreached m ->
nonoptimal_vertices_nb (VertexMap.add v (Reached Open d n) m) =
nonoptimal_vertices_nb m.

Proof.
unfold nonoptimal_vertices_nb; intros.
generalize (add_elements_cons _ m v Unreached (Reached Open d n)
                   (VertexMap.find_1 H)). intro.
destruct H0. destruct H0. destruct H0. do 2 rewrite VertexMap.fold_1.
rewrite eqlistA_fold with (l2 := (x ++ (v, (Reached Open d n)) :: x0)).
rewrite eqlistA_fold with (l1 := VertexMap.elements m) (l2 := (x ++ (v, Unreached) :: x0)).
set (f := (fun (a : nat) (p : VertexMap.key * vertex_status) =>
   match snd p with
   | Reached Open _ _ => S a
   | Reached Optimal _ _ => a
   | Unreached => a
   end)) in *.
rewrite fold_left_app. rewrite fold_left_app.
simpl. unfold f. fold f. simpl. auto.
auto.
intros. inversion H2. destruct x1. destruct y. simpl in *. rewrite H4. auto.
auto.
intros. inversion H2. destruct x1. destruct y. simpl in *. rewrite H4. auto.
Qed.

Definition Dijkstra_measure (p : pathmap) := nonoptimal_vertices_nb (map p).

Function Dijkstra_aux (pm: pathmap) {measure Dijkstra_measure} : pathmap :=
let (o, iter) := iteration_pathmap pm in
match o with
| None => pm
| Some v => Dijkstra_aux iter
end.

Proof.
intros.
unfold Dijkstra_measure.
unfold iteration_pathmap in teq.
unfold iteration in teq. inversion teq. simpl.
case_eq (find_min (set pm)); intros.
destruct e. destruct p.
case_eq ( fold_succ_ne
               (fun (_ : G.t) (_ x : Vertex.t) (w : option EdgeLabel)
                  (ms : VertexMap.t vertex_status * CoupleSet.t) =>
                let (m, s) := ms in update t0 n l m w x s) t0 (graph pm)
               (map pm, set pm)); intros xxx yyy HHH.
simpl.
replace xxx with (fst (fold_succ_ne
        (fun (_ : G.t) (_ x : Vertex.t) (w : option EdgeLabel)
           (ms : VertexMap.t vertex_status * CoupleSet.t) =>
         let (m, s) := ms in update t0 n l m w x s) t0 (graph pm)
        (map pm, set pm))).
set (m := (fst
        (fold_succ_ne
           (fun (_ : G.t) (_ x : Vertex.t) (w : option EdgeLabel)
              (ms : VertexMap.t vertex_status * CoupleSet.t) =>
            let (m, s) := ms in update t0 n l m w x s) t0 (graph pm)
           (map pm, set pm)))) in *.
apply lt_le_trans with (m := nonoptimal_vertices_nb m).
generalize (find_min_1 _ _ _ _ H). intro.
destruct H2 as [p' H2]. destruct H2 as [H2 HH2].
apply open_vertices_nb_eq with (d := n) (n := p').
apply VertexMap.find_2.

unfold m. rewrite fold_succ_ne_spec. rewrite VertexMap.fold_1.
apply fold_invariant. auto.
intros. unfold update. destruct t1.
case_eq (VertexMap.find (fst x) t1); intros.
destruct v0. destruct s.
destruct (le_lt_dec n0 (n + eval (snd x))).
auto. simpl.
destruct (Vertex.eq_dec t0 (fst x)).
simpl in H4. rewrite (MapFacts.find_o _ e) in H4.
rewrite H4 in H5. inversion H5. rewrite H7 in l1.
elim (Lt.lt_irrefl n). intuition.
rewrite MapFacts.add_neq_o. auto.
auto.
simpl. simpl in H4. auto.
simpl. simpl in H4.
destruct (Vertex.eq_dec t0 (fst x)).
rewrite (MapFacts.find_o _ e) in H4. congruence.
rewrite MapFacts.add_neq_o. auto.
auto.
auto.

unfold m. rewrite fold_succ_ne_spec.
rewrite VertexMap.fold_1. apply fold_invariant. auto.
intros.
unfold update. destruct t1.
case_eq (VertexMap.find (fst x) t1); intros.
destruct v0. destruct s.
case_eq (le_lt_dec n0 (n + eval (snd x))); intros.
auto.
simpl. rewrite nonoptimal_vertices_nb_eq_up with (d := n0) (n := l0).
auto. apply VertexMap.find_2. auto.
auto.
simpl. rewrite nonoptimal_vertices_nb_eq_unreached. auto.
apply VertexMap.find_2. eauto.
auto.
rewrite HHH. auto.
auto.
simpl. rewrite H in *. simpl in *. congruence.
Qed.

Definition Dijkstra (g : G.t) (v : Vertex.t) := Dijkstra_aux (init g v).

Lemma iteration_root : forall pm v iter,
iteration_pathmap pm = (Some v, iter) ->
root pm = root iter.

Proof.
intros. unfold iteration_pathmap in H. inversion H. subst.
simpl. auto.
Qed.

Lemma Dijkstra_root_aux : forall t,
root (Dijkstra_aux t) = root t.

Proof.
intros. functional induction (Dijkstra_aux t0). simpl. auto.
simpl in *. rewrite IHp. rewrite (iteration_root pm v iter); auto.
Qed.

Lemma Dijkstra_root : forall g v,
root (Dijkstra g v) = v.

Proof.
unfold Dijkstra. intros. apply Dijkstra_root_aux.
Qed.

Lemma iteration_graph : forall pm v iter,
iteration_pathmap pm = (Some v, iter) ->
graph pm = graph iter.

Proof.
intros. unfold iteration_pathmap in H. inversion H. simpl. auto.
Qed.

Lemma Dijkstra_graph_aux : forall t,
graph (Dijkstra_aux t) = graph t.

Proof.
intros. functional induction (Dijkstra_aux t0). simpl. auto.
simpl in *. rewrite IHp. rewrite (iteration_graph pm v iter); auto.
Qed.

Lemma Dijkstra_graph : forall g v,
graph (Dijkstra g v) = g.

Proof.
intros. unfold Dijkstra. apply Dijkstra_graph_aux.
Qed.

Lemma Dijkstra_path : forall g v x st dist pred,
VertexMap.find x (map (Dijkstra g v)) = Some (Reached st dist pred) ->
path (rev pred) v x g dist.

Proof.
intros.
assert (path (rev pred) (root (Dijkstra g v)) x (graph (Dijkstra g v)) dist).
generalize (is_path (Dijkstra g v)). intro.
rewrite Dijkstra_root in *. rewrite Dijkstra_graph in *.
apply H0 with (s:=st) (d := dist). auto.
rewrite Dijkstra_root in *. rewrite Dijkstra_graph in *. auto.
Qed.

Lemma Dijkstra_optimal : forall g v x dist pred,
VertexMap.find x (map (Dijkstra g v)) = Some (Reached Optimal dist pred) ->
forall p val, path p v x g val ->
dist <= val.

Proof.
intros.
assert (path p (root (Dijkstra g v)) x (graph (Dijkstra g v)) val).
rewrite (Dijkstra_graph g v). rewrite (Dijkstra_root g v). auto.
eapply (shortest (Dijkstra g v) _ _ _ _ _ H1). eauto.
Qed.


Lemma iteration_pathmap_none : forall pm m,
iteration_pathmap pm = (None, m) ->
find_min (set pm) = None.

Proof.
unfold iteration_pathmap. intros.
assert (fst (fst (iteration pm)) = None).
inversion H; auto. clear H.
unfold iteration in H0.
case_eq (find_min (set pm)); intros.
rewrite H in H0. destruct e. destruct p.
case_eq (fold_succ_ne
                 (fun (_ : G.t) (_ x : Vertex.t) (w : option EdgeLabel)
                    (ms : VertexMap.t vertex_status * CoupleSet.t) =>
                  let (m, s) := ms in update t0 n l m w x s) t0 (graph pm)
                 (map pm, set pm)); intros xxx yyy HHH. rewrite HHH in H0.
simpl in H0. congruence.
rewrite H in H0. auto.
Qed.

Lemma infinite_none_no_open : forall pm d l,
find_min (set pm) = None ->
~exists v, VertexMap.find v (map pm) = Some (Reached Open d l).

Proof.
intros.
intro. destruct H0. unfold find_min in H.
generalize (CoupleSet.min_elt_3 H). intro.
generalize (VertexMap.find_2 H0). intro.
generalize (set_open pm d x l). intro.
assert (CoupleSet.In (d,x,l) (set pm)).
rewrite H3. exists l. split. intuition. auto.
elim H1 with (a := (d,x,l)). auto.
Qed.

Lemma find_min_none_charac : forall pm,
find_min (set pm) = None ->
forall v, In_graph_vertex v (graph pm) ->
VertexMap.find v (map pm) = Some Unreached \/
exists d, exists l, VertexMap.find v (map pm) = Some (Reached Optimal d l).

Proof.
intros.
destruct (consistant_status (map pm) v).
right. auto.
destruct H1. do 2 destruct H1.
generalize (infinite_none_no_open pm x x0 H). intro.
elim H2. exists v. auto.
destruct H1. left. auto.
generalize (in_map_in_graph pm v H0). rewrite in_find_iff. unfold_data. congruence.
Qed.

Lemma completeness : forall g r v,
In_graph_vertex v (graph (Dijkstra g r)) ->
VertexMap.find v (map (Dijkstra g r)) = Some Unreached \/
exists d, exists pred,
VertexMap.find v (map (Dijkstra g r)) = Some (Reached Optimal d pred).

Proof.
unfold Dijkstra. intros g r v Hin.
functional induction (Dijkstra_aux (init g r)).
generalize (iteration_pathmap_none _ _ e). clear e. intro.
generalize (find_min_none_charac pm H v Hin). clear H. intro. auto.
apply IHp0. auto.
Qed.

Lemma path_implies_reachable : forall pm p v val,
In_graph_vertex v (graph pm) ->
find_min (set pm) = None ->
path p (root pm) v (graph pm) val ->
VertexMap.find v (map pm) <> Some Unreached.

Proof.
intros pm p v val H H1 H2. intro H3.
assert (~Vertex.eq v (root pm)) as H0.
intro. rewrite (find_o _ H0) in H3.
rewrite root_find in H3. inversion H3.
assert (exists v, exists v', InA Edge.eq (v,v') (rev p) /\
           exists d, exists l, VertexMap.find v (map pm) = Some (Reached Optimal d l) /\
           VertexMap.find v' (map pm) = Some Unreached).

rewrite <-(rev_involutive p) in H2.
generalize v val H0 H H2 H3. clear v val H H0 H2 H3.
induction (rev p). intros. inversion H2; subst. elim H0. auto.
eelim app_cons_not_nil. eauto.

intros.
inversion H2; subst.
eelim app_cons_not_nil. eauto.
generalize (decompose_app _ _ _ _ H4). intro. destruct H8; subst. clear H4.
destruct (Vertex.eq_dec v2 (root pm)).
exists v2. exists v. split.
left. apply Edge.eq_sym. auto.
exists 0. exists nil. rewrite (find_o _ e). split. apply root_find. auto.
assert (In_graph_vertex v2 (graph pm)).
apply (proj1 (In_graph_edge_in_ext _ _ (In_graph_edge_equiv _ _ _ H6))).
generalize (find_min_none_charac _ H1 v2 H4). intro.
destruct H8.
generalize (IHl _ _ n H4 H5 H8). intro.
do 3 destruct H9.
exists x. exists x0.
split. right. auto. auto.
destruct H8. destruct H8.
exists v2. exists v. split.
left. apply Edge.eq_sym. auto.
exists x. exists x0. split. auto. auto.

do 3 destruct H4. do 3 destruct H5.
rewrite InA_rev in H4.
generalize (in_path_in_graph _ _ _ _ _ _ H4 H2). intro.
case_eq (edge_label (x,x0) (graph pm)); intros.
assert (In_graph_labeled_edge (x,x0) (graph pm) o).
rewrite In_graph_labeled_edge_spec.
rewrite edge_label_spec in H8. apply EdgeMap.find_2. auto.
generalize (dynamic pm x x0 x1 x2 o H5 H9). intro.
do 4 destruct H10.
unfold Edge.t, Nat_as_OT.t in *.
rewrite H6 in H10. congruence.
rewrite In_graph_edge_spec in H7. rewrite EMapFacts.in_find_iff in H7.
rewrite edge_label_spec in H8. congruence.
apply equiv_edge_eq.
Qed.

Lemma completeness_2 : forall g r v,
In_graph_vertex v (graph (Dijkstra g r)) ->
(exists p, exists val, path p (root (Dijkstra g r)) v (graph (Dijkstra g r)) val) ->
VertexMap.find v (map (Dijkstra g r)) <> Some Unreached.

Proof.
unfold Dijkstra. intros g r v Hin.
functional induction (Dijkstra_aux (init g r)). intro. destruct H. destruct H.
eapply path_implies_reachable. auto. auto. eapply iteration_pathmap_none. eauto. eauto.
apply IHp0. auto.
Qed.

Lemma correctness_aux : forall g r v val,
In_graph_vertex v (graph (Dijkstra g r)) ->
(exists p, path p (root (Dijkstra g r)) v (graph (Dijkstra g r)) val) ->
exists d, exists l, VertexMap.find v (map (Dijkstra g r)) =
Some (Reached Optimal d l) /\ d <= val /\ path (rev l) r v g d.

Proof.
intros.
assert (exists d, exists l, VertexMap.find v (map (Dijkstra g r)) =
Some (Reached Optimal d l)).
generalize (completeness_2 g r v H). intro.
unfold Dijkstra in *.
functional induction (Dijkstra_aux (init g r)). destruct H0.
generalize (iteration_pathmap_none _ _ e). intro.
destruct (find_min_none_charac _ H2 _ H).
destruct (Vertex.eq_dec v (root pm)).
rewrite (find_o _ e0). rewrite root_find. exists 0. exists nil. auto.
elim H1. exists x. exists val. auto. auto. auto.
apply IHp0; auto.
do 2 destruct H1.
exists x. exists x0. split. auto. destruct H0.
split.
eapply (shortest (Dijkstra g r) _ _ _ _ _ H0). eauto.
eapply Dijkstra_path. eauto.
Qed.

Lemma correctness : forall g r v val,
In_graph_vertex v g ->
(exists p, path p r v g val) ->
exists d, exists l,
VertexMap.find v (map (Dijkstra g r)) = Some (Reached Optimal d l) /\
d <= val /\
path (rev l) r v g d.

Proof.
intros. apply correctness_aux.
rewrite Dijkstra_graph. auto.
rewrite Dijkstra_graph. rewrite Dijkstra_root. auto.
Qed.

Definition shortest_path_length g v v' :=
let m := map (Dijkstra g v) in
let vs := VertexMap.find v' m in
match vs with
| None | Some Unreached => 0
| Some (Reached _ l _) => l
end.

End Shortest_path.