proposition: Lemma path_correct_unique_path: forall (g : @DijkGG size inf) prev dist src m p2m p2m', path_correct g prev dist src m p2m -> path_correct g prev dist src m p2m' -> p2m = p2m'.
proof: Proof. intros. destruct p2m, p2m'. destruct H as [? [? [? [? [? ?]]]]]. destruct H0 as [? [? [? [? [? ?]]]]]. clear H2 H7 H3 H8. destruct H1, H6. simpl in H1, H3. subst v v0. f_equal. simpl snd in *. revert m H H5 H4 H2 l0 H0 H10 H9 H6. apply (backwards_list_ind _ (fun l => forall m, valid_path g (src, l) -> acyclic_path g (src, l) -> Forall (fun x : E => Znth (snd x) prev = fst x) l -> pfoot g (src, l) = m -> forall l0 : list E, valid_path g (src, l0) -> acyclic_path g (src, l0) -> Forall (fun x : E => Znth (snd x) prev = fst x) l0 -> pfoot g (src, l0) = m -> l = l0)); intros. simpl in H2. subst m. pose proof (acyclic_foot_empty g _ _ H3 H4 H6). auto. remember (foot l1). symmetry in Heqo. destruct o. 2: { apply foot_none_nil in Heqo. subst l1. simpl in H7. subst m. symmetry in H7. eapply (acyclic_foot_empty g); eauto. } apply foot_explicit in Heqo. destruct Heqo as [l1' ?]. subst l1. assert (a = e). { destruct a, e. rewrite pfoot_last, (edge_dst_snd g) in H7. rewrite pfoot_last, (edge_dst_snd g) in H3. simpl snd in *. subst v0 v2. rewrite Forall_forall in H2. rewrite Forall_forall in H6. specialize (H2 (v,m)). specialize (H6 (v1, m)). simpl in H2, H6. spec H2. apply in_or_app. right. left. trivial. spec H6. apply in_or_app. right. left. trivial. rewrite H2 in H6. subst v1. trivial. } subst e. f_equal. rename src into src'. apply (H (src g a)). * rewrite valid_path_app in H0. tauto. * clear -H0 H1. red in H1 |- *. rewrite epath_to_vpath_eq in H1; trivial. rewrite valid_path_app in H0. rewrite epath_to_vpath_eq. 2: tauto. rewrite map_app in H1. rewrite app_comm_cons in H1. apply NoDup_app_l in H1. trivial. * rewrite Forall_app_iff in H2. tauto. * rewrite valid_path_app in H0. destruct H0. simpl in H8. destruct H8. apply H8. * rewrite valid_path_app in H4. tauto. * clear -H4 H5. red in H5 |- *. rewrite epath_to_vpath_eq in H5; trivial. rewrite valid_path_app in H4. rewrite epath_to_vpath_eq. 2: tauto. rewrite map_app in H5. rewrite app_comm_cons in H5. apply NoDup_app_l in H5. trivial. * rewrite Forall_app_iff in H6. tauto. * rewrite valid_path_app in H4. destruct H4. simpl in H8. destruct H8. apply H8. Qed.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.dijkstra.MathDijkGraph CertiGraph.dijkstra.dijkstra_spec_pure