proposition: Lemma uf_root_always_exists: forall x, EnumCovered Edge (evalid g) -> vvalid g x -> exists root, uf_root g x root.
proof: Proof. intros. remember (find_list (length (proj1_sig X)) x nil). remember (pfoot g (x, l)) as r. exists r. assert (valid_path g (x, l)) by (rewrite Heql; change x with (edge_list_head nil x); apply valid_path_find_list; simpl; auto). split; auto. - apply (reachable_path_in' g (x, l) x); [|left; simpl; auto]. split; split; auto. rewrite path_prop_equiv; intros; auto. - intros. apply reachable_ind.reachable_ind in H1. destruct H1; auto. assert (pfoot' g (rev nil) x = x) by (simpl; auto). assert (valid_path' g (rev nil)) by (simpl; auto). pose proof (find_list_length (length (proj1_sig X)) x l nil H H2 H3 Heql). clear H2 H3. rename H4 into H2. simpl in H2. rewrite PeanoNat.Nat.add_0_r in H2. destruct H1 as [z [? [? ?]]]. destruct H1 as [? [? ?]]. rewrite step_spec in H6. destruct H6 as [e [? [? ?]]]. assert (g |= (r, e :: nil) is r ~o~> z satisfying (fun _ => True)) by (split; split; simpl; auto; [unfold strong_evalid; rewrite H7, H8; intuition | hnf; rewrite Forall_forall; intros; auto]). exfalso. assert (g |= (x, l) is x ~o~> r satisfying (fun _ => True)) by (split; split; [| | | rewrite path_prop_equiv]; auto). assert (g |= (x, l +:: e) is x ~o~> z satisfying (fun _ => True)). { pose proof (reachable_by_path_merge _ _ _ _ _ _ _ H10 H9). unfold path_glue in H11. simpl in H11. auto. } destruct H2. + destruct X as [li [? ?]]. simpl in Heql, H2. unfold In in i. pose proof (lst_path_NoDup _ _ _ _ _ _ H11). simpl in H12. assert (incl (l +:: e) li) by (repeat intro; apply i; rewrite in_app_iff in H13; destruct H13 as [? | [? | ?]]; [apply (valid_path_evalid g x) in H13 | subst a | exfalso]; auto). pose proof (NoDup_incl_length H12 H13). rewrite app_length in H14. simpl in H14. intuition. + assert (In_path g z (x, l)) by (apply H2; exists (x, l +:: e); auto). pose proof (reachable_path_in' _ _ _ _ H10 _ H12). destruct H13 as [[v li] ?]. assert (g |= (v, li +:: e) is z ~o~> z satisfying (fun _ => True)). { pose proof (reachable_by_path_merge _ _ _ _ _ _ _ H13 H9). unfold path_glue in H14. simpl in H14; auto. } apply no_loop_path in H14. inversion H14. destruct li; inversion H17. 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