proposition: Lemma pregraph_iso_cons_vvalid: 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 v0 : VType, vvalid (reachable_sub_labeledgraph g1 (filter_sum_right roots1)) v0 -> vvalid (reachable_sub_labeledgraph g2 (filter_sum_right roots2)) (vmap12 v0).
proof: Proof. intros roots1 roots2 g1 g2 v vmap12 vmap21 emap12 emap21 lp_pregraph_iso Hrest. intros v0 Hv. pose proof (vvalid_reachable_sub_cons v Hv) as Hr1. destruct lp_pregraph_iso. simpl in *. unfold predicate_vvalid, predicate_evalid in *. hnf in *. destruct Hv as [Hv1 Hr]. destruct (vvalid_bij _ Hr1) as [Hv2 Hr2]. split; auto. destruct Hr2 as [s [Hin Hr2]]. simpl in Hin. destruct Hin as [Hin | Hin]. 2: (exists s; split; auto). subst s. destruct Hr as [s [Hin Hr]]. destruct Hr as [p Hr]. destruct p as [v' p]. destruct Hr as [[Hh Hf] [Hvp _]]. simpl in Hh. subst v'. exists (vmap12 s). split. 1: subst roots2; rewrite <- filter_sum_right_In_iff in Hin |- * ; rewrite in_map_iff; exists (inr s); split; auto. clear Hr2. destruct Hr1 as [_ Hr1]. revert dependent v0. induction p using rev_ind; intros. - simpl in Hf. subst v0. apply reachable_refl. assumption. - assert (valid_path g1 (s, p)) as Hvp1. { rewrite valid_path_app in Hvp. destruct Hvp; assumption. } pose proof (pfoot_split _ _ _ _ _ Hvp) as Hfs. assert (reachable_through_set g1 (v :: filter_sum_right roots1) (src g1 x)) as Hr1s. { exists s. split. 1: simpl; right; assumption. exists (s, p). split; split; simpl; auto. constructor; auto. simpl. rewrite Forall_forall. intros; auto. } assert (vvalid g1 (src g1 x)) as Hv1s. { apply valid_path_valid with (s, p); auto. apply pfoot_in. assumption. } destruct (vvalid_bij _ (conj Hv1s Hr1s)) as [Hv2s _]. specialize (IHp Hvp1 _ Hv1s Hfs Hr1s Hv2s). eapply reachable_edge; eauto. do 2 (split; auto). rewrite pfoot_last in Hf. subst v0. assert (evalid g1 x) as Hev1. { eapply valid_path_evalid. apply Hvp. rewrite in_app_iff. right. left. reflexivity. } pose proof (conj Hev1 (conj Hr1s Hr1)) as Hc. destruct (evalid_bij _ Hc) as [Hev2 _]. specialize (src_bij _ Hc). specialize (dst_bij _ Hc). econstructor; eauto. 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