proposition: Lemma lst_src_dst_determine_path: forall p x y P, g |= p is x ~o~> y satisfying P -> unique (fun pa : path => g |= pa is x ~o~> y satisfying P) p.
proof: Proof. intros. hnf. split; auto. intros p2 ?. destruct p as [v1 p1]. destruct p2 as [v2 p2]. f_equal. - destruct H as [[? _] _]. destruct H0 as [[? _] _]. simpl in H, H0. subst v1 v2; auto. - destruct (Compare_dec.le_dec (length p1) (length p2)). + destruct (lst_reachable_unique v1 p1 v2 p2 x y y P H H0 l) as [p3 [? ?]]. assert (g |= (y, p3) is y ~o~> y satisfying (fun _ => True)) by (apply reachable_by_path_weaken with P; auto; unfold Included, Ensembles.In; intros; auto). apply no_loop_path in H3. inversion H3. subst p3 p2. rewrite app_nil_r; auto. + assert (length p2 <= length p1) by intuition. rename H1 into l. destruct (lst_reachable_unique v2 p2 v1 p1 x y y P H0 H l) as [p3 [? ?]]. assert (g |= (y, p3) is y ~o~> y satisfying (fun _ => True)) by (apply reachable_by_path_weaken with P; auto; unfold Included, Ensembles.In; intros; auto). apply no_loop_path in H3. inversion H3. subst p3 p1. rewrite app_nil_r; auto. Qed.
imports: Coq.Classes.Morphisms Coq.micromega.Lia Coq.Logic.FunctionalExtensionality CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.EnumEnsembles CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.MathGraph CertiGraph.graph.FiniteGraph