proposition: Lemma math_graph_join': forall (g: PreGraph V E) (PV1 PV2 PV: V -> Prop) (PE1 PE2 PE: E -> Prop), Prop_join PV1 PV2 PV -> Prop_join PE1 PE2 PE -> MathGraph' (gpredicate_subgraph PV1 PE1 g) is_null -> MathGraph' (gpredicate_subgraph PV2 PE2 g) is_null -> MathGraph' (gpredicate_subgraph PV PE g) is_null.
proof: Proof. intros. constructor. + simpl; intro; rewrite !Intersection_spec; intros. destruct H, H0. rewrite H0 in H3; destruct H3 as [? [? | ?]]. - pose proof valid_graph' (gpredicate_subgraph PV1 PE1 g) e. simpl in H7; unfold weak_valid in H7; simpl in H7; rewrite !Intersection_spec in H7. specialize (H7 (conj H3 H6)). rewrite !H. tauto. - pose proof valid_graph' (gpredicate_subgraph PV2 PE2 g) e. simpl in H7; unfold weak_valid in H7; simpl in H7; rewrite !Intersection_spec in H7. specialize (H7 (conj H3 H6)). rewrite !H. tauto. + simpl; intros. destruct H, H0. rewrite Intersection_spec, H in H3. destruct H3 as [? [? | ?]]. - apply (valid_not_null' (gpredicate_subgraph PV1 PE1 g) x); auto. simpl; rewrite Intersection_spec; auto. - apply (valid_not_null' (gpredicate_subgraph PV2 PE2 g) x); auto. simpl; rewrite Intersection_spec; auto. Qed.
imports: CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.relation_list CertiGraph.lib.Equivalence_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen