proposition: Lemma toEdgeList_reachable: forall root len x r, reachable g root x -> (forall v, In v (listVertices' Vertex Edge r) -> reachable g root v) -> forall v, In v (listVertices' Vertex Edge (toEdgeList (len, x, r))) -> reachable g root v.
proof: Proof. intros root len x r. remember (lengthInput (len, x, r)) as n. assert (lengthInput (len, x, r) <= n) by lia. clear Heqn. revert len x r H. induction n; intros; simpl; unfold lengthInput in H; rewrite toEdgeList_unfold in H2; destruct (Compare_dec.le_dec len (length r)); [apply H1; auto | exfalso; intuition | apply H1; auto |]. simpl in H2. destruct (filterE (edge_func g x)) eqn:? . 1: apply H1; auto. specialize (IHn len (dst g e) ((e, dst g e) :: r)). assert (reachable g root (dst g e)). { assert (In e (e :: l)) by (simpl; left; auto). rewrite <- Heql in H3. rewrite filter_valid in H3. 2: rewrite Forall_forall; intros; rewrite edge_func_spec in H4; destruct H4; auto. apply reachable_edge with x; auto. destruct H3. rewrite edge_func_spec in H4. hnf. rewrite step_spec. apply reachable_foot_valid in H0. intuition. exists e. intuition. } apply IHn; auto. 1: simpl; intuition. simpl; intros. destruct H4. 2: apply H1; auto. subst v0. auto. Qed.
imports: Coq.Classes.Morphisms Coq.micromega.Lia Coq.Logic.FunctionalExtensionality CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.EnumEnsembles CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.FiniteGraph