proposition: Lemma pregraph_join_proper_aux: forall (PV1 PV2: V -> Prop) (PE1 PE2: E -> Prop) (G11 G12 G21 G22: Graph), Same_set PV1 PV2 -> Same_set PE1 PE2 -> G11 ~=~ G12 -> G21 ~=~ G22 -> pregraph_join PV1 PE1 G11 G21 -> pregraph_join PV2 PE2 G12 G22.
proof: Proof. intros. split; [| split; [| split]]; intros. + eapply Prop_join_proper; [.. | apply (proj1 H3)]; symmetry; auto. - rewrite Same_set_spec; destruct H1; auto. - rewrite Same_set_spec; destruct H2; auto. + eapply Prop_join_proper; [.. | apply (proj1 (proj2 H3))]; symmetry; auto. - rewrite Same_set_spec; destruct H1 as [_ [? _]]; auto. - rewrite Same_set_spec; destruct H2 as [_ [? _]]; auto. + assert (evalid G11 e) by (rewrite (proj1 (proj2 H1)); auto). assert (evalid G21 e) by (rewrite (proj1 (proj2 H2)); auto). rewrite <- (proj1 (proj2 (proj2 H1))) by auto. rewrite <- (proj1 (proj2 (proj2 H2))) by auto. apply (proj1 (proj2 (proj2 H3))); auto. + assert (evalid G11 e) by (rewrite (proj1 (proj2 H1)); auto). assert (evalid G21 e) by (rewrite (proj1 (proj2 H2)); auto). rewrite <- (proj2 (proj2 (proj2 H1))) by auto. rewrite <- (proj2 (proj2 (proj2 H2))) by auto. apply (proj2 (proj2 (proj2 H3))); auto. Qed.
imports: Coq.Logic.ProofIrrelevance Coq.Sets.Ensembles Coq.Sets.Finite_sets Coq.Classes.Morphisms CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.relation_list CertiGraph.lib.List_ext CertiGraph.lib.Equivalence_ext CertiGraph.lib.EquivDec_ext VST.msl.Coqlib2 Coq.Lists.List CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_ind CertiGraph.graph.graph_gen