proposition: Lemma acyclic_foot_empty: forall (g : AdjMatGG) src l, valid_path g (src, l) -> acyclic_path g (src, l) -> pfoot g (src, l) = src -> l = nil.
proof: Proof. destruct l; auto. intros. exfalso. assert (fst e = src). { destruct H. rewrite (edge_src_fst g) in H. auto. } apply pfoot_ptail in H1. simpl ptail in H1. rewrite pfoot_spec in H1. destruct H1. * rewrite (edge_dst_snd g) in H1. inversion H1. subst. red in H0. simpl in H0. rewrite (edge_src_fst g), (edge_dst_snd g) in H0. rewrite H4 in H0. inversion H0. apply H5. left. trivial. * destruct H1 as [v' [l' [e' [? ?]]]]. subst src. inversion H1. subst v' l. rename H into Hx. clear H1. red in H0. rewrite <- (edge_src_fst g) in H2. rewrite epath_to_vpath_cons_eq in H0; auto. rewrite NoDup_cons_iff in H0. destruct H0 as [? _]. apply H. clear H H2. rewrite in_path_eq_epath_to_vpath. eapply path_ends_In_path_dst. split. reflexivity. rewrite pfoot_last. trivial. apply valid_path_tail in Hx. apply Hx. Qed.
imports: Coq.ZArith.BinInt Coq.Classes.EquivDec compcert.lib.Integers CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.FiniteGraph CertiGraph.graph.path_lemmas