proposition: Lemma shiftLeft_toEdgeList_In: forall root len x r, (forall v e, In (v, e) (shiftLeft Vertex Edge root (rev r)) -> v = src g e) -> (r = nil -> x = root) -> (forall e v l, r = (e, v) :: l -> x = v) -> forall e v, In (v, e) (shiftLeft Vertex Edge root (rev (toEdgeList (len, x, r)))) -> v = src 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 H3; destruct (Compare_dec.le_dec len (length r)). - apply H0; auto. - exfalso; intuition. - apply H0; auto. - simpl in H3. destruct (filterE (edge_func g x)) eqn:? . + 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 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. apply IHn; auto; clear IHn H4 H5. * simpl. clear -H. intuition. * intros. simpl in H4. destruct r. -- simpl in H4. assert (x = root) by (apply H1; auto). subst x. destruct H4. 2: exfalso; auto. inversion H4. subst e1. subst v0. auto. -- destruct p as [e' v']. simpl in H4. assert (x = v') by (apply (H2 e' v' r); auto). subst v'. rewrite shiftLeft_app in H4. rewrite tailVertex_foot in H4. destruct H4. ++ simpl in H0. apply H0 in H4; auto. ++ simpl in H4. destruct H4. 2: exfalso; auto. inversion H4. subst v0. subst e1. auto. * intros. inversion H4. * intros. inversion H4. 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