proposition: Lemma valid_path_acyclic: forall (g : Gph) (p : path) n1 n2, path_ends g p n1 n2 -> valid_path g p -> exists p', Subpath g p' p /\ path_ends g p' n1 n2 /\ NoDup (epath_to_vpath g p') /\ valid_path g p'.
proof: Proof. intros until p. destruct p as [v p]. revert v. remember (length p). assert (length p <= n) by lia. clear Heqn. revert p H. induction n; intros. + assert (p = nil) by (destruct p; auto; simpl in H; exfalso; lia). subst. exists (v, nil). simpl. simpl in H1. split. 1: apply Subpath_refl. do 2 (split; auto). constructor. intro; inversion H2. apply NoDup_nil. + destruct (NoDup_dec EV (epath_to_vpath g (v, p))). - exists (v, p); split; [apply Subpath_refl | split; auto]. - destruct (path_shorten _ _ _ _ H0 H1 n0) as [[v2 p2] [? [? [? ?]]]]. simpl in H2. assert (length p2 <= n) by lia. specialize (IHn p2 H6 _ _ _ H4 H5). simpl in IHn, H3. destruct IHn as [p' [? ?]]. exists p'. split; auto. apply Subpath_trans with (v2, p2); 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