proposition: Lemma gToLst_lstToG_eq': forall (g: PreGraph Vertex Edge) v l r len (H: vvalid g v) (LF: LocalFiniteGraph (listToGraph' g v l)) (VVA: ValidVertexAccessible (listToGraph' g v l)), length l + length r <= len -> NoDup (listVertices (v, l)) -> NoDup (listEdges (v, l)) -> (forall x e, In x (listVertices (v, l)) -> ~ out_edges g x e) -> toEdgeList (listToGraph' g v l) VVA LF (len, v, r) = rev l ++ r.
proof: Proof. intros g v l r len. remember (lengthInput (len, v, r)) as n. simpl in Heqn. assert (len - length r <= n) by lia. clear Heqn. revert g v l r len H. induction n; intros; simpl. + rewrite toEdgeList_unfold. destruct (Compare_dec.le_dec len (length r)). 2: exfalso; intuition. destruct l; simpl; auto. simpl in H1; exfalso; intuition. + rewrite toEdgeList_unfold. destruct (Compare_dec.le_dec len (length r)). destruct l; simpl; auto. simpl in H1; exfalso; intuition. simpl. destruct l; simpl. * destruct (filterE (edge_func g v)) eqn:?; auto. assert (In e (e :: l)) by (simpl; auto). rewrite <- Heql in H5. rewrite filter_valid, edge_func_spec in H5. exfalso. apply (H4 v e); simpl. 1: left; auto. hnf. destruct H5; auto. rewrite Forall_forall. intros. rewrite edge_func_spec in H6. destruct H6; auto. * destruct p as [e0 v0]. assert (In e0 (@filterE _ _ _ _ (listToGraph' (pregraph_add_whole_edge g e0 v v0) v0 l) VVA (@edge_func _ _ _ _ (listToGraph' (pregraph_add_whole_edge g e0 v v0) v0 l) LF v))). { rewrite filter_valid. 2: rewrite Forall_forall; intros; rewrite edge_func_spec in H5; destruct H5; auto. split. + apply listToGraph'_preserve_vvalid. rewrite listToGraph'_not_In_dst. * replace (dst (pregraph_add_whole_edge g e0 v v0) e0) with v0. apply addEdge_add_vvalid. symmetry. rewrite addEdge_dst_iff. right. auto. * unfold listEdges in H3 |-* ; simpl in H3 |-* ; rewrite NoDup_cons_iff in H3; destruct H3; auto. + rewrite edge_func_spec. split. 1: apply listToGraph'_preserve_evalid, addEdge_add_evalid. rewrite listToGraph'_not_In_src. * rewrite addEdge_src_iff. right; auto. * clear -H3. unfold listEdges in *. simpl in *. apply NoDup_cons_iff in H3. destruct H3; auto. } destruct (filterE (edge_func (listToGraph' (pregraph_add_whole_edge g e0 v v0) v0 l) v)) eqn: ?. 1: simpl in H5; intuition. assert (e = e0). { assert (In e (e :: l0)) by (simpl; auto). rewrite <- Heql0 in H6. rewrite filter_valid in H6. 2: rewrite Forall_forall; intros; rewrite edge_func_spec in H7; destruct H7; auto. destruct H6. rewrite edge_func_spec in H7. destruct H7. destruct (in_dec equiv_dec e (listEdges (v0, l))). + apply (listToGraph'_In_src (pregraph_add_whole_edge g e0 v v0)) in i. rewrite H8 in i. simpl in H2, i; rewrite NoDup_cons_iff in H2; destruct H2; exfalso; apply H2; simpl; auto. + apply listToGraph'_src in H8. rewrite addEdge_src_iff in H8. destruct H8 as [[[? ?] | [? ?]] | [? ?]]; [ | | exfalso]; auto. apply valid_e_are_in_list in H7. unfold listEdges in n. simpl in n. destruct H7. 2: exfalso; auto. simpl in H7. unfold addValidFunc in H7. destruct H7; auto. unfold out_edges in H4. specialize (H4 v e). exfalso. apply H4; [left|]; auto. } subst e. clear l0 Heql0 H5. remember (dst (listToGraph' (pregraph_add_whole_edge g e0 v v0) v0 l) e0) as x. symmetry in Heqx. apply listToGraph'_dst in Heqx. destruct Heqx as [? | [? ?]]. 2: unfold listEdges in H5, H3; simpl in H5, H3; rewrite NoDup_cons_iff in H3; exfalso; intuition. rewrite addEdge_dst_iff in H5. destruct H5 as [[? ?] | [_ ?]]. 1: exfalso; tauto. subst x. rewrite <- app_assoc, <- app_comm_cons. simpl. rewrite IHn; auto. - simpl; intuition. - apply addEdge_add_vvalid. - simpl in H1 |-* ; intuition. - simpl in H2 |-* . rewrite NoDup_cons_iff in H2. destruct H2; auto. - clear -H3. unfold listEdges in *. simpl in *. rewrite NoDup_cons_iff in H3. destruct H3; auto. - intros xo eo ? ?. unfold out_edges in H4, H6. simpl in H6. unfold addValidFunc, updateEdgeFunc in H6. destruct H6. destruct (equiv_dec e0 eo). -- subst xo. simpl in H2. unfold listVertices in H5. rewrite NoDup_cons_iff in H2. destruct H2; intuition. -- compute in c. destruct H6; auto. specialize (H4 xo eo). apply H4; auto. simpl in H5 |-* . right; 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