proposition: Lemma gen_dst_preserve_lst: forall x pa, ~ reachable g pa x -> vvalid g x -> LstGraph (pregraph_gen_dst g (out_edge x) pa) out_edge.
proof: Proof. intros. constructor. 1: simpl; apply only_one_edge. intro y; intros. destruct (in_dec EE (out_edge x) (snd p)). - destruct p as [p l]. simpl in i. apply (in_split_not_in_first EE) in i. destruct i as [l1 [l2 [? ?]]]. rewrite H2 in H1. apply reachable_by_path_app_cons in H1. destruct H1. simpl src in H1. simpl dst in H4. unfold updateEdgeFunc in H4. destruct (equiv_dec (out_edge x) (out_edge x)). 2: compute in c; exfalso; apply c; auto. clear e. rewrite no_edge_gen_dst_equiv in H1. 2: simpl; auto. pose proof (vvalid_src_evalid x H0). destruct H5. rewrite H5 in H1. destruct (in_dec EE (out_edge x) l2). + apply (in_split_not_in_last EE) in i. destruct i as [l3 [l4 [? ?]]]. rewrite H7 in H4. apply reachable_by_path_app_cons in H4. destruct H4 as [_ ?]. simpl in H4. unfold updateEdgeFunc in H4. destruct (equiv_dec (out_edge x) (out_edge x)). 2: compute in c; exfalso; apply c; auto. clear e. rewrite no_edge_gen_dst_equiv in H4. 2: simpl; auto. pose proof (reachable_by_path_merge _ _ _ _ _ _ _ H4 H1). apply reachable_by_path_is_reachable in H9. exfalso; auto. + rewrite no_edge_gen_dst_equiv in H4. 2: simpl; auto. pose proof (reachable_by_path_merge _ _ _ _ _ _ _ H4 H1). apply reachable_by_path_is_reachable in H7. exfalso; auto. - rewrite no_edge_gen_dst_equiv in H1; auto. apply no_loop_path in H1. 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.MathGraph CertiGraph.graph.FiniteGraph