proposition: Lemma is_partial_make_set_pregraph: forall x (g: UFGraph), ~ vvalid g x -> is_partial_graph g (make_set_pregraph x g).
proof: Proof. intros. hnf. simpl. unfold addValidFunc, updateEdgeFunc. split; [|split; [|split]]; intros; [left; auto..| |]. - destruct (equiv_dec (x, tt) e); auto. hnf in e0. subst e. pose proof (@only_one_edge _ _ _ _ g _ (liGraph g) (src g (x, tt)) (x, tt) H1). simpl in H2. assert (src g (x, tt) = src g (x, tt) /\ evalid g (x, tt)) by (split; auto). rewrite H2 in H3. inversion H3. exfalso. rewrite H5 in H. intuition. - destruct (equiv_dec (x, tt) e); auto. hnf in e0. subst e. destruct (@valid_graph _ _ _ _ g _ (maGraph g) _ H0) as [? _]. pose proof (@only_one_edge _ _ _ _ g _ (liGraph g) (src g (x, tt)) (x, tt) H2). assert (src g (x, tt) = src g (x, tt) /\ evalid g (x, tt)) by (split; auto). rewrite H3 in H4. inversion H4. exfalso. rewrite H6 in H. intuition. Qed.
imports: Coq.Logic.Classical Coq.Lists.List Coq.Sets.Ensembles CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.EquivDec_ext CertiGraph.lib.Relation_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.weak_mark_lemmas CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.subgraph2 CertiGraph.graph.reachable_computable CertiGraph.graph.FiniteGraph CertiGraph.graph.MathGraph CertiGraph.graph.LstGraph CertiGraph.graph.UnionFind CertiGraph.msl_application.Graph CertiGraph.msl_application.UnionFindGraph