proposition: Lemma fits_upath_reduced_list: forall p l g u v, fits_upath g l p -> In u p -> In v p -> exists p' l', connected_by_path g p' u v /\ fits_upath g l' p' /\ incl p' p /\ incl l' l.
proof: Proof. induction p; intros. contradiction. destruct p. destruct H0. destruct H1. 2: contradiction. 2: contradiction. subst u; subst v. destruct l. simpl in H. exists (a::nil); exists nil. split. unfold connected_by_path. split; simpl; auto. split. simpl; auto. unfold incl; split; intros; auto. simpl in H; contradiction. destruct l. simpl in H; contradiction. destruct H. destruct H0; destruct H1. ++ subst u; subst v. exists (a::nil); exists nil. split. unfold connected_by_path. split. simpl. apply adj_edge_vvalid in H; apply H. simpl; auto. split. simpl. apply adj_edge_vvalid in H; apply H. simpl; auto. unfold incl; split; intros; try contradiction. destruct H0. subst a0. left; auto. contradiction. ++ subst u. assert (exists (p' : upath) (l' : list E), connected_by_path g p' v0 v /\ fits_upath g l' p' /\ incl p' (v0 :: p) /\ incl l' l). apply IHp; auto. left; auto. destruct H0 as [p' [l' [? [? [? ?]]]]]. exists (a::p'). exists (e::l'). destruct H0. destruct H6. split. split. apply valid_upath_cons. apply H0. rewrite H6; simpl. exists e; auto. split. simpl; auto. rewrite last_error_cons. auto. unfold not; intros; subst p'. inversion H7. split. destruct p'. inversion H6. simpl. split. inversion H6; subst v1; auto. auto. unfold incl; split; intros. destruct H8. subst a0; left; auto. right; apply H4 in H8; auto. destruct H8. subst a0; left; auto. right; apply H5 in H8; auto. ++ subst v. assert (exists (p' : upath) (l' : list E), connected_by_path g p' u v0 /\ fits_upath g l' p' /\ incl p' (v0 :: p) /\ incl l' l). apply IHp; auto. left; auto. destruct H1 as [p' [l' [? [? [? ?]]]]]. exists (p'+::a). exists (l'+::e). destruct H1. destruct H6. split. split. apply valid_upath_app. apply H1. simpl. apply adj_edge_vvalid in H; apply H. rewrite H7; simpl. apply adjacent_symm. exists e; auto. split. rewrite (hd_error_app _ _ u); auto. rewrite (last_err_app _ _ a); auto. split. apply (fits_upath_app g p' (a::nil) l' nil e v0 a). auto. simpl. apply adj_edge_vvalid in H; apply H. auto. simpl; auto. apply adj_edge_sym; auto. unfold incl; split; intros. apply in_app_or in H8; destruct H8. right; apply H4; auto. destruct H8. subst a0; left; auto. contradiction. apply in_app_or in H8; destruct H8. right; apply H5; auto. destruct H8. subst a0; left; auto. contradiction. ++ assert (exists (p' : upath) (l' : list E), connected_by_path g p' u v /\ fits_upath g l' p' /\ incl p' (v0 :: p) /\ incl l' l). apply IHp; auto. destruct H3 as [p' [l' [? [? [? ?]]]]]. exists p'; exists l'. split. auto. split. auto. unfold incl; split; intros. right; apply H5; auto. right; apply H6; auto. Qed.
imports: Coq.Logic.Classical CertiGraph.lib.List_ext CertiGraph.lib.EquivDec_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_relation CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.FiniteGraph