proposition: Lemma lmc_unmarked_gen_size: forall g v v', graph_has_v g v -> raw_mark (vlabel g v) = false -> unmarked_gen_size g (vgeneration v) = unmarked_gen_size (lgraph_mark_copied g v v') (vgeneration v) + vertex_size g v.
proof: Proof. intros. unfold unmarked_gen_size. unfold nth_gen. simpl glabel. destruct v as [gen index]. simpl vgeneration. change (nth gen (g_gen (glabel g)) null_info) with (nth_gen g gen). remember (nat_inc_list (number_of_vertices (nth_gen g gen))). rewrite (fold_left_ext (vertex_size_accum (lgraph_mark_copied g (gen, index) v') gen) (vertex_size_accum g gen)). - simpl. remember (fun i : nat => negb (raw_mark (vlabel g (gen, i)))) as f1. remember (fun i : nat => negb (raw_mark (update_copied_old_vlabel g (gen, index) v' (gen, i)))) as f2. cut (Permutation (filter f1 l) (index :: filter f2 l)). + intros. rewrite (fold_left_comm _ _ (index :: filter f2 l)). 3: assumption. * simpl. rewrite <- vsa_fold_left. f_equal. * apply vsa_comm. + apply filter_singular_perm; subst. * intros. unfold update_copied_old_vlabel, update_vlabel. rewrite if_false. 1: reflexivity. unfold equiv. intro. apply H2. inversion H3. reflexivity. * rewrite nat_inc_list_In_iff. destruct H. simpl in *. assumption. * unfold update_copied_old_vlabel, update_vlabel. rewrite if_true; reflexivity. * rewrite H0. reflexivity. * apply nat_inc_list_NoDup. - intros. unfold vertex_size_accum. f_equal. unfold vertex_size. f_equal. simpl. unfold update_copied_old_vlabel, update_vlabel. if_tac. 2: reflexivity. simpl. unfold equiv in H2. rewrite H2. 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