proposition: Lemma uf_union_vvalid: forall (g1 g2: PreGraph Vertex Edge) (li1 : LstGraph g1 out_edge) (li2 : LstGraph g2 out_edge) (fin1: FiniteGraph g1) (fin2: FiniteGraph g2) (ma1: MathGraph g1 is_null) (ma2: MathGraph g2 is_null) u v x, vvalid g1 u -> vvalid g1 v -> uf_union g1 u v g2 -> vvalid g1 x <-> vvalid g2 x.
proof: Proof. intros. pose proof (uf_union_create_precons g1 _ _ _ _ _ H H0). destruct H2 as [u_rt [v_rt [? [? [? [? [? ?]]]]]]]. split; intros. - pose proof (vvalid_get_ufroot g1 _ _ H8). destruct H9 as [x_rt ?]. destruct (EV x_rt u_rt). { rewrite e in *. assert (ufroot_same g1 u x). { exists u_rt; split; trivial. } apply (uf_union_affected_vvalid g1 g2 _ _ _ _ _ H4 H5); trivial. } destruct (EV x_rt v_rt). { rewrite e in *. assert (ufroot_same g1 v x). { exists v_rt; split; trivial. } apply (uf_union_affected_vvalid g1 g2 _ _ _ _ _ H5 H4); trivial. apply uf_union_sym; trivial. } assert (ufroot_same g1 x x). { apply (ufroot_same_refl g1 li1); trivial. } apply (uf_union_unaffected_vvalid g1 g2 _ _ _ _ _ _ H4 H5 H10 H6 H7); trivial. + intro. apply (same_set_contra _ _ _ x H11); trivial. intro. apply (ufroot_same_false g1 _ _ _ _ _ H9 H2 c); trivial. apply ufroot_same_symm; trivial. + intro. apply (same_set_contra _ _ _ x H11); trivial. intro. apply (ufroot_same_false g1 _ _ _ _ _ H9 H3 c0); trivial. apply ufroot_same_symm; trivial. + apply (ufroot_uf_set_in g1 li1 x x_rt); trivial. - pose proof (vvalid_get_ufroot g2 _ _ H8). destruct H9 as [x_rt ?]. assert (uf_set_in g2 (ufroot_same g2 x)). { apply (ufroot_uf_set_in g2 li2 _ x_rt); trivial. } assert (ufroot_same g2 x x). { apply (ufroot_same_refl g2 li2); trivial. } apply (uf_union_backwards_cases _ _ _ _ _ _ _ _ H4 H5 H6 H7 H11) in H1; trivial. destruct H1. + apply Ensembles.Extensionality_Ensembles in H1. rewrite H1 in H11. apply Constructive_sets.Union_inv in H11. destruct H11 as [[? [_ ?]] | [? [_ ?]]]; apply (ufroot_vvalid_vert _ x0); trivial. + destruct H1 as [? | [? [? ?]]]. * exfalso. apply (inhabited_set_nonempty _ _ _ H11 H1). * apply (ufroot_vvalid_vert _ x0). apply H12, (ufroot_same_refl g2 li2); trivial. Qed.
imports: CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.Ensembles_ext CertiGraph.lib.EnumEnsembles CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.MathGraph CertiGraph.graph.LstGraph CertiGraph.graph.FiniteGraph CertiGraph.graph.reachable_computable