proposition: Lemma lstToG_gToLst_eq: forall (g: PreGraph Vertex Edge) (LF: LocalFiniteGraph g) (VVA: ValidVertexAccessible g) root (X: EnumCovered Vertex (reachable g root)), vvalid g root -> is_list g root -> (listToGraph (graphToList g VVA LF (length (proj1_sig X)) root)) ~=~ (predicate_subgraph g (reachable g root)).
proof: Proof. intros. hnf. split; [|split; [|split]]; intros; simpl. - unfold predicate_vvalid. rewrite <- list_vertices_vvalid_iff; simpl; auto. rewrite <- listVertices'_In_rev. split; intros. + destruct H1 as [? | [? | ?]]; [subst v; split; [| apply reachable_refl]; auto ..| ]. apply (toEdgeList_reachable g VVA LF root) in H1. * split; auto. apply reachable_foot_valid in H1; auto. * apply reachable_refl; auto. * intros. simpl in H2. exfalso; auto. + destruct (equiv_dec root v). 1: hnf in e; left; auto. compute in c. right; right. apply (reachable_toEdgeList _ _ _ root _ _ _ X); auto. * apply reachable_refl; auto. * simpl. apply NoDup_nil. * simpl. intros. exfalso; auto. * intros. exfalso; auto. * destruct H1; auto. - unfold predicate_evalid. rewrite <- list_edges_evalid_iff. simpl. cut (In e (listEdges' Vertex Edge (rev (toEdgeList g VVA LF (length (proj1_sig X), root, nil)))) <-> evalid g e /\ reachable g root (src g e) /\ reachable g root (dst g e)). 1: intros; intuition. rewrite <- listEdges'_In_rev. split; intros. + apply (toEdgeList_edge_reachable g VVA LF root) in H1; auto. * intros. simpl in H2; exfalso; auto. * apply reachable_refl; auto. + destruct H1 as [? [? ?]]. apply reachable_foot_valid in H3. apply (reachable_edge_toEdgeList _ _ _ root _ _ _ X); auto. * apply reachable_refl; auto. * simpl; apply NoDup_nil. * simpl; intros. exfalso; auto. - simpl in *. unfold predicate_evalid in H2. rewrite <- list_edges_evalid_iff in H1. simpl in H1. destruct H1. 1: exfalso; auto. apply (listToGraph'_NoDup_In_src (single_vertex_pregraph root) root) in H1. + destruct H1 as [v' [? ?]]. rewrite H3. apply shiftLeft_toEdgeList_In in H1; auto; intros. * simpl in H4. exfalso; auto. * inversion H4. + rewrite <- listEdges'_NoDup_rev. apply toEdgeList_edge_NoDup with root; auto. * apply reachable_refl; auto. * simpl. apply NoDup_nil. - simpl in *. unfold predicate_evalid in H2. rewrite <- list_edges_evalid_iff in H1. simpl in H1. destruct H1. 1: exfalso; auto. apply (listToGraph'_NoDup_In_dst (single_vertex_pregraph root) root) in H1. + destruct H1 as [v' [? ?]]. rewrite H3. rewrite <- in_rev in H1. apply toEdgeList_In in H1; auto. intros. simpl in H4. exfalso; auto. + rewrite <- listEdges'_NoDup_rev. apply toEdgeList_edge_NoDup with root; auto. * apply reachable_refl; auto. * simpl. apply NoDup_nil. 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