proposition: Lemma pregraph_iso_cons_evalid: forall (roots1 roots2 : list root_t) (g1 g2 : LGraph) (v : VType) (vmap12 vmap21 : VType -> VType) (emap12 emap21 : EType -> EType), pregraph_isomorphism_explicit (reachable_sub_labeledgraph g1 (v :: filter_sum_right roots1)) (reachable_sub_labeledgraph g2 (vmap12 v :: filter_sum_right roots2)) vmap12 vmap21 emap12 emap21 -> roots2 = map (root_map vmap12) roots1 -> forall e : EType, evalid (reachable_sub_labeledgraph g1 (filter_sum_right roots1)) e -> evalid (reachable_sub_labeledgraph g2 (filter_sum_right roots2)) (emap12 e).
proof: Proof. intros roots1 roots2 g1 g2 v vmap12 vmap21 emap12 emap21 lp_pregraph_iso Hrest. intros e He1v. pose proof (evalid_reachable_sub_cons v He1v) as Hersd. hnf in *. destruct He1v as [He1v [Hr1s Hr1d]]. rewrite reachable_through_set_iff in Hr1s, Hr1d |- * . rewrite reachable_through_set_iff. pose proof (pregraph_iso_cons_vvalid lp_pregraph_iso Hrest _ Hr1s) as Hv2s. pose proof (pregraph_iso_cons_vvalid lp_pregraph_iso Hrest _ Hr1d) as Hv2d. destruct lp_pregraph_iso. simpl in *. unfold predicate_vvalid, predicate_evalid in *. destruct (evalid_bij _ Hersd) as [He2v _]. specialize (src_bij _ Hersd). specialize (dst_bij _ Hersd). rewrite <- src_bij, <- dst_bij. split; [|split]; auto. Qed.
imports: Coq.ZArith.ZArith Coq.Program.Basics compcert.lib.Integers compcert.common.Values VST.veric.base VST.veric.Clight_lemmas VST.veric.val_lemmas VST.veric.shares VST.msl.seplog VST.msl.shares VST.zlist.sublist VST.floyd.coqlib3 VST.floyd.functional_base VST.floyd.data_at_rec_lemmas CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.path_lemmas CertiGraph.graph.subgraph2 CertiGraph.graph.graph_relation CertiGraph.graph.graph_isomorphism CertiGraph.graph.reachable_ind CertiGraph.CertiGC.GCGraph