proposition: Lemma listEdges'_In_length_reachable {EV: EqDec V eq} {EE: EqDec E eq}: forall (g: PreGraph V E) root len r (X: EnumCovered V (reachable g root)), length (proj1_sig X) <= len -> NoDup (listEdges' r) -> len <= length r -> (forall e, In e (listEdges' r) -> evalid g e /\ reachable g root (src g e) /\ vvalid g (dst g e)) -> (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) -> forall e, evalid g e -> reachable g root (src g e) -> vvalid g (dst g e) -> In e (listEdges' r).
proof: Proof. intros. destruct X as [pl [? ?]]. simpl in H. unfold Ensembles.In in i. remember (map (src g) (listEdges' r)). assert (incl l pl). { hnf; intros; subst l; rewrite in_map_iff in H7; destruct H7 as [e' [? ?]]. apply H2 in H8. destruct H8 as [? [? ?]]; rewrite H7 in H9; apply i; auto. } apply NoDup_Permutation_bis in H7; auto. - specialize (i _ H5). apply Permutation_sym in H7. apply (Permutation_in (src g e)) in H7; auto. subst l. rewrite in_map_iff in H7. destruct H7 as [e' [? ?]]. pose proof H8. apply H2 in H8. destruct H8 as [? [? ?]]. assert (e = e') by (apply (H3 (src g e)); auto). subst e; auto. - subst l. remember (listEdges' r) as l. clear Heql H7. induction l; simpl. 1: apply NoDup_nil. apply NoDup_cons. + clear IHl. intro. rewrite in_map_iff in H7. destruct H7 as [a' [? ?]]. assert (In a (a :: l)) by apply in_eq. assert (In a' (a :: l)) by (apply in_cons; auto). apply H2 in H9. apply H2 in H10. destruct H9 as [? [? ?]]. destruct H10 as [? [? ?]]. assert (a = a') by (apply (H3 (src g a)); auto). subst a'. rewrite NoDup_cons_iff in H0. destruct H0. clear -H0 H8. auto. + apply IHl. * rewrite NoDup_cons_iff in H0. destruct H0; auto. * intros. apply H2. simpl; right; auto. - clear -H H1 Heql. pose proof (map_length (src g) (listEdges' r)). rewrite <- Heql in *. rewrite listEdges'_length in H0. rewrite H0. intuition. 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