proposition: Lemma list_expand_nil_or_single: forall root l r, vvalid G root -> is_list root -> l = @new_working_list _ _ is_null nil (map (dst G) (edge_func G root)) (root :: r) -> l = nil \/ (exists v, l = v :: nil /\ G |= root ~> v).
proof: Proof. intros. destruct l. 1: left; auto. destruct l. + right. exists v; split; auto. assert (In v (v :: nil)) by apply in_eq. rewrite H1 in H2. rewrite in_new_working_list in H2. destruct H2 as [? [? ?]]. rewrite app_nil_l in H2. rewrite <- edge_func_step in H2. split; [|split]; auto. rewrite step_spec in H2. destruct H2 as [e [? [? ?]]]. destruct (valid_graph G e H2) as [_ ?]. hnf in H7. rewrite H6 in H7. destruct H7; [exfalso |]; auto. + exfalso. destruct LF in H1. unfold edge_func in H1. simpl in H1. destruct (local_enumerable root) as [l' [? ?]]. simpl in H1. unfold Ensembles.In in i. destruct H0 as [lf [? ?]]. assert (forall v', In v' (v :: v0 :: l) -> reachable G root v'). { intros. rewrite H1 in H3. rewrite in_new_working_list in H3. rewrite app_nil_l in H3. destruct H3 as [? [? ?]]. rewrite in_map_iff in H3. destruct H3 as [e [? ?]]. exists (root, e :: nil). split; split; simpl; auto. + rewrite i in H6. destruct H6. unfold strong_evalid. rewrite H7. rewrite H3. do 3 (split; auto). destruct (valid_graph G e H6) as [_ ?]. hnf in H8. rewrite H3 in H8. destruct H8; [exfalso | ]; auto. + hnf. rewrite Forall_forall. intros; auto. } unfold new_working_list in H1. symmetry in H1. apply filter_2_cons in H1. destruct H1 as [l1 [l2 [l3 [? [? [? [? [? ?]]]]]]]]. simpl in H1. apply map_2_mid in H1. destruct H1 as [y1 [y2 [m1 [m2 [m3 [? [? [? [? [? ?]]]]]]]]]]. rewrite H1 in n. apply NoDup_app_r in n. apply NoDup_cons_2 in n. assert (reachable G root v) by apply H3, in_eq. assert (reachable G root v0) by apply H3, in_cons, in_eq. apply H2 in H14. apply H2 in H15. destruct H14 as [pv [[? ?] ?]]. destruct H15 as [pv0 [[? ?] ?]]. assert (G |= (root, y1 :: nil) is root ~o~> v satisfying (fun _ => True)). { split; split; intros; auto. 2: hnf; rewrite Forall_forall; intros; auto. simpl. unfold strong_evalid. rewrite H12. assert (In y1 l') by (rewrite H1; rewrite in_app_iff; right; apply in_eq). rewrite i in H20. destruct H20. rewrite H21. apply reachable_by_path_is_reachable in H14. apply reachable_foot_valid in H14. split; auto. } pose proof (H16 _ H20). assert (G |= (root, y2 :: nil) is root ~o~> v0 satisfying (fun _ => True)). { split; split; intros; auto. 2: hnf; rewrite Forall_forall; intros; auto. simpl. unfold strong_evalid. rewrite H13. assert (In y2 l') by (rewrite H1; rewrite in_app_iff; right; right; rewrite in_app_iff; right; apply in_eq). rewrite i in H22. destruct H22. rewrite H23. apply reachable_by_path_is_reachable in H15. apply reachable_foot_valid in H15. split; auto. } pose proof (H18 _ H22). apply n. rewrite in_app_iff. right. assert (In_path G v lf) by (apply (In_path_Subpath _ pv); auto; rewrite H21, <- H12; right; exists y1; simpl; tauto). assert (In_path G v0 lf) by (apply (In_path_Subpath _ pv0); auto; rewrite H23, <- H13; right; exists y2; simpl; tauto). pose proof (valid_path_reachable _ _ _ _ H0 H24 H25). destruct H26; destruct H26 as [[vl pl] ?]. - assert (G |= (path_glue (root, y1 :: nil) (vl, pl)) is root ~o~> v0 satisfying (fun _ => True)) by (apply reachable_by_path_merge with v; auto). unfold path_glue, fst, snd in H27. rewrite <- app_comm_cons, app_nil_l in H27. apply H18 in H27. rewrite H23 in H27. inversion H27. apply in_eq. - assert (G |= (path_glue (root, y2 :: nil) (vl, pl)) is root ~o~> v satisfying (fun _ => True)) by (apply reachable_by_path_merge with v0; auto). unfold path_glue, fst, snd in H27. rewrite <- app_comm_cons, app_nil_l in H27. apply H16 in H27. rewrite H21 in H27. inversion H27. apply in_eq. 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