proposition: Corollary path_partition_checkpoint2: forall (g: UAdjMatGG) {fg: FiniteGraph g} (l: list V) p l' a b, In a l -> ~ In b l -> connected_by_path g p a b -> fits_upath g l' p -> exists v1 v2, In v1 p /\ In v2 p /\ In v1 l /\ ~ In v2 l /\ (exists e, adj_edge g e v1 v2 /\ In e l').
proof: Proof. intros. apply (path_partition_checkpoint' g (filter (fun x => (in_dec V_EqDec x l)) (VList g)) (filter (fun x => negb (in_dec V_EqDec x l)) (VList g)) p l' a b ) in H2. 2: { apply filter_list_Permutation. apply NoDup_VList. } 2: { rewrite filter_In. split. rewrite VList_vvalid. apply connected_by_path_vvalid in H1; apply H1. destruct (in_dec V_EqDec a l). auto. contradiction. } 2: { rewrite filter_In. split. rewrite VList_vvalid. apply connected_by_path_vvalid in H1; apply H1. destruct (In_dec V_EqDec b l). contradiction. auto. } 2: auto. destruct H2 as [v1 [v2 [? [? [? [? ?]]]]]]. exists v1; exists v2. split. auto. split. auto. split. rewrite filter_In in H4. destruct H4. destruct (in_dec V_EqDec v1 l). auto. inversion H7. split. rewrite filter_In in H5. destruct H5. destruct (in_dec V_EqDec v2 l). inversion H7. auto. auto. Qed.
imports: VST.floyd.proofauto CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.find_lemmas CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.undirected_graph CertiGraph.graph.MathAdjMatGraph