proposition: Lemma toEdgeList_In: forall len x r, (forall e v, In (e, v) r -> v = dst g e) -> forall e v, In (e, v) (toEdgeList (len, x, r)) -> v = dst g e.
proof: Proof. intros 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 H1; destruct (Compare_dec.le_dec len (length r)). - apply H0; auto. - exfalso; intuition. - apply H0; auto. - simpl in H1. destruct (filterE (edge_func g x)) eqn:? . + apply H0; auto. + specialize (IHn len (dst g e0) ((e0, dst g e0) :: r)). apply IHn; auto. * simpl. clear -H. intuition. * intros. simpl in H2. destruct H2. -- inversion H2. auto. -- apply H0; 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