proposition: Lemma reachable_edge_toEdgeList: forall root len x r (X: EnumCovered Vertex (reachable g root)), is_list g root -> length (proj1_sig X) <= len -> reachable g root x -> NoDup (listEdges' Vertex Edge r) -> (forall e, evalid g e -> reachable g root (src g e) -> vvalid g (dst g e) -> reachable g x (src g e) \/ In e (listEdges' Vertex Edge r)) -> (forall e, In e (listEdges' Vertex Edge r) -> evalid g e /\ reachable g root (src g e) /\ vvalid g (dst g e)) -> (forall e, evalid g e -> reachable g x (src g e) -> vvalid g (dst g e) -> ~ In e (listEdges' Vertex Edge r)) -> forall e, evalid g e -> reachable g root (src g e) -> vvalid g (dst g e) -> In e (listEdges' Vertex Edge (toEdgeList (len, x, r))).
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 H0. assert (forall s e1 e2, reachable g root s -> src g e1 = s -> src g e2 = s -> evalid g e1 -> evalid g e2 -> vvalid g (dst g e1) -> vvalid g (dst g e2) -> e1 = e2) by (intros s e1 e2; apply (is_list_same_src_same_edge g root); auto). induction n; intros; simpl; unfold lengthInput in H1; rewrite toEdgeList_unfold; destruct (Compare_dec.le_dec len (length r)). - apply (listEdges'_In_length_reachable _ _ g root len _ X); auto. - exfalso; intuition. - apply (listEdges'_In_length_reachable _ _ g root len _ X); auto. - assert (HS: Forall (evalid g) (edge_func g x)) by (rewrite Forall_forall; intros; rewrite edge_func_spec in H11; destruct H11; auto). simpl. destruct (filterE (edge_func g x)) eqn:? . + specialize (H5 _ H8 H9 H10). destruct H5; auto. clear IHn. apply reachable_by_ind in H5. destruct H5. * subst x. assert (vvalid g (dst g e) /\ In e (edge_func g (src g e))) by (split; auto; rewrite edge_func_spec; split; auto). rewrite <- filter_valid in H5; auto. rewrite Heql in H5. inversion H5. * destruct H5 as [z [[? [? ?]] ?]]. rewrite step_spec in H12. destruct H12 as [e' [? [? ?]]]. assert (vvalid g (dst g e') /\ In e' (edge_func g x)) by (split; [rewrite H15 | rewrite edge_func_spec; split]; auto). rewrite <- filter_valid in H16; auto. rewrite Heql in H16. inversion H16. + specialize (IHn len (dst g e0) ((e0, dst g e0) :: r)). assert (In e0 (e0 :: l)) by (simpl; left; auto). rewrite <- Heql in H11. rewrite filter_valid in H11; auto. destruct H11. rewrite edge_func_spec in H12. destruct H12. assert (g |= x ~> (dst g e0)) by (apply reachable_foot_valid in H3; split; [|split; [|exists e0]]; auto). apply IHn; clear IHn; auto. * simpl. clear -H1. intuition. * apply reachable_edge with x; auto. * simpl. apply NoDup_cons; auto. apply H7; auto. rewrite H13. apply reachable_refl. apply reachable_foot_valid in H3; auto. * intros. specialize (H5 _ H15 H16 H17). destruct H5. -- apply reachable_by_ind in H5. destruct H5. ++ assert (e1 = e0) by (apply (H0 x); auto). subst e1. simpl. right; left; auto. ++ destruct H5 as [z [? ?]]. pose proof (is_list_edge_dst_the_same _ _ _ _ _ H H3 H5 H14). subst z. apply reachable_by_is_reachable in H18; left; auto. -- right. simpl. right. auto. * simpl. intros. destruct H15. -- subst e1. rewrite H13. split; [|split]; auto. -- apply H6; auto. * intros. simpl. intro. destruct H18. -- subst e1. rewrite H13 in H16. apply (is_list_no_edge_loop g root x (dst g e0)); auto. -- revert H18. apply H7; auto. apply edge_reachable with (dst g e0); 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