proposition: Lemma si_stronger_partialgraph: forall (g1 g2: PreGraph V E) (p1 p2 p1' p2' p: V -> Prop), (forall v, p1' v <-> p1 v /\ p v) -> (forall v, p2' v <-> p2 v /\ p v) -> (predicate_partialgraph g1 p1) ~=~ (predicate_partialgraph g2 p2) -> (predicate_partialgraph g1 p1') ~=~ (predicate_partialgraph g2 p2').
proof: Proof. intros. destruct H1 as [? [? [? ?]]]. split; [| split; [| split]]. + intro v; specialize (H1 v); specialize (H0 v); specialize (H v); simpl in H1 |- *. unfold predicate_vvalid in H1 |- *. tauto. + intro e; specialize (H2 e); specialize (H3 e); specialize (H (src g1 e)); specialize (H0 (src g2 e)); simpl in H2, H3 |- *. unfold predicate_weak_evalid in H2, H3 |- *. clear H4. split; intros; destruct H4. - rewrite H in H5. destruct H5. assert (evalid g1 e /\ p1 (src g1 e)) by auto. specialize (H3 H7). rewrite H2 in H7. specialize (H3 H7). rewrite <- H3 in *. tauto. - rewrite H0 in H5. destruct H5. assert (evalid g2 e /\ p2 (src g2 e)) by auto. assert (evalid g1 e /\ p1 (src g1 e)) by tauto. specialize (H3 H8 H7). rewrite H3 in *. rewrite H. tauto. + simpl in *. unfold predicate_weak_evalid in *. intros. rewrite H in H5. rewrite H0 in H6. apply H3; tauto. + simpl in *. unfold predicate_weak_evalid in *. intros. rewrite H in H5. rewrite H0 in H6. apply H4; 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