proposition: Lemma pregraph_join_partial_si: forall PV PE (G1 G2: Graph) PV1, pregraph_join PV PE G1 G2 -> Disjoint _ PV PV1 -> (forall e, PE e -> evalid G2 e -> PV1 (src G2 e) -> False) -> (predicate_partialgraph G1 PV1) ~=~ (predicate_partialgraph G2 PV1).
proof: Proof. intros. destruct H as [[? ?] [[? ?] [? ?]]]. unfold Complement, Ensembles.In, weak_edge_prop. split; [| split; [| split]]. + simpl; intros. unfold predicate_vvalid. rewrite H. rewrite Disjoint_spec in H0; specialize (H0 v). tauto. + simpl; intros. unfold predicate_weak_evalid. split; intros. - assert (evalid G2 e) by (rewrite H3; tauto). rewrite <- H5 by tauto. tauto. - pose proof proj1 H7. rewrite H3 in H8; destruct H8. * rewrite H5 by tauto. tauto. * exfalso; apply (H1 e); tauto. + simpl; unfold predicate_weak_evalid; intros. apply H5; tauto. + simpl; unfold predicate_weak_evalid; intros. apply H6; tauto. 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