proposition: Lemma initializing_item_list_inc: forall size capacity : Z, 0 <= size < capacity -> upd_Znth size (initializing_item_list size capacity) (Vint (Int.repr size), (Vzero, Vzero)) = initializing_item_list (size + 1) capacity.
proof: Proof. unfold initializing_item_list. intros. rewrite upd_Znth_app2. 1,2: rewrite Zlength_map, Zlength_initial_item_list. 3: rewrite (Zlength_default_val_array t_item); lia. 2,3: lia. rewrite Z.sub_diag. apply List_ext.list_eq_Znth. rewrite Zlength_app, Zlength_app, Zlength_upd_Znth, Zlength_map, Zlength_map. rewrite (Zlength_default_val_array t_item), (Zlength_default_val_array t_item). rewrite Zlength_initial_item_list, Zlength_initial_item_list. 1-5: lia. rewrite Zlength_app, Zlength_upd_Znth, Zlength_map. rewrite Zlength_initial_item_list, (Zlength_default_val_array t_item). 2,3: lia. replace (size + (capacity - size)) with capacity by lia. intros. assert (i < size \/ size <= i) by lia. destruct H1. rewrite Znth_app1, Znth_app1. rewrite Znth_map, Znth_map. rewrite initial_item_list_i, initial_item_list_i. trivial. 5,6: rewrite Zlength_map. 3-6: rewrite Zlength_initial_item_list. 1-10: lia. rewrite Znth_app2. 1,2 : rewrite Zlength_map, Zlength_initial_item_list. 2-4: lia. assert (i = size \/ size < i) by lia. destruct H2. subst i. rewrite Znth_app1. rewrite Znth_map, Z.sub_diag, Znth_upd_Znth_same, initial_item_list_i. trivial. 2: rewrite (Zlength_default_val_array t_item). 6: rewrite Zlength_map. 5,6: rewrite Zlength_initial_item_list. 1-8: lia. rewrite Znth_app2. 1,2: rewrite Zlength_map, Zlength_initial_item_list. rewrite Znth_upd_Znth_diff. unfold default_val. simpl. unfold Zrepeat. rewrite Znth_repeat_inrange, Znth_repeat_inrange; trivial. all: lia. Qed.
imports: RelationClasses VST.floyd.proofauto CertiGraph.lib.List_ext CertiGraph.binheap.binary_heap_pro CertiGraph.binheap.binary_heap_malloc_spec CertiGraph.binheap.binary_heap_model CertiGraph.binheap.binary_heap_Zmodel