proposition: Lemma redirect_to_root: forall x root p l v, vvalid g x -> ~ reachable g root x -> (forall y, reachable g root y -> root = y) -> valid_path (pregraph_gen_dst g (out_edge x) root) (p, l) -> pfoot (pregraph_gen_dst g (out_edge x) root) (p, l) = v -> (valid_path g (p, l) /\ pfoot g (p, l) = v) \/ (v = root /\ exists l1, l = l1 ++ (out_edge x) :: nil /\ g |= (p, l1) is p ~o~> x satisfying (fun _ => True)).
proof: Proof. intros. assert ((pregraph_gen_dst g (out_edge x) root) |= (p, l) is p ~o~> v satisfying (fun _ => True)) by (split; split; auto; rewrite path_prop_equiv; intros; auto). destruct (in_dec EE (out_edge x) l). 2: rewrite no_edge_gen_dst_equiv in H4; auto; destruct H4 as [[_ ?] [? _]]; left; auto. pose proof (gen_dst_preserve_lst g gLst _ _ H0 H). pose proof (lst_path_NoDup _ H5 _ _ _ _ H4). simpl snd in *. apply in_split in i. destruct i as [l1 [l2 ?]]. rewrite H7 in H3. rewrite List_ext.app_cons_assoc in H7. rewrite H7 in H2. apply valid_path_app in H2. destruct H2. rewrite pfoot_last in H8. rewrite (pfoot_app_cons _ _ root) in H3. rewrite pfoot_cons in H3. simpl dst in *. unfold updateEdgeFunc in *. destruct (equiv_dec (out_edge x) (out_edge x)). 2: compute in c; exfalso; apply c; auto. rewrite <- List_ext.app_cons_assoc in H7. rewrite H7 in H6. apply NoDup_remove_2 in H6. assert ((pregraph_gen_dst g (out_edge x) root) |= (root, l2) is root ~o~> v satisfying (fun _ => True)) by (split; split; auto; rewrite path_prop_equiv; intros; auto). assert (~ List.In (out_edge x) l1 /\ ~ List.In (out_edge x) l2) by (split; intro; apply H6; rewrite in_app_iff; [left | right]; auto). clear H6. destruct H10. rewrite no_edge_gen_dst_equiv in H9; auto. assert (root = v) by (apply H1; exists (root, l2); auto). subst v. rewrite <- H11 in *. apply no_loop_path in H9. inversion H9. subst l2. right. clear H11 H9 H10. pose proof (pfoot_split _ _ _ _ _ H2). simpl src in H3. apply valid_path_app in H2. destruct H2. pose proof (@only_one_edge _ _ _ _ _ _ gLst x (out_edge x) H). assert ((out_edge x) = (out_edge x)) by auto. rewrite <- H10 in H11. clear H10. destruct H11. rewrite H10 in H3. assert ((pregraph_gen_dst g (out_edge x) root) |= (p, l1) is p ~o~> x satisfying (fun _ => True)) by (split; split; auto; rewrite path_prop_equiv; intros; auto). rewrite no_edge_gen_dst_equiv in H12; auto. split; [|exists l1; split]; 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