proposition: Lemma path_shorten: forall (g: Gph) (p: path) n1 n2, path_ends g p n1 n2 -> valid_path g p -> Dup (epath_to_vpath g p) -> exists p', length (snd p') < length (snd p) /\ Subpath g p' p /\ path_ends g p' n1 n2 /\ valid_path g p'.
proof: Proof. intros. apply Dup_cyclic in H1. destruct H1 as [a [L1 [L2 [L3 ?]]]]. rewrite <- app_comm_cons in H1. destruct (epath_to_vpath_split _ _ _ _ _ H0 H1) as [p1 [p2 [? [? [? [? ?]]]]]]. rewrite app_comm_cons in H6. destruct (epath_to_vpath_split _ _ _ _ _ H4 H6) as [p3 [p4 [? [? [? [? ?]]]]]]. exists (p1 +++ p4). split; [|split; [|split]]; [destruct p as [v p]; destruct p1 as [v1 p1]; destruct p2 as [v2 p2]; destruct p3 as [v3 p3]; destruct p4 as [v4 p4]; unfold path_glue, fst, snd in * ..|]. + clear - H2 H7 H10. inversion H2. subst p. rewrite !app_length. apply Plus.plus_lt_compat_l. inversion H7. rewrite app_length. destruct p3. 1: simpl in H10 |-* ; inversion H10; destruct L2; inversion H5. simpl; intuition. + clear - H2 H7. inversion H2. subst p. inversion H7. split. 2: left; simpl; auto. simpl. apply incl_app. * apply incl_appl, incl_refl. * apply incl_appr, incl_appr, incl_refl. + inversion H2; subst. clear H2. inversion H7. subst. clear H7. destruct H. split; simpl in H; auto. destruct p4. - rewrite app_nil_r in *. apply epath_to_vpath_pfoot in H5. rewrite H5. simpl in H11. inversion H11. subst L3. replace (L1 ++ a :: L2 +:: a) with ((L1 ++ a :: L2) +:: a) in H1. * apply epath_to_vpath_pfoot in H1. rewrite H2 in H1. auto. * rewrite <- app_assoc. rewrite app_comm_cons. auto. - rewrite pfoot_app_cons with (v2 := v1). rewrite app_assoc in H2. rewrite pfoot_app_cons with (v2 := v1) in H2. auto. + apply valid_path_merge; auto. exists a. split. apply epath_to_vpath_pfoot in H5. auto. apply epath_to_vpath_phead in H11; 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