proposition: Lemma vertex_address_the_same: forall (g1 g2: LGraph) v, (forall v, g1.(vlabel) v = g2.(vlabel) v) -> map start_address g1.(glabel).(g_gen) = map start_address g2.(glabel).(g_gen) -> vertex_address g1 v = vertex_address g2 v.
proof: Proof. intros. unfold vertex_address. f_equal. - f_equal. unfold vertex_offset. f_equal. remember (vindex v). clear Heqn. induction n; simpl; auto. rewrite !pvs_S, IHn. f_equal. unfold vertex_size. rewrite H. reflexivity. - assert (forall gen, graph_has_gen g1 gen <-> graph_has_gen g2 gen). { intros. unfold graph_has_gen. cut (length (g_gen (glabel g1)) = length (g_gen (glabel g2))). - intros. rewrite H1. reflexivity. - do 2 rewrite <- (map_length start_address). rewrite H0. reflexivity. } unfold gen_start. do 2 if_tac; [|rewrite H1 in H2; contradiction.. |reflexivity]. unfold nth_gen. rewrite <- !(map_nth start_address), H0. reflexivity. Qed.
imports: Coq.ZArith.ZArith Coq.Program.Basics Coq.micromega.Lia 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 VST.zlist.list_solver CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen