proposition: Lemma valid_path_unique_edge: forall (g : Gph) (p : path) s t e, path_ends g p s t -> valid_path g p -> In e (snd p) -> exists p1 p2, Subpath g (s, p1 ++ e :: p2) p /\ path_ends g (s, p1 ++ e :: p2) s t /\ valid_path g (s, p1 ++ e :: p2) /\ ~ In e p1 /\ ~ In e p2 /\ length (p1 ++ e :: p2) <= length (snd p).
proof: Proof. intros g p. destruct p as [v p]. simpl snd. revert v. remember (length p). assert (length p <= n) by lia. rewrite Heqn. clear Heqn. revert p H. induction n; intros. - assert (p = nil) by (destruct p; auto; simpl in H; lia). simpl in *. subst p. inversion H2. - simpl in H2. assert (v = s) by (destruct H0; now simpl in H0). subst v. apply in_split in H2. destruct H2 as [l1 [l2 ?]]. subst p. destruct (in_dec equiv_dec e l1). + apply in_split in i. destruct i as [l1' [l3 ?]]. subst l1. rename l1' into l1. assert (length (l1 ++ e :: l2) <= n) by (rewrite !app_length in *; simpl length in *; lia). assert (path_ends g (s, l1 ++ e :: l2) s t). { split; [simpl; auto|]. destruct H0. now rewrite (pfoot_app_cons _ _ s) in *. } assert (valid_path g (s, l1 ++ e :: l2)). { clear -H1. rewrite !valid_path_app, !valid_path_cons_iff in *. destruct H1 as [[? [? [? ?]]] [? [? ?]]]. split; auto. } assert (In e (l1 ++ e :: l2)) by (rewrite in_app_iff; right; now left). specialize (IHn _ H2 _ _ _ _ H3 H4 H5). destruct IHn as [p1 [p2 [? [? [? [? [? ?]]]]]]]. exists p1, p2. split; [|split; [|split; [|split; [|split]]]]; auto. * apply Subpath_trans with (s, l1 ++ e :: l2); auto. red. unfold In_path. simpl. split; [|now left]. apply incl_app. 2: now apply incl_appr. now do 2 apply incl_appl. * transitivity (length (l1 ++ e :: l2)); auto. rewrite !app_length. simpl. lia. + destruct (in_dec equiv_dec e l2); [clear n0|]. 2: exists l1, l2; split; [apply Subpath_refl | auto]. apply in_split in i. destruct i as [l3 [l2' ?]]. subst l2. rename l2' into l2. assert (length (l1 ++ e :: l2) <= n). { rewrite app_length in *; simpl length in *. rewrite app_length in H. simpl length in H. lia. } assert (path_ends g (s, l1 ++ e :: l2) s t). { split; [simpl; auto|]. destruct H0. rewrite app_comm_cons, app_assoc in H3. now rewrite (pfoot_app_cons _ _ s) in *. } assert (valid_path g (s, l1 ++ e :: l2)). { clear -H1. rewrite valid_path_app, valid_path_cons_iff in *. rewrite valid_path_app, valid_path_cons_iff in H1. destruct H1 as [? [? [? [? [? [? ?]]]]]]. split; auto. } assert (In e (l1 ++ e :: l2)) by (rewrite in_app_iff; right; now left). specialize (IHn _ H2 _ _ _ _ H3 H4 H5). destruct IHn as [p1 [p2 [? [? [? [? [? ?]]]]]]]. exists p1, p2. split; [|split; [|split; [|split; [|split]]]]; auto. * apply Subpath_trans with (s, l1 ++ e :: l2); auto. red. unfold In_path. simpl. split; [|now left]. apply incl_app. 1: now apply incl_appl. rewrite app_comm_cons, app_assoc. now apply incl_appr. * transitivity (length (l1 ++ e :: l2)); auto. do 2 (rewrite !app_length; simpl). lia. 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