proposition: Lemma epath_to_vpath_split: forall (g: Gph) n l1 l2 p, valid_path g p -> epath_to_vpath g p = l1 ++ (n :: l2) -> exists p1 p2, p = p1 +++ p2 /\ valid_path g p1 /\ valid_path g p2 /\ epath_to_vpath g p1 = l1 +:: n /\ epath_to_vpath g p2 = n :: l2.
proof: Proof. intros g n. induction l1; intros. + rewrite app_nil_l in H0. exists (n, nil), p. simpl. split; [|split; [|split; [|split]]]; auto; destruct p as [v p]. - unfold path_glue. simpl. simpl in H. destruct p. 1: inversion H0; auto. f_equal; auto. simpl in H0. destruct H. subst v. destruct p; inversion H0; auto. - simpl in H0, H. destruct p. 1: inversion H0; subst; auto. destruct H. simpl in H0, H1. destruct p; [|destruct H1 as [? _]]; destruct H1 as [_ [? _]]; inversion H0; subst; auto. + destruct p as [v p]. rewrite <- app_comm_cons in H0. destruct p. 1: simpl in H0; inversion H0; destruct l1; inversion H3. specialize (IHl1 l2 (dst g e, p) (valid_path_cons _ _ _ _ H) (epath_to_vpath_cons _ _ _ _ _ _ H0)). destruct IHl1 as [p1 [p2 [? [? [? [? ?]]]]]]. exists (v, e :: (snd p1)), p2. split; [|split; [|split; [|split]]]; auto; destruct p1 as [v1 p1]; destruct p2 as [v2 p2]; unfold path_glue, fst, snd in *. - rewrite <- app_comm_cons. inversion H1. auto. - clear H4 H5 H0 H3. inversion H1. subst p. clear H1. destruct H. split; auto. simpl in *. destruct p1. * destruct (nil ++ p2); intuition. * rewrite <- H3 in H2. split; auto. destruct ((e0 :: p1) ++ p2); intuition. - rewrite <- app_comm_cons. inversion H1. subst p. clear H1 H3 H5. simpl epath_to_vpath in *. destruct p1. * rewrite <- H4. f_equal. destruct (nil ++ p2); inversion H0; auto. rewrite H7; auto. * rewrite H4. f_equal; auto. destruct ((e0 :: p1) ++ p2); inversion H0; auto. Qed.
imports: Coq.Logic.ProofIrrelevance Coq.micromega.Lia CertiGraph.lib.Coqlib CertiGraph.lib.EnumEnsembles CertiGraph.lib.List_ext CertiGraph.lib.EquivDec_ext CertiGraph.graph.graph_model Coq.Lists.List Coq.Lists.ListDec