proposition: Lemma construct_reachable_edge: forall lim root r, vvalid G root -> is_list root -> list_composed_by_edges (rev (root :: r)) -> list_composed_by_edges (rev (@construct_reachable _ _ _ _ G is_null _ (lim, root :: nil, r))).
proof: Proof. intros lim root r. remember (lengthInput (lim, root :: nil, r)) as n. assert (lengthInput (lim, root :: nil, r) <= n) by intuition. clear Heqn. revert n lim root r H. induction n; intros. + simpl in H. rewrite construct_reachable_unfold. destruct (le_dec lim (length r)); [apply (lcbe_rev_cons root) | exfalso]; intuition. + rewrite construct_reachable_unfold. unfold lengthInput in H, IHn. destruct (le_dec lim (length r)). 1: apply (lcbe_rev_cons root); auto. remember (@new_working_list _ _ is_null nil (map (dst G) (edge_func G root)) (root :: r)). assert (l = nil \/ exists v, l = (v :: nil) /\ G |= root ~> v) by (apply (list_expand_nil_or_single _ _ r); auto). destruct H3. - clear Heql. subst l. simpl. rewrite construct_reachable_unfold. auto. - destruct H3 as [v [? ?]]. rewrite H3. simpl. apply IHn. * simpl. clear - H n0. intuition. * hnf in H4. intuition. * apply (is_list_edge root); auto. * apply lcbe_rev_cons_inv; auto. 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