proposition: Lemma is_list_edge_dst_the_same: forall root s d v, vvalid G root -> is_list root -> reachable G root s -> G |= s ~> d -> G |= s ~> v -> d = v.
proof: Proof. intros. assert (reachable G root d) by (apply reachable_edge with s; auto). assert (reachable G root v) by (apply reachable_edge with s; auto). destruct H0 as [pf [? ?]]. apply H6 in H4. destruct H4 as [pd [[? ?] ?]]. apply H6 in H5. destruct H5 as [pv [[? ?] ?]]. assert (In_path G v pf) by (apply In_path_Subpath with pv; auto; destruct H5 as [[_ ?] _]; apply pfoot_in; auto). assert (In_path G d pf) by (apply In_path_Subpath with pd; auto; destruct H4 as [[_ ?] _]; apply pfoot_in; auto). pose proof (valid_path_reachable _ _ _ _ H0 H11 H12). clear H8 H10 H11 H12. destruct H2 as [? [? ?]]. rewrite step_spec in H10. destruct H10 as [ed [? [? ?]]]. destruct H3 as [? [? ?]]. rewrite step_spec in H15. destruct H15 as [ev [? [? ?]]]. destruct H1 as [ps ?]. assert (G |= (s, ed :: nil) is s ~o~> d satisfying (fun _ => True)). { split; split; simpl; auto. + unfold strong_evalid. rewrite H11, H12; split; auto. + hnf. rewrite Forall_forall; intros; auto. } assert (G |= (s, ev :: nil) is s ~o~> v satisfying (fun _ => True)). { split; split; simpl; auto. + unfold strong_evalid. rewrite H16, H17; split; auto. + hnf. rewrite Forall_forall; intros; auto. } destruct ps as [vs ps]. assert (vs = root) by (destruct H1 as [[? _] _]; simpl in H1; auto). subst vs. pose proof (reachable_by_path_merge _ _ _ _ _ _ _ H1 H18). unfold path_glue, fst, snd in H20. pose proof (reachable_by_path_merge _ _ _ _ _ _ _ H1 H19). unfold path_glue, fst, snd in H21. clear H4 H5. pose proof (H7 _ H20). pose proof (H9 _ H21). destruct H13. + destruct H13 as [[v' pv'] ?]. assert (v' = v) by (destruct H13 as [[? _] _]; simpl in H13; auto). subst v'. pose proof (reachable_by_path_merge _ _ _ _ _ _ _ H21 H13). unfold path_glue, fst, snd in H22. apply H7 in H22. rewrite H4 in H22. inversion H22. pose proof (f_equal (@length Edge) H24). rewrite !app_length in H23. simpl in H23. assert (length pv' = 0) by intuition. destruct pv'. 2: inversion H25. clear H23 H25. rewrite app_nil_r in H24. apply app_inj_tail in H24. destruct H24. subst ed. rewrite H12 in H17. auto. + destruct H13 as [[d' pd'] ?]. assert (d' = d) by (destruct H13 as [[? _] _]; simpl in H13; auto). subst d'. pose proof (reachable_by_path_merge _ _ _ _ _ _ _ H20 H13). unfold path_glue, fst, snd in H22. apply H9 in H22. rewrite H5 in H22. inversion H22. pose proof (f_equal (@length Edge) H24). rewrite !app_length in H23. simpl in H23. assert (length pd' = 0) by intuition. destruct pd'. 2: inversion H25. clear H23 H25. rewrite app_nil_r in H24. apply app_inj_tail in H24. destruct H24. subst ed. rewrite H12 in H17. auto. Qed.
imports: Coq.Arith.Arith CertiGraph.lib.Coqlib CertiGraph.lib.EnumEnsembles CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.subgraph2 CertiGraph.graph.MathGraph CertiGraph.graph.FiniteGraph CertiGraph.graph.reachable_computable Coq.Lists.List