proposition: Lemma si_subgraph_edge: forall (g1 g2: PreGraph V E) (p1 p2: V -> Prop), g1 ~=~ g2 -> (forall x, vvalid g1 x -> vvalid g2 x -> (p1 x <-> p2 x)) -> (forall x y, edge (predicate_subgraph g1 p1) x y <-> edge (predicate_subgraph g2 p2) x y).
proof: Proof. cut (forall (g1 g2: PreGraph V E) (p1 p2: V -> Prop), g1 ~=~ g2 -> (forall x, vvalid g1 x -> vvalid g2 x -> (p1 x <-> p2 x)) -> (forall x y, edge (predicate_subgraph g1 p1) x y -> edge (predicate_subgraph g2 p2) x y)). 1: intros; split; apply H; auto; symmetry; auto. intros. unfold edge in *; rewrite !@step_spec in *. destruct H1 as [? [? [e [? [? ?]]]]]. simpl in *. unfold predicate_vvalid, predicate_evalid in *. destruct H as [? [? [? ?]]]. pose proof H0 x. pose proof H0 y. pose proof H x. pose proof H y. destruct H3 as [? [? ?]]. specialize (H7 e H3). specialize (H8 e H3). assert (evalid g2 e) by (rewrite <- H6; auto). specialize (H7 H15). specialize (H8 H15). split; [tauto |]. split; [tauto |]. exists e. rewrite <- !H6. rewrite <- !H7. rewrite <- !H8. subst. repeat split; auto; try tauto. Qed.
imports: Coq.Arith.Arith Coq.Logic.ProofIrrelevance Coq.Logic.FunctionalExtensionality Coq.Classes.Morphisms Coq.Classes.Equivalence 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 CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_ind CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation