proposition: Lemma toEdgeList_edge_NoDup: forall root len x r, is_list g root -> reachable g root x -> NoDup (listEdges' Vertex Edge r) -> (forall e, In e (listEdges' Vertex Edge r) -> ~ reachable g x (src g e)) -> NoDup (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. induction n; intros; simpl; unfold lengthInput in H0; rewrite toEdgeList_unfold; destruct (Compare_dec.le_dec len (length r)); auto. - exfalso; intuition. - simpl. destruct (filterE (edge_func g x)) eqn:?; auto. specialize (IHn len (dst g e) ((e, dst g e) :: r)). assert (In e (e :: l)) by (simpl; left; auto). rewrite <- Heql in H4. rewrite filter_valid in H4. 2: rewrite Forall_forall; intros; rewrite edge_func_spec in H5; destruct H5; auto. destruct H4. rewrite edge_func_spec in H5. destruct H5. assert (g |= x ~> (dst g e)) by (hnf; rewrite step_spec; apply reachable_foot_valid in H1; intuition; exists e; intuition). apply IHn; clear IHn; auto; simpl. + intuition. + apply reachable_edge with x; auto. + apply NoDup_cons; auto. intro. apply H3 in H8. apply H8. rewrite H6. apply reachable_refl. apply reachable_foot_valid in H1. auto. + simpl. intros. destruct H8. * subst e0. rewrite H6. intro. apply (is_list_no_edge_loop _ root) in H8; auto. * intro. apply H3 in H8. apply H8. apply edge_reachable with (dst g e); 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