proposition: Theorem is_list_is_list: forall root, vvalid G root -> EnumCovered Vertex (reachable G root) -> is_list root -> {l | graph_list_isomorphism l root}.
proof: Proof. intros. remember (@construct_reachable _ _ _ _ G is_null _ (length (proj1_sig X), root :: nil, nil)). destruct (finite_reachable_computable' _ _ X l H Heql). hnf in H1. exists (rev l). split; [|split]. + intros. destruct X as [ss [? ?]]. simpl in Heql. unfold Ensembles.In in i. assert (list_composed_by_edges (rev (root :: nil))) by (simpl; apply list_composed_by_edges_single). apply (construct_reachable_edge (length ss) _ nil H H0) in H3. hnf in H3. rewrite <- Heql in H3. split; intros. - destruct H4 as [? [? ?]]. pose proof H4. rewrite <- H1, in_rev in H4. apply in_split in H4. destruct H4 as [l1 [l2 ?]]. exists l1. destruct l2. * exfalso. pose proof H5. rewrite <- H1, in_rev, H4 in H8. rewrite in_app_iff in H8. simpl in H8. destruct H8 as [? | [? | ?]]; auto. 2: subst d; apply (is_list_no_self_loop root s); auto. destruct l1. 1: inversion H8. assert (v = root). { rewrite construct_reachable_unfold in Heql. destruct (le_dec (length ss) (length nil)). 1: rewrite Heql in H4; simpl in H4; inversion H4. remember (@new_working_list _ _ is_null nil (map (dst G) (edge_func G root)) (root :: nil)). simpl in Heql. destruct (construct_reachable_tail_preserve (length ss) l0 (root :: nil)) as [l' ?]. rewrite <- Heql in H9. rewrite H9 in H4. rewrite rev_unit in H4. simpl in H4. inversion H4. auto. } subst v. simpl in H8. destruct H8. 1: { subst d. destruct H0 as [pf [? ?]]. apply H8 in H5. clear H8. destruct H5 as [pr [[? ?] ?]]. assert (G |= (root, nil) is root ~o~> root satisfying (fun _ => True)) by (split; split; simpl; auto; red; simpl; auto). destruct H7 as [[vr ps] ?]. destruct H6 as [? [? ?]]. rewrite step_spec in H12. destruct H12 as [e [? [? ?]]]. assert (G |= (s, e :: nil) is s ~o~> root satisfying (fun _ => True)). { split; split; simpl; auto. + unfold strong_evalid. rewrite H13, H14. split; auto. + hnf. rewrite Forall_forall; intros; auto. } pose proof (reachable_by_path_merge _ _ _ _ _ _ _ H7 H15). unfold path_glue, fst, snd in H16. apply H8 in H10. apply H8 in H16. rewrite H10 in H16. inversion H16. destruct ps; simpl in H19; inversion H19. } 1: { apply in_split in H8. destruct H8 as [l0 [l2 ?]]. subst l1. assert (root :: l0 <> nil) by (intro HS; inversion HS). apply exists_last in H8. destruct H8 as [l' [a ?]]. rewrite app_comm_cons, e in H4. rewrite <- app_cons_assoc, <- app_assoc in H4. simpl in H4. specialize (H3 _ _ _ _ H4). assert (a = s) by (apply (is_list_edge_src_the_same root _ d); auto; rewrite <- H1, in_rev, H4, in_app_iff; right; apply in_eq). subst a. assert (NoDup (rev l)) by (apply Permutation_NoDup with (l := l); auto; apply Permutation_rev). rewrite H4 in H8. apply NoDup_app_r in H8. apply NoDup_cons_2 in H8. apply H8. simpl. right. rewrite in_app_iff. right. apply in_eq. } * specialize (H3 _ _ _ _ H4). assert (d = v) by (apply (is_list_edge_dst_the_same root s); auto). subst v. exists l2; auto. - destruct H4 as [l1 [l2 ?]]. split; [|split]; [apply H1; rewrite in_rev; rewrite H4; rewrite in_app_iff; right ..|]; [apply in_eq | right; apply in_eq |]. apply (H3 l1 l2); auto. + intros; rewrite <- in_rev, H1; tauto. + apply Permutation_NoDup with (l := l); auto. apply Permutation_rev. Qed.
imports: Coq.Arith.Arith CertiGraph.lib.Coqlib CertiGraph.lib.EnumEnsembles CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.subgraph2 CertiGraph.graph.MathGraph CertiGraph.graph.FiniteGraph CertiGraph.graph.reachable_computable Coq.Lists.List