proposition: Lemma lgd_semi_iso: forall (from to: nat) (g g1: LGraph) l1 v n e, from <> to -> sound_gc_graph g -> sound_gc_graph g1 -> graph_has_gen g1 to -> forward_p_compatible (inr (v, n)) nil g1 from -> vgeneration (dst g1 e) = from -> Znth n (make_fields g1 v) = inr e -> raw_mark (vlabel g1 (dst g1 e)) = true -> ~ vvalid g v -> no_dangling_dst g -> gc_graph_semi_iso g g1 from to l1 -> gc_graph_semi_iso g (labeledgraph_gen_dst g1 e (copied_vertex (vlabel g1 (dst g1 e)))) from to l1.
proof: Proof. intros from to g g1 l1 v n e H H0 H1 H2 H3 H4 H5 H6 Hp H7 H8. simpl in H3. destruct H3 as [? [? [? ?]]]. assert (Hd: DoubleNoDup l1) by (now apply (semi_iso_DoubleNoDup g g1 from to)). destruct H8 as [? [? ?]]. destruct (split l1) as [from_l to_l] eqn: ?. destruct H13 as [[? ?] [[? [? ?]] ?]]. destruct H0 as [? [? [? Hels]]]. red in H0, H19, H20. destruct H1 as [? [? [? Hels1]]]. red in H1, H21, H22. assert (Hf: from_l = map fst l1) by (rewrite map_fst_split, Heqp; reflexivity). assert (Ht: to_l = map snd l1) by (now rewrite map_snd_split, Heqp). split3. - simpl. destruct H8 as [? [? [? ?]]]. split; [|split;[|split]]; intros; simpl; [now apply H8 | now apply H23 | now apply H24 | unfold updateEdgeFunc]. rewrite if_false; auto. intro. red in H28. subst e0. apply make_fields_Znth_edge in H5; auto. subst e. rewrite H19 in H26. destruct H26. simpl in H5. now rewrite <- H0 in H5. - intros. simpl. pose proof H12. rename H24 into Hi. specialize (H12 _ _ H23). destruct H12 as [? [? ?]]. split3; try easy. intros. specialize (H25 _ H26). unfold updateEdgeFunc. if_tac. 2: easy. red in H27. subst e. apply make_fields_Znth_edge in H5; auto. inversion H5. subst v. rewrite <- H29 in *. assert (vvalid g v1). { apply In_map_fst in H23. rewrite map_fst_split, Heqp, <- H14 in H23. now destruct H23 as [_ [? _]]. } assert (dst g1 (v2, idx) = dst g (v1, idx) -> In (dst g (v1, idx)) from_l). { intros. rewrite H28 in *. rewrite <- H14. do 2 (split; auto). red in H7. rewrite H0. apply (H7 v1). 2: now rewrite get_edges_In. now rewrite <- H0. } destruct_eq_dec (dst g1 (v2, idx)) (dst g (v1, idx)). + rewrite H30. apply H28 in H30. rewrite Hf, In_map_fst_iff in H30. destruct H30 as [b ?]. destruct (DoubleNoDup_list_bi_map _ _ _ Hd H30) as [? _]. rewrite H31. apply Hi in H30. destruct H30 as [? [? ?]]. subst b. now right. + destruct H25. 1: easy. exfalso. destruct (InEither_dec (dst g (v1, idx)) l1). 2: now rewrite list_bi_map_not_In in H25. red in i. rewrite Heqp, in_app_iff in i. destruct i. * rewrite Hf, In_map_fst_iff in H31. destruct H31 as [b ?]. destruct (DoubleNoDup_list_bi_map _ _ _ Hd H31) as [? _]. rewrite H32 in H25. rewrite <- H25 in H31. apply In_map_snd in H31. rewrite <- Ht in H31. apply H17 in H31. now rewrite H4 in H31. * rewrite H16 in H31. destruct H31. red in H7. apply H32. rewrite H0. apply (H7 v1); [now rewrite <- H0 | now rewrite get_edges_In]. - rewrite Heqp. split; [|split]; [split; auto..|]. intros; simpl; now apply H18. 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