proposition: Lemma toEdgeList_edge_reachable: forall root len x r, (forall e, In e (listEdges' Vertex Edge r) -> evalid g e /\ reachable g root (src g e) /\ reachable g root (dst g e)) -> reachable g root x -> forall e, In e (listEdges' Vertex Edge (toEdgeList (len, x, r))) -> evalid g e /\ reachable g root (src g e) /\ reachable g root (dst g e).
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 H0; auto | exfalso; intuition | apply H0; auto |]. simpl in H2. destruct (filterE (edge_func g x)) eqn:? . 1: apply H0; auto. specialize (IHn len (dst g e0) ((e0, dst g e0) :: r)). assert (In e0 (e0 :: l)) by (simpl; left; auto). rewrite <- Heql, filter_valid in H3. 2: rewrite Forall_forall; intros; rewrite edge_func_spec in H4; destruct H4; auto. destruct H3. rewrite edge_func_spec in H4. destruct H4. assert (reachable g root (dst g e0)). { apply reachable_edge with x; auto. hnf. rewrite step_spec. split; [|split]; [apply reachable_foot_valid in H1 | | exists e0; split]; auto. } apply IHn; auto; clear IHn. + unfold lengthInput. simpl. intuition. + intros. simpl in H7. destruct H7. 2: apply H0; auto. subst e1. rewrite H5; split; [|split]; 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