proposition: Lemma find_list_length: forall b x r l, vvalid g x -> pfoot' g (rev l) x = x -> valid_path' g (rev l) -> r = find_list b x l -> length r = b + length l \/ forall y, reachable g x y -> In_path g y (edge_list_head (rev l) x, r).
proof: Proof. induction b; intros; simpl in H2. - assert (r = rev l) by (destruct (projT2 is_null (dst g (out_edge x))); auto). clear H2. subst r. simpl. left. apply rev_length. - destruct ((projT2 is_null (dst g (out_edge x)))). + right. intros. rewrite <- H2 in *. clear l H2. assert (pfoot g (edge_list_head r x, r) = x) by (destruct r; [simpl in * | rewrite pfoot_head_irrel with (v2 := x); unfold pfoot]; auto). apply pfoot_in in H2. apply reachable_ind.reachable_ind in H3. destruct H3. 1: subst y; auto. exfalso. destruct H3 as [z [[? [? ?]] [? ?]]]. rewrite (dst_step g gLst x (dst g (out_edge x))) in H5; auto. rewrite <- H5 in p. apply reachable_head_valid in H7. apply (valid_not_null g z); auto. + specialize (IHb (dst g (out_edge x)) r (out_edge x :: l)). assert (vvalid g (dst g (out_edge x))). { destruct (vvalid_src_evalid g _ _ H); apply (@valid_graph _ _ _ _ g _ MA) in H4. destruct H4 as [_ ?]. destruct H4; auto. exfalso; auto. } specialize (IHb H3). assert (pfoot' g (rev (out_edge x :: l)) (dst g (out_edge x)) = dst g (out_edge x)). { simpl; apply (pfoot_last g (rev l) (out_edge x) (dst g (out_edge x))). } specialize (IHb H4). assert (valid_path' g (rev (out_edge x :: l))). { simpl. clear IHb H2 H4. remember (rev l) as l'. clear l Heql'. revert l' H0 H1. induction l'; intros. simpl in *. - hnf. pose proof (vvalid_src_evalid g _ _ H). destruct H2. rewrite H2. split; auto. - simpl in H1 |-* . assert (strong_evalid g a) by (destruct l'; [|destruct H1]; auto). destruct (l' +:: out_edge x) eqn:? ; auto. split; auto. destruct l'. + clear H2. simpl in H0, Heql. rewrite H0. inversion Heql. subst l. subst e. pose proof (vvalid_src_evalid g _ _ H). destruct H2. split; auto. apply IHl'; simpl; auto. + simpl in Heql. inversion Heql. subst e0. clear H2. destruct H1 as [? [? ?]]. split; auto. rewrite H6. apply IHl'; auto. } specialize (IHb H5 H2). destruct IHb; [left; simpl in H6; intuition | right]. intros. simpl in H6. apply reachable_ind.reachable_ind in H7. destruct H7. * subst y. destruct (find_list_foreside b (dst g (out_edge x)) (out_edge x :: l)) as [l' ?]. rewrite <- H2 in H7. simpl in H7. rewrite H7. right. exists (out_edge x). simpl. rewrite <- app_assoc. rewrite in_app_iff. simpl. split. 1: right; left; auto. left. pose proof (vvalid_src_evalid g _ _ H). destruct H8; auto. * destruct H7 as [z [[_ [_ ?]] [_ ?]]]. rewrite (dst_step g gLst x (dst g (out_edge x))) in H7; auto. rewrite H7 in H8. specialize (H6 _ H8). assert (edge_list_head (rev l +:: out_edge x) (dst g (out_edge x)) = edge_list_head (rev l) x). { remember (rev l ) as l'. destruct l'; simpl; auto. pose proof (vvalid_src_evalid g _ _ H); destruct H9; auto. } rewrite H9 in H6. 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