proposition: Lemma valid_path'_find_list: forall bound v l, vvalid g v -> pfoot' g (rev l) v = v -> valid_path' g (rev l) -> valid_path' g (find_list bound v l).
proof: Proof. induction bound; intros. - assert (find_list 0 v l = rev l) by (simpl; destruct (projT2 is_null (dst g (out_edge v))); auto; destruct (equiv_dec v (dst g (out_edge v))); auto). rewrite H2. auto. - simpl. destruct (projT2 is_null (dst g (out_edge v))); auto. assert (vvalid g (dst g (out_edge v)) /\ src g (out_edge v) = v /\ evalid g (out_edge v)). { destruct is_null as [is_nullP ?]. simpl in *. pose proof (vvalid_src_evalid _ _ _ H). split; auto. destruct H2. destruct MA. apply valid_graph in H3. simpl in *. destruct H3. destruct H4; auto. exfalso; auto. } destruct H2 as [? [? ?]]. apply IHbound; auto. 1: simpl; pose proof (pfoot_last g (rev l) (out_edge v) (dst g (out_edge v))); simpl in H5; auto. destruct l; simpl in *; auto. + unfold strong_evalid. rewrite H3. split; [|split]; auto. + remember (rev l) as l'. clear Heql' l. induction l'. * simpl in *. split; auto. rewrite H0, H3. split; auto. unfold strong_evalid. rewrite H3. split; auto. * rewrite <- app_comm_cons in H0. simpl in H0. destruct (l' +:: e) eqn:? . 1: destruct l'; inversion Heql. rewrite <- Heql in *. clear e0 Heql. specialize (IHl' H0). clear H0. simpl in *. destruct ((l' +:: e) +:: out_edge v) eqn:? . 1: destruct l'; inversion Heql0. destruct (l' +:: e) eqn:? . 1: destruct l'; inversion Heql1. inversion Heql0. subst e1. destruct H1 as [? [? ?]]. split; [|split]; auto. simpl in Heql0. rewrite Heql0. apply IHl'. auto. Qed.
imports: CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.Ensembles_ext CertiGraph.lib.EnumEnsembles CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.MathGraph CertiGraph.graph.LstGraph CertiGraph.graph.FiniteGraph CertiGraph.graph.reachable_computable